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

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

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

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

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

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

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

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

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