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

Goal state before:
pp: case all.e__v.inr.refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin (n✝ + 1)
⊢ ∀ (i : Fin n✝),
    Sum.elim v (fun x ↦ snoc default a (castAdd 0 x))
        (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) (fun x ↦ Sum.map Sum.inr id (finSumFinEquiv.symm x))
          (Sum.inr i.castSucc)) =
      Sum.elim (fun x ↦ v (Sum.inl x)) (snoc (fun x ↦ v (Sum.inr x)) a) (Sum.inr i.castSucc)

Tactic:
·

Goal state after:
case all.e__v.inr.refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin (n✝ + 1)
⊢ ∀ (i : Fin n✝),
    Sum.elim v (fun x ↦ snoc default a (castAdd 0 x))
        (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) (fun x ↦ Sum.map Sum.inr id (finSumFinEquiv.symm x))
          (Sum.inr i.castSucc)) =
      Sum.elim (fun x ↦ v (Sum.inl x)) (snoc (fun x ↦ v (Sum.inr x)) a) (Sum.inr i.castSucc)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s) → A.Definable L s

Tactic:
·

Goal state after:
case mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s) → A.Definable L s
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ A.Definable L s ↔ ∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s

Tactic:
by
  classical
  constructor
  · simp only [definable_iff_exists_formula_sum]
    rintro ⟨φ, rfl⟩
    let A0 := (φ.freeVarFinset.toLeft).image Subtype.val
    refine ⟨A0, by simp [A0], (φ.restrictFreeVar <| fun x => Sum.casesOn x.1
        (fun x hx => Sum.inl ⟨x, by simp [A0, hx]⟩) (fun x _ => Sum.inr x) x.2), ?_⟩
    ext
    simp only [Formula.Realize, mem_ofPred_eq, Finset.coe_sort_coe]
    exact iff_comm.1 <| BoundedFormula.realize_restrictFreeVar _ (by simp)
  · rintro ⟨A0, hA0, hd⟩
    exact Definable.mono hd hA0

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) → ∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)

pp: case mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)) → ∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x

Tactic:
·

Goal state after:
case mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) → ∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e__xs
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin 0
⊢ snoc default a (natAdd 1 x) = default x

Tactic:
·

Goal state after:
case e__xs
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin 0
⊢ snoc default a (natAdd 1 x) = default x
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)) → ∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x

Tactic:
·

Goal state after:
case mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)) → ∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ (sum fun i ↦ lift.{max u v, u} #(L.Functions i)) ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

pp: L : Language
⊢ ℵ₀ ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

Tactic:
·

Goal state after:
L : Language
⊢ (sum fun i ↦ lift.{max u v, u} #(L.Functions i)) ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ ℵ₀ ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

Tactic:
·

Goal state after:
L : Language
⊢ ℵ₀ ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ #((n : ℕ) × L.BoundedFormula Empty n)

pp: L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty n) ≤ max ℵ₀ L.card

Tactic:
·

Goal state after:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ #((n : ℕ) × L.BoundedFormula Empty n)
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty n) ≤ max ℵ₀ L.card

Tactic:
·

Goal state after:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty n) ≤ max ℵ₀ L.card
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case mp
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ (∃ v, M ⊨ equivSentence φ) → M ⊨ φ.exClosure

pp: case mpr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ M ⊨ φ.exClosure → ∃ v, M ⊨ equivSentence φ

Tactic:
·

Goal state after:
case mp
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ (∃ v, M ⊨ equivSentence φ) → M ⊨ φ.exClosure
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case mpr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ M ⊨ φ.exClosure → ∃ v, M ⊨ equivSentence φ

Tactic:
·

Goal state after:
case mpr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ M ⊨ φ.exClosure → ∃ v, M ⊨ equivSentence φ
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case h
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LHom.sumInl.substructureReduct S)
a : M
h : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
φ' : (L.sum L.skolem₁).Functions n := ⋯
⊢ φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑⟨funMap φ' (Subtype.val ∘ x), ?w⟩)

pp: case w
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LHom.sumInl.substructureReduct S)
a : M
h : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
φ' : (L.sum L.skolem₁).Functions n := LHom.sumInr.onFunction φ
⊢ funMap φ' (Subtype.val ∘ x) ∈ LHom.sumInl.substructureReduct S

Tactic:
·

Goal state after:
case h
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LHom.sumInl.substructureReduct S)
a : M
h : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
φ' : (L.sum L.skolem₁).Functions n := ⋯
⊢ φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑⟨funMap φ' (Subtype.val ∘ x), ?w⟩)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mp
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ ((∃ a ∈ s,
        ((a ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘
              ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) →
    ∃ x_1 ∈ s, x_1 ∘ f = x

pp: case intro.intro.mpr
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ (∃ x_1 ∈ s, x_1 ∘ f = x) →
    (∃ a ∈ s,
        ((a ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘
              ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))

Tactic:
·

Goal state after:
case intro.intro.mp
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ ((∃ a ∈ s,
        ((a ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘
              ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) →
    ∃ x_1 ∈ s, x_1 ∘ f = x
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case w
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LHom.sumInl.substructureReduct S)
a : M
h : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
φ' : (L.sum L.skolem₁).Functions n := LHom.sumInr.onFunction φ
⊢ funMap φ' (Subtype.val ∘ x) ∈ LHom.sumInl.substructureReduct S

Tactic:
·

Goal state after:
case w
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LHom.sumInl.substructureReduct S)
a : M
h : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
φ' : (L.sum L.skolem₁).Functions n := LHom.sumInr.onFunction φ
⊢ funMap φ' (Subtype.val ∘ x) ∈ LHom.sumInl.substructureReduct S
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.mp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)) → ∀ (x : M), f✝.Realize v (snoc xs x)

pp: case all.mpr
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : M), f✝.Realize v (snoc xs x)) → ∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)

Tactic:
·

Goal state after:
case all.mp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)) → ∀ (x : M), f✝.Realize v (snoc xs x)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mpr
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ (∃ x_1 ∈ s, x_1 ∘ f = x) →
    (∃ a ∈ s,
        ((a ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘
              ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))

Tactic:
·

Goal state after:
case intro.intro.mpr
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ (∃ x_1 ∈ s, x_1 ∘ f = x) →
    (∃ a ∈ s,
        ((a ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘
              ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.mpr
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : M), f✝.Realize v (snoc xs x)) → ∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)

Tactic:
·

Goal state after:
case all.mpr
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : M), f✝.Realize v (snoc xs x)) → ∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mpr.refine_1
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
⊢ ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    (y ∘ f) ∘ rangeSplitting f

pp: case intro.intro.mpr.refine_2
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
a : α
⊢ (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))

Tactic:
·

Goal state after:
case intro.intro.mpr.refine_1
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
⊢ ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    (y ∘ f) ∘ rangeSplitting f
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mpr.refine_2
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
a : α
⊢ (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))

Tactic:
·

Goal state after:
case intro.intro.mpr.refine_2
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
a : α
⊢ (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: 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'
⊢ ℵ₀ ≤ #↑s' ∧
    #↑(s ∪ ⇑Equiv.ulift '' s') ≤ #↑(⇑Equiv.ulift '' s') ∧
      lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i) ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')

pp: 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.{max u v, w} #↑(s ∪ ⇑Equiv.ulift '' s')

Tactic:
·

Goal state after:
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'
⊢ ℵ₀ ≤ #↑s' ∧
    #↑(s ∪ ⇑Equiv.ulift '' s') ≤ #↑(⇑Equiv.ulift '' s') ∧
      lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i) ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case refine_1
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'
⊢ #↑s + #↑(⇑Equiv.ulift '' s') ≤ #↑(⇑Equiv.ulift '' s')

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

Goal state after:
case refine_1
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'
⊢ #↑s + #↑(⇑Equiv.ulift '' s') ≤ #↑(⇑Equiv.ulift '' s')
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:
·

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