Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_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) (d * c) 0
Tactic:
have h0 (d) : QuasiPeriodic f (d * c) :=
  ((equiv_zero_iff hf).mp h).1.mul_left 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 (d * c)
⊢ ∀ (d : R), (PeriodEquiv f) (d * c) 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 (d * c)
⊢ ∀ (d : R), (PeriodEquiv f) (d * c) 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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
⊢ ∀ (d : R), (PeriodEquiv f) (d * c) 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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
⊢ ∀ (d : R), (PeriodEquiv f) (d * c) 0
Tactic:
have h2 (d x) : f (d * c) = -1 ∨ f (d * x + 1) = 0 := by
  rw [eq_neg_iff_add_eq_zero, ← mul_eq_zero, add_one_mul (f _),
    ← neg_eq_iff_add_eq_zero, ← neg_mul, ← (h0 d).imp_left hf,
    ← add_assoc, ← mul_add, hf.is_good, hf.is_good, h1, add_left_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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
h2 : ∀ (d x : R), f (d * c) = -1 ∨ f (d * x + 1) = 0
⊢ ∀ (d : R), (PeriodEquiv f) (d * c) 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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
h2 : ∀ (d x : R), f (d * c) = -1 ∨ f (d * x + 1) = 0
⊢ ∀ (d : R), (PeriodEquiv f) (d * c) 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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
h2 : ∀ (d x : R), f (d * c) = -1 ∨ f (d * x + 1) = 0
d : R
h3 : f (d * -d + 1) = 0
⊢ f (d * c) = -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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
h2 : ∀ (d x : R), f (d * c) = -1 ∨ f (d * x + 1) = 0
d : R
h3 : f (d * -d + 1) = 0
⊢ f (d * c) = -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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
h2 : ∀ (d x : R), f (d * c) = -1 ∨ f (d * x + 1) = 0
d : R
h3 : f (d * -d + 1) = 0
h4 : f ((d - 1) * c) = -1
⊢ f (d * c) = -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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
h2 : ∀ (d x : R), f (d * c) = -1 ∨ f (d * x + 1) = 0
d : R
h3 : f (d * -d + 1) = 0
h4 : f ((d - 1) * 1 + 1) = 0
⊢ f (d * c) = -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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
d x : R
⊢ f (d * c) = -1 ∨ f (d * x + 1) = 0
Tactic:
rw [eq_neg_iff_add_eq_zero, ← mul_eq_zero, add_one_mul (f _),
  ← neg_eq_iff_add_eq_zero, ← neg_mul, ← (h0 d).imp_left hf,
  ← add_assoc, ← mul_add, hf.is_good, hf.is_good, h1, add_left_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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
h2 : ∀ (d x : R), f (d * c) = -1 ∨ f (d * x + 1) = 0
d : R
h3 : f (d * -d + 1) = 0
h4 : f ((d - 1) * c) = -1
⊢ f (d * c) = -1
Tactic:
rwa [← h1, ← one_add_mul _ c, add_sub_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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
h2 : ∀ (d x : R), f (d * c) = -1 ∨ f (d * x + 1) = 0
d : R
h3 : f (d * -d + 1) = 0
h4 : f ((d - 1) * 1 + 1) = 0
⊢ f (d * c) = -1
Tactic:
rw [mul_one, 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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
h2 : ∀ (d x : R), f (d * c) = -1 ∨ f (d * x + 1) = 0
d : R
h3 : f (d * -d + 1) = 0
h4 : f d = 0
⊢ f (d * c) = -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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
h2 : ∀ (d x : R), f (d * c) = -1 ∨ f (d * x + 1) = 0
d : R
h3 : f (d * -d + 1) = 0
h4 : f d = 0
⊢ f (d * c) = -1
Tactic:
rw [hf.is_good, h4, zero_mul, zero_add, add_neg_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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
h2 : ∀ (d x : R), f (d * c) = -1 ∨ f (d * x + 1) = 0
d : R
h3 : -1 = 0
h4 : f d = 0
⊢ f (d * c) = -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 (d * c)
h1 : ∀ (x : R), f (c + x) = f x
h2 : ∀ (d x : R), f (d * c) = -1 ∨ f (d * x + 1) = 0
d : R
h3 : -1 = 0
h4 : f d = 0
⊢ f (d * c) = -1
Tactic:
rw [h3, ← neg_neg (f _), ← neg_one_mul, h3, zero_mul]
State after:
no goals