awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
⊢ 1 <ᵥ x ↔ LT.lt.{u_2} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
simp [v.vlt_iff_lt]

Premises used: Valuation.vlt_iff_lt
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : ↥(posSubmonoid R)
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (↑x : R) : Γ₀) (0 : Γ₀)

Tactic:
simp [(isEquiv v (valuation R)).eq_zero, valuation_posSubmonoid_ne_zero]

Premises used: ValuativeRel.valuation_posSubmonoid_ne_zero, Valuation.IsEquiv.eq_zero, ValuativeRel.isEquiv, ValuativeRel.valuation
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : ↥(posSubmonoid R)
⊢ LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) (↑x : R) : Γ₀)

Tactic:
zero_lt_iff.mpr <| v.apply_posSubmonoid_ne_zero x

Premises used: Iff.mpr, zero_lt_iff, Valuation.apply_posSubmonoid_ne_zero
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
⊢ @vle _ inst _ x y ∨ @vle _ inst _ y x

Tactic:
have := vle_total x y
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
this : @vle _ inst _ x y ∨ @vle _ inst _ y x
⊢ x <ᵥ y ↔ @vle _ inst _ x y ∧ ¬@vle _ inst _ y x

Tactic:
grind
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x x_1 : R
h : Membership.mem (γ := Set R) {x : R | @vle _ inst _ x 0} x_1
⊢ Membership.mem (γ := Set R) {x : R | @vle _ inst _ x 0} (x • x_1)

Tactic:
simpa using mul_vle_mul_right h _

Premises used: ValuativeRel.mul_vle_mul_right
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
⊢ Membership.mem (γ := Ideal R) (supp R) x ↔ @vle _ inst _ x 0

Tactic:
Iff.refl _

Premises used: Set.Mem, Iff.refl, setOf
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
h :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (supp R) x ↔
      Membership.mem (γ := Ideal R) (Valuation.supp (Γ₀ := ValueGroupWithZero R) (valuation R)) x
⊢ Eq (α := Ideal R) (supp R) (Valuation.supp (Γ₀ := ValueGroupWithZero R) (valuation R))

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
⊢ Membership.mem (γ := Ideal R) (supp R) x ↔
    Membership.mem (γ := Ideal R) (Valuation.supp (Γ₀ := ValueGroupWithZero R) (valuation R)) x

Tactic:
simpa using valuation_eq_zero_iff.symm

Premises used: ValuativeRel.valuation_eq_zero_iff, Iff.symm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
rw : Ideal.IsPrime (Valuation.supp (Γ₀ := ValueGroupWithZero R) (valuation R))
⊢ Ideal.IsPrime (supp R)

Tactic:
rw [supp_eq_valuation_supp]

Premises used: ValuativeRel.supp_eq_valuation_supp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
⊢ Ideal.IsPrime (Valuation.supp (Γ₀ := ValueGroupWithZero R) (valuation R))

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b c : R
hab : a <ᵥ b
hbc : @vle _ inst _ b c
⊢ a <ᵥ c

Tactic:
lt_of_lt_of_le (α := WithPreorder R) hab hbc

Premises used: lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b c : R
hab : @vle _ inst _ a b
hbc : b <ᵥ c
⊢ a <ᵥ c

Tactic:
lt_of_le_of_lt (α := WithPreorder R) hab hbc

Premises used: lt_of_le_of_lt
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : a <ᵥ b
⊢ @ValuativeRel.vle _ inst _ a b

Tactic:
le_of_lt (α := WithPreorder R) hab

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b c : R
hab : a <ᵥ b
hbc : b <ᵥ c
⊢ a <ᵥ c

Tactic:
hab.trans_vle hbc.vle

Premises used: ValuativeRel.vlt.trans_vle, ValuativeRel.vlt.vle
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b c d : R
hab : a <ᵥ b
hcd : @vle _ inst _ c d
hd : 0 <ᵥ d
⊢ a * c <ᵥ b * d

Tactic:
(mul_vle_mul_right hcd _).trans_vlt (mul_vlt_mul_left hd hab)

Premises used: ValuativeRel.vle.trans_vlt, ValuativeRel.mul_vlt_mul_left, ValuativeRel.mul_vle_mul_right
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b c d : R
hab : @vle _ inst _ a b
hcd : c <ᵥ d
ha : 0 <ᵥ a
⊢ a * c <ᵥ b * d

Tactic:
(mul_vlt_mul_right ha hcd).trans_vle (mul_vle_mul_left hab _)

Premises used: ValuativeRel.vlt.trans_vle, ValuativeRel.mul_vlt_mul_right, ValuativeRel.mul_vle_mul_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b c d : R
hab : a <ᵥ b
hcd : c <ᵥ d
⊢ a * c <ᵥ b * d

Tactic:
(mul_vle_mul_right hcd.vle _).trans_vlt (mul_vlt_mul_left ((zero_vle c).trans_vlt hcd) hab)

Premises used: ValuativeRel.vle.trans_vlt, ValuativeRel.zero_vle, ValuativeRel.mul_vlt_mul_left, ValuativeRel.mul_vle_mul_right, ValuativeRel.vlt.vle
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : @vle _ inst _ a b
⊢ @vle _ inst _ (HPow.hPow (β := ℕ) a 0) (HPow.hPow (β := ℕ) b 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : @vle _ inst _ a b
n : ℕ
hn : @vle _ inst _ (a ^ n) (b ^ n)
⊢ @vle _ inst _ (a ^ (n + 1)) (b ^ (n + 1))

Tactic:
simp [pow_succ, mul_vle_mul hn hab]

Premises used: pow_succ, ValuativeRel.mul_vle_mul
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : @vle _ inst _ a b
n : ℕ
zero : @vle _ inst _ (HPow.hPow (β := ℕ) a 0) (HPow.hPow (β := ℕ) b 0)
succ : ∀ (n : ℕ) (hn : @vle _ inst _ (a ^ n) (b ^ n)), @vle _ inst _ (a ^ (n + 1)) (b ^ (n + 1))
⊢ @vle _ inst _ (a ^ n) (b ^ n)

Tactic:
induction n with
  | zero => simp
  | succ _ hn => simp [pow_succ, mul_vle_mul hn hab]

Premises used: pow_succ
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : a <ᵥ b
hn : Ne (α := ℕ) 0 0
⊢ HPow.hPow (β := ℕ) a 0 <ᵥ HPow.hPow (β := ℕ) b 0

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : a <ᵥ b
hn : Ne (α := ℕ) 1 0
⊢ HPow.hPow (β := ℕ) a 1 <ᵥ HPow.hPow (β := ℕ) b 1

Tactic:
simpa
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : a <ᵥ b
n : ℕ
h : ∀ (hn : n ≠ 0), a ^ n <ᵥ b ^ n
h_1 : ∀ (hn : n + 1 ≠ 0), a ^ (n + 1) <ᵥ b ^ (n + 1)
hn : n + 2 ≠ 0
⊢ a ^ (n + 2) <ᵥ b ^ (n + 2)

Tactic:
simp_all [pow_succ, mul_vlt_mul]

Premises used: pow_succ, ValuativeRel.mul_vlt_mul
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : a <ᵥ b
n : ℕ
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), HPow.hPow (β := ℕ) a 0 <ᵥ HPow.hPow (β := ℕ) b 0
one : ∀ (hn : Ne (α := ℕ) 1 0), HPow.hPow (β := ℕ) a 1 <ᵥ HPow.hPow (β := ℕ) b 1
more :
  ∀ (n : ℕ),
    (∀ (hn : n ≠ 0), a ^ n <ᵥ b ^ n) →
      (∀ (hn : n + 1 ≠ 0), a ^ (n + 1) <ᵥ b ^ (n + 1)) → ∀ (hn : n + 2 ≠ 0), a ^ (n + 2) <ᵥ b ^ (n + 2)
⊢ a ^ n <ᵥ b ^ n

Tactic:
induction n using Nat.twoStepInduction with
  | zero => contradiction
  | one => simpa
  | more _ _ => simp_all [pow_succ, mul_vlt_mul]

Premises used: pow_succ, ValuativeRel.mul_vlt_mul
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a : R
ha : @vle _ inst _ a 1
n m : ℕ
hnm : n ≤ m
obtain : ∀ (m : ℕ) (hnm : n ≤ n + m), @vle _ inst _ (a ^ (n + m)) (a ^ n)
⊢ @vle _ inst _ (a ^ m) (a ^ n)

Tactic:
obtain ⟨m, rfl⟩ := exists_add_of_le hnm

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a : R
ha : @vle _ inst _ a 1
n m : ℕ
hnm : n ≤ n + m
⊢ @vle _ inst _ (a ^ (n + m)) (a ^ n)

Tactic:
simpa [pow_add] using mul_vle_mul_right (pow_vle_pow ha m) _

Premises used: ValuativeRel.pow_vle_pow, pow_add, ValuativeRel.mul_vle_mul_right
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a : R
ha : @vle _ inst _ 1 a
n m : ℕ
hnm : n ≤ m
obtain : ∀ (m : ℕ) (hnm : n ≤ n + m), @vle _ inst _ (a ^ n) (a ^ (n + m))
⊢ @vle _ inst _ (a ^ n) (a ^ m)

Tactic:
obtain ⟨m, rfl⟩ := exists_add_of_le hnm

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a : R
ha : @vle _ inst _ 1 a
n m : ℕ
hnm : n ≤ n + m
⊢ @vle _ inst _ (a ^ n) (a ^ (n + m))

Tactic:
simpa [pow_add] using mul_vle_mul_right (pow_vle_pow ha m) _

Premises used: ValuativeRel.pow_vle_pow, pow_add, ValuativeRel.mul_vle_mul_right
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a : K
rw : Membership.mem (γ := Ideal K) (supp K) a ↔ a = 0
rw₁ : Membership.mem (γ := Ideal K) ⊥ a ↔ a = 0
rw₂ rw₃ : a = 0 ↔ a = 0
⊢ @vle _ Field.toCommRing _ a 0 ↔ a = 0

Tactic:
rw [← supp_def, Ideal.eq_bot_of_prime (supp K), Ideal.mem_bot]

Premises used: Ideal.mem_bot, ValuativeRel.supp_def, ValuativeRel.supp, Ideal.eq_bot_of_prime
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a : K
⊢ 0 <ᵥ a ↔ a ≠ 0

Tactic:
simp [vlt]

Premises used: ValuativeRel.vlt
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a : K
⊢ a = 0 → a =ᵥ 0

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a : K
rw : a =ᵥ 0 ↔ 0 = a
rw₁ : a =ᵥ 0 ↔ a = 0
rw₂ rw₃ : a = 0 ↔ a = 0
⊢ 0 =ᵥ a ↔ 0 = a

Tactic:
rw [veq_comm, eq_comm, zero_veq_iff]

Premises used: ValuativeRel.zero_veq_iff, eq_comm, ValuativeRel.veq_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a b c : K
hc : c ≠ 0
⊢ 0 <ᵥ c

Tactic:
simpa
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a b c : K
hc : c ≠ 0
⊢ c ≠ 0

Tactic:
lia
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a b c : K
hc : c ≠ 0
rw : @vle _ Field.toCommRing _ (a * c) (b / c * c) ↔ @vle _ Field.toCommRing _ (a * c) b
rw₁ rw₂ : @vle _ Field.toCommRing _ (a * c) b ↔ @vle _ Field.toCommRing _ (a * c) b
⊢ @vle _ Field.toCommRing _ a (b / c) ↔ @vle _ Field.toCommRing _ (a * c) b

Tactic:
rw [← mul_vle_mul_iff_left (by simpa), div_mul_cancel₀ _ (by lia)]

Premises used: div_mul_cancel₀, ValuativeRel.mul_vle_mul_iff_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a b c : K
hc : c ≠ 0
rw : @vle _ Field.toCommRing _ (a / c * c) (b * c) ↔ @vle _ Field.toCommRing _ a (b * c)
rw₁ rw₂ : @vle _ Field.toCommRing _ a (b * c) ↔ @vle _ Field.toCommRing _ a (b * c)
⊢ @vle _ Field.toCommRing _ (a / c) b ↔ @vle _ Field.toCommRing _ a (b * c)

Tactic:
rw [← mul_vle_mul_iff_left (by simpa), div_mul_cancel₀ _ (by lia)]

Premises used: div_mul_cancel₀, ValuativeRel.mul_vle_mul_iff_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a b : K
hb : b ≠ 0
⊢ @vle _ Field.toCommRing _ 1 (a / b) ↔ @vle _ Field.toCommRing _ b a

Tactic:
simp [vle_div_iff hb]

Premises used: ValuativeRel.vle_div_iff
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a b : K
hb : b ≠ 0
⊢ @vle _ Field.toCommRing _ (a / b) 1 ↔ @vle _ Field.toCommRing _ a b

Tactic:
simp [div_vle_iff hb]

Premises used: ValuativeRel.div_vle_iff
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
x : K
hx : x ≠ 0
⊢ @vle _ Field.toCommRing _ 1 x⁻¹ ↔ @vle _ Field.toCommRing _ x 1

Tactic:
simpa using one_vle_div_iff (a := 1) hx

Premises used: ValuativeRel.one_vle_div_iff
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
x : K
hx : x ≠ 0
⊢ @vle _ Field.toCommRing _ x⁻¹ 1 ↔ @vle _ Field.toCommRing _ 1 x

Tactic:
simpa using div_vle_one_iff (a := 1) hx

Premises used: ValuativeRel.div_vle_one_iff
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
x : K
hx : x ≠ 0
⊢ x⁻¹ <ᵥ 1 ↔ 1 <ᵥ x

Tactic:
(one_vle_inv hx).not

Premises used: ValuativeRel.vlt, Iff.not, ValuativeRel.one_vle_inv
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
x : K
hx : x ≠ 0
⊢ 1 <ᵥ x⁻¹ ↔ x <ᵥ 1

Tactic:
(inv_vle_one hx).not

Premises used: ValuativeRel.vlt, Iff.not, ValuativeRel.inv_vle_one
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsNontrivial R
obtain : ∀ (γ : ValueGroupWithZero R) (h0 : γ ≠ 0) (h1 : γ ≠ 1), ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1
⊢ ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1

Tactic:
obtain ⟨γ, h0, h1⟩ := IsNontrivial.condition (R := R)

Premises used: ValuativeRel.IsNontrivial.condition
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsNontrivial R
γ : ValueGroupWithZero R
h0 : γ ≠ 0
h1 : γ ≠ 1
inl : ∀ (h1 : γ < 1), ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1
inr : ∀ (h1 : 1 < γ), ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1
⊢ ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1

Tactic:
obtain h1 | h1 := lt_or_lt_iff_ne.mpr h1

Premises used: Iff.mpr, lt_or_lt_iff_ne
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsNontrivial R
γ : ValueGroupWithZero R
h0 : γ ≠ 0
h1_1 : γ ≠ 1
h1 : γ < 1
⊢ ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1

Tactic:
⟨γ, zero_lt_iff.mpr h0, h1⟩

Premises used: Iff.mpr, And.intro, Exists.intro, zero_lt_iff
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsNontrivial R
γ : ValueGroupWithZero R
h0 : γ ≠ 0
h1_1 : γ ≠ 1
h1 : γ < 1
⊢ ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1

Tactic:
exact ⟨γ, zero_lt_iff.mpr h0, h1⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsNontrivial R
γ : ValueGroupWithZero R
h0 : γ ≠ 0
h1_1 : γ ≠ 1
h1 : 1 < γ
⊢ 0 < γ⁻¹

Tactic:
simpa [zero_lt_iff]

Premises used: zero_lt_iff
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsNontrivial R
γ : ValueGroupWithZero R
h0 : γ ≠ 0
h1_1 : γ ≠ 1
h1 : 1 < γ
⊢ γ⁻¹ < 1

Tactic:
simp [inv_lt_one_iff₀, h0, h1]

Premises used: inv_lt_one_iff₀
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsNontrivial R
γ : ValueGroupWithZero R
h0 : γ ≠ 0
h1_1 : γ ≠ 1
h1 : 1 < γ
⊢ ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1

Tactic:
exact ⟨γ⁻¹, by simpa [zero_lt_iff], by simp [inv_lt_one_iff₀, h0, h1]⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
mp : IsNontrivial R → Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
mpr : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ → IsNontrivial R
⊢ IsNontrivial R ↔ Nontrivial.{u_1} (ValueGroupWithZero R)ˣ

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : ValueGroupWithZero R
hγ : γ ≠ 0
hγ' : γ ≠ 1
⊢ Nontrivial.{u_1} (ValueGroupWithZero R)ˣ

Tactic:
⟨Units.mk0 _ hγ, 1, ?_⟩

Premises used: Nontrivial.mk, Units.mk0, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : ValueGroupWithZero R
hγ : γ ≠ 0
hγ' : γ ≠ 1
mp : Units.mk0 γ hγ ≠ 1
⊢ Nontrivial.{u_1} (ValueGroupWithZero R)ˣ

Tactic:
refine ⟨Units.mk0 _ hγ, 1, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : ValueGroupWithZero R
hγ : γ ≠ 0
hγ' : γ ≠ 1
⊢ Units.mk0 γ hγ ≠ 1

Tactic:
simp [← Units.val_eq_one, hγ']

Premises used: Units.val_eq_one
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
r s : (ValueGroupWithZero R)ˣ
h : r ≠ s
mpr : ∀ (h : 1 ≠ s), IsNontrivial R
mpr₁ : ∀ (hr : r ≠ 1), IsNontrivial R
⊢ IsNontrivial R

Tactic:
rcases eq_or_ne r 1 with rfl | hr

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
s : (ValueGroupWithZero R)ˣ
h : 1 ≠ s
⊢ (↑s : ValueGroupWithZero R) ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
s : (ValueGroupWithZero R)ˣ
h : 1 ≠ s
⊢ (↑s : ValueGroupWithZero R) ≠ 1

Tactic:
simpa using h.symm

Premises used: Ne.symm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
s : (ValueGroupWithZero R)ˣ
h : 1 ≠ s
⊢ IsNontrivial R

Tactic:
exact ⟨s.val, by simp, by simpa using h.symm⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
r s : (ValueGroupWithZero R)ˣ
h : r ≠ s
hr : r ≠ 1
⊢ (↑r : ValueGroupWithZero R) ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
r s : (ValueGroupWithZero R)ˣ
h : r ≠ s
hr : r ≠ 1
⊢ (↑r : ValueGroupWithZero R) ≠ 1

Tactic:
simpa using hr
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
r s : (ValueGroupWithZero R)ˣ
h : r ≠ s
hr : r ≠ 1
⊢ IsNontrivial R

Tactic:
exact ⟨r.val, by simp, by simpa using hr⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
mp : IsNontrivial R → v.IsNontrivial
mpr : v.IsNontrivial → IsNontrivial R
⊢ IsNontrivial R ↔ v.IsNontrivial

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
r : ValueGroupWithZero R
hr : r ≠ 0
hr' : r ≠ 1
mp :
  ∀ (r : R) (s : ↥(posSubmonoid R)) (hr : ValueGroupWithZero.mk r s ≠ 0) (hr' : ValueGroupWithZero.mk r s ≠ 1),
    v.IsNontrivial
⊢ v.IsNontrivial

Tactic:
induction r using ValueGroupWithZero.ind with | mk r s

Premises used: ValuativeRel.ValueGroupWithZero.ind, ValuativeRel.mk
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)

Tactic:
simpa [Valuation.Compatible.vle_iff_le (v := v)] using hr

Premises used: Valuation.Compatible.vle_iff_le
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)

Tactic:
have hγ : v r ≠ 0 := by simpa [Valuation.Compatible.vle_iff_le (v := v)] using hr
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
⊢ LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀) →
    LT.lt.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀)

Tactic:
simpa [Valuation.Compatible.vle_iff_le (v := v)] using hr'

Premises used: Valuation.Compatible.vle_iff_le
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
⊢ LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀) →
    LT.lt.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀)

Tactic:
have hγ' : v r ≤ v s → v r < v s := by
      simpa [Valuation.Compatible.vle_iff_le (v := v)] using hr'
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
hγ' :
  LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀) →
    LT.lt.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀)
pos : ∀ (hr : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)), v.IsNontrivial
neg : ∀ (hr : ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)), v.IsNontrivial
⊢ v.IsNontrivial

Tactic:
by_cases hr : v r = 1

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr_1 : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
hγ' :
  LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀) →
    LT.lt.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀)
hr : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀) (0 : Γ₀)

Tactic:
simp