awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
inst_55 : Free A R₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
s : Set R₁
t : Set R₂
hs : Eq (α := Subalgebra A R₁) (Algebra.adjoin A s) ⊤
ht : Eq (α := Subalgebra A R₂) (Algebra.adjoin A t) ⊤
⊢ Eq (α := Subalgebra A B) (AlgHom.range (IsScalarTower.toAlgHom A R₁ B) ⊔ AlgHom.range (IsScalarTower.toAlgHom A R₂ B))
    ⊤

Tactic:
range_sup_range_eq_top_of_isCoprime_differentIdeal A B R₁ R₂ h₁ h₂ h₃

Premises used: IsDedekindDomain.range_sup_range_eq_top_of_isCoprime_differentIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
inst_55 : Free A R₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
s : Set R₁
t : Set R₂
hs : Eq (α := Subalgebra A R₁) (Algebra.adjoin A s) ⊤
ht : Eq (α := Subalgebra A R₂) (Algebra.adjoin A t) ⊤
⊢ Eq (α := Subalgebra A B) (AlgHom.range (IsScalarTower.toAlgHom A R₁ B) ⊔ AlgHom.range (IsScalarTower.toAlgHom A R₂ B))
    ⊤

Tactic:
exact range_sup_range_eq_top_of_isCoprime_differentIdeal A B R₁ R₂ h₁ h₂ h₃

Premises used: IsDedekindDomain.range_sup_range_eq_top_of_isCoprime_differentIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
pos : ∀ (hP0 : P = ⊥), P = span {x}
neg : ∀ (hP0 : ¬P = ⊥), P = span {x}
⊢ P = span {x}

Tactic:
by_cases hP0 : P = ⊥
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : P = ⊥
pos :
  ∀ (hP : IsPrime.{u_1} (α := R) ⊥) (x_mem : Membership.mem (γ := Ideal R) ⊥ x)
    (hxP2 : x ∉ HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 2) (hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ ⊥ → x ∉ Q),
    Eq (α := Ideal R) ⊥ (span {x})
⊢ P = span {x}

Tactic:
subst hP0
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
x : R
hP : IsPrime.{u_1} (α := R) ⊥
x_mem : Membership.mem (γ := Ideal R) ⊥ x
hxP2 : x ∉ HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ ⊥ → x ∉ Q
pos : Eq (α := Ideal R) (span {x}) ⊥
pos₁ : x = 0
pos₂ pos₃ pos₄ pos₅ : Membership.mem (γ := Ideal R) ⊥ x
⊢ Eq (α := Ideal R) ⊥ (span {x})

Tactic:
rwa [eq_comm, span_singleton_eq_bot, ← mem_bot]

Premises used: Ideal.mem_bot, Ideal.span_singleton_eq_bot, eq_comm
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
⊢ Ne (α := Ideal R) (span {x}) ⊥

Tactic:
have hspan0 : span {x} ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp (hxP2 <| · ▸ zero_mem _)
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
neg : normalizedFactors P = normalizedFactors (span {x})
⊢ P = span {x}

Tactic:
rw [← associated_iff_eq, associated_iff_normalizedFactors_eq_normalizedFactors hP0 hspan0]

Premises used: UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors, associated_iff_eq
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
⊢ normalizedFactors P = normalizedFactors (span {x})

Tactic:
Multiset.ext' fun Q ↦ ?_

Premises used: Multiset.ext'
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
neg : ∀ (Q : Ideal R), Multiset.count Q (normalizedFactors P) = Multiset.count Q (normalizedFactors (span {x}))
⊢ normalizedFactors P = normalizedFactors (span {x})

Tactic:
refine Multiset.ext' fun Q ↦ ?_

Premises used: Multiset.ext'
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
neg : (if Q = P then 1 else 0) = Multiset.count Q (normalizedFactors (span {x}))
⊢ Multiset.count Q (normalizedFactors P) = Multiset.count Q (normalizedFactors (span {x}))

Tactic:
rw [normalizedFactors_irreducible (Ideal.prime_of_isPrime hP0 hP).irreducible, normalize_eq,
    Multiset.count_singleton]

Premises used: Prime.irreducible, UniqueFactorizationMonoid.normalizedFactors_irreducible, Multiset.count_singleton, Ideal.prime_of_isPrime, normalize_eq
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
neg : Multiset.count Q (normalizedFactors (span {x})) = if Q = P then 1 else 0
⊢ (if Q = P then 1 else 0) = Multiset.count Q (normalizedFactors (span {x}))

Tactic:
symm
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
pos : ∀ (hQ : Q = P), Multiset.count Q (normalizedFactors (span {x})) = 1
neg : ∀ (hQ : ¬Q = P), Multiset.count Q (normalizedFactors (span {x})) = 0
⊢ Multiset.count Q (normalizedFactors (span {x})) = if Q = P then 1 else 0

Tactic:
split_ifs with hQ
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : Q = P
⊢ Q.IsPrime

Tactic:
subst hQ
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : Q = P
hP₁ : Q.IsPrime
⊢ x ∈ Q

Tactic:
subst hQ
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : Q = P
hP₁ : Q.IsPrime
x_mem₁ : x ∈ Q
⊢ x ∉ HPow.hPow (β := ℕ) Q 2

Tactic:
subst hQ
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : Q = P
hP₁ : Q.IsPrime
x_mem₁ : x ∈ Q
hxP2₁ : x ∉ HPow.hPow (β := ℕ) Q 2
⊢ ∀ (Q_1 : Ideal R), Q_1.IsPrime → Q_1 ≠ Q → x ∉ Q_1

Tactic:
subst hQ
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : Q = P
hP₁ : Q.IsPrime
x_mem₁ : x ∈ Q
hxP2₁ : x ∉ HPow.hPow (β := ℕ) Q 2
hxQ₁ : ∀ (Q_1 : Ideal R), Q_1.IsPrime → Q_1 ≠ Q → x ∉ Q_1
⊢ ¬Q = ⊥

Tactic:
subst hQ
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
x : R
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hP : Q.IsPrime
x_mem : x ∈ Q
hxP2 : x ∉ HPow.hPow (β := ℕ) Q 2
hxQ : ∀ (Q_1 : Ideal R), Q_1.IsPrime → Q_1 ≠ Q → x ∉ Q_1
hP0 : ¬Q = ⊥
pos : span {x} ≤ HPow.hPow (β := ℕ) Q 1
pos₁ : ¬span {x} ≤ Q ^ HAdd.hAdd (α := ℕ) 1 1
⊢ Multiset.count Q (normalizedFactors (span {x})) = 1

Tactic:
apply Ideal.count_normalizedFactors_eq

Premises used: Ideal.count_normalizedFactors_eq
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
x : R
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hP : Q.IsPrime
x_mem : x ∈ Q
hxP2 : x ∉ HPow.hPow (β := ℕ) Q 2
hxQ : ∀ (Q_1 : Ideal R), Q_1.IsPrime → Q_1 ≠ Q → x ∉ Q_1
hP0 : ¬Q = ⊥
⊢ span {x} ≤ HPow.hPow (β := ℕ) Q 1

Tactic:
simpa
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
x : R
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hP : Q.IsPrime
x_mem : x ∈ Q
hxP2 : x ∉ HPow.hPow (β := ℕ) Q 2
hxQ : ∀ (Q_1 : Ideal R), Q_1.IsPrime → Q_1 ≠ Q → x ∉ Q_1
hP0 : ¬Q = ⊥
⊢ ¬span {x} ≤ Q ^ HAdd.hAdd (α := ℕ) 1 1

Tactic:
simpa
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : ¬Q = P
pos : ∀ (hQp : Q.IsPrime), Multiset.count Q (normalizedFactors (span {x})) = 0
neg : ∀ (hQp : ¬Q.IsPrime), Multiset.count Q (normalizedFactors (span {x})) = 0
⊢ Multiset.count Q (normalizedFactors (span {x})) = 0

Tactic:
by_cases hQp : IsPrime Q

Premises used: Ideal.IsPrime
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : ¬Q = P
hQp : Q.IsPrime
pos : span {x} ≤ HPow.hPow (β := ℕ) Q 0
pos₁ : ¬span {x} ≤ Q ^ HAdd.hAdd (α := ℕ) 0 1
⊢ Multiset.count Q (normalizedFactors (span {x})) = 0

Tactic:
apply Ideal.count_normalizedFactors_eq

Premises used: Ideal.count_normalizedFactors_eq
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : ¬Q = P
hQp : Q.IsPrime
⊢ span {x} ≤ HPow.hPow (β := ℕ) Q 0

Tactic:
simp [hxQ _ hQp hQ]
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : ¬Q = P
hQp : Q.IsPrime
⊢ ¬span {x} ≤ Q ^ HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp [hxQ _ hQp hQ]
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : ¬Q = P
hQp : ¬Q.IsPrime
⊢ Multiset.count Q (normalizedFactors (span {x})) = 0

Tactic:
Multiset.count_eq_zero.mpr fun hQi ↦
    hQp <| isPrime_of_prime <| irreducible_iff_prime.mp <| irreducible_of_normalized_factor _ hQi

Premises used: Iff.mpr, Iff.mp, UniqueFactorizationMonoid.irreducible_of_normalized_factor, Ideal.isPrime_of_prime, Multiset.count_eq_zero, irreducible_iff_prime
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : ¬Q = P
hQp : ¬Q.IsPrime
⊢ Multiset.count Q (normalizedFactors (span {x})) = 0

Tactic:
exact Multiset.count_eq_zero.mpr fun hQi ↦
    hQp <| isPrime_of_prime <| irreducible_iff_prime.mp <| irreducible_of_normalized_factor _ hQi

Premises used: Iff.mpr, Iff.mp, UniqueFactorizationMonoid.irreducible_of_normalized_factor, Ideal.isPrime_of_prime, Multiset.count_eq_zero, irreducible_iff_prime
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
pos : ∀ (hP0 : P = ⊥), P = span {x}
neg neg₁ : ∀ (hP0 : ¬P = ⊥), P = span {x}
neg₂ : ∀ (hP0 : ¬P = ⊥) (hspan0 : Ne (α := Ideal R) (span {x}) ⊥), P = span {x}
neg₃ : ∀ (hP0 : ¬P = ⊥) (hspan0 : Ne (α := Ideal R) (span {x}) ⊥), normalizedFactors P = normalizedFactors (span {x})
neg₄ :
  ∀ (hP0 : ¬P = ⊥) (hspan0 : Ne (α := Ideal R) (span {x}) ⊥) (Q : Ideal R),
    Multiset.count Q (normalizedFactors P) = Multiset.count Q (normalizedFactors (span {x}))
neg₅ :
  ∀ (hP0 : ¬P = ⊥) (hspan0 : Ne (α := Ideal R) (span {x}) ⊥) (Q : Ideal R),
    (if Q = P then 1 else 0) = Multiset.count Q (normalizedFactors (span {x}))
neg₆ :
  ∀ (hP0 : ¬P = ⊥) (hspan0 : Ne (α := Ideal R) (span {x}) ⊥) (Q : Ideal R),
    Multiset.count Q (normalizedFactors (span {x})) = if Q = P then 1 else 0
pos₁ :
  ∀ (hP0 : ¬P = ⊥) (hspan0 : Ne (α := Ideal R) (span {x}) ⊥) (Q : Ideal R) (hQ : Q = P),
    Multiset.count Q (normalizedFactors (span {x})) = 1
neg₇ neg₈ :
  ∀ (hP0 : ¬P = ⊥) (hspan0 : Ne (α := Ideal R) (span {x}) ⊥) (Q : Ideal R) (hQ : ¬Q = P),
    Multiset.count Q (normalizedFactors (span {x})) = 0
pos₂ :
  ∀ (hP0 : ¬P = ⊥) (hspan0 : Ne (α := Ideal R) (span {x}) ⊥) (Q : Ideal R) (hQ : ¬Q = P) (hQp : Q.IsPrime),
    Multiset.count Q (normalizedFactors (span {x})) = 0
neg₉ neg₁₀ :
  ∀ (hP0 : ¬P = ⊥) (hspan0 : Ne (α := Ideal R) (span {x}) ⊥) (Q : Ideal R) (hQ : ¬Q = P) (hQp : ¬Q.IsPrime),
    Multiset.count Q (normalizedFactors (span {x})) = 0
⊢ P = span {x}

Tactic:
classical
  by_cases hP0 : P = ⊥
  · subst hP0
    rwa [eq_comm, span_singleton_eq_bot, ← mem_bot]
  have hspan0 : span {x} ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp (hxP2 <| · ▸ zero_mem _)
  rw [← associated_iff_eq, associated_iff_normalizedFactors_eq_normalizedFactors hP0 hspan0]
  refine Multiset.ext' fun Q ↦ ?_
  rw [normalizedFactors_irreducible (Ideal.prime_of_isPrime hP0 hP).irreducible, normalize_eq,
    Multiset.count_singleton]
  symm
  split_ifs with hQ
  · subst hQ
    apply Ideal.count_normalizedFactors_eq <;> simpa
  by_cases hQp : IsPrime Q
  · apply Ideal.count_normalizedFactors_eq <;> simp [hxQ _ hQp hQ]
  exact Multiset.count_eq_zero.mpr fun hQi ↦
    hQp <| isPrime_of_prime <| irreducible_iff_prime.mp <| irreducible_of_normalized_factor _ hQi

Premises used: Ideal.mem_bot, Ideal.span_singleton_eq_bot, Ideal.count_normalizedFactors_eq, eq_comm, associated_iff_eq, Multiset.count_singleton, Multiset.ext', normalize_eq
-- 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)
h : Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) = ⊤
⊢ (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1

Tactic:
have hinv := I.mul_inv
-- 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)
h : Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) = ⊤
hinv : (↑I : FractionalIdeal S A) * (↑I⁻¹ : FractionalIdeal S A) = 1
⊢ let J := Submodule.comap (Algebra.linearMap R A) ((↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v));
  J = ⊤

Tactic:
set J := Submodule.comap (Algebra.linearMap R A) ((I : Submodule R A) * Submodule.span R {v})

Premises used: Units.val, HMul.hMul, Algebra.linearMap, FractionalIdeal.coeToSubmodule, Submodule.comap, Submodule.span, Singleton.singleton
-- 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 = ⊤
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)
⊢ IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)

Tactic:
rw [coe_ext_iff, coe_mul, coe_one] at hinv

Premises used: FractionalIdeal.coe_ext_iff, FractionalIdeal.coe_one, FractionalIdeal.coe_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) : 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) ≤ LinearMap.range (Algebra.linearMap R A)
⊢ IsLocalization.coeSubmodule A J = (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v)

Tactic:
apply Submodule.map_comap_eq_self

Premises used: Submodule.map_comap_eq_self
-- 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) : 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)
h₃ 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)
⊢ (↑(↑I : FractionalIdeal S A) : Submodule R A) * (R ∙ v) ≤ LinearMap.range (Algebra.linearMap R A)

Tactic:
grw [← Submodule.one_eq_range, ← hinv, (Submodule.span_singleton_le_iff_mem _ _).2 hv]

Premises used: Iff.mpr, Submodule.span_singleton_le_iff_mem, Submodule.one_eq_range