awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Substructures
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)
h : ∀ (x_1 : Fin n), Eq.{u_1 + 1} (α := N) (((⇑f : (a : M) → N) ∘ x) x_1) (((⇑g : (a : M) → N) ∘ x) x_1)
⊢ Eq.{u_1 + 1} (α := Fin n → N) ((⇑f : (a : M) → N) ∘ x) ((⇑g : (a : M) → N) ∘ x)

Tactic:
ext
-- Module: Mathlib.ModelTheory.Substructures
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)
x_1 : Fin n
h : Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) (x x_1) : N) (((⇑g : (a : M) → N) ∘ x) x_1 : N)
⊢ Eq.{u_1 + 1} (α := N) (((⇑f : (a : M) → N) ∘ x) x_1) (((⇑g : (a : M) → N) ∘ x) x_1)

Tactic:
rw [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.ModelTheory.Substructures
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)
x_1 : Fin n
h : Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) (x x_1) : N) ((g : (a : M) → N) (x x_1) : N)
⊢ Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) (x x_1) : N) (((⇑g : (a : M) → N) ∘ x) x_1 : N)

Tactic:
rw [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.ModelTheory.Substructures
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)
x_1 : Fin n
h : Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) (x x_1) : N) ((g : (a : M) → N) (x x_1) : N)
⊢ Eq.{u_1 + 1} (α := N) (((⇑f : (a : M) → N) ∘ x) x_1) (((⇑g : (a : M) → N) ∘ x) x_1)

Tactic:
repeat' rw [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.ModelTheory.Substructures
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)
x_1 : Fin n
⊢ Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) (x x_1) : N) ((g : (a : M) → N) (x x_1) : N)

Tactic:
apply hx
-- Module: Mathlib.ModelTheory.Substructures
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)
⊢ 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
-- Module: Mathlib.ModelTheory.Substructures
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)
h : Eq.{u_1 + 1} (α := Fin n → N) ((⇑f : (a : M) → N) ∘ x) ((⇑g : (a : M) → N) ∘ x)
⊢ 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)

Tactic:
simp [h]
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f g : M →[L] N
x : M
⊢ x ∈ f.eqLocus g ↔ Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f g : M →[L] N
s : Set M
h : Set.EqOn.{w, u_1} (β := N) (⇑f : (a : M) → N) (⇑g : (a : M) → N) s
⊢ Set.EqOn.{w, u_1} (β := N) (⇑f : (a : M) → N) (⇑g : (a : M) → N)
    (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M)

Tactic:
show closure L s ≤ f.eqLocus g from closure_le.2 h

Premises used: Iff.mpr, Set.Mem, setOf, Set.EqOn, FirstOrder.Language.Substructure.closure_le
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f g : M →[L] N
h : Set.EqOn.{w, u_1} (β := N) (⇑f : (a : M) → N) (⇑g : (a : M) → N) (↑⊤ : Set M)
⊢ f = g

Tactic:
ext fun _ => h trivial

Premises used: trivial, FirstOrder.Language.Hom.ext
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
s : Set M
hs : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ⊤
f g : M →[L] N
h : Set.EqOn.{w, u_1} (β := N) (⇑f : (a : M) → N) (⇑g : (a : M) → N) s
⊢ f = g

Tactic:
eq_of_eqOn_top <| hs ▸ eqOn_closure h

Premises used: Eq.rec, FirstOrder.Language.Hom.eq_of_eqOn_top, FirstOrder.Language.Hom.eqOn_closure
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
p : L.Substructure M
x : ↥p
⊢ Eq.{u_1 + 1} (α := N) ((f.domRestrict p : (a : ↥p) → N) x : N) ((f : (a : M) → N) (↑x : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Substructures
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
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
⊢ RelMap.{u, v, u_1} (M := ↥p) r ((⇑(Hom.codRestrict p f.toHom h) : (a : M) → ↥p) ∘ x) ↔ RelMap r x

Tactic:
rw [← p.subtype.map_rel]

Premises used: FirstOrder.Language.Embedding.map_rel, FirstOrder.Language.Substructure.subtype
-- Module: Mathlib.ModelTheory.Substructures
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
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
⊢ 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:
change RelMap r (Hom.comp p.subtype.toHom (f.toHom.codRestrict p h) ∘ x) ↔ _

Premises used: FirstOrder.Language.Hom.comp, Function.comp, FirstOrder.Language.Structure.RelMap, FirstOrder.Language.Hom.codRestrict, FirstOrder.Language.Substructure.subtype, DFunLike.coe, FirstOrder.Language.Embedding.toHom
-- Module: Mathlib.ModelTheory.Substructures
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
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)
⊢ 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:
rw [Hom.subtype_comp_codRestrict, ← f.map_rel]

Premises used: FirstOrder.Language.Embedding.map_rel, FirstOrder.Language.Hom.subtype_comp_codRestrict
-- Module: Mathlib.ModelTheory.Substructures
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 ((⇑f.toHom : (a : M) → N) ∘ x) ↔ RelMap.{u, v, u_1} (M := N) r ((⇑f : (a : M) → N) ∘ x)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
p : L.Substructure N
f : M ↪[L] N
h : ∀ (c : M), Membership.mem (α := N) p ((f : (a : M) → N) c : N)
x : M
⊢ Eq.{u_1 + 1} (α := N) ((↑((codRestrict p f h : (a : M) → ↥p) x) : N) : N) ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
p : L.Substructure N
f : M ↪[L] N
h : ∀ (c : M), Membership.mem (α := N) p ((f : (a : M) → N) c : N)
x : M
⊢ Eq.{u_1 + 1} (α := ↥p) ((codRestrict p f h : (a : M) → ↥p) x : ↥p)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ p) ((f : (a : M) → N) x) ⋯ : ↥p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Substructures
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
f : M ↪[L] N
g : N ↪[L] P
p : L.Substructure P
h : ∀ (b : N), Membership.mem (α := P) p ((g : (a : N) → P) b : P)
⊢ (codRestrict p g h).comp f = codRestrict p (g.comp f) ⋯

Tactic:
ext fun _ => rfl

Premises used: FirstOrder.Language.Embedding.ext, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
p : L.Substructure N
h : ∀ (b : M), Membership.mem (α := N) p ((f : (a : M) → N) b : N)
⊢ p.subtype.comp (codRestrict p f h) = f

Tactic:
ext fun _ => rfl

Premises used: FirstOrder.Language.Embedding.ext, rfl
-- Module: Mathlib.ModelTheory.Substructures
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_1 : M ↪[L] N
s : L.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → ↥s
⊢ Eq.{u_1 + 1} (α := ↥(Substructure.map f_1.toHom s))
    ((codRestrict (Substructure.map f_1.toHom s) (f_1.domRestrict s) ⋯ : (a : ↥s) → ↥(Substructure.map f_1.toHom s))
        (funMap f x) :
      ↥(Substructure.map f_1.toHom s))
    (funMap f
        ((⇑(codRestrict (Substructure.map f_1.toHom s) (f_1.domRestrict s) ⋯) :
            (a : ↥s) → ↥(Substructure.map f_1.toHom s)) ∘
          x) :
      ↥(Substructure.map f_1.toHom s))

Tactic:
simp
-- Module: Mathlib.ModelTheory.Substructures
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 : M ↪[L] N
s : L.Substructure M
n : ℕ
R : L.Relations n
x : Fin n → ↥s
⊢ RelMap.{u, v, u_1} (M := ↥(Substructure.map f.toHom s)) R
      ((⇑(codRestrict (Substructure.map f.toHom s) (f.domRestrict s) ⋯) : (a : ↥s) → ↥(Substructure.map f.toHom s)) ∘
        x) ↔
    RelMap R x

Tactic:
simp
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
p : L.Substructure M
x : ↥p
⊢ Eq.{u_1 + 1} (α := N) ((↑((f.substructureEquivMap p : (a : ↥p) → ↥(Substructure.map f.toHom p)) x) : N) : N)
    ((f : (a : M) → N) (↑x : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Substructures
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
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)
⊢ (Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding = f.comp s.subtype

Tactic:
ext
-- Module: Mathlib.ModelTheory.Substructures
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
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:
rfl
-- Module: Mathlib.ModelTheory.Substructures
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_1 : M ↪[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Eq.{u_1 + 1} (α := ↥f_1.toHom.range)
    ((codRestrict f_1.toHom.range f_1 ⋯ : (a : M) → ↥f_1.toHom.range) (funMap f x) : ↥f_1.toHom.range)
    (funMap f ((⇑(codRestrict f_1.toHom.range f_1 ⋯) : (a : M) → ↥f_1.toHom.range) ∘ x) : ↥f_1.toHom.range)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Substructures
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 : M ↪[L] N
n : ℕ
R : L.Relations n
x : Fin n → M
⊢ RelMap.{u, v, u_1} (M := ↥f.toHom.range) R ((⇑(codRestrict f.toHom.range f ⋯) : (a : M) → ↥f.toHom.range) ∘ x) ↔
    RelMap R x

Tactic:
simp
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
x : M
⊢ Eq.{u_1 + 1} (α := N) ((↑((f.equivRange : (a : M) → ↥f.toHom.range) x) : N) : N) ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
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)
⊢ f.toHom.range.subtype.comp f.equivRange.toEmbedding = f

Tactic:
ext
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
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:
rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
h : ∀ (n : N), n ∈ f.toHom.range ↔ Membership.mem (γ := L.Substructure N) ⊤ n
⊢ f.toHom.range = ⊤

Tactic:
ext n
-- Module: Mathlib.ModelTheory.Substructures
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
h : ∃ (y : M), (f : (a : M) → N) y = n
⊢ n ∈ f.toHom.range ↔ Membership.mem (γ := L.Substructure N) ⊤ n

Tactic:
simp only [Hom.mem_range, coe_toHom, Substructure.mem_top, iff_true]

Premises used: FirstOrder.Language.Hom.mem_range, iff_true, FirstOrder.Language.Equiv.coe_toHom, FirstOrder.Language.Substructure.mem_top
-- Module: Mathlib.ModelTheory.Substructures
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
⊢ ∃ (y : M), (f : (a : M) → N) y = n

Tactic:
⟨f.symm n, apply_symm_apply _ _⟩

Premises used: FirstOrder.Language.Equiv.apply_symm_apply, Exists.intro, DFunLike.coe, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Substructures
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
⊢ ∃ (y : M), (f : (a : M) → N) y = n

Tactic:
exact ⟨f.symm n, apply_symm_apply _ _⟩
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
⊢ inclusion ⋯ = Embedding.refl L ↥S

Tactic:
rfl

Premises used: FirstOrder.Language.Embedding.refl, FirstOrder.Language.Substructure.inclusion, Function.Embedding.refl, FirstOrder.Language.Embedding.codRestrict, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S T : L.Substructure M
h : S ≤ T
⊢ (⇑(inclusion h) : (a : ↥S) → ↥T) = Set.inclusion (s := (↑S : Set M)) (t := (↑T : Set M)) h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
h : ∀ (x : M), x ∈ S.subtype.toHom.range ↔ x ∈ S
⊢ S.subtype.toHom.range = S

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
x : M
h : (∃ (y : ↥S), (↑y : M) = x) ↔ x ∈ S
⊢ x ∈ S.subtype.toHom.range ↔ x ∈ S

Tactic:
simp only [Hom.mem_range, Embedding.coe_toHom, coe_subtype]

Premises used: FirstOrder.Language.Hom.mem_range, FirstOrder.Language.Substructure.coe_subtype, FirstOrder.Language.Embedding.coe_toHom
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
x : M
⊢ (∃ (y : ↥S), (↑y : M) = x) ↔ x ∈ S

Tactic:
⟨?_, fun h => ⟨⟨x, h⟩, rfl⟩⟩

Premises used: Subtype.mk, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
x : M
h : (∃ (y : ↥S), (↑y : M) = x) → x ∈ S
⊢ (∃ (y : ↥S), (↑y : M) = x) ↔ x ∈ S

Tactic:
refine ⟨?_, fun h => ⟨⟨x, h⟩, rfl⟩⟩
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
y : M
hy : y ∈ S
⊢ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ S) y hy) : M) ∈ S

Tactic:
hy

Premises used: Set.Mem
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
y : M
hy : y ∈ S
⊢ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ S) y hy) : M) ∈ S

Tactic:
exact hy
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S T : L.Substructure M
h : S ≤ T
⊢ T.subtype.comp (inclusion h) = S.subtype

Tactic:
rfl

Premises used: FirstOrder.Language.Embedding.comp, Set.Mem, FirstOrder.Language.Substructure.subtype, rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst : DecidableEq α
inst_1 : (n : ℕ) → DecidableEq (L.Functions n)
a b : α
⊢ a = b ↔ Eq (α := L.Term α) (var a) (var b)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
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
subst :
  ∀ (g : L.Functions m) (ys : Fin m → L.Term α),
    (f = Eq.rec (motive := fun (x : ℕ) (h : m = x) ↦ L.Functions x) g ⋯ ∧ ∀ (i : Fin m), xs i = ys (Fin.cast ⋯ i)) ↔
      func f xs = func g ys
⊢ (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

Tactic:
subst h
-- Module: Mathlib.ModelTheory.Syntax
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 α
this : DecidableEq (L.Term α) := instDecidableEq
g : L.Functions m
ys : Fin m → L.Term α
⊢ (f = Eq.rec (motive := fun (x : ℕ) (h : m = x) ↦ L.Functions x) g ⋯ ∧ ∀ (i : Fin m), xs i = ys (Fin.cast ⋯ i)) ↔
    func f xs = func g ys

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.ModelTheory.Syntax
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
⊢ ¬func f xs = func g ys

Tactic:
simp [h]
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst : DecidableEq α
inst_1 : (n : ℕ) → DecidableEq (L.Functions n)
a : α
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
⊢ ¬var a = func _f _ts

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst : DecidableEq α
inst_1 : (n : ℕ) → DecidableEq (L.Functions n)
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
a : α
⊢ ¬func _f _ts = var a

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
a : α
⊢ Eq (α := L.Term α) (relabel id (var a)) (var a)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
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:
simp [ih]
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
t : L.Term α
var : ∀ (a : α), Eq (α := L.Term α) (relabel id (Language.var a)) (Language.var a)
func :
  ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α) (ih : ∀ (a : Fin l), relabel id (_ts a) = _ts a),
    relabel id (Language.func _f _ts) = Language.func _f _ts
⊢ relabel id t = t

Tactic:
induction t with
  | var => rfl
  | func _ _ ih => simp [ih]

Premises used: FirstOrder.Language.Term.func, FirstOrder.Language.Term.var
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
⊢ Eq (α := L.Term α → L.Term α) (relabel id) id

Tactic:
funext relabel_id

Premises used: funext, FirstOrder.Language.Term.relabel_id
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
a : α
⊢ Eq (α := L.Term γ) (relabel g (relabel f (var a))) (relabel (g ∘ f) (var a))

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
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:
simp [ih]
-- Module: Mathlib.ModelTheory.Syntax
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))
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 (Language.func _f _ts)) = relabel (g ∘ f) (Language.func _f _ts)
⊢ relabel g (relabel f t) = relabel (g ∘ f) t

Tactic:
induction t with
  | var => rfl
  | func _ _ ih => simp [ih]

Premises used: FirstOrder.Language.Term.func, FirstOrder.Language.Term.var
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
⊢ Eq (α := L.Term α → L.Term γ) (relabel g ∘ relabel f) (relabel (g ∘ f))

Tactic:
funext (relabel_relabel f g)

Premises used: funext, FirstOrder.Language.Term.relabel_relabel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
g : α ≃ β
t : L.Term α
⊢ relabel.{u, v, v', u'} (α := β) (⇑g.symm : (a : β) → α) (relabel (⇑g : (a : α) → β) t) = t

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
g : α ≃ β
t : L.Term β
⊢ relabel.{u, v, u', v'} (α := α) (⇑g : (a : α) → β) (relabel (⇑g.symm : (a : β) → α) t) = t

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
a : α
⊢ Eq (α := L[[γ]].Term α) (varsToConstants (constantsToVars (var a))) (var a)

Tactic:
rfl