Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : x * y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ 0 = 0 * 0

pp: case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : x * y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 * 1

pp: case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : x * y = 0
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ 0 = 1 * 0

pp: case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : x * y = 0
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ 0 = 1 * 1

pp: case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : ¬x * y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 * 0

pp: case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : ¬x * y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 1 = 0 * 1

pp: case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : ¬x * y = 0
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ 1 = 1 * 0

pp: case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : ¬x * y = 0
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ 1 = 1 * 1

Tactic:
<;>

Goal state after:
case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : x * y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ 0 = 0 * 0

case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : x * y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 * 1

case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : x * y = 0
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ 0 = 1 * 0

case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : x * y = 0
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ 0 = 1 * 1

case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : ¬x * y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 * 0

case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : ¬x * y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 1 = 0 * 1

case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : ¬x * y = 0
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ 1 = 1 * 0

case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : ¬x * y = 0
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ 1 = 1 * 1