awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
a : FiniteAdeleRing R K
ha₀ : ∀ (v : HeightOneSpectrum R), (a : (a : HeightOneSpectrum R) → adicCompletion K a) v ≠ 0
ha :
  Set.Finite.{u_1} (α := HeightOneSpectrum R)
    {v : HeightOneSpectrum R |
      Ne (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
            ((a : (a : HeightOneSpectrum R) → adicCompletion K a) v) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))}
⊢ IsUnit a
have rw : (∀ (v : HeightOneSpectrum R), (a : (a : HeightOneSpectrum R) → adicCompletion K a) v ≠ 0) ∧
  ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          ((a : (a : HeightOneSpectrum R) → adicCompletion K a) v) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
Tactic: rw [isUnit_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
⊢ gaussNorm (v.intAdicAbv hb) 1 p ≤ 1
have pos : ∀ (hp0 : p = 0), gaussNorm (v.intAdicAbv hb) 1 p ≤ 1
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
pos : ∀ (hp0 : p = 0), gaussNorm (v.intAdicAbv hb) 1 p ≤ 1
⊢ gaussNorm (v.intAdicAbv hb) 1 p ≤ 1
have neg : ∀ (hp0 : ¬p = 0), gaussNorm (v.intAdicAbv hb) 1 p ≤ 1
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal
have pos : ∀ (hp0 : p = 0), gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
pos : ∀ (hp0 : p = 0), gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal
have neg : ∀ (hp0 : ¬p = 0), gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal
have hsupp_nonempty : p.support.Nonempty
Tactic: have hsupp_nonempty : p.support.Nonempty := by grind [support_nonempty]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal
have neg : LT.lt (α := ℝ) (p.support.sup' sorry fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x)) 1 ↔
  ∀ x ∈ p.coeffs, LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) x : ℝ) (1 : ℝ)
Tactic: simp only [gaussNorm, hsupp_nonempty, ↓reduceDIte, one_pow, mul_one, contentIdeal, Ideal.span_le,
    Set.subset_def, SetLike.mem_coe, ← v.intAdicAbv_lt_one_iff hb]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ LT.lt (α := ℝ) (p.support.sup' ⋯ fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x)) 1 ↔
    ∀ x ∈ p.coeffs, LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) x : ℝ) (1 : ℝ)
have neg : LT.lt (α := ℝ) (p.support.sup' sorry fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x)) 1 →
  ∀ x ∈ p.coeffs, LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) x : ℝ) (1 : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
neg :
  LT.lt (α := ℝ) (p.support.sup' ⋯ fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x)) 1 →
    ∀ x ∈ p.coeffs, LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) x : ℝ) (1 : ℝ)
⊢ LT.lt (α := ℝ) (p.support.sup' ⋯ fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x)) 1 ↔
    ∀ x ∈ p.coeffs, LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) x : ℝ) (1 : ℝ)
have neg₁ : (∀ x ∈ p.coeffs, LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) x : ℝ) (1 : ℝ)) →
  LT.lt (α := ℝ) (p.support.sup' sorry fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x)) 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ LT.lt (α := ℝ) (p.support.sup' ⋯ fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x)) 1 →
    ∀ x ∈ p.coeffs, LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) x : ℝ) (1 : ℝ)
have neg : (∃ x ∈ p.coeffs, LE.le (α := ℝ) (1 : ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) x : ℝ)) →
  LE.le (α := ℝ) 1 (p.support.sup' sorry fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x))
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ (∃ x ∈ p.coeffs, LE.le (α := ℝ) (1 : ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) x : ℝ)) →
    LE.le (α := ℝ) 1 (p.support.sup' ⋯ fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x))
have neg : ∀ (x : ℕ),
  p.coeff x ≠ 0 →
    LE.le (α := ℝ) (1 : ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x) : ℝ) →
      LE.le (α := ℝ) 1 (p.support.sup' sorry fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x))
Tactic: simp only [mem_coeffs_iff, mem_support_iff, ↓existsAndEq, and_true, forall_exists_index,
      and_imp]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
h : ∀ x ∈ p.coeffs, LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) x : ℝ) (1 : ℝ)
⊢ LT.lt (α := ℝ) (p.support.sup' ⋯ fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x)) 1
have neg : ∀ i ∈ p.support, LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) (p.coeff i) : ℝ) (1 : ℝ)
Tactic: rw [Finset.sup'_lt_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
h : ∀ x ∈ p.coeffs, LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) x : ℝ) (1 : ℝ)
n : ℕ
hn : n ∈ p.support
⊢ LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) (p.coeff n) : ℝ) (1 : ℝ)
have hn₁ : p.coeff n ≠ 0
Tactic: rw [mem_support_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
b : NNReal
hb : 1 < b
p : R[X]
hR : ¬IsField R
⊢ p.contentIdeal = ⊤ ↔ ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1
have h : (∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1) ↔
  ∀ (x : HeightOneSpectrum R), 1 ≤ gaussNorm (x.intAdicAbv hb) 1 p
Tactic: convert_to _ ↔ ∀ (x : HeightOneSpectrum R), 1 ≤ gaussNorm (x.intAdicAbv hb) 1 p
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
b : NNReal
hb : 1 < b
p : R[X]
hR : ¬IsField R
h :
  (∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1) ↔
    ∀ (x : HeightOneSpectrum R), 1 ≤ gaussNorm (x.intAdicAbv hb) 1 p
⊢ p.contentIdeal = ⊤ ↔ ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1
have convert_2 : p.contentIdeal = ⊤ ↔ ∀ (x : HeightOneSpectrum R), 1 ≤ gaussNorm (x.intAdicAbv hb) 1 p
Tactic: convert_to _ ↔ ∀ (x : HeightOneSpectrum R), 1 ≤ gaussNorm (x.intAdicAbv hb) 1 p
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
hR : ¬IsField R
b : NNReal
hb : 1 < b
p : R[X]
⊢ p.IsPrimitive ↔ ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1
have rw : p.contentIdeal = ⊤ ↔ ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1
Tactic: rw [isPrimitive_iff_contentIdeal_eq_top, p.contentIdeal_eq_top_iff_forall_gaussNorm_eq_one hb hR]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.GaussLemma (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
hR : ¬IsField R
b : NNReal
hb : 1 < b
p : R[X]
rw : p.contentIdeal = ⊤ ↔ ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1
⊢ p.IsPrimitive ↔ ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1
have rw₁ : (∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1) ↔
  ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1
Tactic: rw [isPrimitive_iff_contentIdeal_eq_top, p.contentIdeal_eq_top_iff_forall_gaussNorm_eq_one hb hR]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
h : RingEquiv.{u_2, u_3} (FractionalIdeal (R := A) A⁰ (FractionRing A)) (FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) :=
  mapEquiv (FractionRing.algEquiv A K)
⊢ IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1
have refine : ∀ {x : FractionalIdeal (R := A) A⁰ (FractionRing A)},
  x ≠ ⊥ → x * x⁻¹ = 1 ↔
    Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        ((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) x :
          FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (⊥ : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) →
      HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          ((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) x :
            FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) x)⁻¹ :
            FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) =
        1
Tactic: refine h.toEquiv.forall_congr (fun {x} => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
h : RingEquiv.{u_2, u_3} (FractionalIdeal (R := A) A⁰ (FractionRing A)) (FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) :=
  mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal (R := A) A⁰ (FractionRing A)
⊢ x ≠ ⊥ → x * x⁻¹ = 1 ↔
    Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        ((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) x :
          FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (⊥ : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) →
      HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          ((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) x :
            FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) x)⁻¹ :
            FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) =
        1
have rw : x ≠ ⊥ →
    Eq.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
      ((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) (x * x⁻¹) :
        FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
      ((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) 1 :
        FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↔
  Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
      ((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) x :
        FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
      (⊥ : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) →
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        ((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) x :
          FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) x)⁻¹ :
          FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) =
      1
Tactic: rw [← h.toEquiv.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
hI : IsUnit (M := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (adjoinIntegral A⁰ x hx)
⊢ Eq (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (adjoinIntegral A⁰ x hx) 1
have set : let I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx;
∀ (hI : IsUnit I), I = 1
Tactic: set I := adjoinIntegral A⁰ x hx
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
⊢ IsIdempotentElem I
have a : Eq.{u_3 + 1} (α := Submodule A K) ((fun (I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦ (↑I : Submodule A K)) (I * I))
  ((fun (I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦ (↑I : Submodule A K)) I)
Tactic: apply coeToSubmodule_injective
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
⊢ Eq.{u_3 + 1} (α := Submodule A K)
    ((fun (I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦ (↑I : Submodule A K)) (I * I))
    ((fun (I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦ (↑I : Submodule A K)) I)
have a : HMul.hMul (α := Submodule A K) (β := Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x] : Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x] : Submodule A K) =
  (Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x]
Tactic: simp only [coe_mul, adjoinIntegral_coe, I]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
⊢ HMul.hMul (α := Submodule A K) (β := Submodule A K)
      ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x] : Submodule A K)
      ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x] : Submodule A K) =
    (Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x]
have a : Eq (α := Submodule A K) ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x] : Submodule A K)
  ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x] : Submodule A K)
Tactic: rw [(Algebra.adjoin A {x}).isIdempotentElem_toSubmodule]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
⊢ I = 1
have mul_self : IsIdempotentElem I
Tactic: have mul_self : IsIdempotentElem I := by
    apply coeToSubmodule_injective
    simp only [coe_mul, adjoinIntegral_coe, I]
    rw [(Algebra.adjoin A {x}).isIdempotentElem_toSubmodule]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ I = 1
have h : I = I * I * I⁻¹
Tactic: convert! congr_arg (· * I⁻¹) mul_self
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
h : I = I * I * I⁻¹
⊢ I = 1
have h₁ : 1 = I * I⁻¹
Tactic: convert! congr_arg (· * I⁻¹) mul_self
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
⊢ I / J = I * J⁻¹
have inl : I / 0 = I * 0⁻¹
Tactic: obtain rfl | hJ := eq_or_ne J 0
Cleared hypotheses: J
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
inl : I / 0 = I * 0⁻¹
⊢ I / J = I * J⁻¹
have inr : ∀ (hJ : J ≠ 0), I / J = I * J⁻¹
Tactic: obtain rfl | hJ := eq_or_ne J 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
⊢ I / J = I * J⁻¹
have inr : I / J ≤ I * J⁻¹
Tactic: refine le_antisymm ?_ ((FractionalIdeal.le_div_iff_mul_le hJ).2 ?_)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
inr : I / J ≤ I * J⁻¹
⊢ I / J = I * J⁻¹
have inr₁ : I * J⁻¹ * J ≤ I
Tactic: refine le_antisymm ?_ ((FractionalIdeal.le_div_iff_mul_le hJ).2 ?_)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
⊢ I / J ≤ I * J⁻¹
have inr : I / J * J ≤ I
Tactic: suffices I / J * J ≤ I by
        simpa [mul_assoc, isDedekindDomainInv_iff.mp h _ hJ] using mul_left_mono (a := J⁻¹) this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
⊢ I * J⁻¹ * J ≤ I
have inr : I * (J⁻¹ * J) ≤ I
Tactic: rw [mul_assoc, mul_comm _ J, isDedekindDomainInv_iff.mp h _ hJ, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
inr : I * (J⁻¹ * J) ≤ I
⊢ I * J⁻¹ * J ≤ I
have inr₁ : I * (J * J⁻¹) ≤ I
Tactic: rw [mul_assoc, mul_comm _ J, isDedekindDomainInv_iff.mp h _ hJ, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
inr : I * (J⁻¹ * J) ≤ I
inr₁ : I * (J * J⁻¹) ≤ I
⊢ I * J⁻¹ * J ≤ I
have inr₂ : I * 1 ≤ I
Tactic: rw [mul_assoc, mul_comm _ J, isDedekindDomainInv_iff.mp h _ hJ, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
inr : I * (J⁻¹ * J) ≤ I
inr₁ : I * (J * J⁻¹) ≤ I
inr₂ : I * 1 ≤ I
⊢ I * J⁻¹ * J ≤ I
have inr₃ : I ≤ I
Tactic: rw [mul_assoc, mul_comm _ J, isDedekindDomainInv_iff.mp h _ hJ, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
⊢ IsNoetherianRing A
have refine : ∀ (I : Ideal A), Submodule.FG I
Tactic: refine isNoetherianRing_iff.mpr ⟨fun I : Ideal A => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
I : Ideal A
⊢ Submodule.FG I
have pos : ∀ (hI : I = ⊥), Submodule.FG I
Tactic: by_cases hI : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
I : Ideal A
pos : ∀ (hI : I = ⊥), Submodule.FG I
⊢ Submodule.FG I
have neg : ∀ (hI : ¬I = ⊥), Submodule.FG I
Tactic: by_cases hI : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
I : Ideal A
hI : I = ⊥
⊢ Submodule.FG I
have pos : Submodule.FG.{u_2, u_2} (R := A) (M := A) ⊥
Tactic: rw [hI]