internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.Extra.Infinitesimal.add
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ (2 * k) • |ε₁| + (2 * k) • |ε₂| < 1 + 1
Tactic:
exact add_lt_add (h₁ _) (h₂ _)
Proof state after:
no goals
Theorem: IMOSL.Extra.Infinitesimal.mul_of_abs_le_one_left
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε r : R
hε : Infinitesimal ε
hr : |r| ≤ 1
k : ℕ
⊢ k • |r * ε| < 1
Tactic:
rw [abs_mul, nsmul_eq_mul', mul_assoc, ← nsmul_eq_mul']
Proof state after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε r : R
hε : Infinitesimal ε
hr : |r| ≤ 1
k : ℕ
⊢ |r| * k • |ε| < 1
Theorem: IMOSL.Extra.Infinitesimal.mul_of_abs_le_one_left
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε r : R
hε : Infinitesimal ε
hr : |r| ≤ 1
k : ℕ
⊢ |r| * k • |ε| < 1
Tactic:
exact mul_lt_one_of_nonneg_of_lt_one_right hr (nsmul_nonneg (abs_nonneg ε) k) (hε k)
Proof state after:
no goals
Theorem: IMOSL.Extra.Infinitesimal.mul_of_abs_le_one_right
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε r : R
hε : Infinitesimal ε
hr : |r| ≤ 1
k : ℕ
⊢ k • |ε * r| < 1
Tactic:
rw [abs_mul, nsmul_eq_mul, ← mul_assoc, ← nsmul_eq_mul]
Proof state after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε r : R
hε : Infinitesimal ε
hr : |r| ≤ 1
k : ℕ
⊢ k • |ε| * |r| < 1
Theorem: IMOSL.Extra.Infinitesimal.mul_of_abs_le_one_right
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε r : R
hε : Infinitesimal ε
hr : |r| ≤ 1
k : ℕ
⊢ k • |ε| * |r| < 1
Tactic:
exact mul_lt_one_of_nonneg_of_lt_one_left (nsmul_nonneg (abs_nonneg ε) k) (hε k) hr
Proof state after:
no goals
Theorem: IMOSL.Extra.Infinitesimal.nsmul
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε : R
hε : Infinitesimal ε
n k : ℕ
⊢ k • |n • ε| < 1
Tactic:
rw [abs_nsmul, ← mul_nsmul']
Proof state after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε : R
hε : Infinitesimal ε
n k : ℕ
⊢ (k * n) • |ε| < 1
Theorem: IMOSL.Extra.Infinitesimal.nsmul
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε : R
hε : Infinitesimal ε
n k : ℕ
⊢ (k * n) • |ε| < 1
Tactic:
exact hε _
Proof state after:
no goals
Theorem: IMOSL.Extra.Infinitesimal.iff_nsmul_Nat_bdd
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε : R
x✝ : ∃ N, ∀ (k : ℕ), k • |ε| < ↑N
k N : ℕ
h : ∀ (k : ℕ), k • |ε| < ↑N
⊢ N • k • |ε| < N • 1
Tactic:
rw [← mul_nsmul, nsmul_one]
Proof state after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε : R
x✝ : ∃ N, ∀ (k : ℕ), k • |ε| < ↑N
k N : ℕ
h : ∀ (k : ℕ), k • |ε| < ↑N
⊢ (k * N) • |ε| < ↑N
Theorem: IMOSL.Extra.Infinitesimal.iff_nsmul_Nat_bdd
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε : R
x✝ : ∃ N, ∀ (k : ℕ), k • |ε| < ↑N
k N : ℕ
h : ∀ (k : ℕ), k • |ε| < ↑N
⊢ (k * N) • |ε| < ↑N
Tactic:
exact h _
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.apply_eq
Proof state before:
R : Type u_1
S : Sort u_2
inst✝ : AddCommMonoid R
f : R → S
c d : R
h : (PeriodEquiv f) c d
⊢ f c = f d
Tactic:
rw [← zero_add c, h, zero_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.zero_right
Proof state before:
R : Type u_1
S : Sort u_2
inst✝ : AddCommMonoid R
f : R → S
c x : R
⊢ f (x + c) = f (x + 0) ↔ f (x + c) = f x
Tactic:
rw [add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.zero_right'
Proof state before:
R : Type u_1
S : Sort u_2
inst✝ : AddCommMonoid R
f : R → S
c x : R
⊢ f (x + c) = f x ↔ f (c + x) = f x
Tactic:
rw [add_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.iff_sub
Proof state before:
R : Type u_1
S : Sort u_2
inst✝ : AddCommGroup R
f : R → S
c d : R
h : (PeriodEquiv f) c d
x : R
⊢ f (x + (c - d)) = f (x + 0)
Tactic:
rw [← add_comm_sub, h, sub_add_cancel, add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.iff_sub
Proof state before:
R : Type u_1
S : Sort u_2
inst✝ : AddCommGroup R
f : R → S
c d : R
h : (PeriodEquiv f) (c - d) 0
x : R
⊢ f (x + c) = f (x + d)
Tactic:
rw [← add_add_sub_cancel x c d, h, add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.equiv_zero_iff
Proof 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
⊢ (PeriodEquiv f) c 0 ↔ QuasiPeriodic f c ∧ f c = -1
Tactic:
rw [zero_right, QuasiPeriodic.iff_right hf]
Proof 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
⊢ (∀ (x : R), f (x + c) = f x) ↔ (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1
Theorem: IMOSL.IMO2012A5.PeriodEquiv.equiv_zero_iff
Proof 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
⊢ (∀ (x : R), f (x + c) = f x) ↔ (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1
Tactic:
refine ⟨λ h ↦ ?_, λ h x ↦ by rw [h.1, h.2, neg_neg, mul_one]⟩
Proof 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 : ∀ (x : R), f (x + c) = f x
⊢ (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1
Theorem: IMOSL.IMO2012A5.PeriodEquiv.equiv_zero_iff
Proof 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 : ∀ (x : R), f (x + c) = f x
⊢ (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1
Tactic:
have h0 : f c = -1 := by rw [← zero_add c, h, hf.map_zero]
Proof 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 : ∀ (x : R), f (x + c) = f x
h0 : f c = -1
⊢ (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1
Theorem: IMOSL.IMO2012A5.PeriodEquiv.equiv_zero_iff
Proof 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 : ∀ (x : R), f (x + c) = f x
h0 : f c = -1
⊢ (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1
Tactic:
refine ⟨λ x ↦ ?_, h0⟩
Proof 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 : ∀ (x : R), f (x + c) = f x
h0 : f c = -1
x : R
⊢ f (x + c) = f x * -f c
Theorem: IMOSL.IMO2012A5.PeriodEquiv.equiv_zero_iff
Proof 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 : ∀ (x : R), f (x + c) = f x
h0 : f c = -1
x : R
⊢ f (x + c) = f x * -f c
Tactic:
rw [h0, neg_neg, mul_one, h]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.equiv_zero_iff
Proof 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 : (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1
x : R
⊢ f (x + c) = f x
Tactic:
rw [h.1, h.2, neg_neg, mul_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.equiv_zero_iff
Proof 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 : ∀ (x : R), f (x + c) = f x
⊢ f c = -1
Tactic:
rw [← zero_add c, h, hf.map_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_equiv_zero
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_equiv_zero
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_equiv_zero
Proof 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]
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_equiv_zero
Proof 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 ↦ ?_⟩
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_equiv_zero
Proof 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 ↦ ?_)
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_equiv_zero
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_equiv_zero
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_equiv_zero
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_equiv_zero
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_equiv_zero
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv_zero
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv_zero
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv_zero
Proof 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]
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv_zero
Proof 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 ↦ ?_⟩
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv_zero
Proof 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 ↦ ?_)
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv_zero
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv_zero
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv_zero
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv_zero
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv_zero
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_equiv
Proof 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 d : R
h : (PeriodEquiv f) c d
a : R
⊢ (PeriodEquiv f) (a * c) (a * d)
Tactic:
rw [iff_sub, ← mul_sub]
Proof 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 d : R
h : (PeriodEquiv f) c d
a : R
⊢ (PeriodEquiv f) (a * (c - d)) 0
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_left_equiv
Proof 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 d : R
h : (PeriodEquiv f) c d
a : R
⊢ (PeriodEquiv f) (a * (c - d)) 0
Tactic:
exact mul_left_equiv_zero hf (iff_sub.mp h) a
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv
Proof 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 d : R
h : (PeriodEquiv f) c d
a : R
⊢ (PeriodEquiv f) (c * a) (d * a)
Tactic:
rw [iff_sub, ← sub_mul]
Proof 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 d : R
h : (PeriodEquiv f) c d
a : R
⊢ (PeriodEquiv f) ((c - d) * a) 0
Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv
Proof 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 d : R
h : (PeriodEquiv f) c d
a : R
⊢ (PeriodEquiv f) ((c - d) * a) 0
Tactic:
exact mul_right_equiv_zero hf (iff_sub.mp h) a
Proof state after:
no goals