awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : K
⊢ a ∈ Subtype.val (p := fun (x : K) ↦ x ∈ A) '' (↑(IsLocalRing.maximalIdeal ↥A) : Set ↥A) ↔ a ∈ (↑A.nonunits : Set K)
have 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)
Tactic: simp only [Set.mem_image, SetLike.mem_coe, mem_nonunits_iff_exists_mem_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : K
⊢ (∃ (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)
have 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)
Tactic: rw [Subtype.exists]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : K
⊢ (∃ (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)
have 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 sorry) ∧
      a_1 = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ (∃ (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)
have 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 sorry)) ∧
      a_1 = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
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
⊢ 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 * b)
have ha₁ : 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 ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
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)
⊢ 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 * b)
have hb₁ : 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 ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
have 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)
Tactic: refine lt_of_le_of_lt ?_ (max_lt hb ha)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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) - 1) : A.ValueGroup)
    (max ((A.valuation : (a : K) → A.ValueGroup) ((↑b : K) - 1))
        ((A.valuation : (a : K) → A.ValueGroup) ((↑a : K) - 1)) :
      A.ValueGroup)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ 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)
have b₁ : K
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]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
| LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
have lhs : (A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1)
Tactic: lhs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
| (A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1)
have 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)
Tactic: rw [← mul_one (A.valuation _), ← A.valuation.map_one_add_of_lt ha]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
| LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
have 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)
Tactic: lhs
      rw [← mul_one (A.valuation _), ← A.valuation.map_one_add_of_lt ha]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) - 1) : A.ValueGroup) (1 : A.ValueGroup)
have 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
Tactic: conv =>
      lhs
      rw [← mul_one (A.valuation _), ← A.valuation.map_one_add_of_lt ha]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ 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
have 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
Tactic: rwa [add_sub_cancel, ← Valuation.map_mul, sub_mul, Units.inv_mul, ← neg_sub, one_mul,
      Valuation.map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
⊢ 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
have rwa₁ : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (((↑a⁻¹ : K) - 1) * (↑a : K)) : A.ValueGroup)
  (1 : A.ValueGroup)
Tactic: rwa [add_sub_cancel, ← Valuation.map_mul, sub_mul, Units.inv_mul, ← neg_sub, one_mul,
      Valuation.map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ 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
have rwa₂ : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) ((↑a⁻¹ : K) * (↑a : K) - 1 * (↑a : K)) : A.ValueGroup)
  (1 : A.ValueGroup)
Tactic: rwa [add_sub_cancel, ← Valuation.map_mul, sub_mul, Units.inv_mul, ← neg_sub, one_mul,
      Valuation.map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ 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
have rwa₃ : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (1 - 1 * (↑a : K)) : A.ValueGroup) (1 : A.ValueGroup)
Tactic: rwa [add_sub_cancel, ← Valuation.map_mul, sub_mul, Units.inv_mul, ← neg_sub, one_mul,
      Valuation.map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ 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
have rwa₄ : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (-(1 * (↑a : K) - 1)) : A.ValueGroup)
  (1 : A.ValueGroup)
Tactic: rwa [add_sub_cancel, ← Valuation.map_mul, sub_mul, Units.inv_mul, ← neg_sub, one_mul,
      Valuation.map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ 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
have rwa₅ : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (-((↑a : K) - 1)) : A.ValueGroup) (1 : A.ValueGroup)
Tactic: rwa [add_sub_cancel, ← Valuation.map_mul, sub_mul, Units.inv_mul, ← neg_sub, one_mul,
      Valuation.map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
⊢ B.principalUnitGroup ≤ A.principalUnitGroup ↔ A ≤ B
have mp : B.principalUnitGroup ≤ A.principalUnitGroup → A ≤ B
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
mp : B.principalUnitGroup ≤ A.principalUnitGroup → A ≤ B
⊢ B.principalUnitGroup ≤ A.principalUnitGroup ↔ A ≤ B
have mpr : A ≤ B → B.principalUnitGroup ≤ A.principalUnitGroup
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
⊢ x ∈ B
have pos : ∀ (h_1 : x = 0), x ∈ B
Tactic: by_cases h_1 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
⊢ x ∈ B
have neg : ∀ (h_1 : ¬x = 0), x ∈ B
Tactic: by_cases h_1 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
have pos : ∀ (h_2 : x⁻¹ + 1 = 0), x ∈ B
Tactic: by_cases h_2 : x⁻¹ + 1 = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
⊢ x ∈ B
have neg : ∀ (h_2 : ¬x⁻¹ + 1 = 0), x ∈ B
Tactic: by_cases h_2 : x⁻¹ + 1 = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
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 ∈ B
have h_2₁ : x = -1
Tactic: rw [add_eq_zero_iff_eq_neg, inv_eq_iff_eq_inv, inv_neg, inv_one] at h_2
Cleared hypotheses: h_2
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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 ∈ B
have 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
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 ⊢
Cleared hypotheses: hx, h_1, h_2
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : x ∈ B.principalUnitGroup
⊢ x ∈ A.principalUnitGroup
have mpr : ∀ (h_1 : x ∉ A.principalUnitGroup), False
Tactic: by_contra h_1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
⊢ (↑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)ˣ)
have 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)
Tactic: rw [MonoidHom.mem_ker, Units.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* HasQuotient.Quotient ↥A (B := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) :=
  Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ (↑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)
have convert_3 : (↑x : Kˣ) ∈ A.principalUnitGroup ↔
  Eq (α := HasQuotient.Quotient ↥A (B := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A))
    ((π : (a : ↥A) → ↥A ⧸ IsLocalRing.maximalIdeal ↥A) (↑((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x) : ↥A)) 1
Tactic: convert_to _ ↔ π _ = 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* HasQuotient.Quotient ↥A (B := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) :=
  Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ (↑x : Kˣ) ∈ A.principalUnitGroup ↔
    Eq (α := HasQuotient.Quotient ↥A (B := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A))
      ((π : (a : ↥A) → ↥A ⧸ IsLocalRing.maximalIdeal ↥A) (↑((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x) : ↥A))
      1
have convert_3 : (↑x : Kˣ) ∈ A.principalUnitGroup ↔
  LT.lt (α := A.ValueGroup)
    ((A.valuation : (a : K) → A.ValueGroup)
        (↑(HSub.hSub (α := ↥A) (↑((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x) : ↥A) 1) : K) :
      A.ValueGroup)
    (1 : A.ValueGroup)
Tactic: rw [← π.map_one, ← sub_eq_zero, ← π.map_sub, Ideal.Quotient.eq_zero_iff_mem, valuation_lt_one_iff]