awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : ¬x = 0
neg :
  ∀ (hx : ¬LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x⁻¹ : A.ValueGroup) (1 : A.ValueGroup))
    (h_1 : ¬x = 0),
    ¬LT.lt (α := B.ValueGroup) ((B.valuation : (a : K) → B.ValueGroup) x⁻¹ : B.ValueGroup) (1 : B.ValueGroup)
⊢ x ∈ B

Tactic:
rw [← valuation_le_one_iff, ← not_lt, Valuation.one_lt_val_iff _ h_1] at hx ⊢

Premises used: Valuation.one_lt_val_iff, ValuationSubring.valuation_le_one_iff, not_lt
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : ¬LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x⁻¹ : A.ValueGroup) (1 : A.ValueGroup)
h_1 : ¬x = 0
neg :
  ∀ (h_2 : LT.lt (α := B.ValueGroup) ((B.valuation : (a : K) → B.ValueGroup) x⁻¹ : B.ValueGroup) (1 : B.ValueGroup)),
    False
⊢ ¬LT.lt (α := B.ValueGroup) ((B.valuation : (a : K) → B.ValueGroup) x⁻¹ : B.ValueGroup) (1 : B.ValueGroup)

Tactic:
by_contra h_2
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : ¬LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x⁻¹ : A.ValueGroup) (1 : A.ValueGroup)
h_1 : ¬x = 0
h_2 : LT.lt (α := B.ValueGroup) ((B.valuation : (a : K) → B.ValueGroup) x⁻¹ : B.ValueGroup) (1 : B.ValueGroup)
⊢ False

Tactic:
hx (h h_2)
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : ¬LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x⁻¹ : A.ValueGroup) (1 : A.ValueGroup)
h_1 : ¬x = 0
h_2 : LT.lt (α := B.ValueGroup) ((B.valuation : (a : K) → B.ValueGroup) x⁻¹ : B.ValueGroup) (1 : B.ValueGroup)
⊢ False

Tactic:
exact hx (h h_2)
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A ≤ B
x : K
hx : x ∈ B.nonunits
mpr : ∀ (h_1 : x ∉ A.nonunits), False
⊢ x ∈ A.nonunits

Tactic:
by_contra h_1
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A ≤ B
x : K
hx : x ∈ B.nonunits
h_1 : x ∉ A.nonunits
⊢ False

Tactic:
not_lt.2 (monotone_mapOfLE _ _ h (not_lt.1 h_1)) hx

Premises used: Iff.mpr, ValuationSubring.monotone_mapOfLE, not_lt, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A ≤ B
x : K
hx : x ∈ B.nonunits
h_1 : x ∉ A.nonunits
⊢ False

Tactic:
exact not_lt.2 (monotone_mapOfLE _ _ h (not_lt.1 h_1)) hx

Premises used: Iff.mpr, ValuationSubring.monotone_mapOfLE, not_lt, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.nonunits = B.nonunits
⊢ A = B

Tactic:
simpa only [le_antisymm_iff, nonunits_le_nonunits] using h.symm

Premises used: ValuationSubring.nonunits_le_nonunits, le_antisymm_iff, Eq.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
⊢ A.nonunits = B.nonunits ↔ A = B

Tactic:
nonunits_injective.eq_iff

Premises used: ValuationSubring.nonunits_injective, Function.Injective.eq_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
⊢ (↑a : K) ∈ A.nonunits ↔ Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) a

Tactic:
(valuation_lt_one_iff _ _).symm

Premises used: ValuationSubring.valuation_lt_one_iff, Set.Mem, setOf, Iff.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ A.nonunits ≤ A.toNonUnitalSubring

Tactic:
fun _a ha =>
  (A.valuation_le_one_iff _).mp (A.mem_nonunits_iff.mp ha).le

Premises used: Set.Mem, ValuationSubring.valuation_le_one_iff, LT.lt.le, Iff.mp, ValuationSubring.mem_nonunits_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ (↑A.nonunits : Set K) ⊆ (↑A : Set K)

Tactic:
nonunits_le

Premises used: Set.Mem, Set.Subset, ValuationSubring.nonunits_le
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : K
⊢ a ∈ A.nonunits ↔
    ∃ (ha : a ∈ A),
      Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) a ha)

Tactic:
⟨fun h => ⟨nonunits_subset h, coe_mem_nonunits_iff.mp h⟩, fun ⟨_, h⟩ =>
    coe_mem_nonunits_iff.mpr h⟩

Premises used: Iff.mpr, ValuationSubring.nonunits_subset, Membership.mem, ValuationSubring.coe_mem_nonunits_iff, ValuationSubring.nonunits, _private.0.ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal.match_1, Iff.intro, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
h :
  ∀ (a : K),
    a ∈ Subtype.val (p := fun (x : K) ↦ x ∈ A) '' (↑(IsLocalRing.maximalIdeal ↥A) : Set ↥A) ↔ a ∈ (↑A.nonunits : Set K)
⊢ Subtype.val (p := fun (x : K) ↦ x ∈ A) '' (↑(IsLocalRing.maximalIdeal ↥A) : Set ↥A) = (↑A.nonunits : Set K)

Tactic:
ext a
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : K
h :
  (∃ (x : ↥A), Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) x ∧ (↑x : K) = a) ↔
    ∃ (ha : a ∈ A),
      Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) a ha)
⊢ a ∈ Subtype.val (p := fun (x : K) ↦ x ∈ A) '' (↑(IsLocalRing.maximalIdeal ↥A) : Set ↥A) ↔ a ∈ (↑A.nonunits : Set K)

Tactic:
simp only [Set.mem_image, SetLike.mem_coe, mem_nonunits_iff_exists_mem_maximalIdeal]

Premises used: Set.mem_image, ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal, SetLike.mem_coe
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : K
h :
  (∃ (a_1 : K) (b : a_1 ∈ A),
      Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) (Subtype.mk (p := fun (a : K) ↦ a ∈ A) a_1 b) ∧
        (↑(Subtype.mk (p := fun (a : K) ↦ a ∈ A) a_1 b) : K) = a) ↔
    ∃ (ha : a ∈ A),
      Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) a ha)
⊢ (∃ (x : ↥A), Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) x ∧ (↑x : K) = a) ↔
    ∃ (ha : a ∈ A),
      Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) a ha)

Tactic:
rw [Subtype.exists]

Premises used: Subtype.exists
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : K
h h₁ :
  (∃ (a_1 : K) (h : a_1 ∈ A),
      Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) (Subtype.mk (p := fun (a : K) ↦ a ∈ A) a_1 ⋯) ∧
        a_1 = a) ↔
    ∃ (ha : a ∈ A),
      Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) a ha)
h₂ :
  (∃ (a_1 : K),
      (∃ (x : a_1 ∈ A),
          Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) (Subtype.mk (p := fun (a : K) ↦ a ∈ A) a_1 ⋯)) ∧
        a_1 = a) ↔
    ∃ (ha : a ∈ A),
      Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) a ha)
⊢ (∃ (a_1 : K) (b : a_1 ∈ A),
      Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) (Subtype.mk (p := fun (a : K) ↦ a ∈ A) a_1 b) ∧
        (↑(Subtype.mk (p := fun (a : K) ↦ a ∈ A) a_1 b) : K) = a) ↔
    ∃ (ha : a ∈ A),
      Membership.mem (γ := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) a ha)

Tactic:
simp_rw [exists_and_right, exists_eq_right]

Premises used: exists_eq_right, exists_and_right
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : Kˣ
ha :
  Membership.mem (γ := Set Kˣ)
    {x : Kˣ |
      LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑x : K) - 1) : A.ValueGroup)
        (1 : A.ValueGroup)}
    a
hb :
  Membership.mem (γ := Set Kˣ)
    {x : Kˣ |
      LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑x : K) - 1) : A.ValueGroup)
        (1 : A.ValueGroup)}
    b
⊢ LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
rw [Set.mem_setOf] at ha hb ⊢

Premises used: Set.mem_setOf
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : Kˣ
ha :
  Membership.mem (γ := Set Kˣ)
    {x : Kˣ |
      LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑x : K) - 1) : A.ValueGroup)
        (1 : A.ValueGroup)}
    a
hb :
  Membership.mem (γ := Set Kˣ)
    {x : Kˣ |
      LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑x : K) - 1) : A.ValueGroup)
        (1 : A.ValueGroup)}
    b
ha₁ :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
⊢ LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑b : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
rw [Set.mem_setOf] at ha hb ⊢

Premises used: Set.mem_setOf
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : Kˣ
ha : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
hb : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑b : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
⊢ LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑(a * b) : K) - 1) : A.ValueGroup)
    (1 : A.ValueGroup)

Tactic:
lt_of_le_of_lt ?_ (max_lt hb ha)

Premises used: lt_of_le_of_lt, max_lt
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : Kˣ
ha : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
hb : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑b : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
refine :
  LE.le (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑(a * b) : K) - 1) : A.ValueGroup)
    (max ((A.valuation : (a : K) → A.ValueGroup) ((↑b : K) - 1))
        ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1)) :
      A.ValueGroup)
⊢ LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑(a * b) : K) - 1) : A.ValueGroup)
    (1 : A.ValueGroup)

Tactic:
refine lt_of_le_of_lt ?_ (max_lt hb ha)

Premises used: lt_of_le_of_lt, max_lt
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : Kˣ
ha : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
hb : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑b : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
rw :
  LE.le (α := A.ValueGroup)
    ((A.valuation : (a : K) → A.ValueGroup) ((↑(a * b) : K) - (↑a : K) + ((↑a : K) - 1)) : A.ValueGroup)
    (max ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) * (↑b : K) - (↑a : K)))
        ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1)) :
      A.ValueGroup)
b₁ : K
⊢ LE.le (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑(a * b) : K) - 1) : A.ValueGroup)
    (max ((A.valuation : (a : K) → A.ValueGroup) ((↑b : K) - 1))
        ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1)) :
      A.ValueGroup)

Tactic:
rw [← one_mul (A.valuation (b - 1)), ← A.valuation.map_one_add_of_lt ha, add_sub_cancel,
      ← Valuation.map_mul, mul_sub_one, ← sub_add_sub_cancel]

Premises used: Units.val, Valuation.map_one_add_of_lt, sub_add_sub_cancel, HSub.hSub, ValuationSubring.valuation, Valuation.map_mul, mul_sub_one, add_sub_cancel, OfNat.ofNat, DFunLike.coe, one_mul
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : Kˣ
ha : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
hb : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑b : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
⊢ LE.le (α := A.ValueGroup)
    ((A.valuation : (a : K) → A.ValueGroup) ((↑(a * b) : K) - (↑a : K) + ((↑a : K) - 1)) : A.ValueGroup)
    (max ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) * (↑b : K) - (↑a : K)))
        ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1)) :
      A.ValueGroup)

Tactic:
A.valuation.map_add _ _

Premises used: Valuation.map_add, ValuationSubring.valuation
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ Membership.mem (γ := Set Kˣ)
    {x : Kˣ |
      LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑x : K) - 1) : A.ValueGroup)
        (1 : A.ValueGroup)}
    1

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : Kˣ
ha : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
lhs : (A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1)
| LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
lhs
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : Kˣ
ha : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
rw :
  HMul.hMul (α := A.ValueGroup) (β := A.ValueGroup)
    ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1) : A.ValueGroup)
    ((A.valuation : (a : K) → A.ValueGroup) (1 + ((↑a : K) - 1)) : A.ValueGroup)
| (A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1)

Tactic:
rw [← mul_one (A.valuation _), ← A.valuation.map_one_add_of_lt ha]

Premises used: Valuation.map_one_add_of_lt, ValuationSubring.valuation, mul_one, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : Kˣ
ha : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
rw :
  HMul.hMul (α := A.ValueGroup) (β := A.ValueGroup)
    ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1) : A.ValueGroup)
    ((A.valuation : (a : K) → A.ValueGroup) (1 + ((↑a : K) - 1)) : A.ValueGroup)
| LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
lhs
      rw [← mul_one (A.valuation _), ← A.valuation.map_one_add_of_lt ha]

Premises used: Valuation.map_one_add_of_lt, ValuationSubring.valuation, mul_one, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : Kˣ
ha : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
conv :
  HMul.hMul (α := A.ValueGroup) (β := A.ValueGroup)
      ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1) : A.ValueGroup)
      ((A.valuation : (a : K) → A.ValueGroup) (1 + ((↑a : K) - 1)) : A.ValueGroup) <
    1
⊢ LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
conv =>
      lhs
      rw [← mul_one (A.valuation _), ← A.valuation.map_one_add_of_lt ha]

Premises used: Valuation.map_one_add_of_lt, ValuationSubring.valuation, mul_one, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : Kˣ
ha : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
rwa :
  HMul.hMul (α := A.ValueGroup) (β := A.ValueGroup)
      ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1) : A.ValueGroup)
      ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) <
    1
rwa₁ :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (((↑a⁻¹ : K) - 1) * (↑a : K)) : A.ValueGroup)
    (1 : A.ValueGroup)
rwa₂ :
  LT.lt (α := A.ValueGroup)
    ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) * (↑a : K) - 1 * (↑a : K)) : A.ValueGroup) (1 : A.ValueGroup)
rwa₃ :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (1 - 1 * (↑a : K)) : A.ValueGroup)
    (1 : A.ValueGroup)
rwa₄ :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (-(1 * (↑a : K) - 1)) : A.ValueGroup)
    (1 : A.ValueGroup)
rwa₅ :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (-((↑a : K) - 1)) : A.ValueGroup) (1 : A.ValueGroup)
rwa₆ rwa₇ rwa₈ rwa₉ :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
⊢ HMul.hMul (α := A.ValueGroup) (β := A.ValueGroup)
      ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1) : A.ValueGroup)
      ((A.valuation : (a : K) → A.ValueGroup) (1 + ((↑a : K) - 1)) : A.ValueGroup) <
    1

Tactic:
rwa [add_sub_cancel, ← Valuation.map_mul, sub_mul, Units.inv_mul, ← neg_sub, one_mul,
      Valuation.map_neg]

Premises used: neg_sub, Units.inv_mul, Valuation.map_mul, sub_mul, add_sub_cancel, Valuation.map_neg, one_mul
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : Kˣ
h : a ∈ A.principalUnitGroup
⊢ a ∈ A.unitGroup

Tactic:
simpa only [add_sub_cancel] using A.valuation.map_one_add_of_lt h

Premises used: Valuation.map_one_add_of_lt, ValuationSubring.valuation, add_sub_cancel
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : Kˣ
⊢ x ∈ A.principalUnitGroup ↔
    LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑x : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
mp : B.principalUnitGroup ≤ A.principalUnitGroup → A ≤ B
mpr : A ≤ B → B.principalUnitGroup ≤ A.principalUnitGroup
⊢ B.principalUnitGroup ≤ A.principalUnitGroup ↔ A ≤ B

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
pos : ∀ (h_1 : x = 0), x ∈ B
neg : ∀ (h_1 : ¬x = 0), x ∈ B
⊢ x ∈ B

Tactic:
by_cases h_1 : x = 0
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : x = 0
⊢ x ∈ B

Tactic:
simp only [h_1, zero_mem]

Premises used: ValuationSubring.zero_mem
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
pos : ∀ (h_2 : x⁻¹ + 1 = 0), x ∈ B
neg : ∀ (h_2 : ¬x⁻¹ + 1 = 0), x ∈ B
⊢ x ∈ B

Tactic:
by_cases h_2 : x⁻¹ + 1 = 0
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : x⁻¹ + 1 = 0
⊢ x = -1

Tactic:
rw [add_eq_zero_iff_eq_neg, inv_eq_iff_eq_inv, inv_neg, inv_one] at h_2

Premises used: inv_one, inv_neg, add_eq_zero_iff_eq_neg, inv_eq_iff_eq_inv
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : x = -1
⊢ x ∈ B

Tactic:
simpa only [h_2] using B.neg_mem _ B.one_mem

Premises used: ValuationSubring.neg_mem, ValuationSubring.one_mem
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : ¬x⁻¹ + 1 = 0
neg :
  ∀ (hx : ¬LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x⁻¹ : A.ValueGroup) (1 : A.ValueGroup))
    (hx :
      ¬LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (x⁻¹ + 1 - 1) : A.ValueGroup)
          (1 : A.ValueGroup))
    (h_1 : ¬x = 0) (h_2 : ¬x⁻¹ + 1 = 0) (hx : (Units.mk0 (x⁻¹ + 1) h_2 : Kˣ) ∉ A.principalUnitGroup),
    (Units.mk0 (x⁻¹ + 1) h_2 : Kˣ) ∉ B.principalUnitGroup
⊢ x ∈ B

Tactic:
rw [← valuation_le_one_iff, ← not_lt, Valuation.one_lt_val_iff _ h_1,
        ← add_sub_cancel_right x⁻¹, ← Units.val_mk0 h_2, ← mem_principalUnitGroup_iff] at hx ⊢

Premises used: Valuation.one_lt_val_iff, ValuationSubring.valuation_le_one_iff, Inv.inv, not_lt, ValuationSubring.mem_principalUnitGroup_iff, add_sub_cancel_right, Units.val_mk0
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx_1 : ¬LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x⁻¹ : A.ValueGroup) (1 : A.ValueGroup)
hx_2 :
  ¬LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (x⁻¹ + 1 - 1) : A.ValueGroup) (1 : A.ValueGroup)
h_1 : ¬x = 0
h_2 : ¬x⁻¹ + 1 = 0
hx : (Units.mk0 (x⁻¹ + 1) h_2 : Kˣ) ∉ A.principalUnitGroup
⊢ (Units.mk0 (x⁻¹ + 1) h_2 : Kˣ) ∉ B.principalUnitGroup

Tactic:
simpa only [hx] using @h (Units.mk0 (x⁻¹ + 1) h_2)
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : x ∈ B.principalUnitGroup
mpr : ∀ (h_1 : x ∉ A.principalUnitGroup), False
⊢ x ∈ A.principalUnitGroup

Tactic:
by_contra h_1
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : x ∈ B.principalUnitGroup
h_1 : x ∉ A.principalUnitGroup
⊢ False

Tactic:
not_lt.2 (monotone_mapOfLE _ _ h (not_lt.1 h_1)) hx

Premises used: Iff.mpr, ValuationSubring.monotone_mapOfLE, not_lt, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : x ∈ B.principalUnitGroup
h_1 : x ∉ A.principalUnitGroup
⊢ False

Tactic:
exact not_lt.2 (monotone_mapOfLE _ _ h (not_lt.1 h_1)) hx

Premises used: Iff.mpr, ValuationSubring.monotone_mapOfLE, not_lt, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.principalUnitGroup = B.principalUnitGroup
⊢ A = B

Tactic:
simpa [le_antisymm_iff, principalUnitGroup_le_principalUnitGroup] using h.symm

Premises used: ValuationSubring.principalUnitGroup_le_principalUnitGroup, le_antisymm_iff, Eq.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
⊢ A = B ↔ A.principalUnitGroup = B.principalUnitGroup

Tactic:
principalUnitGroup_injective.eq_iff.symm

Premises used: Function.Injective.eq_iff, Iff.symm, ValuationSubring.principalUnitGroup_injective
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
rw :
  (↑x : Kˣ) ∈ A.principalUnitGroup ↔
    Eq.{u + 1} (α := IsLocalRing.ResidueField ↥A)
      (↑((Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A) :
              (a : (↥A)ˣ) → (IsLocalRing.ResidueField ↥A)ˣ)
            ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x)) :
        IsLocalRing.ResidueField ↥A)
      (↑1 : IsLocalRing.ResidueField ↥A)
⊢ (↑x : Kˣ) ∈ A.principalUnitGroup ↔
    Membership.mem (α := (↥A)ˣ) (γ := Subgroup (↥A)ˣ)
      (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))
      ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x : (↥A)ˣ)

Tactic:
rw [MonoidHom.mem_ker, Units.ext_iff]

Premises used: Units.ext_iff, MonoidHom.mem_ker