awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = a * b
ha : Membership.mem (γ := Ideal R) (maximalIdeal R) a
hb : Membership.mem (γ := Ideal R) (maximalIdeal R) b
ha₁ : ∃ (a_1 : R), a_1 * ϖ = a
⊢ ∃ (a : R), a * ϖ = b

Tactic:
rw [h, mem_span_singleton'] at ha hb

Premises used: Ideal.mem_span_singleton'
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = a * b
ha : ∃ (a_1 : R), a_1 * ϖ = a
hb : ∃ (a : R), a * ϖ = b
rcases : ∀ (a : R) (hab : ϖ = a * ϖ * b), False
⊢ False

Tactic:
rcases ha with ⟨a, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
b : R
hb : ∃ (a : R), a * ϖ = b
a : R
hab : ϖ = a * ϖ * b
rcases : ∀ (b : R) (hab : ϖ = a * ϖ * (b * ϖ)), False
⊢ False

Tactic:
rcases hb with ⟨b, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = a * ϖ * (b * ϖ)
⊢ a * ϖ * (b * ϖ) = ϖ * (ϖ * (a * b))

Tactic:
ring
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = a * ϖ * (b * ϖ)
⊢ ϖ = ϖ * (ϖ * (a * b))

Tactic:
rw [show a * ϖ * (b * ϖ) = ϖ * (ϖ * (a * b)) by ring] at hab
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = ϖ * (ϖ * (a * b))
apply : ϖ = 0
⊢ False

Tactic:
apply hϖ
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = ϖ * (ϖ * (a * b))
apply : ϖ * (a * b) ≠ 1
⊢ ϖ = 0

Tactic:
apply eq_zero_of_mul_eq_self_right _ hab.symm

Premises used: eq_zero_of_mul_eq_self_right, Eq.symm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = ϖ * (ϖ * (a * b))
⊢ ϖ * (a * b) ≠ 1

Tactic:
fun hh => h2 (isUnit_of_dvd_one ⟨_, hh.symm⟩)

Premises used: HMul.hMul, isUnit_of_dvd_one, Exists.intro, Eq.symm, Not
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = ϖ * (ϖ * (a * b))
⊢ ϖ * (a * b) ≠ 1

Tactic:
exact fun hh => h2 (isUnit_of_dvd_one ⟨_, hh.symm⟩)

Premises used: isUnit_of_dvd_one, Exists.intro
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
e : ϖ = 0
rwa : Eq (α := Ideal R) (span {ϖ}) ⊥
rwa₁ rwa₂ rwa₃ rwa₄ : ϖ = 0
⊢ Eq (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
rwa [h, span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
h : Irreducible ϖ
⊢ Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})

Tactic:
(irreducible_iff_uniformizer _).mp h

Premises used: IsDiscreteValuationRing.irreducible_iff_uniformizer, Iff.mp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
simp_rw : ∃ (ϖ : R), Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
⊢ ∃ (ϖ : R), Irreducible ϖ

Tactic:
simp_rw [irreducible_iff_uniformizer]

Premises used: IsDiscreteValuationRing.irreducible_iff_uniformizer
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ ∃ (ϖ : R), Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})

Tactic:
(IsPrincipalIdealRing.principal <| maximalIdeal R).principal

Premises used: Submodule.IsPrincipal.principal
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ ∃ (ϖ : R), Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})

Tactic:
exact (IsPrincipalIdealRing.principal <| maximalIdeal R).principal

Premises used: Submodule.IsPrincipal.principal
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ ∃ (ϖ : R), Prime ϖ

Tactic:
(exists_irreducible R).imp fun _ => irreducible_iff_prime.1

Premises used: IsDiscreteValuationRing.exists_irreducible, Exists.imp, Iff.mp, irreducible_iff_prime
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
mp : IsDiscreteValuationRing R → IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
mpr : (IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime) → IsDiscreteValuationRing R
⊢ IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime

Tactic:
constructor
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
⊢ IsPrincipalIdealRing R

Tactic:
rcases id RDVR with ⟨Rlocal⟩

Premises used: id
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
⊢ IsLocalRing R

Tactic:
rcases id RDVR with ⟨Rlocal⟩

Premises used: id
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
⊢ Ne (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
rcases id RDVR with ⟨Rlocal⟩

Premises used: id
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
mp : IsPrincipalIdealRing R
mp₁ : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
⊢ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime

Tactic:
constructor
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
⊢ IsPrincipalIdealRing R

Tactic:
assumption
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
h :
  (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R) ∧
    ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R
⊢ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime

Tactic:
use IsLocalRing.maximalIdeal R

Premises used: IsLocalRing.maximalIdeal
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
h : (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R)
h₁ : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R
⊢ (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R) ∧
    ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R

Tactic:
constructor
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
⊢ (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R)

Tactic:
⟨Rlocal, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
⊢ (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R)

Tactic:
exact ⟨Rlocal, inferInstance⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
Q : Ideal R
hQ1 : Q ≠ ⊥
hQ2 : Q.IsPrime
h : ∀ (q : R) (hQ1 : Ne (α := Ideal R) (R ∙ q) ⊥) (hQ2 : IsPrime (R ∙ q)), Eq (α := Ideal R) (R ∙ q) (maximalIdeal R)
⊢ Q = maximalIdeal R

Tactic:
obtain ⟨q, rfl⟩ := (IsPrincipalIdealRing.principal Q).1

Premises used: Submodule.IsPrincipal.principal, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
hQ1 : Ne (α := Ideal R) (R ∙ 0) ⊥
hQ2 : IsPrime (R ∙ 0)
apply : Eq (α := Ideal R) (R ∙ 0) ⊥
⊢ False

Tactic:
apply hQ1
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
hQ1 : Ne (α := Ideal R) (R ∙ 0) ⊥
hQ2 : IsPrime (R ∙ 0)
⊢ Eq (α := Ideal R) (R ∙ 0) ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
q : R
hQ1 : Ne (α := Ideal R) (R ∙ q) ⊥
hQ2 : IsPrime (R ∙ q)
⊢ q ≠ 0

Tactic:
have hq : q ≠ 0 := by
        rintro rfl
        apply hQ1
        simp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
q : R
hQ1 : Ne (α := Ideal R) (R ∙ q) ⊥
hQ2 : IsPrime (R ∙ q)
hq : q ≠ 0
⊢ Prime q

Tactic:
rw [submodule_span_eq, span_singleton_prime hq] at hQ2

Premises used: Ideal.submodule_span_eq, Ideal.span_singleton_prime
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
q : R
hQ1 : Ne (α := Ideal R) (R ∙ q) ⊥
hQ2 : IsPrime (R ∙ q)
hq : q ≠ 0
hQ2₁ : Prime q
⊢ q ≠ 0

Tactic:
rw [submodule_span_eq, span_singleton_prime hq] at hQ2

Premises used: Ideal.submodule_span_eq, Ideal.span_singleton_prime
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
q : R
hQ1 : Ne (α := Ideal R) (R ∙ q) ⊥
hQ2 : Prime q
hq : q ≠ 0
⊢ Irreducible q

Tactic:
replace hQ2 := hQ2.irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
q : R
hQ1 : Ne (α := Ideal R) (R ∙ q) ⊥
hq : q ≠ 0
hQ2 : Irreducible q
⊢ Eq (α := Ideal R) (maximalIdeal R) (span {q})

Tactic:
rw [irreducible_iff_uniformizer] at hQ2

Premises used: IsDiscreteValuationRing.irreducible_iff_uniformizer
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
q : R
hQ1 : Ne (α := Ideal R) (R ∙ q) ⊥
hq : q ≠ 0
hQ2 : Eq (α := Ideal R) (maximalIdeal R) (span {q})
⊢ Eq (α := Ideal R) (R ∙ q) (maximalIdeal R)

Tactic:
hQ2.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
q : R
hQ1 : Ne (α := Ideal R) (R ∙ q) ⊥
hq : q ≠ 0
hQ2 : Eq (α := Ideal R) (maximalIdeal R) (span {q})
⊢ Eq (α := Ideal R) (R ∙ q) (maximalIdeal R)

Tactic:
exact hQ2.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
⊢ IsLocalRing R

Tactic:
haveI : IsLocalRing R := IsLocalRing.of_unique_nonzero_prime Punique
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
this : IsLocalRing R
⊢ IsDiscreteValuationRing R

Tactic:
{ not_a_field' := ?_ }

Premises used: IsDiscreteValuationRing.mk
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
this : IsLocalRing R
mpr : Ne (α := Ideal R) (maximalIdeal R) ⊥
⊢ IsDiscreteValuationRing R

Tactic:
refine { not_a_field' := ?_ }
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
this : IsLocalRing R
mpr :
  ∀ (P : Ideal R),
    (∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P) →
      ∀ (hP1 : P ≠ ⊥) (hP2 : P.IsPrime), Ne (α := Ideal R) (maximalIdeal R) ⊥
⊢ Ne (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
rcases Punique with ⟨P, ⟨hP1, hP2⟩, _⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RPID : IsPrincipalIdealRing R
this : IsLocalRing R
P : Ideal R
right : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hP1 : P ≠ ⊥
hP2 : P.IsPrime
⊢ P ≤ maximalIdeal R

Tactic:
have hPM : P ≤ maximalIdeal R := le_maximalIdeal hP2.1
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RPID : IsPrincipalIdealRing R
this : IsLocalRing R
P : Ideal R
right : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hP1 : P ≠ ⊥
hP2 : P.IsPrime
hPM : P ≤ maximalIdeal R
mpr mpr₁ mpr₂ mpr₃ mpr₄ mpr₅ mpr₆ mpr₇ mpr₈ mpr₉ mpr₁₀ mpr₁₁ : Eq (α := Ideal R) (maximalIdeal R) ⊥ → False
⊢ Ne (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
order
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
ha : Irreducible a
hb : Irreducible b
⊢ Eq (α := Ideal R) (maximalIdeal R) (span {a})

Tactic:
rw [irreducible_iff_uniformizer] at ha hb

Premises used: IsDiscreteValuationRing.irreducible_iff_uniformizer
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
ha : Irreducible a
hb : Irreducible b
ha₁ : Eq (α := Ideal R) (maximalIdeal R) (span {a})
⊢ Eq (α := Ideal R) (maximalIdeal R) (span {b})

Tactic:
rw [irreducible_iff_uniformizer] at ha hb

Premises used: IsDiscreteValuationRing.irreducible_iff_uniformizer
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
ha : Eq (α := Ideal R) (maximalIdeal R) (span {a})
hb : Eq (α := Ideal R) (maximalIdeal R) (span {b})
rw : Eq (α := Ideal R) (span {a}) (span {b})
rw₁ : Eq (α := Ideal R) (maximalIdeal R) (span {b})
rw₂ rw₃ : Eq (α := Ideal R) (span {b}) (span {b})
⊢ Associated a b

Tactic:
rw [← span_singleton_eq_span_singleton, ← ha, hb]

Premises used: Ideal.span_singleton_eq_span_singleton
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
p q : R
hp : Irreducible p
hq : Irreducible q
rcases : ∀ (ϖ : R) (hϖ : Irreducible ϖ) (hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x), Associated p q
⊢ Associated p q

Tactic:
rcases hR with ⟨ϖ, hϖ, hR⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
p q : R
hp : Irreducible p
hq : Irreducible q
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
this : ∀ {p : R}, Irreducible p → Associated p ϖ
⊢ Associated p q

Tactic:
apply Associated.trans (this hp) (this hq).symm

Premises used: Associated.trans, Associated.symm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
p q : R
hp : Irreducible p
hq : Irreducible q
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
suffices : ∀ {p : R}, Irreducible p → Associated p ϖ
⊢ Associated p q

Tactic:
suffices ∀ {p : R} (_ : Irreducible p), Associated p ϖ by
    apply Associated.trans (this hp) (this hq).symm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
obtain : ∀ (n : ℕ) (hn : Associated (ϖ ^ n) p), Associated p ϖ
⊢ Associated p ϖ

Tactic:
obtain ⟨n, hn⟩ := hR hp.ne_zero

Premises used: Irreducible.ne_zero
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
⊢ Irreducible (ϖ ^ n)

Tactic:
have : Irreducible (ϖ ^ n) := hn.symm.irreducible hp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
inl : ∀ (H : n < 1), Associated p ϖ
inr : ∀ (hn : Associated (HPow.hPow (β := ℕ) ϖ 1) p) (this : Irreducible (HPow.hPow (β := ℕ) ϖ 1)), Associated p ϖ
inr₁ : ∀ (H : 1 < n), Associated p ϖ
⊢ Associated p ϖ

Tactic:
rcases lt_trichotomy n 1 with (H | rfl | H)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
H : n < 1
revert : ∀ (n : ℕ) (H : n < 1), n = 0
⊢ n = 0

Tactic:
revert H n
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
⊢ ∀ (n : ℕ) (H : n < 1), n = 0

Tactic:
decide
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : n < 1
⊢ Associated (HPow.hPow (β := ℕ) ϖ 0) p

Tactic:
obtain rfl : n = 0 := by
      clear hn this
      revert H n
      decide

Premises used: rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : n < 1
hn₁ : Associated (HPow.hPow (β := ℕ) ϖ 0) p
⊢ Irreducible (HPow.hPow (β := ℕ) ϖ 0)

Tactic:
obtain rfl : n = 0 := by
      clear hn this
      revert H n
      decide

Premises used: rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : n < 1
hn₁ : Associated (HPow.hPow (β := ℕ) ϖ 0) p
this₁ : Irreducible (HPow.hPow (β := ℕ) ϖ 0)
⊢ LT.lt (α := ℕ) 0 1

Tactic:
obtain rfl : n = 0 := by
      clear hn this
      revert H n
      decide

Premises used: rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
hn : Associated (HPow.hPow (β := ℕ) ϖ 0) p
this : Irreducible (HPow.hPow (β := ℕ) ϖ 0)
H : LT.lt (α := ℕ) 0 1
⊢ Associated p ϖ

Tactic:
simp [not_irreducible_one, pow_zero] at this

Premises used: pow_zero, not_irreducible_one
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
hn : Associated (HPow.hPow (β := ℕ) ϖ 1) p
this : Irreducible (HPow.hPow (β := ℕ) ϖ 1)
⊢ Associated p ϖ

Tactic:
simpa only [pow_one] using hn.symm

Premises used: Associated.symm, pow_one
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : 1 < n
⊢ ∃ (k : ℕ), n = 1 + k + 1

Tactic:
Nat.exists_eq_add_of_lt H

Premises used: Nat.exists_eq_add_of_lt
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : 1 < n
inr :
  ∀ (n : ℕ) (hn : Associated (ϖ ^ (1 + n + 1)) p) (this : Irreducible (ϖ ^ (1 + n + 1))) (H : 1 < 1 + n + 1),
    Associated p ϖ
⊢ Associated p ϖ

Tactic:
obtain ⟨n, rfl⟩ : ∃ k, n = 1 + k + 1 := Nat.exists_eq_add_of_lt H

Premises used: Nat.exists_eq_add_of_lt, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ ^ (1 + n + 1))
H : 1 < 1 + n + 1
⊢ Irreducible (ϖ * ϖ ^ (1 + n))

Tactic:
rw [pow_succ'] at this

Premises used: pow_succ'
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ ^ (1 + n + 1))
H : 1 < 1 + n + 1
this₁ : Irreducible (ϖ * ϖ ^ (1 + n))
⊢ 1 < 1 + n + 1

Tactic:
rw [pow_succ'] at this

Premises used: pow_succ'