Theorem: IMOSL.IMO2011A3.step2 (IMOSLLean4/IMO2011/A3/A3.lean)

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
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

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
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

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
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

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
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

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
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

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)
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

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
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

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
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

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
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

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
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

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
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

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
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

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⟩
State after:
no goals

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))
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

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
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

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
State after:
no goals