R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ LocalRing R ∧ IsBezout R → ValuationRing R
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ValuationRing R ↔ LocalRing R ∧ IsBezout R
refine ⟨fun H => ⟨inferInstance, inferInstance⟩, ?_⟩
case intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
⊢ ValuationRing R
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ LocalRing R ∧ IsBezout R → ValuationRing R
rintro ⟨h₁, h₂⟩
case intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
a b : R
⊢ a ∣ b ∨ b ∣ a
case intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
⊢ ValuationRing R
refine iff_dvd_total.mpr ⟨fun a b => ?_⟩
case intro.mk.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
a b g : R
e : Ideal.span {a, b} = Ideal.span {g}
⊢ a ∣ b ∨ b ∣ a
case intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
a b : R
⊢ a ∣ b ∨ b ∣ a
obtain ⟨g, e : _ = Ideal.span _⟩ := IsBezout.span_pair_isPrincipal a b
case intro.mk.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
b g a : R
e : Ideal.span {a * g, b} = Ideal.span {g}
⊢ a * g ∣ b ∨ b ∣ a * g
case intro.mk.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
a b g : R
e : Ideal.span {a, b} = Ideal.span {g}
⊢ a ∣ b ∨ b ∣ a
obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp
    (show a ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
case intro.mk.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
case intro.mk.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
b g a : R
e : Ideal.span {a * g, b} = Ideal.span {g}
⊢ a * g ∣ b ∨ b ∣ a * g
obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.mp
    (show b ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
case intro.mk.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
case intro.mk.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
obtain ⟨x, y, e'⟩ := Ideal.mem_span_pair.mp
    (show g ∈ Ideal.span {a * g, b * g} by rw [e]; exact Ideal.subset_span (by simp))
case intro.mk.intro.intro.intro.intro.intro.inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g = 0
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

case intro.mk.intro.intro.intro.intro.intro.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
case intro.mk.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
cases' eq_or_ne g 0 with h h
case intro.mk.intro.intro.intro.intro.intro.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
case intro.mk.intro.intro.intro.intro.intro.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
have : x * a + y * b = 1 := by
  apply mul_left_injective₀ h; convert e' using 1 <;> ring
case intro.mk.intro.intro.intro.intro.intro.inr.inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (x * a)
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

case intro.mk.intro.intro.intro.intro.intro.inr.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
case intro.mk.intro.intro.intro.intro.intro.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
cases' LocalRing.isUnit_or_isUnit_of_add_one this with h' h'
case intro.mk.intro.intro.intro.intro.intro.inr.inl.h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (x * a)
⊢ a * g ∣ b * g

case intro.mk.intro.intro.intro.intro.intro.inr.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
case intro.mk.intro.intro.intro.intro.intro.inr.inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (x * a)
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

case intro.mk.intro.intro.intro.intro.intro.inr.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
left
case intro.mk.intro.intro.intro.intro.intro.inr.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

case intro.mk.intro.intro.intro.intro.intro.inr.inl.h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (x * a)
⊢ a * g ∣ b * g
case intro.mk.intro.intro.intro.intro.intro.inr.inl.h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (x * a)
⊢ a * g ∣ b * g

case intro.mk.intro.intro.intro.intro.intro.inr.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
swap
case intro.mk.intro.intro.intro.intro.intro.inr.inr.h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ b * g ∣ a * g

case intro.mk.intro.intro.intro.intro.intro.inr.inl.h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (x * a)
⊢ a * g ∣ b * g
case intro.mk.intro.intro.intro.intro.intro.inr.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

case intro.mk.intro.intro.intro.intro.intro.inr.inl.h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (x * a)
⊢ a * g ∣ b * g
right
no goals
case intro.mk.intro.intro.intro.intro.intro.inr.inr.h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ b * g ∣ a * g

case intro.mk.intro.intro.intro.intro.intro.inr.inl.h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (x * a)
⊢ a * g ∣ b * g
all_goals exact mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
a b g : R
e : Ideal.span {a, b} = Ideal.span {g}
⊢ a ∈ Ideal.span {a, b}
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
a b g : R
e : Ideal.span {a, b} = Ideal.span {g}
⊢ a ∈ Ideal.span {g}
rw [← e]
no goals
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
a b g : R
e : Ideal.span {a, b} = Ideal.span {g}
⊢ a ∈ Ideal.span {a, b}
exact Ideal.subset_span (by simp)
no goals
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
a b g : R
e : Ideal.span {a, b} = Ideal.span {g}
⊢ a ∈ {a, b}
simp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
b g a : R
e : Ideal.span {a * g, b} = Ideal.span {g}
⊢ b ∈ Ideal.span {a * g, b}
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
b g a : R
e : Ideal.span {a * g, b} = Ideal.span {g}
⊢ b ∈ Ideal.span {g}
rw [← e]
no goals
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
b g a : R
e : Ideal.span {a * g, b} = Ideal.span {g}
⊢ b ∈ Ideal.span {a * g, b}
exact Ideal.subset_span (by simp)
no goals
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
b g a : R
e : Ideal.span {a * g, b} = Ideal.span {g}
⊢ b ∈ {a * g, b}
simp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
⊢ g ∈ Ideal.span {g}
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
⊢ g ∈ Ideal.span {a * g, b * g}
rw [e]
no goals
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
⊢ g ∈ Ideal.span {g}
exact Ideal.subset_span (by simp)
no goals
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
⊢ g ∈ {g}
simp
no goals
case intro.mk.intro.intro.intro.intro.intro.inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g = 0
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
simp [h]
case a
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ (fun a => a * g) (x * a + y * b) = (fun a => a * g) 1
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ x * a + y * b = 1
apply mul_left_injective₀ h
no goals
case a
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ (fun a => a * g) (x * a + y * b) = (fun a => a * g) 1
convert e' using 1 <;> ring
no goals
case intro.mk.intro.intro.intro.intro.intro.inr.inl.h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.591460
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h₁ : LocalRing R
h₂ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (x * a)
⊢ a * g ∣ b * g
exact mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _