Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_mul_left_eq_zero_imp (IMOSLLean4/IMO2012/A5/A5General/A5QuasiPeriodic.lean)

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
⊢ QuasiPeriodic f d
Tactic:
rw [iff_left2 hf.toNontrivialGood]
State after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
⊢ ∀ (x : R), f (d * x + 1) = 0

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
⊢ ∀ (x : R), f (d * x + 1) = 0
Tactic:
intro x
State after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
⊢ f (d * x + 1) = 0

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
⊢ f (d * x + 1) = 0
Tactic:
have h2 := reduced_map_eq_one hf h h0
State after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
⊢ f (d * x + 1) = 0

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
⊢ f (d * x + 1) = 0
Tactic:
have h3 : f (d * (c + x) + 1) = -f (d * x + 1) := by
  rw [iff_left hf.toNontrivialGood] at h
  rw [hf.is_good, h, add_left_comm, h, h2, neg_one_mul,
    neg_one_mul, mul_neg, ← neg_add, hf.is_good]
State after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
h3 : f (d * (c + x) + 1) = -f (d * x + 1)
⊢ f (d * x + 1) = 0

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
h3 : f (d * (c + x) + 1) = -f (d * x + 1)
⊢ f (d * x + 1) = 0
Tactic:
rw [mul_add, h1, zero_add, eq_neg_iff_add_eq_zero, ← two_mul, mul_eq_zero] at h3
State after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
h3 : 2 = 0 ∨ f (d * x + 1) = 0
⊢ f (d * x + 1) = 0

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
h3 : 2 = 0 ∨ f (d * x + 1) = 0
⊢ f (d * x + 1) = 0
Tactic:
refine h3.resolve_left λ h3 ↦ h0 ?_
State after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
h3✝ : 2 = 0 ∨ f (d * x + 1) = 0
h3 : 2 = 0
⊢ c = 0

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
h3✝ : 2 = 0 ∨ f (d * x + 1) = 0
h3 : 2 = 0
⊢ c = 0
Tactic:
rw [reduced_eq_zero_iff hf h, h2, eq_neg_iff_add_eq_zero, one_add_one_eq_two, h3]
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
⊢ f (d * (c + x) + 1) = -f (d * x + 1)
Tactic:
rw [iff_left hf.toNontrivialGood] at h
State after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : ∀ (x : R), f (c + x) = -f c * f x
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
⊢ f (d * (c + x) + 1) = -f (d * x + 1)

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : ∀ (x : R), f (c + x) = -f c * f x
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
⊢ f (d * (c + x) + 1) = -f (d * x + 1)
Tactic:
rw [hf.is_good, h, add_left_comm, h, h2, neg_one_mul,
  neg_one_mul, mul_neg, ← neg_add, hf.is_good]
State after:
no goals