R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1, y_1 ∈ span {x} ∧ ∃ z, z ∈ span {y} ∧ y_1 + z = 1) ↔ IsCoprime x y
R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ span {x} ⊔ span {y} = ⊤ ↔ IsCoprime x y
rw [eq_top_iff_one, Submodule.mem_sup]
case mp
R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1, y_1 ∈ span {x} ∧ ∃ z, z ∈ span {y} ∧ y_1 + z = 1) → IsCoprime x y

case mpr
R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ y_1, y_1 ∈ span {x} ∧ ∃ z, z ∈ span {y} ∧ y_1 + z = 1
R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1, y_1 ∈ span {x} ∧ ∃ z, z ∈ span {y} ∧ y_1 + z = 1) ↔ IsCoprime x y
constructor
case mp.intro.intro.intro.intro
R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y u : R
hu : u ∈ span {x}
v : R
hv : v ∈ span {y}
h1 : u + v = 1
⊢ IsCoprime x y
case mp
R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1, y_1 ∈ span {x} ∧ ∃ z, z ∈ span {y} ∧ y_1 + z = 1) → IsCoprime x y
rintro ⟨u, hu, v, hv, h1⟩
case mp.intro.intro.intro.intro
R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y u : R
hu : ∃ a, a * x = u
v : R
hv : ∃ a, a * y = v
h1 : u + v = 1
⊢ IsCoprime x y
case mp.intro.intro.intro.intro
R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y u : R
hu : u ∈ span {x}
v : R
hv : v ∈ span {y}
h1 : u + v = 1
⊢ IsCoprime x y
rw [mem_span_singleton'] at hu hv
case mp.intro.intro.intro.intro
R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y u : R
hu : ∃ a, a * x = u
v : R
hv : ∃ a, a * y = v
h1 : Exists.choose hu * x + Exists.choose hv * y = 1
⊢ IsCoprime x y
case mp.intro.intro.intro.intro
R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y u : R
hu : ∃ a, a * x = u
v : R
hv : ∃ a, a * y = v
h1 : u + v = 1
⊢ IsCoprime x y
rw [← hu.choose_spec, ← hv.choose_spec] at h1
no goals
case mp.intro.intro.intro.intro
R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y u : R
hu : ∃ a, a * x = u
v : R
hv : ∃ a, a * y = v
h1 : Exists.choose hu * x + Exists.choose hv * y = 1
⊢ IsCoprime x y
exact ⟨_, _, h1⟩
no goals
case mpr
R✝ : Type u
ι : Type ?u.257363
inst✝¹ : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ y_1, y_1 ∈ span {x} ∧ ∃ z, z ∈ span {y} ∧ y_1 + z = 1
exact fun ⟨u, v, h1⟩ =>
  ⟨_, mem_span_singleton'.mpr ⟨_, rfl⟩, _, mem_span_singleton'.mpr ⟨_, rfl⟩, h1⟩