awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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.Hom.comp, 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
⊢ f.comp (id L M) = f

Tactic:
rfl

Premises used: FirstOrder.Language.Hom.comp, 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
⊢ comp (id L N) f = f

Tactic:
rfl

Premises used: FirstOrder.Language.Hom.comp, 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
f g : M ↪[L] N
h : Eq (α := (a : M) → N) ((fun (f : M ↪[L] N) ↦ f.toFun) f) ((fun (f : M ↪[L] N) ↦ f.toFun) g)
mk :
  ∀ (toEmbedding : M ↪ N)
    (map_fun' :
      ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding.toFun (funMap f x) = funMap f (toEmbedding.toFun ∘ x))
    (map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding.toFun ∘ x) ↔ RelMap r x)
    (h :
      Eq (α := (a : M) → N)
        ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' })
        ((fun (f : M ↪[L] N) ↦ f.toFun) g)),
    { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' : M ↪[L] N } = g
⊢ f = g

Tactic:
cases f
-- 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
g : M ↪[L] N
toEmbedding : M ↪ N
map_fun' :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding.toFun (funMap f x) = funMap f (toEmbedding.toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding.toFun ∘ x) ↔ RelMap r x
h :
  Eq (α := (a : M) → N)
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' })
    ((fun (f : M ↪[L] N) ↦ f.toFun) g)
mk :
  ∀ (toEmbedding_1 : M ↪ N)
    (map_fun'_1 :
      ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toEmbedding_1.toFun (funMap f x) = funMap f (toEmbedding_1.toFun ∘ x))
    (map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding_1.toFun ∘ x) ↔ RelMap r x)
    (h :
      Eq (α := (a : M) → N)
        ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' })
        ((fun (f : M ↪[L] N) ↦ f.toFun)
          { toEmbedding := toEmbedding_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 })),
    { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' : M ↪[L] N } =
      { toEmbedding := toEmbedding_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 }
⊢ { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' : M ↪[L] N } = g

Tactic:
cases g
-- 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
toEmbedding : M ↪ N
map_fun' :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding.toFun (funMap f x) = funMap f (toEmbedding.toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding.toFun ∘ x) ↔ RelMap r x
toEmbedding_1 : M ↪ N
map_fun'_1 :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding_1.toFun (funMap f x) = funMap f (toEmbedding_1.toFun ∘ x)
map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding_1.toFun ∘ x) ↔ RelMap r x
h :
  Eq (α := (a : M) → N)
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' })
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 })
mk : toEmbedding = toEmbedding_1
⊢ { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' : M ↪[L] N } =
    { toEmbedding := toEmbedding_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 }

Tactic:
congr
-- 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
toEmbedding : M ↪ N
map_fun' :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding.toFun (funMap f x) = funMap f (toEmbedding.toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding.toFun ∘ x) ↔ RelMap r x
toEmbedding_1 : M ↪ N
map_fun'_1 :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding_1.toFun (funMap f x) = funMap f (toEmbedding_1.toFun ∘ x)
map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding_1.toFun ∘ x) ↔ RelMap r x
h :
  Eq (α := (a : M) → N)
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' })
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 })
mk : ∀ (x : M), Eq.{w' + 1} (α := N) ((toEmbedding : (a : M) → N) x : N) ((toEmbedding_1 : (a : M) → N) x : N)
⊢ toEmbedding = toEmbedding_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
toEmbedding : M ↪ N
map_fun' :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding.toFun (funMap f x) = funMap f (toEmbedding.toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding.toFun ∘ x) ↔ RelMap r x
toEmbedding_1 : M ↪ N
map_fun'_1 :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding_1.toFun (funMap f x) = funMap f (toEmbedding_1.toFun ∘ x)
map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding_1.toFun ∘ x) ↔ RelMap r x
h :
  Eq (α := (a : M) → N)
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' })
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 })
x : M
⊢ Eq.{w' + 1} (α := N) ((toEmbedding : (a : M) → N) x : N) ((toEmbedding_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
toEmbedding : M ↪ N
map_fun' :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding.toFun (funMap f x) = funMap f (toEmbedding.toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding.toFun ∘ x) ↔ RelMap r x
toEmbedding_1 : M ↪ N
map_fun'_1 :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding_1.toFun (funMap f x) = funMap f (toEmbedding_1.toFun ∘ x)
map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding_1.toFun ∘ x) ↔ RelMap r x
h :
  Eq (α := (a : M) → N)
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' })
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 })
x : M
⊢ Eq.{w' + 1} (α := N) ((toEmbedding : (a : M) → N) x : N) ((toEmbedding_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
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
⊢ 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 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: FirstOrder.Language.Embedding.coe_injective, funext
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f f' : M ↪[L] N
h : Eq (α := M →[L] N) ((fun (x : M ↪[L] N) ↦ x.toHom) f) ((fun (x : M ↪[L] N) ↦ x.toHom) f')
h₁ : ∀ (x : M), Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((f' : (a : M) → N) x : N)
⊢ f = f'

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 f' : M ↪[L] N
h : Eq (α := M →[L] N) ((fun (x : M ↪[L] N) ↦ x.toHom) f) ((fun (x : M ↪[L] N) ↦ x.toHom) f')
x : M
⊢ Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((f' : (a : M) → N) x : N)

Tactic:
congr_fun (congr_arg (↑) h) _

Premises used: congr_arg, congr_fun
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f f' : M ↪[L] N
h : Eq (α := M →[L] N) ((fun (x : M ↪[L] N) ↦ x.toHom) f) ((fun (x : M ↪[L] N) ↦ x.toHom) f')
x : M
⊢ Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((f' : (a : M) → N) x : N)

Tactic:
exact congr_fun (congr_arg (↑) h) _

Premises used: congr_arg, congr_fun
-- 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
⊢ f.toHom = g.toHom ↔ f = g

Tactic:
⟨fun h ↦ toHom_injective h, fun h ↦ congr_arg (·.toHom) h⟩

Premises used: FirstOrder.Language.Embedding.toHom_injective, Iff.intro
-- 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:
f.toEmbedding.injective

Premises used: FirstOrder.Language.Embedding.toEmbedding, Function.Embedding.injective
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.IsAlgebraic
f : M →[L] N
hf : Function.Injective.{w + 1, w' + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Eq (α := (a : M) → N) (⇑(ofInjective hf) : (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
inst_2 : L.IsAlgebraic
f : M →[L] N
hf : Function.Injective.{w + 1, w' + 1} (α := M) (β := N) (⇑f : (a : M) → N)
h : ∀ (x : M), Eq.{w' + 1} (α := N) (((ofInjective hf).toHom : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
⊢ (ofInjective hf).toHom = f

Tactic:
ext
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.IsAlgebraic
f : M →[L] N
hf : Function.Injective.{w + 1, w' + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : M
⊢ Eq.{w' + 1} (α := N) (((ofInjective hf).toHom : (a : M) → N) x : N) ((f : (a : M) → N) x : N)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
inst : L.Structure M
x : M
⊢ (refl L M : (a : M) → M) x = x

Tactic:
rfl

Premises used: 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.Embedding.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.Embedding.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
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.Embedding.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 (DFunLike.congr_fun hfg x)

Premises used: DFunLike.congr_fun, FirstOrder.Language.Embedding.injective
-- 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 (DFunLike.congr_fun hfg x)

Premises used: DFunLike.congr_fun, FirstOrder.Language.Embedding.injective
-- 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
⊢ h.comp f = h.comp g ↔ f = g

Tactic:
⟨fun eq ↦ h.comp_injective eq, congr_arg h.comp⟩

Premises used: FirstOrder.Language.Embedding.comp, congr_arg, Iff.intro, FirstOrder.Language.Embedding.comp_injective
-- 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.toHom.comp f = h.toHom.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.toHom.comp f = h.toHom.comp g
x : M
⊢ Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

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

Premises used: DFunLike.congr_fun, FirstOrder.Language.Embedding.injective
-- 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.toHom.comp f = h.toHom.comp g
x : M
⊢ Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

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

Premises used: DFunLike.congr_fun, FirstOrder.Language.Embedding.injective
-- 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
⊢ h.toHom.comp f = h.toHom.comp g ↔ f = g

Tactic:
⟨fun eq ↦ h.toHom_comp_injective eq, congr_arg h.toHom.comp⟩

Premises used: FirstOrder.Language.Hom.comp, congr_arg, FirstOrder.Language.Embedding.toHom_comp_injective, Iff.intro, 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
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
f : M ↪[L] N
⊢ f.comp (refl L M) = f

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, 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
⊢ comp (refl L N) f = f

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, 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.Hom.id, FirstOrder.Language.Embedding.toHom, 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
f g : M ≃[L] N
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
mk :
  ∀ (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)
    (h₁ : { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.toFun = g.toFun)
    (h₂ : { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.invFun = g.invFun),
    { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N } = g
⊢ f = g

Tactic:
cases f
-- 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
g : M ≃[L] N
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
h₁ : { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.toFun = g.toFun
h₂ : { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.invFun = g.invFun
mk :
  ∀ (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 }
⊢ { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N } = g

Tactic:
cases g
-- 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 : toEquiv = toEquiv_1
⊢ { 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 }

Tactic:
simp only [mk.injEq]

Premises used: FirstOrder.Language.Equiv.mk.injEq