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

Goal state before:
pp: case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : ↥f₁✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₁✝.freeVarFinset), v (f a) = v' ↑a) → ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : ↥f₂✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₂✝.freeVarFinset), v (f a) = v' ↑a) → ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : ↥(f₁✝ ⟹ f₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(f₁✝ ⟹ f₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ ∀ (a : ↥f₂✝.freeVarFinset), v ((f ∘ Set.inclusion ⋯) a) = v' ↑a

pp: case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : ↥f₁✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₁✝.freeVarFinset), v (f a) = v' ↑a) → ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : ↥f₂✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₂✝.freeVarFinset), v (f a) = v' ↑a) → ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : ↥(f₁✝ ⟹ f₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(f₁✝ ⟹ f₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ ∀ (a : ↥f₁✝.freeVarFinset), v ((f ∘ Set.inclusion ⋯) a) = v' ↑a

Tactic:
<;>

Goal state after:
case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : ↥f₁✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₁✝.freeVarFinset), v (f a) = v' ↑a) → ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : ↥f₂✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₂✝.freeVarFinset), v (f a) = v' ↑a) → ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : ↥(f₁✝ ⟹ f₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(f₁✝ ⟹ f₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ ∀ (a : ↥f₂✝.freeVarFinset), v ((f ∘ Set.inclusion ⋯) a) = v' ↑a

case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : ↥f₁✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₁✝.freeVarFinset), v (f a) = v' ↑a) → ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : ↥f₂✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₂✝.freeVarFinset), v (f a) = v' ↑a) → ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : ↥(f₁✝ ⟹ f₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(f₁✝ ⟹ f₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ ∀ (a : ↥f₁✝.freeVarFinset), v ((f ∘ Set.inclusion ⋯) a) = v' ↑a
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case inl
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
i : α
⊢ (Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n)))) (Sum.inl i) = Sum.elim (v ∘ ⇑g) xs (Sum.inl i)

pp: case inr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
i : Fin n
⊢ (Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n)))) (Sum.inr i) = Sum.elim (v ∘ ⇑g) xs (Sum.inr i)

Tactic:
<;>

Goal state after:
case inl
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
i : α
⊢ (Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n)))) (Sum.inl i) = Sum.elim (v ∘ ⇑g) xs (Sum.inl i)

case inr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
i : Fin n
⊢ (Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n)))) (Sum.inr i) = Sum.elim (v ∘ ⇑g) xs (Sum.inr i)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
s : Set M
inst✝ : Countable ((l : ℕ) × L.Functions l)
h : s.Countable
⊢ Countable ↥((closure L).toFun s)

Tactic:
have : Countable s := h.to_subtype
  rw [← mk_le_aleph0_iff, ← lift_le_aleph0]
  exact lift_card_closure_le_card_term.trans mk_le_aleph0

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case e_v.inl.inl
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
val✝ : ↑A
⊢ (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) (Sum.inl (Sum.inl val✝)) =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ (Sum.inl (Sum.inl val✝))

pp: case e_v.inl.inr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
val✝ : α
⊢ (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) (Sum.inl (Sum.inr val✝)) =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ (Sum.inl (Sum.inr val✝))

pp: case e_v.inr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
val✝ : Fin n✝
⊢ (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) (Sum.inr val✝) =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case e_v.inl.inl
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
val✝ : ↑A
⊢ (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) (Sum.inl (Sum.inl val✝)) =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ (Sum.inl (Sum.inl val✝))

case e_v.inl.inr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
val✝ : α
⊢ (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) (Sum.inl (Sum.inr val✝)) =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ (Sum.inl (Sum.inr val✝))

case e_v.inr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
val✝ : Fin n✝
⊢ (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) (Sum.inr val✝) =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ (Sum.inr val✝)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.inf f)

Tactic:
refine Finset.induction definable_univ (fun i s _ h => ?_) s

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : i ∉ s
h : A.Definable L (s.inf f)
⊢ A.Definable L ((insert i s).inf f)
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: case e'_8.last
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
v : Fin 1 → M
⊢ Fin.snoc (Subtype.val ∘ x) (v 0) (Fin.last n) =
    ((Sum.elim (fun a ↦ Term.realize v (Fin.lastCases (var 0) (fun j ↦ (L.con ⟨↑(x j), ⋯⟩).term) a)) default ∘
          Sum.inl ∘ Sum.elim Empty.elim id) ∘
        Sum.inr)
      (Fin.last n)

pp: case e'_8.cast
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
v : Fin 1 → M
i✝ : Fin n
⊢ Fin.snoc (Subtype.val ∘ x) (v 0) i✝.castSucc =
    ((Sum.elim (fun a ↦ Term.realize v (Fin.lastCases (var 0) (fun j ↦ (L.con ⟨↑(x j), ⋯⟩).term) a)) default ∘
          Sum.inl ∘ Sum.elim Empty.elim id) ∘
        Sum.inr)
      i✝.castSucc

Tactic:
<;>

Goal state after:
case e'_8.last
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
v : Fin 1 → M
⊢ Fin.snoc (Subtype.val ∘ x) (v 0) (Fin.last n) =
    ((Sum.elim (fun a ↦ Term.realize v (Fin.lastCases (var 0) (fun j ↦ (L.con ⟨↑(x j), ⋯⟩).term) a)) default ∘
          Sum.inl ∘ Sum.elim Empty.elim id) ∘
        Sum.inr)
      (Fin.last n)

case e'_8.cast
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
v : Fin 1 → M
i✝ : Fin n
⊢ Fin.snoc (Subtype.val ∘ x) (v 0) i✝.castSucc =
    ((Sum.elim (fun a ↦ Term.realize v (Fin.lastCases (var 0) (fun j ↦ (L.con ⟨↑(x j), ⋯⟩).term) a)) default ∘
          Sum.inl ∘ Sum.elim Empty.elim id) ∘
        Sum.inr)
      i✝.castSucc
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
⊢ ↥S ⊨ ψ

Tactic:
← Formula.realize_equivSentence_symm_con,

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
⊢ (equivSentence.symm ψ).Realize fun a ↦ ↑(L.con a)
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: case e'_7.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  (BoundedFormula.constantsVarsEquiv φ).Realize (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (⇑S.subtype ∘ default)
val✝ : ↑↑S
⊢ Sum.elim (fun a ↦ ↑(L.con a)) (Subtype.val ∘ v') (Sum.inl val✝) =
    (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (Sum.inl val✝)

pp: case e'_7.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  (BoundedFormula.constantsVarsEquiv φ).Realize (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (⇑S.subtype ∘ default)
val✝ : Fin 1
⊢ Sum.elim (fun a ↦ ↑(L.con a)) (Subtype.val ∘ v') (Sum.inr val✝) =
    (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case e'_7.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  (BoundedFormula.constantsVarsEquiv φ).Realize (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (⇑S.subtype ∘ default)
val✝ : ↑↑S
⊢ Sum.elim (fun a ↦ ↑(L.con a)) (Subtype.val ∘ v') (Sum.inl val✝) =
    (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (Sum.inl val✝)

case e'_7.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  (BoundedFormula.constantsVarsEquiv φ).Realize (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (⇑S.subtype ∘ default)
val✝ : Fin 1
⊢ Sum.elim (fun a ↦ ↑(L.con a)) (Subtype.val ∘ v') (Sum.inr val✝) =
    (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (Sum.inr val✝)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case h₁.e__v.inl
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
val✝ : α
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) Sum.inr (Sum.inl val✝)) =
    Sum.elim v y (Sum.inl val✝)

pp: case h₁.e__v.inr
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
val✝ : γ
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) Sum.inr (Sum.inr val✝)) =
    Sum.elim v y (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case h₁.e__v.inl
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
val✝ : α
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) Sum.inr (Sum.inl val✝)) =
    Sum.elim v y (Sum.inl val✝)

case h₁.e__v.inr
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
val✝ : γ
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) Sum.inr (Sum.inr val✝)) =
    Sum.elim v y (Sum.inr val✝)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case left
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable L.Symbols

pp: case right
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable (constantsOn α).Symbols

Tactic:
<;>

Goal state after:
case left
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable L.Symbols

case right
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable (constantsOn α).Symbols
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case left
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable α

pp: case right
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable L.Symbols

Tactic:
<;>

Goal state after:
case left
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable α

case right
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable L.Symbols
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{w, max v u} (max ℵ₀ L.card) ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')

Tactic:
rw [lift_max, lift_aleph0, max_le_iff, aleph0_le_lift, and_comm, ← lift_le.{w'},
        lift_lift, lift_lift, ← aleph0_le_lift, h]
      refine ⟨?_, h1⟩
      rw [← lift_lift.{w', w}]
      refine _root_.trans (lift_le.{w}.2 h3) ?_
      rw [lift_lift, ← lift_lift.{w, max u v}, ← hs', ← h, lift_lift]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case pos
M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst✝ : DecidablePred p
hp : A.Definable L (ofPred p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w | p (w ∘ some)}
hP : A.Definable L P
w : Option α → M
h : p (w ∘ some)
⊢ (w ∈ tupleGraph fun v ↦ if p v then f v else g v) ↔ w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g

pp: case neg
M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst✝ : DecidablePred p
hp : A.Definable L (ofPred p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w | p (w ∘ some)}
hP : A.Definable L P
w : Option α → M
h : ¬p (w ∘ some)
⊢ (w ∈ tupleGraph fun v ↦ if p v then f v else g v) ↔ w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g

Tactic:
<;>

Goal state after:
case pos
M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst✝ : DecidablePred p
hp : A.Definable L (ofPred p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w | p (w ∘ some)}
hP : A.Definable L P
w : Option α → M
h : p (w ∘ some)
⊢ (w ∈ tupleGraph fun v ↦ if p v then f v else g v) ↔ w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g

case neg
M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst✝ : DecidablePred p
hp : A.Definable L (ofPred p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w | p (w ∘ some)}
hP : A.Definable L P
w : Option α → M
h : ¬p (w ∘ some)
⊢ (w ∈ tupleGraph fun v ↦ if p v then f v else g v) ↔ w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing

Goal state before:
pp: case pos
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
a✝ : m ∈ (monoms i).attach
h0 : f (Sum.inl ⟨i, m⟩) = 0
⊢ f (Sum.inl ⟨i, m⟩) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x = 0

pp: case neg
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
a✝ : m ∈ (monoms i).attach
h0 : ¬f (Sum.inl ⟨i, m⟩) = 0
⊢ f (Sum.inl ⟨i, m⟩) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x =
    f (Sum.inl ⟨i, m⟩) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
a✝ : m ∈ (monoms i).attach
h0 : f (Sum.inl ⟨i, m⟩) = 0
⊢ f (Sum.inl ⟨i, m⟩) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x = 0

case neg
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
a✝ : m ∈ (monoms i).attach
h0 : ¬f (Sum.inl ⟨i, m⟩) = 0
⊢ f (Sum.inl ⟨i, m⟩) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x =
    f (Sum.inl ⟨i, m⟩) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite ↑M
φ : L.Sentence
w✝ : T.ModelType
h✝ : #↑w✝ = κ
MF : T.ModelType
hMF : ¬↑MF ⊨ φ
MT : T.ModelType
hMT : ¬¬↑MT ⊨ φ
⊢ False

Tactic:
Classical.not_not

Goal state after:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite ↑M
φ : L.Sentence
w✝ : T.ModelType
h✝ : #↑w✝ = κ
MF : T.ModelType
hMF : ¬↑MF ⊨ φ
MT : T.ModelType
hMT : ↑MT ⊨ φ
⊢ False
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case refine_1
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ ℵ₀ ≤ lift.{v, u} #↥S

pp: case refine_2
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ ℵ₀ ≤ lift.{u, v} #X

Tactic:
<;>

Goal state after:
case refine_1
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ ℵ₀ ≤ lift.{v, u} #↥S

case refine_2
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ ℵ₀ ≤ lift.{u, v} #X
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_2.inl.inl
a : Cardinal.{u}
ha : ℵ₀ ≤ a
c : Cardinal.{u}
hbc : a ∣ 0 * c
hz : 0 * c = 0
⊢ a ∣ 0 ∨ a ∣ c

pp: case refine_2.inl.inr
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b : Cardinal.{u}
hbc : a ∣ b * 0
hz : b * 0 = 0
⊢ a ∣ b ∨ a ∣ 0

Tactic:
<;>

Goal state after:
case refine_2.inl.inl
a : Cardinal.{u}
ha : ℵ₀ ≤ a
c : Cardinal.{u}
hbc : a ∣ 0 * c
hz : 0 * c = 0
⊢ a ∣ 0 ∨ a ∣ c

case refine_2.inl.inr
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b : Cardinal.{u}
hbc : a ∣ b * 0
hz : b * 0 = 0
⊢ a ∣ b ∨ a ∣ 0
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case inl
n : ℕ
h✝¹ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
h✝ : b = 0
⊢ False

pp: case inr
n : ℕ
h✝¹ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
h✝ : c = 0
⊢ False

Tactic:
<;>

Goal state after:
case inl
n : ℕ
h✝¹ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
h✝ : b = 0
⊢ False

case inr
n : ℕ
h✝¹ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
h✝ : c = 0
⊢ False
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b

pp: n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b

Tactic:
<;>

Goal state after:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b

n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b