awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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)

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]
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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)
rw : ∃ (y : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) y : A) (1 : A)
⊢ 1 ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)

Tactic:
rw [← hJ, h, IsLocalization.coeSubmodule_top, Submodule.mem_one]

Premises used: Submodule.mem_one, IsLocalization.coeSubmodule_top
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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)
⊢ ∃ (y : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) y : A) (1 : A)

Tactic:
⟨1, (algebraMap R _).map_one⟩

Premises used: Algebra.algebraMap, RingHom.map_one, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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)
⊢ ∃ (y : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) y : A) (1 : A)

Tactic:
exact ⟨1, (algebraMap R _).map_one⟩
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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)

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⟩
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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)
obtain :
  ∀ (w : A) (hw : w ∈ (↑(↑I : FractionalIdeal S A) : Submodule R A)) (hvw : w * v = 1),
    (↑(↑I : FractionalIdeal S A) : Submodule R A).IsPrincipal
⊢ (↑(↑I : FractionalIdeal S A) : Submodule R A).IsPrincipal

Tactic:
obtain ⟨w, hw, hvw⟩ := Submodule.mem_mul_span_singleton.1 this

Premises used: Submodule.mem_mul_span_singleton, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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

Tactic:
⟨⟨w, ?_⟩⟩

Premises used: Submodule.IsPrincipal.mk, Exists.intro
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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 : (↑(↑I : FractionalIdeal S A) : Submodule R A) = R ∙ w
⊢ (↑(↑I : FractionalIdeal S A) : Submodule R A).IsPrincipal

Tactic:
refine ⟨⟨w, ?_⟩⟩
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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
rw : (↑(spanSingleton S w) : Submodule R A) = (↑(↑I⁻¹⁻¹ : FractionalIdeal S A) : Submodule R A)
⊢ (↑(↑I : FractionalIdeal S A) : Submodule R A) = R ∙ w

Tactic:
rw [← FractionalIdeal.coe_spanSingleton S, ← inv_inv I, eq_comm]

Premises used: eq_comm, inv_inv, FractionalIdeal.coe_spanSingleton
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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)

Tactic:
congr_arg coeToSubmodule (Units.eq_inv_of_mul_eq_one_left (le_antisymm ?_ ?_))

Premises used: congr_arg, le_antisymm, FractionalIdeal.coeToSubmodule, Units.eq_inv_of_mul_eq_one_left
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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
refine_2 : 1 ≤ (↑I⁻¹ : FractionalIdeal S A) * spanSingleton S w
⊢ (↑(spanSingleton S w) : Submodule R A) = (↑(↑I⁻¹⁻¹ : FractionalIdeal S A) : Submodule R A)

Tactic:
refine congr_arg coeToSubmodule (Units.eq_inv_of_mul_eq_one_left (le_antisymm ?_ ?_))

Premises used: congr_arg, le_antisymm, FractionalIdeal.coeToSubmodule, Units.eq_inv_of_mul_eq_one_left
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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
rw : (↑I⁻¹ : FractionalIdeal S A) * (↑I : FractionalIdeal S A)
| 1

Tactic:
rw [← hinv, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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 ≤ (↑I⁻¹ : FractionalIdeal S A) * (↑I : FractionalIdeal S A)
⊢ (↑I⁻¹ : FractionalIdeal S A) * spanSingleton S w ≤ 1

Tactic:
conv_rhs => rw [← hinv, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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 refine_1₁ :
  (↑I⁻¹ : FractionalIdeal S A) * (↑I : FractionalIdeal S A) ≤ (↑I⁻¹ : FractionalIdeal S A) * (↑I : FractionalIdeal S A)
⊢ (↑I⁻¹ : FractionalIdeal S A) * spanSingleton S w ≤ (↑I⁻¹ : FractionalIdeal S A) * (↑I : FractionalIdeal S A)

Tactic:
grw [FractionalIdeal.spanSingleton_le_iff_mem.mpr hw]

Premises used: Iff.mpr, FractionalIdeal.spanSingleton_le_iff_mem
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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_2 : w * v ∈ spanSingleton S w * (↑I⁻¹ : FractionalIdeal S A)
⊢ 1 ≤ (↑I⁻¹ : FractionalIdeal S A) * spanSingleton S w

Tactic:
rw [FractionalIdeal.one_le, ← hvw, mul_comm]

Premises used: FractionalIdeal.one_le, mul_comm
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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
⊢ w * v ∈ spanSingleton S w * (↑I⁻¹ : FractionalIdeal S A)

Tactic:
FractionalIdeal.mul_mem_mul (FractionalIdeal.mem_spanSingleton_self _ _) hv

Premises used: Set.Mem, FractionalIdeal.mem_spanSingleton_self, FractionalIdeal.mul_mem_mul
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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
⊢ w * v ∈ spanSingleton S w * (↑I⁻¹ : FractionalIdeal S A)

Tactic:
exact FractionalIdeal.mul_mem_mul (FractionalIdeal.mem_spanSingleton_self _ _) hv

Premises used: FractionalIdeal.mem_spanSingleton_self, FractionalIdeal.mul_mem_mul
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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 * I' = 1
⊢ I * I' = 1

Tactic:
have hinv' := hinv
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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) * (↑I' : Submodule R A) = (↑1 : Submodule R A)

Tactic:
rw [coe_ext_iff, coe_mul] at hinv

Premises used: FractionalIdeal.coe_ext_iff, FractionalIdeal.coe_mul
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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
hinv₁ : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
⊢ I * I' = 1

Tactic:
rw [coe_ext_iff, coe_mul] at hinv

Premises used: FractionalIdeal.coe_ext_iff, FractionalIdeal.coe_mul
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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})
haveI : ∀ (this : DecidableEq (Ideal R)), (↑I : Submodule R A).IsPrincipal
⊢ (↑I : Submodule R A).IsPrincipal

Tactic:
haveI := Classical.decEq (Ideal R)
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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)
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' = ⊤
⊢ ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤

Tactic:
simp_rw [s, Finset.mem_erase, hf.mem_toFinset]

Premises used: Set.Finite.mem_toFinset, Finset.mem_erase
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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 : Ideal R
hM : Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} M
M' : Ideal R
hne : M' ≠ M
hM' : Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} M'
⊢ M ⊔ M' = ⊤

Tactic:
Ideal.IsMaximal.coprime_of_ne hM hM' hne.symm

Premises used: Set.Mem, setOf, Ne.symm, Ideal.IsMaximal.coprime_of_ne
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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 : Ideal R
hM : Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} M
M' : Ideal R
hne : M' ≠ M
hM' : Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} M'
⊢ M ⊔ M' = ⊤

Tactic:
exact Ideal.IsMaximal.coprime_of_ne hM hM' hne.symm

Premises used: Ne.symm, Ideal.IsMaximal.coprime_of_ne
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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' = ⊤

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
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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' = ⊤
⊢ ∀ 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)
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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
by_contra! :
  ∀
    (h :
      ∀ (a : A) (_ : a ∈ I) (b : A) (_ : b ∈ I'),
        Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a * b)),
    False
⊢ ∃ a ∈ I, ∃ b ∈ I', a * b ∉ IsLocalization.coeSubmodule A M

Tactic:
by_contra! h
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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)
obtain :
  ∀ (x : A) (hx : x ∈ (↑I : Submodule R A) * (↑I' : Submodule R A)) (hxM : x ∉ IsLocalization.coeSubmodule A M), False
⊢ 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)

Premises used: SetLike.exists_of_lt, Set.Finite.mem_toFinset, LT.lt.trans_eq, Iff.mp, Ideal.IsMaximal.lt_top, IsLocalization.coeSubmodule_strictMono, Eq.symm
-- Module: Mathlib.RingTheory.DedekindDomain.PID
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)
x : A
hx : x ∈ (↑I : Submodule R A) * (↑I' : Submodule R A)
hxM : x ∉ IsLocalization.coeSubmodule A M
⊢ False

Tactic:
hxM (Submodule.mul_le.2 h hx)

Premises used: Iff.mpr, Submodule.mul_le