awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
⊢ Eq.{v + 1} (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
        ((algebraMap A K : (a : A) → K) 0) ⋯ :
      ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    (0 : ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
have a : Eq.{v + 1} (α := K)
  ((↑(Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) 0) sorry) :
      K) :
    K)
  ((↑0 : K) : K)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x x_1 : A
⊢ Subtype.mk (p := fun (x : K) ↦
      Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
      ((algebraMap A K : (a : A) → K) (x + x_1)) ⋯ =
    HAdd.hAdd (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) (β :=
      ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
      (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) x) ⋯ :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
      (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) x_1) ⋯ :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
have a : (↑(Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
        ((algebraMap A K : (a : A) → K) (x + x_1)) sorry) :
    K) =
  (↑(HAdd.hAdd (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) (β :=
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
        (Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
            ((algebraMap A K : (a : A) → K) x) sorry :
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
        (Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
            ((algebraMap A K : (a : A) → K) x_1) sorry :
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))) :
    K)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
⊢ Function.Bijective.{u + 1, v + 1} (α := A) (β := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    (⇑(have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
          {
            toFun := fun (a : A) ↦
              Subtype.mk (p := fun (x : K) ↦
                Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                ((algebraMap A K : (a : A) → K) a) ⋯,
            map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
        this) :
      (a : A) → ↥(valuation A K).integer)
have left : Function.Injective.{u + 1, v + 1} (α := A) (β := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
  (⇑(have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
        {
          toFun := fun (a : A) ↦
            Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) a) sorry,
          map_mul' := sorry, map_zero' := sorry, map_add' := sorry };
      this) :
    (a : A) → ↥(valuation A K).integer)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
left :
  Function.Injective.{u + 1, v + 1} (α := A) (β := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    (⇑(have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
          {
            toFun := fun (a : A) ↦
              Subtype.mk (p := fun (x : K) ↦
                Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                ((algebraMap A K : (a : A) → K) a) ⋯,
            map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
        this) :
      (a : A) → ↥(valuation A K).integer)
⊢ Function.Bijective.{u + 1, v + 1} (α := A) (β := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    (⇑(have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
          {
            toFun := fun (a : A) ↦
              Subtype.mk (p := fun (x : K) ↦
                Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                ((algebraMap A K : (a : A) → K) a) ⋯,
            map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
        this) :
      (a : A) → ↥(valuation A K).integer)
have right : Function.Surjective.{u + 1, v + 1} (α := A) (β := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
  (⇑(have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
        {
          toFun := fun (a : A) ↦
            Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) a) sorry,
          map_mul' := sorry, map_zero' := sorry, map_add' := sorry };
      this) :
    (a : A) → ↥(valuation A K).integer)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x y : A
h :
  Eq.{v + 1} (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
            {
              toFun := fun (a : A) ↦
                Subtype.mk (p := fun (x : K) ↦
                  Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                  ((algebraMap A K : (a : A) → K) a) ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
          this :
          (a : A) → ↥(valuation A K).integer)
        x :
      ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
            {
              toFun := fun (a : A) ↦
                Subtype.mk (p := fun (x : K) ↦
                  Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                  ((algebraMap A K : (a : A) → K) a) ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
          this :
          (a : A) → ↥(valuation A K).integer)
        y :
      ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
⊢ x = y
have h₁ : Eq (α := K)
  ((algebraMap (↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) K : (a : ↥(valuation A K).integer) → K)
      ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
              {
                toFun := fun (a : A) ↦
                  Subtype.mk (p := fun (x : K) ↦
                    Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                    ((algebraMap A K : (a : A) → K) a) sorry,
                map_mul' := sorry, map_zero' := sorry, map_add' := sorry };
            this :
            (a : A) → ↥(valuation A K).integer)
          x :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) :
    K)
  ((algebraMap (↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) K : (a : ↥(valuation A K).integer) → K)
      ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
              {
                toFun := fun (a : A) ↦
                  Subtype.mk (p := fun (x : K) ↦
                    Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                    ((algebraMap A K : (a : A) → K) a) sorry,
                map_mul' := sorry, map_zero' := sorry, map_add' := sorry };
            this :
            (a : A) → ↥(valuation A K).integer)
          y :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) :
    K)
Tactic: apply_fun (algebraMap (valuation A K).integer K) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
val : K
ha : Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) val
⊢ ∃ (a : A),
    (have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
            {
              toFun := fun (a : A) ↦
                Subtype.mk (p := fun (x : K) ↦
                  Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                  ((algebraMap A K : (a : A) → K) a) ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
          this :
          (a : A) → ↥(valuation A K).integer)
        a =
      Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x) val ha
have ha₁ : ∃ (a : A), (algebraMap A K : (a : A) → K) a = val
Tactic: rw [mem_integer_iff] at ha
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
val : K
ha_1 : Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) val
ha : ∃ (a : A), (algebraMap A K : (a : A) → K) a = val
⊢ ∃ (a : A),
    (have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
            {
              toFun := fun (a : A) ↦
                Subtype.mk (p := fun (x : K) ↦
                  Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                  ((algebraMap A K : (a : A) → K) a) ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
          this :
          (a : A) → ↥(valuation A K).integer)
        a =
      Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x) val ha_1
have right : ∀ (a : A)
  (ha :
    Membership.mem (α := K) (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))
      ((algebraMap A K : (a : A) → K) a : K)),
  ∃ (a_1 : A),
    Eq.{v + 1} (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
      ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
              {
                toFun := fun (a : A) ↦
                  Subtype.mk (p := fun (x : K) ↦
                    Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                    ((algebraMap A K : (a : A) → K) a) sorry,
                map_mul' := sorry, map_zero' := sorry, map_add' := sorry };
            this :
            (a : A) → ↥(valuation A K).integer)
          a_1 :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
      (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) a) ha :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
Tactic: obtain ⟨a, rfl⟩ := ha
Cleared hypotheses: val, ha_1, ha
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
⊢ Eq (α := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))
    (RingHom.range.{u, v} (R := A) (algebraMap A K))
have h : ∀ (x : K),
  Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x ↔
    Membership.mem (γ := Subring K) (RingHom.range.{u, v} (R := A) (algebraMap A K)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
a : A
⊢ IsUnit a ∨ IsUnit (1 - a)
have inl : ∀ (c : A) (h : a * c = 1 - a), IsUnit a ∨ IsUnit (1 - a)
Tactic: obtain ⟨c, h | h⟩ := PreValuationRing.cond a (1 - a)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
a : A
inl : ∀ (c : A) (h : a * c = 1 - a), IsUnit a ∨ IsUnit (1 - a)
⊢ IsUnit a ∨ IsUnit (1 - a)
have inr : ∀ (c : A) (h : (1 - a) * c = a), IsUnit a ∨ IsUnit (1 - a)
Tactic: obtain ⟨c, h | h⟩ := PreValuationRing.cond a (1 - a)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
a c : A
h : a * c = 1 - a
⊢ IsUnit a ∨ IsUnit (1 - a)
have inl : IsUnit a
Tactic: left
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
a c : A
h : a * c = 1 - a
⊢ IsUnit a
have inl : a * (c + 1) = 1
Tactic: refine .of_mul_eq_one (c + 1) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
a c : A
h : (1 - a) * c = a
⊢ IsUnit a ∨ IsUnit (1 - a)
have inr : IsUnit (1 - a)
Tactic: right
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
a c : A
h : (1 - a) * c = a
⊢ IsUnit (1 - a)
have inr : (1 - a) * (c + 1) = 1
Tactic: refine .of_mul_eq_one (c + 1) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
⊢ Std.Total fun (x1 x2 : Ideal A) ↦ x1 ≤ x2
have total : ∀ (a b : Ideal A), a ≤ b ∨ b ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
⊢ α ≤ β ∨ β ≤ α
have pos : ∀ (h : ∀ x ∈ α, x ∈ β), α ≤ β ∨ β ≤ α
Tactic: by_cases! h : ∀ x : A, x ∈ α → x ∈ β
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
pos : ∀ (h : ∀ x ∈ α, x ∈ β), α ≤ β ∨ β ≤ α
⊢ α ≤ β ∨ β ≤ α
have neg : ∀ (h : ∃ x ∈ α, x ∉ β), α ≤ β ∨ β ≤ α
Tactic: by_cases! h : ∀ x : A, x ∈ α → x ∈ β
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
h : ∃ x ∈ α, x ∉ β
⊢ α ≤ β ∨ β ≤ α
have neg : ∀ (a : A) (h₁ : a ∈ α) (h₂ : a ∉ β), α ≤ β ∨ β ≤ α
Tactic: obtain ⟨a, h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
⊢ α ≤ β ∨ β ≤ α
have neg : β ≤ α
Tactic: right
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
b : A
hb : b ∈ β
⊢ b ∈ α
have neg : ∀ (c : A) (h : a * c = b), b ∈ α
Tactic: obtain ⟨c, h | h⟩ := PreValuationRing.cond a b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
b : A
hb : b ∈ β
neg : ∀ (c : A) (h : a * c = b), b ∈ α
⊢ b ∈ α
have neg₁ : ∀ (c : A) (h : b * c = a), b ∈ α
Tactic: obtain ⟨c, h | h⟩ := PreValuationRing.cond a b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
b : A
hb : b ∈ β
c : A
h : a * c = b
⊢ b ∈ α
have neg : a * c ∈ α
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
b : A
hb : b ∈ β
c : A
h : b * c = a
⊢ b ∈ α
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
b : A
hb : b ∈ β
c : A
h : b * c = a
⊢ False
have neg : a ∈ β
Tactic: apply h₂
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
b : A
hb : b ∈ β
c : A
h : b * c = a
⊢ a ∈ β
have neg : b * c ∈ β
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : Semigroup R
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
have refine_1 : ∀ (H : PreValuationRing R) (a b : R), a ∣ b ∨ b ∣ a
Tactic: refine ⟨fun H => ⟨fun a b => ?_⟩, fun H => ⟨fun a b => ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : Semigroup R
refine_1 : ∀ (H : PreValuationRing R) (a b : R), a ∣ b ∨ b ∣ a
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
have refine_2 : ∀ (H : Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2) (a b : R), ∃ (c : R), a * c = b ∨ b * c = a
Tactic: refine ⟨fun H => ⟨fun a b => ?_⟩, fun H => ⟨fun a b => ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : Semigroup R
H : PreValuationRing R
a b : R
⊢ a ∣ b ∨ b ∣ a
have refine_1 : ∀ (c : R), a ∣ a * c ∨ a * c ∣ a
Tactic: obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : Semigroup R
H : PreValuationRing R
a b : R
refine_1 : ∀ (c : R), a ∣ a * c ∨ a * c ∣ a
⊢ a ∣ b ∨ b ∣ a
have refine_1₁ : ∀ (c : R), b * c ∣ b ∨ b ∣ b * c
Tactic: obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : Semigroup R
H : Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
a b : R
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have refine_2 : ∀ (c : R), ∃ (c_1 : R), a * c_1 = a * c ∨ a * c * c_1 = a
Tactic: obtain ⟨c, rfl⟩ | ⟨c, rfl⟩ := H.total a b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : Semigroup R
H : Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
a b : R
refine_2 : ∀ (c : R), ∃ (c_1 : R), a * c_1 = a * c ∨ a * c * c_1 = a
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have refine_2₁ : ∀ (c : R), ∃ (c_1 : R), b * c * c_1 = b ∨ b * c_1 = b * c
Tactic: obtain ⟨c, rfl⟩ | ⟨c, rfl⟩ := H.total a b
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : Semigroup R
H : Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
a c : R
⊢ ∃ (c_1 : R), a * c_1 = a * c ∨ a * c * c_1 = a
have h : a * c = a * c ∨ a * c * c = a
Tactic: use c
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : Semigroup R
H : Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
b c : R
⊢ ∃ (c_1 : R), b * c * c_1 = b ∨ b * c_1 = b * c
have h : b * c * c = b ∨ b * c = b * c
Tactic: use c
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : Semigroup R
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
have refine_1 : ∀ (H : PreValuationRing R) (a b : R), a ∣ b ∨ b ∣ a
Tactic: classical
  refine ⟨fun H => ⟨fun a b => ?_⟩, fun H => ⟨fun a b => ?_⟩⟩
  · obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b <;> simp
  · obtain ⟨c, rfl⟩ | ⟨c, rfl⟩ := H.total a b <;> use c <;> simp
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : Semigroup R
refine_1 : ∀ (H : PreValuationRing R) (a b : R), a ∣ b ∨ b ∣ a
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
have refine_2 : ∀ (H : Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2) (a b : R), ∃ (c : R), a * c = b ∨ b * c = a
Tactic: classical
  refine ⟨fun H => ⟨fun a b => ?_⟩, fun H => ⟨fun a b => ?_⟩⟩
  · obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b <;> simp
  · obtain ⟨c, rfl⟩ | ⟨c, rfl⟩ := H.total a b <;> use c <;> simp
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
have refine : ∀ (H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) (a b : R), a ∣ b ∨ b ∣ a
Tactic: refine ⟨fun _ => ⟨le_total⟩, fun H => PreValuationRing.iff_dvd_total.mpr ⟨fun a b => ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
a b : R
⊢ a ∣ b ∨ b ∣ a
have this : LE.le (α := Ideal R) (Ideal.span {a}) (Ideal.span {b}) ∨ LE.le (α := Ideal R) (Ideal.span {b}) (Ideal.span {a})
Tactic: have := H.total (Ideal.span {a}) (Ideal.span {b})
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
a b : R
this : LE.le (α := Ideal R) (Ideal.span {a}) (Ideal.span {b}) ∨ LE.le (α := Ideal R) (Ideal.span {b}) (Ideal.span {a})
⊢ a ∣ b ∨ b ∣ a
have this₁ : b ∣ a ∨ a ∣ b
Tactic: simp_rw [Ideal.span_singleton_le_span_singleton] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
have refine : ∀ (H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) (a b : R), a ∣ b ∨ b ∣ a
Tactic: classical
  refine ⟨fun _ => ⟨le_total⟩, fun H => PreValuationRing.iff_dvd_total.mpr ⟨fun a b => ?_⟩⟩
  have := H.total (Ideal.span {a}) (Ideal.span {b})
  simp_rw [Ideal.span_singleton_le_span_singleton] at this
  exact this.symm