case mk.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Submodule.span R {d}
⊢ Ideal.span {gcd x y} = Ideal.span {x, y}
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
⊢ Ideal.span {gcd x y} = Ideal.span {x, y}
obtain ⟨d, hd⟩ := IsPrincipalIdealRing.principal (span ({x, y} : Set R))
case mk.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ Ideal.span {gcd x y} = Ideal.span {x, y}
case mk.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Submodule.span R {d}
⊢ Ideal.span {gcd x y} = Ideal.span {x, y}
rw [submodule_span_eq] at hd
case mk.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ Ideal.span {gcd x y} = Ideal.span {d}
case mk.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ Ideal.span {gcd x y} = Ideal.span {x, y}
rw [hd]
case mk.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ Associated d (gcd x y)
case mk.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ Ideal.span {gcd x y} = Ideal.span {d}
suffices Associated d (gcd x y) by
  obtain ⟨D, HD⟩ := this
  rw [← HD]
  exact span_singleton_mul_right_unit D.isUnit _
case mk.intro.hab
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ d ∣ gcd x y

case mk.intro.hba
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ gcd x y ∣ d
case mk.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ Associated d (gcd x y)
apply associated_of_dvd_dvd
case intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
D : Rˣ
HD : d * ↑D = gcd x y
⊢ Ideal.span {gcd x y} = Ideal.span {d}
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
this : Associated d (gcd x y)
⊢ Ideal.span {gcd x y} = Ideal.span {d}
obtain ⟨D, HD⟩ := this
case intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
D : Rˣ
HD : d * ↑D = gcd x y
⊢ Ideal.span {d * ↑D} = Ideal.span {d}
case intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
D : Rˣ
HD : d * ↑D = gcd x y
⊢ Ideal.span {gcd x y} = Ideal.span {d}
rw [← HD]
no goals
case intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
D : Rˣ
HD : d * ↑D = gcd x y
⊢ Ideal.span {d * ↑D} = Ideal.span {d}
exact span_singleton_mul_right_unit D.isUnit _
case mk.intro.hab
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ d ∣ x ∧ d ∣ y
case mk.intro.hab
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ d ∣ gcd x y
rw [dvd_gcd_iff]
case mk.intro.hab.left
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ ∃ a b, a * x + b * y = x

case mk.intro.hab.right
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ ∃ a b, a * x + b * y = y
case mk.intro.hab
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ d ∣ x ∧ d ∣ y
constructor <;> rw [← Ideal.mem_span_singleton, ← hd, Ideal.mem_span_pair]
case mk.intro.hab.left
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ 1 * x + 0 * y = x
case mk.intro.hab.left
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ ∃ a b, a * x + b * y = x
use 1, 0
no goals
case mk.intro.hab.left
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ 1 * x + 0 * y = x
rw [one_mul, MulZeroClass.zero_mul, add_zero]
case mk.intro.hab.right
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ 0 * x + 1 * y = y
case mk.intro.hab.right
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ ∃ a b, a * x + b * y = y
use 0, 1
no goals
case mk.intro.hab.right
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ 0 * x + 1 * y = y
rw [one_mul, MulZeroClass.zero_mul, zero_add]
case mk.intro.hba.intro.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y r s : R
hd : Ideal.span {x, y} = Ideal.span {r * x + s * y}
⊢ gcd x y ∣ r * x + s * y
case mk.intro.hba
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ gcd x y ∣ d
obtain ⟨r, s, rfl⟩ : ∃ r s, r * x + s * y = d := by
  rw [← Ideal.mem_span_pair, hd, Ideal.mem_span_singleton]
case mk.intro.hba.intro.intro.h₁.h
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y r s : R
hd : Ideal.span {x, y} = Ideal.span {r * x + s * y}
⊢ gcd x y ∣ x

case mk.intro.hba.intro.intro.h₂.h
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y r s : R
hd : Ideal.span {x, y} = Ideal.span {r * x + s * y}
⊢ gcd x y ∣ y
case mk.intro.hba.intro.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y r s : R
hd : Ideal.span {x, y} = Ideal.span {r * x + s * y}
⊢ gcd x y ∣ r * x + s * y
apply dvd_add <;> apply dvd_mul_of_dvd_right
no goals
case mk.intro.hba.intro.intro.h₁.h
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y r s : R
hd : Ideal.span {x, y} = Ideal.span {r * x + s * y}
⊢ gcd x y ∣ x

case mk.intro.hba.intro.intro.h₂.h
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y r s : R
hd : Ideal.span {x, y} = Ideal.span {r * x + s * y}
⊢ gcd x y ∣ y
exacts [gcd_dvd_left x y, gcd_dvd_right x y]
no goals
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ ∃ r s, r * x + s * y = d
rw [← Ideal.mem_span_pair, hd, Ideal.mem_span_singleton]