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 : 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
⊢ Submodule.IsPrincipal (maximalIdeal R)
have neg : Eq (α := Submodule R R) (maximalIdeal R) (R ∙ y)
Tactic: refine ⟨⟨y, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ Eq (α := Submodule R R) (maximalIdeal R) (R ∙ y)
have neg : LE.le (α := Submodule R R) (maximalIdeal R) (R ∙ y)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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 : LE.le (α := Submodule R R) (maximalIdeal R) (R ∙ y)
⊢ Eq (α := Submodule R R) (maximalIdeal R) (R ∙ y)
have neg₁ : LE.le (α := Submodule R R) (R ∙ y) (maximalIdeal R)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
m : R
hm : Membership.mem (γ := Submodule R R) (maximalIdeal R) m
⊢ Membership.mem (γ := Submodule R R) (R ∙ y) m
have neg : ∀ (k : R) (hk : k * a = b * m), Membership.mem (γ := Submodule R R) (R ∙ y) m
Tactic: obtain ⟨k, hk⟩ := hb₃ m hm
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (hypothesis)
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
m : R
hm : Membership.mem (γ := Submodule R R) (maximalIdeal R) m
k : R
hk : k * a = b * m
⊢ Membership.mem (γ := Submodule R R) (R ∙ y) m
have hk₁ : b * (y * k) = b * m
Tactic: rw [← hy₂, mul_comm, mul_assoc] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
m : R
hm : Membership.mem (γ := Submodule R R) (maximalIdeal R) m
k : R
hk : b * (y * k) = b * m
⊢ Membership.mem (γ := Submodule R R) (R ∙ y) m
have neg : Membership.mem (γ := Submodule R R) (R ∙ y) (k * y)
Tactic: rw [← mul_left_cancel₀ hb₄ hk, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ LE.le (α := Submodule R R) (R ∙ y) (maximalIdeal R)
have neg : {y} ⊆ (↑(maximalIdeal R) : Set R)
Tactic: rwa [Submodule.span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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)
⊢ LE.le (α := Submodule R R) (R ∙ y) (maximalIdeal R)
have neg₁ : y ∈ (↑(maximalIdeal R) : Set R)
Tactic: rwa [Submodule.span_le, Set.singleton_subset_iff]
-- 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
⊢ [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_1_to_2 : ∀ (a : IsPrincipalIdealRing R), ValuationRing R
Tactic: tfae_have 1 → 2 := fun _ ↦ inferInstance
-- 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
⊢ [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_2_to_1 : ∀ (a : ValuationRing R), IsPrincipalIdealRing R
Tactic: tfae_have 2 → 1 := fun _ ↦ ((IsBezout.TFAE (R := R)).out 0 1).mp ‹_›
-- 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
⊢ [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_1_to_4 : ∀ (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)⟩
-- 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
⊢ [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_4_to_3 : ∀ (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) }
-- 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
⊢ [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_3_to_5 : ∀ (a : IsDedekindDomain R), Submodule.IsPrincipal (maximalIdeal R)
Tactic: tfae_have 3 → 5 := fun h ↦ maximalIdeal_isPrincipal_of_isDedekindDomain R
-- 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)
⊢ [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_6_iff_5 : finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
Tactic: tfae_have 6 ↔ 5 := finrank_cotangentSpace_le_one_iff
-- 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)
⊢ [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_5_to_7 : ∀ (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
-- 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
⊢ ∀ (a : ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n), ValuationRing R
have rw : ∀ (a : ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n),
  Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
Tactic: rw [ValuationRing.iff_ideal_total]
-- 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
⊢ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
have total : ∀ (a b : Ideal R), a ≤ b ∨ b ≤ a
Tactic: constructor
-- 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
⊢ I ≤ J ∨ J ≤ I
have pos : ∀ (hI : I = ⊥), I ≤ J ∨ J ≤ I
Tactic: by_cases hI : I = ⊥
-- 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
pos : ∀ (hI : I = ⊥), I ≤ J ∨ J ≤ I
⊢ I ≤ J ∨ J ≤ I
have neg : ∀ (hI : ¬I = ⊥), I ≤ J ∨ J ≤ I
Tactic: by_cases hI : I = ⊥