awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst_1 : DecidablePred p
hp : A.Definable L (setOf p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w : Option α → M | p (w ∘ some)}
hP : A.Definable L P
w : Option α → M
⊢ Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) w ↔
    w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
have pos : ∀ (h : p (w ∘ some)),
  Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) w ↔
    w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
Tactic: by_cases h : p (w ∘ some)
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst_1 : DecidablePred p
hp : A.Definable L (setOf p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w : Option α → M | p (w ∘ some)}
hP : A.Definable L P
w : Option α → M
pos :
  ∀ (h : p (w ∘ some)),
    Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) w ↔
      w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
⊢ Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) w ↔
    w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
have neg : ∀ (h : ¬p (w ∘ some)),
  Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) w ↔
    w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
Tactic: by_cases h : p (w ∘ some)
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (hypothesis)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f g : (α → M) → M
hf : DefinableFun L A f
hg : DefinableFun L A g
⊢ Definable.{u_4, u_5, u_1, u_2} A L (α := α) {v : α → M | f v = g v}
have hF : DefinableMap.{u_1, u_2, 0, u_4, u_5} L (α := α) (β := Fin (Nat.succ 0).succ) A fun (v : α → M) ↦ ![f v, g v]
Tactic: have hF : A.DefinableMap L (fun v => ![f v, g v]) := by
    simp [DefinableMap, *]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
f : (α → M) → M
h : A.TermDefinable L f
⊢ A.Definable L (Function.tupleGraph f)
have obtain : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α),
  Definable.{u, v, w, u₁} A L (α := Option α) (Function.tupleGraph fun (v : α → M) ↦ Term.realize v φ)
Tactic: obtain ⟨φ, rfl⟩ := h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
⊢ Definable.{u, v, w, u₁} A L (α := Option α) (Function.tupleGraph fun (v : α → M) ↦ Term.realize v φ)
have h : Eq (α := Set (Option α → M)) (Function.tupleGraph fun (v : α → M) ↦ Term.realize v φ)
  (setOf ((Term.relabel some φ).equal (var none)).Realize)
Tactic: use (φ.relabel some).equal (Term.var none)
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
⊢ Eq (α := Set (Option α → M)) (Function.tupleGraph fun (v : α → M) ↦ Term.realize v φ)
    (setOf ((Term.relabel some φ).equal (var none)).Realize)
have h : ∀ (x : Option α → M),
  Membership.mem (γ := Set (Option α → M)) (Function.tupleGraph fun (v : α → M) ↦ Term.realize v φ) x ↔
    Membership.mem (γ := Set (Option α → M)) (setOf ((Term.relabel some φ).equal (var none)).Realize) x
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
L' : Language
inst : L.Structure M
inst_1 : L'.Structure M
α : Type u₁
f : (α → M) → M
h : A.TermDefinable L f
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
⊢ A.TermDefinable L' f
have obtain : ∀ (ψ : (withConstants.{u, v, w} L (↑A : Type w)).Term α),
  TermDefinable.{u_2, u_3, w, u₁} A L' (α := α) fun (v : α → M) ↦ Term.realize v ψ
Tactic: obtain ⟨ψ, rfl⟩ := h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
L' : Language
inst : L.Structure M
inst_1 : L'.Structure M
α : Type u₁
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
⊢ TermDefinable.{u_2, u_3, w, u₁} A L' (α := α) fun (v : α → M) ↦ Term.realize v ψ
have h : Eq (α := (α → M) → M) (fun (v : α → M) ↦ Term.realize v ψ) fun (v : α → M) ↦
  Term.realize v (LHom.onTerm (LHom.addConstants (↑A : Type w) φ) ψ)
Tactic: use (φ.addConstants A).onTerm ψ
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
L : Language
inst : L.Structure M
α : Type u₁
f : (α → M) → M
⊢ TermDefinable ∅ L f ↔ ∃ (φ : L.Term α), f = fun (v : α → M) ↦ Term.realize v φ
have rw : (∃ (φ : (withConstants.{u, v, w} L (↑∅ : Type w)).Term α), f = fun (v : α → M) ↦ Term.realize v φ) ↔
  ∃ (b : (withConstants.{u, v, w} L (↑∅ : Type w)).Term α),
    f = fun (v : α → M) ↦
      Term.realize.{u, v, w, u₁} (L := L) v
        ((Equiv.symm (LEquiv.onTerm (LEquiv.addEmptyConstants L (↑∅ : Type w))) :
            (a : L[[(↑∅ : Type w)]].Term α) → L.Term α)
          b)
Tactic: rw [TermDefinable, Equiv.exists_congr_left (LEquiv.addEmptyConstants L (∅ : Set M)).onTerm]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
B : Set M
f : (α → M) → M
h : A.TermDefinable L f
hAB : A ⊆ B
⊢ B.TermDefinable L f
have rw : ∀ (h : TermDefinable ∅ (withConstants.{u, v, w} L (↑A : Type w)) f) (hAB : A ⊆ B),
  TermDefinable ∅ (withConstants.{u, v, w} L (↑B : Type w)) f
Tactic: rw [← termDefinable_empty_withConstants_iff] at h ⊢
Cleared hypotheses: h, hAB
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
L' : Language
inst : L.Structure M
inst_1 : L'.Structure M
β : Type u_1
f : (β → M) → M
h₁ : A.TermDefinable L f
h₂ :
  ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n),
    A.TermDefinable L' (α := Fin n) fun (v : Fin n → M) ↦ Term.realize v g.term
⊢ A.TermDefinable L' f
have obtain : ∀ (x : (withConstants.{u, v, w} L (↑A : Type w)).Term β),
  TermDefinable.{u_2, u_3, w, u_1} A L' (α := β) fun (v : β → M) ↦ Term.realize v x
Tactic: obtain ⟨x, rfl⟩ := h₁
Cleared hypotheses: f, h₁
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
L' : Language
inst : L.Structure M
inst_1 : L'.Structure M
β : Type u_1
h₂ :
  ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n),
    A.TermDefinable L' (α := Fin n) fun (v : Fin n → M) ↦ Term.realize v g.term
x : (withConstants.{u, v, w} L (↑A : Type w)).Term β
⊢ TermDefinable.{u_2, u_3, w, u_1} A L' (α := β) fun (v : β → M) ↦ Term.realize v x
have choose : ∀
  (c :
    {n : ℕ} →
      (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n) →
        (withConstants.{u_2, u_3, w} L' (↑A : Type w)).Term (Fin n))
  (hc :
    ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n),
      Eq.{w + 1} (α := (Fin n → M) → M) (fun (v : Fin n → M) ↦ Term.realize v g.term) fun (v : Fin n → M) ↦
        Term.realize v (c g)),
  TermDefinable.{u_2, u_3, w, u_1} A L' (α := β) fun (v : β → M) ↦ Term.realize v x
Tactic: choose c hc using @h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (hypothesis)
Goal:
M : Type w
A : Set M
L : Language
L' : Language
inst : L.Structure M
inst_1 : L'.Structure M
β : Type u_1
x : (withConstants.{u, v, w} L (↑A : Type w)).Term β
c :
  {n : ℕ} →
    (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n) →
      (withConstants.{u_2, u_3, w} L' (↑A : Type w)).Term (Fin n)
hc :
  ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n),
    Eq.{w + 1} (α := (Fin n → M) → M) (fun (v : Fin n → M) ↦ Term.realize v g.term) fun (v : Fin n → M) ↦
      Term.realize v (c g)
⊢ TermDefinable.{u_2, u_3, w, u_1} A L' (α := β) fun (v : β → M) ↦ Term.realize v x
have hc₁ : ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n) (x : Fin n → M),
  Term.realize x g.term = Term.realize x (c g)
Tactic: simp only [funext_iff] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
L' : Language
inst : L.Structure M
inst_1 : L'.Structure M
β : Type u_1
x : (withConstants.{u, v, w} L (↑A : Type w)).Term β
c :
  {n : ℕ} →
    (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n) →
      (withConstants.{u_2, u_3, w} L' (↑A : Type w)).Term (Fin n)
hc :
  ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n) (x : Fin n → M),
    Term.realize x g.term = Term.realize x (c g)
⊢ TermDefinable.{u_2, u_3, w, u_1} A L' (α := β) fun (v : β → M) ↦ Term.realize v x
have h : Eq (α := (β → M) → M) (fun (v : β → M) ↦ Term.realize v x) fun (v : β → M) ↦
  Term.realize (L := withConstants.{u_2, u_3, w} L' (↑A : Type w)) v (x.substFunc fun {n : ℕ} ↦ c)
Tactic: use x.substFunc c
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
⊢ TermDefinable₁ (A := A) L f ↔
    ∃ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Term Unit),
      f = (fun (v : Unit → M) ↦ Term.realize v φ) ∘ Function.const Unit
have refine : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Term Unit),
  (Eq.{w + 1} (α := (Unit → M) → M) (fun (x : Unit → M) ↦ f (x ())) fun (v : Unit → M) ↦ Term.realize v φ) ↔
    f = (fun (v : Unit → M) ↦ Term.realize v φ) ∘ Function.const Unit
Tactic: refine exists_congr fun φ ↦ ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term Unit
⊢ (Eq.{w + 1} (α := (Unit → M) → M) (fun (x : Unit → M) ↦ f (x ())) fun (v : Unit → M) ↦ Term.realize v φ) ↔
    f = (fun (v : Unit → M) ↦ Term.realize v φ) ∘ Function.const Unit
have rw : ∀ (b : M),
  f (((Equiv.funUnique Unit M).symm : (a : M) → Unit → M) b ()) =
      Term.realize (((Equiv.funUnique Unit M).symm : (a : M) → Unit → M) b) φ ↔
    f b = ((fun (v : Unit → M) ↦ Term.realize v φ) ∘ Function.const Unit) b
Tactic: rw [funext_iff, funext_iff, (Equiv.funUnique Unit M).forall_congr']
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term Unit
⊢ ∀ (b : M),
    f (((Equiv.funUnique Unit M).symm : (a : M) → Unit → M) b ()) =
        Term.realize (((Equiv.funUnique Unit M).symm : (a : M) → Unit → M) b) φ ↔
      f b = ((fun (v : Unit → M) ↦ Term.realize v φ) ∘ Function.const Unit) b
have simp : ∀ (b : M), f b = Term.realize (uniqueElim (α := fun (a : Unit) ↦ M) b) φ ↔ f b = Term.realize (Function.const Unit b) φ
Tactic: simp only [Equiv.funUnique_symm_apply, uniqueElim_const, Function.comp_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
h : TermDefinable₁ (A := A) L f
⊢ A.Definable₂ L (Function.graph f)
have obtain : ∀ (t : (withConstants.{u, v, w} L (↑A : Type w)).Formula (Option Unit))
  (h : Eq.{w + 1} (α := Set (Option Unit → M)) (Function.tupleGraph fun (v : Unit → M) ↦ f (v ())) (setOf t.Realize)),
  A.Definable₂ L (Function.graph f)
Tactic: obtain ⟨t, h⟩ := h.termDefinable.definable_tupleGraph A L
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
h_1 : TermDefinable₁ (A := A) L f
t : (withConstants.{u, v, w} L (↑A : Type w)).Formula (Option Unit)
h : Eq.{w + 1} (α := Set (Option Unit → M)) (Function.tupleGraph fun (v : Unit → M) ↦ f (v ())) (setOf t.Realize)
⊢ A.Definable₂ L (Function.graph f)
have h₁ : Eq.{w + 1} (α := Set (Fin 2 → M)) {x : Fin 2 → M | (x 0, x 1) ∈ Function.graph f}
  (setOf (Formula.Realize (Formula.relabel (fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0) t)))
Tactic: use t.relabel (Option.elim · 1 (fun _ ↦ 0))
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
h_1 : TermDefinable₁ (A := A) L f
t : (withConstants.{u, v, w} L (↑A : Type w)).Formula (Option Unit)
h : Eq.{w + 1} (α := Set (Option Unit → M)) (Function.tupleGraph fun (v : Unit → M) ↦ f (v ())) (setOf t.Realize)
⊢ Eq.{w + 1} (α := Set (Fin 2 → M)) {x : Fin 2 → M | (x 0, x 1) ∈ Function.graph f}
    (setOf (Formula.Realize (Formula.relabel (fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0) t)))
have h₁ : ∀ (v : Fin 2 → M),
  Membership.mem (γ := Set (Fin 2 → M)) {x : Fin 2 → M | (x 0, x 1) ∈ Function.graph f} v ↔
    Membership.mem (γ := Set (Fin 2 → M))
      (setOf (Formula.Realize (Formula.relabel (fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0) t))) v
Tactic: ext v
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
h_1 : TermDefinable₁ (A := A) L f
t : (withConstants.{u, v, w} L (↑A : Type w)).Formula (Option Unit)
h : Eq.{w + 1} (α := Set (Option Unit → M)) (Function.tupleGraph fun (v : Unit → M) ↦ f (v ())) (setOf t.Realize)
v : Fin 2 → M
⊢ Membership.mem (γ := Set (Fin 2 → M)) {x : Fin 2 → M | (x 0, x 1) ∈ Function.graph f} v ↔
    Membership.mem (γ := Set (Fin 2 → M))
      (setOf (Formula.Realize (Formula.relabel (fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0) t))) v
have h₁ : Membership.mem (γ := Set (Fin 2 → M))
    (setOf (Formula.Realize (Formula.relabel (fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0) t))) v ↔
  Membership.mem (γ := Set (Option Unit → M)) (setOf t.Realize)
    (v ∘ fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0)
Tactic: convert! Set.ext_iff.1 h (v ∘ (Option.elim · 1 (fun _ ↦ 0)))
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
C : (withConstants.{u, v, w} L (↑A : Type w)).Constants
⊢ Eq (α := (α → M) → M) (Function.const (α → M) (↑C : M)) fun (v : α → M) ↦ Term.realize v C.term
have simp : Eq (α := (α → M) → M) (Function.const (α → M) (↑C : M)) fun (v : α → M) ↦ (↑C : M)
Tactic: simp only [Term.realize_constants]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
f : (α → M) → M
g : α → (β → M) → M
hf : A.TermDefinable L f
hg : ∀ (i : α), A.TermDefinable L (g i)
⊢ TermDefinable.{u, v, w, u_1} A L (α := β) fun (b : β → M) ↦ f fun (x : α) ↦ g x b
have obtain : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α),
  TermDefinable.{u, v, w, u_1} A L (α := β) fun (b : β → M) ↦ (fun (v : α → M) ↦ Term.realize v φ) fun (x : α) ↦ g x b
Tactic: obtain ⟨φ, rfl⟩ := hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
g : α → (β → M) → M
hg : ∀ (i : α), A.TermDefinable L (g i)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
⊢ TermDefinable.{u, v, w, u_1} A L (α := β) fun (b : β → M) ↦ (fun (v : α → M) ↦ Term.realize v φ) fun (x : α) ↦ g x b
have choose : ∀ (ψ : (i : α) → (withConstants.{u, v, w} L (↑A : Type w)).Term β)
  (hψ : ∀ (i : α), g i = fun (v : β → M) ↦ Term.realize v (ψ i)),
  TermDefinable.{u, v, w, u_1} A L (α := β) fun (b : β → M) ↦ (fun (v : α → M) ↦ Term.realize v φ) fun (x : α) ↦ g x b
Tactic: choose ψ hψ using hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
g : α → (β → M) → M
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
ψ : (i : α) → (withConstants.{u, v, w} L (↑A : Type w)).Term β
hψ : ∀ (i : α), g i = fun (v : β → M) ↦ Term.realize v (ψ i)
⊢ TermDefinable.{u, v, w, u_1} A L (α := β) fun (b : β → M) ↦ (fun (v : α → M) ↦ Term.realize v φ) fun (x : α) ↦ g x b
have h : Eq (α := (β → M) → M) (fun (b : β → M) ↦ (fun (v : α → M) ↦ Term.realize v φ) fun (x : α) ↦ g x b) fun (v : β → M) ↦
  Term.realize v (φ.subst ψ)
Tactic: use φ.subst ψ
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m n : ℕ
h : m ≤ n
⊢ Eq (α := (a : G' m) → G' n) (⇑(natLERec (G' := G') f' m n h) : (a : G' m) → G' n) fun (a : G' m) ↦
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) a
have obtain : ∀ (k : ℕ) (h : m ≤ m + k),
  Eq (α := (a : G' m) → G' (m + k)) (⇑(natLERec (G' := G') f' m (m + k) h) : (a : G' m) → G' (m + k)) fun (a : G' m) ↦
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) a
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m k : ℕ
h : m ≤ m + k
⊢ Eq (α := (a : G' m) → G' (m + k)) (⇑(natLERec (G' := G') f' m (m + k) h) : (a : G' m) → G' (m + k)) fun (a : G' m) ↦
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) a
have h₁ : ∀ (x : G' m),
  (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih :
  ∀ (h : m ≤ m + k),
    (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
      Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
h : m ≤ m + (k + 1)
⊢ (natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
have h₁ : Eq (α := G' (m + (k + 1)))
  ((natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x : G' (m + (k + 1)))
  ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
      (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) sorry (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
    G' (m + k + 1))
Tactic: rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
      Embedding.comp_apply, ih]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih :
  ∀ (h : m ≤ m + k),
    (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
      Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
h : m ≤ m + (k + 1)
h₁ :
  Eq (α := G' (m + (k + 1)))
    ((natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x : G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
⊢ (natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
have h₂ : Eq (α := G' (m + (k + 1)))
  (((Nat.leRecOn (C := fun (x : ℕ) ↦ G' m ↪[L] G' x) h (fun (k : ℕ) (g : G' m ↪[L] G' k) ↦ (f' k).comp g)
            (Embedding.refl L (G' m)) :
          G' m ↪[L] G' (m + (k + 1))) :
        (a : G' m) → G' (m + (k + 1)))
      x :
    G' (m + (k + 1)))
  ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
      (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) sorry (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
    G' (m + k + 1))
Tactic: rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
      Embedding.comp_apply, ih]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih :
  ∀ (h : m ≤ m + k),
    (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
      Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
h : m ≤ m + (k + 1)
h₁ :
  Eq (α := G' (m + (k + 1)))
    ((natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x : G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
h₂ :
  Eq (α := G' (m + (k + 1)))
    (((Nat.leRecOn (C := fun (x : ℕ) ↦ G' m ↪[L] G' x) h (fun (k : ℕ) (g : G' m ↪[L] G' k) ↦ (f' k).comp g)
              (Embedding.refl L (G' m)) :
            G' m ↪[L] G' (m + (k + 1))) :
          (a : G' m) → G' (m + (k + 1)))
        x :
      G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
⊢ (natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
have h₃ : Eq (α := G' (m + (k + 1)))
  ((Embedding.comp (f' (m + k))
          (Nat.leRecOn (C := fun (x : ℕ) ↦ G' m ↪[L] G' x) (n := m) (m := m + k) sorry
            (fun {k : ℕ} (g : G' m ↪[L] G' k) ↦ (f' k).comp g) (Embedding.refl L (G' m))) :
        (a : G' m) → G' (m + (k + 1)))
      x :
    G' (m + (k + 1)))
  ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
      (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) sorry (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
    G' (m + k + 1))
Tactic: rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
      Embedding.comp_apply, ih]