awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ : Type u_1
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ
inst_2 : LinearOrderedCommGroupWithZero Γ₁
inst_3 : LinearOrderedCommGroupWithZero Γ₂
v : Valuation K Γ
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
x : K
inl : ∀ (h : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ)), x ∈ v.integer.carrier ∨ x⁻¹ ∈ v.integer.carrier
inr : ∀ (h : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x⁻¹ : Γ) (1 : Γ)), x ∈ v.integer.carrier ∨ x⁻¹ ∈ v.integer.carrier
⊢ x ∈ v.integer.carrier ∨ x⁻¹ ∈ v.integer.carrier

Tactic:
rcases val_le_one_or_val_inv_le_one v x with h | h

Premises used: Valuation.val_le_one_or_val_inv_le_one
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ : Type u_1
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ
inst_2 : LinearOrderedCommGroupWithZero Γ₁
inst_3 : LinearOrderedCommGroupWithZero Γ₂
v : Valuation K Γ
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
x : K
h : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ)
⊢ x ∈ v.integer.carrier ∨ x⁻¹ ∈ v.integer.carrier

Tactic:
Or.inl h

Premises used: Or.inl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ : Type u_1
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ
inst_2 : LinearOrderedCommGroupWithZero Γ₁
inst_3 : LinearOrderedCommGroupWithZero Γ₂
v : Valuation K Γ
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
x : K
h : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x⁻¹ : Γ) (1 : Γ)
⊢ x ∈ v.integer.carrier ∨ x⁻¹ ∈ v.integer.carrier

Tactic:
Or.inr h

Premises used: Or.inr
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ : Type u_1
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ
inst_2 : LinearOrderedCommGroupWithZero Γ₁
inst_3 : LinearOrderedCommGroupWithZero Γ₂
v : Valuation K Γ
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
x : K
h : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ)
⊢ x ∈ v.integer.carrier ∨ x⁻¹ ∈ v.integer.carrier

Tactic:
exacts [Or.inl h, Or.inr h]

Premises used: Or.inl, Or.inr
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ : Type u_1
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
x : K
⊢ x ∈ v.valuationSubring ↔ LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ)

Tactic:
Iff.refl _

Premises used: Set.Mem, Iff.refl, setOf
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
mp : v₁.IsEquiv v₂ → v₁.valuationSubring = v₂.valuationSubring
mpr : v₁.valuationSubring = v₂.valuationSubring → v₁.IsEquiv v₂
⊢ v₁.IsEquiv v₂ ↔ v₁.valuationSubring = v₂.valuationSubring

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.IsEquiv v₂
mp : ∀ (x : K), x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring
⊢ v₁.valuationSubring = v₂.valuationSubring

Tactic:
ext x
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.IsEquiv v₂
x : K
⊢ LE.le.{u_2} (α := Γ₁) ((v₁ : (a : K) → Γ₁) x : Γ₁) ((v₁ : (a : K) → Γ₁) 1 : Γ₁) ↔
    LE.le.{u_3} (α := Γ₂) ((v₂ : (a : K) → Γ₂) x : Γ₂) ((v₂ : (a : K) → Γ₂) 1 : Γ₂)

Tactic:
specialize h x 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
x : K
h :
  LE.le.{u_2} (α := Γ₁) ((v₁ : (a : K) → Γ₁) x : Γ₁) ((v₁ : (a : K) → Γ₁) 1 : Γ₁) ↔
    LE.le.{u_3} (α := Γ₂) ((v₂ : (a : K) → Γ₂) x : Γ₂) ((v₂ : (a : K) → Γ₂) 1 : Γ₂)
⊢ x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
mpr :
  ∀ (x : K),
    LE.le.{u_2} (α := Γ₁) ((v₁ : (a : K) → Γ₁) x : Γ₁) (1 : Γ₁) ↔
      LE.le.{u_3} (α := Γ₂) ((v₂ : (a : K) → Γ₂) x : Γ₂) (1 : Γ₂)
⊢ v₁.IsEquiv v₂

Tactic:
apply isEquiv_of_val_le_one

Premises used: Valuation.isEquiv_of_val_le_one
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
x : K
rw rw₁ : x ∈ v₂.valuationSubring ↔ x ∈ v₂.valuationSubring
⊢ x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
x : K
⊢ x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring

Tactic:
have : x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring := by rw [h]
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
x : K
this : x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring
⊢ LE.le.{u_2} (α := Γ₁) ((v₁ : (a : K) → Γ₁) x : Γ₁) (1 : Γ₁) ↔
    LE.le.{u_3} (α := Γ₂) ((v₂ : (a : K) → Γ₂) x : Γ₂) (1 : Γ₂)

Tactic:
simpa using this
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ : Type u_1
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
rw :
  ∀ {x : K},
    LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ) ↔
      LE.le (α := v.valuationSubring.ValueGroup)
        ((v.valuationSubring.valuation : (a : K) → v.valuationSubring.ValueGroup) x : v.valuationSubring.ValueGroup)
        (1 : v.valuationSubring.ValueGroup)
⊢ v.IsEquiv v.valuationSubring.valuation

Tactic:
rw [isEquiv_iff_val_le_one]

Premises used: Valuation.isEquiv_iff_val_le_one
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ : Type u_1
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
x : K
rw : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ) ↔ x ∈ v.valuationSubring
rw₁ rw₂ :
  LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ) ↔ LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ)
⊢ LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ) ↔
    LE.le (α := v.valuationSubring.ValueGroup)
      ((v.valuationSubring.valuation : (a : K) → v.valuationSubring.ValueGroup) x : v.valuationSubring.ValueGroup)
      (1 : v.valuationSubring.ValueGroup)

Tactic:
rw [ValuationSubring.valuation_le_one_iff, mem_valuationSubring_iff]

Premises used: Valuation.mem_valuationSubring_iff, ValuationSubring.valuation_le_one_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ : Type u_1
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ v.valuationSubring.valuation.IsNontrivial ↔ v.IsNontrivial

Tactic:
(isEquiv_valuation_valuationSubring v).isNontrivial_iff.symm

Premises used: Valuation.IsEquiv.isNontrivial_iff, Valuation.isEquiv_valuation_valuationSubring, Iff.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ : Type u_1
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ v.Integers ↥v.valuationSubring

Tactic:
Valuation.integer.integers _

Premises used: Set.Mem, Subsemiring.ofClass, setOf, Valuation.integer.integers, Valuation.integer, Valuation.valuationSubring
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ : Type u_1
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ v.valuationSubring = ⊤ ↔ ¬v.IsNontrivial

Tactic:
simp [ValuationSubring.eq_top_iff]

Premises used: ValuationSubring.eq_top_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
h : ∀ (x : K), x ∈ A.valuation.valuationSubring ↔ x ∈ A
⊢ A.valuation.valuationSubring = A

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
h :
  x ∈ A.valuation.valuationSubring ↔
    LE.le (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
⊢ x ∈ A.valuation.valuationSubring ↔ x ∈ A

Tactic:
rw [← A.valuation_le_one_iff]

Premises used: ValuationSubring.valuation_le_one_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
⊢ x ∈ A.valuation.valuationSubring ↔
    LE.le (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ A.valuation.integer = A.toSubring

Tactic:
congr(($A.valuationSubring_valuation).toSubring)

Premises used: congrArg, id, ValuationSubring.toSubring, ValuationSubring.valuationSubring_valuation
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : Kˣ
⊢ x ∈ A.unitGroup ↔
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑x : K) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
⊢ (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑x : Kˣ) : K) ⋯ *
          Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑x⁻¹ : Kˣ) : K) ⋯) :
      K) =
    (↑1 : K)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
⊢ (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑x⁻¹ : Kˣ) : K) ⋯ *
          Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑x : Kˣ) : K) ⋯) :
      K) =
    (↑1 : K)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A.unitGroup
huv :
  (↑(↑{ val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑(a * b) : Kˣ) : K) ⋯,
              inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑(a * b)⁻¹ : Kˣ) : K) ⋯, val_inv := ⋯, inv_val := ⋯ :
              (↥A)ˣ } :
          ↥A) :
      K) =
    (↑(↑({ val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑a : Kˣ) : K) ⋯,
                inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑a⁻¹ : Kˣ) : K) ⋯, val_inv := ⋯, inv_val := ⋯ :
                (↥A)ˣ } *
              { val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑b : Kˣ) : K) ⋯,
                inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑b⁻¹ : Kˣ) : K) ⋯, val_inv := ⋯, inv_val := ⋯ :
                (↥A)ˣ }) :
          ↥A) :
      K)
⊢ { val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑(a * b) : Kˣ) : K) ⋯,
      inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑(a * b)⁻¹ : Kˣ) : K) ⋯, val_inv := ⋯, inv_val := ⋯ : (↥A)ˣ } =
    { val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑a : Kˣ) : K) ⋯,
        inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑a⁻¹ : Kˣ) : K) ⋯, val_inv := ⋯, inv_val := ⋯ : (↥A)ˣ } *
      { val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑b : Kˣ) : K) ⋯,
        inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑b⁻¹ : Kˣ) : K) ⋯, val_inv := ⋯, inv_val := ⋯ : (↥A)ˣ }

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A.unitGroup
⊢ (↑(↑{ val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑(a * b) : Kˣ) : K) ⋯,
              inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑(a * b)⁻¹ : Kˣ) : K) ⋯, val_inv := ⋯, inv_val := ⋯ :
              (↥A)ˣ } :
          ↥A) :
      K) =
    (↑(↑({ val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑a : Kˣ) : K) ⋯,
                inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑a⁻¹ : Kˣ) : K) ⋯, val_inv := ⋯, inv_val := ⋯ :
                (↥A)ˣ } *
              { val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑b : Kˣ) : K) ⋯,
                inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑b⁻¹ : Kˣ) : K) ⋯, val_inv := ⋯, inv_val := ⋯ :
                (↥A)ˣ }) :
          ↥A) :
      K)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A.unitGroup
⊢ (↑(↑((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) a) : ↥A) : K) = (↑(↑a : Kˣ) : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ (↑(↑((A.unitGroupMulEquiv.symm : (a : (↥A)ˣ) → ↥A.unitGroup) a) : Kˣ) : K) = (↑(↑a : ↥A) : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
mp : A.unitGroup ≤ B.unitGroup → A ≤ B
mpr : A ≤ B → A.unitGroup ≤ B.unitGroup
⊢ A.unitGroup ≤ B.unitGroup ↔ A ≤ B

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : x ∈ A
⊢ LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
rw [← A.valuation_le_one_iff x, le_iff_lt_or_eq] at hx

Premises used: ValuationSubring.valuation_le_one_iff, le_iff_lt_or_eq
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
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 : A.unitGroup ≤ B.unitGroup
x : K
hx :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
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 : A.unitGroup ≤ B.unitGroup
x : K
hx :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
h_1 : ¬x = 0
pos : ∀ (h_2 : 1 + x = 0), x ∈ B
neg : ∀ (h_2 : ¬1 + x = 0), x ∈ B
⊢ x ∈ B

Tactic:
by_cases h_2 : 1 + x = 0
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
h_1 : ¬x = 0
h_2 : 1 + x = 0
⊢ x ∈ B

Tactic:
simp only [← add_eq_zero_iff_neg_eq.1 h_2, neg_mem _ _ (one_mem _)]

Premises used: ValuationSubring.neg_mem, add_eq_zero_iff_neg_eq, ValuationSubring.one_mem, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
neg :
  ∀ (hx : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)), x ∈ B
neg₁ :
  ∀ (hx : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)), x ∈ B
⊢ x ∈ B

Tactic:
rcases hx with hx | hx
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
⊢ Membership.mem (α := Kˣ) B.unitGroup (Units.mk0 (1 + x) h_2 : Kˣ)

Tactic:
have := h (show Units.mk0 _ h_2 ∈ A.unitGroup from A.valuation.map_one_add_of_lt hx)
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
this : Membership.mem (α := Kˣ) B.unitGroup (Units.mk0 (1 + x) h_2 : Kˣ)
⊢ x ∈ B

Tactic:
simpa using
        B.add_mem _ _ (show 1 + x ∈ B from SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B))
          (B.neg_mem _ B.one_mem)

Premises used: Units.val, SetLike.coe_mem, ValuationSubring.unitGroupMulEquiv, ValuationSubring.neg_mem, Subtype.mk, ValuationSubring.add_mem, Units.mk0, HAdd.hAdd, ValuationSubring.one_mem, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
⊢ Membership.mem (α := Kˣ) B.unitGroup (Units.mk0 x h_1 : Kˣ)

Tactic:
have := h (show Units.mk0 x h_1 ∈ A.unitGroup from hx)
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
this : Membership.mem (α := Kˣ) B.unitGroup (Units.mk0 x h_1 : Kˣ)
⊢ x ∈ B

Tactic:
SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B)

Premises used: Units.val, SetLike.coe_mem, ValuationSubring.unitGroupMulEquiv, Set.Mem, Subtype.mk, Units.mk0, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
this : Membership.mem (α := Kˣ) B.unitGroup (Units.mk0 x h_1 : Kˣ)
⊢ x ∈ B

Tactic:
exact SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B)

Premises used: Units.val, SetLike.coe_mem, ValuationSubring.unitGroupMulEquiv, Subtype.mk, Units.mk0, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑x : K) : A.ValueGroup) (1 : A.ValueGroup)
⊢ Eq (α := B.ValueGroup)
    ((A.mapOfLE B h : (a : A.ValueGroup) → B.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑x : K)) :
      B.ValueGroup)
    ((A.mapOfLE B h : (a : A.ValueGroup) → B.ValueGroup) 1 : B.ValueGroup)

Tactic:
apply_fun A.mapOfLE B h at hx

Premises used: ValuationSubring.mapOfLE
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx :
  Eq (α := B.ValueGroup)
    ((A.mapOfLE B h : (a : A.ValueGroup) → B.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑x : K)) :
      B.ValueGroup)
    ((A.mapOfLE B h : (a : A.ValueGroup) → B.ValueGroup) 1 : B.ValueGroup)
⊢ x ∈ B.unitGroup

Tactic:
simpa using hx
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup = B.unitGroup
⊢ A = B

Tactic:
simpa only [le_antisymm_iff, unitGroup_le_unitGroup] using h

Premises used: ValuationSubring.unitGroup_le_unitGroup, le_antisymm_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
⊢ A = B ↔ A.unitGroup = B.unitGroup

Tactic:
unitGroup_injective.eq_iff.symm

Premises used: Function.Injective.eq_iff, ValuationSubring.unitGroup_injective, Iff.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
⊢ StrictMono.{u, u} (α := ValuationSubring K) unitGroup

Tactic:
unitGroupOrderEmbedding.strictMono

Premises used: ValuationSubring.unitGroup, OrderEmbedding.strictMono, MonoidHom.ker, ValuationSubring.unitGroupOrderEmbedding
-- 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 : A.ValueGroup) (1 : A.ValueGroup)} 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
⊢ x ∈ A.nonunits ↔
    LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : 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 : ValuationSubring K
x : K
rw : x = 0 → x ∈ A.nonunits
⊢ x ∈ A.nonunits ↔ x = 0 ∨ x⁻¹ ∉ A

Tactic:
rw [← valuation_le_one_iff, ← or_congr_right' fun h ↦ (A.valuation.one_le_val_iff h).not,
    ← lt_iff_not_ge, ← mem_nonunits_iff, or_iff_right_of_imp]

Premises used: lt_iff_not_ge, or_congr_right', ValuationSubring.valuation, Iff.not, ValuationSubring.valuation_le_one_iff, or_iff_right_of_imp, ValuationSubring.mem_nonunits_iff, Valuation.one_le_val_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ 0 ∈ A.nonunits

Tactic:
A.nonunits.zero_mem

Premises used: Set.Mem, NonUnitalSubring.zero_mem, setOf, ValuationSubring.nonunits
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ 0 ∈ A.nonunits

Tactic:
exact A.nonunits.zero_mem

Premises used: NonUnitalSubring.zero_mem, ValuationSubring.nonunits
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
rw : x⁻¹ = 0 ∨ x⁻¹⁻¹ ∉ A ↔ x = 0 ∨ x ∉ A
rw₁ : x⁻¹ = 0 ∨ x ∉ A ↔ x = 0 ∨ x ∉ A
rw₂ rw₃ : x = 0 ∨ x ∉ A ↔ x = 0 ∨ x ∉ A
⊢ x⁻¹ ∈ A.nonunits ↔ x = 0 ∨ x ∉ A

Tactic:
rw [mem_nonunits_iff_or, inv_inv, inv_eq_zero]

Premises used: inv_eq_zero, inv_inv, ValuationSubring.mem_nonunits_iff_or
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
mp : B.nonunits ≤ A.nonunits → A ≤ B
mpr : A ≤ B → B.nonunits ≤ A.nonunits
⊢ B.nonunits ≤ A.nonunits ↔ A ≤ B

Tactic:
constructor
-- 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
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.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : x = 0
⊢ x ∈ B

Tactic:
simp only [h_1, zero_mem]

Premises used: ValuationSubring.zero_mem