awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
I J : Ideal R
pos : ∀ (hI : I = ⊥), I ≤ J ∨ J ≤ I
neg : ∀ (hI : ¬I = ⊥), I ≤ J ∨ J ≤ I
⊢ I ≤ J ∨ J ≤ I

Tactic:
by_cases hI : I = ⊥
-- 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
I J : Ideal R
hI : I = ⊥
pos pos₁ pos₂ pos₃ : ¬(I ≤ J ∨ J ≤ I) → False
pos₄ pos₅ pos₆ pos₇ pos₈ pos₉ pos₁₀ pos₁₁ : ¬I ≤ J ∧ ¬J ≤ I → False
⊢ I ≤ J ∨ J ≤ I

Tactic:
order
-- 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
I J : Ideal R
hI : ¬I = ⊥
pos : ∀ (hJ : J = ⊥), I ≤ J ∨ J ≤ I
neg : ∀ (hJ : ¬J = ⊥), I ≤ J ∨ J ≤ I
⊢ I ≤ J ∨ J ≤ I

Tactic:
by_cases hJ : J = ⊥
-- 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
I J : Ideal R
hI : ¬I = ⊥
hJ : J = ⊥
pos pos₁ pos₂ pos₃ : ¬(I ≤ J ∨ J ≤ I) → False
pos₄ pos₅ pos₆ pos₇ pos₈ pos₉ pos₁₀ pos₁₁ : ¬I ≤ J ∧ ¬J ≤ I → False
⊢ I ≤ J ∨ J ≤ I

Tactic:
order
-- 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
I J : Ideal R
hI : ¬I = ⊥
hJ : ¬J = ⊥
neg :
  ∀ (n : ℕ) (hI : ¬HPow.hPow (α := Ideal R) (maximalIdeal R) n = ⊥),
    HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ J ∨ J ≤ HPow.hPow (α := Ideal R) (maximalIdeal R) n
⊢ I ≤ J ∨ J ≤ I

Tactic:
obtain ⟨n, rfl⟩ := H I hI

Premises used: rfl
-- 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
J : Ideal R
hJ : ¬J = ⊥
n : ℕ
hI : ¬HPow.hPow (α := Ideal R) (maximalIdeal R) n = ⊥
neg :
  ∀ (m : ℕ) (hJ : ¬HPow.hPow (α := Ideal R) (maximalIdeal R) m = ⊥),
    HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ HPow.hPow (α := Ideal R) (maximalIdeal R) m ∨
      HPow.hPow (α := Ideal R) (maximalIdeal R) m ≤ HPow.hPow (α := Ideal R) (maximalIdeal R) n
⊢ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ J ∨ J ≤ HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
obtain ⟨m, rfl⟩ := H J hJ

Premises used: rfl
-- 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
n : ℕ
hI : ¬HPow.hPow (α := Ideal R) (maximalIdeal R) n = ⊥
m : ℕ
hJ : ¬HPow.hPow (α := Ideal R) (maximalIdeal R) m = ⊥
⊢ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ HPow.hPow (α := Ideal R) (maximalIdeal R) m ∨
    HPow.hPow (α := Ideal R) (maximalIdeal R) m ≤ HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
(le_total m n).imp Ideal.pow_le_pow_right Ideal.pow_le_pow_right

Premises used: le_total, Ideal.pow_le_pow_right, Or.imp
-- 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
n : ℕ
hI : ¬HPow.hPow (α := Ideal R) (maximalIdeal R) n = ⊥
m : ℕ
hJ : ¬HPow.hPow (α := Ideal R) (maximalIdeal R) m = ⊥
⊢ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ HPow.hPow (α := Ideal R) (maximalIdeal R) m ∨
    HPow.hPow (α := Ideal R) (maximalIdeal R) m ≤ HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
exact (le_total m n).imp Ideal.pow_le_pow_right Ideal.pow_le_pow_right

Premises used: le_total, Ideal.pow_le_pow_right, Or.imp
-- 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:
tfae_have 7 → 2 := by
    rw [ValuationRing.iff_ideal_total]
    intro H
    constructor
    intro I J
    by_cases hI : I = ⊥; · order
    by_cases hJ : J = ⊥; · order
    obtain ⟨n, rfl⟩ := H I hI
    obtain ⟨m, rfl⟩ := H J hJ
    exact (le_total m n).imp Ideal.pow_le_pow_right Ideal.pow_le_pow_right
-- 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
tfae_7_to_2 :
  ∀ (a : ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n), ValuationRing R
⊢ [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R,
      Submodule.IsPrincipal (maximalIdeal R), finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n].TFAE

Tactic:
tfae_finish
-- 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
h : ¬IsField R
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔
    finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1

Tactic:
simp [Nat.le_one_iff_eq_zero_or_eq_one, finrank_cotangentSpace_eq_zero_iff, h]

Premises used: Nat.le_one_iff_eq_zero_or_eq_one, IsLocalRing.finrank_cotangentSpace_eq_zero_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
h : ¬IsField R
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔
    finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1

Tactic:
have : finrank (ResidueField R) (CotangentSpace R) = 1 ↔
      finrank (ResidueField R) (CotangentSpace R) ≤ 1 := by
    simp [Nat.le_one_iff_eq_zero_or_eq_one, finrank_cotangentSpace_eq_zero_iff, h]
-- 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
h : ¬IsField R
this :
  finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔
    finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1
rw :
  [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime, Submodule.IsPrincipal (maximalIdeal R),
      finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n].TFAE
⊢ [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime, Submodule.IsPrincipal (maximalIdeal R),
      finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n].TFAE

Tactic:
rw [this]
-- 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
h : ¬IsField R
this :
  finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔
    finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1
⊢ Ne (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
have : maximalIdeal R ≠ ⊥ := isField_iff_maximalIdeal_eq.not.mp h
-- 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
h : ¬IsField R
this_1 :
  finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔
    finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1
this : Ne (α := Ideal R) (maximalIdeal R) ⊥
⊢ [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R,
      Submodule.IsPrincipal (maximalIdeal R), finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n].TFAE

Tactic:
tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain R

Premises used: tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain
-- 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
h : ¬IsField R
this_1 :
  finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔
    finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1
this : Ne (α := Ideal R) (maximalIdeal R) ⊥
h₁ : IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R
h₂ : (∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime) ↔ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
⊢ [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime, Submodule.IsPrincipal (maximalIdeal R),
      finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n].TFAE

Tactic:
convert! tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain R

Premises used: tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain
-- 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
h : ¬IsField R
this_1 :
  finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔
    finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1
this : Ne (α := Ideal R) (maximalIdeal R) ⊥
⊢ IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R

Tactic:
⟨fun _ ↦ inferInstance, fun h ↦ { h with not_a_field' := this }⟩

Premises used: inferInstance, IsDiscreteValuationRing.mk, Iff.intro
-- 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
h : ¬IsField R
this_1 :
  finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔
    finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1
this : Ne (α := Ideal R) (maximalIdeal R) ⊥
⊢ IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R

Tactic:
exact ⟨fun _ ↦ inferInstance, fun h ↦ { h with not_a_field' := this }⟩
-- 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
h : ¬IsField R
this_1 :
  finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔
    finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1
this : Ne (α := Ideal R) (maximalIdeal R) ⊥
⊢ (∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime) ↔ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R

Tactic:
⟨fun h P h₁ h₂ ↦ h.unique ⟨h₁, h₂⟩ ⟨this, inferInstance⟩,
      fun H ↦ ⟨_, ⟨this, inferInstance⟩, fun P hP ↦ H P hP.1 hP.2⟩⟩

Premises used: IsLocalRing.maximalIdeal, inferInstance, And.right, And.left, And.intro, Iff.intro, Exists.intro, ExistsUnique.unique
-- 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
h : ¬IsField R
this_1 :
  finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔
    finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1
this : Ne (α := Ideal R) (maximalIdeal R) ⊥
⊢ (∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime) ↔ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R

Tactic:
exact ⟨fun h P h₁ h₂ ↦ h.unique ⟨h₁, h₂⟩ ⟨this, inferInstance⟩,
      fun H ↦ ⟨_, ⟨this, inferInstance⟩, fun P hP ↦ H P hP.1 hP.2⟩⟩
-- 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
pos : ∀ (hR : IsField R), finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R
neg : ∀ (hR : ¬IsField R), finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

Tactic:
by_cases hR : IsField R

Premises used: IsField
-- 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
hR : IsField R
this : Field R := hR.toField
pos : ¬IsDiscreteValuationRing R
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

Tactic:
simp only [finrank_cotangentSpace_eq_zero, zero_ne_one, false_iff]

Premises used: IsLocalRing.finrank_cotangentSpace_eq_zero, zero_ne_one, false_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
hR : IsField R
this : Field R := hR.toField
⊢ ¬IsDiscreteValuationRing R

Tactic:
fun h ↦ h.3 maximalIdeal_eq_bot

Premises used: IsLocalRing.maximalIdeal_eq_bot, IsDiscreteValuationRing.not_a_field', Not
-- 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
hR : IsField R
this : Field R := hR.toField
⊢ ¬IsDiscreteValuationRing R

Tactic:
exact fun h ↦ h.3 maximalIdeal_eq_bot
-- 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
hR : ¬IsField R
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

Tactic:
(IsDiscreteValuationRing.TFAE R hR).out 5 0

Premises used: List.TFAE.out, IsDiscreteValuationRing.TFAE, OfNat.ofNat
-- 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
hR : ¬IsField R
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

Tactic:
exact (IsDiscreteValuationRing.TFAE R hR).out 5 0

Premises used: List.TFAE.out, IsDiscreteValuationRing.TFAE, OfNat.ofNat
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1

Tactic:
finrank_CotangentSpace_eq_one_iff.mpr ‹_›

Premises used: Iff.mpr, IsLocalRing.finrank_CotangentSpace_eq_one_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ ringKrullDim R = 1

Tactic:
eq_of_le_of_not_lt (krullDimLE_iff (n := 1).mp ?_) fun h ↦ ?_

Premises used: Ring.krullDimLE_iff, Iff.mp, eq_of_le_of_not_lt
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
refine_1 : KrullDimLE 1 R
refine_2 : ∀ (h : ringKrullDim R < 1), False
⊢ ringKrullDim R = 1

Tactic:
refine eq_of_le_of_not_lt (krullDimLE_iff (n := 1).mp ?_) fun h ↦ ?_

Premises used: Ring.krullDimLE_iff, Iff.mp, eq_of_le_of_not_lt
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ KrullDimLE 1 R

Tactic:
krullDimLE_one_iff_of_isPrime_bot.mpr fun I hI hI' ↦ hI'.isMaximal hI

Premises used: Iff.mpr, Ideal.IsPrime.isMaximal, Ring.krullDimLE_one_iff_of_isPrime_bot
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ KrullDimLE 1 R

Tactic:
exact krullDimLE_one_iff_of_isPrime_bot.mpr fun I hI hI' ↦ hI'.isMaximal hI

Premises used: Iff.mpr, Ideal.IsPrime.isMaximal, Ring.krullDimLE_one_iff_of_isPrime_bot
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
h : ringKrullDim R < 1
⊢ KrullDimLE 0 R

Tactic:
have : KrullDimLE 0 R := krullDimLE_iff.mpr (ENat.WithBot.lt_add_one_iff.mp h)
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
h : ringKrullDim R < 1
this : KrullDimLE 0 R
⊢ False

Tactic:
IsDiscreteValuationRing.not_isField R KrullDimLE.isField_of_isDomain

Premises used: IsDiscreteValuationRing.not_isField, Ring.KrullDimLE.isField_of_isDomain