Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv_zero (IMOSLLean4/IMO2012/A5/A5General/A5Periodic.lean)

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
⊢ ∀ (d : R), (PeriodEquiv f) (c * d) 0
Tactic:
have h0 (d) : QuasiPeriodic f (c * d) :=
  ((equiv_zero_iff hf).mp h).1.mul_right hf d
State after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
⊢ ∀ (d : R), (PeriodEquiv f) (c * d) 0

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
⊢ ∀ (d : R), (PeriodEquiv f) (c * d) 0
Tactic:
have h1 := zero_right.mp h
State after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
⊢ ∀ (d : R), (PeriodEquiv f) (c * d) 0

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
⊢ ∀ (d : R), (PeriodEquiv f) (c * d) 0
Tactic:
have h2 (d x) : f (c * d) = -1 ∨ f (x * d + 1) = 0 := by
  rw [eq_neg_iff_add_eq_zero, or_comm, ← mul_eq_zero, mul_add_one (f _),
    ← neg_eq_iff_add_eq_zero, ← mul_neg, ← (h0 d).imp_right hf,
    add_right_comm, ← add_mul, hf.is_good, hf.is_good, h1, add_right_comm, h1]
State after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
h2 : ∀ (d x : R), f (c * d) = -1 ∨ f (x * d + 1) = 0
⊢ ∀ (d : R), (PeriodEquiv f) (c * d) 0

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
h2 : ∀ (d x : R), f (c * d) = -1 ∨ f (x * d + 1) = 0
⊢ ∀ (d : R), (PeriodEquiv f) (c * d) 0
Tactic:
refine λ d ↦ (equiv_zero_iff hf).mpr ⟨h0 d, (h2 d (-d)).elim id λ h3 ↦ ?_⟩
State after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
h2 : ∀ (d x : R), f (c * d) = -1 ∨ f (x * d + 1) = 0
d : R
h3 : f (-d * d + 1) = 0
⊢ f (c * d) = -1

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
h2 : ∀ (d x : R), f (c * d) = -1 ∨ f (x * d + 1) = 0
d : R
h3 : f (-d * d + 1) = 0
⊢ f (c * d) = -1
Tactic:
refine (h2 (d - 1) 1).elim (λ h4 ↦ ?_) (λ h4 ↦ ?_)
State after:
case refine_1
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
h2 : ∀ (d x : R), f (c * d) = -1 ∨ f (x * d + 1) = 0
d : R
h3 : f (-d * d + 1) = 0
h4 : f (c * (d - 1)) = -1
⊢ f (c * d) = -1

case refine_2
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
h2 : ∀ (d x : R), f (c * d) = -1 ∨ f (x * d + 1) = 0
d : R
h3 : f (-d * d + 1) = 0
h4 : f (1 * (d - 1) + 1) = 0
⊢ f (c * d) = -1

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
d x : R
⊢ f (c * d) = -1 ∨ f (x * d + 1) = 0
Tactic:
rw [eq_neg_iff_add_eq_zero, or_comm, ← mul_eq_zero, mul_add_one (f _),
  ← neg_eq_iff_add_eq_zero, ← mul_neg, ← (h0 d).imp_right hf,
  add_right_comm, ← add_mul, hf.is_good, hf.is_good, h1, add_right_comm, h1]
State after:
no goals

State before:
case refine_1
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
h2 : ∀ (d x : R), f (c * d) = -1 ∨ f (x * d + 1) = 0
d : R
h3 : f (-d * d + 1) = 0
h4 : f (c * (d - 1)) = -1
⊢ f (c * d) = -1
Tactic:
rwa [← h1, ← mul_add_one c, sub_add_cancel] at h4
State after:
no goals

State before:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
h2 : ∀ (d x : R), f (c * d) = -1 ∨ f (x * d + 1) = 0
d : R
h3 : f (-d * d + 1) = 0
h4 : f (1 * (d - 1) + 1) = 0
⊢ f (c * d) = -1
Tactic:
rw [one_mul, sub_add_cancel] at h4
State after:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
h2 : ∀ (d x : R), f (c * d) = -1 ∨ f (x * d + 1) = 0
d : R
h3 : f (-d * d + 1) = 0
h4 : f d = 0
⊢ f (c * d) = -1

State before:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
h2 : ∀ (d x : R), f (c * d) = -1 ∨ f (x * d + 1) = 0
d : R
h3 : f (-d * d + 1) = 0
h4 : f d = 0
⊢ f (c * d) = -1
Tactic:
rw [hf.is_good, h4, mul_zero, zero_add, neg_add_self, hf.map_zero] at h3
State after:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
h2 : ∀ (d x : R), f (c * d) = -1 ∨ f (x * d + 1) = 0
d : R
h3 : -1 = 0
h4 : f d = 0
⊢ f (c * d) = -1

State before:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : (PeriodEquiv f) c 0
h0 : ∀ (d : R), QuasiPeriodic f (c * d)
h1 : ∀ (x : R), f (x + c) = f x
h2 : ∀ (d x : R), f (c * d) = -1 ∨ f (x * d + 1) = 0
d : R
h3 : -1 = 0
h4 : f d = 0
⊢ f (c * d) = -1
Tactic:
rw [h3, ← neg_neg (f _), ← neg_one_mul, h3, zero_mul]
State after:
no goals