awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h_1 : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  {
    toFun := fun (x : Multiplicative ℝ) ↦
      Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
a b : (ValueGroup₀ v)ˣ
h : a < b
⊢ LT.lt (α := ℝ≥0ˣ) ((rf.comp e : (a : (ValueGroup₀ v)ˣ) → ℝ≥0ˣ) a : ℝ≥0ˣ)
    ((rf.comp e : (a : (ValueGroup₀ v)ˣ) → ℝ≥0ˣ) b : ℝ≥0ˣ)

Tactic:
simpa [← Units.val_lt_val, ← NNReal.coe_lt_coe, rf] using he h

Premises used: NNReal.coe_lt_coe, Units.val_lt_val
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  {
    toFun := fun (x : Multiplicative ℝ) ↦
      Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
⊢ StrictMono (α := WithZero (ValueGroup₀ v)ˣ) (β := WithZero ℝ≥0ˣ)
    (⇑(map' (rf.comp e)) : (a : WithZero (ValueGroup₀ v)ˣ) → WithZero ℝ≥0ˣ)

Tactic:
have H : StrictMono (map' (rf.comp e)) := by
      refine map'_strictMono ?_
      intro a b h
      simpa [← Units.val_lt_val, ← NNReal.coe_lt_coe, rf] using he h
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  {
    toFun := fun (x : Multiplicative ℝ) ↦
      Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
H :
  StrictMono (α := WithZero (ValueGroup₀ v)ˣ) (β := WithZero ℝ≥0ˣ)
    (⇑(map' (rf.comp e)) : (a : WithZero (ValueGroup₀ v)ˣ) → WithZero ℝ≥0ˣ)
⊢ Nonempty.{u_2 + 1} v.RankOne

Tactic:
⟨{
      hom' := withZeroUnitsEquiv.toMonoidWithZeroHom.comp <| (map' (rf.comp e)).comp
        withZeroUnitsEquiv.symm.toMonoidWithZeroHom
      strictMono' := withZeroUnitsEquiv_strictMono.comp <| H.comp
        withZeroUnitsEquiv_symm_strictMono
    }⟩

Premises used: Valuation.RankOne.mk, Nonempty.intro
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  {
    toFun := fun (x : Multiplicative ℝ) ↦
      Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
H :
  StrictMono (α := WithZero (ValueGroup₀ v)ˣ) (β := WithZero ℝ≥0ˣ)
    (⇑(map' (rf.comp e)) : (a : WithZero (ValueGroup₀ v)ˣ) → WithZero ℝ≥0ˣ)
⊢ Nonempty.{u_2 + 1} v.RankOne

Tactic:
exact ⟨{
      hom' := withZeroUnitsEquiv.toMonoidWithZeroHom.comp <| (map' (rf.comp e)).comp
        withZeroUnitsEquiv.symm.toMonoidWithZeroHom
      strictMono' := withZeroUnitsEquiv_strictMono.comp <| H.comp
        withZeroUnitsEquiv_symm_strictMono
    }⟩
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
⊢ StrictMono (α := ValueGroup₀ v) (β := ℝ≥0) (⇑(hom v) : (a : ValueGroup₀ v) → ℝ≥0)

Tactic:
hv.strictMono'

Premises used: Valuation.RankLeOne.strictMono'
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
⊢ ∃ (r : R),
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ∧
      Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)

Tactic:
IsNontrivial.exists_val_nontrivial

Premises used: Valuation.IsNontrivial.exists_val_nontrivial
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : ValueGroup₀ v
hx : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
⊢ x = 0

Tactic:
(eq_of_le_of_not_lt (zero_le' (a := x)) fun h_lt ↦ ?_).symm

Premises used: zero_le', Eq.symm, eq_of_le_of_not_lt
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : ValueGroup₀ v
hx : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
refine : ∀ (h_lt : 0 < x), False
⊢ x = 0

Tactic:
refine (eq_of_le_of_not_lt (zero_le' (a := x)) fun h_lt ↦ ?_).symm

Premises used: zero_le', Eq.symm, eq_of_le_of_not_lt
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : ValueGroup₀ v
hx : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
h_lt : 0 < x
⊢ LT.lt (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) 0 : ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0)

Tactic:
have hs := strictMono v h_lt
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : ValueGroup₀ v
hx : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
h_lt : 0 < x
hs : LT.lt (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) 0 : ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) 0 0

Tactic:
rw [map_zero, hx] at hs

Premises used: map_zero
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : ValueGroup₀ v
hx : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
h_lt : 0 < x
hs : LT.lt (α := ℝ≥0) 0 0
⊢ False

Tactic:
hs.false

Premises used: LT.lt.false
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : ValueGroup₀ v
hx : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
h_lt : 0 < x
hs : LT.lt (α := ℝ≥0) 0 0
⊢ False

Tactic:
exact hs.false

Premises used: LT.lt.false
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : ValueGroup₀ v
h : x = 0
rw : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) 0 : ℝ≥0) (0 : ℝ≥0)
rw₁ rw₂ : Eq (α := ℝ≥0) 0 0
⊢ Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)

Tactic:
rw [h, map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
rw : ¬(↑(unit v) : Γ₀) = 1
⊢ unit v ≠ 1

Tactic:
rw [Ne, ← Units.val_inj, Units.val_one]

Premises used: Ne, Units.val_inj, Units.val_one
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
⊢ ¬(↑(unit v) : Γ₀) = 1

Tactic:
((nontrivial v).choose_spec).2

Premises used: Exists.choose_spec, And.right, Valuation.RankOne.nontrivial
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
⊢ ¬(↑(unit v) : Γ₀) = 1

Tactic:
exact ((nontrivial v).choose_spec).2

Premises used: Exists.choose_spec, And.right, Valuation.RankOne.nontrivial
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
inst_2 : v.IsNontrivial
obtain :
  ∀ (x : R) (hx0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (hx1 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)),
    ∃ (x : R),
      Ne.{u_2 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ∧
        Ne.{u_2 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
⊢ ∃ (x : R),
    Ne.{u_2 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ∧
      Ne.{u_2 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
obtain ⟨x, ⟨hx0, hx1⟩⟩ := IsNontrivial.exists_val_nontrivial (v := v)

Premises used: Valuation.IsNontrivial.exists_val_nontrivial
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
inst_2 : v.IsNontrivial
x : R
hx0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hx1 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Ne.{u_2 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
simp [hx0]
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
inst_2 : v.IsNontrivial
x : R
hx0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hx1 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Ne.{u_2 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
grind [restrict_eq_one_iff]

Premises used: Valuation.restrict_eq_one_iff
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
inst_2 : v.IsNontrivial
x : R
hx0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hx1 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (x : R),
    Ne.{u_2 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ∧
      Ne.{u_2 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
exact ⟨x, by simp [hx0], by grind [restrict_eq_one_iff]⟩
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
⊢ hom v.restrict = (hom v).comp embedding

Tactic:
rfl

Premises used: Set.Mem, MonoidWithZeroHomClass.toMonoidWithZeroHom, setOf, MonoidWithZeroHom.valueGroup, rfl
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
⊢ 0 < γ

Tactic:
have hγ_pos : 0 < γ := pos_iff_ne_zero.mpr hγ
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
obtain :
  ∀ (x : (ValueGroup₀ v.restrict)ˣ)
    (h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ),
    ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ
⊢ ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ

Tactic:
obtain ⟨x, h⟩ := NNReal.exists_lt_of_strictMono (RankOne.strictMono v.restrict) hγ_pos

Premises used: NNReal.exists_lt_of_strictMono, Valuation.RankOne.strictMono, Valuation.restrict
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
obtain :
  ∀ (k : K)
    (hk :
      ((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) :
            (a : K) → ValueGroup₀ v.restrict)
          k =
        (↑x : ValueGroup₀ v.restrict)),
    ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ
⊢ ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ

Tactic:
obtain ⟨k, hk⟩ := ValueGroup₀.restrict₀_surjective _ x.val

Premises used: Units.val, MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  ((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) : (a : K) → ValueGroup₀ v.restrict)
      k =
    (↑x : ValueGroup₀ v.restrict)
⊢ ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ

Tactic:
⟨k, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  ((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) : (a : K) → ValueGroup₀ v.restrict)
      k =
    (↑x : ValueGroup₀ v.restrict)
refine_1 : k ≠ 0
refine_2 : (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k) < γ
⊢ ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ

Tactic:
refine ⟨k, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  (if h :
        Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
          else
            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
              WithZero ↥(valueGroup v)))
          0 then
      0
    else
      (↑(Subtype.mk (p := fun (x : (ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))ˣ) ↦
            Membership.mem (γ := Subgroup (ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))ˣ) (valueGroup v.restrict) x)
            (Units.mk0
              (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
              else
                (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                      (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
                  WithZero ↥(valueGroup v)))
              ⋯)
            ⋯) :
        WithZero ↥(valueGroup v.restrict))) =
    (↑x : ValueGroup₀ v.restrict)
refine_1 : ∀ (h0 : k = 0), False
⊢ k ≠ 0

Tactic:
by_contra h0
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  (if h :
        Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
          else
            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
              WithZero ↥(valueGroup v)))
          0 then
      0
    else
      (↑(Subtype.mk (p := fun (x : (ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))ˣ) ↦
            Membership.mem (γ := Subgroup (ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))ˣ) (valueGroup v.restrict) x)
            (Units.mk0
              (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
              else
                (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                      (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
                  WithZero ↥(valueGroup v)))
              ⋯)
            ⋯) :
        WithZero ↥(valueGroup v.restrict))) =
    (↑x : ValueGroup₀ v.restrict)
h0 : k = 0
rw rw₁ : Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) 0 0
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
    else
      (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
            (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
        WithZero ↥(valueGroup v)))
    0

Tactic:
rw [dif_pos ((zero_iff v).mpr h0)]

Premises used: Iff.mpr, dif_pos, Valuation.zero_iff
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  (if h :
        Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
          else
            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
              WithZero ↥(valueGroup v)))
          0 then
      0
    else
      (↑(Subtype.mk (p := fun (x : (ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))ˣ) ↦
            Membership.mem (γ := Subgroup (ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))ˣ) (valueGroup v.restrict) x)
            (Units.mk0
              (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
              else
                (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                      (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
                  WithZero ↥(valueGroup v)))
              ⋯)
            ⋯) :
        WithZero ↥(valueGroup v.restrict))) =
    (↑x : ValueGroup₀ v.restrict)
h0 : k = 0
⊢ (↑x : ValueGroup₀ v.restrict) = 0

Tactic:
rw [dif_pos (by rw [dif_pos ((zero_iff v).mpr h0)]), eq_comm] at hk

Premises used: dif_pos, eq_comm
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  (if h :
        Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
          else
            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
              WithZero ↥(valueGroup v)))
          0 then
      0
    else
      (↑(Subtype.mk (p := fun (x : (ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))ˣ) ↦
            Membership.mem (γ := Subgroup (ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))ˣ) (valueGroup v.restrict) x)
            (Units.mk0
              (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
              else
                (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                      (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
                  WithZero ↥(valueGroup v)))
              ⋯)
            ⋯) :
        WithZero ↥(valueGroup v.restrict))) =
    (↑x : ValueGroup₀ v.restrict)
h0 : k = 0
hk₁ : (↑x : ValueGroup₀ v.restrict) = 0
⊢ k = 0

Tactic:
rw [dif_pos (by rw [dif_pos ((zero_iff v).mpr h0)]), eq_comm] at hk

Premises used: dif_pos, eq_comm
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk : (↑x : ValueGroup₀ v.restrict) = 0
h0 : k = 0
⊢ False

Tactic:
simp at hk