Theorem: IMOSL.IMO2012A5.good_Nontrivial_or_eq_zero (IMOSLLean4/IMO2012/A5/A5Answers/ZeroMap.lean)

State before:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
⊢ 0 + f (1 + 1) = f 1 * f 1 + f (1 + 1)
Tactic:
rw [zero_add, ← h, one_mul]
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
h0 : f 1 = 0
x : R
⊢ 0 = f x * (f 0 + 1)
Tactic:
have h1 := h x 0
State after:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
h0 : f 1 = 0
x : R
h1 : f (x * 0 + 1) = f x * f 0 + f (x + 0)
⊢ 0 = f x * (f 0 + 1)

State before:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
h0 : f 1 = 0
x : R
h1 : f (x * 0 + 1) = f x * f 0 + f (x + 0)
⊢ 0 = f x * (f 0 + 1)
Tactic:
rwa [mul_zero, zero_add, h0, add_zero, ← mul_add_one (f x)] at h1
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
h0 : f 1 = 0
h1 : ∀ (x : R), 0 = f x * (f 0 + 1)
h2 : f 0 = 0
x : R
⊢ f x = 0
Tactic:
specialize h1 x
State after:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
h0 : f 1 = 0
h2 : f 0 = 0
x : R
h1 : 0 = f x * (f 0 + 1)
⊢ f x = 0

State before:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
h0 : f 1 = 0
h2 : f 0 = 0
x : R
h1 : 0 = f x * (f 0 + 1)
⊢ f x = 0
Tactic:
rwa [h2, zero_add, mul_one, eq_comm] at h1
State after:
no goals