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 : ∃ (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.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤

Tactic:
have :
        (M.map (DistribSMul.toLinearMap R K x)).comap (Algebra.linearMap R K) = ⊤ := by
      contrapose! hx with h
      rintro m' ⟨m, hm, rfl : algebraMap R K m = m'⟩
      obtain ⟨k, hk⟩ := hb₃ m hm
      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₃]
      exact ⟨k, le_maximalIdeal h ⟨_, ⟨_, hm, rfl⟩, hk'⟩, hk'.symm⟩
-- 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 : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
⊢ (Algebra.linearMap R K : (a : R) → K) 1 ∈ Submodule.map (DistribSMul.toLinearMap R K x) M

Tactic:
rw [Ideal.eq_top_iff_one, Submodule.mem_comap] at this

Premises used: Submodule.mem_comap, Ideal.eq_top_iff_one
-- 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 : (Algebra.linearMap R K : (a : R) → K) 1 ∈ Submodule.map (DistribSMul.toLinearMap R K x) M
obtain :
  ∀ (y : R) (hy : y ∈ (↑(maximalIdeal R) : Set R))
    (hy' : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) y : K) = (algebraMap R K : (a : R) → K) 1),
    ∃ (y : R), Membership.mem (γ := Ideal R) (maximalIdeal R) y ∧ b * y = a
⊢ ∃ (y : R), Membership.mem (γ := Ideal R) (maximalIdeal R) y ∧ b * y = a

Tactic:
obtain ⟨_, ⟨y, hy, rfl⟩, hy' : x * algebraMap R K y = algebraMap R K 1⟩ := this

Premises used: Algebra.algebraMap, OfNat.ofNat, DFunLike.coe, 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
y : R
hy : y ∈ (↑(maximalIdeal R) : Set R)
hy' : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) y : K) = (algebraMap R K : (a : R) → K) 1
⊢ Eq (α := K) ((algebraMap R K : (a : R) → K) (b * y) : K) ((algebraMap R K : (a : R) → K) a : K)

Tactic:
rw [map_one, ← mul_div_right_comm, div_eq_one_iff_eq ha₃, ← map_mul] at hy'

Premises used: div_eq_one_iff_eq, mul_div_right_comm, map_mul, map_one
-- 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
y : R
hy : y ∈ (↑(maximalIdeal R) : Set R)
hy' : Eq (α := K) ((algebraMap R K : (a : R) → K) (b * y) : K) ((algebraMap R K : (a : R) → K) a : K)
⊢ ∃ (y : R), Membership.mem (γ := Ideal R) (maximalIdeal R) y ∧ b * y = a

Tactic:
⟨y, hy, IsFractionRing.injective R K hy'⟩

Premises used: IsFractionRing.injective, And.intro, 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 : ∃ (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
y : R
hy : y ∈ (↑(maximalIdeal R) : Set R)
hy' : Eq (α := K) ((algebraMap R K : (a : R) → K) (b * y) : K) ((algebraMap R K : (a : R) → K) a : K)
⊢ ∃ (y : R), Membership.mem (γ := Ideal R) (maximalIdeal R) y ∧ b * y = a

Tactic:
exact ⟨y, hy, IsFractionRing.injective R K hy'⟩
-- 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 : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
neg :
  ∀ (y : R) (hy₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) y) (hy₂ : b * y = a),
    Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
obtain ⟨y, hy₁, hy₂⟩ : ∃ y ∈ maximalIdeal R, b * y = a := by
      rw [Ideal.eq_top_iff_one, Submodule.mem_comap] at this
      obtain ⟨_, ⟨y, hy, rfl⟩, hy' : x * algebraMap R K y = algebraMap R K 1⟩ := this
      rw [map_one, ← mul_div_right_comm, div_eq_one_iff_eq ha₃, ← map_mul] at hy'
      exact ⟨y, hy, IsFractionRing.injective R K hy'⟩

Premises used: IsLocalRing.maximalIdeal
-- 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 : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) y
hy₂ : b * y = a
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
⟨⟨y, ?_⟩⟩

Premises used: Submodule.IsPrincipal.mk, 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 : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) y
hy₂ : b * y = a
neg : Eq (α := Submodule R R) (maximalIdeal R) (R ∙ y)
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
refine ⟨⟨y, ?_⟩⟩
-- 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 : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) y
hy₂ : b * y = a
neg : LE.le (α := Submodule R R) (maximalIdeal R) (R ∙ y)
neg₁ : LE.le (α := Submodule R R) (R ∙ y) (maximalIdeal R)
⊢ Eq (α := Submodule R R) (maximalIdeal R) (R ∙ y)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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 : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) y
hy₂ : b * y = a
m : R
hm : Membership.mem (γ := Submodule R R) (maximalIdeal R) m
neg : ∀ (k : R) (hk : k * a = b * m), Membership.mem (γ := Submodule R R) (R ∙ y) m
⊢ Membership.mem (γ := Submodule R R) (R ∙ y) 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_2 : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this_2 = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) y
hy₂ : b * y = a
m : R
hm : Membership.mem (γ := Submodule R R) (maximalIdeal R) m
k : R
hk : k * a = b * m
⊢ b * (y * k) = b * m

Tactic:
rw [← hy₂, mul_comm, mul_assoc] at hk

Premises used: mul_assoc, mul_comm
-- 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 : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) y
hy₂ : b * y = a
m : R
hm : Membership.mem (γ := Submodule R R) (maximalIdeal R) m
k : R
hk : b * (y * k) = b * m
neg : Membership.mem (γ := Submodule R R) (R ∙ y) (k * y)
⊢ Membership.mem (γ := Submodule R R) (R ∙ y) m

Tactic:
rw [← mul_left_cancel₀ hb₄ hk, mul_comm]

Premises used: mul_left_cancel₀, mul_comm
-- 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 : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) y
hy₂ : b * y = a
m : R
hm : Membership.mem (γ := Submodule R R) (maximalIdeal R) m
k : R
hk : b * (y * k) = b * m
⊢ Membership.mem (γ := Submodule R R) (R ∙ y) (k * y)

Tactic:
Ideal.mem_span_singleton'.mpr ⟨_, rfl⟩

Premises used: Iff.mpr, Ideal.mem_span_singleton', Set.Mem, 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_2 : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this_2 = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) y
hy₂ : b * y = a
m : R
hm : Membership.mem (γ := Submodule R R) (maximalIdeal R) m
k : R
hk : b * (y * k) = b * m
⊢ Membership.mem (γ := Submodule R R) (R ∙ y) (k * y)

Tactic:
exact Ideal.mem_span_singleton'.mpr ⟨_, rfl⟩

Premises used: Iff.mpr, Ideal.mem_span_singleton', Exists.intro, rfl