awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : IsIntegral R x
y : R
e : (algebraMap R K : (a : R) → K) y = x
pos : y * a = b
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
refine (hb₂ (Ideal.mem_span_singleton'.mpr ⟨y, ?_⟩)).elim

Premises used: Iff.mpr, Ideal.mem_span_singleton', False.elim, Exists.intro
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : IsIntegral R x
y : R
e : (algebraMap R K : (a : R) → K) y = x
pos : Eq (α := K) ((algebraMap R K : (a : R) → K) (y * a) : K) ((algebraMap R K : (a : R) → K) b : K)
⊢ y * a = b

Tactic:
apply IsFractionRing.injective R K

Premises used: IsFractionRing.injective
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : IsIntegral R x
y : R
e : (algebraMap R K : (a : R) → K) y = x
pos :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) ((algebraMap R K : (a : R) → K) a : K) =
    (algebraMap R K : (a : R) → K) b
pos₁ : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) a : K) = (algebraMap R K : (a : R) → K) b
pos₂ pos₃ : Eq (α := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) b : K)
⊢ Eq (α := K) ((algebraMap R K : (a : R) → K) (y * a) : K) ((algebraMap R K : (a : R) → K) b : K)

Tactic:
rw [map_mul, e, div_mul_cancel₀ _ ha₃]

Premises used: div_mul_cancel₀, map_mul
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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
pos : ∃ x ∈ M, x ≠ 0
⊢ M ≠ ⊥

Tactic:
rw [Submodule.ne_bot_iff]

Premises used: Submodule.ne_bot_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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
⊢ ∃ x ∈ M, x ≠ 0

Tactic:
⟨_, ⟨a, ha₁, rfl⟩, ?_⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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
pos : Ne (α := K) ((Algebra.linearMap R K : (a : R) → K) a : K) (0 : K)
⊢ ∃ x ∈ M, x ≠ 0

Tactic:
refine ⟨_, ⟨a, ha₁, rfl⟩, ?_⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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
⊢ Ne (α := K) ((Algebra.linearMap R K : (a : R) → K) a : K) (0 : K)

Tactic:
(IsFractionRing.to_map_eq_zero_iff (K := K)).not.mpr ha₂

Premises used: Iff.mpr, IsFractionRing.to_map_eq_zero_iff, Iff.not, Quotient.mk', OreLocalization.oreDiv
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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
⊢ Ne (α := K) ((Algebra.linearMap R K : (a : R) → K) a : K) (0 : K)

Tactic:
exact (IsFractionRing.to_map_eq_zero_iff (K := K)).not.mpr ha₂

Premises used: Iff.mpr, IsFractionRing.to_map_eq_zero_iff, Iff.not
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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
pos : Submodule.FG (maximalIdeal R)
⊢ M.FG

Tactic:
apply Submodule.FG.map

Premises used: Submodule.FG.map
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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
⊢ Submodule.FG (maximalIdeal R)

Tactic:
IsNoetherian.noetherian _

Premises used: IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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
⊢ Submodule.FG (maximalIdeal R)

Tactic:
exact IsNoetherian.noetherian _

Premises used: IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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
contrapose! :
  ∀ (h : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) ≠ ⊤),
    ∀ y ∈ M, x * y ∈ M
⊢ Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤

Tactic:
contrapose! hx with h
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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)
h : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) ≠ ⊤
m : R
hm : m ∈ (↑(maximalIdeal R) : Set R)
obtain : ∀ (k : R) (hk : k * a = b * m), HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) m : K) ∈ M
⊢ HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) m : K) ∈ M

Tactic:
obtain ⟨k, hk⟩ := hb₃ m hm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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)
h : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) ≠ ⊤
m : R
hm : m ∈ (↑(maximalIdeal R) : Set R)
k : R
hk : k * a = b * m
rw :
  HDiv.hDiv (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) m : K))
      ((algebraMap R K : (a : R) → K) a : K) =
    (algebraMap R K : (a : R) → K) k
rw₁ :
  HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) (b * m) : K) ((algebraMap R K : (a : R) → K) a : K) =
    (algebraMap R K : (a : R) → K) k
rw₂ :
  HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) (k * a) : K) ((algebraMap R K : (a : R) → K) a : K) =
    (algebraMap R K : (a : R) → K) k
rw₃ :
  HDiv.hDiv (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) k : K) ((algebraMap R K : (a : R) → K) a : K))
      ((algebraMap R K : (a : R) → K) a : K) =
    (algebraMap R K : (a : R) → K) k
rw₄ rw₅ : Eq (α := K) ((algebraMap R K : (a : R) → K) k : K) ((algebraMap R K : (a : R) → K) k : K)
⊢ HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) m : K) = (algebraMap R K : (a : R) → K) k

Tactic:
rw [← mul_div_right_comm, ← map_mul, ← hk, map_mul, mul_div_cancel_right₀ _ ha₃]

Premises used: mul_div_right_comm, mul_div_cancel_right₀, map_mul
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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)
h : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) ≠ ⊤
m : R
hm : m ∈ (↑(maximalIdeal R) : Set R)
k : R
hk : k * a = b * m
⊢ HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) m : K) = (algebraMap R K : (a : R) → K) k

Tactic:
have hk' : x * algebraMap R K m = algebraMap R K k := by
        rw [← mul_div_right_comm, ← map_mul, ← hk, map_mul, mul_div_cancel_right₀ _ ha₃]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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)
h : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) ≠ ⊤
m : R
hm : m ∈ (↑(maximalIdeal R) : Set R)
k : R
hk : k * a = b * m
hk' : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) m : K) = (algebraMap R K : (a : R) → K) k
⊢ HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) m : K) ∈ M

Tactic:
⟨k, le_maximalIdeal h ⟨_, ⟨_, hm, rfl⟩, hk'⟩, hk'.symm⟩

Premises used: Set.Mem, setOf, And.intro, IsLocalRing.le_maximalIdeal, Exists.intro, Set.image, Eq.symm, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
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 : ∃ (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 = 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)
h : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) ≠ ⊤
m : R
hm : m ∈ (↑(maximalIdeal R) : Set R)
k : R
hk : k * a = b * m
hk' : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) m : K) = (algebraMap R K : (a : R) → K) k
⊢ HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) m : K) ∈ M

Tactic:
exact ⟨k, le_maximalIdeal h ⟨_, ⟨_, hm, rfl⟩, hk'⟩, hk'.symm⟩