awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ

Tactic:
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 < γ
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)
h₁ :
  Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k) : ℝ≥0)
    ((hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) : ℝ≥0)
⊢ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k) < γ

Tactic:
convert! 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 < γ
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)
h₁ :
  Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k) : ℝ≥0)
    ((hom v : (a : ValueGroup₀ v) → ℝ≥0)
        ((embedding : (a : ValueGroup₀ v.restrict) → ValueGroup₀ v)
          (((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) :
                (a : K) → ValueGroup₀ v.restrict)
              k :
            ValueGroup₀ v.restrict)) :
      ℝ≥0)
⊢ Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k) : ℝ≥0)
    ((hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) : ℝ≥0)

Tactic:
simp only [restrict_RankOne_hom_eq, coe_comp, Function.comp_apply, ← hk]

Premises used: MonoidWithZeroHom.coe_comp, Function.comp_apply, Valuation.RankOne.restrict_RankOne_hom_eq
-- 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)
h₁ :
  Eq.{u_2 + 1} (α := ValueGroup₀ v)
    ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((embedding : (a : ValueGroup₀ v.restrict) → ValueGroup₀ v)
        (((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) :
              (a : K) → ValueGroup₀ v.restrict)
            k :
          ValueGroup₀ v.restrict) :
      ValueGroup₀ v)
⊢ Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k) : ℝ≥0)
    ((hom v : (a : ValueGroup₀ v) → ℝ≥0)
        ((embedding : (a : ValueGroup₀ v.restrict) → ValueGroup₀ v)
          (((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) :
                (a : K) → ValueGroup₀ v.restrict)
              k :
            ValueGroup₀ v.restrict)) :
      ℝ≥0)

Tactic:
congr 1
-- 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)
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ v)
    ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((embedding : (a : ValueGroup₀ v.restrict) → ValueGroup₀ v)
        (((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) :
              (a : K) → ValueGroup₀ v.restrict)
            k :
          ValueGroup₀ v.restrict) :
      ValueGroup₀ v)

Tactic:
(embedding_restrict₀ k).symm

Premises used: Set.Mem, MonoidWithZeroHomClass.toMonoidWithZeroHom, setOf, MonoidWithZeroHom.valueGroup, MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀, Eq.symm
-- 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)
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ v)
    ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((embedding : (a : ValueGroup₀ v.restrict) → ValueGroup₀ v)
        (((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) :
              (a : K) → ValueGroup₀ v.restrict)
            k :
          ValueGroup₀ v.restrict) :
      ValueGroup₀ v)

Tactic:
exact (embedding_restrict₀ k).symm

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀, Eq.symm
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H : ∃ (x : K), x ≠ 0 ∧ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
by_contra! :
  ∀
    (H' :
      ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
        Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)),
    False
⊢ ∃ (x : K),
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
      Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
by_contra! H'
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H : ∃ (x : K), x ≠ 0 ∧ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
obtain : ∀ (x : K) (hx : x ≠ 0) (hx' : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)), False
⊢ False

Tactic:
obtain ⟨x, hx, hx'⟩ := H
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : K
hx : x ≠ 0
hx' : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ False

Tactic:
hx' (H' x ((ne_zero_iff v).mpr hx))

Premises used: Iff.mpr, Valuation.ne_zero_iff
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : K
hx : x ≠ 0
hx' : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ False

Tactic:
exact hx' (H' x ((ne_zero_iff v).mpr hx))

Premises used: Iff.mpr, Valuation.ne_zero_iff
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H : Nontrivial.{u_2} (ValueGroup₀ v)ˣ
by_contra! :
  ∀
    (H' :
      ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
        Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)),
    False
⊢ ∃ (x : K),
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
      Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
by_contra! H'
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H : Nontrivial.{u_2} (ValueGroup₀ v)ˣ
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (y : (ValueGroup₀ v)ˣ), y ≠ 1

Tactic:
rw [nontrivial_iff_exists_ne 1] at H

Premises used: nontrivial_iff_exists_ne, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H : Nontrivial.{u_2} (ValueGroup₀ v)ˣ
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
H₁ : ∃ (y : (ValueGroup₀ v)ˣ), y ≠ 1
⊢ ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rw [nontrivial_iff_exists_ne 1] at H

Premises used: nontrivial_iff_exists_ne, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H : ∃ (y : (ValueGroup₀ v)ˣ), y ≠ 1
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
obtain : ∀ (x : (ValueGroup₀ v)ˣ) (hx : x ≠ 1), False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := H
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
obtain :
  ∀ (k : K)
    (hk :
      ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k =
        (↑x : ValueGroup₀ v)),
    False
⊢ False

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

Premises used: Units.val, MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
k : K
hk : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k = (↑x : ValueGroup₀ v)
rw : ¬(↑x : ValueGroup₀ v) = 0
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀)

Tactic:
rw [ne_eq, ← restrict₀_eq_zero_iff, hk]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff, ne_eq
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
k : K
hk : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k = (↑x : ValueGroup₀ v)
⊢ ¬(↑x : ValueGroup₀ v) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
k : K
hk : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k = (↑x : ValueGroup₀ v)
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀)

Tactic:
have h0 : v k ≠ 0 := by
      rw [ne_eq, ← restrict₀_eq_zero_iff, hk]
      simp
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
k : K
hk : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k = (↑x : ValueGroup₀ v)
h0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀)
rw : ¬(↑x : ValueGroup₀ v) = 1
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (1 : Γ₀)

Tactic:
rw [ne_eq, ← restrict₀_eq_one_iff, hk]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_one_iff, ne_eq
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
k : K
hk : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k = (↑x : ValueGroup₀ v)
h0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀)
⊢ ¬(↑x : ValueGroup₀ v) = 1

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
k : K
hk : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k = (↑x : ValueGroup₀ v)
h0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀)
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (1 : Γ₀)

Tactic:
have h1 : v k ≠ 1 := by
      rw [ne_eq, ← restrict₀_eq_one_iff, hk]
      simp [hx]
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
k : K
hk : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k = (↑x : ValueGroup₀ v)
h0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀)
h1 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (1 : Γ₀)
⊢ False

Tactic:
h1 (H' k h0)
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
k : K
hk : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k = (↑x : ValueGroup₀ v)
h0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀)
h1 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (1 : Γ₀)
⊢ False

Tactic:
exact h1 (H' k h0)
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_4
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankLeOne
simp :
  Nontrivial.{u_2} (ValueGroup₀ v)ˣ →
    ∀ {γ : ℝ≥0},
      ¬γ = 0 →
        ∃ (x : K),
          ¬x = 0 ∧ (hom' v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ
⊢ Subsingleton.{u_2 + 1} (ValueGroup₀ v)ˣ ∨
    ∀ {γ : ℝ≥0},
      γ ≠ 0 →
        ∃ (x : K),
          x ≠ 0 ∧ (hom' v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ

Tactic:
simp only [ne_eq, or_iff_not_imp_left, not_subsingleton_iff_nontrivial]

Premises used: ne_eq, Classical.or_iff_not_imp_left, not_subsingleton_iff_nontrivial
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_4
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankLeOne
⊢ Nontrivial.{u_2} (ValueGroup₀ v)ˣ →
    ∀ {γ : ℝ≥0},
      ¬γ = 0 →
        ∃ (x : K),
          ¬x = 0 ∧ (hom' v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ

Tactic:
fun H ↦ (rankOne_of_nontrivial v H).exists_val_lt

Premises used: Valuation.RankOne.exists_val_lt
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_4
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankLeOne
⊢ Nontrivial.{u_2} (ValueGroup₀ v)ˣ →
    ∀ {γ : ℝ≥0},
      ¬γ = 0 →
        ∃ (x : K),
          ¬x = 0 ∧ (hom' v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ

Tactic:
exact fun H ↦ (rankOne_of_nontrivial v H).exists_val_lt

Premises used: Valuation.RankOne.exists_val_lt
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : Valuation.RankOne (Γ₀ := ValueGroupWithZero R) (valuation R)
⊢ IsRankLeOne R

Tactic:
⟨⟨h.rankLeOneStruct⟩⟩

Premises used: Nonempty.intro, ValuativeRel.IsRankLeOne.mk, Valuation.RankOne.rankLeOneStruct
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : Valuation.RankOne (Γ₀ := ValueGroupWithZero R) (valuation R)
⊢ IsNontrivial R

Tactic:
(isNontrivial_iff_isNontrivial _).mpr h.toIsNontrivial

Premises used: Iff.mpr, ValuativeRel.isNontrivial_iff_isNontrivial, Valuation.RankOne.toIsNontrivial
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
mp : IsRankLeOne R → MulArchimedean.{u_3} (ValueGroupWithZero R)
mpr : MulArchimedean.{u_3} (ValueGroupWithZero R) → IsRankLeOne R
⊢ IsRankLeOne R ↔ MulArchimedean.{u_3} (ValueGroupWithZero R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
f : ValueGroupWithZero R →*₀ ℝ≥0
hf : StrictMono (α := ValueGroupWithZero R) (β := ℝ≥0) (⇑f : (a : ValueGroupWithZero R) → ℝ≥0)
⊢ MulArchimedean.{u_3} (ValueGroupWithZero R)

Tactic:
.comap f.toMonoidHom hf

Premises used: MulArchimedean.comap, MonoidWithZeroHom.toMonoidHom
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
f : ValueGroupWithZero R →*₀ ℝ≥0
hf : StrictMono (α := ValueGroupWithZero R) (β := ℝ≥0) (⇑f : (a : ValueGroupWithZero R) → ℝ≥0)
⊢ MulArchimedean.{u_3} (ValueGroupWithZero R)

Tactic:
exact .comap f.toMonoidHom hf
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
pos : ∀ (H : IsNontrivial R), IsRankLeOne R
neg : ∀ (H : ¬IsNontrivial R), IsRankLeOne R
⊢ IsRankLeOne R

Tactic:
by_cases H : IsNontrivial R

Premises used: ValuativeRel.IsNontrivial
-- 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
⊢ Valuation.IsNontrivial (Γ₀ := ValueGroupWithZero R) (valuation R)

Tactic:
rw [isNontrivial_iff_isNontrivial (valuation R)] at H

Premises used: ValuativeRel.isNontrivial_iff_isNontrivial, ValuativeRel.valuation
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
H : Valuation.IsNontrivial (Γ₀ := ValueGroupWithZero R) (valuation R)
⊢ MulArchimedean.{u_3} (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))

Tactic:
have h' : MulArchimedean (ValueGroup₀ (valuation R)) :=
        MulArchimedean.comap embedding.toMonoidHom embedding_strictMono
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
H : Valuation.IsNontrivial (Γ₀ := ValueGroupWithZero R) (valuation R)
h' : MulArchimedean.{u_3} (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))
⊢ Nonempty.{u_3 + 1} (Valuation.RankOne (Γ₀ := ValueGroupWithZero R) (valuation R))

Tactic:
rw [← (valuation R).nonempty_rankOne_iff_mulArchimedean] at h'

Premises used: Valuation.nonempty_rankOne_iff_mulArchimedean
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
H : Valuation.IsNontrivial (Γ₀ := ValueGroupWithZero R) (valuation R)
h' : Nonempty.{u_3 + 1} (Valuation.RankOne (Γ₀ := ValueGroupWithZero R) (valuation R))
pos : ∀ (f : Valuation.RankOne (Γ₀ := ValueGroupWithZero R) (valuation R)), IsRankLeOne R
⊢ IsRankLeOne R

Tactic:
obtain ⟨f⟩ := h'
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
H : Valuation.IsNontrivial (Γ₀ := ValueGroupWithZero R) (valuation R)
f : Valuation.RankOne (Γ₀ := ValueGroupWithZero R) (valuation R)
⊢ IsRankLeOne R

Tactic:
isRankLeOne_of_rankOne

Premises used: ValuativeRel.isRankLeOne_of_rankOne
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
H : Valuation.IsNontrivial (Γ₀ := ValueGroupWithZero R) (valuation R)
f : Valuation.RankOne (Γ₀ := ValueGroupWithZero R) (valuation R)
⊢ IsRankLeOne R

Tactic:
exact isRankLeOne_of_rankOne

Premises used: ValuativeRel.isRankLeOne_of_rankOne
-- 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
⊢ IsRankLeOne R

Tactic:
⟨⟨{ emb := 1, strictMono := ?_ }⟩⟩

Premises used: Nonempty.intro, ValuativeRel.RankLeOneStruct.mk, ValuativeRel.IsRankLeOne.mk, OfNat.ofNat
-- 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
neg : StrictMono.{u_3, 0} (α := ValueGroupWithZero R) (β := ℝ≥0) (⇑1 : (a : ValueGroupWithZero R) → ℝ≥0)
⊢ IsRankLeOne R

Tactic:
refine ⟨⟨{ emb := 1, strictMono := ?_ }⟩⟩