case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
⊢ ∃ N, lift κ ≤ (#↑N)
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ∃ N, lift κ ≤ (#↑N)
obtain ⟨N⟩ :=
  isSatisfiable_union_distinctConstantsTheory_of_infinite T (Set.univ : Set κ.out) M
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
⊢ lift κ ≤
    (#↑(ModelType.reduct (lhomWithConstants L (Quotient.out κ))
          (Model.bundled (_ : ↑N ⊨ LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T))))
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
⊢ ∃ N, lift κ ≤ (#↑N)
refine' ⟨(N.is_model.mono (Set.subset_union_left _ _)).bundled.reduct _, _⟩
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift κ ≤
    (#↑(ModelType.reduct (lhomWithConstants L (Quotient.out κ))
          (Model.bundled (_ : ↑N ⊨ LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T))))
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
⊢ lift κ ≤
    (#↑(ModelType.reduct (lhomWithConstants L (Quotient.out κ))
          (Model.bundled (_ : ↑N ⊨ LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T))))
haveI : N ⊨ distinctConstantsTheory _ _ := N.is_model.mono (Set.subset_union_right _ _)
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift κ ≤ (#↑N)
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift κ ≤
    (#↑(ModelType.reduct (lhomWithConstants L (Quotient.out κ))
          (Model.bundled (_ : ↑N ⊨ LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T))))
rw [ModelType.reduct_Carrier, coe_of]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift (#Quotient.out κ) ≤ (#↑N)
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift κ ≤ (#↑N)
refine' _root_.trans (lift_le.2 (le_of_eq (Cardinal.mk_out κ).symm)) _
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift (#↑Set.univ) ≤ (#↑N)
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift (#Quotient.out κ) ≤ (#↑N)
rw [← mk_univ]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift (lift (#↑N)) ≤ lift (#↑N)
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift (#↑Set.univ) ≤ (#↑N)
refine'
  (card_le_of_model_distinctConstantsTheory L Set.univ N).trans (lift_le.{_, max u v w}.1 _)
no goals
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift (lift (#↑N)) ≤ lift (#↑N)
rw [lift_lift]