awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun (s : Set T) ↦ Sigma.mk (β := f) U (cast ⋯ s)
s t : Set T
h : g s = g t
⊢ s = t
have suffices : cast hU ((g s).snd (β := f)) = cast hU ((g t).snd (β := f))
Tactic: suffices cast hU (g s).2 = cast hU (g t).2 by
      simp only [g, cast_cast, cast_eq] at this
      assumption
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun (s : Set T) ↦ Sigma.mk (β := f) U (cast ⋯ s)
⊢ False
have hg : Injective g
Tactic: have hg : Injective g := by
    intro s t h
    suffices cast hU (g s).2 = cast hU (g t).2 by
      simp only [g, cast_cast, cast_eq] at this
      assumption
    · congr
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
⊢ False
have x : ∃ (a : α), f a = Set T
Tactic: cases hf (Set T) with | intro U hU =>
  let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩
  have hg : Injective g := by
    intro s t h
    suffices cast hU (g s).2 = cast hU (g t).2 by
      simp only [g, cast_cast, cast_eq] at this
      assumption
    · congr
  exact cantor_injective g hg
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : β → α
h : β → γ
i : γ → β
hf : LeftInverse f g
hh : LeftInverse h i
a : γ
⊢ h (f (g (i a))) = a
have rw : h (i a) = a
Tactic: rw [hf (i a), hh a]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : β → α
h : β → γ
i : γ → β
hf : LeftInverse f g
hh : LeftInverse h i
a : γ
rw : h (i a) = a
⊢ h (f (g (i a))) = a
have rw₁ : a = a
Tactic: rw [hf (i a), hh a]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ = g₁ ∘ f ∘ g₂
have rw : g₁ = g₁ ∘ id
Tactic: rw [h₂.comp_eq_id, comp_id]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
rw : g₁ = g₁ ∘ id
⊢ g₁ = g₁ ∘ f ∘ g₂
have rw₁ : g₁ = g₁
Tactic: rw [h₂.comp_eq_id, comp_id]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ ∘ f ∘ g₂ = g₂
have rw : (g₁ ∘ f) ∘ g₂ = g₂
Tactic: rw [← comp_assoc, h₁.comp_eq_id, id_comp]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
rw : (g₁ ∘ f) ∘ g₂ = g₂
⊢ g₁ ∘ f ∘ g₂ = g₂
have rw₁ : id ∘ g₂ = g₂
Tactic: rw [← comp_assoc, h₁.comp_eq_id, id_comp]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
rw : (g₁ ∘ f) ∘ g₂ = g₂
rw₁ : id ∘ g₂ = g₂
⊢ g₁ ∘ f ∘ g₂ = g₂
have rw₂ : g₂ = g₂
Tactic: rw [← comp_assoc, h₁.comp_eq_id, id_comp]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ∃ (a : α), f a = b
hpi₁ : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h'₁ : ∃ (a : α), f a = b
⊢ f a = b
have h₁ : some (Classical.choose (p := fun (x : α) ↦ f x = b) h'₁) = some a
Tactic: rw [hpi, dif_pos h'] at h
Cleared hypotheses: h, hpi, h'
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ∃ (a : α), f a = b
h : some (Classical.choose (p := fun (x : α) ↦ f x = b) h') = some a
⊢ f a = b
have h₁ : Classical.choose (p := fun (x : α) ↦ f x = b) h' = a
Tactic: injection h with h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ∃ (a : α), f a = b
h : Classical.choose (p := fun (x : α) ↦ f x = b) h' = a
⊢ f a = b
have subst : f (Classical.choose (p := fun (x : α) ↦ f x = b) h') = b
Tactic: subst h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ¬∃ (a : α), f a = b
⊢ f a = b
have h₁ : none = some a
Tactic: rw [hpi, dif_neg h'] at h
Cleared hypotheses: h, hpi, h'
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = f (g b)
have rw : f (invFun f b) = b
Tactic: rw [hg b]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
β : Sort v
γ : Sort w
inst : Nonempty α
g : β → γ
⊢ (Surjective (β := α → γ) fun (x : α → β) ↦ g ∘ x) ↔ Surjective g
have refine : ∀ (h : Surjective (β := α → γ) fun (x : α → β) ↦ g ∘ x) (c : γ) (a : α), ∃ (a : β), g a = c
Tactic: refine ⟨fun h c ↦ Nonempty.elim ‹_› fun a ↦ ?_, (·.comp_left)⟩
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
β : Sort v
γ : Sort w
inst : Nonempty α
g : β → γ
h : Surjective (β := α → γ) fun (x : α → β) ↦ g ∘ x
c : γ
a : α
⊢ ∃ (a : β), g a = c
have have : ∀ (f : α → β) (hf : Eq (α := α → γ) ((fun (x : α → β) ↦ g ∘ x) f) fun (x : α) ↦ c), ∃ (a : β), g a = c
Tactic: have ⟨f, hf⟩ := h fun _ ↦ c
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
inst : DecidableEq α
β : Sort u_1
f : α → β
a' : α
b : β
a : α
⊢ update (β := fun (a : α) ↦ β) f a' b a = if a = a' then b else f a
have inl : update (β := fun (a : α) ↦ β) f a b a = if a = a then b else f a
Tactic: rcases Decidable.eq_or_ne a a' with rfl | hne
Cleared hypotheses: a'
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
inst : DecidableEq α
β : Sort u_1
f : α → β
a' : α
b : β
a : α
inl : update (β := fun (a : α) ↦ β) f a b a = if a = a then b else f a
⊢ update (β := fun (a : α) ↦ β) f a' b a = if a = a' then b else f a
have inr : ∀ (hne : a ≠ a'), update (β := fun (a : α) ↦ β) f a' b a = if a = a' then b else f a
Tactic: rcases Decidable.eq_or_ne a a' with rfl | hne
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update (β := β) f a' v = update (β := β) f a' v'
⊢ v = v'
have this : update (β := β) f a' v a' = update (β := β) f a' v' a'
Tactic: have := congr_fun h a'
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update (β := β) f a' v = update (β := β) f a' v'
this : update (β := β) f a' v a' = update (β := β) f a' v' a'
⊢ v = v'
have rwa : ∀ (this : v = update (β := β) f a' v' a'), v = v'
Tactic: rwa [update_self, update_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update (β := β) f a' v = update (β := β) f a' v'
this : update (β := β) f a' v a' = update (β := β) f a' v' a'
rwa : ∀ (this : v = update (β := β) f a' v' a'), v = v'
⊢ v = v'
have rwa₁ : ∀ (this : v = v'), v = v'
Tactic: rwa [update_self, update_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∀ (x : α), p x (update (β := β) f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
have rw : (p a b ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update (β := β) f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
Tactic: rw [← and_forall_ne a, update_self]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∃ (x : α), p x (update (β := β) f a b x)) ↔ p a b ∨ ∃ (x : α), x ≠ a ∧ p x (f x)
have rw : ¬(¬p a b ∧ ∀ (x : α), x ≠ a → ¬p x (f x)) ↔ p a b ∨ ∃ (x : α), x ≠ a ∧ p x (f x)
Tactic: rw [← not_forall_not, forall_update_iff f fun a b ↦ ¬p a b]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
ι : Sort u_1
inst : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
⊢ Pi.map (α := α) (β := β) f (update (β := α) g i a) = update (β := β) (Pi.map (α := α) (β := β) f g) i (f i a)
have h : ∀ (j : ι),
  Pi.map (α := α) (β := β) f (update (β := α) g i a) j = update (β := β) (Pi.map (α := α) (β := β) f g) i (f i a) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
ι : Sort u_1
inst : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
j : ι
⊢ Pi.map (α := α) (β := β) f (update (β := α) g i a) j = update (β := β) (Pi.map (α := α) (β := β) f g) i (f i a) j
have h : ∀ (a : α j),
  Pi.map (α := α) (β := β) f (update (β := α) g j a) j = update (β := β) (Pi.map (α := α) (β := β) f g) j (f j a) j
Tactic: obtain rfl | hij := eq_or_ne j i
Cleared hypotheses: i, a
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
ι : Sort u_1
inst : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
j : ι
h :
  ∀ (a : α j),
    Pi.map (α := α) (β := β) f (update (β := α) g j a) j = update (β := β) (Pi.map (α := α) (β := β) f g) j (f j a) j
⊢ Pi.map (α := α) (β := β) f (update (β := α) g i a) j = update (β := β) (Pi.map (α := α) (β := β) f g) i (f i a) j
have h₁ : ∀ (hij : j ≠ i),
  Pi.map (α := α) (β := β) f (update (β := α) g i a) j = update (β := β) (Pi.map (α := α) (β := β) f g) i (f i a) j
Tactic: obtain rfl | hij := eq_or_ne j i
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
⊢ x = y
have have : ∀ (this : Inhabited ((i : ι) → α i)), x = y
Tactic: have : Inhabited (∀ i, α i) := ⟨fun _ => Classical.choice inferInstance⟩
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ x = y
have refine_2 : ∀ (h : update (β := α) default i x = update (β := α) default i y), x = y
Tactic: replace h := @h (Function.update default i x) (Function.update default i y) ?_
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
refine_2 : ∀ (h : update (β := α) default i x = update (β := α) default i y), x = y
⊢ x = y
have refine_1 : Pi.map (α := α) (β := β) f (update (β := α) default i x) = Pi.map (α := α) (β := β) f (update (β := α) default i y)
Tactic: replace h := @h (Function.update default i x) (Function.update default i y) ?_
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ Pi.map (α := α) (β := β) f (update (β := α) default i x) = Pi.map (α := α) (β := β) f (update (β := α) default i y)
have refine_1 : update (β := β) (Pi.map (α := α) (β := β) f default) i (f i x) =
  Pi.map (α := α) (β := β) f (update (β := α) default i y)
Tactic: rw [Pi.map_update, Pi.map_update, hxy]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
refine_1 :
  update (β := β) (Pi.map (α := α) (β := β) f default) i (f i x) =
    Pi.map (α := α) (β := β) f (update (β := α) default i y)
⊢ Pi.map (α := α) (β := β) f (update (β := α) default i x) = Pi.map (α := α) (β := β) f (update (β := α) default i y)
have refine_1₁ : update (β := β) (Pi.map (α := α) (β := β) f default) i (f i x) =
  update (β := β) (Pi.map (α := α) (β := β) f default) i (f i y)
Tactic: rw [Pi.map_update, Pi.map_update, hxy]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
refine_1 :
  update (β := β) (Pi.map (α := α) (β := β) f default) i (f i x) =
    Pi.map (α := α) (β := β) f (update (β := α) default i y)
refine_1₁ :
  update (β := β) (Pi.map (α := α) (β := β) f default) i (f i x) =
    update (β := β) (Pi.map (α := α) (β := β) f default) i (f i y)
⊢ Pi.map (α := α) (β := β) f (update (β := α) default i x) = Pi.map (α := α) (β := β) f (update (β := α) default i y)
have refine_1₂ : update (β := β) (Pi.map (α := α) (β := β) f default) i (f i y) =
  update (β := β) (Pi.map (α := α) (β := β) f default) i (f i y)
Tactic: rw [Pi.map_update, Pi.map_update, hxy]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
⊢ x = y
have have : ∀ (this : Inhabited ((i : ι) → α i)), x = y
Tactic: classical
    have : Inhabited (∀ i, α i) := ⟨fun _ => Classical.choice inferInstance⟩
    replace h := @h (Function.update default i x) (Function.update default i y) ?_
    · simpa using congrFun h i
    rw [Pi.map_update, Pi.map_update, hxy]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
have have₁ have₂ : ∀ (this : Inhabited ((i : ι) → α i)), x = y
⊢ x = y
have refine_2 : ∀ (this : Inhabited ((i : ι) → α i)) (h : update (β := α) default i x = update (β := α) default i y), x = y
Tactic: classical
    have : Inhabited (∀ i, α i) := ⟨fun _ => Classical.choice inferInstance⟩
    replace h := @h (Function.update default i x) (Function.update default i y) ?_
    · simpa using congrFun h i
    rw [Pi.map_update, Pi.map_update, hxy]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
have have₁ have₂ : ∀ (this : Inhabited ((i : ι) → α i)), x = y
refine_2 : ∀ (this : Inhabited ((i : ι) → α i)) (h : update (β := α) default i x = update (β := α) default i y), x = y
⊢ x = y
have refine_1 : ∀ (this : Inhabited ((i : ι) → α i)),
  Pi.map (α := α) (β := β) f (update (β := α) default i x) = Pi.map (α := α) (β := β) f (update (β := α) default i y)
Tactic: classical
    have : Inhabited (∀ i, α i) := ⟨fun _ => Classical.choice inferInstance⟩
    replace h := @h (Function.update default i x) (Function.update default i y) ?_
    · simpa using congrFun h i
    rw [Pi.map_update, Pi.map_update, hxy]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
inst : Decidable (∃ (a : α), f a = b)
⊢ extend f g e' b = if h : ∃ (a : α), f a = b then g (Classical.choose (p := fun (x : α) ↦ f x = b) h) else e' b
have unfold : Eq.{u_3} (α := γ) (if h : ∃ (a : α), f a = b then g (Classical.choose (p := fun (x : α) ↦ f x = b) h) else e' b)
  (if h : ∃ (a : α), f a = b then g (Classical.choose (p := fun (x : α) ↦ f x = b) h) else e' b)
Tactic: unfold extend
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ extend f g e' (f a) = g a
have simp : g (Classical.choose (p := fun (x : α) ↦ f x = f a) sorry) = g a
Tactic: simp only [extend_def, dif_pos, exists_apply_eq_apply]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ extend f g e' (f a) = g a
have simp : g (Classical.choose (p := fun (x : α) ↦ f x = f a) sorry) = g a
Tactic: classical
  simp only [extend_def, dif_pos, exists_apply_eq_apply]
  exact hf (Classical.choose_spec (exists_apply_eq_apply f a))
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
⊢ extend (f₂₃ ∘ f₁₂) g e' = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e'
have h : ∀ (a : α₃), extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
have pos : ∀ (h₃ : ∃ (b : α₂), f₂₃ b = a), extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
Tactic: by_cases h₃ : ∃ b, f₂₃ b = a
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
pos : ∀ (h₃ : ∃ (b : α₂), f₂₃ b = a), extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
have neg : ∀ (h₃ : ¬∃ (b : α₂), f₂₃ b = a), extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
Tactic: by_cases h₃ : ∃ b, f₂₃ b = a
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ∃ (b : α₂), f₂₃ b = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
have pos : ∀ (b : α₂), extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' (f₂₃ b)
Tactic: obtain ⟨b, rfl⟩ := h₃
Cleared hypotheses: a, h₃
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' (f₂₃ b)
have pos : extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
Tactic: rw [Injective.extend_apply h₂₃]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
have pos : ∀ (h₂ : ∃ (c : α₁), f₁₂ c = b), extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
Tactic: by_cases h₂ : ∃ c, f₁₂ c = b
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
pos : ∀ (h₂ : ∃ (c : α₁), f₁₂ c = b), extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
have neg : ∀ (h₂ : ¬∃ (c : α₁), f₁₂ c = b), extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
Tactic: by_cases h₂ : ∃ c, f₁₂ c = b
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ∃ (c : α₁), f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
have pos : ∀ (c : α₁), extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = extend f₁₂ g (e' ∘ f₂₃) (f₁₂ c)
Tactic: obtain ⟨c, rfl⟩ := h₂
Cleared hypotheses: b, h₂
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
c : α₁
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = extend f₁₂ g (e' ∘ f₂₃) (f₁₂ c)
have pos : extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = g c
Tactic: rw [h₁₂.extend_apply]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ (c : α₁), f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
have neg : ¬∃ (a : α₁), (f₂₃ ∘ f₁₂) a = f₂₃ b
Tactic: rw [extend_apply' _ _ _ h₂, extend_apply', comp_apply]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ (b : α₂), f₂₃ b = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
have neg : ¬∃ (a_1 : α₁), (f₂₃ ∘ f₁₂) a_1 = a
Tactic: rw [extend_apply' _ _ _ h₃, extend_apply']
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst : Nonempty γ
h : ∃ (e : β → γ), g = e ∘ f
x x_1 : α
hf : f x = f x_1
⊢ g x = g x_1
have rw : (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x =
  (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x_1
Tactic: rw [Classical.choose_spec h, comp_apply, comp_apply, hf]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst : Nonempty γ
h : ∃ (e : β → γ), g = e ∘ f
x x_1 : α
hf : f x = f x_1
rw :
  (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x =
    (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x_1
⊢ g x = g x_1
have rw₁ : Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x) =
  (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x_1
Tactic: rw [Classical.choose_spec h, comp_apply, comp_apply, hf]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst : Nonempty γ
h : ∃ (e : β → γ), g = e ∘ f
x x_1 : α
hf : f x = f x_1
rw :
  (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x =
    (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x_1
rw₁ :
  Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x) =
    (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x_1
⊢ g x = g x_1
have rw₂ : Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x) =
  Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x_1)
Tactic: rw [Classical.choose_spec h, comp_apply, comp_apply, hf]