awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
this_1 : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)
this_2 : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this_2 = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) y
hy₂ : b * y = a
neg : {y} ⊆ (↑(maximalIdeal R) : Set R)
neg₁ neg₂ neg₃ neg₄ : y ∈ (↑(maximalIdeal R) : Set R)
⊢ LE.le (α := Submodule R R) (R ∙ y) (maximalIdeal R)

Tactic:
rwa [Submodule.span_le, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Submodule.span_le
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
⊢ IsPrincipalIdealRing R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
⊢ ValuationRing R

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
⊢ ∀ (a : IsPrincipalIdealRing R), ValuationRing R

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
⊢ ∀ (a : IsPrincipalIdealRing R), ValuationRing R

Tactic:
tfae_have 1 → 2 := fun _ ↦ inferInstance
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
⊢ ValuationRing R

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
⊢ IsPrincipalIdealRing R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
⊢ ∀ (a : ValuationRing R), IsPrincipalIdealRing R

Tactic:
2 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
⊢ ∀ (a : ValuationRing R), IsPrincipalIdealRing R

Tactic:
tfae_have 2 → 1 := fun _ ↦ ((IsBezout.TFAE (R := R)).out 0 1).mp ‹_›
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
⊢ IsPrincipalIdealRing R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
⊢ IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
⊢ ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R

Tactic:
1 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
⊢ ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R

Tactic:
tfae_have 1 → 4
  | H => ⟨inferInstance, fun P hP hP' ↦ eq_maximalIdeal (hP'.isMaximal hP)⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
⊢ IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
⊢ IsDedekindDomain R

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
⊢ ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R

Tactic:
4 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
⊢ ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R

Tactic:
tfae_have 4 → 3 :=
    fun ⟨h₁, h₂⟩ ↦ { h₁ with maximalOfPrime := (h₂ _ · · ▸ maximalIdeal.isMaximal R) }
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
⊢ IsDedekindDomain R

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
⊢ ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)

Tactic:
3 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
⊢ ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)

Tactic:
tfae_have 3 → 5 := fun h ↦ maximalIdeal_isPrincipal_of_isDedekindDomain R
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
6 ↔ 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
tfae_have 6 ↔ 5 := finrank_cotangentSpace_le_one_iff

Premises used: IsLocalRing.finrank_cotangentSpace_le_one_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
⊢ ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
⊢ ∀ (a : Submodule.IsPrincipal (maximalIdeal R)) (I : Ideal R),
    I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
5 → 7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
⊢ ∀ (a : Submodule.IsPrincipal (maximalIdeal R)) (I : Ideal R),
    I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
tfae_have 5 → 7 := exists_maximalIdeal_pow_eq_of_principal R

Premises used: exists_maximalIdeal_pow_eq_of_principal
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 :
  ∀ (a : Submodule.IsPrincipal (maximalIdeal R)) (I : Ideal R),
    I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
⊢ ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 :
  ∀ (a : Submodule.IsPrincipal (maximalIdeal R)) (I : Ideal R),
    I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
⊢ ValuationRing R

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 :
  ∀ (a : Submodule.IsPrincipal (maximalIdeal R)) (I : Ideal R),
    I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
⊢ ∀ (a : ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n), ValuationRing R

Tactic:
7 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 :
  ∀ (a : Submodule.IsPrincipal (maximalIdeal R)) (I : Ideal R),
    I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
rw :
  ∀ (a : ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n),
    Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
⊢ ∀ (a : ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n), ValuationRing R

Tactic:
rw [ValuationRing.iff_ideal_total]

Premises used: ValuationRing.iff_ideal_total
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
tfae_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
tfae_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
tfae_1_to_4 :
  ∀ (a : IsPrincipalIdealRing R), IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : ∀ (a : IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R), IsDedekindDomain R
tfae_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 :
  ∀ (a : Submodule.IsPrincipal (maximalIdeal R)) (I : Ideal R),
    I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
total : ∀ (a b : Ideal R), a ≤ b ∨ b ≤ a
⊢ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2

Tactic:
constructor