awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
N :
  ModelType (L := withConstants.{u, v, w} L (Quotient.out κ))
    (LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T ∪ L.distinctConstantsTheory Set.univ)
this :
  Model (L := withConstants.{u, v, w} L (Quotient.out κ)) (↑N : Type (max (max u v) w))
    (L.distinctConstantsTheory Set.univ)
⊢ lift.{max u v w, w} κ ≤ #(↑N : Type (max (max u v) w))

Tactic:
_root_.trans (lift_le.2 (le_of_eq (Cardinal.mk_out κ).symm)) ?_

Premises used: Iff.mpr, trans, Cardinal.mk_out, le_of_eq, Eq.symm, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
N :
  ModelType (L := withConstants.{u, v, w} L (Quotient.out κ))
    (LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T ∪ L.distinctConstantsTheory Set.univ)
this :
  Model (L := withConstants.{u, v, w} L (Quotient.out κ)) (↑N : Type (max (max u v) w))
    (L.distinctConstantsTheory Set.univ)
refine : lift.{max (max u v) w, w} #(Quotient.out κ) ≤ #(↑N : Type (max (max u v) w))
⊢ lift.{max u v w, w} κ ≤ #(↑N : Type (max (max u v) w))

Tactic:
refine _root_.trans (lift_le.2 (le_of_eq (Cardinal.mk_out κ).symm)) ?_

Premises used: Iff.mpr, trans, Cardinal.mk_out, le_of_eq, Eq.symm, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
N :
  ModelType (L := withConstants.{u, v, w} L (Quotient.out κ))
    (LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T ∪ L.distinctConstantsTheory Set.univ)
this :
  Model (L := withConstants.{u, v, w} L (Quotient.out κ)) (↑N : Type (max (max u v) w))
    (L.distinctConstantsTheory Set.univ)
rw : lift.{max (max u v) w, w} #(↑Set.univ : Type w) ≤ #(↑N : Type (max (max u v) w))
⊢ lift.{max (max u v) w, w} #(Quotient.out κ) ≤ #(↑N : Type (max (max u v) w))

Tactic:
rw [← mk_univ]

Premises used: Cardinal.mk_univ
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
N :
  ModelType (L := withConstants.{u, v, w} L (Quotient.out κ))
    (LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T ∪ L.distinctConstantsTheory Set.univ)
this :
  Model (L := withConstants.{u, v, w} L (Quotient.out κ)) (↑N : Type (max (max u v) w))
    (L.distinctConstantsTheory Set.univ)
⊢ lift.{max (max u v) w, w} #(↑Set.univ : Type w) ≤ #(↑N : Type (max (max u v) w))

Tactic:
(card_le_of_model_distinctConstantsTheory L Set.univ N).trans (lift_le.{max u v w}.1 ?_)

Premises used: Set.univ, FirstOrder.Language.Theory.ModelType.Carrier, Iff.mp, LE.le.trans, FirstOrder.Language.card_le_of_model_distinctConstantsTheory, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
N :
  ModelType (L := withConstants.{u, v, w} L (Quotient.out κ))
    (LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T ∪ L.distinctConstantsTheory Set.univ)
this :
  Model (L := withConstants.{u, v, w} L (Quotient.out κ)) (↑N : Type (max (max u v) w))
    (L.distinctConstantsTheory Set.univ)
L₁ :
  lift.{max u v w, max (max u v) w} (lift.{w, max (max u v) w} #(↑N : Type (max (max u v) w))) ≤
    lift.{max u v w, max (max u v) w} #(↑N : Type (max (max u v) w))
⊢ lift.{max (max u v) w, w} #(↑Set.univ : Type w) ≤ #(↑N : Type (max (max u v) w))

Tactic:
refine
    (card_le_of_model_distinctConstantsTheory L Set.univ N).trans (lift_le.{max u v w}.1 ?_)
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
N :
  ModelType (L := withConstants.{u, v, w} L (Quotient.out κ))
    (LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T ∪ L.distinctConstantsTheory Set.univ)
this :
  Model (L := withConstants.{u, v, w} L (Quotient.out κ)) (↑N : Type (max (max u v) w))
    (L.distinctConstantsTheory Set.univ)
rw rw₁ :
  lift.{max (max u v) w, max (max u v) w} #(↑N : Type (max (max u v) w)) ≤
    lift.{max (max u v) w, max (max u v) w} #(↑N : Type (max (max u v) w))
⊢ lift.{max u v w, max (max u v) w} (lift.{w, max (max u v) w} #(↑N : Type (max (max u v) w))) ≤
    lift.{max u v w, max (max u v) w} #(↑N : Type (max (max u v) w))

Tactic:
rw [lift_lift]

Premises used: Cardinal.lift_lift
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
T : ι → L.Theory
⊢ IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i) ↔ ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)

Tactic:
⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _),
        fun h => ?_⟩

Premises used: Iff.mpr, Set.iUnion_subset_iff, FirstOrder.Language.Theory.IsSatisfiable.mono, Iff.intro, Set.iUnion_mono, refl
-- Module: Mathlib.ModelTheory.Satisfiability
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)
⊢ IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i) ↔ ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)

Tactic:
refine
      ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _),
        fun h => ?_⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)
rw : IsFinitelySatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)
⊢ IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)

Tactic:
rw [isSatisfiable_iff_isFinitelySatisfiable]

Premises used: FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : (↑s : Set L.Sentence) ⊆ ⋃ (i : ι), T i
⊢ (↑s : Set L.Sentence) ⊆ ⋃ (t : Finset ι), ⋃ i ∈ t, T i

Tactic:
rw [Set.iUnion_eq_iUnion_finset] at hs

Premises used: Set.iUnion_eq_iUnion_finset
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
T : ι → L.Theory
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
⊢ Directed (fun (x1 x2 : Set L.Sentence) ↦ x1 ⊆ x2) fun (i : Finset ι) ↦ ⋃ i_1 ∈ i, T i_1

Tactic:
Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
        Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩

Premises used: Set.iUnion_mono', Exists.intro, Set.iUnion_mono, Monotone.directed_le, refl
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
T : ι → L.Theory
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
⊢ Directed (fun (x1 x2 : Set L.Sentence) ↦ x1 ⊆ x2) fun (i : Finset ι) ↦ ⋃ i_1 ∈ i, T i_1

Tactic:
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 _⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
T : ι → L.Theory
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
obtain : ∀ (t : Finset ι) (ht : (↑s : Set L.Sentence) ⊆ ⋃ i ∈ t, T i), IsSatisfiable (↑s : Set L.Sentence)
⊢ IsSatisfiable (↑s : Set L.Sentence)

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

Premises used: Directed.exists_mem_subset_of_finset_subset_biUnion
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
T : ι → L.Theory
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:
(h t).mono ht

Premises used: FirstOrder.Language.Theory.IsSatisfiable.mono
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
T : ι → L.Theory
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:
exact (h t).mono ht

Premises used: FirstOrder.Language.Theory.IsSatisfiable.mono
-- Module: Mathlib.ModelTheory.Satisfiability
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)
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)
⊢ IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i) ↔ ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)

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

Premises used: FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable, Set.iUnion_eq_iUnion_finset
-- Module: Mathlib.ModelTheory.Satisfiability
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
⊢ lift.{w, w'} #(↑∅ : Type w') ≤ lift.{w', w} κ

Tactic:
simp
-- Module: Mathlib.ModelTheory.Satisfiability
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
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) = κ
⊢ ∃ (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

Premises used: EmptyCollection.emptyCollection, FirstOrder.Language.exists_elementarySubstructure_card_eq
-- Module: Mathlib.ModelTheory.Satisfiability
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} κ
⊢ lift.{w + 1, w'} #↥S = lift.{max w' (w + 1), w} κ

Tactic:
rw [← lift_inj.{_, w + 1}, lift_lift, lift_lift] at hS

Premises used: Cardinal.lift_lift
-- Module: Mathlib.ModelTheory.Satisfiability
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 + 1, w'} #↥S = lift.{max w' (w + 1), w} κ
⊢ Small.{w, w'} ↥S

Tactic:
small_iff_lift_mk_lt_univ.2 (lt_of_eq_of_lt hS κ.lift_lt_univ')

Premises used: Iff.mpr, Cardinal.lift_lt_univ', lt_of_eq_of_lt, Cardinal.small_iff_lift_mk_lt_univ
-- Module: Mathlib.ModelTheory.Satisfiability
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 + 1, w'} #↥S = lift.{max w' (w + 1), w} κ
⊢ Small.{w, w'} ↥S

Tactic:
exact small_iff_lift_mk_lt_univ.2 (lt_of_eq_of_lt hS κ.lift_lt_univ')

Premises used: Iff.mpr, Cardinal.lift_lt_univ', lt_of_eq_of_lt, Cardinal.small_iff_lift_mk_lt_univ
-- Module: Mathlib.ModelTheory.Satisfiability
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

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')
-- Module: Mathlib.ModelTheory.Satisfiability
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) = κ

Tactic:
⟨(equivShrink S).bundledInduced L,
      ⟨S.subtype.comp (Equiv.bundledInducedEquiv L _).symm.toElementaryEmbedding⟩,
      lift_inj.1 (_root_.trans ?_ hS)⟩

Premises used: FirstOrder.Language.ElementarySubstructure.subtype, trans, Membership.mem, FirstOrder.Language.ElementaryEmbedding.comp, Subtype, Nonempty.intro, Equiv.bundledInducedEquiv, Cardinal.lift_inj, Equiv.bundledInduced, And.intro, Exists.intro, Iff.mp, FirstOrder.Language.Equiv.toElementaryEmbedding, equivShrink, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Satisfiability
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
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
⊢ ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∧ #(↑N : Type w) = κ

Tactic:
refine
    ⟨(equivShrink S).bundledInduced L,
      ⟨S.subtype.comp (Equiv.bundledInducedEquiv L _).symm.toElementaryEmbedding⟩,
      lift_inj.1 (_root_.trans ?_ hS)⟩
-- Module: Mathlib.ModelTheory.Satisfiability
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
⊢ 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:
simp only [Equiv.bundledInduced_α, lift_mk_shrink']

Premises used: Equiv.bundledInduced_α, Cardinal.lift_mk_shrink'
-- Module: Mathlib.ModelTheory.Satisfiability
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} κ
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) = κ
⊢ ∃ (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

Premises used: FirstOrder.Language.elementaryDiagram, FirstOrder.Language.Theory.exists_large_model_of_infinite_model
-- Module: Mathlib.ModelTheory.Satisfiability
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))
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) = κ
⊢ ∃ (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

Premises used: Cardinal.lift_lift
-- Module: Mathlib.ModelTheory.Satisfiability
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))
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} κ
⊢ lift.{w, max (max w' u) v} L[[M]].card ≤ lift.{max (max w' u) v, w} κ

Tactic:
simp only [card_withConstants, lift_add, lift_lift]

Premises used: Cardinal.lift_lift, FirstOrder.Language.card_withConstants, Cardinal.lift_add
-- Module: Mathlib.ModelTheory.Satisfiability
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 :
  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} κ
⊢ 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:
rw [add_comm, add_eq_max (aleph0_le_lift.2 (infinite_iff.1 iM)), max_le_iff]

Premises used: Iff.mpr, Cardinal.infinite_iff, max_le_iff, add_comm, Cardinal.aleph0_le_lift, Cardinal.add_eq_max, Iff.mp
-- Module: Mathlib.ModelTheory.Satisfiability
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 :
  ∀ (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} κ
⊢ 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

Premises used: Cardinal.lift_lift
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
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:
⟨h2, h1⟩

Premises used: And.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
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:
exact ⟨h2, h1⟩
-- Module: Mathlib.ModelTheory.Satisfiability
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'))
rw₁ rw₂ : #(↑N0 : Type (max (max (max u w') v) 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'))

Tactic:
rw [← lift_umax, lift_id]

Premises used: Cardinal.lift_umax, Cardinal.lift_id
-- Module: Mathlib.ModelTheory.Satisfiability
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))
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) = κ
⊢ ∃ (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]))

Premises used: Iff.mpr, FirstOrder.Language.withConstants, Cardinal.aleph0_le_lift, FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_le, FirstOrder.Language.Theory.ModelType.Carrier, Iff.mp, LE.le.trans, Cardinal.aleph0_le_mk
-- Module: Mathlib.ModelTheory.Satisfiability
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 : Type w) ⊨ L.elementaryDiagram M

Tactic:
haveI h : N ⊨ L.elementaryDiagram M :=
    (NN0.theory_model_iff (L.elementaryDiagram M)).2 inferInstance