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

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

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

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, ?_, ?_⟩
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

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

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

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