awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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 = ⊥
⊢ I ≤ J ∨ J ≤ I
have pos : ¬(I ≤ J ∨ J ≤ I) → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ I ≤ J ∨ J ≤ I
have pos₄ : ¬I ≤ J ∧ ¬J ≤ I → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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 = ⊥
⊢ I ≤ J ∨ J ≤ I
have pos : ∀ (hJ : J = ⊥), I ≤ J ∨ J ≤ I
Tactic: by_cases hJ : J = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ I ≤ J ∨ J ≤ I
have neg : ∀ (hJ : ¬J = ⊥), I ≤ J ∨ J ≤ I
Tactic: by_cases hJ : J = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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 = ⊥
⊢ I ≤ J ∨ J ≤ I
have pos : ¬(I ≤ J ∨ J ≤ I) → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ I ≤ J ∨ J ≤ I
have pos₄ : ¬I ≤ J ∧ ¬J ≤ I → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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 = ⊥
⊢ I ≤ J ∨ J ≤ I
have 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
Tactic: obtain ⟨n, rfl⟩ := H I hI
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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 = ⊥
⊢ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ J ∨ J ≤ HPow.hPow (α := Ideal R) (maximalIdeal R) n
have 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
Tactic: obtain ⟨m, rfl⟩ := H J hJ
Cleared hypotheses: J, hJ
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (hypothesis)
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
⊢ [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
have tfae_7_to_2 : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
h : ¬IsField 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
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ [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
have 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
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (hypothesis)
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
⊢ [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
have this₁ : Ne (α := Ideal R) (maximalIdeal R) ⊥
Tactic: have : maximalIdeal R ≠ ⊥ := isField_iff_maximalIdeal_eq.not.mp h
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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, 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
have h₁ : IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R
Tactic: convert! tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain R
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ [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
have h₂ : (∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime) ↔ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
Tactic: convert! tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain R
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R
have pos : ∀ (hR : IsField R), finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R
Tactic: by_cases hR : IsField R
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R
have neg : ∀ (hR : ¬IsField R), finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R
Tactic: by_cases hR : IsField R
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R
have pos : ¬IsDiscreteValuationRing R
Tactic: simp only [finrank_cotangentSpace_eq_zero, zero_ne_one, false_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ ringKrullDim R = 1
have refine_1 : KrullDimLE 1 R
Tactic: refine eq_of_le_of_not_lt (krullDimLE_iff (n := 1).mp ?_) fun h ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
refine_1 : KrullDimLE 1 R
⊢ ringKrullDim R = 1
have refine_2 : ∀ (h : ringKrullDim R < 1), False
Tactic: refine eq_of_le_of_not_lt (krullDimLE_iff (n := 1).mp ?_) fun h ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
h : ringKrullDim R < 1
⊢ False
have this : KrullDimLE 0 R
Tactic: have : KrullDimLE 0 R := krullDimLE_iff.mpr (ENat.WithBot.lt_add_one_iff.mp h)
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
B : Type v
C : Type z
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : CommRing C
inst_5 : Algebra A C
inst_6 : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
⊢ (traceMatrix A b).det = discr.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b)
have e_M : traceMatrix A b = traceMatrix.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
B : Type v
C : Type z
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : CommRing C
inst_5 : Algebra A C
inst_6 : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
⊢ traceMatrix A b = traceMatrix.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b)
have e_M : ∀ (i j : ι), traceMatrix A b i j = traceMatrix.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
B : Type v
C : Type z
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : CommRing C
inst_5 : Algebra A C
inst_6 : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
i j : ι
⊢ traceMatrix A b i j = traceMatrix.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b) i j
have e_M : Eq.{u + 1} (α := A) ((((traceForm A B : (a : B) → B →ₗ[A] A) (b i) : B →ₗ[A] A) : (a : B) → A) (b j) : A)
  (((traceForm A C : (a : C) → C →ₗ[A] A) (((⇑f : (a : B) → C) ∘ b) i) : (a : C) → A) (((⇑f : (a : B) → C) ∘ b) j) : A)
Tactic: simp_rw [traceMatrix_apply, traceForm_apply, Function.comp, ← map_mul f, trace_eq_of_algEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
B : Type v
C : Type z
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : CommRing C
inst_5 : Algebra A C
inst_6 : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
i j : ι
e_M :
  Eq.{u + 1} (α := A) ((((traceForm A B : (a : B) → B →ₗ[A] A) (b i) : B →ₗ[A] A) : (a : B) → A) (b j) : A)
    (((traceForm A C : (a : C) → C →ₗ[A] A) (((⇑f : (a : B) → C) ∘ b) i) : (a : C) → A) (((⇑f : (a : B) → C) ∘ b) j) :
      A)
⊢ traceMatrix A b i j = traceMatrix.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b) i j
have e_M₁ : Eq.{u + 1} (α := A) ((trace A B : (a : B) → A) (b i * b j) : A)
  ((trace A C : (a : C) → A) (HMul.hMul (α := C) (((⇑f : (a : B) → C) ∘ b) i) (((⇑f : (a : B) → C) ∘ b) j)) : A)
Tactic: simp_rw [traceMatrix_apply, traceForm_apply, Function.comp, ← map_mul f, trace_eq_of_algEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
B : Type v
C : Type z
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : CommRing C
inst_5 : Algebra A C
inst_6 : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
i j : ι
e_M :
  Eq.{u + 1} (α := A) ((((traceForm A B : (a : B) → B →ₗ[A] A) (b i) : B →ₗ[A] A) : (a : B) → A) (b j) : A)
    (((traceForm A C : (a : C) → C →ₗ[A] A) (((⇑f : (a : B) → C) ∘ b) i) : (a : C) → A) (((⇑f : (a : B) → C) ∘ b) j) :
      A)
e_M₁ :
  Eq.{u + 1} (α := A) ((trace A B : (a : B) → A) (b i * b j) : A)
    ((trace A C : (a : C) → A) (HMul.hMul (α := C) (((⇑f : (a : B) → C) ∘ b) i) (((⇑f : (a : B) → C) ∘ b) j)) : A)
⊢ traceMatrix A b i j = traceMatrix.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b) i j
have e_M₂ : Eq.{u + 1} (α := A) ((trace A B : (a : B) → A) (b i * b j) : A)
  ((trace A C : (a : C) → A) (HMul.hMul (α := C) (β := C) ((f : (a : B) → C) (b i) : C) ((f : (a : B) → C) (b j) : C)) :
    A)
Tactic: simp_rw [traceMatrix_apply, traceForm_apply, Function.comp, ← map_mul f, trace_eq_of_algEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
B : Type v
C : Type z
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : CommRing C
inst_5 : Algebra A C
inst_6 : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
i j : ι
e_M :
  Eq.{u + 1} (α := A) ((((traceForm A B : (a : B) → B →ₗ[A] A) (b i) : B →ₗ[A] A) : (a : B) → A) (b j) : A)
    (((traceForm A C : (a : C) → C →ₗ[A] A) (((⇑f : (a : B) → C) ∘ b) i) : (a : C) → A) (((⇑f : (a : B) → C) ∘ b) j) :
      A)
e_M₁ :
  Eq.{u + 1} (α := A) ((trace A B : (a : B) → A) (b i * b j) : A)
    ((trace A C : (a : C) → A) (HMul.hMul (α := C) (((⇑f : (a : B) → C) ∘ b) i) (((⇑f : (a : B) → C) ∘ b) j)) : A)
e_M₂ :
  Eq.{u + 1} (α := A) ((trace A B : (a : B) → A) (b i * b j) : A)
    ((trace A C : (a : C) → A)
        (HMul.hMul (α := C) (β := C) ((f : (a : B) → C) (b i) : C) ((f : (a : B) → C) (b j) : C)) :
      A)
⊢ traceMatrix A b i j = traceMatrix.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b) i j
have e_M₃ : Eq.{u + 1} (α := A) ((trace A B : (a : B) → A) (b i * b j) : A)
  ((trace A C : (a : C) → A) ((f : (a : B) → C) (b i * b j) : C) : A)
Tactic: simp_rw [traceMatrix_apply, traceForm_apply, Function.comp, ← map_mul f, trace_eq_of_algEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
ι' : Type u_1
inst_4 : Fintype ι'
inst_5 : Fintype ι
inst_6 : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ discr.{u, v, u_1} (ι := ι') A (B := B)
      (Function.comp.{u_1 + 1, w + 1, v + 1} (β := ι) (⇑b : (a : ι) → B) (⇑f.symm : (a : ι') → ι)) =
    discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
have rw : discr.{u, v, u_1} (ι := ι') A (B := B) (⇑(b.reindex f) : (a : ι') → B) =
  discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
Tactic: rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]