-- Mathlib/ModelTheory/Satisfiability.lean
theorem exists_large_model_of_infinite_model (T : L.Theory) (κ : Cardinal.{w}) (M : Type w')
    [L.Structure M] [M ⊨ T] [Infinite M] :
    ∃ N : ModelType.{_, _, max u v w} T, Cardinal.lift.{max u v w} κ ≤ #N

Proof state:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max u v w, max (max u v) w} (lift.{w, max (max u v) w} #↑N) ≤ lift.{max u v w, max (max u v) w} #↑N

Tactic:
rw [lift_lift]

Result:
no goals

Proof state:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max (max u v) w, w} #(Quotient.out κ) ≤ #↑N

Tactic:
rw [← mk_univ]

Result:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max (max u v) w, w} #↑Set.univ ≤ #↑N

Proof state:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
⊢ ∃ N, lift.{max u v w, w} κ ≤ #↑N

Tactic:
refine ⟨(N.is_model.mono Set.subset_union_left).bundled.reduct _, ?_⟩

Result:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
⊢ lift.{max u v w, w} κ ≤ #↑(ModelType.reduct (L.lhomWithConstants (Quotient.out κ)) ⋯.bundled)

Proof state:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
⊢ lift.{max u v w, w} κ ≤ #↑(ModelType.reduct (L.lhomWithConstants (Quotient.out κ)) ⋯.bundled)

Tactic:
haveI : N ⊨ distinctConstantsTheory _ _ := N.is_model.mono Set.subset_union_right

Result:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max u v w, w} κ ≤ #↑(ModelType.reduct (L.lhomWithConstants (Quotient.out κ)) ⋯.bundled)

Proof state:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max (max u v) w, w} #↑Set.univ ≤ #↑N

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

Result:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max u v w, max (max u v) w} (lift.{w, max (max u v) w} #↑N) ≤ lift.{max u v w, max (max u v) w} #↑N

Proof state:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max u v w, w} κ ≤ #↑(ModelType.reduct (L.lhomWithConstants (Quotient.out κ)) ⋯.bundled)

Tactic:
rw [ModelType.reduct_Carrier, coe_of]

Result:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max u v w, w} κ ≤ #↑N

Proof state:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ∃ N, lift.{max u v w, w} κ ≤ #↑N

Tactic:
obtain ⟨N⟩ :=
  isSatisfiable_union_distinctConstantsTheory_of_infinite T (Set.univ : Set κ.out) M

Result:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
⊢ ∃ N, lift.{max u v w, w} κ ≤ #↑N

Proof state:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max u v w, w} κ ≤ #↑N

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

Result:
case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max (max u v) w, w} #(Quotient.out κ) ≤ #↑N