awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
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) ⋯,
                map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
            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:
exact ⟨a, rfl⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
a : A
⊢ Eq.{v + 1} (α := K)
    ((↑(((equivInteger A K : RingEquiv.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) :
              (a : A) → ↥(valuation A K).integer)
            a) :
        K) :
      K)
    ((algebraMap A K : (a : A) → K) a : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
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
⊢ Eq (α := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))
    (RingHom.range.{u, v} (R := A) (algebraMap A K))

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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 : 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:
mem_integer_iff _ _ _

Premises used: ValuationRing.mem_integer_iff, Set.Mem, setOf, Set.range
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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 : 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:
exact mem_integer_iff _ _ _

Premises used: ValuationRing.mem_integer_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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)
inr : ∀ (c : A) (h : (1 - a) * c = a), IsUnit a ∨ IsUnit (1 - a)
⊢ IsUnit a ∨ IsUnit (1 - a)

Tactic:
obtain ⟨c, h | h⟩ := PreValuationRing.cond a (1 - a)

Premises used: PreValuationRing.cond, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
a c : A
h : a * c = 1 - a
inl : IsUnit a
⊢ IsUnit a ∨ IsUnit (1 - a)

Tactic:
left
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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

Tactic:
.of_mul_eq_one (c + 1) ?_

Premises used: IsUnit.of_mul_eq_one, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
a c : A
h : a * c = 1 - a
inl : a * (c + 1) = 1
⊢ IsUnit a

Tactic:
refine .of_mul_eq_one (c + 1) ?_
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
a c : A
h : a * c = 1 - a
⊢ a * (c + 1) = 1

Tactic:
simp [mul_add, h]

Premises used: mul_add
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
a c : A
h : (1 - a) * c = a
inr : IsUnit (1 - a)
⊢ IsUnit a ∨ IsUnit (1 - a)

Tactic:
right
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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)

Tactic:
.of_mul_eq_one (c + 1) ?_

Premises used: IsUnit.of_mul_eq_one, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
a c : A
h : (1 - a) * c = a
inr : (1 - a) * (c + 1) = 1
⊢ IsUnit (1 - a)

Tactic:
refine .of_mul_eq_one (c + 1) ?_
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
a c : A
h : (1 - a) * c = a
⊢ (1 - a) * (c + 1) = 1

Tactic:
simp [mul_add, h]

Premises used: mul_add
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
total : ∀ (a b : Ideal A), a ≤ b ∨ b ≤ a
⊢ Std.Total fun (x1 x2 : Ideal A) ↦ x1 ≤ x2

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
pos : ∀ (h : ∀ x ∈ α, x ∈ β), α ≤ β ∨ β ≤ α
neg : ∀ (h : ∃ x ∈ α, x ∉ β), α ≤ β ∨ β ≤ α
⊢ α ≤ β ∨ β ≤ α

Tactic:
by_cases! h : ∀ x : A, x ∈ α → x ∈ β
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
h : ∀ x ∈ α, x ∈ β
⊢ α ≤ β ∨ β ≤ α

Tactic:
Or.inl h

Premises used: Or.inl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
h : ∀ x ∈ α, x ∈ β
⊢ α ≤ β ∨ β ≤ α

Tactic:
exact Or.inl h

Premises used: Or.inl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
h : ∃ x ∈ α, x ∉ β
neg : ∀ (a : A) (h₁ : a ∈ α) (h₂ : a ∉ β), α ≤ β ∨ β ≤ α
⊢ α ≤ β ∨ β ≤ α

Tactic:
obtain ⟨a, h₁, h₂⟩ := h
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
inst_2 : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
neg : β ≤ α
⊢ α ≤ β ∨ β ≤ α

Tactic:
right
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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 ∈ α
neg₁ : ∀ (c : A) (h : b * c = a), b ∈ α
⊢ b ∈ α

Tactic:
obtain ⟨c, h | h⟩ := PreValuationRing.cond a b

Premises used: PreValuationRing.cond
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
neg : a * c ∈ α
⊢ b ∈ α

Tactic:
rw [← h]
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
⊢ a * c ∈ α

Tactic:
Ideal.mul_mem_right _ _ h₁

Premises used: Set.Mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
⊢ a * c ∈ α

Tactic:
exact Ideal.mul_mem_right _ _ h₁

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
neg : False
⊢ b ∈ α

Tactic:
exfalso
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
neg : a ∈ β
⊢ False

Tactic:
apply h₂
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
neg : b * c ∈ β
⊢ a ∈ β

Tactic:
rw [← h]
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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 * c ∈ β

Tactic:
apply Ideal.mul_mem_right _ _ hb

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : Semigroup R
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2

Tactic:
⟨fun H => ⟨fun a b => ?_⟩, fun H => ⟨fun a b => ?_⟩⟩

Premises used: PreValuationRing.mk, Iff.intro, Std.Total.mk
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : Semigroup R
refine_1 : ∀ (H : PreValuationRing R) (a b : R), a ∣ b ∨ b ∣ a
refine_2 : ∀ (H : Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2) (a b : R), ∃ (c : R), a * c = b ∨ b * c = a
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2

Tactic:
refine ⟨fun H => ⟨fun a b => ?_⟩, fun H => ⟨fun a b => ?_⟩⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : Semigroup R
H : PreValuationRing R
a b : R
refine_1 : ∀ (c : R), a ∣ a * c ∨ a * c ∣ a
refine_1₁ : ∀ (c : R), b * c ∣ b ∨ b ∣ b * c
⊢ a ∣ b ∨ b ∣ a

Tactic:
obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b

Premises used: PreValuationRing.cond, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : Semigroup R
H : PreValuationRing R
a c : R
⊢ a ∣ a * c ∨ a * c ∣ a

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : Semigroup R
H : PreValuationRing R
b c : R
⊢ b * c ∣ b ∨ b ∣ b * c

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
refine_2₁ : ∀ (c : R), ∃ (c_1 : R), b * c * c_1 = b ∨ b * c_1 = b * c
⊢ ∃ (c : R), a * c = b ∨ b * c = a

Tactic:
obtain ⟨c, rfl⟩ | ⟨c, rfl⟩ := H.total a b

Premises used: Std.Total.total, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : Semigroup R
H : Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
a c : R
h : a * c = a * c ∨ a * c * c = a
⊢ ∃ (c_1 : R), a * c_1 = a * c ∨ a * c * c_1 = a

Tactic:
use c
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : Semigroup R
H : Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
b c : R
h : b * c * c = b ∨ b * c = b * c
⊢ ∃ (c_1 : R), b * c * c_1 = b ∨ b * c_1 = b * c

Tactic:
use c
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : Semigroup R
H : Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
a c : R
⊢ a * c = a * c ∨ a * c * c = a

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : Semigroup R
H : Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
b c : R
⊢ b * c * c = b ∨ b * c = b * c

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : Semigroup R
refine_1 : ∀ (H : PreValuationRing R) (a b : R), a ∣ b ∨ b ∣ a
refine_2 refine_2₁ : ∀ (H : Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2) (a b : R), ∃ (c : R), a * c = b ∨ b * c = a
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2

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

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2

Tactic:
⟨fun _ => ⟨le_total⟩, fun H => PreValuationRing.iff_dvd_total.mpr ⟨fun a b => ?_⟩⟩

Premises used: Iff.mpr, PreValuationRing.iff_dvd_total, le_total, Iff.intro, Std.Total.mk
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
refine : ∀ (H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) (a b : R), a ∣ b ∨ b ∣ a
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2

Tactic:
refine ⟨fun _ => ⟨le_total⟩, fun H => PreValuationRing.iff_dvd_total.mpr ⟨fun a b => ?_⟩⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
a b : R
⊢ 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})
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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})
⊢ b ∣ a ∨ a ∣ b

Tactic:
simp_rw [Ideal.span_singleton_le_span_singleton] at this

Premises used: Ideal.span_singleton_le_span_singleton
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
a b : R
this : b ∣ a ∨ a ∣ b
⊢ a ∣ b ∨ b ∣ a

Tactic:
this.symm

Premises used: Or.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
a b : R
this : b ∣ a ∨ a ∣ b
⊢ a ∣ b ∨ b ∣ a

Tactic:
exact this.symm

Premises used: Or.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
refine : ∀ (H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) (a b : R), a ∣ b ∨ b ∣ a
refine₁ :
  ∀ (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
refine₂ : ∀ (H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) (a b : R) (this : b ∣ a ∨ a ∣ b), a ∣ b ∨ b ∣ a
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2

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

Premises used: Ideal.span_singleton_le_span_singleton
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : Semigroup R
h : PreValuationRing R
x y : R
⊢ x ∣ y ∨ y ∣ x

Tactic:
(PreValuationRing.iff_dvd_total.mp h).total x y

Premises used: Std.Total.total
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2

Tactic:
Iff.trans (⟨fun inst ↦ inst.toPreValuationRing, fun _ ↦ .mk⟩)
    PreValuationRing.iff_dvd_total

Premises used: ValuationRing.toPreValuationRing, PreValuationRing.iff_dvd_total, Iff.intro, Iff.trans, ValuationRing.mk
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ ValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2

Tactic:
Iff.trans (⟨fun inst ↦ inst.toPreValuationRing, fun _ ↦ .mk⟩)
    PreValuationRing.iff_ideal_total

Premises used: ValuationRing.toPreValuationRing, PreValuationRing.iff_ideal_total, Iff.intro, Iff.trans, ValuationRing.mk
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : PreValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
⊢ p ∣ q ∨ q ∣ p

Tactic:
have := dvd_total p q
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : PreValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : p ∣ q ∨ q ∣ p
⊢ q ∣ p

Tactic:
rw [Irreducible.dvd_comm hp hq, or_self_iff] at this

Premises used: Irreducible.dvd_comm, or_self_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : PreValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : q ∣ p
⊢ Associated p q

Tactic:
associated_of_dvd_dvd (Irreducible.dvd_symm hq hp this) this

Premises used: associated_of_dvd_dvd, Irreducible.dvd_symm
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : PreValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : q ∣ p
⊢ Associated p q

Tactic:
exact associated_of_dvd_dvd (Irreducible.dvd_symm hq hp this) this

Premises used: associated_of_dvd_dvd, Irreducible.dvd_symm
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
mp : ValuationRing R → ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
mpr : (∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹) → ValuationRing R
⊢ ValuationRing R ↔ ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ValuationRing R
x : K
mp :
  ∀ (x y : R) (hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y),
    IsLocalization.IsInteger R
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)) ∨
      IsLocalization.IsInteger R
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K))⁻¹
⊢ IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

Tactic:
obtain ⟨x : R, y, hy, rfl⟩ := IsFractionRing.div_surjective R x

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ValuationRing R
x y : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
⊢ Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) y : K) (0 : K)

Tactic:
have := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr (nonZeroDivisors.ne_zero hy)
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ValuationRing R
x y : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) y : K) (0 : K)
mp :
  ∀ (s : R) (hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * s))
    (this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)),
    IsLocalization.IsInteger R
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
          ((algebraMap R K : (a : R) → K) (x * s) : K)) ∨
      IsLocalization.IsInteger R
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
            ((algebraMap R K : (a : R) → K) (x * s) : K))⁻¹
mp₁ :
  ∀ (s : R),
    IsLocalization.IsInteger R
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) (y * s) : K)
          ((algebraMap R K : (a : R) → K) y : K)) ∨
      IsLocalization.IsInteger R
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) (y * s) : K)
            ((algebraMap R K : (a : R) → K) y : K))⁻¹
⊢ IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)) ∨
    IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K))⁻¹

Tactic:
obtain ⟨s, rfl | rfl⟩ := ValuationRing.cond x y

Premises used: ValuationRing.cond, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ValuationRing R
x s : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * s)
this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
rwa :
  HDiv.hDiv (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) x : K))
      ((algebraMap R K : (a : R) → K) (x * s) : K) =
    1
rwa₁ :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) x : K) =
    (algebraMap R K : (a : R) → K) (x * s)
rwa₂ : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
rwa₃ :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) x : K) =
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) s : K)
rwa₄ : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
rwa₅ :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) s : K) =
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) s : K)
rwa₆ : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
rwa₇ :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) s : K) =
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) s : K)
rwa₈ rwa₉ rwa₁₀ : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
⊢ HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) s : K)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
        ((algebraMap R K : (a : R) → K) (x * s) : K)) =
    1

Tactic:
rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]

Premises used: mul_div, div_eq_one_iff_eq, map_mul, mul_comm
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ValuationRing R
x s : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * s)
this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
⊢ IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
        ((algebraMap R K : (a : R) → K) (x * s) : K)) ∨
    IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
          ((algebraMap R K : (a : R) → K) (x * s) : K))⁻¹

Tactic:
exact Or.inr
        ⟨s, eq_inv_of_mul_eq_one_left <| by rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]⟩

Premises used: Or.inr