mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁵ : L.Structure M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : L.Structure M
inst✝³ : L'.Structure M
inst✝² : L''.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
f : (L.sum L'').Functions n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L.Functions n✝), funMap ((ϕ.sumElim ψ).onFunction (Sum.inl val)) x✝ = funMap (Sum.inl val) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁵ : L.Structure M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : L.Structure M
inst✝³ : L'.Structure M
inst✝² : L''.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
f : (L.sum L'').Functions n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L''.Functions n✝), funMap ((ϕ.sumElim ψ).onFunction (Sum.inr val)) x✝ = funMap (Sum.inr val) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁵ : L.Structure M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : L.Structure M
inst✝³ : L'.Structure M
inst✝² : L''.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
R : (L.sum L'').Relations n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L.Relations n✝), RelMap ((ϕ.sumElim ψ).onRelation (Sum.inl val)) x✝ = RelMap (Sum.inl val) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁵ : L.Structure M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : L.Structure M
inst✝³ : L'.Structure M
inst✝² : L''.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
R : (L.sum L'').Relations n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L''.Relations n✝), RelMap ((ϕ.sumElim ψ).onRelation (Sum.inr val)) x✝ = RelMap (Sum.inr val) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁶ : L.Structure M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : L.Structure M
inst✝⁴ : L'.Structure M
inst✝³ : L₁.Structure M
inst✝² : L₂.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
f : (L.sum L₁).Functions n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L.Functions n✝), funMap ((ϕ.sumMap ψ).onFunction (Sum.inl val)) x✝ = funMap (Sum.inl val) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁶ : L.Structure M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : L.Structure M
inst✝⁴ : L'.Structure M
inst✝³ : L₁.Structure M
inst✝² : L₂.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
f : (L.sum L₁).Functions n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L₁.Functions n✝), funMap ((ϕ.sumMap ψ).onFunction (Sum.inr val)) x✝ = funMap (Sum.inr val) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁶ : L.Structure M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : L.Structure M
inst✝⁴ : L'.Structure M
inst✝³ : L₁.Structure M
inst✝² : L₂.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
R : (L.sum L₁).Relations n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L.Relations n✝), RelMap ((ϕ.sumMap ψ).onRelation (Sum.inl val)) x✝ = RelMap (Sum.inl val) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁶ : L.Structure M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : L.Structure M
inst✝⁴ : L'.Structure M
inst✝³ : L₁.Structure M
inst✝² : L₂.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
R : (L.sum L₁).Relations n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L₁.Relations n✝), RelMap ((ϕ.sumMap ψ).onRelation (Sum.inr val)) x✝ = RelMap (Sum.inr val) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N →[L] P
hmn : M →[L] N
n✝ : ℕ
x✝¹ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ (⇑hnp ∘ ⇑hmn) (funMap x✝¹ x✝) = funMap x✝¹ ((⇑hnp ∘ ⇑hmn) ∘ x✝)

Tactic:
simp

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N →[L] P
hmn : M →[L] N
n✝ : ℕ
x✝¹ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ funMap x✝¹ (⇑hnp ∘ ⇑hmn ∘ x✝) = funMap x✝¹ ((⇑hnp ∘ ⇑hmn) ∘ x✝)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.IsAlgebraic
f : M →[L] N
hf : Function.Injective ⇑f
x✝ : M
⊢ (ofInjective hf).toHom x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: case add
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 2 → R), f.toFun (funMap add x) = funMap add (f.toFun ∘ x)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: case mul
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 2 → R), f.toFun (funMap mul x) = funMap mul (f.toFun ∘ x)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: case neg
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 1 → R), f.toFun (funMap neg x) = funMap neg (f.toFun ∘ x)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: case zero
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 0 → R), f.toFun (funMap zero x) = funMap zero (f.toFun ∘ x)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: case one
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 0 → R), f.toFun (funMap one x) = funMap one (f.toFun ∘ x)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing

Goal state before:
pp: α : Type u_1
p : FreeCommRing α
⊢ Term.realize FreeCommRing.of (-1) = -1

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing

Goal state before:
pp: case var
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a✝ : α
⊢ Term.realize v (var a✝) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (var a✝))

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : (n : ℕ) → DecidableEq (L.Functions n)
a b : α
⊢ a = b ↔ var a = var b

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : (n : ℕ) → DecidableEq (L.Functions n)
a✝ : α
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
⊢ ¬var a✝ = func _f✝ _ts✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : (n : ℕ) → DecidableEq (L.Functions n)
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
a✝ : α
⊢ ¬func _f✝ _ts✝ = var a✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
g : α ≃ β
t : L.Term α
⊢ relabel (⇑g.symm) (relabel (⇑g) t) = t

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
g : α ≃ β
t : L.Term β
⊢ relabel (⇑g) (relabel (⇑g.symm) t) = t

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
α : Type u'
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
h : n✝ ≤ n✝
⊢ castLE h (equal t₁✝ t₂✝) = equal t₁✝ t₂✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
h : n✝ ≤ n✝
⊢ castLE h (rel R✝ ts✝) = rel R✝ ts✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
α : Type u'
k n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km (equal t₁✝ t₂✝)) = castLE ⋯ (equal t₁✝ t₂✝)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
α : Type u'
k n✝¹ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝¹)
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ rel R✝ (Term.relabel (Sum.map id (Fin.castLE mn✝) ∘ Sum.map id (Fin.castLE km✝)) ∘ ts✝) =
    rel R✝ (Term.relabel (Sum.map id (Fin.castLE ⋯)) ∘ ts✝)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n ≃ L'.Relations n
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel (fun n ↦ ⇑(ft n).symm) (fun n ↦ ⇑(fr n).symm) (fun x ↦ id)
      (mapTermRel (fun n ↦ ⇑(ft n)) (fun n ↦ ⇑(fr n)) (fun x ↦ id) φ) =
    φ

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n ≃ L'.Relations n
n : ℕ
φ : L'.BoundedFormula β n
⊢ mapTermRel (fun n ↦ ⇑(ft n)) (fun n ↦ ⇑(fr n)) (fun x ↦ id)
      (mapTermRel (fun n ↦ ⇑(ft n).symm) (fun n ↦ ⇑(fr n).symm) (fun x ↦ id) φ) =
    φ

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case inl.inl
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
l : β
⊢ Sum.elim v xs (Sum.map id (⇑finSumFinEquiv) ((Equiv.sumAssoc β (Fin n) (Fin m)) (Sum.inl (Sum.inl l)))) =
    Sum.elim v (xs ∘ castAdd m) (Sum.inl l)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case inl.inr
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
r : Fin n
⊢ Sum.elim v xs (Sum.map id (⇑finSumFinEquiv) ((Equiv.sumAssoc β (Fin n) (Fin m)) (Sum.inl (Sum.inr r)))) =
    Sum.elim v (xs ∘ castAdd m) (Sum.inr r)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ y ∈ {y, z}

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ z ∈ {y, z}

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
β : Type v'
inst✝ : L'.Structure M
c : {n : ℕ} → L.Functions n → L'.Term (Fin n)
hc : ∀ {n : ℕ} (g : L.Functions n) (y : Fin n → M), realize y g.term = realize y (c g)
v : β → M
a✝ : β
⊢ realize v ((var a✝).substFunc fun {n} ↦ c) = realize v (var a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ (castLE ⋯ (mapTermRel (fun x t ↦ Term.relabel (relabelAux g x) t) (fun x ↦ id) (fun x ↦ castLE ⋯) φ)).all =
    (mapTermRel (fun x t ↦ Term.relabel (relabelAux g x) t) (fun x ↦ id) (fun x ↦ castLE ⋯) φ).all

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
t : L.Term α
s : Set α
h : ↑t.varFinset ⊆ s
v : α → M
⊢ ∀ (a : ↥t.varFinset), (v ∘ Subtype.val) (Set.inclusion h a) = v ↑a

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
γ : Type u_4
t : L.Term (α ⊕ γ)
s : Set α
h : ↑t.varFinsetLeft ⊆ s
v : α → M
xs : γ → M
⊢ ∀ (a : ↥t.varFinsetLeft), Sum.elim (v ∘ Subtype.val) xs (Sum.inl (Set.inclusion h a)) = v ↑a

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
a✝ : β
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (var a✝).constantsToVars = realize v (var a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case refine_1
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨i, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case refine_2
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨j, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n : ℕ
f : L[[α]].Functions n
ts : Fin n → L[[α]].Term β
ih : ∀ (a : Fin n), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)

Tactic:
| @func n f ts ih =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e_v.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
a : α
⊢ (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) (Sum.inl a) =
    Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs) (Sum.inl a)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e_v.inr.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
b : β
⊢ (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) (Sum.inr (Sum.inl b)) =
    Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs) (Sum.inr (Sum.inl b))

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e_v.inr.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
i : Fin n
⊢ (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) (Sum.inr (Sum.inr i)) =
    Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs) (Sum.inr (Sum.inr i))

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case nil
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤ []).Realize v xs ↔ ∀ φ ∈ [], φ.Realize v xs

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
⊢ (List.foldr imp f []).Realize v xs = ((∀ i ∈ [], i.Realize v xs) → f.Realize v xs)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case nil
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ []).Realize v xs ↔ ∃ φ ∈ [], φ.Realize v xs

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case h1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (m + n) → M),
    realize (Sum.elim v xs') (Term.relabel (relabelAux g n) t) =
      realize (Sum.elim (Sum.elim v (xs' ∘ castAdd n) ∘ g) (xs' ∘ natAdd m)) t

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case h2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (id R) x = RelMap R x

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case hv
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ ∀ (n : ℕ) (xs : Fin (m + n) → M) (x : M),
    Sum.elim v (snoc xs x ∘ castAdd (n + 1)) ∘ g = Sum.elim v (xs ∘ castAdd n) ∘ g

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case func
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode ((func f ts).listEncode ++ l) = func f ts :: listDecode l

Tactic:
| @func n f ts ih =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case pos
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
h✝ : ↑i < m
⊢ ↑(castAdd n' i.castSucc) = ↑(castAdd n' i)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case neg
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
h✝ : ¬↑i < m
⊢ ↑(i.castSucc.addNat n') = ↑(i.addNat n')

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
n : ℕ
φ : L.BoundedFormula α n
tf : α → L.Term β
v : β → M
xs : Fin n → M
⊢ ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (id R) x = RelMap R x

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ ∀ (a : ↥φ.freeVarFinset), (v ∘ Subtype.val) (id a) = v ↑a

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case equal
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
f : ↥(equal t₁✝ t₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(equal t₁✝ t₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) t₁✝ = realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) t₂✝ ↔
    realize (Sum.elim v' xs) t₁✝ = realize (Sum.elim v' xs) t₂✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case rel
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
f : ↥(rel R✝ ts✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(rel R✝ ts✝).freeVarFinset), v (f a) = v' ↑a
x✝ : Fin l✝
⊢ realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) (ts✝ x✝) = realize (Sum.elim v' xs) (ts✝ x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
inst✝ : L.Structure Q
f✝ : M ↪ₑ[L] N
x✝ : ℕ
f : L.Functions x✝
x : Fin x✝ → M
⊢ f✝ (funMap f x) = funMap f (⇑f✝ ∘ x)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
inst✝ : L.Structure Q
f : M ↪ₑ[L] N
x✝ : ℕ
R : L.Relations x✝
x : Fin x✝ → M
⊢ RelMap R (⇑f ∘ x) ↔ RelMap R x

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
inst✝ : L.Structure Q
f : M ↪ₑ[L] N
x✝ : ℕ
R : L.Relations x✝
x : Fin x✝ → M
⊢ RelMap R x → RelMap R (⇑f ∘ x)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
s : Set α
h : ↑φ.freeVarFinset ⊆ s
v : α → M
xs : Fin n → M
⊢ ∀ (a : ↥φ.freeVarFinset), (v ∘ Subtype.val) (Set.inclusion h a) = v ↑a

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
xs : Fin n → M
val✝ : L.Relations n
⊢ RelMap
      ((L.lhomWithConstants α).onRelation
        ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) (Sum.inl val✝)))
      xs ↔
    RelMap (Sum.inl val✝) xs

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ (∀' liftAt 1 n φ).Realize v xs ↔ φ.Realize v xs

Tactic:
simp

Goal state after: