internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2011A3.relation_summary
Proof state before:
case intro.intro.intro.intro
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A B C : R
h : good (fun x => x * (x * A) - x * B + C) fun x => x * A + B
⊢ ∃ A_1 C_1,
    A_1 * A_1 = A_1 ∧
      C_1 * A_1 = C_1 ∧
        ((fun x => x * (x * A) - x * B + C) = fun x => x * x * A_1 + C_1) ∧ (fun x => x * A + B) = fun x => x * A_1
Tactic:
rcases step2 hR h with ⟨rfl, h0, h1⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h : good (fun x => x * (x * A) - x * 0 + C) fun x => x * A + 0
h0 : A * A = A
h1 : C * A = C
⊢ ∃ A_1 C_1,
    A_1 * A_1 = A_1 ∧
      C_1 * A_1 = C_1 ∧
        ((fun x => x * (x * A) - x * 0 + C) = fun x => x * x * A_1 + C_1) ∧ (fun x => x * A + 0) = fun x => x * A_1
Theorem: IMOSL.IMO2011A3.relation_summary
Proof state before:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h : good (fun x => x * (x * A) - x * 0 + C) fun x => x * A + 0
h0 : A * A = A
h1 : C * A = C
⊢ ∃ A_1 C_1,
    A_1 * A_1 = A_1 ∧
      C_1 * A_1 = C_1 ∧
        ((fun x => x * (x * A) - x * 0 + C) = fun x => x * x * A_1 + C_1) ∧ (fun x => x * A + 0) = fun x => x * A_1
Tactic:
refine ⟨A, C, h0, h1, ?_, ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.refine_1
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h : good (fun x => x * (x * A) - x * 0 + C) fun x => x * A + 0
h0 : A * A = A
h1 : C * A = C
⊢ (fun x => x * (x * A) - x * 0 + C) = fun x => x * x * A + C

case intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h : good (fun x => x * (x * A) - x * 0 + C) fun x => x * A + 0
h0 : A * A = A
h1 : C * A = C
⊢ (fun x => x * A + 0) = fun x => x * A
Theorem: IMOSL.IMO2011A3.relation_summary
Proof state before:
case intro.intro.intro.intro.intro.intro.refine_1
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h : good (fun x => x * (x * A) - x * 0 + C) fun x => x * A + 0
h0 : A * A = A
h1 : C * A = C
⊢ (fun x => x * (x * A) - x * 0 + C) = fun x => x * x * A + C
Tactic:
funext x
Proof state after:
case intro.intro.intro.intro.intro.intro.refine_1.h
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h : good (fun x => x * (x * A) - x * 0 + C) fun x => x * A + 0
h0 : A * A = A
h1 : C * A = C
x : R
⊢ x * (x * A) - x * 0 + C = x * x * A + C
Theorem: IMOSL.IMO2011A3.relation_summary
Proof state before:
case intro.intro.intro.intro.intro.intro.refine_1.h
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h : good (fun x => x * (x * A) - x * 0 + C) fun x => x * A + 0
h0 : A * A = A
h1 : C * A = C
x : R
⊢ x * (x * A) - x * 0 + C = x * x * A + C
Tactic:
rw [mul_zero, sub_zero, ← mul_assoc]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.relation_summary
Proof state before:
case intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h : good (fun x => x * (x * A) - x * 0 + C) fun x => x * A + 0
h0 : A * A = A
h1 : C * A = C
⊢ (fun x => x * A + 0) = fun x => x * A
Tactic:
simp only [add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.quot_self_comp_idempotent_self_mul_part
Proof state before:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ (idempotent_self_mul_part h) ⟦x⟧ - x = (1 - a) * -x
Tactic:
rw [mul_neg, ← neg_mul, neg_sub, sub_one_mul, mul_comm]
Proof state after:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ (idempotent_self_mul_part h) ⟦x⟧ - x = x * a - x
Theorem: IMOSL.IMO2011A3.quot_self_comp_idempotent_self_mul_part
Proof state before:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ (idempotent_self_mul_part h) ⟦x⟧ - x = x * a - x
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.quot_compl_comp_idempotent_compl_mul_part
Proof state before:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ (idempotent_compl_mul_part h) ⟦x⟧ - x = a * -x
Tactic:
change x * (1 - a) - x = _
Proof state after:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ x * (1 - a) - x = a * -x
Theorem: IMOSL.IMO2011A3.quot_compl_comp_idempotent_compl_mul_part
Proof state before:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ x * (1 - a) - x = a * -x
Tactic:
rw [mul_one_sub, sub_sub_cancel_left, mul_neg, mul_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.idempotent_decomp_AddHom_map_quot_self
Proof state before:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ (idempotent_decomp_AddHom h) ((Ideal.Quotient.mk (Ideal.span {1 - a})) x, (Ideal.Quotient.mk (Ideal.span {a})) x) = x
Tactic:
rw [idempotent_decomp_AddHom_map_quot, ← mul_add, add_sub_cancel, mul_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.quot_self_comp_idempotent_decomp_AddHom
Proof state before:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
p : (R ⧸ Ideal.span {1 - a}) × R ⧸ Ideal.span {a}
⊢ (Ideal.Quotient.mk (Ideal.span {1 - a})) ((idempotent_decomp_AddHom h) p) = p.1
Tactic:
rw [idempotent_decomp_AddHom, AddMonoidHom.coprod_apply,
  map_add, quot_self_comp_idempotent_self_mul_part,
  quot_self_comp_idempotent_compl_mul_part, add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.quot_compl_comp_idempotent_decomp_AddHom
Proof state before:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
p : (R ⧸ Ideal.span {1 - a}) × R ⧸ Ideal.span {a}
⊢ (Ideal.Quotient.mk (Ideal.span {a})) ((idempotent_decomp_AddHom h) p) = p.2
Tactic:
rw [idempotent_decomp_AddHom, AddMonoidHom.coprod_apply,
  map_add, quot_compl_comp_idempotent_self_mul_part,
  quot_compl_comp_idempotent_compl_mul_part, zero_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.final_solution
Proof state before:
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
⊢ ∃ R₁ R₂ x x_1 φ c, f = φ.conj (Prod.map (fun x_2 => x_2 * x_2 + c) 0) ∧ g = φ.conj (Prod.map id 0)
Tactic:
rcases relation_summary hR h with ⟨A, C, h0, h1, rfl, rfl⟩
Proof state after:
case intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h0 : A * A = A
h1 : C * A = C
h : good (fun x => x * x * A + C) fun x => x * A
⊢ ∃ R₁ R₂ x x_1 φ c,
    (fun x => x * x * A + C) = φ.conj (Prod.map (fun x_2 => x_2 * x_2 + c) 0) ∧
      (fun x => x * A) = φ.conj (Prod.map id 0)
Theorem: IMOSL.IMO2011A3.final_solution
Proof state before:
case intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h0 : A * A = A
h1 : C * A = C
h : good (fun x => x * x * A + C) fun x => x * A
⊢ ∃ R₁ R₂ x x_1 φ c,
    (fun x => x * x * A + C) = φ.conj (Prod.map (fun x_2 => x_2 * x_2 + c) 0) ∧
      (fun x => x * A) = φ.conj (Prod.map id 0)
Tactic:
refine ⟨R ⧸ Ideal.span {1 - A}, R ⧸ Ideal.span {A},
  Ideal.Quotient.commRing _, Ideal.Quotient.commRing _,
  (idempotent_decomp h0).symm, idempotent_self_mul_part h0 C,
  funext λ x ↦ ?_, funext λ x ↦ ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.refine_1
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h0 : A * A = A
h1 : C * A = C
h : good (fun x => x * x * A + C) fun x => x * A
x : R
⊢ x * x * A + C =
    (idempotent_decomp h0).symm.conj
      (Prod.map
        (fun x =>
          x * x +
            (Ideal.Quotient.mk (Ideal.span {1 - A}))
              ((idempotent_self_mul_part h0) ((Ideal.Quotient.mk (Ideal.span {1 - A})) C)))
        0)
      x

case intro.intro.intro.intro.intro.refine_2
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h0 : A * A = A
h1 : C * A = C
h : good (fun x => x * x * A + C) fun x => x * A
x : R
⊢ x * A = (idempotent_decomp h0).symm.conj (Prod.map id 0) x
Theorem: IMOSL.IMO2011A3.final_solution
Proof state before:
case intro.intro.intro.intro.intro.refine_1
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h0 : A * A = A
h1 : C * A = C
h : good (fun x => x * x * A + C) fun x => x * A
x : R
⊢ x * x * A + C =
    (idempotent_decomp h0).symm.conj
      (Prod.map
        (fun x =>
          x * x +
            (Ideal.Quotient.mk (Ideal.span {1 - A}))
              ((idempotent_self_mul_part h0) ((Ideal.Quotient.mk (Ideal.span {1 - A})) C)))
        0)
      x
Tactic:
change _ = (idempotent_decomp h0).symm (_, 0)
Proof state after:
case intro.intro.intro.intro.intro.refine_1
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h0 : A * A = A
h1 : C * A = C
h : good (fun x => x * x * A + C) fun x => x * A
x : R
⊢ x * x * A + C =
    (idempotent_decomp h0).symm
      ((fun x =>
            x * x +
              (Ideal.Quotient.mk (Ideal.span {1 - A}))
                ((idempotent_self_mul_part h0) ((Ideal.Quotient.mk (Ideal.span {1 - A})) C)))
          ((Ideal.Quotient.mk (Ideal.span {1 - A})) x),
        0)
Theorem: IMOSL.IMO2011A3.final_solution
Proof state before:
case intro.intro.intro.intro.intro.refine_1
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h0 : A * A = A
h1 : C * A = C
h : good (fun x => x * x * A + C) fun x => x * A
x : R
⊢ x * x * A + C =
    (idempotent_decomp h0).symm
      ((fun x =>
            x * x +
              (Ideal.Quotient.mk (Ideal.span {1 - A}))
                ((idempotent_self_mul_part h0) ((Ideal.Quotient.mk (Ideal.span {1 - A})) C)))
          ((Ideal.Quotient.mk (Ideal.span {1 - A})) x),
        0)
Tactic:
rw [idempotent_decomp_symm_apply, idempotent_self_mul_part_map_quot, map_zero,
  add_zero, h1, map_add, idempotent_self_mul_part_map_quot, ← map_mul,
  idempotent_self_mul_part_map_quot, h1]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.final_solution
Proof state before:
case intro.intro.intro.intro.intro.refine_2
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h0 : A * A = A
h1 : C * A = C
h : good (fun x => x * x * A + C) fun x => x * A
x : R
⊢ x * A = (idempotent_decomp h0).symm.conj (Prod.map id 0) x
Tactic:
change x * A = x * A + 0 * (1 - A)
Proof state after:
case intro.intro.intro.intro.intro.refine_2
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h0 : A * A = A
h1 : C * A = C
h : good (fun x => x * x * A + C) fun x => x * A
x : R
⊢ x * A = x * A + 0 * (1 - A)
Theorem: IMOSL.IMO2011A3.final_solution
Proof state before:
case intro.intro.intro.intro.intro.refine_2
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A C : R
h0 : A * A = A
h1 : C * A = C
h : good (fun x => x * x * A + C) fun x => x * A
x : R
⊢ x * A = x * A + 0 * (1 - A)
Tactic:
rw [zero_mul, add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.final_solution
Proof state before:
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
x✝ : ∃ R₁ R₂ x x_1 φ c, f = φ.conj (Prod.map (fun x_2 => x_2 * x_2 + c) 0) ∧ g = φ.conj (Prod.map id 0)
R₁ R₂ : Type u
hR₁ : CommRing R₁
hR₂ : CommRing R₂
φ : R₁ × R₂ ≃+* R
c : R₁
h : f = φ.conj (Prod.map (fun x => x * x + c) 0)
h0 : g = φ.conj (Prod.map id 0)
⊢ good f g
Tactic:
rw [h, h0, ← good_Equiv_conj_iff]
Proof state after:
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
x✝ : ∃ R₁ R₂ x x_1 φ c, f = φ.conj (Prod.map (fun x_2 => x_2 * x_2 + c) 0) ∧ g = φ.conj (Prod.map id 0)
R₁ R₂ : Type u
hR₁ : CommRing R₁
hR₂ : CommRing R₂
φ : R₁ × R₂ ≃+* R
c : R₁
h : f = φ.conj (Prod.map (fun x => x * x + c) 0)
h0 : g = φ.conj (Prod.map id 0)
⊢ good (Prod.map (fun x => x * x + c) 0) (Prod.map id 0)
Theorem: IMOSL.IMO2011A3.final_solution
Proof state before:
R : Type u
inst✝ : CommRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
x✝ : ∃ R₁ R₂ x x_1 φ c, f = φ.conj (Prod.map (fun x_2 => x_2 * x_2 + c) 0) ∧ g = φ.conj (Prod.map id 0)
R₁ R₂ : Type u
hR₁ : CommRing R₁
hR₂ : CommRing R₂
φ : R₁ × R₂ ≃+* R
c : R₁
h : f = φ.conj (Prod.map (fun x => x * x + c) 0)
h0 : g = φ.conj (Prod.map id 0)
⊢ good (Prod.map (fun x => x * x + c) 0) (Prod.map id 0)
Tactic:
exact prod_is_good (main_answer_is_good c) zero_is_good
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_neg
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
⊢ f (-c) = f c
Tactic:
have h0 : f (c + 1) = 0 := by cases h with
| Left h => rw [h, hf.map_one, mul_zero]
| Right h => rw [add_comm, h, hf.map_one, zero_mul]
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
h0 : f (c + 1) = 0
⊢ f (-c) = f c
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_neg
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
h0 : f (c + 1) = 0
⊢ f (-c) = f c
Tactic:
have h1 := hf.is_good (c + 1) (-1)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
h0 : f (c + 1) = 0
h1 : f ((c + 1) * -1 + 1) = f (c + 1) * f (-1) + f (c + 1 + -1)
⊢ f (-c) = f c
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_neg
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
h0 : f (c + 1) = 0
h1 : f ((c + 1) * -1 + 1) = f (c + 1) * f (-1) + f (c + 1 + -1)
⊢ f (-c) = f c
Tactic:
rwa [h0, zero_mul, zero_add, add_neg_cancel_right,
  mul_neg_one, neg_add_rev, neg_add_cancel_comm] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_neg
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
⊢ f (c + 1) = 0
Tactic:
cases h with
| Left h => rw [h, hf.map_one, mul_zero]
| Right h => rw [add_comm, h, hf.map_one, zero_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_neg
Proof state before:
case Left
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : ∀ (x : R), f (c + x) = -f c * f x
⊢ f (c + 1) = 0
Tactic:
rw [h, hf.map_one, mul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_neg
Proof state before:
case Right
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing 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) = 0
Tactic:
rw [add_comm, h, hf.map_one, zero_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_mul_self_eq_one
Proof state before:
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
h0 : f (-c) = f c
⊢ f 0 = -(f c * f c)
Tactic:
cases h with
| Left h => specialize h (-c); rwa [add_neg_self, h0, neg_mul] at h
| Right h => specialize h (-c); rwa [neg_add_self, h0, mul_neg] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_mul_self_eq_one
Proof state before:
case Left
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h0 : f (-c) = f c
h : ∀ (x : R), f (c + x) = -f c * f x
⊢ f 0 = -(f c * f c)
Tactic:
specialize h (-c)
Proof state after:
case Left
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h0 : f (-c) = f c
h : f (c + -c) = -f c * f (-c)
⊢ f 0 = -(f c * f c)
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_mul_self_eq_one
Proof state before:
case Left
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h0 : f (-c) = f c
h : f (c + -c) = -f c * f (-c)
⊢ f 0 = -(f c * f c)
Tactic:
rwa [add_neg_self, h0, neg_mul] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_mul_self_eq_one
Proof state before:
case Right
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h0 : f (-c) = f c
h : ∀ (x : R), f (x + c) = f x * -f c
⊢ f 0 = -(f c * f c)
Tactic:
specialize h (-c)
Proof state after:
case Right
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h0 : f (-c) = f c
h : f (-c + c) = f (-c) * -f c
⊢ f 0 = -(f c * f c)
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_mul_self_eq_one
Proof state before:
case Right
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h0 : f (-c) = f c
h : f (-c + c) = f (-c) * -f c
⊢ f 0 = -(f c * f c)
Tactic:
rwa [neg_add_self, h0, mul_neg] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_mul_self_eq_one
Proof state before:
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
h0 : f (-c) = f c
h1 : f 0 = -(f c * f c)
⊢ f c * f c = 1
Tactic:
rwa [hf.map_zero, neg_inj, eq_comm] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_commute
Proof state before:
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
x : R
⊢ Commute (-f c) (f x)
Tactic:
cases map_eq_one_or_neg_one hf h with
| inl h => rw [h]; exact Commute.neg_one_left (f x)
| inr h => rw [h, neg_neg]; exact Commute.one_left (f x)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_commute
Proof state before:
case inl
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h✝ : QuasiPeriodic f c
x : R
h : f c = 1
⊢ Commute (-f c) (f x)
Tactic:
rw [h]
Proof state after:
case inl
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h✝ : QuasiPeriodic f c
x : R
h : f c = 1
⊢ Commute (-1) (f x)
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_commute
Proof state before:
case inl
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h✝ : QuasiPeriodic f c
x : R
h : f c = 1
⊢ Commute (-1) (f x)
Tactic:
exact Commute.neg_one_left (f x)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_commute
Proof state before:
case inr
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h✝ : QuasiPeriodic f c
x : R
h : f c = -1
⊢ Commute (-f c) (f x)
Tactic:
rw [h, neg_neg]
Proof state after:
case inr
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h✝ : QuasiPeriodic f c
x : R
h : f c = -1
⊢ Commute 1 (f x)
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.map_commute
Proof state before:
case inr
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h✝ : QuasiPeriodic f c
x : R
h : f c = -1
⊢ Commute 1 (f x)
Tactic:
exact Commute.one_left (f x)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.imp_left
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
h0 : ∀ (x : R), f (x + c) = f x * -f c
x : R
⊢ f (c + x) = -f c * f x
Tactic:
rw [add_comm, h0, map_commute hf h]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.imp_right
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
h0 : ∀ (x : R), f (c + x) = -f c * f x
x : R
⊢ f (x + c) = f x * -f c
Tactic:
rw [add_comm, h0, map_commute hf h]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.iff_left2
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
x : R
⊢ f (c + x) = -f c * f x ↔ f (c * x + 1) = 0
Tactic:
rw [neg_mul, hf.is_good, eq_neg_iff_add_eq_zero, add_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.iff_right2
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
x : R
⊢ f (x + c) = f x * -f c ↔ f (x * c + 1) = 0
Tactic:
rw [mul_neg, hf.is_good, eq_neg_iff_add_eq_zero, add_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.mul_left
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 : QuasiPeriodic f c
d : R
⊢ QuasiPeriodic f (d * c)
Tactic:
rw [iff_right2 hf] at 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 : ∀ (x : R), f (x * c + 1) = 0
d : R
⊢ ∀ (x : R), f (x * (d * c) + 1) = 0
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.mul_left
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 + 1) = 0
d : R
⊢ ∀ (x : R), f (x * (d * c) + 1) = 0
Tactic:
intro x
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 + 1) = 0
d x : R
⊢ f (x * (d * c) + 1) = 0
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.mul_left
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 + 1) = 0
d x : R
⊢ f (x * (d * c) + 1) = 0
Tactic:
rw [← mul_assoc]
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 + 1) = 0
d x : R
⊢ f (x * d * c + 1) = 0
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.mul_left
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 + 1) = 0
d x : R
⊢ f (x * d * c + 1) = 0
Tactic:
exact h (x * d)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.mul_right
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 : QuasiPeriodic f c
d : R
⊢ QuasiPeriodic f (c * d)
Tactic:
rw [iff_left2 hf] at 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 : ∀ (x : R), f (c * x + 1) = 0
d : R
⊢ ∀ (x : R), f (c * d * x + 1) = 0
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.mul_right
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 (c * x + 1) = 0
d : R
⊢ ∀ (x : R), f (c * d * x + 1) = 0
Tactic:
intro x
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 (c * x + 1) = 0
d x : R
⊢ f (c * d * x + 1) = 0