α : Type u_2
β : Type u_1
H : Infinite (α ⊕ β)
⊢ Infinite α ∨ Infinite β
α : Type u_2
β : Type u_1
⊢ Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β
refine' ⟨fun H => _, fun H => H.elim (@Sum.infinite_of_left α β) (@Sum.infinite_of_right α β)⟩
α : Type u_2
β : Type u_1
H : ¬Infinite α ∧ ¬Infinite β
⊢ ¬Infinite (α ⊕ β)
α : Type u_2
β : Type u_1
H : Infinite (α ⊕ β)
⊢ Infinite α ∨ Infinite β
contrapose! H
α : Type u_2
β : Type u_1
H : ¬Infinite α ∧ ¬Infinite β
this : Fintype α
⊢ ¬Infinite (α ⊕ β)
α : Type u_2
β : Type u_1
H : ¬Infinite α ∧ ¬Infinite β
⊢ ¬Infinite (α ⊕ β)
haveI := fintypeOfNotInfinite H.1
α : Type u_2
β : Type u_1
H : ¬Infinite α ∧ ¬Infinite β
this✝ : Fintype α
this : Fintype β
⊢ ¬Infinite (α ⊕ β)
α : Type u_2
β : Type u_1
H : ¬Infinite α ∧ ¬Infinite β
this : Fintype α
⊢ ¬Infinite (α ⊕ β)
haveI := fintypeOfNotInfinite H.2
no goals
α : Type u_2
β : Type u_1
H : ¬Infinite α ∧ ¬Infinite β
this✝ : Fintype α
this : Fintype β
⊢ ¬Infinite (α ⊕ β)
exact Infinite.false