α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Zero α
inst✝ : Mul α
a b : WithTop α
⊢ (a = 0 ∨ b = 0) ∧ 0 = none ∨ ¬(a = 0 ∨ b = 0) ∧ (a = none ∨ b = none) ↔ a ≠ 0 ∧ b = none ∨ a = none ∧ b ≠ 0
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Zero α
inst✝ : Mul α
a b : WithTop α
⊢ a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
rw [mul_def, ite_eq_iff, ← none_eq_top, Option.map₂_eq_none_iff]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Zero α
inst✝ : Mul α
a b : WithTop α
ha : a = 0 → a ≠ none
⊢ (a = 0 ∨ b = 0) ∧ 0 = none ∨ ¬(a = 0 ∨ b = 0) ∧ (a = none ∨ b = none) ↔ a ≠ 0 ∧ b = none ∨ a = none ∧ b ≠ 0
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Zero α
inst✝ : Mul α
a b : WithTop α
⊢ (a = 0 ∨ b = 0) ∧ 0 = none ∨ ¬(a = 0 ∨ b = 0) ∧ (a = none ∨ b = none) ↔ a ≠ 0 ∧ b = none ∨ a = none ∧ b ≠ 0
have ha : a = 0 → a ≠ none := fun h => h.symm ▸ zero_ne_top
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Zero α
inst✝ : Mul α
a b : WithTop α
ha : a = 0 → a ≠ none
hb : b = 0 → b ≠ none
⊢ (a = 0 ∨ b = 0) ∧ 0 = none ∨ ¬(a = 0 ∨ b = 0) ∧ (a = none ∨ b = none) ↔ a ≠ 0 ∧ b = none ∨ a = none ∧ b ≠ 0
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Zero α
inst✝ : Mul α
a b : WithTop α
ha : a = 0 → a ≠ none
⊢ (a = 0 ∨ b = 0) ∧ 0 = none ∨ ¬(a = 0 ∨ b = 0) ∧ (a = none ∨ b = none) ↔ a ≠ 0 ∧ b = none ∨ a = none ∧ b ≠ 0
have hb : b = 0 → b ≠ none := fun h => h.symm ▸ zero_ne_top
no goals
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Zero α
inst✝ : Mul α
a b : WithTop α
ha : a = 0 → a ≠ none
hb : b = 0 → b ≠ none
⊢ (a = 0 ∨ b = 0) ∧ 0 = none ∨ ¬(a = 0 ∨ b = 0) ∧ (a = none ∨ b = none) ↔ a ≠ 0 ∧ b = none ∨ a = none ∧ b ≠ 0
tauto