awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : K
h_mono :
  Monotone (α := WithZero (Multiplicative ℤ)) (β := ℝ≥0) (⇑(toNNReal ⋯) : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
rw :
  LE.le (α := ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (x + y)) :
      ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (max (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x)
          (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) y)) :
      ℝ≥0)
⊢ LE.le (α := ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (x + y)) :
      ℝ≥0)
    (max
        ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
          (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x))
        ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
          (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) y)) :
      ℝ≥0)

Tactic:
rw [← h_mono.map_max]

Premises used: Monotone.map_max
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : K
h_mono :
  Monotone (α := WithZero (Multiplicative ℤ)) (β := ℝ≥0) (⇑(toNNReal ⋯) : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
⊢ LE.le (α := ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (x + y)) :
      ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (max (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x)
          (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) y)) :
      ℝ≥0)

Tactic:
h_mono ((v.valuation _).map_add x y)

Premises used: Valuation.map_add, IsDedekindDomain.HeightOneSpectrum.valuation
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : K
h_mono :
  Monotone (α := WithZero (Multiplicative ℤ)) (β := ℝ≥0) (⇑(toNNReal ⋯) : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
⊢ LE.le (α := ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (x + y)) :
      ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (max (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x)
          (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) y)) :
      ℝ≥0)

Tactic:
exact h_mono ((v.valuation _).map_add x y)

Premises used: Valuation.map_add, IsDedekindDomain.HeightOneSpectrum.valuation
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst_2 : Field K
inst_3 : CommSemiring S
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
x x_1 x_2 : K
⊢ (↑(v.adicAbvDef hb (x_1 * x_2)) : ℝ) = (↑(v.adicAbvDef hb x_1) : ℝ) * (↑(v.adicAbvDef hb x_2) : ℝ)

Tactic:
simp [adicAbvDef]

Premises used: IsDedekindDomain.HeightOneSpectrum.adicAbvDef
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst_2 : Field K
inst_3 : CommSemiring S
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
x x_1 : K
⊢ (↑(v.adicAbvDef hb x_1) : ℝ) = 0 ↔ x_1 = 0

Tactic:
simp [adicAbvDef]

Premises used: IsDedekindDomain.HeightOneSpectrum.adicAbvDef
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
⊢ IsNonarchimedean.{0, u_2} (R := ℝ) (α := K) (⇑(v.adicAbv hb) : (a : K) → ℝ)

Tactic:
isNonarchimedean_adicAbvDef v hb

Premises used: IsDedekindDomain.HeightOneSpectrum.adicAbvDef, dite, IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDef, IsNonarchimedean, NNReal.toReal
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
s : ↥(nonZeroDivisors R)
⊢ (v.adicAbv hb : (a : K) → ℝ) (IsLocalization.mk' K r s) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) (↑s : R) : ℝ)

Tactic:
simp [adicAbv, adicAbvDef, intAdicAbv, intAdicAbvDef, valuation_of_algebraMap]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, IsDedekindDomain.HeightOneSpectrum.adicAbvDef, IsDedekindDomain.HeightOneSpectrum.intAdicAbv, IsDedekindDomain.HeightOneSpectrum.adicAbv, IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ Eq (α := ℝ) ((v.adicAbv hb : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) r : K) : ℝ)
    ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ)

Tactic:
simp [adicAbv, adicAbvDef, intAdicAbv, intAdicAbvDef, valuation_of_algebraMap]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, IsDedekindDomain.HeightOneSpectrum.adicAbvDef, IsDedekindDomain.HeightOneSpectrum.intAdicAbv, IsDedekindDomain.HeightOneSpectrum.adicAbv, IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
rw : LE.le (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ)
⊢ LE.le (α := ℝ) ((v.adicAbv hb : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) r : K) : ℝ) (1 : ℝ)

Tactic:
rw [adicAbv_of_algebraMap]

Premises used: IsDedekindDomain.HeightOneSpectrum.adicAbv_of_algebraMap
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ LE.le (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ)

Tactic:
intAdicAbv_le_one v hb r

Premises used: IsDedekindDomain.HeightOneSpectrum.intAdicAbv_le_one
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ LE.le (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ)

Tactic:
exact intAdicAbv_le_one v hb r

Premises used: IsDedekindDomain.HeightOneSpectrum.intAdicAbv_le_one
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
rw : LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∈ v.asIdeal
⊢ LT.lt (α := ℝ) ((v.adicAbv hb : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) r : K) : ℝ) (1 : ℝ) ↔ r ∈ v.asIdeal

Tactic:
rw [adicAbv_of_algebraMap]

Premises used: IsDedekindDomain.HeightOneSpectrum.adicAbv_of_algebraMap
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∈ v.asIdeal

Tactic:
intAdicAbv_lt_one_iff v hb r

Premises used: IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∈ v.asIdeal

Tactic:
exact intAdicAbv_lt_one_iff v hb r

Premises used: IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
rw : Eq (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∉ v.asIdeal
⊢ Eq (α := ℝ) ((v.adicAbv hb : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) r : K) : ℝ) (1 : ℝ) ↔ r ∉ v.asIdeal

Tactic:
rw [adicAbv_of_algebraMap]

Premises used: IsDedekindDomain.HeightOneSpectrum.adicAbv_of_algebraMap
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ Eq (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∉ v.asIdeal

Tactic:
intAdicAbv_eq_one_iff v hb r

Premises used: IsDedekindDomain.HeightOneSpectrum.intAdicAbv_eq_one_iff
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ Eq (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∉ v.asIdeal

Tactic:
exact intAdicAbv_eq_one_iff v hb r

Premises used: IsDedekindDomain.HeightOneSpectrum.intAdicAbv_eq_one_iff
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
𝔭 : HeightOneSpectrum R
x : ℚ
⊢ Function.Injective (β := ℚ) (Function.comp (β := R) (⇑(algebraMap R ℚ) : (a : R) → ℚ) Nat.cast)

Tactic:
simpa using Nat.cast_injective

Premises used: Nat.cast_injective
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
𝔭 : HeightOneSpectrum R
x : ℚ
⊢ CharZero R

Tactic:
have : CharZero R := ⟨.of_comp (f := algebraMap R ℚ) (by simpa using Nat.cast_injective)⟩
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
𝔭 : HeightOneSpectrum R
x : ℚ
this : CharZero R
⊢ Ne.{u_4 + 1} (α := R) (↑x.den : R) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
𝔭 : HeightOneSpectrum R
x : ℚ
this : CharZero R
⊢ Ne.{u_4 + 1} (α := R) (↑x.den : R) 0

Tactic:
have : (x.den : R) ≠ 0 := by simp
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
𝔭 : HeightOneSpectrum R
x : ℚ
this_1 : CharZero R
this : Ne.{u_4 + 1} (α := R) (↑x.den : R) 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((valuation ℚ 𝔭 : (a : ℚ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    (↑x.den : R) ∉ 𝔭.asIdeal

Tactic:
simp [x.num_div_den, ← 𝔭.valuation_div_le_one_iff ℚ x.num this
    (Ideal.IsPrime.notMem_of_isCoprime_of_mem (mod_cast x.isCoprime_num_den.symm.intCast))]

Premises used: Rat.num_div_den, Int.cast, Rat.num, Rat, IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff, Ideal.IsPrime.notMem_of_isCoprime_of_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_4
inst : CommRing R
inst_1 : DimensionLEOne R
p : Ideal R
h : p.IsPrime
hp : p ≠ ⊥
⊢ p.IsMaximal

Tactic:
DimensionLEOne.maximalOfPrime hp h

Premises used: Ring.DimensionLEOne.maximalOfPrime
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
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 : Nontrivial R
inst_4 : IsDomain A
inst_5 : Algebra R A
inst_6 : DimensionLEOne R
⊢ DimensionLEOne.{u_2} ↥(_root_.integralClosure R A)

Tactic:
DimensionLEOne.of_isIntegral R (integralClosure R A)

Premises used: Membership.mem, Subtype, integralClosure, Ring.DimensionLEOne.of_isIntegral
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : DimensionLEOne R
p P : Ideal R
inst_2 : p.IsPrime
inst_3 : P.IsPrime
hpP : p < P
⊢ p = ⊥

Tactic:
by_contra fun hp0 => not_lt_lt ⊥ p P ⟨Ne.bot_lt hp0, hpP⟩

Premises used: Ring.DimensionLEOne.not_lt_lt, Bot.bot, And.intro, by_contra, Ne.bot_lt
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
hA : DimensionLEOne A
e : R ≃+* A
P : Ideal R
hP_ne : P ≠ ⊥
hP_prime : P.IsPrime
rw : IsMaximal (comap e.symm P)
⊢ P.IsMaximal

Tactic:
rw [← Ideal.map_comap_eq_self_of_equiv e.symm P,
      Ideal.isMaximal_map_iff_of_bijective _ e.symm.bijective]

Premises used: Ideal.map_comap_eq_self_of_equiv, Ideal.isMaximal_map_iff_of_bijective, RingEquiv.bijective, RingEquiv.symm
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
hA : DimensionLEOne A
e : R ≃+* A
P : Ideal R
hP_ne : P ≠ ⊥
hP_prime : P.IsPrime
apply : Ne (α := Ideal A) (comap e.symm P) ⊥
⊢ IsMaximal (comap e.symm P)

Tactic:
apply Ring.DimensionLEOne.maximalOfPrime ?_ (P.comap_isPrime e.symm)

Premises used: Ring.DimensionLEOne.maximalOfPrime, Ideal.comap_isPrime, RingEquiv.symm
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
hA : DimensionLEOne A
e : R ≃+* A
P : Ideal R
hP_ne : P ≠ ⊥
hP_prime : P.IsPrime
⊢ Ne (α := Ideal A) (comap e.symm P) ⊥

Tactic:
simp [Ideal.map_eq_bot_iff_of_injective e.injective, hP_ne]

Premises used: RingEquiv.injective, Ideal.map_eq_bot_iff_of_injective
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R_1 : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R_1
inst_1 : CommRing A
inst_2 : Field K
R : Type u_4
inst_3 : CommRing R
inst_4 : DimensionLEOne R
⊢ KrullDimLE 1 R

Tactic:
.mk₁' fun _ hI hI' ↦ hI'.isMaximal hI

Premises used: Ring.KrullDimLE.mk₁', Ideal.IsPrime.isMaximal
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
A : Type u_2
inst : CommRing A
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
⊢ IsDedekindRing A ↔
    IsNoetherianRing A ∧ DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ (y : A), (algebraMap A K : (a : A) → K) y = x

Tactic:
⟨fun _ => ⟨inferInstance, inferInstance,
             fun {_} => (isIntegrallyClosed_iff K).mp inferInstance⟩,
   fun ⟨hr, hd, hi⟩ => { hr, hd, (isIntegrallyClosed_iff K).mpr @hi with }⟩

Premises used: Iff.mpr, inferInstance, _private.0.isDedekindRing_iff.match_1, And.intro, Iff.intro, Iff.mp, IsDedekindRing.mk, isIntegrallyClosed_iff, IsDedekindRing
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
A : Type u_2
inst : CommRing A
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
⊢ IsDedekindDomain A ↔
    IsDomain A ∧
      IsNoetherianRing A ∧
        DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ (y : A), (algebraMap A K : (a : A) → K) y = x

Tactic:
⟨fun _ => ⟨inferInstance, inferInstance, inferInstance,
             fun {_} => (isIntegrallyClosed_iff K).mp inferInstance⟩,
   fun ⟨hid, hr, hd, hi⟩ => { hid, hr, hd, (isIntegrallyClosed_iff K).mpr @hi with }⟩

Premises used: Iff.mpr, inferInstance, IsDedekindDomain.mk, And.intro, Iff.intro, Iff.mp, isIntegrallyClosed_iff, IsDedekindDomain, _private.0.isDedekindDomain_iff.match_1
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
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 : IsPrincipalIdealRing A
⊢ IsDedekindDomain A

Tactic:
{ PrincipalIdealRing.isNoetherianRing, Ring.DimensionLEOne.principal_ideal_ring A,
    UniqueFactorizationMonoid.instIsIntegrallyClosed with }

Premises used: PrincipalIdealRing.isNoetherianRing, Ring.DimensionLEOne.principal_ideal_ring, IsDedekindDomain.mk, UniqueFactorizationMonoid.instIsIntegrallyClosed
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsLocalRing A
inst_3 : IsDedekindDomain A
inst_4 : Algebra R A
inst_5 : FaithfulSMul R A
inst_6 : Module.Finite R A
p : Ideal R
inst_7 : p.IsMaximal
hp0 : p ≠ ⊥
⊢ IsDomain R

Tactic:
have : IsDomain R := .of_faithfulSMul R A
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsLocalRing A
inst_3 : IsDedekindDomain A
inst_4 : Algebra R A
inst_5 : FaithfulSMul R A
inst_6 : Module.Finite R A
p : Ideal R
inst_7 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
⊢ Eq (α := Set (Ideal A)) (p.primesOver A) {maximalIdeal A}

Tactic:
Set.eq_singleton_iff_nonempty_unique_mem.mpr ⟨?_, fun P hP ↦ ?_⟩

Premises used: Iff.mpr, Set.eq_singleton_iff_nonempty_unique_mem, And.intro
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsLocalRing A
inst_3 : IsDedekindDomain A
inst_4 : Algebra R A
inst_5 : FaithfulSMul R A
inst_6 : Module.Finite R A
p : Ideal R
inst_7 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
refine_1 : Set.Nonempty (α := Ideal A) (p.primesOver A)
refine_2 : ∀ (P : Ideal A) (hP : Membership.mem (γ := Set (Ideal A)) (p.primesOver A) P), P = maximalIdeal A
⊢ Eq (α := Set (Ideal A)) (p.primesOver A) {maximalIdeal A}

Tactic:
refine Set.eq_singleton_iff_nonempty_unique_mem.mpr ⟨?_, fun P hP ↦ ?_⟩

Premises used: Iff.mpr, Set.eq_singleton_iff_nonempty_unique_mem, And.intro
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsLocalRing A
inst_3 : IsDedekindDomain A
inst_4 : Algebra R A
inst_5 : FaithfulSMul R A
inst_6 : Module.Finite R A
p : Ideal R
inst_7 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
refine_1 : ∀ (w' : Ideal A) (hmax : w'.IsMaximal) (hover : w'.LiesOver p), Set.Nonempty (α := Ideal A) (p.primesOver A)
⊢ Set.Nonempty (α := Ideal A) (p.primesOver A)

Tactic:
obtain ⟨w', hmax, hover⟩ := exists_maximal_ideal_liesOver_of_isIntegral (S := A) p

Premises used: Ideal.exists_maximal_ideal_liesOver_of_isIntegral
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsLocalRing A
inst_3 : IsDedekindDomain A
inst_4 : Algebra R A
inst_5 : FaithfulSMul R A
inst_6 : Module.Finite R A
p : Ideal R
inst_7 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
w' : Ideal A
hmax : w'.IsMaximal
hover : w'.LiesOver p
⊢ Set.Nonempty (α := Ideal A) (p.primesOver A)

Tactic:
⟨w', hmax.isPrime, hover⟩

Premises used: Ideal.IsMaximal.isPrime, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsLocalRing A
inst_3 : IsDedekindDomain A
inst_4 : Algebra R A
inst_5 : FaithfulSMul R A
inst_6 : Module.Finite R A
p : Ideal R
inst_7 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
w' : Ideal A
hmax : w'.IsMaximal
hover : w'.LiesOver p
⊢ Set.Nonempty (α := Ideal A) (p.primesOver A)

Tactic:
exact ⟨w', hmax.isPrime, hover⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsLocalRing A
inst_3 : IsDedekindDomain A
inst_4 : Algebra R A
inst_5 : FaithfulSMul R A
inst_6 : Module.Finite R A
p : Ideal R
inst_7 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
P : Ideal A
hP : Membership.mem (γ := Set (Ideal A)) (p.primesOver A) P
⊢ P = maximalIdeal A

Tactic:
IsLocalRing.eq_maximalIdeal <| hP.1.isMaximal (Ideal.ne_bot_of_mem_primesOver hp0 hP)

Premises used: Ideal.ne_bot_of_mem_primesOver, Ideal.IsPrime.isMaximal, And.left, IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsLocalRing A
inst_3 : IsDedekindDomain A
inst_4 : Algebra R A
inst_5 : FaithfulSMul R A
inst_6 : Module.Finite R A
p : Ideal R
inst_7 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
P : Ideal A
hP : Membership.mem (γ := Set (Ideal A)) (p.primesOver A) P
⊢ P = maximalIdeal A

Tactic:
exact IsLocalRing.eq_maximalIdeal <| hP.1.isMaximal (Ideal.ne_bot_of_mem_primesOver hp0 hP)

Premises used: Ideal.ne_bot_of_mem_primesOver, Ideal.IsPrime.isMaximal, And.left, IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
I : Submodule B L
c : B
x : L
hx :
  x ∈
    (toAddSubmonoid
        (LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (S := K) (traceForm K L) (restrictScalars A I))).carrier
a : L
ha : Membership.mem (γ := Submodule A L) (restrictScalars A I) a
rw : Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1 ((Algebra.trace K L : (a : L) → K) (x * c • a) : K)
⊢ Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1
    ((((traceForm K L : (a : L) → L →ₗ[K] K) (c • x) : L →ₗ[K] K) : (a : L) → K) a : K)

Tactic:
rw [traceForm_apply, smul_mul_assoc, mul_comm, ← smul_mul_assoc, mul_comm]

Premises used: Algebra.traceForm_apply, smul_mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
I : Submodule B L
c : B
x : L
hx :
  x ∈
    (toAddSubmonoid
        (LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (S := K) (traceForm K L) (restrictScalars A I))).carrier
a : L
ha : Membership.mem (γ := Submodule A L) (restrictScalars A I) a
⊢ Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1 ((Algebra.trace K L : (a : L) → K) (x * c • a) : K)

Tactic:
hx _ (Submodule.smul_mem _ c ha)

Premises used: Set.Mem, Submodule.smul_mem