awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
⊢ M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s
have refine : M ⊨ L.distinctConstantsTheory s
Tactic: refine ((LHom.onTheory_model _ _).2 inferInstance).union ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
⊢ M ⊨ L.distinctConstantsTheory s
have rw : Set.InjOn.{w, w'} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s
Tactic: rw [model_distinctConstantsTheory]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
⊢ Set.InjOn.{w, w'} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s
have refine : ∀ (a : α) (as : a ∈ s) (b : α) (bs : b ∈ s)
  (ab : Eq.{w' + 1} (α := M) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) a) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) b)),
  a = b
Tactic: refine fun a as b bs ab => ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : Eq.{w' + 1} (α := M) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) a) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) b)
⊢ a = b
have rw : Subtype.mk (p := Membership.mem s) a as = Subtype.mk (p := Membership.mem s) b bs
Tactic: rw [← Subtype.coe_mk a as, ← Subtype.coe_mk b bs, ← Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
have this₁ : M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s
Tactic: have : M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s := by
    refine ((LHom.onTheory_model _ _).2 inferInstance).union ?_
    rw [model_distinctConstantsTheory]
    refine fun a as b bs ab => ?_
    rw [← Subtype.coe_mk a as, ← Subtype.coe_mk b bs, ← Subtype.ext_iff]
    exact
      h.some.injective
        ((Subtype.coe_injective.extend_apply h.some default ⟨a, as⟩).symm.trans
          (ab.trans (Subtype.coe_injective.extend_apply h.some default ⟨b, bs⟩)))
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
have rw : ∀ (i : Finset (↑s : Type w)),
  IsSatisfiable
    ((L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
Tactic: rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
rw :
  ∀ (i : Finset (↑s : Type w)),
    IsSatisfiable
      ((L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
have rw₁ : Directed (fun (x1 x2 : L[[α]].Theory) ↦ x1 ⊆ x2) fun (i : Finset (↑s : Type w)) ↦
  (L.lhomWithConstants α).onTheory T ∪
    L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
Tactic: rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
⊢ Directed (fun (x1 x2 : L[[α]].Theory) ↦ x1 ⊆ x2) fun (i : Finset (↑s : Type w)) ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
have a : Monotone (β := L[[α]].Theory) fun (i : Finset (↑s : Type w)) ↦
  (L.lhomWithConstants α).onTheory T ∪
    L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
Tactic: apply Monotone.directed_le
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
⊢ Monotone (β := L[[α]].Theory) fun (i : Finset (↑s : Type w)) ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
have a : Monotone (β := Set α) fun (i : Finset (↑s : Type w)) ↦
  (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
Tactic: refine monotone_const.union (monotone_distinctConstantsTheory.comp ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
⊢ Monotone (β := Set α) fun (i : Finset (↑s : Type w)) ↦
    (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
have a : Monotone (β := Set α) fun (i : Finset (↑s : Type w)) ↦
  (fun (a : { x : α // x ∈ s }) ↦ (↑a : α)) '' (↑i : Set { x : α // x ∈ s })
Tactic: simp only [Finset.coe_map, Function.Embedding.coe_subtype]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
have rw : ((L.lhomWithConstants α).onTheory T ∪
    ⋃ (t : Finset (↑s : Type w)),
      L.distinctConstantsTheory
        (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)).IsSatisfiable
Tactic: classical
    rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
    · exact fun t =>
        isSatisfiable_union_distinctConstantsTheory_of_card_le T _ M
          ((lift_le_aleph0.2 (finset_card_lt_aleph0 _).le).trans
            (aleph0_le_lift.2 (aleph0_le_mk M)))
    · apply Monotone.directed_le
      refine monotone_const.union (monotone_distinctConstantsTheory.comp ?_)
      simp only [Finset.coe_map, Function.Embedding.coe_subtype]
      exact Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s))
        Set.monotone_image fun _ _ => Finset.coe_subset.2
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
rw :
  ((L.lhomWithConstants α).onTheory T ∪
      ⋃ (t : Finset (↑s : Type w)),
        L.distinctConstantsTheory
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)).IsSatisfiable
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
have rw₁ : IsSatisfiable (L := L[[α]])
  (⋃ (i : Finset (↑s : Type w)),
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
Tactic: classical
    rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
    · exact fun t =>
        isSatisfiable_union_distinctConstantsTheory_of_card_le T _ M
          ((lift_le_aleph0.2 (finset_card_lt_aleph0 _).le).trans
            (aleph0_le_lift.2 (aleph0_le_mk M)))
    · apply Monotone.directed_le
      refine monotone_const.union (monotone_distinctConstantsTheory.comp ?_)
      simp only [Finset.coe_map, Function.Embedding.coe_subtype]
      exact Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s))
        Set.monotone_image fun _ _ => Finset.coe_subset.2
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
rw :
  ((L.lhomWithConstants α).onTheory T ∪
      ⋃ (t : Finset (↑s : Type w)),
        L.distinctConstantsTheory
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)).IsSatisfiable
rw₁ :
  IsSatisfiable (L := L[[α]])
    (⋃ (i : Finset (↑s : Type w)),
      (L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
have rw₂ : ∀ (i : Finset (↑s : Type w)),
  IsSatisfiable
    ((L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
Tactic: classical
    rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
    · exact fun t =>
        isSatisfiable_union_distinctConstantsTheory_of_card_le T _ M
          ((lift_le_aleph0.2 (finset_card_lt_aleph0 _).le).trans
            (aleph0_le_lift.2 (aleph0_le_mk M)))
    · apply Monotone.directed_le
      refine monotone_const.union (monotone_distinctConstantsTheory.comp ?_)
      simp only [Finset.coe_map, Function.Embedding.coe_subtype]
      exact Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s))
        Set.monotone_image fun _ _ => Finset.coe_subset.2
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
rw :
  ((L.lhomWithConstants α).onTheory T ∪
      ⋃ (t : Finset (↑s : Type w)),
        L.distinctConstantsTheory
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)).IsSatisfiable
rw₁ :
  IsSatisfiable (L := L[[α]])
    (⋃ (i : Finset (↑s : Type w)),
      (L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
rw₂ :
  ∀ (i : Finset (↑s : Type w)),
    IsSatisfiable
      ((L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
have rw₃ : Directed (fun (x1 x2 : L[[α]].Theory) ↦ x1 ⊆ x2) fun (i : Finset (↑s : Type w)) ↦
  (L.lhomWithConstants α).onTheory T ∪
    L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
Tactic: classical
    rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
    · exact fun t =>
        isSatisfiable_union_distinctConstantsTheory_of_card_le T _ M
          ((lift_le_aleph0.2 (finset_card_lt_aleph0 _).le).trans
            (aleph0_le_lift.2 (aleph0_le_mk M)))
    · apply Monotone.directed_le
      refine monotone_const.union (monotone_distinctConstantsTheory.comp ?_)
      simp only [Finset.coe_map, Function.Embedding.coe_subtype]
      exact Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s))
        Set.monotone_image fun _ _ => Finset.coe_subset.2
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
⊢ ∃ (N : T.ModelType), lift.{max u v w, w} κ ≤ #(↑N : Type (max (max u v) w))
have obtain : ∀
  (N :
    ModelType (L := withConstants.{u, v, w} L (Quotient.out κ))
      (LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T ∪ L.distinctConstantsTheory Set.univ)),
  ∃ (N : T.ModelType), lift.{max u v w, w} κ ≤ #(↑N : Type (max (max u v) w))
Tactic: obtain ⟨N⟩ :=
    isSatisfiable_union_distinctConstantsTheory_of_infinite T (Set.univ : Set κ.out) M
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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)
⊢ ∃ (N : T.ModelType), lift.{max u v w, w} κ ≤ #(↑N : Type (max (max u v) w))
have refine : lift.{max u v w, w} κ ≤
  #(↑(ModelType.reduct (T := T) (L.lhomWithConstants (Quotient.out κ))
          (sorry.bundled (T := LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T))) :
      Type (max (max u v) w))
Tactic: refine ⟨(N.is_model.mono Set.subset_union_left).bundled.reduct _, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
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)
⊢ lift.{max u v w, w} κ ≤
    #(↑(ModelType.reduct (T := T) (L.lhomWithConstants (Quotient.out κ))
            (⋯.bundled (T := LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T))) :
        Type (max (max u v) w))
have this : Model (L := withConstants.{u, v, w} L (Quotient.out κ)) (↑N : Type (max (max u v) w))
  (L.distinctConstantsTheory Set.univ)
Tactic: haveI : N ⊨ distinctConstantsTheory _ _ := N.is_model.mono Set.subset_union_right
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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} κ ≤
    #(↑(ModelType.reduct (T := T) (L.lhomWithConstants (Quotient.out κ))
            (⋯.bundled (T := LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T))) :
        Type (max (max u v) w))
have rw : lift.{max u v w, w} κ ≤ #(↑N : Type (max (max u v) w))
Tactic: rw [ModelType.reduct_Carrier, coe_of]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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))
have refine : lift.{max (max u v) w, w} #(Quotient.out κ) ≤ #(↑N : Type (max (max u v) w))
Tactic: refine _root_.trans (lift_le.2 (le_of_eq (Cardinal.mk_out κ).symm)) ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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} #(Quotient.out κ) ≤ #(↑N : Type (max (max u v) w))
have rw : lift.{max (max u v) w, w} #(↑Set.univ : Type w) ≤ #(↑N : Type (max (max u v) w))
Tactic: rw [← mk_univ]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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))
have 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))
Tactic: refine
    (card_le_of_model_distinctConstantsTheory L Set.univ N).trans (lift_le.{max u v w}.1 ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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, 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))
have 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))
Tactic: rw [lift_lift]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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)
have h : ∀ (h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)), IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)
Tactic: refine
      ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _),
        fun h => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)
⊢ IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)
have rw : IsFinitelySatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)
Tactic: rw [isSatisfiable_iff_isFinitelySatisfiable]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
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
⊢ IsSatisfiable (↑s : Set L.Sentence)
have hs₁ : (↑s : Set L.Sentence) ⊆ ⋃ (t : Finset ι), ⋃ i ∈ t, T i
Tactic: rw [Set.iUnion_eq_iUnion_finset] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ IsSatisfiable (↑s : Set L.Sentence)
have obtain : ∀ (t : Finset ι) (ht : (↑s : Set L.Sentence) ⊆ ⋃ i ∈ t, T i), 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
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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)
have h : ∀ (h : ∀ (s : Finset ι), IsSatisfiable.{u, v} (L := L) (⋃ i ∈ s, T i)), IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), 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
-- 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)
⊢ 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)),
  IsFinitelySatisfiable.{u, v} (L := L) (⋃ (i : ι), 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
-- 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)
⊢ 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) ⊆ ⋃ (i : ι), 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