awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : IsDomain 𝒪
inst_4 : ValuationRing 𝒪
h :
  (∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a) ∧
    Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
⊢ IsFractionRing 𝒪 K

Tactic:
isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective h.1 h.2

Premises used: And.right, And.left, isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : IsDomain 𝒪
inst_4 : ValuationRing 𝒪
h :
  (∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a) ∧
    Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
⊢ IsFractionRing 𝒪 K

Tactic:
exact isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective h.1 h.2

Premises used: And.right, And.left, isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
K : Type u
inst : Field K
⊢ ValuationRing K

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
toSubring : Subring K
mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier
this :
  ∀ (toSubring_1 : Subring K) (mem_or_inv_mem'_1 : ∀ (x : K), x ∈ toSubring_1.carrier ∨ x⁻¹ ∈ toSubring_1.carrier),
    Eq.{u + 1} (α := Set K)
        ((fun (A : ValuationSubring K) ↦ (↑A.toSubring : Set K))
          { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' })
        ((fun (A : ValuationSubring K) ↦ (↑A.toSubring : Set K))
          { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }) →
      { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } =
        { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }
⊢ ∀ ⦃a₂ : ValuationSubring K⦄,
    Eq.{u + 1} (α := Set K)
        ((fun (A : ValuationSubring K) ↦ (↑A.toSubring : Set K))
          { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' })
        ((fun (A : ValuationSubring K) ↦ (↑A.toSubring : Set K)) a₂) →
      { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } = a₂

Tactic:
⟨_, _⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
toSubring : Subring K
mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier
toSubring_1 : Subring K
mem_or_inv_mem'_1 : ∀ (x : K), x ∈ toSubring_1.carrier ∨ x⁻¹ ∈ toSubring_1.carrier
h :
  Eq.{u + 1} (α := Set K)
    ((fun (A : ValuationSubring K) ↦ (↑A.toSubring : Set K))
      { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' })
    ((fun (A : ValuationSubring K) ↦ (↑A.toSubring : Set K))
      { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 })
⊢ { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K }.toSubring =
    { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }.toSubring

Tactic:
replace h := SetLike.coe_injective' h
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
toSubring : Subring K
mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier
toSubring_1 : Subring K
mem_or_inv_mem'_1 : ∀ (x : K), x ∈ toSubring_1.carrier ∨ x⁻¹ ∈ toSubring_1.carrier
h :
  { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K }.toSubring =
    { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }.toSubring
⊢ { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } =
    { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }

Tactic:
congr
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
⊢ x ∈ A.carrier ↔ x ∈ A

Tactic:
Iff.refl _

Premises used: Set.Mem, Iff.refl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
⊢ x ∈ A.toSubring ↔ x ∈ A

Tactic:
Iff.refl _

Premises used: Set.Mem, Iff.refl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : ∀ (x : K), x ∈ A ↔ x ∈ B
⊢ A = B

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ 0 ∈ A

Tactic:
A.toSubring.zero_mem

Premises used: Subring.zero_mem, Set.Mem, ValuationSubring.toSubring
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ 1 ∈ A

Tactic:
A.toSubring.one_mem

Premises used: Set.Mem, ValuationSubring.toSubring, Subring.one_mem
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x y : K
⊢ x ∈ A → y ∈ A → x + y ∈ A

Tactic:
A.toSubring.add_mem

Premises used: Subring.add_mem, Set.Mem, ValuationSubring.toSubring
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x y : K
⊢ x ∈ A → y ∈ A → x * y ∈ A

Tactic:
A.toSubring.mul_mem

Premises used: Set.Mem, Subring.mul_mem, ValuationSubring.toSubring
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
⊢ x ∈ A → -x ∈ A

Tactic:
A.toSubring.neg_mem

Premises used: Set.Mem, Subring.neg_mem, ValuationSubring.toSubring
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
⊢ x ∈ A ∨ x⁻¹ ∈ A

Tactic:
A.mem_or_inv_mem' _

Premises used: Set.Mem, ValuationSubring.mem_or_inv_mem'
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
x y : ValuationSubring K
h : x.toSubring = y.toSubring
mk :
  ∀ (toSubring : Subring K) (mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier)
    (h : { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K }.toSubring = y.toSubring),
    { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } = y
⊢ x = y

Tactic:
cases x
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
y : ValuationSubring K
toSubring : Subring K
mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier
h : { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K }.toSubring = y.toSubring
mk :
  ∀ (toSubring_1 : Subring K) (mem_or_inv_mem'_1 : ∀ (x : K), x ∈ toSubring_1.carrier ∨ x⁻¹ ∈ toSubring_1.carrier)
    (h :
      { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K }.toSubring =
        { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }.toSubring),
    { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } =
      { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }
⊢ { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } = y

Tactic:
cases y
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
toSubring : Subring K
mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier
toSubring_1 : Subring K
mem_or_inv_mem'_1 : ∀ (x : K), x ∈ toSubring_1.carrier ∨ x⁻¹ ∈ toSubring_1.carrier
h :
  { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K }.toSubring =
    { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }.toSubring
⊢ { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } =
    { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }

Tactic:
congr
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ IsDomain.{u} ↥A

Tactic:
inferInstanceAs <| IsDomain A.toSubring

Premises used: _private.0.ValuationSubring.instIsDomainSubtypeMem._proof_1
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
⊢ Eq.{u + 1} (α := Subring K) (toSubring ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
x : K
⊢ Membership.mem (γ := ValuationSubring K) ⊤ x

Tactic:
trivial

Premises used: trivial, Set.Mem, Set.univ, setOf
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ A ≤ ⊤

Tactic:
fun _a _ha => mem_top _

Premises used: ValuationSubring.mem_top
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
x y : ↥⊤
⊢ (↑(x / y) : K) = (↑x : K) / (↑y : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
x : ↥⊤
⊢ (↑x⁻¹ : K) = (↑x : K)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
pos : ∀ (h : (↑b : K) = 0), ∃ (c : ↥A), a * c = b ∨ b * c = a
neg : ∀ (h : ¬(↑b : K) = 0), ∃ (c : ↥A), a * c = b ∨ b * c = a
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a

Tactic:
by_cases h : (b : K) = 0

Premises used: Subtype.val
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : (↑b : K) = 0
h₁ : a * 0 = b ∨ b * 0 = a
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a

Tactic:
use 0
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : (↑b : K) = 0
h₁ : a * 0 = b
⊢ a * 0 = b ∨ b * 0 = a

Tactic:
left
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : (↑b : K) = 0
h₁ : (↑(a * 0) : K) = (↑b : K)
⊢ a * 0 = b

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : (↑b : K) = 0
⊢ (↑(a * 0) : K) = (↑b : K)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : ¬(↑b : K) = 0
pos : ∀ (h : (↑a : K) = 0), ∃ (c : ↥A), a * c = b ∨ b * c = a
neg : ∀ (h : ¬(↑a : K) = 0), ∃ (c : ↥A), a * c = b ∨ b * c = a
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a

Tactic:
by_cases h : (a : K) = 0

Premises used: Subtype.val
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : (↑a : K) = 0
h₁ : a * 0 = b ∨ b * 0 = a
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a

Tactic:
use 0
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : (↑a : K) = 0
h₁ : b * 0 = a
⊢ a * 0 = b ∨ b * 0 = a

Tactic:
right
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : (↑a : K) = 0
h₁ : (↑(b * 0) : K) = (↑a : K)
⊢ b * 0 = a

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : (↑a : K) = 0
⊢ (↑(b * 0) : K) = (↑a : K)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
neg : ∀ (hh : (↑a : K) / (↑b : K) ∈ A), ∃ (c : ↥A), a * c = b ∨ b * c = a
neg₁ : ∀ (hh : ((↑a : K) / (↑b : K))⁻¹ ∈ A), ∃ (c : ↥A), a * c = b ∨ b * c = a
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a

Tactic:
rcases A.mem_or_inv_mem (a / b) with hh | hh

Premises used: ValuationSubring.mem_or_inv_mem, HDiv.hDiv, Subtype.val
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑a : K) / (↑b : K) ∈ A
h₁ :
  a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh = b ∨
    b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh = a
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a

Tactic:
use ⟨a / b, hh⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑a : K) / (↑b : K) ∈ A
h₁ : b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh = a
⊢ a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh = b ∨
    b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh = a

Tactic:
right
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑a : K) / (↑b : K) ∈ A
h₁ : (↑(b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh) : K) = (↑a : K)
⊢ b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh = a

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑a : K) / (↑b : K) ∈ A
⊢ (↑(b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh) : K) = (↑a : K)

Tactic:
simp [field]
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : ((↑a : K) / (↑b : K))⁻¹ ∈ A
⊢ ((↑a : K) / (↑b : K))⁻¹ = (↑b : K) / (↑a : K)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : ((↑a : K) / (↑b : K))⁻¹ ∈ A
⊢ (↑b : K) / (↑a : K) ∈ A

Tactic:
rw [show (a / b : K)⁻¹ = b / a by simp] at hh
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑b : K) / (↑a : K) ∈ A
h₁ :
  a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh = b ∨
    b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh = a
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a

Tactic:
use ⟨b / a, hh⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑b : K) / (↑a : K) ∈ A
h₁ : a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh = b
⊢ a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh = b ∨
    b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh = a

Tactic:
left
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑b : K) / (↑a : K) ∈ A
h₁ : (↑(a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh) : K) = (↑b : K)
⊢ a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh = b

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑b : K) / (↑a : K) ∈ A
⊢ (↑(a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh) : K) = (↑b : K)

Tactic:
simp [field]
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ IsLocalRing.{u} ↥A

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
⊢ (algebraMap (↥A) K : (a : ↥A) → K) a = (↑a : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
pos :
  ∀ (h : z = 0),
    ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
      HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
neg :
  ∀ (h : ¬z = 0),
    ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
      HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1

Tactic:
by_cases h : z = 0
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : z = 0
h₁ :
  HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑(0, 1).2 : ↥A) : K) =
    (algebraMap (↥A) K : (a : ↥A) → K) (0, 1).1
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1

Tactic:
use (0, 1)

Premises used: Prod.mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : z = 0
⊢ HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑(0, 1).2 : ↥A) : K) =
    (algebraMap (↥A) K : (a : ↥A) → K) (0, 1).1

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
neg :
  ∀ (hh : z ∈ A),
    ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
      HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
neg₁ :
  ∀ (hh : z⁻¹ ∈ A),
    ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
      HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1

Tactic:
rcases A.mem_or_inv_mem z with hh | hh

Premises used: ValuationSubring.mem_or_inv_mem
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z ∈ A
h₁ :
  HMul.hMul (β := K) z
      ((algebraMap (↥A) K : (a : ↥A) → K) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ A) z hh, 1).2 : ↥A) : K) =
    (algebraMap (↥A) K : (a : ↥A) → K) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) z hh, 1).1
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1

Tactic:
use (⟨z, hh⟩, 1)

Premises used: Prod.mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z ∈ A
⊢ HMul.hMul (β := K) z
      ((algebraMap (↥A) K : (a : ↥A) → K) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ A) z hh, 1).2 : ↥A) : K) =
    (algebraMap (↥A) K : (a : ↥A) → K) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) z hh, 1).1

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z⁻¹ ∈ A
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1

Tactic:
⟨⟨1, ⟨⟨_, hh⟩, ?_⟩⟩, mul_inv_cancel₀ h⟩

Premises used: mul_inv_cancel₀, Prod.mk, Subtype.mk, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z⁻¹ ∈ A
neg : Membership.mem (γ := Submonoid ↥A) (nonZeroDivisors ↥A) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) z⁻¹ hh)
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1

Tactic:
refine ⟨⟨1, ⟨⟨_, hh⟩, ?_⟩⟩, mul_inv_cancel₀ h⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z⁻¹ ∈ A
⊢ Membership.mem (γ := Submonoid ↥A) (nonZeroDivisors ↥A) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) z⁻¹ hh)

Tactic:
mem_nonZeroDivisors_iff_ne_zero.2 fun c => h (inv_eq_zero.mp (congr_arg Subtype.val c))

Premises used: Iff.mpr, inv_eq_zero, Set.Mem, congr_arg, Iff.mp, mem_nonZeroDivisors_iff_ne_zero, Subtype.val
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z⁻¹ ∈ A
⊢ Membership.mem (γ := Submonoid ↥A) (nonZeroDivisors ↥A) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) z⁻¹ hh)

Tactic:
exact mem_nonZeroDivisors_iff_ne_zero.2 fun c => h (inv_eq_zero.mp (congr_arg Subtype.val c))

Premises used: Iff.mpr, inv_eq_zero, Iff.mp, mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : Eq (α := K) ((algebraMap (↥A) K : (a : ↥A) → K) a : K) ((algebraMap (↥A) K : (a : ↥A) → K) b : K)
a₁ : (↑((↑1 : ↥A) * a) : K) = (↑((↑1 : ↥A) * b) : K)
⊢ (↑1 : ↥A) * a = (↑1 : ↥A) * b

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : Eq (α := K) ((algebraMap (↥A) K : (a : ↥A) → K) a : K) ((algebraMap (↥A) K : (a : ↥A) → K) b : K)
⊢ (↑((↑1 : ↥A) * a) : K) = (↑((↑1 : ↥A) * b) : K)

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
⊢ LE.le (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
(ValuationRing.mem_integer_iff A K _).2 ⟨a, rfl⟩

Premises used: ValuationRing.mem_integer_iff, Iff.mpr, Set.Mem, setOf, Membership.mem, Subtype, Exists.intro, rfl, Quotient.liftOn₂'
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
h : LE.le (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
⊢ x ∈ A

Tactic:
let ⟨a, ha⟩ := (ValuationRing.mem_integer_iff A K x).1 h
  ha ▸ a.2

Premises used: ValuationRing.mem_integer_iff, Membership.mem, Eq.rec, Subtype, _private.0.ValuationSubring.mem_of_valuation_le_one.match_1, Iff.mp, Subtype.property
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
⊢ LE.le (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ↔ x ∈ A

Tactic:
⟨mem_of_valuation_le_one _ _, fun ha => A.valuation_le_one ⟨x, ha⟩⟩

Premises used: ValuationSubring.mem_of_valuation_le_one, ValuationSubring.valuation_le_one, Subtype.mk, Iff.intro
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x y : K
⊢ Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup)
      ((A.valuation : (a : K) → A.ValueGroup) y : A.ValueGroup) ↔
    ∃ (a : (↥A)ˣ), (↑(↑a : ↥A) : K) * y = x

Tactic:
Quotient.eq''

Premises used: Set.Mem, ValuationSubring.ValueGroup, Quotient.eq'', ValuationRing.ValueGroup, setOf, MulAction.orbit, Set.range
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x y : K
⊢ LE.le (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup)
      ((A.valuation : (a : K) → A.ValueGroup) y : A.ValueGroup) ↔
    ∃ (a : ↥A), (↑a : K) * y = x

Tactic:
Iff.rfl

Premises used: Iff.rfl, Quotient.liftOn₂'
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ Function.Surjective (α := K) (β := A.ValueGroup) (⇑A.valuation : (a : K) → A.ValueGroup)

Tactic:
Quot.mk_surjective

Premises used: ValuationSubring.ValueGroup, ValuationRing.ValueGroup, Quotient, Quot.mk_surjective