internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2017A4.max_two_nsmul_b_and_c_bdd
Proof state before:
case inr
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : b n < c n - b n
h7 : c (n + 1) = c D
⊢ max (b n) (c n - b n) ≤ c D - b D
Tactic:
rw [max_eq_right h6.le, ← h7]
Proof state after:
case inr
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : b n < c n - b n
h7 : c (n + 1) = c D
⊢ c n - b n ≤ c (n + 1) - b D
Theorem: IMOSL.IMO2017A4.max_two_nsmul_b_and_c_bdd
Proof state before:
case inr
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : b n < c n - b n
h7 : c (n + 1) = c D
⊢ c n - b n ≤ c (n + 1) - b D
Tactic:
exact sub_le_sub (h2 n.le_succ) (h1 h4)
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.main_answer_is_good
Proof state before:
R : Type u_1
inst✝ : NonUnitalCommRing R
C x y : R
⊢ id ((fun x => x * x + C) (x + y)) = (fun x => x * x + C) x + (2 • x + y) * id y
Tactic:
rw [id, id, add_right_comm, add_left_inj, two_nsmul, mul_add,
  add_mul, mul_comm y, add_assoc, ← add_mul, add_assoc]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.good_Equiv_conj_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
⊢ ∀ {x y : R},
    g (f (x + y)) = f x + (2 • x + y) * g y ↔
      φ.conj g (φ.conj f (φ.toEquiv x + φ.toEquiv y)) =
        φ.conj f (φ.toEquiv x) + (2 • φ.toEquiv x + φ.toEquiv y) * φ.conj g (φ.toEquiv y)
Tactic:
have X (z : R) : φ.toEquiv z = (φ : R ≃+* S) z := rfl
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
⊢ ∀ {x y : R},
    g (f (x + y)) = f x + (2 • x + y) * g y ↔
      φ.conj g (φ.conj f (φ.toEquiv x + φ.toEquiv y)) =
        φ.conj f (φ.toEquiv x) + (2 • φ.toEquiv x + φ.toEquiv y) * φ.conj g (φ.toEquiv y)
Theorem: IMOSL.IMO2011A3.good_Equiv_conj_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
⊢ ∀ {x y : R},
    g (f (x + y)) = f x + (2 • x + y) * g y ↔
      φ.conj g (φ.conj f (φ.toEquiv x + φ.toEquiv y)) =
        φ.conj f (φ.toEquiv x) + (2 • φ.toEquiv x + φ.toEquiv y) * φ.conj g (φ.toEquiv y)
Tactic:
intro x y
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔
    φ.conj g (φ.conj f (φ.toEquiv x + φ.toEquiv y)) =
      φ.conj f (φ.toEquiv x) + (2 • φ.toEquiv x + φ.toEquiv y) * φ.conj g (φ.toEquiv y)
Theorem: IMOSL.IMO2011A3.good_Equiv_conj_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔
    φ.conj g (φ.conj f (φ.toEquiv x + φ.toEquiv y)) =
      φ.conj f (φ.toEquiv x) + (2 • φ.toEquiv x + φ.toEquiv y) * φ.conj g (φ.toEquiv y)
Tactic:
simp only [φ.conj_apply, X]
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔
    φ (g (φ.symm (φ (f (φ.symm (φ x + φ y)))))) = φ (f (φ.symm (φ x))) + (2 • φ x + φ y) * φ (g (φ.symm (φ y)))
Theorem: IMOSL.IMO2011A3.good_Equiv_conj_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔
    φ (g (φ.symm (φ (f (φ.symm (φ x + φ y)))))) = φ (f (φ.symm (φ x))) + (2 • φ x + φ y) * φ (g (φ.symm (φ y)))
Tactic:
rw [← φ.map_add, ← map_nsmul, ← φ.map_add]
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔
    φ (g (φ.symm (φ (f (φ.symm (φ (x + y))))))) = φ (f (φ.symm (φ x))) + φ (2 • x + y) * φ (g (φ.symm (φ y)))
Theorem: IMOSL.IMO2011A3.good_Equiv_conj_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔
    φ (g (φ.symm (φ (f (φ.symm (φ (x + y))))))) = φ (f (φ.symm (φ x))) + φ (2 • x + y) * φ (g (φ.symm (φ y)))
Tactic:
simp only [φ.toEquiv_eq_coe, EquivLike.coe_symm_apply_apply]
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔ φ (g (f (x + y))) = φ (f x) + φ (2 • x + y) * φ (g y)
Theorem: IMOSL.IMO2011A3.good_Equiv_conj_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔ φ (g (f (x + y))) = φ (f x) + φ (2 • x + y) * φ (g y)
Tactic:
rw [← φ.map_mul, ← φ.map_add]
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔ φ (g (f (x + y))) = φ (f x + (2 • x + y) * g y)
Theorem: IMOSL.IMO2011A3.good_Equiv_conj_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔ φ (g (f (x + y))) = φ (f x + (2 • x + y) * g y)
Tactic:
exact φ.apply_eq_iff_eq.symm
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.step1_1
Proof state before:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
f g : R → R
h : good f g
x y : R
⊢ f x - x * g x - (f y - y * g y) = 2 • (y * g x - x * g y)
Tactic:
rw [nsmul_sub, sub_eq_sub_iff_add_eq_add, ← add_sub_right_comm, ← add_sub_assoc,
  sub_eq_sub_iff_add_eq_add, two_nsmul, ← add_mul, add_assoc, ← add_mul,
  ← two_nsmul, ← h, add_comm _ (f y), add_assoc, two_nsmul, ← add_mul,
  ← add_mul, ← two_nsmul, ← h, add_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.step1
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
⊢ ∃ A B C, (f = fun x => x * (x * A) - x * B + C) ∧ g = fun x => x * A + B
Tactic:
obtain ⟨A, h0⟩ : ∃ A, ∀ x, g x = x * A + g 0 := ⟨g 1 - g 0, λ x ↦ by
  have h0 : _ + _ = _ + _ := congrArg₂ _ (step1_1 h x 1) (step1_1 h 1 0)
  rw [sub_add_sub_cancel, step1_1 h, ← nsmul_add] at h0
  replace h0 := hR _ _ h0
  rwa [zero_mul, zero_sub, one_mul, zero_mul, one_mul, zero_sub, eq_add_neg_iff_add_eq,
    eq_sub_iff_add_eq', ← add_assoc, ← sub_eq_add_neg, ← mul_sub, eq_comm] at h0⟩
Proof state after:
case intro
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
A : R
h0 : ∀ (x : R), g x = x * A + g 0
⊢ ∃ A B C, (f = fun x => x * (x * A) - x * B + C) ∧ g = fun x => x * A + B
Theorem: IMOSL.IMO2011A3.step1
Proof state before:
case intro
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
A : R
h0 : ∀ (x : R), g x = x * A + g 0
⊢ ∃ A B C, (f = fun x => x * (x * A) - x * B + C) ∧ g = fun x => x * A + B
Tactic:
refine ⟨A, g 0, f 0, funext λ x ↦ ?_, funext h0⟩
Proof state after:
case intro
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
A : R
h0 : ∀ (x : R), g x = x * A + g 0
x : R
⊢ f x = x * (x * A) - x * g 0 + f 0
Theorem: IMOSL.IMO2011A3.step1
Proof state before:
case intro
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
A : R
h0 : ∀ (x : R), g x = x * A + g 0
x : R
⊢ f x = x * (x * A) - x * g 0 + f 0
Tactic:
have h1 := step1_1 h x 0
Proof state after:
case intro
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
A : R
h0 : ∀ (x : R), g x = x * A + g 0
x : R
h1 : f x - x * g x - (f 0 - 0 * g 0) = 2 • (0 * g x - x * g 0)
⊢ f x = x * (x * A) - x * g 0 + f 0
Theorem: IMOSL.IMO2011A3.step1
Proof state before:
case intro
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
A : R
h0 : ∀ (x : R), g x = x * A + g 0
x : R
h1 : f x - x * g x - (f 0 - 0 * g 0) = 2 • (0 * g x - x * g 0)
⊢ f x = x * (x * A) - x * g 0 + f 0
Tactic:
rwa [zero_mul, sub_zero, zero_mul, zero_sub, sub_eq_iff_eq_add,
  sub_eq_iff_eq_add', h0, mul_add, two_nsmul, add_assoc _ _ (f 0),
  add_add_add_comm, add_neg_cancel_left, ← sub_eq_add_neg] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.step1
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
x : R
⊢ g x = x * (g 1 - g 0) + g 0
Tactic:
have h0 : _ + _ = _ + _ := congrArg₂ _ (step1_1 h x 1) (step1_1 h 1 0)
Proof state after:
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
x : R
h0 :
  f x - x * g x - (f 1 - 1 * g 1) + (f 1 - 1 * g 1 - (f 0 - 0 * g 0)) =
    2 • (1 * g x - x * g 1) + 2 • (0 * g 1 - 1 * g 0)
⊢ g x = x * (g 1 - g 0) + g 0
Theorem: IMOSL.IMO2011A3.step1
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
x : R
h0 :
  f x - x * g x - (f 1 - 1 * g 1) + (f 1 - 1 * g 1 - (f 0 - 0 * g 0)) =
    2 • (1 * g x - x * g 1) + 2 • (0 * g 1 - 1 * g 0)
⊢ g x = x * (g 1 - g 0) + g 0
Tactic:
rw [sub_add_sub_cancel, step1_1 h, ← nsmul_add] at h0
Proof state after:
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
x : R
h0 : 2 • (0 * g x - x * g 0) = 2 • (1 * g x - x * g 1 + (0 * g 1 - 1 * g 0))
⊢ g x = x * (g 1 - g 0) + g 0
Theorem: IMOSL.IMO2011A3.step1
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
x : R
h0 : 2 • (0 * g x - x * g 0) = 2 • (1 * g x - x * g 1 + (0 * g 1 - 1 * g 0))
⊢ g x = x * (g 1 - g 0) + g 0
Tactic:
replace h0 := hR _ _ h0
Proof state after:
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
x : R
h0 : 0 * g x - x * g 0 = 1 * g x - x * g 1 + (0 * g 1 - 1 * g 0)
⊢ g x = x * (g 1 - g 0) + g 0
Theorem: IMOSL.IMO2011A3.step1
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
x : R
h0 : 0 * g x - x * g 0 = 1 * g x - x * g 1 + (0 * g 1 - 1 * g 0)
⊢ g x = x * (g 1 - g 0) + g 0
Tactic:
rwa [zero_mul, zero_sub, one_mul, zero_mul, one_mul, zero_sub, eq_add_neg_iff_add_eq,
  eq_sub_iff_add_eq', ← add_assoc, ← sub_eq_add_neg, ← mul_sub, eq_comm] at h0
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
have h0 (x) : (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C := by
  specialize h x (-(2 • x)); simp only at h
  rwa [add_right_neg, zero_mul, add_zero, two_nsmul, neg_add, add_neg_cancel_comm_assoc,
    neg_mul x A, neg_mul_neg, neg_mul, sub_neg_eq_add] at h
Proof state after:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
have h1 := h0 0
Proof state after:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : (0 * (0 * A) + 0 * B + C) * A + B = 0 * (0 * A) - 0 * B + C
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : (0 * (0 * A) + 0 * B + C) * A + B = 0 * (0 * A) - 0 * B + C
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
rw [zero_mul, zero_mul, zero_add, sub_zero, zero_add] at h1
Proof state after:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
have h2 := h0 1
Proof state after:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : (1 * (1 * A) + 1 * B + C) * A + B = 1 * (1 * A) - 1 * B + C
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : (1 * (1 * A) + 1 * B + C) * A + B = 1 * (1 * A) - 1 * B + C
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
rw [one_mul, one_mul, one_mul, add_mul, add_assoc, h1, add_left_inj] at h2
Proof state after:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : (A + B) * A = A - B
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : (A + B) * A = A - B
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
have h3 := h0 (-1)
Proof state after:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : (A + B) * A = A - B
h3 : (-1 * (-1 * A) + -1 * B + C) * A + B = -1 * (-1 * A) - -1 * B + C
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : (A + B) * A = A - B
h3 : (-1 * (-1 * A) + -1 * B + C) * A + B = -1 * (-1 * A) - -1 * B + C
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
rw [neg_one_mul, neg_one_mul, neg_one_mul, neg_neg,
← sub_eq_add_neg, sub_neg_eq_add, add_mul, add_assoc, h1, add_left_inj] at h3
Proof state after:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : (A + B) * A = A - B
h3 : (A - B) * A = A + B
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : (A + B) * A = A - B
h3 : (A + B) * A - (A - B) * A = A - B - (A + B)
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
rw [← sub_mul, add_sub_sub_cancel, add_mul, ← two_nsmul, ← sub_sub,
  sub_sub_cancel_left, sub_eq_add_neg, ← two_nsmul] at h3
Proof state after:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : (A + B) * A = A - B
h3 : 2 • (B * A) = 2 • -B
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : (A + B) * A = A - B
h3 : 2 • (B * A) = 2 • -B
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
replace h3 := hR _ _ h3
Proof state after:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : (A + B) * A = A - B
h3 : B * A = -B
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : (A + B) * A = A - B
h3 : B * A = -B
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
rw [add_mul, h3, sub_eq_add_neg, add_left_inj] at h2
Proof state after:
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
h0 : ∀ (x : R), (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
h1 : C * A + B = C
h2 : A * A = A
h3 : B * A = -B
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
h1 : C * A + B = C
h2 : A * A = A
h3 : B * A = -B
h0 : (C * A + B) * A = C * A
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
rw [add_mul, mul_assoc, h2, add_right_eq_self, h3, neg_eq_zero] at h0
Proof state after:
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
h1 : C * A + B = C
h2 : A * A = A
h3 : B * A = -B
h0 : B = 0
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
h1 : C * A + B = C
h2 : A * A = A
h3 : B * A = -B
h0 : B = 0
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
rw [h0, add_zero] at h1
Proof state after:
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
h1 : C * A = C
h2 : A * A = A
h3 : B * A = -B
h0 : B = 0
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
h1 : C * A = C
h2 : A * A = A
h3 : B * A = -B
h0 : B = 0
⊢ B = 0 ∧ A * A = A ∧ C * A = C
Tactic:
exact ⟨h0, h2, h1⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
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
x : R
⊢ (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
Tactic:
specialize h x (-(2 • x))
Proof state after:
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A B C x : R
h :
  (fun x => x * A + B) ((fun x => x * (x * A) - x * B + C) (x + -(2 • x))) =
    (fun x => x * (x * A) - x * B + C) x + (2 • x + -(2 • x)) * (fun x => x * A + B) (-(2 • x))
⊢ (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A B C x : R
h :
  (fun x => x * A + B) ((fun x => x * (x * A) - x * B + C) (x + -(2 • x))) =
    (fun x => x * (x * A) - x * B + C) x + (2 • x + -(2 • x)) * (fun x => x * A + B) (-(2 • x))
⊢ (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
Tactic:
simp only at h
Proof state after:
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A B C x : R
h :
  ((x + -(2 • x)) * ((x + -(2 • x)) * A) - (x + -(2 • x)) * B + C) * A + B =
    x * (x * A) - x * B + C + (2 • x + -(2 • x)) * (-(2 • x) * A + B)
⊢ (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
Theorem: IMOSL.IMO2011A3.step2
Proof state before:
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
A B C x : R
h :
  ((x + -(2 • x)) * ((x + -(2 • x)) * A) - (x + -(2 • x)) * B + C) * A + B =
    x * (x * A) - x * B + C + (2 • x + -(2 • x)) * (-(2 • x) * A + B)
⊢ (x * (x * A) + x * B + C) * A + B = x * (x * A) - x * B + C
Tactic:
rwa [add_right_neg, zero_mul, add_zero, two_nsmul, neg_add, add_neg_cancel_comm_assoc,
  neg_mul x A, neg_mul_neg, neg_mul, sub_neg_eq_add] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2011A3.relation_summary
Proof state before:
R : Type u_1
inst✝ : Ring R
hR : ∀ (x y : R), 2 • x = 2 • y → x = y
f g : R → R
h : good f g
⊢ ∃ A C, A * A = A ∧ C * A = C ∧ (f = fun x => x * x * A + C) ∧ g = fun x => x * A
Tactic:
rcases step1 hR h with ⟨A, B, C, rfl, rfl⟩
Proof state after:
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