awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
⊢ IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
have rw : ∀ (hinv : (↑(↑I : FractionalIdeal S A) : Submodule R A) * (↑(↑I⁻¹ : FractionalIdeal S A) : Submodule R A) = 1),
  let J := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v));
  ∀ (h : J = ⊤), IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
Tactic: rw [coe_ext_iff, coe_mul, coe_one] at hinv
Cleared hypotheses: hinv, J, h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑(↑I : FractionalIdeal S A) : Submodule R A) * (↑(↑I⁻¹ : FractionalIdeal S A) : Submodule R A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
⊢ IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
have h₁ : (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v) ≤ LinearMap.range (Algebra.linearMap R A)
Tactic: apply Submodule.map_comap_eq_self
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑(↑I : FractionalIdeal S A) : Submodule R A) * (↑(↑I⁻¹ : FractionalIdeal S A) : Submodule R A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
⊢ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v) ≤ LinearMap.range (Algebra.linearMap R A)
have h₁ : (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v) ≤ 1
Tactic: grw [← Submodule.one_eq_range, ← hinv, (Submodule.span_singleton_le_iff_mem _ _).2 hv]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑(↑I : FractionalIdeal S A) : Submodule R A) * (↑(↑I⁻¹ : FractionalIdeal S A) : Submodule R A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
h₁ : (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v) ≤ 1
⊢ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v) ≤ LinearMap.range (Algebra.linearMap R A)
have h₂ : (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v) ≤
  (↑(↑I : FractionalIdeal S A) : Submodule R A) * (↑(↑I⁻¹ : FractionalIdeal S A) : Submodule R A)
Tactic: grw [← Submodule.one_eq_range, ← hinv, (Submodule.span_singleton_le_iff_mem _ _).2 hv]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑(↑I : FractionalIdeal S A) : Submodule R A) * (↑(↑I⁻¹ : FractionalIdeal S A) : Submodule R A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
h₁ : (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v) ≤ 1
h₂ :
  (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v) ≤
    (↑(↑I : FractionalIdeal S A) : Submodule R A) * (↑(↑I⁻¹ : FractionalIdeal S A) : Submodule R A)
⊢ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v) ≤ LinearMap.range (Algebra.linearMap R A)
have h₃ : (↑(↑I : FractionalIdeal S A) : Submodule R A) * (↑(↑I⁻¹ : FractionalIdeal S A) : Submodule R A) ≤
  (↑(↑I : FractionalIdeal S A) : Submodule R A) * (↑(↑I⁻¹ : FractionalIdeal S A) : Submodule R A)
Tactic: grw [← Submodule.one_eq_range, ← hinv, (Submodule.span_singleton_le_iff_mem _ _).2 hv]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
⊢ (↑(↑I : FractionalIdeal S A) : Submodule R A).IsPrincipal
have hJ : IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
Tactic: have hJ : IsLocalization.coeSubmodule A J = ↑I * Submodule.span R {v} := by
    rw [coe_ext_iff, coe_mul, coe_one] at hinv
    apply Submodule.map_comap_eq_self
    grw [← Submodule.one_eq_range, ← hinv, (Submodule.span_singleton_le_iff_mem _ _).2 hv]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
⊢ 1 ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
have rw : ∃ (y : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) y : A) (1 : A)
Tactic: rw [← hJ, h, IsLocalization.coeSubmodule_top, Submodule.mem_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
⊢ (↑(↑I : FractionalIdeal S A) : Submodule R A).IsPrincipal
have this : 1 ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
Tactic: have : (1 : A) ∈ ↑I * Submodule.span R {v} := by
    rw [← hJ, h, IsLocalization.coeSubmodule_top, Submodule.mem_one]
    exact ⟨1, (algebraMap R _).map_one⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
this : 1 ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
⊢ (↑(↑I : FractionalIdeal S A) : Submodule R A).IsPrincipal
have obtain : ∀ (w : A) (hw : w ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A)) (hvw : w * v = 1),
  (↑(↑I : FractionalIdeal S A) : Submodule R A).IsPrincipal
Tactic: obtain ⟨w, hw, hvw⟩ := Submodule.mem_mul_span_singleton.1 this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
this : 1 ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
w : A
hw : w ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A)
hvw : w * v = 1
⊢ (↑(↑I : FractionalIdeal S A) : Submodule R A).IsPrincipal
have refine : (↑(↑I : FractionalIdeal S A) : Submodule R A) = R ∙ w
Tactic: refine ⟨⟨w, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
this : 1 ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
w : A
hw : w ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A)
hvw : w * v = 1
⊢ (↑(↑I : FractionalIdeal S A) : Submodule R A) = R ∙ w
have rw : (↑(spanSingleton S w) : Submodule R A) = (↑(↑I⁻¹⁻¹ : FractionalIdeal S A) : Submodule R A)
Tactic: rw [← FractionalIdeal.coe_spanSingleton S, ← inv_inv I, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
this : 1 ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
w : A
hw : w ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A)
hvw : w * v = 1
⊢ (↑(spanSingleton S w) : Submodule R A) = (↑(↑I⁻¹⁻¹ : FractionalIdeal S A) : Submodule R A)
have refine_1 : (↑I⁻¹ : FractionalIdeal S A) * spanSingleton S w ≤ 1
Tactic: refine congr_arg coeToSubmodule (Units.eq_inv_of_mul_eq_one_left (le_antisymm ?_ ?_))
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
this : 1 ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
w : A
hw : w ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A)
hvw : w * v = 1
refine_1 : (↑I⁻¹ : FractionalIdeal S A) * spanSingleton S w ≤ 1
⊢ (↑(spanSingleton S w) : Submodule R A) = (↑(↑I⁻¹⁻¹ : FractionalIdeal S A) : Submodule R A)
have refine_2 : 1 ≤ (↑I⁻¹ : FractionalIdeal S A) * spanSingleton S w
Tactic: refine congr_arg coeToSubmodule (Units.eq_inv_of_mul_eq_one_left (le_antisymm ?_ ?_))
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
this : 1 ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
w : A
hw : w ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A)
hvw : w * v = 1
| 1
have rw : (↑I⁻¹ : FractionalIdeal S A) * (↑I : FractionalIdeal S A)
Tactic: rw [← hinv, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
this : 1 ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
w : A
hw : w ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A)
hvw : w * v = 1
⊢ (↑I⁻¹ : FractionalIdeal S A) * spanSingleton S w ≤ 1
have refine_1 : (↑I⁻¹ : FractionalIdeal S A) * spanSingleton S w ≤ (↑I⁻¹ : FractionalIdeal S A) * (↑I : FractionalIdeal S A)
Tactic: conv_rhs => rw [← hinv, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
this : 1 ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
w : A
hw : w ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A)
hvw : w * v = 1
⊢ (↑I⁻¹ : FractionalIdeal S A) * spanSingleton S w ≤ (↑I⁻¹ : FractionalIdeal S A) * (↑I : FractionalIdeal S A)
have refine_1 : (↑I⁻¹ : FractionalIdeal S A) * (↑I : FractionalIdeal S A) ≤ (↑I⁻¹ : FractionalIdeal S A) * (↑I : FractionalIdeal S A)
Tactic: grw [FractionalIdeal.spanSingleton_le_iff_mem.mpr hw]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ (↑I⁻¹ : FractionalIdeal S A)
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
this : 1 ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)
w : A
hw : w ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A)
hvw : w * v = 1
⊢ 1 ≤ (↑I⁻¹ : FractionalIdeal S A) * spanSingleton S w
have refine_2 : w * v ∈ spanSingleton S w * (↑I⁻¹ : FractionalIdeal S A)
Tactic: rw [FractionalIdeal.one_le, ← hvw, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv hinv' : I * I' = 1
⊢ (↑I : Submodule R A).IsPrincipal
have hinv₁ : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
Tactic: rw [coe_ext_iff, coe_mul] at hinv
Cleared hypotheses: hinv, hinv'
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
⊢ (↑I : Submodule R A).IsPrincipal
have haveI : ∀ (this : DecidableEq (Ideal R)), (↑I : Submodule R A).IsPrincipal
Tactic: haveI := Classical.decEq (Ideal R)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : DecidableEq (Ideal R)
⊢ ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
have simp_rw : ∀ (M : Ideal R),
  Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} M →
    ∀ (M' : Ideal R), M' ≠ M ∧ Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} M' → M ⊔ M' = ⊤
Tactic: simp_rw [s, Finset.mem_erase, hf.mem_toFinset]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : DecidableEq (Ideal R)
⊢ (↑I : Submodule R A).IsPrincipal
have coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
Tactic: have coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤ := by
    simp_rw [s, Finset.mem_erase, hf.mem_toFinset]
    rintro M hM M' ⟨hne, hM'⟩
    exact Ideal.IsMaximal.coprime_of_ne hM hM' hne.symm
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
⊢ (↑I : Submodule R A).IsPrincipal
have nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
Tactic: have nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M := fun M hM =>
    left_lt_sup.1
      ((hf.mem_toFinset.1 hM).lt_top.trans_eq (Ideal.sup_iInf_eq_top <| coprime M hM).symm)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
M : Ideal R
hM : M ∈ s
⊢ ∃ a ∈ I, ∃ b ∈ I', a * b ∉ IsLocalization.coeSubmodule A M
have by_contra! : ∀
  (h :
    ∀ (a : A) (_ : a ∈ I) (b : A) (_ : b ∈ I'),
      Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a * b)),
  False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
M : Ideal R
hM : M ∈ s
h :
  ∀ (a : A) (_ : a ∈ I) (b : A) (_ : b ∈ I'),
    Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a * b)
⊢ False
have obtain : ∀ (x : A) (hx : x ∈ (↑I : Submodule R A) * (↑I' : Submodule R A)) (hxM : x ∉ IsLocalization.coeSubmodule A M), False
Tactic: obtain ⟨x, hx, hxM⟩ :=
      SetLike.exists_of_lt
        ((IsLocalization.coeSubmodule_strictMono hS (hf.mem_toFinset.1 hM).lt_top).trans_eq
          hinv.symm)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
⊢ (↑I : Submodule R A).IsPrincipal
have this₁ : ∀ M ∈ s, ∃ a ∈ I, ∃ b ∈ I', a * b ∉ IsLocalization.coeSubmodule A M
Tactic: have : ∀ M ∈ s, ∃ a ∈ I, ∃ b ∈ I', a * b ∉ IsLocalization.coeSubmodule A M := by
    intro M hM; by_contra! h
    obtain ⟨x, hx, hxM⟩ :=
      SetLike.exists_of_lt
        ((IsLocalization.coeSubmodule_strictMono hS (hf.mem_toFinset.1 hM).lt_top).trans_eq
          hinv.symm)
    exact hxM (Submodule.mul_le.2 h hx)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
this : ∀ M ∈ s, ∃ a ∈ I, ∃ b ∈ I', a * b ∉ IsLocalization.coeSubmodule A M
⊢ (↑I : Submodule R A).IsPrincipal
have choose! : ∀ (a : (M : Ideal R) → A) (ha : ∀ M ∈ s, a M ∈ I) (b : (M : Ideal R) → A) (hb : ∀ M ∈ s, b M ∈ I')
  (hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M), (↑I : Submodule R A).IsPrincipal
Tactic: choose! a ha b hb hm using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
⊢ (↑I : Submodule R A).IsPrincipal
have choose! : ∀ (u : (M : Ideal R) → R)
  (hu : ∀ (M : Ideal R) (hM : M ∈ s), Membership.mem (γ := Ideal R) (⨅ M' ∈ s.erase M, M') (u M))
  (hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M), (↑I : Submodule R A).IsPrincipal
Tactic: choose! u hu hum using fun M hM => SetLike.not_le_iff_exists.1 (nle M hM)