awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Basic
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
mk : ∀ (x : M), Eq.{w' + 1} (α := N) ((toEquiv : (a : M) → N) x : N) ((toEquiv_1 : (a : M) → N) x : N)
⊢ toEquiv = toEquiv_1

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Basic
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
x : M
⊢ Eq.{w' + 1} (α := N) ((toEquiv : (a : M) → N) x : N) ((toEquiv_1 : (a : M) → N) x : N)

Tactic:
funext_iff.1 h₁ x

Premises used: funext_iff, Iff.mp
-- Module: Mathlib.ModelTheory.Basic
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
x : M
⊢ Eq.{w' + 1} (α := N) ((toEquiv : (a : M) → N) x : N) ((toEquiv_1 : (a : M) → N) x : N)

Tactic:
exact funext_iff.1 h₁ x

Premises used: funext_iff, Iff.mp
-- Module: Mathlib.ModelTheory.Basic
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
simp : Eq.{w + 1} (α := M) ((f.symm : (a : N) → M) (funMap f' x) : M) (funMap f' ((⇑f.symm : (a : N) → M) ∘ x) : M)
⊢ f.symm.toFun (funMap f' x) = funMap f' (f.symm.toFun ∘ x)

Tactic:
simp only [Equiv.toFun_as_coe]

Premises used: Equiv.toFun_as_coe
-- Module: Mathlib.ModelTheory.Basic
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 = (f.toEquiv : (a : M) → N) (funMap f' ((⇑f.symm : (a : N) → M) ∘ x))
⊢ Eq.{w + 1} (α := M) ((f.symm : (a : N) → M) (funMap f' x) : M) (funMap f' ((⇑f.symm : (a : N) → M) ∘ x) : M)

Tactic:
rw [Equiv.symm_apply_eq]

Premises used: Equiv.symm_apply_eq
-- Module: Mathlib.ModelTheory.Basic
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))

Tactic:
Eq.trans ?_ (f.map_fun' f' (f.toEquiv.symm ∘ x)).symm

Premises used: FirstOrder.Language.Equiv.map_fun', Function.comp, FirstOrder.Language.Equiv.toEquiv, Equiv.symm, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.ModelTheory.Basic
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
refine : funMap f' x = funMap f' (f.toFun ∘ (⇑f.symm : (a : N) → M) ∘ x)
⊢ funMap f' x = (f.toEquiv : (a : M) → N) (funMap f' ((⇑f.symm : (a : N) → M) ∘ x))

Tactic:
refine Eq.trans ?_ (f.map_fun' f' (f.toEquiv.symm ∘ x)).symm

Premises used: FirstOrder.Language.Equiv.map_fun', Function.comp, FirstOrder.Language.Equiv.toEquiv, Equiv.symm, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.ModelTheory.Basic
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)
rw₃ rw₄ : funMap f' x = funMap f' x
⊢ 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]

Premises used: Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.comp_assoc, Function.id_comp
-- Module: Mathlib.ModelTheory.Basic
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
simp : RelMap.{u, v, w} (M := M) r ((⇑f.symm : (a : N) → M) ∘ x) ↔ RelMap r x
⊢ RelMap r (f.symm.toFun ∘ x) ↔ RelMap r x

Tactic:
simp only [Equiv.toFun_as_coe]

Premises used: Equiv.toFun_as_coe
-- Module: Mathlib.ModelTheory.Basic
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

Tactic:
(f.map_rel' r (f.toEquiv.symm ∘ x)).symm.trans ?_

Premises used: FirstOrder.Language.Equiv.map_rel', Function.comp, FirstOrder.Language.Equiv.toEquiv, Iff.trans, Equiv.symm, DFunLike.coe, Iff.symm
-- Module: Mathlib.ModelTheory.Basic
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
refine : RelMap r (f.toFun ∘ (⇑f.symm : (a : N) → M) ∘ x) ↔ RelMap r x
⊢ RelMap.{u, v, w} (M := M) r ((⇑f.symm : (a : N) → M) ∘ x) ↔ RelMap r x

Tactic:
refine (f.map_rel' r (f.toEquiv.symm ∘ x)).symm.trans ?_

Premises used: FirstOrder.Language.Equiv.map_rel', Function.comp, FirstOrder.Language.Equiv.toEquiv, Iff.trans, Equiv.symm, DFunLike.coe, Iff.symm
-- Module: Mathlib.ModelTheory.Basic
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
rw₃ rw₄ : RelMap r x ↔ RelMap r x
⊢ 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]

Premises used: Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.comp_assoc, Function.id_comp
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ f.symm.symm = f

Tactic:
rfl

Premises used: Equiv.symm, rfl, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
⊢ Function.Bijective (α := M ≃[L] N) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, FirstOrder.Language.Equiv.symm_symm
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
a : N
⊢ (f : (a : M) → N) ((f.symm : (a : N) → M) a : M) = a

Tactic:
f.toEquiv.apply_symm_apply a

Premises used: Equiv.apply_symm_apply, FirstOrder.Language.Equiv.toEquiv
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
a : M
⊢ (f.symm : (a : N) → M) ((f : (a : M) → N) a : N) = a

Tactic:
f.toEquiv.symm_apply_apply a

Premises used: Equiv.symm_apply_apply, FirstOrder.Language.Equiv.toEquiv
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
φ : M ≃[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Eq.{w' + 1} (α := N) ((φ : (a : M) → N) (funMap f x) : N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N)

Tactic:
HomClass.map_fun φ f x

Premises used: FirstOrder.Language.HomClass.map_fun
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
φ : M ≃[L] N
c : L.Constants
⊢ Eq.{w' + 1} (α := N) ((φ : (a : M) → N) (↑c : M) : N) ((↑c : N) : N)

Tactic:
HomClass.map_constants φ c

Premises used: FirstOrder.Language.HomClass.map_constants
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
φ : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ RelMap.{u, v, w'} (M := N) r ((⇑φ : (a : M) → N) ∘ x) ↔ RelMap r x

Tactic:
StrongHomClass.map_rel φ r x

Premises used: FirstOrder.Language.StrongHomClass.map_rel
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ f.toEmbedding.toHom = f.toHom

Tactic:
rfl

Premises used: FirstOrder.Language.Equiv.toHom, FirstOrder.Language.StrongHomClass.toEmbedding, FirstOrder.Language.HomClass.toHom, FirstOrder.Language.Equiv.toEmbedding, rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ Eq (α := (a : M) → N) (⇑f.toHom : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ Eq (α := (a : M) → N) (⇑f.toEmbedding : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
a₁ : M ≃[L] N
_ : ∀ ⦃a₂ : M ≃[L] N⦄, a₁.toEmbedding = a₂.toEmbedding → a₁ = a₂
⊢ ∀ ⦃a₂ : M ≃[L] N⦄, a₁.toEmbedding = a₂.toEmbedding → a₁ = a₂

Tactic:
_
-- Module: Mathlib.ModelTheory.Basic
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 :
  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₂)
⊢ a₁ = a₂

Tactic:
apply DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.ModelTheory.Basic
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
⊢ 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:
congr_arg (DFunLike.coe ∘ Embedding.toHom) h

Premises used: Function.comp, congr_arg, DFunLike.coe, FirstOrder.Language.Embedding.toHom
-- Module: Mathlib.ModelTheory.Basic
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
⊢ 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:
exact congr_arg (DFunLike.coe ∘ Embedding.toHom) h

Premises used: Function.comp, congr_arg, DFunLike.coe, FirstOrder.Language.Embedding.toHom
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
⊢ Function.Injective (α := M ≃[L] N) (β := M → N) (DFunLike.coe (β := fun (x : M) ↦ N))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f g : M ≃[L] N
h : ∀ (x : M), Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
⊢ f = g

Tactic:
coe_injective (funext h)

Premises used: funext, FirstOrder.Language.Equiv.coe_injective
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ Function.Bijective.{w + 1, w' + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
EquivLike.bijective f

Premises used: EquivLike.bijective
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ Function.Injective.{w + 1, w' + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
EquivLike.injective f

Premises used: EquivLike.injective
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ Function.Surjective.{w + 1, w' + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
EquivLike.surjective f

Premises used: EquivLike.surjective
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
inst : L.Structure M
x : M
simp : ({ toEquiv := _root_.Equiv.refl M, map_fun' := ⋯, map_rel' := ⋯ } : (a : M) → M) x = x
⊢ (refl L M : (a : M) → M) x = x

Tactic:
simp [refl]

Premises used: FirstOrder.Language.Equiv.refl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
inst : L.Structure M
x : M
⊢ ({ toEquiv := _root_.Equiv.refl M, map_fun' := ⋯, map_rel' := ⋯ } : (a : M) → M) x = x

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Basic
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
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))
⊢ 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))

Tactic:
simp only [Function.comp_apply, map_fun]

Premises used: FirstOrder.Language.Equiv.map_fun, Function.comp_apply
-- Module: Mathlib.ModelTheory.Basic
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)
    (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:
trivial
-- Module: Mathlib.ModelTheory.Basic
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
rw₂ rw₃ : RelMap r 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

Tactic:
rw [Function.comp_assoc, map_rel, map_rel]

Premises used: FirstOrder.Language.Equiv.map_rel, Function.comp_assoc
-- Module: Mathlib.ModelTheory.Basic
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
g : N ≃[L] P
f : M ≃[L] N
x : M
⊢ Eq.{u_1 + 1} (α := P) ((g.comp f : (a : M) → P) x : P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : M ≃[L] N
⊢ g.comp (refl L M) = g

Tactic:
rfl

Premises used: FirstOrder.Language.Equiv.comp, rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : M ≃[L] N
⊢ comp (refl L N) g = g

Tactic:
rfl

Premises used: FirstOrder.Language.Equiv.comp, rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ Eq (α := M ↪[L] M) (toEmbedding (refl L M)) (Embedding.refl L M)

Tactic:
rfl

Premises used: FirstOrder.Language.StrongHomClass.toEmbedding, FirstOrder.Language.Embedding.refl, FirstOrder.Language.Equiv.toEmbedding, Function.Embedding.refl, rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ Eq (α := M →[L] M) (toHom (refl L M)) (Hom.id L M)

Tactic:
rfl

Premises used: FirstOrder.Language.Equiv.toHom, FirstOrder.Language.Hom.id, rfl
-- Module: Mathlib.ModelTheory.Basic
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
Q : Type u_2
inst_3 : L.Structure Q
f : M ≃[L] N
g : N ≃[L] P
h : P ≃[L] Q
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
rfl

Premises used: FirstOrder.Language.Equiv.comp, rfl
-- Module: Mathlib.ModelTheory.Basic
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
h₁ : ∀ (x : M), Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Basic
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
x : M
⊢ Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

Tactic:
h.injective (congr_fun (congr_arg DFunLike.coe hfg) x)

Premises used: FirstOrder.Language.Equiv.injective, congr_arg, congr_fun, DFunLike.coe
-- Module: Mathlib.ModelTheory.Basic
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
x : M
⊢ Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

Tactic:
exact h.injective (congr_fun (congr_arg DFunLike.coe hfg) x)

Premises used: FirstOrder.Language.Equiv.injective, congr_arg, congr_fun, DFunLike.coe
-- Module: Mathlib.ModelTheory.Basic
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
hnp : N ≃[L] P
hmn : M ≃[L] N
⊢ (hnp.comp hmn).toHom = hnp.toHom.comp hmn.toHom

Tactic:
rfl

Premises used: FirstOrder.Language.Hom.comp, FirstOrder.Language.HomClass.toHom, rfl
-- Module: Mathlib.ModelTheory.Basic
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
hnp : N ≃[L] P
hmn : M ≃[L] N
⊢ (hnp.comp hmn).toEmbedding = hnp.toEmbedding.comp hmn.toEmbedding

Tactic:
rfl

Premises used: FirstOrder.Language.Embedding.comp, FirstOrder.Language.StrongHomClass.toEmbedding, rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
h : ∀ (x : N), Eq (α := N) ((f.comp f.symm : (a : N) → N) x : N) ((refl L N : (a : N) → N) x : N)
⊢ f.comp f.symm = refl L N

Tactic:
ext
-- Module: Mathlib.ModelTheory.Basic
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
h₂ h₃ : x = x
⊢ Eq (α := N) ((f.comp f.symm : (a : N) → N) x : N) ((refl L N : (a : N) → N) x : N)

Tactic:
rw [comp_apply, apply_symm_apply, refl_apply]

Premises used: FirstOrder.Language.Equiv.refl_apply, FirstOrder.Language.Equiv.apply_symm_apply, FirstOrder.Language.Equiv.comp_apply
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
h : ∀ (x : M), Eq (α := M) ((f.symm.comp f : (a : M) → M) x : M) ((refl L M : (a : M) → M) x : M)
⊢ f.symm.comp f = refl L M

Tactic:
ext
-- Module: Mathlib.ModelTheory.Basic
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
h₂ h₃ : x = x
⊢ Eq (α := M) ((f.symm.comp f : (a : M) → M) x : M) ((refl L M : (a : M) → M) x : M)

Tactic:
rw [comp_apply, symm_apply_apply, refl_apply]

Premises used: FirstOrder.Language.Equiv.symm_apply_apply, FirstOrder.Language.Equiv.refl_apply, FirstOrder.Language.Equiv.comp_apply
-- Module: Mathlib.ModelTheory.Basic
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)
rw₂ rw₃ : Eq (α := M ↪[L] M) (Embedding.refl L M) (Embedding.refl L M)
⊢ f.symm.toEmbedding.comp f.toEmbedding = Embedding.refl L M

Tactic:
rw [← comp_toEmbedding, symm_comp_self, refl_toEmbedding]

Premises used: FirstOrder.Language.Equiv.comp_toEmbedding, FirstOrder.Language.Equiv.symm_comp_self, FirstOrder.Language.Equiv.refl_toEmbedding