awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : (↥A)ˣ
rw : ∃ (a_1 : (↥A)ˣ), (↑(↑a_1 : ↥A) : K) * 1 = (↑(↑a : ↥A) : K)
⊢ Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑(↑a : ↥A) : K) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
rw [← A.valuation.map_one, valuation_eq_iff]

Premises used: ValuationSubring.valuation, ValuationSubring.valuation_eq_iff, Valuation.map_one
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : (↥A)ˣ
h : (↑(↑a : ↥A) : K) * 1 = (↑(↑a : ↥A) : K)
⊢ ∃ (a_1 : (↥A)ˣ), (↑(↑a_1 : ↥A) : K) * 1 = (↑(↑a : ↥A) : K)

Tactic:
use a
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ (↑(↑a : ↥A) : K) * 1 = (↑(↑a : ↥A) : K)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
h : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)
c : (↑a : K) = 0
⊢ Eq.{u + 1} (α := A.ValueGroup) 0 1

Tactic:
rw [c, A.valuation.map_zero] at h

Premises used: ValuationSubring.valuation, Valuation.map_zero
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
h : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)
c : (↑a : K) = 0
h₁ : Eq.{u + 1} (α := A.ValueGroup) 0 1
⊢ (↑a : K) = 0

Tactic:
rw [c, A.valuation.map_zero] at h

Premises used: ValuationSubring.valuation, Valuation.map_zero
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
h : Eq.{u + 1} (α := A.ValueGroup) 0 1
c : (↑a : K) = 0
⊢ False

Tactic:
zero_ne_one h

Premises used: zero_ne_one
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
h : Eq.{u + 1} (α := A.ValueGroup) 0 1
c : (↑a : K) = 0
⊢ False

Tactic:
exact zero_ne_one h

Premises used: zero_ne_one
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
h : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)
⊢ (↑a : K) ≠ 0

Tactic:
have ha : (a : K) ≠ 0 := by
      intro c
      rw [c, A.valuation.map_zero] at h
      exact zero_ne_one h
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
h : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)
ha : (↑a : K) ≠ 0
rw : LE.le (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K)⁻¹ : A.ValueGroup) (1 : A.ValueGroup)
rw₁ : LE.le (α := A.ValueGroup) (((A.valuation : (a : K) → A.ValueGroup) (↑a : K))⁻¹ : A.ValueGroup) (1 : A.ValueGroup)
rw₂ : LE.le.{u} (α := A.ValueGroup) 1⁻¹ 1
rw₃ rw₄ : LE.le.{u} (α := A.ValueGroup) 1 1
⊢ (↑a : K)⁻¹ ∈ A

Tactic:
rw [← valuation_le_one_iff, map_inv₀, h, inv_one]

Premises used: inv_one, map_inv₀, ValuationSubring.valuation_le_one_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
h : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)
ha : (↑a : K) ≠ 0
⊢ (↑a : K)⁻¹ ∈ A

Tactic:
have ha' : (a : K)⁻¹ ∈ A := by rw [← valuation_le_one_iff, map_inv₀, h, inv_one]
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
h : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)
ha : (↑a : K) ≠ 0
ha' : (↑a : K)⁻¹ ∈ A
⊢ IsUnit a

Tactic:
.of_mul_eq_one ⟨a⁻¹, ha'⟩ ?_

Premises used: IsUnit.of_mul_eq_one, Subtype.mk, Inv.inv, Subtype.val
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
h : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)
ha : (↑a : K) ≠ 0
ha' : (↑a : K)⁻¹ ∈ A
refine : a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑a : K)⁻¹ ha' = 1
⊢ IsUnit a

Tactic:
refine .of_mul_eq_one ⟨a⁻¹, ha'⟩ ?_
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
h : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)
ha : (↑a : K) ≠ 0
ha' : (↑a : K)⁻¹ ∈ A
a₁ : (↑(a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑a : K)⁻¹ ha') : K) = (↑1 : K)
⊢ a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑a : K)⁻¹ ha' = 1

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
h : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)
ha : (↑a : K) ≠ 0
ha' : (↑a : K)⁻¹ ∈ A
⊢ (↑(a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑a : K)⁻¹ ha') : K) = (↑1 : K)

Tactic:
simp [field]
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ A = ⊤ ↔ ¬A.valuation.IsNontrivial

Tactic:
simp [Valuation.IsNontrivial_iff_exists_one_lt, SetLike.ext_iff]

Premises used: SetLike.ext_iff, Valuation.IsNontrivial_iff_exists_one_lt
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
⊢ LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
lt_or_eq_of_le (A.valuation_le_one a)

Premises used: lt_or_eq_of_le, ValuationSubring.valuation_le_one
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
rw :
  ¬Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup) ↔
    LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)
⊢ ¬IsUnit a ↔
    LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
rw [valuation_eq_one_iff]

Premises used: ValuationSubring.valuation_eq_one_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
⊢ ¬Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup) ↔
    LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
(A.valuation_le_one a).lt_iff_ne.symm

Premises used: ValuationSubring.valuation_le_one, LE.le.lt_iff_ne, Iff.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
⊢ ¬Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup) ↔
    LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)

Tactic:
exact (A.valuation_le_one a).lt_iff_ne.symm

Premises used: ValuationSubring.valuation_le_one, LE.le.lt_iff_ne, Iff.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R : Subring K
hR : ∀ (x : K), x ∈ R ∨ x⁻¹ ∈ R
x : K
⊢ x ∈ ofSubring R hR ↔ x ∈ R

Tactic:
Iff.refl _

Premises used: Set.Mem, Iff.refl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R : ValuationSubring K
x : ↥R
⊢ (R.subtype : (a : ↥R) → K) x = (↑x : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R : ValuationSubring K
⊢ Function.Injective (α := ↥R) (β := K) (⇑R.subtype : (a : ↥R) → K)

Tactic:
R.toSubring.subtype_injective

Premises used: Set.Mem, Subring.subtype_injective, ValuationSubring.toSubring
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R : ValuationSubring K
⊢ Eq (α := (a : ↥R) → K) (⇑R.subtype : (a : ↥R) → K) (Subtype.val (p := fun (x : K) ↦ x ∈ R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A R S : ValuationSubring K
h : R ≤ S
x : R.ValueGroup
a : K
y : R.ValueGroup
a_1 : K
⊢ Quotient.map' id ⋯
      (HMul.hMul (α := R.ValueGroup) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K) : K → K → Prop) a)
        (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K) : K → K → Prop) a_1)) =
    HMul.hMul (α := S.ValueGroup)
      (Quotient.map' (s₁ := MulAction.orbitRel (↥R)ˣ K) id ⋯ (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K) : K → K → Prop) a))
      (Quotient.map' (s₁ := MulAction.orbitRel (↥R)ˣ K) id ⋯
        (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K) : K → K → Prop) a_1))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
a_1 : R.ValueGroup
a_2 : K
b : R.ValueGroup
a_3 : K
a : ↥R
ha : a • a_3 = a_2
⊢ LE.le (α := S.ValueGroup)
    ((R.mapOfLE S h : (a : R.ValueGroup) → S.ValueGroup) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K) : K → K → Prop) a_2) :
      S.ValueGroup)
    ((R.mapOfLE S h : (a : R.ValueGroup) → S.ValueGroup) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K) : K → K → Prop) a_3) :
      S.ValueGroup)

Tactic:
⟨R.inclusion S h a, ha⟩

Premises used: Exists.intro, ValuationSubring.inclusion, DFunLike.coe, Quotient.liftOn₂'
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
a_1 : R.ValueGroup
a_2 : K
b : R.ValueGroup
a_3 : K
a : ↥R
ha : a • a_3 = a_2
⊢ LE.le (α := S.ValueGroup)
    ((R.mapOfLE S h : (a : R.ValueGroup) → S.ValueGroup) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K) : K → K → Prop) a_2) :
      S.ValueGroup)
    ((R.mapOfLE S h : (a : R.ValueGroup) → S.ValueGroup) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K) : K → K → Prop) a_3) :
      S.ValueGroup)

Tactic:
exact ⟨R.inclusion S h a, ha⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
h₁ :
  ∀ (x : K),
    Eq (α := S.ValueGroup)
      (Function.comp (β := R.ValueGroup) (⇑(R.mapOfLE S h) : (a : R.ValueGroup) → S.ValueGroup)
          (⇑R.valuation : (a : K) → R.ValueGroup) x :
        S.ValueGroup)
      ((S.valuation : (a : K) → S.ValueGroup) x : S.ValueGroup)
⊢ Eq (α := K → S.ValueGroup)
    (Function.comp (β := R.ValueGroup) (⇑(R.mapOfLE S h) : (a : R.ValueGroup) → S.ValueGroup)
      (⇑R.valuation : (a : K) → R.ValueGroup))
    (⇑S.valuation : (a : K) → S.ValueGroup)

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ Eq (α := S.ValueGroup)
    (Function.comp (β := R.ValueGroup) (⇑(R.mapOfLE S h) : (a : R.ValueGroup) → S.ValueGroup)
        (⇑R.valuation : (a : K) → R.ValueGroup) x :
      S.ValueGroup)
    ((S.valuation : (a : K) → S.ValueGroup) x : S.ValueGroup)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ Eq (α := S.ValueGroup)
    ((R.mapOfLE S h : (a : R.ValueGroup) → S.ValueGroup) ((R.valuation : (a : K) → R.ValueGroup) x) : S.ValueGroup)
    ((S.valuation : (a : K) → S.ValueGroup) x : S.ValueGroup)

Tactic:
rfl

Premises used: Quotient.map', rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ A.idealOfLE A ⋯ = IsLocalRing.maximalIdeal ↥A

Tactic:
rfl

Premises used: Set.Mem, setOf, IsLocalRing.maximalIdeal, nonunits, ValuationSubring.idealOfLE, Set.preimage, Ideal.comap, Not, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
hf : Function.Injective (α := ↥A) (β := ↥⊤) (⇑(A.inclusion ⊤ ⋯) : (a : ↥A) → ↥⊤)
⊢ A.idealOfLE ⊤ ⋯ = ⊥

Tactic:
rw [ValuationSubring.idealOfLE, IsLocalRing.maximalIdeal_eq_bot, Ideal.comap_bot_of_injective]

Premises used: IsLocalRing.maximalIdeal_eq_bot, ValuationSubring.idealOfLE, Ideal.comap_bot_of_injective
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ Function.Injective (α := ↥A) (β := ↥⊤) (⇑(A.inclusion ⊤ ⋯) : (a : ↥A) → ↥⊤)

Tactic:
Subring.inclusion_injective _

Premises used: Set.Mem, Subring.inclusion_injective
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ Function.Injective (α := ↥A) (β := ↥⊤) (⇑(A.inclusion ⊤ ⋯) : (a : ↥A) → ↥⊤)

Tactic:
exact Subring.inclusion_injective _

Premises used: Subring.inclusion_injective
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A R S : ValuationSubring K
h : R ≤ S
⊢ (R.idealOfLE S h).IsPrime

Tactic:
(IsLocalRing.maximalIdeal S).comap_isPrime _

Premises used: IsLocalRing.maximalIdeal, Membership.mem, ValuationSubring.idealOfLE, Subtype, Ideal.comap_isPrime
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A_1 A : ValuationSubring K
P : Ideal ↥A
inst_1 : P.IsPrime
⊢ IsScalarTower (↥A) (↥(A.ofPrime P)) K

Tactic:
IsScalarTower.subalgebra' A K K
    (Localization.subalgebra.ofField K _ P.primeCompl_le_nonZeroDivisors)

Premises used: Set.Mem, Localization.subalgebra.ofField, setOf, Membership.mem, Subtype, Ideal.primeCompl_le_nonZeroDivisors, IsScalarTower.subalgebra'
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A_1 A : ValuationSubring K
P : Ideal ↥A
inst_1 : P.IsPrime
⊢ IsLocalization.AtPrime (↥(A.ofPrime P)) P

Tactic:
Localization.subalgebra.isLocalization_ofField K P.primeCompl
    P.primeCompl_le_nonZeroDivisors

Premises used: Set.Mem, setOf, Localization.subalgebra.isLocalization_ofField, ValuationSubring.ofLE, Ideal.primeCompl_le_nonZeroDivisors, Ideal.primeCompl, ValuationSubring.ofPrime
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : Ideal ↥A
inst_1 : P.IsPrime
⊢ A ≤ A.ofPrime P

Tactic:
fun a ha => Subalgebra.mem_toSubring.mpr <| Subalgebra.algebraMap_mem _ (⟨a, ha⟩ : A)

Premises used: Iff.mpr, Set.Mem, Localization.subalgebra.ofField, ValuationSubring.ofPrime._proof_1, Subtype.mk, Subalgebra.algebraMap_mem, Ideal.primeCompl, Subalgebra.mem_toSubring
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : Ideal ↥A
inst_1 : P.IsPrime
x : ↥A
rw :
  Eq (α := (A.ofPrime P).ValueGroup)
      (((A.ofPrime P).valuation : (a : K) → (A.ofPrime P).ValueGroup) (↑x : K) : (A.ofPrime P).ValueGroup)
      (1 : (A.ofPrime P).ValueGroup) ↔
    Eq (α := (A.ofPrime P).ValueGroup)
      (((A.ofPrime P).valuation : (a : K) → (A.ofPrime P).ValueGroup)
        (↑((algebraMap ↥A ↥(A.ofPrime P) : (a : ↥A) → ↥(A.ofPrime P)) x) : K))
      1
⊢ Eq (α := (A.ofPrime P).ValueGroup)
      (((A.ofPrime P).valuation : (a : K) → (A.ofPrime P).ValueGroup) (↑x : K) : (A.ofPrime P).ValueGroup)
      (1 : (A.ofPrime P).ValueGroup) ↔
    x ∈ P.primeCompl

Tactic:
rw [← IsLocalization.AtPrime.isUnit_to_map_iff (A.ofPrime P) P x, valuation_eq_one_iff]

Premises used: Membership.mem, Subtype, IsLocalization.AtPrime.isUnit_to_map_iff, ValuationSubring.ofPrime, ValuationSubring.valuation_eq_one_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : Ideal ↥A
inst_1 : P.IsPrime
x : ↥A
⊢ Eq (α := (A.ofPrime P).ValueGroup)
      (((A.ofPrime P).valuation : (a : K) → (A.ofPrime P).ValueGroup) (↑x : K) : (A.ofPrime P).ValueGroup)
      (1 : (A.ofPrime P).ValueGroup) ↔
    Eq (α := (A.ofPrime P).ValueGroup)
      (((A.ofPrime P).valuation : (a : K) → (A.ofPrime P).ValueGroup)
        (↑((algebraMap ↥A ↥(A.ofPrime P) : (a : ↥A) → ↥(A.ofPrime P)) x) : K))
      1

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : Ideal ↥A
inst_1 : P.IsPrime
⊢ A.idealOfLE (A.ofPrime P) ⋯ = P

Tactic:
Ideal.ext (fun x => ?_)

Premises used: Ideal.ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : Ideal ↥A
inst_1 : P.IsPrime
refine : ∀ (x : ↥A), x ∈ A.idealOfLE (A.ofPrime P) ⋯ ↔ x ∈ P
⊢ A.idealOfLE (A.ofPrime P) ⋯ = P

Tactic:
refine Ideal.ext (fun x => ?_)

Premises used: Ideal.ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : Ideal ↥A
inst_1 : P.IsPrime
x : ↥A
h : optParam (IsLocalRing.{u} ↥(A.ofPrime P)) ⋯
⊢ x ∈ A.idealOfLE (A.ofPrime P) ⋯ ↔ x ∈ P

Tactic:
apply IsLocalization.AtPrime.to_map_mem_maximal_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : Ideal ↥A
inst_1 : P.IsPrime
x : ↥A
⊢ optParam (IsLocalRing.{u} ↥(A.ofPrime P)) ⋯

Tactic:
isLocalRing (ofPrime A P)

Premises used: ValuationSubring.isLocalRing, ValuationSubring.ofPrime
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : Ideal ↥A
inst_1 : P.IsPrime
x : ↥A
⊢ optParam (IsLocalRing.{u} ↥(A.ofPrime P)) ⋯

Tactic:
exact isLocalRing (ofPrime A P)

Premises used: ValuationSubring.isLocalRing, ValuationSubring.ofPrime
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
h₁ : ∀ (x : K), x ∈ R.ofPrime (R.idealOfLE S h) ↔ x ∈ S
⊢ R.ofPrime (R.idealOfLE S h) = S

Tactic:
ext x
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
h₁ : x ∈ R.ofPrime (R.idealOfLE S h) → x ∈ S
h₂ : x ∈ S → x ∈ R.ofPrime (R.idealOfLE S h)
⊢ x ∈ R.ofPrime (R.idealOfLE S h) ↔ x ∈ S

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
h₁ : Membership.mem (α := K) S ((algebraMap (↥R) K : (a : ↥R) → K) a : K)
h₂ : Membership.mem (α := K) S (((algebraMap (↥R) K : (a : ↥R) → K) r)⁻¹ : K)
⊢ HMul.hMul (α := K) (β := K) ((algebraMap (↥R) K : (a : ↥R) → K) a : K)
      (((algebraMap (↥R) K : (a : ↥R) → K) r)⁻¹ : K) ∈
    S

Tactic:
apply mul_mem

Premises used: ValuationSubring.mul_mem
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ Membership.mem (α := K) S ((algebraMap (↥R) K : (a : ↥R) → K) a : K)

Tactic:
h a.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ Membership.mem (α := K) S ((algebraMap (↥R) K : (a : ↥R) → K) a : K)

Tactic:
exact h a.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
h₁ :
  LE.le (α := S.ValueGroup) (1 : S.ValueGroup)
    ((S.valuation : (a : K) → S.ValueGroup) ((algebraMap (↥R) K : (a : ↥R) → K) r) : S.ValueGroup)
h₂ :
  LT.lt (α := S.ValueGroup) (0 : S.ValueGroup)
    ((S.valuation : (a : K) → S.ValueGroup) ((algebraMap (↥R) K : (a : ↥R) → K) r) : S.ValueGroup)
h₃ : LT.lt.{u} (α := S.ValueGroup) 0 1
⊢ Membership.mem (α := K) S (((algebraMap (↥R) K : (a : ↥R) → K) r)⁻¹ : K)

Tactic:
rw [← valuation_le_one_iff, map_inv₀, ← inv_one, inv_le_inv₀]

Premises used: inv_one, map_inv₀, ValuationSubring.valuation_le_one_iff, inv_le_inv₀
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ LE.le (α := S.ValueGroup) (1 : S.ValueGroup)
    ((S.valuation : (a : K) → S.ValueGroup) ((algebraMap (↥R) K : (a : ↥R) → K) r) : S.ValueGroup)

Tactic:
not_lt.1 ((not_iff_not.2 <| valuation_lt_one_iff S _).1 hr)

Premises used: not_iff_not, Iff.mpr, ValuationSubring.valuation_lt_one_iff, not_lt, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ LE.le (α := S.ValueGroup) (1 : S.ValueGroup)
    ((S.valuation : (a : K) → S.ValueGroup) ((algebraMap (↥R) K : (a : ↥R) → K) r) : S.ValueGroup)

Tactic:
exact not_lt.1 ((not_iff_not.2 <| valuation_lt_one_iff S _).1 hr)

Premises used: not_iff_not, Iff.mpr, ValuationSubring.valuation_lt_one_iff, not_lt, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ LT.lt (α := S.ValueGroup) (0 : S.ValueGroup)
    ((S.valuation : (a : K) → S.ValueGroup) ((algebraMap (↥R) K : (a : ↥R) → K) r) : S.ValueGroup)

Tactic:
simpa [Valuation.pos_iff] using fun hr₀ ↦ hr₀ ▸ hr <| Ideal.zero_mem (R.idealOfLE S h)

Premises used: Valuation.pos_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ LT.lt.{u} (α := S.ValueGroup) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ LT.lt.{u} (α := S.ValueGroup) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
pos : ∀ (hr : x ∈ R), x ∈ R.ofPrime (R.idealOfLE S h)
neg : ∀ (hr : x ∉ R), x ∈ R.ofPrime (R.idealOfLE S h)
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
by_cases hr : x ∈ R
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∈ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
R.le_ofPrime _ hr

Premises used: ValuationSubring.le_ofPrime
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∈ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
exact R.le_ofPrime _ hr

Premises used: ValuationSubring.le_ofPrime
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h_1 : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
h : x = 0
rw : 0 ∈ R
⊢ x ∈ R

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h_1 : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
h : x = 0
⊢ 0 ∈ R

Tactic:
R.zero_mem

Premises used: ValuationSubring.zero_mem
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h_1 : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
h : x = 0
⊢ 0 ∈ R

Tactic:
exact R.zero_mem

Premises used: ValuationSubring.zero_mem
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
⊢ x ≠ 0

Tactic:
have : x ≠ 0 := fun h => hr (by rw [h]; exact R.zero_mem)
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
this : x ≠ 0
⊢ x⁻¹ ∈ R

Tactic:
replace hr := (R.mem_or_inv_mem x).resolve_left hr
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
⟨1, ⟨x⁻¹, hr⟩, ?_, ?_⟩

Premises used: Set.Mem, setOf, Subtype.mk, Inv.inv, Exists.intro, OfNat.ofNat