awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (hypothesis)
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx :
  ∀ (i : Fin n),
    Membership.mem (γ := Set M) {x : M | Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)}
      (x i)
⊢ Membership.mem (γ := Set M) {x : M | Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)}
    (funMap fn x)
have h : Eq.{u_1 + 1} (α := Fin n → N) ((⇑f : (a : M) → N) ∘ x) ((⇑g : (a : M) → N) ∘ x)
Tactic: have h : f ∘ x = g ∘ x := by
      ext
      repeat' rw [Function.comp_apply]
      apply hx
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
p : L.Substructure N
f : M ↪[L] N
h : ∀ (c : M), Membership.mem (α := N) p ((f : (a : M) → N) c : N)
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ RelMap.{u, v, u_1} (M := ↥p) r ((⇑(Hom.codRestrict p f.toHom h) : (a : M) → ↥p) ∘ x) ↔ RelMap r x
have rw : RelMap (M := N) r
    (Function.comp (β := ↥p) (⇑p.subtype : (a : ↥p) → N) ((⇑(Hom.codRestrict p f.toHom h) : (a : M) → ↥p) ∘ x)) ↔
  RelMap r x
Tactic: rw [← p.subtype.map_rel]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
p : L.Substructure N
f : M ↪[L] N
h : ∀ (c : M), Membership.mem (α := N) p ((f : (a : M) → N) c : N)
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ RelMap (M := N) r
      (Function.comp (β := ↥p) (⇑p.subtype : (a : ↥p) → N) ((⇑(Hom.codRestrict p f.toHom h) : (a : M) → ↥p) ∘ x)) ↔
    RelMap r x
have change : RelMap.{u, v, u_1} (M := N) r ((⇑(p.subtype.toHom.comp (Hom.codRestrict p f.toHom h)) : (a : M) → N) ∘ x) ↔ RelMap r x
Tactic: change RelMap r (Hom.comp p.subtype.toHom (f.toHom.codRestrict p h) ∘ x) ↔ _
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
p : L.Substructure N
f : M ↪[L] N
h : ∀ (c : M), Membership.mem (α := N) p ((f : (a : M) → N) c : N)
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ RelMap.{u, v, u_1} (M := N) r ((⇑(p.subtype.toHom.comp (Hom.codRestrict p f.toHom h)) : (a : M) → N) ∘ x) ↔ RelMap r x
have rw : RelMap.{u, v, u_1} (M := N) r ((⇑f.toHom : (a : M) → N) ∘ x) ↔ RelMap.{u, v, u_1} (M := N) r ((⇑f : (a : M) → N) ∘ x)
Tactic: rw [Hom.subtype_comp_codRestrict, ← f.map_rel]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
⊢ (Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding = f.comp s.subtype
have h : ∀ (x : ↥s),
  Eq.{u_1 + 1} (α := N)
    (((Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding : (a : ↥s) → N) x : N)
    ((f.comp s.subtype : (a : ↥s) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
⊢ f.toHom.range.subtype.comp f.equivRange.toEmbedding = f
have h : ∀ (x : M),
  Eq.{u_1 + 1} (α := N) ((f.toHom.range.subtype.comp f.equivRange.toEmbedding : (a : M) → N) x : N)
    ((f : (a : M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ f.toHom.range = ⊤
have h : ∀ (n : N), n ∈ f.toHom.range ↔ Membership.mem (γ := L.Substructure N) ⊤ n
Tactic: ext n
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
n : N
⊢ n ∈ f.toHom.range ↔ Membership.mem (γ := L.Substructure N) ⊤ n
have h : ∃ (y : M), (f : (a : M) → N) y = n
Tactic: simp only [Hom.mem_range, coe_toHom, Substructure.mem_top, iff_true]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
⊢ S.subtype.toHom.range = S
have h : ∀ (x : M), x ∈ S.subtype.toHom.range ↔ x ∈ S
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
x : M
⊢ x ∈ S.subtype.toHom.range ↔ x ∈ S
have h : (∃ (y : ↥S), (↑y : M) = x) ↔ x ∈ S
Tactic: simp only [Hom.mem_range, Embedding.coe_toHom, coe_subtype]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
x : M
⊢ (∃ (y : ↥S), (↑y : M) = x) ↔ x ∈ S
have h : (∃ (y : ↥S), (↑y : M) = x) → x ∈ S
Tactic: refine ⟨?_, fun h => ⟨⟨x, h⟩, rfl⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst : DecidableEq α
inst_1 : (n : ℕ) → DecidableEq (L.Functions n)
m : ℕ
f : L.Functions m
xs : Fin m → L.Term α
n : ℕ
g : L.Functions n
ys : Fin n → L.Term α
h : m = n
this : DecidableEq (L.Term α) := instDecidableEq
⊢ (f = Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ L.Functions x) g ⋯ ∧ ∀ (i : Fin m), xs i = ys (Fin.cast h i)) ↔
    func f xs = func g ys
have subst : ∀ (g : L.Functions m) (ys : Fin m → L.Term α),
  (f = Eq.rec (motive := fun (x : ℕ) (h : m = x) ↦ L.Functions x) g sorry ∧ ∀ (i : Fin m), xs i = ys (Fin.cast sorry i)) ↔
    func f xs = func g ys
Tactic: subst h
Cleared hypotheses: n, g, ys, h
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
t : L.Term α
⊢ relabel id t = t
have var : ∀ (a : α), Eq (α := L.Term α) (relabel id (var a)) (var a)
Tactic: induction t with
  | var => rfl
  | func _ _ ih => simp [ih]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
t : L.Term α
var : ∀ (a : α), Eq (α := L.Term α) (relabel id (Language.var a)) (Language.var a)
⊢ relabel id t = t
have func : ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α) (ih : ∀ (a : Fin l), relabel id (_ts a) = _ts a),
  relabel id (func _f _ts) = func _f _ts
Tactic: induction t with
  | var => rfl
  | func _ _ ih => simp [ih]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
t : L.Term α
⊢ relabel g (relabel f t) = relabel (g ∘ f) t
have var : ∀ (a : α), Eq (α := L.Term γ) (relabel g (relabel f (var a))) (relabel (g ∘ f) (var a))
Tactic: induction t with
  | var => rfl
  | func _ _ ih => simp [ih]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
t : L.Term α
var : ∀ (a : α), Eq (α := L.Term γ) (relabel g (relabel f (Language.var a))) (relabel (g ∘ f) (Language.var a))
⊢ relabel g (relabel f t) = relabel (g ∘ f) t
have func : ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α)
  (ih : ∀ (a : Fin l), relabel g (relabel f (_ts a)) = relabel (g ∘ f) (_ts a)),
  relabel g (relabel f (func _f _ts)) = relabel (g ∘ f) (func _f _ts)
Tactic: induction t with
  | var => rfl
  | func _ _ ih => simp [ih]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L[[γ]].Functions n
_ts : Fin n → L[[γ]].Term α
ih : ∀ (a : Fin n), (_ts a).constantsToVars.varsToConstants = _ts a
⊢ (func f _ts).constantsToVars.varsToConstants = func f _ts
have func : ∀ (f : L[[γ]].Functions 0) (_ts : Fin 0 → L[[γ]].Term α)
  (ih : ∀ (a : Fin 0), (_ts a).constantsToVars.varsToConstants = _ts a),
  (func f _ts).constantsToVars.varsToConstants = func f _ts
Tactic: cases n
Cleared hypotheses: n, f, _ts, ih
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L[[γ]].Functions n
_ts : Fin n → L[[γ]].Term α
ih : ∀ (a : Fin n), (_ts a).constantsToVars.varsToConstants = _ts a
func :
  ∀ (f : L[[γ]].Functions 0) (_ts : Fin 0 → L[[γ]].Term α)
    (ih : ∀ (a : Fin 0), (_ts a).constantsToVars.varsToConstants = _ts a),
    (Language.func f _ts).constantsToVars.varsToConstants = Language.func f _ts
⊢ (Language.func f _ts).constantsToVars.varsToConstants = Language.func f _ts
have func₁ : ∀ (n : ℕ) (f : L[[γ]].Functions (n + 1)) (_ts : Fin (n + 1) → L[[γ]].Term α)
  (ih : ∀ (a : Fin (n + 1)), (_ts a).constantsToVars.varsToConstants = _ts a),
  (Language.func f _ts).constantsToVars.varsToConstants = Language.func f _ts
Tactic: cases n
Cleared hypotheses: n, f, _ts, ih
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L[[γ]].Functions 0
_ts : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts a).constantsToVars.varsToConstants = _ts a
⊢ (func f _ts).constantsToVars.varsToConstants = func f _ts
have func : ∀ (val : L.Functions 0), (func (Sum.inl val) _ts).constantsToVars.varsToConstants = func (Sum.inl val) _ts
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L[[γ]].Functions 0
_ts : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts a).constantsToVars.varsToConstants = _ts a
func :
  ∀ (val : L.Functions 0),
    (Language.func (Sum.inl val) _ts).constantsToVars.varsToConstants = Language.func (Sum.inl val) _ts
⊢ (Language.func f _ts).constantsToVars.varsToConstants = Language.func f _ts
have func₁ : ∀ (val : (constantsOn γ).Functions 0),
  (Language.func (Sum.inr val) _ts).constantsToVars.varsToConstants = Language.func (Sum.inr val) _ts
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L[[γ]].Functions (n + 1)
_ts : Fin (n + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n + 1)), (_ts a).constantsToVars.varsToConstants = _ts a
⊢ (func f _ts).constantsToVars.varsToConstants = func f _ts
have func : ∀ (val : L.Functions (n + 1)), (func (Sum.inl val) _ts).constantsToVars.varsToConstants = func (Sum.inl val) _ts
Tactic: obtain - | f := f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L[[γ]].Functions (n + 1)
_ts : Fin (n + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n + 1)), (_ts a).constantsToVars.varsToConstants = _ts a
func :
  ∀ (val : L.Functions (n + 1)),
    (Language.func (Sum.inl val) _ts).constantsToVars.varsToConstants = Language.func (Sum.inl val) _ts
⊢ (Language.func f _ts).constantsToVars.varsToConstants = Language.func f _ts
have func₁ : ∀ (f : (constantsOn γ).Functions (n + 1)),
  (Language.func (Sum.inr f) _ts).constantsToVars.varsToConstants = Language.func (Sum.inr f) _ts
Tactic: obtain - | f := f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
t : L[[γ]].Term α
⊢ t.constantsToVars.varsToConstants = t
have var : ∀ (a : α), Eq (α := L[[γ]].Term α) (varsToConstants (constantsToVars (var a))) (var a)
Tactic: induction t with
    | var => rfl
    | @func n f _ ih =>
      cases n
      · cases f
        · simp [constantsToVars, varsToConstants, ih]
        · simp [constantsToVars, varsToConstants, Constants.term, eq_iff_true_of_subsingleton]
      · obtain - | f := f
        · simp [constantsToVars, varsToConstants, ih]
        · exact isEmptyElim f
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
t : L[[γ]].Term α
var : ∀ (a : α), Eq (α := L[[γ]].Term α) (varsToConstants (constantsToVars (Language.var a))) (Language.var a)
⊢ t.constantsToVars.varsToConstants = t
have func : ∀ {n : ℕ} (f : L[[γ]].Functions n) (_ts : Fin n → L[[γ]].Term α)
  (ih : ∀ (a : Fin n), (_ts a).constantsToVars.varsToConstants = _ts a),
  (func f _ts).constantsToVars.varsToConstants = func f _ts
Tactic: induction t with
    | var => rfl
    | @func n f _ ih =>
      cases n
      · cases f
        · simp [constantsToVars, varsToConstants, ih]
        · simp [constantsToVars, varsToConstants, Constants.term, eq_iff_true_of_subsingleton]
      · obtain - | f := f
        · simp [constantsToVars, varsToConstants, ih]
        · exact isEmptyElim f
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
x : γ ⊕ α
⊢ Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (var x))) (var x)
have var : ∀ (val : γ), Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (var (Sum.inl val)))) (var (Sum.inl val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
x : γ ⊕ α
var :
  ∀ (val : γ),
    Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (Language.var (Sum.inl val))))
      (Language.var (Sum.inl val))
⊢ Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (Language.var x))) (Language.var x)
have var₁ : ∀ (val : α),
  Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (Language.var (Sum.inr val)))) (Language.var (Sum.inr val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L.Functions n
_ts : Fin n → L.Term (γ ⊕ α)
ih : ∀ (a : Fin n), (_ts a).varsToConstants.constantsToVars = _ts a
⊢ (func f _ts).varsToConstants.constantsToVars = func f _ts
have func : ∀ (f : L.Functions 0) (_ts : Fin 0 → L.Term (γ ⊕ α))
  (ih : ∀ (a : Fin 0), (_ts a).varsToConstants.constantsToVars = _ts a),
  (func f _ts).varsToConstants.constantsToVars = func f _ts
Tactic: cases n
Cleared hypotheses: n, f, _ts, ih
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L.Functions n
_ts : Fin n → L.Term (γ ⊕ α)
ih : ∀ (a : Fin n), (_ts a).varsToConstants.constantsToVars = _ts a
func :
  ∀ (f : L.Functions 0) (_ts : Fin 0 → L.Term (γ ⊕ α))
    (ih : ∀ (a : Fin 0), (_ts a).varsToConstants.constantsToVars = _ts a),
    (Language.func f _ts).varsToConstants.constantsToVars = Language.func f _ts
⊢ (Language.func f _ts).varsToConstants.constantsToVars = Language.func f _ts
have func₁ : ∀ (n : ℕ) (f : L.Functions (n + 1)) (_ts : Fin (n + 1) → L.Term (γ ⊕ α))
  (ih : ∀ (a : Fin (n + 1)), (_ts a).varsToConstants.constantsToVars = _ts a),
  (Language.func f _ts).varsToConstants.constantsToVars = Language.func f _ts
Tactic: cases n
Cleared hypotheses: n, f, _ts, ih
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
t : L.Term (γ ⊕ α)
⊢ t.varsToConstants.constantsToVars = t
have var : ∀ (x : γ ⊕ α), Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (var x))) (var x)
Tactic: induction t with
    | var x => cases x <;> rfl
    | @func n f _ ih => cases n <;> · simp [varsToConstants, constantsToVars, ih]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
t : L.Term (γ ⊕ α)
var : ∀ (x : γ ⊕ α), Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (Language.var x))) (Language.var x)
⊢ t.varsToConstants.constantsToVars = t
have func : ∀ {n : ℕ} (f : L.Functions n) (_ts : Fin n → L.Term (γ ⊕ α))
  (ih : ∀ (a : Fin n), (_ts a).varsToConstants.constantsToVars = _ts a),
  (func f _ts).varsToConstants.constantsToVars = func f _ts
Tactic: induction t with
    | var x => cases x <;> rfl
    | @func n f _ ih => cases n <;> · simp [varsToConstants, constantsToVars, ih]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
t : L.Term α
⊢ (t.substFunc fun {n : ℕ} ↦ Functions.term) = t
have var : ∀ (a : α), Eq (α := L.Term α) (substFunc (L := L) (var a) fun {n : ℕ} ↦ Functions.term) (var a)
Tactic: induction t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
t : L.Term α
var : ∀ (a : α), Eq (α := L.Term α) (substFunc (L := L) (Language.var a) fun {n : ℕ} ↦ Functions.term) (Language.var a)
⊢ (t.substFunc fun {n : ℕ} ↦ Functions.term) = t
have func : ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α),
  (∀ (a : Fin l), ((_ts a).substFunc fun {n : ℕ} ↦ Functions.term) = _ts a) →
    ((func _f _ts).substFunc fun {n : ℕ} ↦ Functions.term) = func _f _ts
Tactic: induction t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
⊢ Eq (α := L.Term α → L.Term α) (LHom.id L).onTerm id
have h : ∀ (t : L.Term α), (LHom.id L).onTerm t = id t
Tactic: ext t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
ih : ∀ (a : Fin l), (LHom.id L).onTerm (_ts a) = id (_ts a)
⊢ (LHom.id L).onTerm (func _f _ts) = id (func _f _ts)
have h : (func ((LHom.id L).onFunction _f) fun (i : Fin l) ↦ id (_ts i)) = id (func _f _ts)
Tactic: simp_rw [onTerm, ih]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
t : L.Term α
⊢ (LHom.id L).onTerm t = id t
have h : ∀ (a : α), (LHom.id L).onTerm (var a) = id (var a)
Tactic: induction t with
  | var => rfl
  | func _ _ ih => simp_rw [onTerm, ih]; rfl
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
t : L.Term α
h : ∀ (a : α), (LHom.id L).onTerm (var a) = id (var a)
⊢ (LHom.id L).onTerm t = id t
have h₁ : ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α) (ih : ∀ (a : Fin l), (LHom.id L).onTerm (_ts a) = id (_ts a)),
  (LHom.id L).onTerm (func _f _ts) = id (func _f _ts)
Tactic: induction t with
  | var => rfl
  | func _ _ ih => simp_rw [onTerm, ih]; rfl
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
⊢ Eq (α := L.Term α → L''.Term α) (φ.comp ψ).onTerm (φ.onTerm ∘ ψ.onTerm)
have h : ∀ (t : L.Term α), (φ.comp ψ).onTerm t = (φ.onTerm ∘ ψ.onTerm) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
ih : ∀ (a : Fin l), (φ.comp ψ).onTerm (_ts a) = (φ.onTerm ∘ ψ.onTerm) (_ts a)
⊢ (φ.comp ψ).onTerm (func _f _ts) = (φ.onTerm ∘ ψ.onTerm) (func _f _ts)
have h : (func ((φ.comp ψ).onFunction _f) fun (i : Fin l) ↦ (φ.onTerm ∘ ψ.onTerm) (_ts i)) = (φ.onTerm ∘ ψ.onTerm) (func _f _ts)
Tactic: simp_rw [onTerm, ih]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
t : L.Term α
⊢ (φ.comp ψ).onTerm t = (φ.onTerm ∘ ψ.onTerm) t
have h : ∀ (a : α), (φ.comp ψ).onTerm (var a) = (φ.onTerm ∘ ψ.onTerm) (var a)
Tactic: induction t with
  | var => rfl
  | func _ _ ih => simp_rw [onTerm, ih]; rfl
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
t : L.Term α
h : ∀ (a : α), (φ.comp ψ).onTerm (var a) = (φ.onTerm ∘ ψ.onTerm) (var a)
⊢ (φ.comp ψ).onTerm t = (φ.onTerm ∘ ψ.onTerm) t
have h₁ : ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α)
  (ih : ∀ (a : Fin l), (φ.comp ψ).onTerm (_ts a) = (φ.onTerm ∘ ψ.onTerm) (_ts a)),
  (φ.comp ψ).onTerm (func _f _ts) = (φ.onTerm ∘ ψ.onTerm) (func _f _ts)
Tactic: induction t with
  | var => rfl
  | func _ _ ih => simp_rw [onTerm, ih]; rfl
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
⊢ Function.LeftInverse (α := L.Term α) φ.invLHom.onTerm φ.toLHom.onTerm
have rw : Eq (α := L.Term α → L.Term α) (φ.invLHom.onTerm ∘ φ.toLHom.onTerm) id
Tactic: rw [Function.leftInverse_iff_comp, ← LHom.comp_onTerm, φ.left_inv, LHom.id_onTerm]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
rw : Eq (α := L.Term α → L.Term α) (φ.invLHom.onTerm ∘ φ.toLHom.onTerm) id
⊢ Function.LeftInverse (α := L.Term α) φ.invLHom.onTerm φ.toLHom.onTerm
have rw₁ : Eq (α := L.Term α → L.Term α) (φ.invLHom.comp φ.toLHom).onTerm id
Tactic: rw [Function.leftInverse_iff_comp, ← LHom.comp_onTerm, φ.left_inv, LHom.id_onTerm]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
rw : Eq (α := L.Term α → L.Term α) (φ.invLHom.onTerm ∘ φ.toLHom.onTerm) id
rw₁ : Eq (α := L.Term α → L.Term α) (φ.invLHom.comp φ.toLHom).onTerm id
⊢ Function.LeftInverse (α := L.Term α) φ.invLHom.onTerm φ.toLHom.onTerm
have rw₂ : Eq (α := L.Term α → L.Term α) (LHom.id L).onTerm id
Tactic: rw [Function.leftInverse_iff_comp, ← LHom.comp_onTerm, φ.left_inv, LHom.id_onTerm]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
rw : Eq (α := L.Term α → L.Term α) (φ.invLHom.onTerm ∘ φ.toLHom.onTerm) id
rw₁ : Eq (α := L.Term α → L.Term α) (φ.invLHom.comp φ.toLHom).onTerm id
rw₂ : Eq (α := L.Term α → L.Term α) (LHom.id L).onTerm id
⊢ Function.LeftInverse (α := L.Term α) φ.invLHom.onTerm φ.toLHom.onTerm
have rw₃ : Eq (α := L.Term α → L.Term α) id id
Tactic: rw [Function.leftInverse_iff_comp, ← LHom.comp_onTerm, φ.left_inv, LHom.id_onTerm]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
⊢ Function.RightInverse (α := L.Term α) φ.invLHom.onTerm φ.toLHom.onTerm
have rw : Eq (α := L'.Term α → L'.Term α) (φ.toLHom.onTerm ∘ φ.invLHom.onTerm) id
Tactic: rw [Function.rightInverse_iff_comp, ← LHom.comp_onTerm, φ.right_inv, LHom.id_onTerm]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
rw : Eq (α := L'.Term α → L'.Term α) (φ.toLHom.onTerm ∘ φ.invLHom.onTerm) id
⊢ Function.RightInverse (α := L.Term α) φ.invLHom.onTerm φ.toLHom.onTerm
have rw₁ : Eq (α := L'.Term α → L'.Term α) (φ.toLHom.comp φ.invLHom).onTerm id
Tactic: rw [Function.rightInverse_iff_comp, ← LHom.comp_onTerm, φ.right_inv, LHom.id_onTerm]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
rw : Eq (α := L'.Term α → L'.Term α) (φ.toLHom.onTerm ∘ φ.invLHom.onTerm) id
rw₁ : Eq (α := L'.Term α → L'.Term α) (φ.toLHom.comp φ.invLHom).onTerm id
⊢ Function.RightInverse (α := L.Term α) φ.invLHom.onTerm φ.toLHom.onTerm
have rw₂ : Eq (α := L'.Term α → L'.Term α) (LHom.id L').onTerm id
Tactic: rw [Function.rightInverse_iff_comp, ← LHom.comp_onTerm, φ.right_inv, LHom.id_onTerm]