awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
ι : Type u_1
T : ι → L.Theory
h :
  ∀ (h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)), IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)
h₁ :
  ∀ (h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)),
    IsFinitelySatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)
h₂ :
  ∀ (h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)) (s : Finset L.Sentence)
    (hs : (↑s : Set L.Sentence) ⊆ ⋃ (i : ι), T i), IsSatisfiable (↑s : Set L.Sentence)
⊢ IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i) ↔ ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)
have h₃ : ∀ (h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)) (s : Finset L.Sentence)
  (hs : (↑s : Set L.Sentence) ⊆ ⋃ (t : Finset ι), ⋃ i ∈ t, T i), IsSatisfiable (↑s : Set L.Sentence)
Tactic: classical
    refine
      ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _),
        fun h => ?_⟩
    rw [isSatisfiable_iff_isFinitelySatisfiable]
    intro s hs
    rw [Set.iUnion_eq_iUnion_finset] at hs
    obtain ⟨t, ht⟩ := Directed.exists_mem_subset_of_finset_subset_biUnion (by
      exact Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
        Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩) hs
    exact (h t).mono ht
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
ι : Type u_1
T : ι → L.Theory
h :
  ∀ (h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)), IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)
h₁ :
  ∀ (h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)),
    IsFinitelySatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)
h₂ :
  ∀ (h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)) (s : Finset L.Sentence)
    (hs : (↑s : Set L.Sentence) ⊆ ⋃ (i : ι), T i), IsSatisfiable (↑s : Set L.Sentence)
h₃ :
  ∀ (h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)) (s : Finset L.Sentence)
    (hs : (↑s : Set L.Sentence) ⊆ ⋃ (t : Finset ι), ⋃ i ∈ t, T i), IsSatisfiable (↑s : Set L.Sentence)
⊢ IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i) ↔ ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)
have h₄ : ∀ (h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)) (s : Finset L.Sentence)
  (hs : (↑s : Set L.Sentence) ⊆ ⋃ (t : Finset ι), ⋃ i ∈ t, T i) (t : Finset ι)
  (ht : (↑s : Set L.Sentence) ⊆ ⋃ i ∈ t, T i), IsSatisfiable (↑s : Set L.Sentence)
Tactic: classical
    refine
      ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _),
        fun h => ?_⟩
    rw [isSatisfiable_iff_isFinitelySatisfiable]
    intro s hs
    rw [Set.iUnion_eq_iUnion_finset] at hs
    obtain ⟨t, ht⟩ := Directed.exists_mem_subset_of_finset_subset_biUnion (by
      exact Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
        Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩) hs
    exact (h t).mono ht
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
inst_1 : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
⊢ ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∧ #(↑N : Type w) = κ
have obtain : ∀ (S : L.ElementarySubstructure M),
  ∅ ⊆ (↑S : Set M) →
    ∀ (hS : lift.{w, w'} #↥S = lift.{w', w} κ),
      ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∧ #(↑N : Type w) = κ
Tactic: obtain ⟨S, _, hS⟩ := exists_elementarySubstructure_card_eq L ∅ κ h1 (by simp) h2 h3
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
M : Type w'
inst : L.Structure M
inst_1 : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left : ∅ ⊆ (↑S : Set M)
hS : lift.{w, w'} #↥S = lift.{w', w} κ
⊢ Small.{w, w'} ↥S
have hS₁ : lift.{w + 1, w'} #↥S = lift.{max w' (w + 1), w} κ
Tactic: rw [← lift_inj.{_, w + 1}, lift_lift, lift_lift] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
M : Type w'
inst : L.Structure M
inst_1 : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left : ∅ ⊆ (↑S : Set M)
hS : lift.{w, w'} #↥S = lift.{w', w} κ
⊢ ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∧ #(↑N : Type w) = κ
have this : Small.{w, w'} ↥S
Tactic: have : Small.{w} S := by
    rw [← lift_inj.{_, w + 1}, lift_lift, lift_lift] at hS
    exact small_iff_lift_mk_lt_univ.2 (lt_of_eq_of_lt hS κ.lift_lt_univ')
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
inst_1 : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left : ∅ ⊆ (↑S : Set M)
hS : lift.{w, w'} #↥S = lift.{w', w} κ
this : Small.{w, w'} ↥S
⊢ ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∧ #(↑N : Type w) = κ
have L₁ : lift.{w', w} #(↑(Equiv.bundledInduced.{u, v, w', w} L (M := ↥S) (N := Shrink.{w, w'} ↥S) (equivShrink ↥S)) : Type w) =
  lift.{w, w'} #↥S
Tactic: refine
    ⟨(equivShrink S).bundledInduced L,
      ⟨S.subtype.comp (Equiv.bundledInducedEquiv L _).symm.toElementaryEmbedding⟩,
      lift_inj.1 (_root_.trans ?_ hS)⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{w, w'} #M ≤ lift.{w', w} κ
⊢ ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w)) ∧ #(↑N : Type w) = κ
have obtain : ∀ (N0 : (L.elementaryDiagram M).ModelType)
  (hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))),
  ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w)) ∧ #(↑N : Type w) = κ
Tactic: obtain ⟨N0, hN0⟩ := (L.elementaryDiagram M).exists_large_model_of_infinite_model κ M
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{w, w'} #M ≤ lift.{w', w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))
⊢ ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w)) ∧ #(↑N : Type w) = κ
have rw : ∀ (h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ) (N0 : (L.elementaryDiagram M).ModelType)
  (hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))),
  ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w)) ∧ #(↑N : Type w) = κ
Tactic: rw [← lift_le.{max u v}, lift_lift, lift_lift] at h2
Cleared hypotheses: h2, N0, hN0
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))
⊢ lift.{w, max (max w' u) v} L[[M]].card ≤ lift.{max (max w' u) v, w} κ
have simp : lift.{max w' w, max u v} L.card + lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ
Tactic: simp only [card_withConstants, lift_add, lift_lift]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))
⊢ lift.{max w' w, max u v} L.card + lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ
have rw : lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ ∧
  lift.{max w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ
Tactic: rw [add_comm, add_eq_max (aleph0_le_lift.2 (infinite_iff.1 iM)), max_le_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))
⊢ lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ ∧
    lift.{max w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ
have rw : ∀ (h1 : lift.{max w w', max u v} L.card ≤ lift.{max (max u v) w', w} κ)
  (h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ) (N0 : (L.elementaryDiagram M).ModelType)
  (hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))),
  lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ ∧
    lift.{max w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ
Tactic: rw [← lift_le.{w'}, lift_lift, lift_lift] at h1
Cleared hypotheses: h1, h2, N0, hN0
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))
⊢ #(↑N0 : Type (max (max (max u w') v) w)) ≤ lift.{w, max (max (max u v) w) w'} #(↑N0 : Type (max (max (max u v) w) w'))
have rw : #(↑N0 : Type (max (max (max u w') v) w)) ≤
  lift.{max (max (max (max u v) w) w') w, max (max (max u v) w) w'} #(↑N0 : Type (max (max (max u v) w) w'))
Tactic: rw [← lift_umax, lift_id]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))
rw :
  #(↑N0 : Type (max (max (max u w') v) w)) ≤
    lift.{max (max (max (max u v) w) w') w, max (max (max u v) w) w'} #(↑N0 : Type (max (max (max u v) w) w'))
⊢ #(↑N0 : Type (max (max (max u w') v) w)) ≤ lift.{w, max (max (max u v) w) w'} #(↑N0 : Type (max (max (max u v) w) w'))
have rw₁ : #(↑N0 : Type (max (max (max u w') v) w)) ≤ #(↑N0 : Type (max (max (max u w') v) w))
Tactic: rw [← lift_umax, lift_id]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))
⊢ ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w)) ∧ #(↑N : Type w) = κ
have obtain : ∀ (N : Bundled L[[M]].Structure) (hN : #(↑N : Type w) = κ)
  (NN0 : (↑N : Type w) ↪ₑ[L[[M]]] (↑N0 : Type (max (max (max u v) w) w'))),
  ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w)) ∧ #(↑N : Type w) = κ
Tactic: obtain ⟨N, ⟨NN0⟩, hN⟩ :=
    exists_elementaryEmbedding_card_eq_of_le L[[M]] N0 κ
      (aleph0_le_lift.1 ((aleph0_le_lift.2 (aleph0_le_mk M)).trans h2))
      (by
        simp only [card_withConstants, lift_add, lift_lift]
        rw [add_comm, add_eq_max (aleph0_le_lift.2 (infinite_iff.1 iM)), max_le_iff]
        rw [← lift_le.{w'}, lift_lift, lift_lift] at h1
        exact ⟨h2, h1⟩)
      (hN0.trans (by rw [← lift_umax, lift_id]))
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))
N : Bundled L[[M]].Structure
hN : #(↑N : Type w) = κ
NN0 : (↑N : Type w) ↪ₑ[L[[M]]] (↑N0 : Type (max (max (max u v) w) w'))
this : Structure.{u, v, w} L (↑N : Type w) := (L.lhomWithConstants M).reduct (↑N : Type w)
⊢ ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w)) ∧ #(↑N : Type w) = κ
have h : (↑N : Type w) ⊨ L.elementaryDiagram M
Tactic: haveI h : N ⊨ L.elementaryDiagram M :=
    (NN0.theory_model_iff (L.elementaryDiagram M)).2 inferInstance
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))
N : Bundled L[[M]].Structure
hN : #(↑N : Type w) = κ
NN0 : (↑N : Type w) ↪ₑ[L[[M]]] (↑N0 : Type (max (max (max u v) w) w'))
this : Structure.{u, v, w} L (↑N : Type w) := (L.lhomWithConstants M).reduct (↑N : Type w)
h : (↑N : Type w) ⊨ L.elementaryDiagram M
⊢ ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w)) ∧ #(↑N : Type w) = κ
have refine : ElementaryEmbedding.{w', w, u, v} L M (↑(Bundled.of (↑N : Type w)) : Type w)
Tactic: refine ⟨Bundled.of N, ⟨?_⟩, hN⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w', w} κ ≤ lift.{w, w'} #M
⊢ ∃ (N : Bundled L.Structure),
    (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
        Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
      #(↑N : Type w) = κ
have inl : ∀ (N : Bundled L.Structure) (hN1 : Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M))
  (hN2 : #(↑N : Type w) = κ),
  ∃ (N : Bundled L.Structure),
    (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
        Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
      #(↑N : Type w) = κ
Tactic: obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w, w'} #M < lift.{w', w} κ
⊢ ∃ (N : Bundled L.Structure),
    (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
        Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
      #(↑N : Type w) = κ
have inr : ∀ (N : Bundled L.Structure) (hN1 : Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w)))
  (hN2 : #(↑N : Type w) = κ),
  ∃ (N : Bundled L.Structure),
    (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
        Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
      #(↑N : Type w) = κ
Tactic: obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
⊢ ∃ (N : Bundled L.Structure),
    (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
        Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
      #(↑N : Type w) = κ
have x : lift.{w', w} κ ≤ lift.{w, w'} #M ∨ lift.{w, w'} #M < lift.{w', w} κ
Tactic: cases le_or_gt (lift.{w'} κ) (Cardinal.lift.{w} #M) with
  | inl h =>
    obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
    exact ⟨N, Or.inl hN1, hN2⟩
  | inr h =>
    obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)
    exact ⟨N, Or.inr hN1, hN2⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
inst_1 : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
⊢ ∃ (N : Bundled L.Structure), ElementarilyEquivalent.{u, v, w', w} L M (↑N : Type w) ∧ #(↑N : Type w) = κ
have inl : ∀ (N : Bundled L.Structure) (hNκ : #(↑N : Type w) = κ)
  (NM : Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M)),
  ∃ (N : Bundled L.Structure), ElementarilyEquivalent.{u, v, w', w} L M (↑N : Type w) ∧ #(↑N : Type w) = κ
Tactic: obtain ⟨N, NM | MN, hNκ⟩ := exists_elementaryEmbedding_card_eq L M κ h1 h2
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w'
inst : L.Structure M
inst_1 : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
inl :
  ∀ (N : Bundled L.Structure) (hNκ : #(↑N : Type w) = κ)
    (NM : Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M)),
    ∃ (N : Bundled L.Structure), ElementarilyEquivalent.{u, v, w', w} L M (↑N : Type w) ∧ #(↑N : Type w) = κ
⊢ ∃ (N : Bundled L.Structure), ElementarilyEquivalent.{u, v, w', w} L M (↑N : Type w) ∧ #(↑N : Type w) = κ
have inr : ∀ (N : Bundled L.Structure) (hNκ : #(↑N : Type w) = κ)
  (MN : Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))),
  ∃ (N : Bundled L.Structure), ElementarilyEquivalent.{u, v, w', w} L M (↑N : Type w) ∧ #(↑N : Type w) = κ
Tactic: obtain ⟨N, NM | MN, hNκ⟩ := exists_elementaryEmbedding_card_eq L M κ h1 h2
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
M : T.ModelType
MI : Infinite (↑M : Type (max u v))
⊢ ∃ (N : ModelType.{u, v, w} T), #(↑N : Type w) = κ
have intro : ∀ (N : Bundled L.Structure) (hN : (↑M : Type (max u v)) ≅[L] (↑N : Type w)) (h1 : ℵ₀ ≤ #(↑N : Type w))
  (h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} #(↑N : Type w)),
  ∃ (N_1 : ModelType.{u, v, w} T), #(↑N_1 : Type w) = #(↑N : Type w)
Tactic: obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
Cleared hypotheses: κ, h1, h2
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
T : L.Theory
M : T.ModelType
MI : Infinite (↑M : Type (max u v))
N : Bundled L.Structure
hN : (↑M : Type (max u v)) ≅[L] (↑N : Type w)
h1 : ℵ₀ ≤ #(↑N : Type w)
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} #(↑N : Type w)
⊢ ∃ (N_1 : ModelType.{u, v, w} T), #(↑N_1 : Type w) = #(↑N : Type w)
have this : Nonempty.{w + 1} (↑N : Type w)
Tactic: haveI : Nonempty N := hN.nonempty
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
h : ∃ (M : T.ModelType), Infinite (↑M : Type (max u v))
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
⊢ ∃ (N : ModelType.{u, v, w} T), #(↑N : Type w) = κ
have intro : ∀ (M : T.ModelType) (MI : Infinite (↑M : Type (max u v))), ∃ (N : ModelType.{u, v, w} T), #(↑N : Type w) = κ
Tactic: cases h with
  | intro M MI =>
    obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
    haveI : Nonempty N := hN.nonempty
    exact ⟨hN.theory_model.bundled, rfl⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
⊢ T ⊨ᵇ φ ↔ ¬(T ∪ {Formula.not φ}).IsSatisfiable
have rw : (∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ) ↔ ¬Nonempty (T ∪ {Formula.not φ}).ModelType
Tactic: rw [models_sentence_iff, IsSatisfiable]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
⊢ (∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ) ↔ ¬Nonempty (T ∪ {Formula.not φ}).ModelType
have h1 : ∀ (h : ¬Nonempty (T ∪ {Formula.not φ}).ModelType) (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ
Tactic: refine
    ⟨fun h1 h2 =>
      (Sentence.realize_not _).1
        (realize_sentence_of_mem (T ∪ {Formula.not φ})
          (Set.subset_union_right (Set.mem_singleton _)))
        (h1 (h2.some.subtheoryModel Set.subset_union_left)),
      fun h M => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
h : ¬Nonempty (T ∪ {Formula.not φ}).ModelType
M : T.ModelType
⊢ (↑M : Type (max u v)) ⊨ φ
have contrapose : ∀ (h : ¬(↑M : Type (max u v)) ⊨ φ), Nonempty (T ∪ {Formula.not φ}).ModelType
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ¬(↑M : Type (max u v)) ⊨ φ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType
have h₁ : (↑M : Type (max u v)) ⊨ Formula.not φ
Tactic: rw [← Sentence.realize_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : (↑M : Type (max u v)) ⊨ Formula.not φ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType
have Carrier : ∀ (ψ : L.Sentence) (hψ : ψ ∈ T ∪ {Formula.not φ}) (h' : Membership.mem (γ := Set L.Sentence) {Formula.not φ} ψ),
  (↑M : Type (max u v)) ⊨ ψ
Tactic: refine
    ⟨{  Carrier := M
        is_model := ⟨fun ψ hψ => hψ.elim (realize_sentence_of_mem _) fun h' => ?_⟩ }⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
h : T ⊨ᵇ φ
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
⊢ M ⊨ φ
have rw : ∀ (h : ¬(T ∪ {Formula.not φ}).IsSatisfiable) (M : Type u_1) [inst : L.Structure M] [M ⊨ T] [Nonempty M], M ⊨ φ
Tactic: rw [models_iff_not_satisfiable] at h
Cleared hypotheses: h, M, inst, inst_1, inst_2
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
h : ¬(T ∪ {Formula.not φ}).IsSatisfiable
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
⊢ M ⊨ φ
have contrapose : ∀ (h : ¬M ⊨ φ), (T ∪ {Formula.not φ}).IsSatisfiable
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
h : ¬M ⊨ φ
⊢ M ⊨ T ∪ {Formula.not φ}
have simp : ¬M ⊨ φ ∧ ∀ a ∈ T, M ⊨ a
Tactic: simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp,
      Sentence.realize_not]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ ∀ a ∈ T, M ⊨ a
have rw : ¬M ⊨ φ ∧ M ⊨ T
Tactic: rw [← model_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
h : ¬M ⊨ φ
⊢ (T ∪ {Formula.not φ}).IsSatisfiable
have this : M ⊨ T ∪ {Formula.not φ}
Tactic: have : M ⊨ T ∪ {Formula.not φ} := by
    simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp,
      Sentence.realize_not]
    rw [← model_iff]
    exact ⟨h, inferInstance⟩