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

Goal state before:
pp: case func.zero
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L.Functions 0
_ts✝ : Fin 0 → L.Term (γ ⊕ α)
ih : ∀ (a : Fin 0), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝

pp: case func.succ
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
f : L.Functions (n✝ + 1)
_ts✝ : Fin (n✝ + 1) → L.Term (γ ⊕ α)
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝

Tactic:
<;>

Goal state after:
case func.zero
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L.Functions 0
_ts✝ : Fin 0 → L.Term (γ ⊕ α)
ih : ∀ (a : Fin 0), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝

case func.succ
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
f : L.Functions (n✝ + 1)
_ts✝ : Fin (n✝ + 1) → L.Term (γ ⊕ α)
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝
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)

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:
<;>

Goal state after:
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)

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)
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case inl
α : Type u'
n k : ℕ
val✝ : α
⊢ relabelAux Sum.inl k (Sum.inl val✝) = Sum.map id (natAdd n) (Sum.inl val✝)

pp: case inr
α : Type u'
n k : ℕ
val✝ : Fin k
⊢ relabelAux Sum.inl k (Sum.inr val✝) = Sum.map id (natAdd n) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u'
n k : ℕ
val✝ : α
⊢ relabelAux Sum.inl k (Sum.inl val✝) = Sum.map id (natAdd n) (Sum.inl val✝)

case inr
α : Type u'
n k : ℕ
val✝ : Fin k
⊢ relabelAux Sum.inl k (Sum.inr val✝) = Sum.map id (natAdd n) (Sum.inr val✝)
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 ∈ F⟮y, z⟯

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 ∈ F⟮y, z⟯

Tactic:
<;>

Goal state after:
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 ∈ F⟮y, z⟯

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 ∈ F⟮y, z⟯
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}

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:
<;>

Goal state after:
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}

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}
Module: Mathlib.ModelTheory.Algebra.Field.Basic

Goal state before:
pp: case addAssoc
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ addAssoc.toSentence ↔ toProp K addAssoc

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

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

Goal state before:
pp: case zeroAdd
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ zeroAdd.toSentence ↔ toProp K zeroAdd

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

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

Goal state before:
pp: case negAddCancel
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ negAddCancel.toSentence ↔ toProp K negAddCancel

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

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

Goal state before:
pp: case mulAssoc
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ mulAssoc.toSentence ↔ toProp K mulAssoc

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

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

Goal state before:
pp: case mulComm
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ mulComm.toSentence ↔ toProp K mulComm

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

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

Goal state before:
pp: case oneMul
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ oneMul.toSentence ↔ toProp K oneMul

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

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

Goal state before:
pp: case existsInv
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ existsInv.toSentence ↔ toProp K existsInv

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

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

Goal state before:
pp: case leftDistrib
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ leftDistrib.toSentence ↔ toProp K leftDistrib

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

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

Goal state before:
pp: case existsPairNE
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ existsPairNE.toSentence ↔ toProp K existsPairNE

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var.inl
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
val✝ : α
f : ↥(var (Sum.inl val✝)).varFinsetLeft → β
hxs' : ∀ (a : ↥(var (Sum.inl val✝)).varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a
⊢ realize xs ((var (Sum.inl val✝)).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (var (Sum.inl val✝))

pp: case var.inr
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
val✝ : γ
f : ↥(var (Sum.inr val✝)).varFinsetLeft → β
hxs' : ∀ (a : ↥(var (Sum.inr val✝)).varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a
⊢ realize xs ((var (Sum.inr val✝)).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (var (Sum.inr val✝))

Tactic:
<;>

Goal state after:
case var.inl
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
val✝ : α
f : ↥(var (Sum.inl val✝)).varFinsetLeft → β
hxs' : ∀ (a : ↥(var (Sum.inl val✝)).varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a
⊢ realize xs ((var (Sum.inl val✝)).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (var (Sum.inl val✝))

case var.inr
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
val✝ : γ
f : ↥(var (Sum.inr val✝)).varFinsetLeft → β
hxs' : ∀ (a : ↥(var (Sum.inr val✝)).varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a
⊢ realize xs ((var (Sum.inr val✝)).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (var (Sum.inr val✝))
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ (RelMap r fun i ↦ ⟦x i⟧) ↔ RelMap r x

Tactic:
change
    Quotient.lift (@RelMap L M ps.toStructure n r) Prestructure.rel_equiv (Quotient.finChoice _) ↔
      _
  rw [Quotient.finChoice_eq, Quotient.lift_mk]

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: case neg.inl
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
H : CharP K p
h✝ : Nat.Prime p
⊢ False

pp: case neg.inr
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
H : CharP K p
h✝ : p = 0
⊢ False

Tactic:
<;>

Goal state after:
case neg.inl
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
H : CharP K p
h✝ : Nat.Prime p
⊢ False

case neg.inr
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
H : CharP K p
h✝ : p = 0
⊢ False
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var.inl
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 v (var (Sum.inl a)).varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (var (Sum.inl a))

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

Tactic:
<;>

Goal state after:
case var.inl
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 v (var (Sum.inl a)).varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (var (Sum.inl a))

case var.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
b : β
⊢ realize v (var (Sum.inr b)).varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (var (Sum.inr b))
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)

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))

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:
<;>

Goal state after:
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)

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))

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))
Module: Mathlib.ModelTheory.Semantics

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

pp: case neg
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
f' : L.BoundedFormula α k
tail✝ : List (L.BoundedFormula α k)
tail_ih✝ : (List.foldr imp f tail✝).Realize v xs = ((∀ i ∈ tail✝, i.Realize v xs) → f.Realize v xs)
h✝ : ¬f'.Realize v xs
⊢ (List.foldr imp f (f' :: tail✝)).Realize v xs = ((∀ i ∈ f' :: tail✝, i.Realize v xs) → f.Realize v xs)

Tactic:
<;>

Goal state after:
case pos
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
f' : L.BoundedFormula α k
tail✝ : List (L.BoundedFormula α k)
tail_ih✝ : (List.foldr imp f tail✝).Realize v xs = ((∀ i ∈ tail✝, i.Realize v xs) → f.Realize v xs)
h✝ : f'.Realize v xs
⊢ (List.foldr imp f (f' :: tail✝)).Realize v xs = ((∀ i ∈ f' :: tail✝, i.Realize v xs) → f.Realize v xs)

case neg
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
f' : L.BoundedFormula α k
tail✝ : List (L.BoundedFormula α k)
tail_ih✝ : (List.foldr imp f tail✝).Realize v xs = ((∀ i ∈ tail✝, i.Realize v xs) → f.Realize v xs)
h✝ : ¬f'.Realize v xs
⊢ (List.foldr imp f (f' :: tail✝)).Realize v xs = ((∀ i ∈ f' :: tail✝, i.Realize v xs) → f.Realize v xs)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∃ x, ¬¬θ.Realize v (snoc xs x)) ↔ ∃ a, θ.Realize v (snoc xs a)

Tactic:
Classical.not_not

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case cons
L : Language
α : Type u'
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
t : L.Term α
l : List (L.Term α)
lih : listDecode (flatMap listEncode l) = l
⊢ listDecode (flatMap listEncode (t :: l)) = t :: l

Tactic:
| cons t l lih =>

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

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

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:
<;>

Goal state after:
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

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

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
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
h✝ : k < m
⊢ ↑(Fin.cast h (castAdd n' (last k))) = ↑(last (k + n'))

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
h✝ : ¬k < m
⊢ ↑(Fin.cast h ((last k).addNat n')) = ↑(last (k + n'))

Tactic:
<;>

Goal state after:
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
h✝ : k < m
⊢ ↑(Fin.cast h (castAdd n' (last k))) = ↑(last (k + n'))

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
h✝ : ¬k < m
⊢ ↑(Fin.cast h ((last k).addNat n')) = ↑(last (k + n'))
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)

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:
<;>

Goal state after:
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)

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')