case top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
a b : WithTop α
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤

case coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
a b : WithTop α
c : α
⊢ (a + b) * ↑c = a * ↑c + b * ↑c
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
a b c : WithTop α
⊢ (a + b) * c = a * c + b * c
induction' c using WithTop.recTopCoe with c
no goals
case top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
a b : WithTop α
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤
by_cases ha : a = 0 <;> simp [ha]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
a b : WithTop α
c : α
hc : c = 0
⊢ (a + b) * ↑c = a * ↑c + b * ↑c

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (a + b) * ↑c = a * ↑c + b * ↑c
case coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
a b : WithTop α
c : α
⊢ (a + b) * ↑c = a * ↑c + b * ↑c
by_cases hc : c = 0
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (Option.bind (a + b) fun a => Option.some (a * c)) =
    (Option.bind a fun a => Option.some (a * c)) + Option.bind b fun a => Option.some (a * c)
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (a + b) * ↑c = a * ↑c + b * ↑c
simp [mul_coe hc]
case neg.none.none
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
c : α
hc : ¬c = 0
⊢ (Option.bind (none + none) fun a => Option.some (a * c)) =
    (Option.bind none fun a => Option.some (a * c)) + Option.bind none fun a => Option.some (a * c)

case neg.none.some
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
c : α
hc : ¬c = 0
val✝ : α
⊢ (Option.bind (none + Option.some val✝) fun a => Option.some (a * c)) =
    (Option.bind none fun a => Option.some (a * c)) + Option.bind (Option.some val✝) fun a => Option.some (a * c)

case neg.some.none
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
c : α
hc : ¬c = 0
val✝ : α
⊢ (Option.bind (Option.some val✝ + none) fun a => Option.some (a * c)) =
    (Option.bind (Option.some val✝) fun a => Option.some (a * c)) + Option.bind none fun a => Option.some (a * c)

case neg.some.some
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
c : α
hc : ¬c = 0
val✝¹ val✝ : α
⊢ (Option.bind (Option.some val✝¹ + Option.some val✝) fun a => Option.some (a * c)) =
    (Option.bind (Option.some val✝¹) fun a => Option.some (a * c)) +
      Option.bind (Option.some val✝) fun a => Option.some (a * c)
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (Option.bind (a + b) fun a => Option.some (a * c)) =
    (Option.bind a fun a => Option.some (a * c)) + Option.bind b fun a => Option.some (a * c)
cases a <;> cases b
no goals
case neg.none.none
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
c : α
hc : ¬c = 0
⊢ (Option.bind (none + none) fun a => Option.some (a * c)) =
    (Option.bind none fun a => Option.some (a * c)) + Option.bind none fun a => Option.some (a * c)

case neg.none.some
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
c : α
hc : ¬c = 0
val✝ : α
⊢ (Option.bind (none + Option.some val✝) fun a => Option.some (a * c)) =
    (Option.bind none fun a => Option.some (a * c)) + Option.bind (Option.some val✝) fun a => Option.some (a * c)

case neg.some.none
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
c : α
hc : ¬c = 0
val✝ : α
⊢ (Option.bind (Option.some val✝ + none) fun a => Option.some (a * c)) =
    (Option.bind (Option.some val✝) fun a => Option.some (a * c)) + Option.bind none fun a => Option.some (a * c)

case neg.some.some
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
c : α
hc : ¬c = 0
val✝¹ val✝ : α
⊢ (Option.bind (Option.some val✝¹ + Option.some val✝) fun a => Option.some (a * c)) =
    (Option.bind (Option.some val✝¹) fun a => Option.some (a * c)) +
      Option.bind (Option.some val✝) fun a => Option.some (a * c)
repeat' first | rfl |exact congr_arg some (add_mul _ _ _)
no goals
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
a b : WithTop α
c : α
hc : c = 0
⊢ (a + b) * ↑c = a * ↑c + b * ↑c
simp [hc]
no goals
case neg.some.some
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
c : α
hc : ¬c = 0
val✝¹ val✝ : α
⊢ (Option.bind (Option.some val✝¹ + Option.some val✝) fun a => Option.some (a * c)) =
    (Option.bind (Option.some val✝¹) fun a => Option.some (a * c)) +
      Option.bind (Option.some val✝) fun a => Option.some (a * c)
first | rfl |exact congr_arg some (add_mul _ _ _)
case neg.some.some
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
c : α
hc : ¬c = 0
val✝¹ val✝ : α
⊢ (Option.bind (Option.some val✝¹ + Option.some val✝) fun a => Option.some (a * c)) =
    (Option.bind (Option.some val✝¹) fun a => Option.some (a * c)) +
      Option.bind (Option.some val✝) fun a => Option.some (a * c)
case neg.some.some
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
c : α
hc : ¬c = 0
val✝¹ val✝ : α
⊢ (Option.bind (Option.some val✝¹ + Option.some val✝) fun a => Option.some (a * c)) =
    (Option.bind (Option.some val✝¹) fun a => Option.some (a * c)) +
      Option.bind (Option.some val✝) fun a => Option.some (a * c)
rfl
no goals
case neg.some.some
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CanonicallyOrderedCommSemiring α
c : α
hc : ¬c = 0
val✝¹ val✝ : α
⊢ (Option.bind (Option.some val✝¹ + Option.some val✝) fun a => Option.some (a * c)) =
    (Option.bind (Option.some val✝¹) fun a => Option.some (a * c)) +
      Option.bind (Option.some val✝) fun a => Option.some (a * c)
exact congr_arg some (add_mul _ _ _)