awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
toEquiv : M ≃ N
map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv.toFun (funMap f x) = funMap f (toEquiv.toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv.toFun ∘ x) ↔ RelMap r x
toEquiv_1 : M ≃ N
map_fun'_1 :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv_1.toFun (funMap f x) = funMap f (toEquiv_1.toFun ∘ x)
map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv_1.toFun ∘ x) ↔ RelMap r x
h₁ :
  { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.toFun =
    { toEquiv := toEquiv_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 : M ≃[L] N }.toFun
h₂ :
  { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.invFun =
    { toEquiv := toEquiv_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 : M ≃[L] N }.invFun
⊢ { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N } =
    { toEquiv := toEquiv_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 }
have mk : toEquiv = toEquiv_1
Tactic: simp only [mk.injEq]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
toEquiv : M ≃ N
map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv.toFun (funMap f x) = funMap f (toEquiv.toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv.toFun ∘ x) ↔ RelMap r x
toEquiv_1 : M ≃ N
map_fun'_1 :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv_1.toFun (funMap f x) = funMap f (toEquiv_1.toFun ∘ x)
map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv_1.toFun ∘ x) ↔ RelMap r x
h₁ :
  { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.toFun =
    { toEquiv := toEquiv_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 : M ≃[L] N }.toFun
h₂ :
  { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.invFun =
    { toEquiv := toEquiv_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 : M ≃[L] N }.invFun
⊢ toEquiv = toEquiv_1
have mk : ∀ (x : M), Eq.{w' + 1} (α := N) ((toEquiv : (a : M) → N) x : N) ((toEquiv_1 : (a : M) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
⊢ f.symm.toFun (funMap f' x) = funMap f' (f.symm.toFun ∘ x)
have simp : Eq.{w + 1} (α := M) ((f.symm : (a : N) → M) (funMap f' x) : M) (funMap f' ((⇑f.symm : (a : N) → M) ∘ x) : M)
Tactic: simp only [Equiv.toFun_as_coe]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
⊢ Eq.{w + 1} (α := M) ((f.symm : (a : N) → M) (funMap f' x) : M) (funMap f' ((⇑f.symm : (a : N) → M) ∘ x) : M)
have rw : funMap f' x = (f.toEquiv : (a : M) → N) (funMap f' ((⇑f.symm : (a : N) → M) ∘ x))
Tactic: rw [Equiv.symm_apply_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
⊢ funMap f' x = (f.toEquiv : (a : M) → N) (funMap f' ((⇑f.symm : (a : N) → M) ∘ x))
have refine : funMap f' x = funMap f' (f.toFun ∘ (⇑f.symm : (a : N) → M) ∘ x)
Tactic: refine Eq.trans ?_ (f.map_fun' f' (f.toEquiv.symm ∘ x)).symm
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
⊢ funMap f' x = funMap f' (f.toFun ∘ (⇑f.symm : (a : N) → M) ∘ x)
have rw : funMap f' x = funMap f' ((f.toFun ∘ (⇑f.symm : (a : N) → M)) ∘ x)
Tactic: rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
rw : funMap f' x = funMap f' ((f.toFun ∘ (⇑f.symm : (a : N) → M)) ∘ x)
⊢ funMap f' x = funMap f' (f.toFun ∘ (⇑f.symm : (a : N) → M) ∘ x)
have rw₁ : funMap f' x =
  funMap f' (Function.comp.{w' + 1, w + 1, w' + 1} (β := M) (⇑f.toEquiv : (a : M) → N) (⇑f.symm : (a : N) → M) ∘ x)
Tactic: rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
rw : funMap f' x = funMap f' ((f.toFun ∘ (⇑f.symm : (a : N) → M)) ∘ x)
rw₁ :
  funMap f' x =
    funMap f' (Function.comp.{w' + 1, w + 1, w' + 1} (β := M) (⇑f.toEquiv : (a : M) → N) (⇑f.symm : (a : N) → M) ∘ x)
⊢ funMap f' x = funMap f' (f.toFun ∘ (⇑f.symm : (a : N) → M) ∘ x)
have rw₂ : funMap f' x = funMap f' (id ∘ x)
Tactic: rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
rw : funMap f' x = funMap f' ((f.toFun ∘ (⇑f.symm : (a : N) → M)) ∘ x)
rw₁ :
  funMap f' x =
    funMap f' (Function.comp.{w' + 1, w + 1, w' + 1} (β := M) (⇑f.toEquiv : (a : M) → N) (⇑f.symm : (a : N) → M) ∘ x)
rw₂ : funMap f' x = funMap f' (id ∘ x)
⊢ funMap f' x = funMap f' (f.toFun ∘ (⇑f.symm : (a : N) → M) ∘ x)
have rw₃ : funMap f' x = funMap f' x
Tactic: rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → N
⊢ RelMap r (f.symm.toFun ∘ x) ↔ RelMap r x
have simp : RelMap.{u, v, w} (M := M) r ((⇑f.symm : (a : N) → M) ∘ x) ↔ RelMap r x
Tactic: simp only [Equiv.toFun_as_coe]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → N
⊢ RelMap.{u, v, w} (M := M) r ((⇑f.symm : (a : N) → M) ∘ x) ↔ RelMap r x
have refine : RelMap r (f.toFun ∘ (⇑f.symm : (a : N) → M) ∘ x) ↔ RelMap r x
Tactic: refine (f.map_rel' r (f.toEquiv.symm ∘ x)).symm.trans ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → N
⊢ RelMap r (f.toFun ∘ (⇑f.symm : (a : N) → M) ∘ x) ↔ RelMap r x
have rw : RelMap r ((f.toFun ∘ (⇑f.symm : (a : N) → M)) ∘ x) ↔ RelMap r x
Tactic: rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → N
rw : RelMap r ((f.toFun ∘ (⇑f.symm : (a : N) → M)) ∘ x) ↔ RelMap r x
⊢ RelMap r (f.toFun ∘ (⇑f.symm : (a : N) → M) ∘ x) ↔ RelMap r x
have rw₁ : RelMap (M := N) r
    (Function.comp.{w' + 1, w + 1, w' + 1} (β := M) (⇑f.toEquiv : (a : M) → N) (⇑f.symm : (a : N) → M) ∘ x) ↔
  RelMap r x
Tactic: rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → N
rw : RelMap r ((f.toFun ∘ (⇑f.symm : (a : N) → M)) ∘ x) ↔ RelMap r x
rw₁ :
  RelMap (M := N) r
      (Function.comp.{w' + 1, w + 1, w' + 1} (β := M) (⇑f.toEquiv : (a : M) → N) (⇑f.symm : (a : N) → M) ∘ x) ↔
    RelMap r x
⊢ RelMap r (f.toFun ∘ (⇑f.symm : (a : N) → M) ∘ x) ↔ RelMap r x
have rw₂ : RelMap r (id ∘ x) ↔ RelMap r x
Tactic: rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → N
rw : RelMap r ((f.toFun ∘ (⇑f.symm : (a : N) → M)) ∘ x) ↔ RelMap r x
rw₁ :
  RelMap (M := N) r
      (Function.comp.{w' + 1, w + 1, w' + 1} (β := M) (⇑f.toEquiv : (a : M) → N) (⇑f.symm : (a : N) → M) ∘ x) ↔
    RelMap r x
rw₂ : RelMap r (id ∘ x) ↔ RelMap r x
⊢ RelMap r (f.toFun ∘ (⇑f.symm : (a : N) → M) ∘ x) ↔ RelMap r x
have rw₃ : RelMap r x ↔ RelMap r x
Tactic: rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
a₁ a₂ : M ≃[L] N
h : a₁.toEmbedding = a₂.toEmbedding
⊢ a₁ = a₂
have a : Eq (α := (a : M) → N) ((fun (f : M ≃[L] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) a₁)
  ((fun (f : M ≃[L] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) a₂)
Tactic: apply DFunLike.coe_injective
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
x : M
⊢ (refl L M : (a : M) → M) x = x
have simp : ({ toEquiv := _root_.Equiv.refl M, map_fun' := sorry, map_rel' := sorry } : (a : M) → M) x = x
Tactic: simp [refl]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Eq.{u_1 + 1} (α := P)
    (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) (funMap f x))
    (funMap f (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x))
have simp : Eq.{u_1 + 1} (α := P)
  (funMap f (Function.comp.{1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) ((⇑hmn : (a : M) → N) ∘ x)))
  (funMap f (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x))
Tactic: simp only [Function.comp_apply, map_fun]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ RelMap.{u, v, u_1} (M := P) r
      (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x) ↔
    RelMap r x
have rw : RelMap.{u, v, u_1} (M := P) r
    (Function.comp.{1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) ((⇑hmn : (a : M) → N) ∘ x)) ↔
  RelMap r x
Tactic: rw [Function.comp_assoc, map_rel, map_rel]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → M
rw :
  RelMap.{u, v, u_1} (M := P) r
      (Function.comp.{1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) ((⇑hmn : (a : M) → N) ∘ x)) ↔
    RelMap r x
⊢ RelMap.{u, v, u_1} (M := P) r
      (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x) ↔
    RelMap r x
have rw₁ : RelMap.{u, v, w'} (M := N) r ((⇑hmn : (a : M) → N) ∘ x) ↔ RelMap r x
Tactic: rw [Function.comp_assoc, map_rel, map_rel]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → M
rw :
  RelMap.{u, v, u_1} (M := P) r
      (Function.comp.{1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) ((⇑hmn : (a : M) → N) ∘ x)) ↔
    RelMap r x
rw₁ : RelMap.{u, v, w'} (M := N) r ((⇑hmn : (a : M) → N) ∘ x) ↔ RelMap r x
⊢ RelMap.{u, v, u_1} (M := P) r
      (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x) ↔
    RelMap r x
have rw₂ : RelMap r x ↔ RelMap r x
Tactic: rw [Function.comp_assoc, map_rel, map_rel]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : N ≃[L] P
f g : M ≃[L] N
hfg : h.comp f = h.comp g
⊢ f = g
have h₁ : ∀ (x : M), Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ f.comp f.symm = refl L N
have h : ∀ (x : N), Eq (α := N) ((f.comp f.symm : (a : N) → N) x : N) ((refl L N : (a : N) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
x : N
⊢ Eq (α := N) ((f.comp f.symm : (a : N) → N) x : N) ((refl L N : (a : N) → N) x : N)
have h : Eq.{w' + 1} (α := N) ((f : (a : M) → N) ((f.symm : (a : N) → M) x : M) : N) ((refl L N : (a : N) → N) x : N)
Tactic: rw [comp_apply, apply_symm_apply, refl_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
x : N
h : Eq.{w' + 1} (α := N) ((f : (a : M) → N) ((f.symm : (a : N) → M) x : M) : N) ((refl L N : (a : N) → N) x : N)
⊢ Eq (α := N) ((f.comp f.symm : (a : N) → N) x : N) ((refl L N : (a : N) → N) x : N)
have h₁ : x = (refl L N : (a : N) → N) x
Tactic: rw [comp_apply, apply_symm_apply, refl_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
x : N
h : Eq.{w' + 1} (α := N) ((f : (a : M) → N) ((f.symm : (a : N) → M) x : M) : N) ((refl L N : (a : N) → N) x : N)
h₁ : x = (refl L N : (a : N) → N) x
⊢ Eq (α := N) ((f.comp f.symm : (a : N) → N) x : N) ((refl L N : (a : N) → N) x : N)
have h₂ : x = x
Tactic: rw [comp_apply, apply_symm_apply, refl_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ f.symm.comp f = refl L M
have h : ∀ (x : M), Eq (α := M) ((f.symm.comp f : (a : M) → M) x : M) ((refl L M : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
x : M
⊢ Eq (α := M) ((f.symm.comp f : (a : M) → M) x : M) ((refl L M : (a : M) → M) x : M)
have h : Eq.{w + 1} (α := M) ((f.symm : (a : N) → M) ((f : (a : M) → N) x : N) : M) ((refl L M : (a : M) → M) x : M)
Tactic: rw [comp_apply, symm_apply_apply, refl_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
x : M
h : Eq.{w + 1} (α := M) ((f.symm : (a : N) → M) ((f : (a : M) → N) x : N) : M) ((refl L M : (a : M) → M) x : M)
⊢ Eq (α := M) ((f.symm.comp f : (a : M) → M) x : M) ((refl L M : (a : M) → M) x : M)
have h₁ : x = (refl L M : (a : M) → M) x
Tactic: rw [comp_apply, symm_apply_apply, refl_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
x : M
h : Eq.{w + 1} (α := M) ((f.symm : (a : N) → M) ((f : (a : M) → N) x : N) : M) ((refl L M : (a : M) → M) x : M)
h₁ : x = (refl L M : (a : M) → M) x
⊢ Eq (α := M) ((f.symm.comp f : (a : M) → M) x : M) ((refl L M : (a : M) → M) x : M)
have h₂ : x = x
Tactic: rw [comp_apply, symm_apply_apply, refl_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ f.symm.toEmbedding.comp f.toEmbedding = Embedding.refl L M
have rw : (f.symm.comp f).toEmbedding = Embedding.refl L M
Tactic: rw [← comp_toEmbedding, symm_comp_self, refl_toEmbedding]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
rw : (f.symm.comp f).toEmbedding = Embedding.refl L M
⊢ f.symm.toEmbedding.comp f.toEmbedding = Embedding.refl L M
have rw₁ : Eq (α := M ↪[L] M) (toEmbedding (refl L M)) (Embedding.refl L M)
Tactic: rw [← comp_toEmbedding, symm_comp_self, refl_toEmbedding]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
rw : (f.symm.comp f).toEmbedding = Embedding.refl L M
rw₁ : Eq (α := M ↪[L] M) (toEmbedding (refl L M)) (Embedding.refl L M)
⊢ f.symm.toEmbedding.comp f.toEmbedding = Embedding.refl L M
have rw₂ : Eq (α := M ↪[L] M) (Embedding.refl L M) (Embedding.refl L M)
Tactic: rw [← comp_toEmbedding, symm_comp_self, refl_toEmbedding]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ f.toEmbedding.comp f.symm.toEmbedding = Embedding.refl L N
have rw : (f.comp f.symm).toEmbedding = Embedding.refl L N
Tactic: rw [← comp_toEmbedding, self_comp_symm, refl_toEmbedding]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
rw : (f.comp f.symm).toEmbedding = Embedding.refl L N
⊢ f.toEmbedding.comp f.symm.toEmbedding = Embedding.refl L N
have rw₁ : Eq (α := N ↪[L] N) (toEmbedding (refl L N)) (Embedding.refl L N)
Tactic: rw [← comp_toEmbedding, self_comp_symm, refl_toEmbedding]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
rw : (f.comp f.symm).toEmbedding = Embedding.refl L N
rw₁ : Eq (α := N ↪[L] N) (toEmbedding (refl L N)) (Embedding.refl L N)
⊢ f.toEmbedding.comp f.symm.toEmbedding = Embedding.refl L N
have rw₂ : Eq (α := N ↪[L] N) (Embedding.refl L N) (Embedding.refl L N)
Tactic: rw [← comp_toEmbedding, self_comp_symm, refl_toEmbedding]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ f.symm.toHom.comp f.toHom = Hom.id L M
have rw : (f.symm.comp f).toHom = Hom.id L M
Tactic: rw [← comp_toHom, symm_comp_self, refl_toHom]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
rw : (f.symm.comp f).toHom = Hom.id L M
⊢ f.symm.toHom.comp f.toHom = Hom.id L M
have rw₁ : Eq (α := M →[L] M) (toHom (refl L M)) (Hom.id L M)
Tactic: rw [← comp_toHom, symm_comp_self, refl_toHom]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
rw : (f.symm.comp f).toHom = Hom.id L M
rw₁ : Eq (α := M →[L] M) (toHom (refl L M)) (Hom.id L M)
⊢ f.symm.toHom.comp f.toHom = Hom.id L M
have rw₂ : Eq (α := M →[L] M) (Hom.id L M) (Hom.id L M)
Tactic: rw [← comp_toHom, symm_comp_self, refl_toHom]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ f.toHom.comp f.symm.toHom = Hom.id L N
have rw : (f.comp f.symm).toHom = Hom.id L N
Tactic: rw [← comp_toHom, self_comp_symm, refl_toHom]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
rw : (f.comp f.symm).toHom = Hom.id L N
⊢ f.toHom.comp f.symm.toHom = Hom.id L N
have rw₁ : Eq (α := N →[L] N) (toHom (refl L N)) (Hom.id L N)
Tactic: rw [← comp_toHom, self_comp_symm, refl_toHom]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
rw : (f.comp f.symm).toHom = Hom.id L N
rw₁ : Eq (α := N →[L] N) (toHom (refl L N)) (Hom.id L N)
⊢ f.toHom.comp f.symm.toHom = Hom.id L N
have rw₂ : Eq (α := N →[L] N) (Hom.id L N) (Hom.id L N)
Tactic: rw [← comp_toHom, self_comp_symm, refl_toHom]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : Eq (α := M ≃[L] P) ((fun (f : N ≃[L] P) ↦ f.comp h) f) ((fun (f : N ≃[L] P) ↦ f.comp h) g)
⊢ f = g
have h₁ : f = comp ((fun (f : N ≃[L] P) ↦ f.comp h) f) h.symm
Tactic: convert! (congr_arg (fun r : (M ≃[L] P) ↦ r.comp h.symm) hfg)
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : Eq (α := M ≃[L] P) ((fun (f : N ≃[L] P) ↦ f.comp h) f) ((fun (f : N ≃[L] P) ↦ f.comp h) g)
h₁ : f = comp ((fun (f : N ≃[L] P) ↦ f.comp h) f) h.symm
⊢ f = g
have h₂ : g = comp ((fun (f : N ≃[L] P) ↦ f.comp h) g) h.symm
Tactic: convert! (congr_arg (fun r : (M ≃[L] P) ↦ r.comp h.symm) hfg)
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : Eq (α := M ≃[L] P) ((fun (f : N ≃[L] P) ↦ f.comp h) f) ((fun (f : N ≃[L] P) ↦ f.comp h) g)
⊢ f = comp ((fun (f : N ≃[L] P) ↦ f.comp h) f) h.symm
have h₁ : f = f.comp (h.comp h.symm)
Tactic: rw [comp_assoc, self_comp_symm, comp_refl]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : Eq (α := M ≃[L] P) ((fun (f : N ≃[L] P) ↦ f.comp h) f) ((fun (f : N ≃[L] P) ↦ f.comp h) g)
h₁ : f = f.comp (h.comp h.symm)
⊢ f = comp ((fun (f : N ≃[L] P) ↦ f.comp h) f) h.symm
have h₂ : f = f.comp (refl L N)
Tactic: rw [comp_assoc, self_comp_symm, comp_refl]