awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
refine_1 :
  ∀ (d : Derivation.{u, v, w} R A ↥I),
    Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d))
      (IsScalarTower.toAlgHom R A (B ⧸ I))
⊢ Derivation.{u, v, w} R A ↥I ≃
    { f : A →ₐ[R] B //
      Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
        (IsScalarTower.toAlgHom R A (B ⧸ I)) }
have refine_2 : Function.LeftInverse
  (fun
      (f :
        { f : A →ₐ[R] B //
          Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
            (IsScalarTower.toAlgHom R A (B ⧸ I)) }) ↦
    derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) sorry)
  fun (d : Derivation.{u, v, w} R A ↥I) ↦
  Subtype.mk (p := fun (f : A →ₐ[R] B) ↦
    Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
      (IsScalarTower.toAlgHom R A (B ⧸ I)))
    (liftOfDerivationToSquareZero I hI d) sorry
Tactic: refine ⟨fun d => ⟨liftOfDerivationToSquareZero I hI d, ?_⟩, fun f =>
    (derivationToSquareZeroOfLift I hI f.1 f.2 :), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
refine_1 :
  ∀ (d : Derivation.{u, v, w} R A ↥I),
    Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d))
      (IsScalarTower.toAlgHom R A (B ⧸ I))
refine_2 :
  Function.LeftInverse
    (fun
        (f :
          { f : A →ₐ[R] B //
            Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
              (IsScalarTower.toAlgHom R A (B ⧸ I)) }) ↦
      derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) ⋯)
    fun (d : Derivation.{u, v, w} R A ↥I) ↦
    Subtype.mk (p := fun (f : A →ₐ[R] B) ↦
      Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
        (IsScalarTower.toAlgHom R A (B ⧸ I)))
      (liftOfDerivationToSquareZero I hI d) ⋯
⊢ Derivation.{u, v, w} R A ↥I ≃
    { f : A →ₐ[R] B //
      Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
        (IsScalarTower.toAlgHom R A (B ⧸ I)) }
have refine_3 : Function.RightInverse
  (fun
      (f :
        { f : A →ₐ[R] B //
          Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
            (IsScalarTower.toAlgHom R A (B ⧸ I)) }) ↦
    derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) sorry)
  fun (d : Derivation.{u, v, w} R A ↥I) ↦
  Subtype.mk (p := fun (f : A →ₐ[R] B) ↦
    Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
      (IsScalarTower.toAlgHom R A (B ⧸ I)))
    (liftOfDerivationToSquareZero I hI d) sorry
Tactic: refine ⟨fun d => ⟨liftOfDerivationToSquareZero I hI d, ?_⟩, fun f =>
    (derivationToSquareZeroOfLift I hI f.1 f.2 :), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
d : Derivation.{u, v, w} R A ↥I
⊢ Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d))
    (IsScalarTower.toAlgHom R A (B ⧸ I))
have refine_1 : ∀ (x : A),
  Eq.{w + 1} (α := B ⧸ I)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d) : AlgHom.{u, v, w} R A (B ⧸ I)) :
          (a : A) → B ⧸ I)
        x :
      B ⧸ I)
    ((IsScalarTower.toAlgHom R A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
d : Derivation.{u, v, w} R A ↥I
⊢ (fun
          (f :
            { f : A →ₐ[R] B //
              Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
                (IsScalarTower.toAlgHom R A (B ⧸ I)) }) ↦
        derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) ⋯)
      ((fun (d : Derivation.{u, v, w} R A ↥I) ↦
          (Subtype.mk (p := fun (f : A →ₐ[R] B) ↦
              Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
                (IsScalarTower.toAlgHom R A (B ⧸ I)))
              (liftOfDerivationToSquareZero I hI d) ⋯ :
            { f : A →ₐ[R] B //
              Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
                (IsScalarTower.toAlgHom R A (B ⧸ I)) }))
        d) =
    d
have refine_2 : ∀ (x : A),
  Eq.{w + 1} (α := B)
    (↑((((fun
                    (f :
                      { f : A →ₐ[R] B //
                        Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
                          (IsScalarTower.toAlgHom R A (B ⧸ I)) }) ↦
                  derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) sorry)
                ((fun (d : Derivation.{u, v, w} R A ↥I) ↦
                    (Subtype.mk (p := fun (f : A →ₐ[R] B) ↦
                        Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
                          (IsScalarTower.toAlgHom R A (B ⧸ I)))
                        (liftOfDerivationToSquareZero I hI d) sorry :
                      { f : A →ₐ[R] B //
                        Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
                          (IsScalarTower.toAlgHom R A (B ⧸ I)) }))
                  d) :
              Derivation.{u, v, w} R A ↥I) :
            (a : A) → ↥I)
          x) :
      B)
    (↑((d : (a : A) → ↥I) x) : B)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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 {ϖ})
⊢ Irreducible ϖ
have h2 : ¬IsUnit ϖ
Tactic: have h2 : ¬IsUnit ϖ := show ϖ ∈ maximalIdeal R from h.symm ▸ Submodule.mem_span_singleton_self ϖ
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 ϖ
⊢ Irreducible ϖ
have refine : ∀ ⦃a b : R⦄, ϖ = a * b → IsUnit a ∨ IsUnit b
Tactic: refine ⟨h2, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ IsUnit a ∨ IsUnit b
have by_contra! : ∀ (ha : Membership.mem (γ := Ideal R) (maximalIdeal R) a) (hb : Membership.mem (γ := Ideal R) (maximalIdeal R) b), False
Tactic: by_contra! ⟨ha : a ∈ maximalIdeal R, hb : b ∈ maximalIdeal R⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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
⊢ False
have ha₁ : ∃ (a_1 : R), a_1 * ϖ = a
Tactic: rw [h, mem_span_singleton'] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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
⊢ False
have hb₁ : ∃ (a : R), a * ϖ = b
Tactic: rw [h, mem_span_singleton'] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ False
have rcases : ∀ (a : R) (hab : ϖ = a * ϖ * b), False
Tactic: rcases ha with ⟨a, rfl⟩
Cleared hypotheses: a, hab, ha
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ False
have rcases : ∀ (b : R) (hab : ϖ = a * ϖ * (b * ϖ)), False
Tactic: rcases hb with ⟨b, rfl⟩
Cleared hypotheses: b, hb, hab
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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 * ϖ)
⊢ False
have hab₁ : ϖ = ϖ * (ϖ * (a * b))
Tactic: rw [show a * ϖ * (b * ϖ) = ϖ * (ϖ * (a * b)) by ring] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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))
⊢ False
have apply : ϖ = 0
Tactic: apply hϖ
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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))
⊢ ϖ = 0
have apply : ϖ * (a * b) ≠ 1
Tactic: apply eq_zero_of_mul_eq_self_right _ hab.symm
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ Eq (α := Ideal R) (maximalIdeal R) ⊥
have rwa : Eq (α := Ideal R) (span {ϖ}) ⊥
Tactic: rwa [h, span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ ∃ (ϖ : R), Irreducible ϖ
have simp_rw : ∃ (ϖ : R), Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
Tactic: simp_rw [irreducible_iff_uniformizer]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
have mp : IsDiscreteValuationRing R → IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
mp : IsDiscreteValuationRing R → IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
⊢ IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
have mpr : (IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime) → IsDiscreteValuationRing R
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
⊢ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
have toIsPrincipalIdealRing : IsPrincipalIdealRing R
Tactic: rcases id RDVR with ⟨Rlocal⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
⊢ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
have toIsLocalRing : IsLocalRing R
Tactic: rcases id RDVR with ⟨Rlocal⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing : IsPrincipalIdealRing R
toIsLocalRing : IsLocalRing R
⊢ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
have Rlocal : Ne (α := Ideal R) (maximalIdeal R) ⊥
Tactic: rcases id RDVR with ⟨Rlocal⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
have mp₁ : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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) ⊥
⊢ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
have h : (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R) ∧
  ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R
Tactic: use IsLocalRing.maximalIdeal R
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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) ∧
    ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R
have h : (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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)
⊢ (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R) ∧
    ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R
have h₁ : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ Q = maximalIdeal R
have h : ∀ (q : R) (hQ1 : Ne (α := Ideal R) (R ∙ q) ⊥) (hQ2 : IsPrime (R ∙ q)), Eq (α := Ideal R) (R ∙ q) (maximalIdeal R)
Tactic: obtain ⟨q, rfl⟩ := (IsPrincipalIdealRing.principal Q).1
Cleared hypotheses: Q, hQ1, hQ2
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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)
⊢ False
have apply : Eq (α := Ideal R) (R ∙ 0) ⊥
Tactic: apply hQ1
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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)
⊢ Eq (α := Ideal R) (R ∙ q) (maximalIdeal R)
have hq : q ≠ 0
Tactic: have hq : q ≠ 0 := by
        rintro rfl
        apply hQ1
        simp
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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
⊢ Eq (α := Ideal R) (R ∙ q) (maximalIdeal R)
have hQ2₁ : Prime q
Tactic: rw [submodule_span_eq, span_singleton_prime hq] at hQ2
Cleared hypotheses: hQ2, hq
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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
⊢ Eq (α := Ideal R) (R ∙ q) (maximalIdeal R)
have hQ2₁ : Irreducible q
Tactic: replace hQ2 := hQ2.irreducible
Cleared hypotheses: hQ2
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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) (R ∙ q) (maximalIdeal R)
have hQ2₁ : Eq (α := Ideal R) (maximalIdeal R) (span {q})
Tactic: rw [irreducible_iff_uniformizer] at hQ2
Cleared hypotheses: hQ2
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
⊢ IsDiscreteValuationRing R
have this : IsLocalRing R
Tactic: haveI : IsLocalRing R := IsLocalRing.of_unique_nonzero_prime Punique
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
have mpr : Ne (α := Ideal R) (maximalIdeal R) ⊥
Tactic: refine { not_a_field' := ?_ }
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
this : IsLocalRing R
⊢ Ne (α := Ideal R) (maximalIdeal R) ⊥
have 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) ⊥
Tactic: rcases Punique with ⟨P, ⟨hP1, hP2⟩, _⟩
Cleared hypotheses: Punique
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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
⊢ Ne (α := Ideal R) (maximalIdeal R) ⊥
have hPM : P ≤ maximalIdeal R
Tactic: have hPM : P ≤ maximalIdeal R := le_maximalIdeal hP2.1
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
ha : Irreducible a
hb : Irreducible b
⊢ Associated a b
have ha₁ : Eq (α := Ideal R) (maximalIdeal R) (span {a})
Tactic: rw [irreducible_iff_uniformizer] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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})
⊢ Associated a b
have hb₁ : Eq (α := Ideal R) (maximalIdeal R) (span {b})
Tactic: rw [irreducible_iff_uniformizer] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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})
⊢ Associated a b
have rw : Eq (α := Ideal R) (span {a}) (span {b})
Tactic: rw [← span_singleton_eq_span_singleton, ← ha, hb]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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})
⊢ Associated a b
have rw₂ : Eq (α := Ideal R) (span {b}) (span {b})
Tactic: rw [← span_singleton_eq_span_singleton, ← ha, hb]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
p q : R
hp : Irreducible p
hq : Irreducible q
⊢ Associated p q
have rcases : ∀ (ϖ : R) (hϖ : Irreducible ϖ) (hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x), Associated p q
Tactic: rcases hR with ⟨ϖ, hϖ, hR⟩
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ Associated p q
have suffices : ∀ {p : R}, Irreducible p → Associated p ϖ
Tactic: suffices ∀ {p : R} (_ : Irreducible p), Associated p ϖ by
    apply Associated.trans (this hp) (this hq).symm
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ Associated p ϖ
have obtain : ∀ (n : ℕ) (hn : Associated (ϖ ^ n) p), Associated p ϖ
Tactic: obtain ⟨n, hn⟩ := hR hp.ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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
⊢ Associated p ϖ
have this : Irreducible (ϖ ^ n)
Tactic: have : Irreducible (ϖ ^ n) := hn.symm.irreducible hp
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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)
⊢ Associated p ϖ
have inl : ∀ (H : n < 1), Associated p ϖ
Tactic: rcases lt_trichotomy n 1 with (H | rfl | H)
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 ϖ
⊢ Associated p ϖ
have inr : ∀ (hn : Associated (HPow.hPow (β := ℕ) ϖ 1) p) (this : Irreducible (HPow.hPow (β := ℕ) ϖ 1)), Associated p ϖ
Tactic: rcases lt_trichotomy n 1 with (H | rfl | H)
Cleared hypotheses: n, hn, this