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

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

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

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

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

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

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

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

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