awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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)ˣ
⊢ ∀ (a_1 : HeightOneSpectrum R),
    (↑((RestrictedProduct.unitsEquiv (adicCompletion K) (S := fun (i : HeightOneSpectrum R) ↦
                    ValuationSubring (adicCompletion K i)) :
                  (a :
                      Πʳ (i : HeightOneSpectrum R), [adicCompletion K i,
                          (↑(adicCompletionIntegers K i) : Set (adicCompletion K i))]ˣ) →
                    Πʳ (i : HeightOneSpectrum R), [(adicCompletion K i)ˣ,
                      (↑(Submonoid.ofClass (adicCompletionIntegers K i)).units : Set (adicCompletion K i)ˣ)])
                a) :
            (i : HeightOneSpectrum R) → (adicCompletion K i)ˣ)
          a_1 ∈
        (↑(Submonoid.units
              (Submonoid.ofClass (S := ValuationSubring (adicCompletion K a_1)) (adicCompletionIntegers K a_1))) :
          Set (adicCompletion K a_1)ˣ) →
      Eq (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation (adicCompletion K a_1) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K a_1) → WithZero (Multiplicative ℤ))
            (↑((((RestrictedProduct.unitsEquiv (adicCompletion K) (S := fun (i : HeightOneSpectrum R) ↦
                            ValuationSubring (adicCompletion K i)) :
                          (a :
                              Πʳ (i : HeightOneSpectrum R), [adicCompletion K i,
                                  (↑(adicCompletionIntegers K i) : Set (adicCompletion K i))]ˣ) →
                            Πʳ (i : HeightOneSpectrum R), [(adicCompletion K i)ˣ,
                              (↑(Submonoid.ofClass (adicCompletionIntegers K i)).units : Set (adicCompletion K i)ˣ)])
                        a :
                      Πʳ (i : HeightOneSpectrum R), [(adicCompletion K i)ˣ,
                        (↑(Submonoid.units
                              (Submonoid.ofClass (S := ValuationSubring (adicCompletion K i))
                                (adicCompletionIntegers K i))) :
                          Set (adicCompletion K i)ˣ)]) :
                    (a : HeightOneSpectrum R) → (adicCompletion K a)ˣ)
                  a_1) :
              adicCompletion K a_1) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))

Tactic:
fun _ h ↦
    adicCompletionIntegers.mem_units_iff_valued_eq_one.1 h

Premises used: Iff.mp, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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 : ¬IsUnit a
contrapose! :
  ∀
    (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
⊢ Set.Infinite.{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 ℤ))}

Tactic:
contrapose! ha
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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 ℤ))}
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 ℤ))
⊢ IsUnit a

Tactic:
rw [isUnit_iff]

Premises used: IsDedekindDomain.FiniteAdeleRing.isUnit_iff
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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 ℤ))}
⊢ (∀ (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:
⟨ha₀, ha⟩

Premises used: And.intro
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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 ℤ))}
⊢ (∀ (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:
exact ⟨ha₀, ha⟩
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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
k : Kˣ
⊢ Eq (α := FiniteAdeleRing R K)
    ((↑((unitEmbedding R K : (a : Kˣ) → (FiniteAdeleRing R K)ˣ) k) : FiniteAdeleRing R K) : FiniteAdeleRing R K)
    ((algebraMap K (FiniteAdeleRing R K) : (a : K) → FiniteAdeleRing R K) (↑k : K) : FiniteAdeleRing R K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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
neg : ∀ (hp0 : ¬p = 0), gaussNorm (v.intAdicAbv hb) 1 p ≤ 1
⊢ gaussNorm (v.intAdicAbv hb) 1 p ≤ 1

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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

Tactic:
simp [hp0]
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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

Tactic:
simp [gaussNorm, hp0, intAdicAbv_le_one]

Premises used: IsDedekindDomain.HeightOneSpectrum.intAdicAbv_le_one, Polynomial.gaussNorm
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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
neg : ∀ (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

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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

Tactic:
simp [hp0]
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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
⊢ p.support.Nonempty

Tactic:
grind [support_nonempty]

Premises used: Polynomial.support_nonempty
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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
⊢ p.support.Nonempty

Tactic:
have hsupp_nonempty : p.support.Nonempty := by grind [support_nonempty]
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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 : ℝ)
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal

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]

Premises used: Ideal.span_le, Polynomial.contentIdeal, one_pow, Set.subset_def, reduceDIte, IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff, SetLike.mem_coe, mul_one, Polynomial.gaussNorm
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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 : ℝ)
neg₁ :
  (∀ 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
⊢ 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 : ℝ)

Tactic:
constructor
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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 :
  (∃ 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))
⊢ 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 : ℝ)

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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 :
  ∀ (x : ℕ),
    p.coeff x ≠ 0 →
      LE.le (α := ℝ) (1 : ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x) : ℝ) →
        LE.le (α := ℝ) 1 (p.support.sup' ⋯ fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x))
⊢ (∃ 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))

Tactic:
simp only [mem_coeffs_iff, mem_support_iff, ↓existsAndEq, and_true, forall_exists_index,
      and_imp]

Premises used: and_true, and_imp, forall_exists_index, Polynomial.mem_support_iff, ExistsAndEq.existsAndEq, Polynomial.mem_coeffs_iff
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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 : ℕ
h1 : p.coeff x ≠ 0
h2 : LE.le (α := ℝ) (1 : ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x) : ℝ)
⊢ x ∈ p.support

Tactic:
simp [h1]
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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 : ℕ
h1 : p.coeff x ≠ 0
h2 : LE.le (α := ℝ) (1 : ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x) : ℝ)
⊢ LE.le (α := ℝ) 1 (p.support.sup' ⋯ fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x))

Tactic:
exact Finset.le_sup'_of_le (fun n ↦ (v.intAdicAbv hb) (p.coeff n)) (by simp [h1]) h2

Premises used: Finset.le_sup'_of_le, IsDedekindDomain.HeightOneSpectrum.intAdicAbv, Polynomial.coeff, DFunLike.coe
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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 : ℝ)
neg : ∀ i ∈ p.support, LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) (p.coeff i) : ℝ) (1 : ℝ)
⊢ LT.lt (α := ℝ) (p.support.sup' ⋯ fun (x : ℕ) ↦ (v.intAdicAbv hb : (a : R) → ℝ) (p.coeff x)) 1

Tactic:
rw [Finset.sup'_lt_iff]

Premises used: Finset.sup'_lt_iff
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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
⊢ p.coeff n ≠ 0

Tactic:
rw [mem_support_iff] at hn

Premises used: Polynomial.mem_support_iff
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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 : p.coeff n ≠ 0
⊢ LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) (p.coeff n) : ℝ) (1 : ℝ)

Tactic:
h _ <| p.coeff_mem_coeffs hn

Premises used: Polynomial.coeff_mem_coeffs
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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 : p.coeff n ≠ 0
⊢ LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) (p.coeff n) : ℝ) (1 : ℝ)

Tactic:
exact h _ <| p.coeff_mem_coeffs hn

Premises used: Polynomial.coeff_mem_coeffs
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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
convert_2 : p.contentIdeal = ⊤ ↔ ∀ (x : HeightOneSpectrum R), 1 ≤ gaussNorm (x.intAdicAbv hb) 1 p
⊢ p.contentIdeal = ⊤ ↔ ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1

Tactic:
convert_to _ ↔ ∀ (x : HeightOneSpectrum R), 1 ≤ gaussNorm (x.intAdicAbv hb) 1 p
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
b : NNReal
hb : 1 < b
p : R[X]
hR : ¬IsField R
⊢ (∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1) ↔
    ∀ (x : HeightOneSpectrum R), 1 ≤ gaussNorm (x.intAdicAbv hb) 1 p

Tactic:
grind [gaussNorm_intAdicAbv_le_one]

Premises used: Polynomial.gaussNorm_intAdicAbv_le_one
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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 = ⊤ ↔ ∀ (x : HeightOneSpectrum R), 1 ≤ gaussNorm (x.intAdicAbv hb) 1 p

Tactic:
simp [← not_iff_not, gaussNorm_lt_one_iff_contentIdeal_le, ideal_ne_top_iff_exists hR]

Premises used: not_iff_not, Polynomial.gaussNorm_lt_one_iff_contentIdeal_le, IsDedekindDomain.HeightOneSpectrum.ideal_ne_top_iff_exists
-- Module: Mathlib.RingTheory.DedekindDomain.GaussLemma
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
rw₁ rw₂ :
  (∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1) ↔
    ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1
⊢ p.IsPrimitive ↔ ∀ (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]

Premises used: Polynomial.isPrimitive_iff_contentIdeal_eq_top, Polynomial.contentIdeal_eq_top_iff_forall_gaussNorm_eq_one
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
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

Tactic:
h.toEquiv.forall_congr (fun {x} => ?_)

Premises used: RingEquiv.toEquiv, IsDedekindDomainInv, Equiv.forall_congr
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
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)
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
⊢ IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1

Tactic:
refine h.toEquiv.forall_congr (fun {x} => ?_)

Premises used: RingEquiv.toEquiv, Equiv.forall_congr
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
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)
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
⊢ 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:
rw [← h.toEquiv.apply_eq_iff_eq]

Premises used: RingEquiv.toEquiv, Equiv.apply_eq_iff_eq