Theorem: Tutorial.not_HasFinSubCover_concat (Tutorial/Advanced/Analysis/Lecture3.lean)

State before:
ι : Type
U : ι → Set ℝ
a b c : ℝ
⊢ ¬HasFinSubCover U (Icc a b) → HasFinSubCover U (Icc a c) → ¬HasFinSubCover U (Icc c b)
Tactic:
contrapose!
State after:
ι : Type
U : ι → Set ℝ
a b c : ℝ
⊢ HasFinSubCover U (Icc a c) ∧ HasFinSubCover U (Icc c b) → HasFinSubCover U (Icc a b)

State before:
ι : Type
U : ι → Set ℝ
a b c : ℝ
⊢ HasFinSubCover U (Icc a c) ∧ HasFinSubCover U (Icc c b) → HasFinSubCover U (Icc a b)
Tactic:
apply (fun H ↦ hasFinSubCover_concat H.1 H.2)
State after:
no goals