Functions · easy

Statement, exactly as the model and Lean see it

theorem lg_target {α β γ : Type*} (f : α → β) (g : β → γ) (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (g ∘ f) := by

Source: Written for LeanGraph, reference proof certified
Premises used by the reference proof: 0

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Verified2 model calls · 2 Lean checks · $0.00029

Plan

To prove that the composition `g ∘ f` is injective, given that both `f` and `g` are injective, we proceed by assuming two inputs `a` and `b` such that `(g ∘ f) a = (g ∘ f) b`. Using the definition of composition, this means `g (f a) = g (f b)`. Since `g` is injective, this implies `f a = f b`. Then, since `f` is also injective, it follows that `a = b`. Thus, `g ∘ f` is injective. Here's the Lean 4 proof skeleton using tactics: In this skeleton: - `intros a b h` introduces variables `a`, `b`, and the hypothesis `h : g (f a) = g (f b)`. - `have hf_eq : f a = f b := by apply hg at h; exact h` uses the injectivity of `g` to derive that `f a = f b`. - `have hfinal : a = b := by apply hf at hf_eq; exact hf_eq` uses the injectivity of `f` to conclude `a = b`. - `exact hfinal` completes the proof.

Skeleton — Lean accepts it with only sorry steps left

intros a b h
have hf_eq : f a = f b := by apply hg at h; exact h
have hfinal : a = b := by apply hf at hf_eq; exact hf_eq
exact hfinal

Attempts

sample 0 · round 0Verified1.8 s model time

Proof

intros a b h
have hf_eq : f a = f b := by apply hg at h; exact h
have hfinal : a = b := by apply hf at hf_eq; exact hf_eq
exact hfinal

Verified proof

theorem lg_target {α β γ : Type*} (f : α → β) (g : β → γ) (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (g ∘ f) := by
  intros a b h
  have hf_eq : f a = f b := by apply hg at h; exact h
  have hfinal : a = b := by apply hf at hf_eq; exact hf_eq
  exact hfinal

Axioms used: none

Reference proof

The proof we wrote and certified before any model ran.

exact hg.comp hf