Theorem: IMOSL.IMO2012N1.final_solution (IMOSLLean4/IMO2012/N1/N1.lean)

State before:
R : Type u_1
inst✝ : CommRing R
x y : R
h : ∀ (A : Set R), admissible A → x ∈ A → y ∈ A → ∀ (z : R), z ∈ A
⊢ IsCoprime x y
Tactic:
specialize h (Ideal.span {x, y}) (admissible_ideal _)
  (Ideal.subset_span (Set.mem_insert x _))
  (Ideal.subset_span (Set.mem_insert_of_mem x rfl)) 1
State after:
R : Type u_1
inst✝ : CommRing R
x y : R
h : 1 ∈ ↑(Ideal.span {x, y})
⊢ IsCoprime x y

State before:
R : Type u_1
inst✝ : CommRing R
x y : R
h : 1 ∈ ↑(Ideal.span {x, y})
⊢ IsCoprime x y
Tactic:
rwa [SetLike.mem_coe, Ideal.mem_span_pair] at h
State after:
no goals

State before:
R : Type u_1
inst✝ : CommRing R
x y : R
h : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
⊢ ∀ (z : R), z ∈ A
Tactic:
suffices 1 ∈ A from λ z ↦ mul_one z ▸
  one_pow (M := R) 2 ▸ admissible_mem_sq_mul h0 this z
State after:
R : Type u_1
inst✝ : CommRing R
x y : R
h : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
⊢ 1 ∈ A

State before:
R : Type u_1
inst✝ : CommRing R
x y : R
h : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
⊢ 1 ∈ A
Tactic:
obtain ⟨a, b, h⟩ : IsCoprime (x ^ 2) (y ^ 2) := IsCoprime.pow h
State after:
case intro.intro
R : Type u_1
inst✝ : CommRing R
x y : R
h✝ : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
a b : R
h : a * x ^ 2 + b * y ^ 2 = 1
⊢ 1 ∈ A

State before:
case intro.intro
R : Type u_1
inst✝ : CommRing R
x y : R
h✝ : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
a b : R
h : a * x ^ 2 + b * y ^ 2 = 1
⊢ 1 ∈ A
Tactic:
rw [← one_pow 2, ← h]
State after:
case intro.intro
R : Type u_1
inst✝ : CommRing R
x y : R
h✝ : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
a b : R
h : a * x ^ 2 + b * y ^ 2 = 1
⊢ (a * x ^ 2 + b * y ^ 2) ^ 2 ∈ A

State before:
case intro.intro
R : Type u_1
inst✝ : CommRing R
x y : R
h✝ : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
a b : R
h : a * x ^ 2 + b * y ^ 2 = 1
⊢ (a * x ^ 2 + b * y ^ 2) ^ 2 ∈ A
Tactic:
refine admissible_add_sq h0 (admissible_mem_sq_mul h0 h1 a)
  (admissible_mem_sq_mul h0 h2 b)
State after:
no goals