G₀ : Type u
M₀ : Type u_2
M₀' : Type u_1
G₀' : Type ?u.9044
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
a b : M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬0 = 1
G₀ : Type u
M₀ : Type u_2
M₀' : Type u_1
G₀' : Type ?u.9044
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
a b : M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬f 0 = f 1
rw [zero, one]
no goals
G₀ : Type u
M₀ : Type u_2
M₀' : Type u_1
G₀' : Type ?u.9044
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
a b : M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬0 = 1
exact zero_ne_one