-- Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
lemma hasCardinalLT_sum_iff (X : Type u) (Y : Type u') (κ : Cardinal.{w})
    (hκ : Cardinal.aleph0 ≤ κ) :
    HasCardinalLT (X ⊕ Y) κ ↔ HasCardinalLT X κ ∧ HasCardinalLT Y κ

Proof state:
case mpr.intro
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

Result:
no goals

Proof state:
case mp
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (X ⊕ Y) κ → HasCardinalLT X κ ∧ HasCardinalLT Y κ

Tactic:
intro h

Result:
case mp
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h : HasCardinalLT (X ⊕ Y) κ
⊢ HasCardinalLT X κ ∧ HasCardinalLT Y κ

Proof state:
case mpr.intro
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.{w, u'} (Cardinal.mk Y) < Cardinal.lift.{u', w} κ
⊢ Cardinal.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ

Tactic:
rw [← Cardinal.lift_lt.{_, u}, Cardinal.lift_lift, Cardinal.lift_lift] at hY

Result:
case mpr.intro
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.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ

Proof state:
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κ

Result:
no goals

Proof state:
case mpr.intro
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : Cardinal.lift.{w, u} (Cardinal.mk X) < Cardinal.lift.{u, w} κ
hY : Cardinal.lift.{w, u'} (Cardinal.mk Y) < Cardinal.lift.{u', w} κ
⊢ Cardinal.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ

Tactic:
rw [← Cardinal.lift_lt.{_, u'}, Cardinal.lift_lift, Cardinal.lift_lift] at hX

Result:
case mpr.intro
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.{w, u'} (Cardinal.mk Y) < Cardinal.lift.{u', w} κ
⊢ Cardinal.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ

Proof state:
case mpr.intro
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : HasCardinalLT X κ
hY : HasCardinalLT Y κ
⊢ HasCardinalLT (X ⊕ Y) κ

Tactic:
dsimp [HasCardinalLT] at hX hY ⊢

Result:
case mpr.intro
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : Cardinal.lift.{w, u} (Cardinal.mk X) < Cardinal.lift.{u, w} κ
hY : Cardinal.lift.{w, u'} (Cardinal.mk Y) < Cardinal.lift.{u', w} κ
⊢ Cardinal.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ

Proof state:
case mpr.intro
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.{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]

Result:
case mpr.intro
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} κ

Proof state:
case mpr
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X κ ∧ HasCardinalLT Y κ → HasCardinalLT (X ⊕ Y) κ

Tactic:
rintro ⟨hX, hY⟩

Result:
case mpr.intro
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : HasCardinalLT X κ
hY : HasCardinalLT Y κ
⊢ HasCardinalLT (X ⊕ Y) κ

Proof state:
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (X ⊕ Y) κ ↔ HasCardinalLT X κ ∧ HasCardinalLT Y κ

Tactic:
constructor

Result:
case mp
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (X ⊕ Y) κ → HasCardinalLT X κ ∧ HasCardinalLT Y κ

case mpr
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X κ ∧ HasCardinalLT Y κ → HasCardinalLT (X ⊕ Y) κ

Proof state:
case mp
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h : HasCardinalLT (X ⊕ Y) κ
⊢ HasCardinalLT X κ ∧ HasCardinalLT Y κ

Tactic:
exact ⟨h.of_injective _ Sum.inl_injective,
  h.of_injective _ Sum.inr_injective⟩

Result:
no goals