[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
R : Type u_4
inst✝ : AddGroup R
a b : R
h : a - b = 0
⊢ a + -b = b + -b
[PROOFSTEP]
rw [← sub_eq_add_neg, h, add_neg_self]
  -- Porting note:
  -- This theorem was introduced during ad-hoc porting
  -- and hopefully can be removed again after `Mathlib.Algebra.Ring.Basic` is fully ported.
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
⊢ 1 ≠ 0
[PROOFSTEP]
intro h
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
⊢ False
[PROOFSTEP]
rcases exists_pair_ne M₀ with ⟨x, y, hx⟩
[GOAL]
case intro.intro
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ False
[PROOFSTEP]
apply hx
[GOAL]
case intro.intro
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ x = y
[PROOFSTEP]
calc
  x = 1 * x := by rw [one_mul]
  _ = 0 := by rw [h, zero_mul]
  _ = 1 * y := by rw [h, zero_mul]
  _ = y := by rw [one_mul]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ x = 1 * x
[PROOFSTEP]
rw [one_mul]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 1 * x = 0
[PROOFSTEP]
rw [h, zero_mul]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 0 = 1 * y
[PROOFSTEP]
rw [h, zero_mul]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 1 * y = y
[PROOFSTEP]
rw [one_mul]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
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
[PROOFSTEP]
rw [zero, one]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
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
[PROOFSTEP]
exact zero_ne_one
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
⊢ 0 = a * b ↔ a = 0 ∨ b = 0
[PROOFSTEP]
rw [eq_comm, mul_eq_zero]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
⊢ a * a = 0 ↔ a = 0
[PROOFSTEP]
simp
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
⊢ 0 = a * a ↔ a = 0
[PROOFSTEP]
simp
