Theorem: mul_eq_zero_of (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝³ : Monad m
ι : Type ?u.82027
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
α : Type u_1
inst✝ : MulZeroClass α
x y : α
h : x = 0
⊢ x * y = 0
Tactic:
rw [h]
State after:
m : Type u → Type v
inst✝³ : Monad m
ι : Type ?u.82027
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
α : Type u_1
inst✝ : MulZeroClass α
x y : α
h : x = 0
⊢ 0 * y = 0

State before:
m : Type u → Type v
inst✝³ : Monad m
ι : Type ?u.82027
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
α : Type u_1
inst✝ : MulZeroClass α
x y : α
h : x = 0
⊢ 0 * y = 0
Tactic:
exact MulZeroClass.zero_mul y
State after:
no goals

State before:
m : Type u → Type v
inst✝³ : Monad m
ι : Type ?u.82027
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
α : Type u_1
inst✝ : MulZeroClass α
x y : α
h : y = 0
⊢ x * y = 0
Tactic:
rw [h]
State after:
m : Type u → Type v
inst✝³ : Monad m
ι : Type ?u.82027
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
α : Type u_1
inst✝ : MulZeroClass α
x y : α
h : y = 0
⊢ x * 0 = 0

State before:
m : Type u → Type v
inst✝³ : Monad m
ι : Type ?u.82027
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
α : Type u_1
inst✝ : MulZeroClass α
x y : α
h : y = 0
⊢ x * 0 = 0
Tactic:
exact MulZeroClass.mul_zero x
State after:
no goals