awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : Cardinal.lift.{max w u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', w} κ
hY : Cardinal.lift.{max w u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, w} κ
mpr :
  Cardinal.lift.{max u' w, u} (Cardinal.mk X) + Cardinal.lift.{max u w, u'} (Cardinal.mk Y) <
    Cardinal.lift.{max u' u, w} κ
⊢ Cardinal.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ

Tactic:
simp only [Cardinal.mk_sum, Cardinal.lift_add, Cardinal.lift_lift]

Premises used: Cardinal.lift_lift, Cardinal.mk_sum, Cardinal.lift_add
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : Cardinal.lift.{max w u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', w} κ
hY : Cardinal.lift.{max w u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, w} κ
⊢ Cardinal.aleph0 ≤ Cardinal.lift.{max u' u, w} κ

Tactic:
simpa using hκ
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : Cardinal.lift.{max w u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', w} κ
hY : Cardinal.lift.{max w u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, w} κ
⊢ Cardinal.lift.{max u' w, u} (Cardinal.mk X) + Cardinal.lift.{max u w, u'} (Cardinal.mk Y) <
    Cardinal.lift.{max u' u, w} κ

Tactic:
exact Cardinal.add_lt_of_lt (by simpa using hκ) hX hY

Premises used: Cardinal.add_lt_of_lt
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
rw : HasCardinalLT X κ → HasCardinalLT PUnit.{1} κ
⊢ HasCardinalLT.{w, u} (Option X) κ ↔ HasCardinalLT X κ

Tactic:
rw [hasCardinalLT_iff_of_equiv (Equiv.optionEquivSumPUnit.{0} X),
    hasCardinalLT_sum_iff _ _ _ hκ, and_iff_left_iff_imp]

Premises used: hasCardinalLT_iff_of_equiv, Equiv.optionEquivSumPUnit, hasCardinalLT_sum_iff, and_iff_left_iff_imp
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X κ → HasCardinalLT PUnit.{1} κ

Tactic:
fun _ ↦ HasCardinalLT.of_le ?_ hκ

Premises used: HasCardinalLT.of_le
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
refine : HasCardinalLT X κ → HasCardinalLT PUnit.{1} Cardinal.aleph0
⊢ HasCardinalLT X κ → HasCardinalLT PUnit.{1} κ

Tactic:
refine fun _ ↦ HasCardinalLT.of_le ?_ hκ

Premises used: HasCardinalLT.of_le
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h : HasCardinalLT X κ
rw : Finite PUnit.{1}
⊢ HasCardinalLT PUnit.{1} Cardinal.aleph0

Tactic:
rw [hasCardinalLT_aleph0_iff]

Premises used: hasCardinalLT_aleph0_iff
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h : HasCardinalLT X κ
⊢ Finite PUnit.{1}

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
rw : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ ∧ HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
⊢ HasCardinalLT.{u_2, u_1} (Subtype P₁ ⊕ Subtype P₂) κ

Tactic:
rw [hasCardinalLT_sum_iff _ _ _ hκ]

Premises used: hasCardinalLT_sum_iff
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
⊢ HasCardinalLT.{u_2, u_1} (Subtype P₁) κ ∧ HasCardinalLT.{u_2, u_1} (Subtype P₂) κ

Tactic:
⟨h₁, h₂⟩

Premises used: And.intro
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
⊢ HasCardinalLT.{u_2, u_1} (Subtype P₁) κ ∧ HasCardinalLT.{u_2, u_1} (Subtype P₂) κ

Tactic:
exact ⟨h₁, h₂⟩
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
⊢ HasCardinalLT.{u_2, u_1} (Subtype P₁ ⊕ Subtype P₂) κ

Tactic:
have : HasCardinalLT (Subtype P₁ ⊕ Subtype P₂) κ := by
    rw [hasCardinalLT_sum_iff _ _ _ hκ]
    exact ⟨h₁, h₂⟩
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
this : HasCardinalLT.{u_2, u_1} (Subtype P₁ ⊕ Subtype P₂) κ
⊢ HasCardinalLT.{u_2, u_1} (Subtype (P₁ ⊔ P₂)) κ

Tactic:
this.of_surjective (Sum.elim (fun x ↦ ⟨x.1, Or.inl x.2⟩)
    (fun x ↦ ⟨x.1, Or.inr x.2⟩)) ?_

Premises used: HasCardinalLT.of_surjective, Subtype.mk, Or.inl, Subtype.val, Or.inr, Subtype.property, Sum.elim
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
this : HasCardinalLT.{u_2, u_1} (Subtype P₁ ⊕ Subtype P₂) κ
refine :
  Function.Surjective.{u_1 + 1, u_1 + 1} (α := Subtype P₁ ⊕ Subtype P₂) (β := Subtype (P₁ ⊔ P₂))
    (Sum.elim (fun (x : Subtype P₁) ↦ Subtype.mk (p := P₁ ⊔ P₂) (↑x : X) ⋯) fun (x : Subtype P₂) ↦
      Subtype.mk (p := P₁ ⊔ P₂) (↑x : X) ⋯)
⊢ HasCardinalLT.{u_2, u_1} (Subtype (P₁ ⊔ P₂)) κ

Tactic:
refine this.of_surjective (Sum.elim (fun x ↦ ⟨x.1, Or.inl x.2⟩)
    (fun x ↦ ⟨x.1, Or.inr x.2⟩)) ?_

Premises used: HasCardinalLT.of_surjective, Sum.elim
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
this : HasCardinalLT.{u_2, u_1} (Subtype P₁ ⊕ Subtype P₂) κ
x : X
hx : P₁ x
⊢ ∃ (a : Subtype P₁ ⊕ Subtype P₂),
    Eq (α := Subtype (P₁ ⊔ P₂))
      (Sum.elim (fun (x : Subtype P₁) ↦ Subtype.mk (p := P₁ ⊔ P₂) (↑x : X) ⋯)
        (fun (x : Subtype P₂) ↦ Subtype.mk (p := P₁ ⊔ P₂) (↑x : X) ⋯) a)
      (Subtype.mk (p := P₁ ⊔ P₂) x ⋯)

Tactic:
⟨Sum.inl ⟨x, hx⟩, rfl⟩

Premises used: Sum.inl, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
this : HasCardinalLT.{u_2, u_1} (Subtype P₁ ⊕ Subtype P₂) κ
x : X
hx : P₁ x
⊢ ∃ (a : Subtype P₁ ⊕ Subtype P₂),
    Eq (α := Subtype (P₁ ⊔ P₂))
      (Sum.elim (fun (x : Subtype P₁) ↦ Subtype.mk (p := P₁ ⊔ P₂) (↑x : X) ⋯)
        (fun (x : Subtype P₂) ↦ Subtype.mk (p := P₁ ⊔ P₂) (↑x : X) ⋯) a)
      (Subtype.mk (p := P₁ ⊔ P₂) x ⋯)

Tactic:
exact ⟨Sum.inl ⟨x, hx⟩, rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
this : HasCardinalLT.{u_2, u_1} (Subtype P₁ ⊕ Subtype P₂) κ
x : X
hx : P₂ x
⊢ ∃ (a : Subtype P₁ ⊕ Subtype P₂),
    Eq (α := Subtype (P₁ ⊔ P₂))
      (Sum.elim (fun (x : Subtype P₁) ↦ Subtype.mk (p := P₁ ⊔ P₂) (↑x : X) ⋯)
        (fun (x : Subtype P₂) ↦ Subtype.mk (p := P₁ ⊔ P₂) (↑x : X) ⋯) a)
      (Subtype.mk (p := P₁ ⊔ P₂) x ⋯)

Tactic:
⟨Sum.inr ⟨x, hx⟩, rfl⟩

Premises used: Subtype.mk, Sum.inr, Exists.intro, rfl
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (Subtype P₁) κ
h₂ : HasCardinalLT.{u_2, u_1} (Subtype P₂) κ
this : HasCardinalLT.{u_2, u_1} (Subtype P₁ ⊕ Subtype P₂) κ
x : X
hx : P₂ x
⊢ ∃ (a : Subtype P₁ ⊕ Subtype P₂),
    Eq (α := Subtype (P₁ ⊔ P₂))
      (Sum.elim (fun (x : Subtype P₁) ↦ Subtype.mk (p := P₁ ⊔ P₂) (↑x : X) ⋯)
        (fun (x : Subtype P₂) ↦ Subtype.mk (p := P₁ ⊔ P₂) (↑x : X) ⋯) a)
      (Subtype.mk (p := P₁ ⊔ P₂) x ⋯)

Tactic:
exact ⟨Sum.inr ⟨x, hx⟩, rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u_1
S₁ S₂ : Set X
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT.{u_2, u_1} (↑S₁ : Type u_1) κ
h₂ : HasCardinalLT.{u_2, u_1} (↑S₂ : Type u_1) κ
⊢ HasCardinalLT.{u_2, u_1} (↑(S₁ ∪ S₂) : Type u_1) κ

Tactic:
hasCardinalLT_subtype_max hκ h₁ h₂

Premises used: Set.union, Set.Mem, hasCardinalLT_subtype_max, setOf
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type w
α : ι → Type w
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT (α i) κ
simp : ∀ (hι : Cardinal.mk ι < κ) (hα : ∀ (i : ι), Cardinal.mk (α i) < κ), Cardinal.mk ((i : ι) × α i) < κ
⊢ HasCardinalLT ((i : ι) × α i) κ

Tactic:
simp only [hasCardinalLT_iff_cardinal_mk_lt] at hι hα ⊢

Premises used: hasCardinalLT_iff_cardinal_mk_lt
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type w
α : ι → Type w
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : Cardinal.mk ι < κ
hα : ∀ (i : ι), Cardinal.mk (α i) < κ
rw : (Cardinal.sum fun (i : ι) ↦ Cardinal.mk (α i)) < κ
⊢ Cardinal.mk ((i : ι) × α i) < κ

Tactic:
rw [Cardinal.mk_sigma]

Premises used: Cardinal.mk_sigma
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type w
α : ι → Type w
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : Cardinal.mk ι < κ
hα : ∀ (i : ι), Cardinal.mk (α i) < κ
⊢ Cardinal.lift.{w, w} (Cardinal.mk ι) < κ

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type w
α : ι → Type w
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : Cardinal.mk ι < κ
hα : ∀ (i : ι), Cardinal.mk (α i) < κ
⊢ (Cardinal.sum fun (i : ι) ↦ Cardinal.mk (α i)) < κ

Tactic:
exact Cardinal.sum_lt_lift_of_isRegular.{w, w} Fact.out (by simpa) hα
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT.{w, v} (α i) κ
⊢ Fact (Cardinal.lift.{max u v, w} κ).IsRegular

Tactic:
have : Fact (Cardinal.lift.{max u v} κ).IsRegular := ⟨Cardinal.IsRegular.lift Fact.out⟩
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT.{w, v} (α i) κ
this : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
⊢ HasCardinalLT (ULift.{max v w, u} ι) (Cardinal.lift.{max u v, w} κ)

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT.{w, v} (α i) κ
this : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
i : ULift.{max v w, u} ι
⊢ HasCardinalLT ((fun (i : ULift.{max v w, u} ι) ↦ ULift.{max u w, v} (α i.down)) i) (Cardinal.lift.{max u v, w} κ)

Tactic:
simpa using hα (ULift.down i)

Premises used: ULift.down
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT.{w, v} (α i) κ
this : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
⊢ HasCardinalLT ((i : ULift.{max v w, u} ι) × (fun (i : ULift.{max v w, u} ι) ↦ ULift.{max u w, v} (α i.down)) i)
    (Cardinal.lift.{max u v, w} κ)

Tactic:
have := hasCardinalLT_sigma'
    (fun (i : ULift.{max v w} ι) ↦ ULift.{max u w} (α (ULift.down i)))
    (Cardinal.lift.{max u v} κ) (by simpa)
    (fun i ↦ by simpa using hα (ULift.down i))
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT.{w, v} (α i) κ
this_1 : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
this :
  HasCardinalLT ((i : ULift.{max v w, u} ι) × (fun (i : ULift.{max v w, u} ι) ↦ ULift.{max u w, v} (α i.down)) i)
    (Cardinal.lift.{max u v, w} κ)
⊢ HasCardinalLT ((i : ULift.{max v w, u} ι) × (fun (i : ULift.{max v w, u} ι) ↦ ULift.{max u w, v} (α i.down)) i) κ

Tactic:
rw [hasCardinalLT_lift_iff] at this

Premises used: hasCardinalLT_lift_iff
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT.{w, v} (α i) κ
this_1 : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
this : HasCardinalLT ((i : ULift.{max v w, u} ι) × (fun (i : ULift.{max v w, u} ι) ↦ ULift.{max u w, v} (α i.down)) i) κ
⊢ HasCardinalLT ((i : ι) × α i) κ

Tactic:
this.of_surjective (fun ⟨i, a⟩ ↦ ⟨ULift.down i, ULift.down a⟩)
    (fun ⟨i, a⟩ ↦ ⟨⟨ULift.up i, ULift.up a⟩, rfl⟩)

Premises used: _private.0.hasCardinalLT_sigma.match_1, Exists, HasCardinalLT.of_surjective, Exists.intro, Sigma.mk, ULift.up, Eq, ULift.down, Sigma, _private.0.hasCardinalLT_sigma.match_2, rfl
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT.{w, v} (α i) κ
this_1 : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
this : HasCardinalLT ((i : ULift.{max v w, u} ι) × (fun (i : ULift.{max v w, u} ι) ↦ ULift.{max u w, v} (α i.down)) i) κ
⊢ HasCardinalLT ((i : ι) × α i) κ

Tactic:
exact this.of_surjective (fun ⟨i, a⟩ ↦ ⟨ULift.down i, ULift.down a⟩)
    (fun ⟨i, a⟩ ↦ ⟨⟨ULift.up i, ULift.up a⟩, rfl⟩)

Premises used: HasCardinalLT.of_surjective
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (Subtype (P i)) κ
x_1 : (i : ι) × Subtype (P i)
i : ι
x : X
hx : P i x
simp : ∃ (i : ι), P i x
⊢ (⨆ (i : ι), P i) x

Tactic:
simp only [iSup_apply, iSup_Prop_eq]

Premises used: iSup_Prop_eq, iSup_apply
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (Subtype (P i)) κ
x_1 : (i : ι) × Subtype (P i)
i : ι
x : X
hx : P i x
⊢ ∃ (i : ι), P i x

Tactic:
⟨i, hx⟩

Premises used: Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (Subtype (P i)) κ
x_1 : (i : ι) × Subtype (P i)
i : ι
x : X
hx : P i x
⊢ ∃ (i : ι), P i x

Tactic:
exact ⟨i, hx⟩
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (Subtype (P i)) κ
val : X
h : (⨆ (i : ι), P i) val
⊢ ∃ (i : ι), P i val

Tactic:
simp only [iSup_apply, iSup_Prop_eq] at h

Premises used: iSup_Prop_eq, iSup_apply
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (Subtype (P i)) κ
val : X
h_1 : (⨆ (i : ι), P i) val
h : ∃ (i : ι), P i val
obtain :
  ∀ (i : ι) (hi : P i val),
    ∃ (a : (i : ι) × Subtype (P i)),
      (fun (x : (i : ι) × Subtype (P i)) ↦
            (match (motive := (i : ι) × Subtype (P i) → Subtype (α := X) (⨆ (i : ι), P i)) x with
              | ⟨i, ⟨x, hx⟩⟩ => Subtype.mk (p := ⨆ (i : ι), P i) x ⋯ :
              Subtype (α := X) (⨆ (i : ι), P i)))
          a =
        Subtype.mk (p := ⨆ (i : ι), P i) val h_1
⊢ ∃ (a : (i : ι) × Subtype (P i)),
    (fun (x : (i : ι) × Subtype (P i)) ↦
          (match (motive := (i : ι) × Subtype (P i) → Subtype (α := X) (⨆ (i : ι), P i)) x with
            | ⟨i, ⟨x, hx⟩⟩ => Subtype.mk (p := ⨆ (i : ι), P i) x ⋯ :
            Subtype (α := X) (⨆ (i : ι), P i)))
        a =
      Subtype.mk (p := ⨆ (i : ι), P i) val h_1

Tactic:
obtain ⟨i, hi⟩ := h
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (Subtype (P i)) κ
val : X
h : (⨆ (i : ι), P i) val
i : ι
hi : P i val
⊢ ∃ (a : (i : ι) × Subtype (P i)),
    (fun (x : (i : ι) × Subtype (P i)) ↦
          (match (motive := (i : ι) × Subtype (P i) → Subtype (α := X) (⨆ (i : ι), P i)) x with
            | ⟨i, ⟨x, hx⟩⟩ => Subtype.mk (p := ⨆ (i : ι), P i) x ⋯ :
            Subtype (α := X) (⨆ (i : ι), P i)))
        a =
      Subtype.mk (p := ⨆ (i : ι), P i) val h

Tactic:
⟨⟨i, _, hi⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, Sigma.mk, rfl
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (Subtype (P i)) κ
val : X
h : (⨆ (i : ι), P i) val
i : ι
hi : P i val
⊢ ∃ (a : (i : ι) × Subtype (P i)),
    (fun (x : (i : ι) × Subtype (P i)) ↦
          (match (motive := (i : ι) × Subtype (P i) → Subtype (α := X) (⨆ (i : ι), P i)) x with
            | ⟨i, ⟨x, hx⟩⟩ => Subtype.mk (p := ⨆ (i : ι), P i) x ⋯ :
            Subtype (α := X) (⨆ (i : ι), P i)))
        a =
      Subtype.mk (p := ⨆ (i : ι), P i) val h

Tactic:
exact ⟨⟨i, _, hi⟩, rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u_1
X : Type u_2
S : ι → Set X
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hS : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (↑(S i) : Type u_2) κ
⊢ HasCardinalLT.{u_3, u_2} (↑(setOf (⨆ (i : ι), S i)) : Type u_2) κ

Tactic:
show HasCardinalLT (setOf ((⨆ i, S i))) κ from hasCardinalLT_subtype_iSup S hι hS

Premises used: hasCardinalLT_subtype_iSup
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u_1
X : Type u_2
S : ι → Set X
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hS : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (↑(S i) : Type u_2) κ
h : Eq.{u_2 + 1} (α := Set X) (⋃ (i : ι), S i) (setOf (⨆ (i : ι), S i))
⊢ HasCardinalLT.{u_3, u_2} (↑(⋃ (i : ι), S i) : Type u_2) κ

Tactic:
convert! show HasCardinalLT (setOf ((⨆ i, S i))) κ from hasCardinalLT_subtype_iSup S hι hS

Premises used: hasCardinalLT_subtype_iSup
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type u_1
X : Type u_2
S : ι → Set X
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hS : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (↑(S i) : Type u_2) κ
⊢ Eq.{u_2 + 1} (α := Set X) (⋃ (i : ι), S i) (setOf (⨆ (i : ι), S i))

Tactic:
aesop
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
T₁ T₂ : Type w
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
rw : ∀ (h₁ : Cardinal.mk T₁ < κ) (h₂ : Cardinal.mk T₂ < κ), Cardinal.mk (T₁ × T₂) < κ
⊢ HasCardinalLT (T₁ × T₂) κ

Tactic:
rw [hasCardinalLT_iff_cardinal_mk_lt] at h₁ h₂ ⊢

Premises used: hasCardinalLT_iff_cardinal_mk_lt
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
T₁ T₂ : Type w
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : Cardinal.mk T₁ < κ
h₂ : Cardinal.mk T₂ < κ
⊢ Cardinal.mk (T₁ × T₂) < κ

Tactic:
simpa using Cardinal.mul_lt_of_lt hκ h₁ h₂

Premises used: Cardinal.mul_lt_of_lt
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ Cardinal.aleph0 ≤ Cardinal.lift.{max u u', w} κ

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ HasCardinalLT (ULift.{max u' w, u} T₁) (Cardinal.lift.{max u u', w} κ)

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ HasCardinalLT (ULift.{max u w, u'} T₂) (Cardinal.lift.{max u u', w} κ)

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ HasCardinalLT (ULift.{max u' w, u} T₁ × ULift.{max u w, u'} T₂) (Cardinal.lift.{max u u', w} κ)

Tactic:
have := hasCardinalLT_prod' (T₁ := ULift.{max u' w} T₁) (T₂ := ULift.{max u w} T₂)
    (κ := Cardinal.lift.{max u u'} κ) (by simpa) (by simpa) (by simpa)
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
this : HasCardinalLT (ULift.{max u' w, u} T₁ × ULift.{max u w, u'} T₂) (Cardinal.lift.{max u u', w} κ)
⊢ HasCardinalLT (ULift.{max u' w, u} T₁ × ULift.{max u w, u'} T₂) κ

Tactic:
simp only [hasCardinalLT_lift_iff] at this

Premises used: hasCardinalLT_lift_iff
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
this : HasCardinalLT (ULift.{max u' w, u} T₁ × ULift.{max u w, u'} T₂) κ
⊢ HasCardinalLT (T₁ × T₂) κ

Tactic:
this.of_surjective (fun ⟨x₁, x₂⟩ ↦ ⟨ULift.down x₁, ULift.down x₂⟩) (fun ⟨x₁, x₂⟩ ↦
    ⟨⟨ULift.up x₁, ULift.up x₂⟩, rfl⟩)

Premises used: Exists, Prod.mk, _private.0.hasCardinalLT_prod.match_2, HasCardinalLT.of_surjective, _private.0.hasCardinalLT_prod.match_1, Exists.intro, Prod, ULift.up, Eq, ULift.down, rfl
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
this : HasCardinalLT (ULift.{max u' w, u} T₁ × ULift.{max u w, u'} T₂) κ
⊢ HasCardinalLT (T₁ × T₂) κ

Tactic:
exact this.of_surjective (fun ⟨x₁, x₂⟩ ↦ ⟨ULift.down x₁, ULift.down x₂⟩) (fun ⟨x₁, x₂⟩ ↦
    ⟨⟨ULift.up x₁, ULift.up x₂⟩, rfl⟩)

Premises used: HasCardinalLT.of_surjective
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
X : Type u
inst : Small.{w, u} X
⊢ HasCardinalLT.{w, u} X (Order.succ (max (Cardinal.mk (Shrink.{w, u} X)) Cardinal.aleph0))

Tactic:
simp [hasCardinalLT_iff_of_equiv (equivShrink.{w} X),
        hasCardinalLT_iff_cardinal_mk_lt]

Premises used: hasCardinalLT_iff_cardinal_mk_lt
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type v
X : ι → Type u
inst : Small.{w, v} ι
inst_1 : ∀ (i : ι), Small.{w, u} (X i)
obtain :
  ∀ (κ : Cardinal.{w}) (hκ : κ.IsRegular) (h : HasCardinalLT (Sigma X) κ),
    ∃ (κ : Cardinal.{w}), κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT.{w, u} (X i) κ
⊢ ∃ (κ : Cardinal.{w}), κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT.{w, u} (X i) κ

Tactic:
obtain ⟨κ, hκ, h⟩ := exists_regular_cardinal.{w} (Sigma X)
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type v
X : ι → Type u
inst : Small.{w, v} ι
inst_1 : ∀ (i : ι), Small.{w, u} (X i)
κ : Cardinal.{w}
hκ : κ.IsRegular
h : HasCardinalLT (Sigma X) κ
⊢ ∃ (κ : Cardinal.{w}), κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT.{w, u} (X i) κ

Tactic:
⟨κ, hκ, fun i ↦ h.of_injective _ sigma_mk_injective⟩

Premises used: HasCardinalLT.of_injective, And.intro, Exists.intro, Sigma.mk, sigma_mk_injective
-- Module: Mathlib.SetTheory.Cardinal.HasCardinalLT
Goal:
ι : Type v
X : ι → Type u
inst : Small.{w, v} ι
inst_1 : ∀ (i : ι), Small.{w, u} (X i)
κ : Cardinal.{w}
hκ : κ.IsRegular
h : HasCardinalLT (Sigma X) κ
⊢ ∃ (κ : Cardinal.{w}), κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT.{w, u} (X i) κ

Tactic:
exact ⟨κ, hκ, fun i ↦ h.of_injective _ sigma_mk_injective⟩
-- Module: Mathlib.SetTheory.Cardinal.NatCount
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
rw : Cardinal.mk { k : ℕ // k < n ∧ p k } ≤ Cardinal.mk (↑{k : ℕ | p k} : Type)
⊢ (↑(count p n) : Cardinal.{0}) ≤ Cardinal.mk (↑{k : ℕ | p k} : Type)

Tactic:
rw [count_eq_card_fintype, ← Cardinal.mk_fintype]

Premises used: Nat.count_eq_card_fintype, Cardinal.mk_fintype
-- Module: Mathlib.SetTheory.Cardinal.NatCount
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ Cardinal.mk { k : ℕ // k < n ∧ p k } ≤ Cardinal.mk (↑{k : ℕ | p k} : Type)

Tactic:
Cardinal.mk_subtype_mono fun x hx ↦ hx.2

Premises used: Cardinal.mk_subtype_mono, And.right