-- Module: Mathlib.ModelTheory.DirectLimit
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))
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) ⋯
              (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) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
h₄ :
  Eq (α := G' (m + (k + 1)))
    ((Embedding.comp (f' (m + k)) (natLERec (G' := G') f' m (m + k) ⋯) : (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)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        ((natLERec (G' := G') f' m (m + k) ⋯ : (a : G' m) → G' (m + k)) x : G' (m + k)) :
      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₆ h₇ :
  Eq (α := G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := G') ⋯ (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (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

Tactic:
rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
      Embedding.comp_apply, ih]

Premises used: Nat.leRecOn_succ, FirstOrder.Language.DirectedSystem.natLERec, FirstOrder.Language.Embedding.comp_apply, le_self_add