awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
H : ¬IsNontrivial R
a b : ValueGroupWithZero R
neg :
  ∀
    (H :
      a < b ∧
        LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
          (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)),
    IsNontrivial R
⊢ a < b →
    LT.lt (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
      (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)

Tactic:
contrapose! H
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H :
  a < b ∧
    LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
      (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
⊢ a < b

Tactic:
obtain ⟨H, H'⟩ := H
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H :
  a < b ∧
    LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
      (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
H₁ : a < b
⊢ LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
    (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)

Tactic:
obtain ⟨H, H'⟩ := H
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H : a < b
H' :
  LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
    (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
neg :
  ∀ (H : 0 < b)
    (H' :
      LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
        (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) 0 : ℝ≥0)),
    IsNontrivial R
neg₁ : ∀ (ha : a ≠ 0), IsNontrivial R
⊢ IsNontrivial R

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
b : ValueGroupWithZero R
H : 0 < b
H' :
  LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
    (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) 0 : ℝ≥0)
⊢ IsNontrivial R

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H : a < b
H' :
  LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
    (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
ha : a ≠ 0
neg :
  ∀ (H : 1 < b)
    (H' :
      LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
        (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) 1 : ℝ≥0))
    (ha : Ne.{u_3 + 1} (α := ValueGroupWithZero R) 1 0), IsNontrivial R
neg₁ : ∀ (ha' : a ≠ 1), IsNontrivial R
⊢ IsNontrivial R

Tactic:
rcases eq_or_ne a 1 with rfl | ha'

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
b : ValueGroupWithZero R
H : 1 < b
H' :
  LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
    (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) 1 : ℝ≥0)
ha : Ne.{u_3 + 1} (α := ValueGroupWithZero R) 1 0
⊢ IsNontrivial R

Tactic:
⟨⟨b, (H.trans' zero_lt_one).ne', H.ne'⟩⟩

Premises used: ValuativeRel.IsNontrivial.mk, LT.lt.trans', LT.lt.ne', zero_lt_one, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
b : ValueGroupWithZero R
H : 1 < b
H' :
  LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
    (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) 1 : ℝ≥0)
ha : Ne.{u_3 + 1} (α := ValueGroupWithZero R) 1 0
⊢ IsNontrivial R

Tactic:
exact ⟨⟨b, (H.trans' zero_lt_one).ne', H.ne'⟩⟩
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H : a < b
H' :
  LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
    (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
ha : a ≠ 0
ha' : a ≠ 1
⊢ IsNontrivial R

Tactic:
⟨⟨a, ha, ha'⟩⟩

Premises used: ValuativeRel.IsNontrivial.mk, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H : a < b
H' :
  LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
    (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
ha : a ≠ 0
ha' : a ≠ 1
⊢ IsNontrivial R

Tactic:
exact ⟨⟨a, ha, ha'⟩⟩
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : CommRing R
inst_2 : ValuativeRel R
inst_3 : MulArchimedean Γ₀
v : Valuation R Γ₀
inst_4 : v.Compatible
rw : MulArchimedean.{u_3} (ValueGroupWithZero R)
⊢ IsRankLeOne R

Tactic:
rw [isRankLeOne_iff_mulArchimedean]

Premises used: ValuativeRel.isRankLeOne_iff_mulArchimedean
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : CommRing R
inst_2 : ValuativeRel R
inst_3 : MulArchimedean Γ₀
v : Valuation R Γ₀
inst_4 : v.Compatible
⊢ MulArchimedean.{u_3} (ValueGroupWithZero R)

Tactic:
MulArchimedean.comap (embedding.toMonoidHom.comp (ValueGroupWithZero.embed v).toMonoidHom)
    (embedding_strictMono.comp (ValueGroupWithZero.embed_strictMono v))

Premises used: ValuativeRel.ValueGroupWithZero.embed_strictMono, MonoidHom.comp, ValuativeRel.ValueGroupWithZero.embed, MulArchimedean.comap, MonoidWithZeroHom.toMonoidHom, MonoidWithZeroHom.ValueGroup₀.embedding, StrictMono.comp, MonoidWithZeroHom.ValueGroup₀.embedding_strictMono
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : CommRing R
inst_2 : ValuativeRel R
inst_3 : MulArchimedean Γ₀
v : Valuation R Γ₀
inst_4 : v.Compatible
⊢ MulArchimedean.{u_3} (ValueGroupWithZero R)

Tactic:
exact MulArchimedean.comap (embedding.toMonoidHom.comp (ValueGroupWithZero.embed v).toMonoidHom)
    (embedding_strictMono.comp (ValueGroupWithZero.embed_strictMono v))

Premises used: ValuativeRel.ValueGroupWithZero.embed_strictMono, MonoidHom.comp, ValuativeRel.ValueGroupWithZero.embed, MulArchimedean.comap, MonoidWithZeroHom.toMonoidHom, MonoidWithZeroHom.ValueGroup₀.embedding, StrictMono.comp, MonoidWithZeroHom.ValueGroup₀.embedding_strictMono
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : Mul A
inst_1 : PreValuationRing A
a b : A
⊢ ∃ (c : A), a * c = b ∨ b * c = a

Tactic:
@PreValuationRing.cond' A _ _ _ _

Premises used: PreValuationRing.cond'
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
a₁ :
  (fun (a b : K) ↦ ∃ (c : A), c • b = a) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d) ↔
    (fun (a b : K) ↦ ∃ (c : A), c • b = a) a b
⊢ Eq (α := Prop) ((fun (a b : K) ↦ ∃ (c : A), c • b = a) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d))
    ((fun (a b : K) ↦ ∃ (c : A), c • b = a) a b)

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
x y : ValueGroup A K
a b : K
c d : Aˣ
a₁ :
  (fun (a b : K) ↦ ∃ (c : A), c • b = a) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d) →
    (fun (a b : K) ↦ ∃ (c : A), c • b = a) a b
a₂ :
  (fun (a b : K) ↦ ∃ (c : A), c • b = a) a b →
    (fun (a b : K) ↦ ∃ (c : A), c • b = a) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d)
⊢ (fun (a b : K) ↦ ∃ (c : A), c • b = a) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d) ↔
    (fun (a b : K) ↦ ∃ (c : A), c • b = a) a b

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : HSMul.hSMul (β := K) e ((fun (m : Aˣ) ↦ m • b) d) = (fun (m : Aˣ) ↦ m • a) c
h : ((↑c⁻¹ : A) * e * (↑d : A)) • b = a
⊢ ∃ (c : A), c • b = a

Tactic:
use (c⁻¹ : Aˣ) * e * d

Premises used: Inv.inv
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : HSMul.hSMul (β := K) e ((fun (m : Aˣ) ↦ m • b) d) = (fun (m : Aˣ) ↦ m • a) c
⊢ c⁻¹ • HSMul.hSMul (β := K) e ((fun (m : Aˣ) ↦ m • b) d) = HSMul.hSMul (β := K) c⁻¹ ((fun (m : Aˣ) ↦ m • a) c)

Tactic:
apply_fun fun t => c⁻¹ • t at he

Premises used: Inv.inv, HSMul.hSMul
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : c⁻¹ • HSMul.hSMul (β := K) e ((fun (m : Aˣ) ↦ m • b) d) = HSMul.hSMul (β := K) c⁻¹ ((fun (m : Aˣ) ↦ m • a) c)
⊢ ((↑c⁻¹ : A) * e * (↑d : A)) • b = a

Tactic:
simpa [mul_smul] using he

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • b = a
a₁ : ∃ (c_1 : A), c_1 • d • b = c • a
⊢ ∃ (c_1 : A), HSMul.hSMul (β := K) c_1 ((fun (m : Aˣ) ↦ m • b) d) = (fun (m : Aˣ) ↦ m • a) c

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • b = a
h : ((↑c : A) * e * (↑d⁻¹ : A)) • d • b = c • a
⊢ ∃ (c_1 : A), c_1 • d • b = c • a

Tactic:
use c * e * (d⁻¹ : Aˣ)

Premises used: Inv.inv
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • b = a
h : (↑c : A) • e • (↑d⁻¹ : A) • (↑d : A) • b = (↑c : A) • e • b
⊢ ((↑c : A) * e * (↑d⁻¹ : A)) • d • b = c • a

Tactic:
simp_rw [Units.smul_def, ← he, mul_smul]

Premises used: Units.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • b = a
h : (↑c : A) • e • ((↑d⁻¹ : A) * (↑d : A)) • b = (↑c : A) • e • b
h₁ : (↑c : A) • e • HSMul.hSMul.{u, v, v} (α := A) 1 b = (↑c : A) • e • b
h₂ h₃ : (↑c : A) • e • b = (↑c : A) • e • b
⊢ (↑c : A) • e • (↑d⁻¹ : A) • (↑d : A) • b = (↑c : A) • e • b

Tactic:
rw [← mul_smul _ _ b, Units.inv_mul, one_smul]

Premises used: Units.inv_mul, one_smul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
a₁ :
  (MulAction.orbitRel Aˣ K : K → K → Prop) (HMul.hMul (α := K) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d))
    (a * b)
⊢ Eq.{v + 1} (α := ValueGroup A K)
    ((fun (a b : K) ↦ (Quotient.mk'' (a * b) : Quotient (MulAction.orbitRel.{u, v} Aˣ K))) ((fun (m : Aˣ) ↦ m • a) c)
      ((fun (m : Aˣ) ↦ m • b) d))
    ((fun (a b : K) ↦ (Quotient.mk'' (a * b) : Quotient (MulAction.orbitRel.{u, v} Aˣ K))) a b)

Tactic:
apply Quotient.sound'

Premises used: Quotient.sound'
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
a₁ : (MulAction.orbitRel Aˣ K : K → K → Prop) (c • a * d • b) (a * b)
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (HMul.hMul (α := K) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d))
    (a * b)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
h : (fun (m : Aˣ) ↦ m • (a * b)) (c * d) = c • a * d • b
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (c • a * d • b) (a * b)

Tactic:
use c * d
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
h :
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑c : A) : K)
      (HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑d : A) : K) (a * b)) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑c : A) : K) a *
      HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑d : A) : K) b
⊢ (fun (m : Aˣ) ↦ m • (a * b)) (c * d) = c • a * d • b

Tactic:
simp only [mul_smul, Algebra.smul_def, Units.smul_def]

Premises used: Units.smul_def, Algebra.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑c : A) : K)
      (HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑d : A) : K) (a * b)) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑c : A) : K) a *
      HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑d : A) : K) b

Tactic:
ring
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x : ValueGroup A K
a : K
b : Aˣ
a₁ : (MulAction.orbitRel Aˣ K : K → K → Prop) ((fun (m : Aˣ) ↦ m • a) b)⁻¹ a⁻¹
⊢ Eq.{v + 1} (α := ValueGroup A K)
    ((fun (a : K) ↦ (Quotient.mk'' a⁻¹ : Quotient (MulAction.orbitRel.{u, v} Aˣ K))) ((fun (m : Aˣ) ↦ m • a) b))
    ((fun (a : K) ↦ (Quotient.mk'' a⁻¹ : Quotient (MulAction.orbitRel.{u, v} Aˣ K))) a)

Tactic:
apply Quotient.sound'

Premises used: Quotient.sound'
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x : ValueGroup A K
a : K
b : Aˣ
h : Eq.{v + 1} (α := K) ((fun (m : Aˣ) ↦ m • a⁻¹) b⁻¹) ((fun (m : Aˣ) ↦ m • a) b)⁻¹
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) ((fun (m : Aˣ) ↦ m • a) b)⁻¹ a⁻¹

Tactic:
use b⁻¹
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x : ValueGroup A K
a : K
b : Aˣ
h : b⁻¹ • a⁻¹ = (b • a)⁻¹
⊢ Eq.{v + 1} (α := K) ((fun (m : Aˣ) ↦ m • a⁻¹) b⁻¹) ((fun (m : Aˣ) ↦ m • a) b)⁻¹

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
x : ValueGroup A K
a : K
b : Aˣ
h : (↑b⁻¹ : A) • a⁻¹ = (b • a)⁻¹
h₁ : (↑b⁻¹ : A) • a⁻¹ = ((↑b : A) • a)⁻¹
h₂ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b⁻¹ : A) : K) a⁻¹ = ((↑b : A) • a)⁻¹
h₃ :
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b⁻¹ : A) : K) a⁻¹ =
    (HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b : A) : K) a)⁻¹
h₄ :
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b⁻¹ : A) : K) a⁻¹ =
    HMul.hMul (α := K) (((algebraMap A K : (a : A) → K) (↑b : A))⁻¹ : K) a⁻¹
h₅ h₆ :
  HMul.hMul (α := K) (((algebraMap A K : (a : A) → K) (↑b : A))⁻¹ : K) a⁻¹ =
    HMul.hMul (α := K) (((algebraMap A K : (a : A) → K) (↑b : A))⁻¹ : K) a⁻¹
⊢ b⁻¹ • a⁻¹ = (b • a)⁻¹

Tactic:
rw [Units.smul_def, Units.smul_def, Algebra.smul_def, Algebra.smul_def, mul_inv,
          map_units_inv]

Premises used: mul_inv, map_units_inv, Units.smul_def, Algebra.smul_def
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
c : Eq.{v + 1} (α := ValueGroup A K) 0 1
obtain : ∀ (d : Aˣ) (hd : Eq.{v + 1} (α := K) ((fun (m : Aˣ) ↦ HSMul.hSMul (β := K) m 1) d) 0), False
⊢ False

Tactic:
obtain ⟨d, hd⟩ := Quotient.exact' c

Premises used: Quotient.exact'
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
c : Eq.{v + 1} (α := ValueGroup A K) 0 1
d : Aˣ
hd : Eq.{v + 1} (α := K) ((fun (m : Aˣ) ↦ HSMul.hSMul (β := K) m 1) d) 0
⊢ HSMul.hSMul (β := K) d⁻¹ ((fun (m : Aˣ) ↦ HSMul.hSMul (β := K) m 1) d) = HSMul.hSMul (β := K) d⁻¹ 0

Tactic:
apply_fun fun t => d⁻¹ • t at hd

Premises used: Inv.inv, HSMul.hSMul
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
c : Eq.{v + 1} (α := ValueGroup A K) 0 1
d : Aˣ
hd : d⁻¹ • HSMul.hSMul (β := K) d 1 = HSMul.hSMul (β := K) d⁻¹ 0
⊢ False

Tactic:
simp only [inv_smul_smul, smul_zero, one_ne_zero] at hd

Premises used: smul_zero, inv_smul_smul, one_ne_zero
-- 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 b : ValueGroup A K
mk :
  ∀ (a : K),
    Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a ≤ b ∨
      b ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a
⊢ a ≤ b ∨ b ≤ a

Tactic:
rcases a with ⟨a⟩
-- 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_1 b : ValueGroup A K
a : K
mk :
  ∀ (b : K),
    LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b) ∨
      LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a ≤ b ∨ b ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a

Tactic:
rcases b with ⟨b⟩
-- 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_1 b_1 : ValueGroup A K
a b : K
mk :
  ∀ (xa ya : A) (hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya),
    LE.le (α := ValueGroup A K)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b) ∨
      LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
⊢ LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b) ∨
    LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)

Tactic:
obtain ⟨xa, ya, hya, rfl⟩ := IsFractionRing.div_surjective A a

Premises used: IsFractionRing.div_surjective, 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 b_1 : ValueGroup A K
b : K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
mk :
  ∀ (xb yb : A) (hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb),
    LE.le (α := ValueGroup A K)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K)
            ((algebraMap A K : (a : A) → K) yb : K))) ∨
      LE.le (α := ValueGroup A K)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
⊢ LE.le (α := ValueGroup A K)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b) ∨
    LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))

Tactic:
obtain ⟨xb, yb, hyb, rfl⟩ := IsFractionRing.div_surjective A b

Premises used: IsFractionRing.div_surjective, 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 b : ValueGroup A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
⊢ Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)

Tactic:
have : (algebraMap A K) ya ≠ 0 := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hya
-- 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 b : ValueGroup A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
⊢ Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)

Tactic:
have : (algebraMap A K) yb ≠ 0 := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hyb