awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg : Subtype.mk (p := fun (x : K) ↦ x ∈ R) x⁻¹ hr ∈ (R.idealOfLE S h).primeCompl
neg₁ :
  x =
    HMul.hMul (α := K) (β := K) ((algebraMap (↥R) K : (a : ↥R) → K) 1 : K)
      (((algebraMap (↥R) K : (a : ↥R) → K) (Subtype.mk (p := fun (x : K) ↦ x ∈ R) x⁻¹ hr))⁻¹ : K)
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
refine ⟨1, ⟨x⁻¹, 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
neg : IsUnit (M := ↥S) ((R.inclusion S h : (a : ↥R) → ↥S) (Subtype.mk (p := fun (x : K) ↦ x ∈ R) x⁻¹ hr) : ↥S)
⊢ Subtype.mk (p := fun (x : K) ↦ x ∈ R) x⁻¹ hr ∈ (R.idealOfLE S h).primeCompl

Tactic:
simp only [Ideal.primeCompl, Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_compl_iff,
        SetLike.mem_coe, idealOfLE, Ideal.mem_comap, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
        not_not]

Premises used: Classical.not_not, mem_nonunits_iff, IsLocalRing.mem_maximalIdeal, ValuationSubring.idealOfLE, Subsemigroup.mem_mk, Submonoid.mem_mk, SetLike.mem_coe, Ideal.primeCompl, Ideal.mem_comap, Set.mem_compl_iff
-- 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
neg : IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ S) x⁻¹ ⋯)
⊢ IsUnit (M := ↥S) ((R.inclusion S h : (a : ↥R) → ↥S) (Subtype.mk (p := fun (x : K) ↦ x ∈ R) x⁻¹ hr) : ↥S)

Tactic:
change IsUnit (⟨x⁻¹, h hr⟩ : S)

Premises used: IsUnit, Subtype.mk, Inv.inv
-- 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
⊢ IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ S) x⁻¹ ⋯)

Tactic:
.of_mul_eq_one (⟨x, hx⟩ : S) ?_

Premises used: IsUnit.of_mul_eq_one, Subtype.mk
-- 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
neg : Subtype.mk (p := fun (x : K) ↦ x ∈ S) x⁻¹ ⋯ * Subtype.mk (p := fun (x : K) ↦ x ∈ S) x hx = 1
⊢ IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ S) x⁻¹ ⋯)

Tactic:
refine .of_mul_eq_one (⟨x, hx⟩ : S) ?_
-- 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
neg : (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ S) x⁻¹ ⋯ * Subtype.mk (p := fun (x : K) ↦ x ∈ S) x hx) : K) = (↑1 : K)
⊢ Subtype.mk (p := fun (x : K) ↦ x ∈ S) x⁻¹ ⋯ * Subtype.mk (p := fun (x : K) ↦ x ∈ S) x hx = 1

Tactic:
ext
-- 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
⊢ (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ S) x⁻¹ ⋯ * Subtype.mk (p := fun (x : K) ↦ x ∈ S) x hx) : K) = (↑1 : K)

Tactic:
simp [field]
-- 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 =
    HMul.hMul (α := K) (β := K) ((algebraMap (↥R) K : (a : ↥R) → K) 1 : K)
      (((algebraMap (↥R) K : (a : ↥R) → K) (Subtype.mk (p := fun (x : K) ↦ x ∈ R) x⁻¹ hr))⁻¹ : K)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ A.ofPrime ⊥ = ⊤

Tactic:
simp [← idealOfLE_top]

Premises used: ValuationSubring.idealOfLE_top
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ A.ofPrime (IsLocalRing.maximalIdeal ↥A) = A

Tactic:
simp [← idealOfLE_self]

Premises used: ValuationSubring.idealOfLE_self
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P Q : Ideal ↥A
inst_1 : P.IsPrime
inst_2 : Q.IsPrime
h : P ≤ Q
⊢ A.ofPrime Q ≤ A.ofPrime P

Tactic:
fun _x ⟨a, s, hs, he⟩ => ⟨a, s, fun c => hs (h c), he⟩

Premises used: _private.0.ValuationSubring.ofPrime_le_of_le.match_1, Membership.mem, Exists.intro, ValuationSubring.ofPrime
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
by_contra! :
  ∀
    (c :
      LE.le (α := R.ValueGroup) 1
        ((R.valuation : (a : K) → R.ValueGroup) (↑((A.inclusion R hR : (a : ↥A) → ↥R) x) : K))),
    False
⊢ LT.lt (α := R.ValueGroup) ((R.valuation : (a : K) → R.ValueGroup) (↑((A.inclusion R hR : (a : ↥A) → ↥R) x) : K)) 1

Tactic:
by_contra! c
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : LE.le (α := R.ValueGroup) 1 ((R.valuation : (a : K) → R.ValueGroup) (↑((A.inclusion R hR : (a : ↥A) → ↥R) x) : K))
⊢ LE.le (α := S.ValueGroup) ((R.mapOfLE S h : (a : R.ValueGroup) → S.ValueGroup) 1)
    ((R.mapOfLE S h : (a : R.ValueGroup) → S.ValueGroup)
      ((R.valuation : (a : K) → R.ValueGroup) (↑((A.inclusion R hR : (a : ↥A) → ↥R) x) : K)))

Tactic:
replace c := monotone_mapOfLE R S h c
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c :
  LE.le (α := S.ValueGroup) ((R.mapOfLE S h : (a : R.ValueGroup) → S.ValueGroup) 1)
    ((R.mapOfLE S h : (a : R.ValueGroup) → S.ValueGroup)
      ((R.valuation : (a : K) → R.ValueGroup) (↑((A.inclusion R hR : (a : ↥A) → ↥R) x) : K)))
⊢ LE.le (α := S.ValueGroup) 1 ((S.valuation : (a : K) → S.ValueGroup) (↑((A.inclusion R hR : (a : ↥A) → ↥R) x) : K))

Tactic:
rw [(mapOfLE _ _ _).map_one, mapOfLE_valuation_apply] at c

Premises used: ValuationSubring.mapOfLE_valuation_apply, MonoidWithZeroHom.map_one, ValuationSubring.mapOfLE
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : LE.le (α := S.ValueGroup) 1 ((S.valuation : (a : K) → S.ValueGroup) (↑((A.inclusion R hR : (a : ↥A) → ↥R) x) : K))
⊢ False

Tactic:
apply not_le_of_gt ((valuation_lt_one_iff S _).1 hx) c

Premises used: ValuationSubring.valuation_lt_one_iff, Iff.mp, not_le_of_gt
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : PrimeSpectrum ↥A
asIdeal :
  PrimeSpectrum.asIdeal
      ((fun (S : { S : ValuationSubring K // A ≤ S }) ↦
          { asIdeal := A.idealOfLE (↑S : ValuationSubring K) ⋯, isPrime := ⋯ : PrimeSpectrum ↥A })
        ((fun (P : PrimeSpectrum ↥A) ↦ Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime P.asIdeal) ⋯)
          P)) =
    P.asIdeal
⊢ (fun (S : { S : ValuationSubring K // A ≤ S }) ↦
        { asIdeal := A.idealOfLE (↑S : ValuationSubring K) ⋯, isPrime := ⋯ : PrimeSpectrum ↥A })
      ((fun (P : PrimeSpectrum ↥A) ↦ Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime P.asIdeal) ⋯)
        P) =
    P

Tactic:
ext1
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : PrimeSpectrum ↥A
⊢ PrimeSpectrum.asIdeal
      ((fun (S : { S : ValuationSubring K // A ≤ S }) ↦
          { asIdeal := A.idealOfLE (↑S : ValuationSubring K) ⋯, isPrime := ⋯ : PrimeSpectrum ↥A })
        ((fun (P : PrimeSpectrum ↥A) ↦ Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime P.asIdeal) ⋯)
          P)) =
    P.asIdeal

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
S : { S : ValuationSubring K // A ≤ S }
a :
  (↑((fun (P : PrimeSpectrum ↥A) ↦ Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime P.asIdeal) ⋯)
          ((fun (S : { S : ValuationSubring K // A ≤ S }) ↦
              { asIdeal := A.idealOfLE (↑S : ValuationSubring K) ⋯, isPrime := ⋯ : PrimeSpectrum ↥A })
            S)) :
      ValuationSubring K) =
    (↑S : ValuationSubring K)
⊢ (fun (P : PrimeSpectrum ↥A) ↦ Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime P.asIdeal) ⋯)
      ((fun (S : { S : ValuationSubring K // A ≤ S }) ↦
          { asIdeal := A.idealOfLE (↑S : ValuationSubring K) ⋯, isPrime := ⋯ : PrimeSpectrum ↥A })
        S) =
    S

Tactic:
ext1
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
S : { S : ValuationSubring K // A ≤ S }
⊢ (↑((fun (P : PrimeSpectrum ↥A) ↦ Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime P.asIdeal) ⋯)
          ((fun (S : { S : ValuationSubring K // A ≤ S }) ↦
              { asIdeal := A.idealOfLE (↑S : ValuationSubring K) ⋯, isPrime := ⋯ : PrimeSpectrum ↥A })
            S)) :
      ValuationSubring K) =
    (↑S : ValuationSubring K)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a_1 b_1 : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h :
  LE.le (α := { S : ValuationSubring K // A ≤ S })
    ((Equiv.trans OrderDual.ofDual A.primeSpectrumEquiv :
          (a : (PrimeSpectrum ↥A)ᵒᵈ) → { S : ValuationSubring K // A ≤ S })
        ((OrderDual.toDual : (a : PrimeSpectrum ↥A) → (PrimeSpectrum ↥A)ᵒᵈ) a) :
      { S : ValuationSubring K // A ≤ S })
    ((Equiv.trans OrderDual.ofDual A.primeSpectrumEquiv :
          (a : (PrimeSpectrum ↥A)ᵒᵈ) → { S : ValuationSubring K // A ≤ S })
        ((OrderDual.toDual : (a : PrimeSpectrum ↥A) → (PrimeSpectrum ↥A)ᵒᵈ) b) :
      { S : ValuationSubring K // A ≤ S })
simp : b ≤ a
⊢ LE.le (α := (PrimeSpectrum ↥A)ᵒᵈ)
    ((OrderDual.toDual : (a : PrimeSpectrum ↥A) → (PrimeSpectrum ↥A)ᵒᵈ) a : (PrimeSpectrum ↥A)ᵒᵈ)
    ((OrderDual.toDual : (a : PrimeSpectrum ↥A) → (PrimeSpectrum ↥A)ᵒᵈ) b : (PrimeSpectrum ↥A)ᵒᵈ)

Tactic:
simp only [OrderDual.toDual_le_toDual]

Premises used: OrderDual.toDual_le_toDual
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a_1 b_1 : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h :
  Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) ⋯ ≤
    Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) ⋯
refine_3 :
  ∀
    (this :
      A.idealOfLE
          (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) ⋯) : ValuationSubring K) ⋯ ≤
        A.idealOfLE
          (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) ⋯) : ValuationSubring K) ⋯),
    b ≤ a
refine_1 : A ≤ (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) ⋯) : ValuationSubring K)
refine_2 : A ≤ (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) ⋯) : ValuationSubring K)
⊢ b ≤ a

Tactic:
have := idealOfLE_le_of_le A _ _ ?_ ?_ h
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a_1 b_1 : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h :
  Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) ⋯ ≤
    Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) ⋯
this :
  A.idealOfLE (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) ⋯) : ValuationSubring K)
      ⋯ ≤
    A.idealOfLE (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) ⋯) : ValuationSubring K)
      ⋯
refine_3 :
  ∀
    (this :
      b.asIdeal ≤
        A.idealOfLE
          (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) ⋯) : ValuationSubring K) ⋯),
    b ≤ a
refine_3₁ refine_3₂ refine_3₃ refine_3₄ : ∀ (this : b.asIdeal ≤ a.asIdeal), b ≤ a
⊢ b ≤ a

Tactic:
rwa [idealOfLE_ofPrime, idealOfLE_ofPrime] at this

Premises used: ValuationSubring.idealOfLE_ofPrime
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a_1 b_1 : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h :
  Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) ⋯ ≤
    Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) ⋯
⊢ A ≤ (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) ⋯) : ValuationSubring K)

Tactic:
le_ofPrime A (PrimeSpectrum.asIdeal _)

Premises used: Set.Mem, setOf, ValuationSubring.le_ofPrime, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a_1 b_1 : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h :
  Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) ⋯ ≤
    Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) ⋯
⊢ A ≤ (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) ⋯) : ValuationSubring K)

Tactic:
exact le_ofPrime A (PrimeSpectrum.asIdeal _)

Premises used: ValuationSubring.le_ofPrime, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a_1 b_1 : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h :
  Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) ⋯ ≤
    Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) ⋯
⊢ A ≤ (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) ⋯) : ValuationSubring K)

Tactic:
le_ofPrime A (PrimeSpectrum.asIdeal _)

Premises used: Set.Mem, setOf, ValuationSubring.le_ofPrime, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a_1 b_1 : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h :
  Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) ⋯ ≤
    Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) ⋯
⊢ A ≤ (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) ⋯) : ValuationSubring K)

Tactic:
exact le_ofPrime A (PrimeSpectrum.asIdeal _)

Premises used: ValuationSubring.le_ofPrime, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : (PrimeSpectrum ↥A)ᵒᵈ
h : a ≤ b
h₁ :
  LE.le.{u} (α := Ideal ↥A)
    (PrimeSpectrum.asIdeal ((OrderDual.ofDual : (a : (PrimeSpectrum ↥A)ᵒᵈ) → PrimeSpectrum ↥A) b))
    (PrimeSpectrum.asIdeal ((OrderDual.ofDual : (a : (PrimeSpectrum ↥A)ᵒᵈ) → PrimeSpectrum ↥A) a))
⊢ LE.le (α := { S : ValuationSubring K // A ≤ S })
    ((Equiv.trans OrderDual.ofDual A.primeSpectrumEquiv :
          (a : (PrimeSpectrum ↥A)ᵒᵈ) → { S : ValuationSubring K // A ≤ S })
        a :
      { S : ValuationSubring K // A ≤ S })
    ((Equiv.trans OrderDual.ofDual A.primeSpectrumEquiv :
          (a : (PrimeSpectrum ↥A)ᵒᵈ) → { S : ValuationSubring K // A ≤ S })
        b :
      { S : ValuationSubring K // A ≤ S })

Tactic:
apply ofPrime_le_of_le

Premises used: ValuationSubring.ofPrime_le_of_le
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : (PrimeSpectrum ↥A)ᵒᵈ
h : a ≤ b
⊢ LE.le.{u} (α := Ideal ↥A)
    (PrimeSpectrum.asIdeal ((OrderDual.ofDual : (a : (PrimeSpectrum ↥A)ᵒᵈ) → PrimeSpectrum ↥A) b))
    (PrimeSpectrum.asIdeal ((OrderDual.ofDual : (a : (PrimeSpectrum ↥A)ᵒᵈ) → PrimeSpectrum ↥A) a))

Tactic:
h

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : (PrimeSpectrum ↥A)ᵒᵈ
h : a ≤ b
⊢ LE.le.{u} (α := Ideal ↥A)
    (PrimeSpectrum.asIdeal ((OrderDual.ofDual : (a : (PrimeSpectrum ↥A)ᵒᵈ) → PrimeSpectrum ↥A) b))
    (PrimeSpectrum.asIdeal ((OrderDual.ofDual : (a : (PrimeSpectrum ↥A)ᵒᵈ) → PrimeSpectrum ↥A) a))

Tactic:
exact h
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
h : Std.Total fun (x1 x2 : PrimeSpectrum ↥A) ↦ x1 ≤ x2 := ⋯
⊢ Std.Total fun (x1 x2 : { S : ValuationSubring K // A ≤ S }) ↦ x1 ≤ x2

Tactic:
(primeSpectrumOrderEquiv A).symm.toRelEmbedding.total

Premises used: ValuationSubring.primeSpectrumOrderEquiv, OrderIso.symm, RelEmbedding.total, RelIso.toRelEmbedding
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
h : Std.Total fun (x1 x2 : PrimeSpectrum ↥A) ↦ x1 ≤ x2 := ⋯
⊢ Std.Total fun (x1 x2 : { S : ValuationSubring K // A ≤ S }) ↦ x1 ≤ x2

Tactic:
exact (primeSpectrumOrderEquiv A).symm.toRelEmbedding.total

Premises used: ValuationSubring.primeSpectrumOrderEquiv, OrderIso.symm, RelEmbedding.total, RelIso.toRelEmbedding
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
let let₁ let₂ : Std.Total fun (x1 x2 : { S : ValuationSubring K // A ≤ S }) ↦ x1 ≤ x2
⊢ Std.Total fun (x1 x2 : { S : ValuationSubring K // A ≤ S }) ↦ x1 ≤ x2

Tactic:
classical
  let _ : @Std.Total (PrimeSpectrum A) (· ≤ ·) := ⟨fun ⟨x, _⟩ ⟨y, _⟩ => LE.total.total x y⟩
  exact (primeSpectrumOrderEquiv A).symm.toRelEmbedding.total
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
inl :
  ∀
    (h :
      Eq (α := PrimeSpectrum ↥A)
        ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
            (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle) :
          PrimeSpectrum ↥A)
        (⊥ : PrimeSpectrum ↥A)),
    A = B ∨ B = ⊤
inr :
  ∀
    (h :
      Eq (α := PrimeSpectrum ↥A)
        ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
            (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle) :
          PrimeSpectrum ↥A)
        (⊤ : PrimeSpectrum ↥A)),
    A = B ∨ B = ⊤
⊢ A = B ∨ B = ⊤

Tactic:
obtain h | h := IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top (A.primeSpectrumEquiv.symm ⟨B, hle⟩)

Premises used: Subtype.mk, IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top, ValuationSubring.primeSpectrumEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h :
  Eq (α := PrimeSpectrum ↥A)
    ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
        (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle) :
      PrimeSpectrum ↥A)
    (⊥ : PrimeSpectrum ↥A)
⊢ Eq (α := { S : ValuationSubring K // A ≤ S })
    ((A.primeSpectrumEquiv : (a : PrimeSpectrum ↥A) → { S : ValuationSubring K // A ≤ S })
        ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
          (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle)) :
      { S : ValuationSubring K // A ≤ S })
    ((A.primeSpectrumEquiv : (a : PrimeSpectrum ↥A) → { S : ValuationSubring K // A ≤ S }) ⊥ :
      { S : ValuationSubring K // A ≤ S })

Tactic:
replace h := congr(primeSpectrumEquiv A $h)
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h :
  Eq (α := { S : ValuationSubring K // A ≤ S })
    ((A.primeSpectrumEquiv : (a : PrimeSpectrum ↥A) → { S : ValuationSubring K // A ≤ S })
        ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
          (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle)) :
      { S : ValuationSubring K // A ≤ S })
    ((A.primeSpectrumEquiv : (a : PrimeSpectrum ↥A) → { S : ValuationSubring K // A ≤ S }) ⊥ :
      { S : ValuationSubring K // A ≤ S })
⊢ A = B ∨ B = ⊤

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h :
  Eq (α := PrimeSpectrum ↥A)
    ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
        (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle) :
      PrimeSpectrum ↥A)
    (⊤ : PrimeSpectrum ↥A)
⊢ Eq (α := { S : ValuationSubring K // A ≤ S })
    ((A.primeSpectrumEquiv : (a : PrimeSpectrum ↥A) → { S : ValuationSubring K // A ≤ S })
        ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
          (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle)) :
      { S : ValuationSubring K // A ≤ S })
    ((A.primeSpectrumEquiv : (a : PrimeSpectrum ↥A) → { S : ValuationSubring K // A ≤ S }) ⊤ :
      { S : ValuationSubring K // A ≤ S })

Tactic:
replace h := congr(primeSpectrumEquiv A $h)
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h :
  Eq (α := { S : ValuationSubring K // A ≤ S })
    ((A.primeSpectrumEquiv : (a : PrimeSpectrum ↥A) → { S : ValuationSubring K // A ≤ S })
        ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
          (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle)) :
      { S : ValuationSubring K // A ≤ S })
    ((A.primeSpectrumEquiv : (a : PrimeSpectrum ↥A) → { S : ValuationSubring K // A ≤ S }) ⊤ :
      { S : ValuationSubring K // A ≤ S })
⊢ A = B ∨ B = ⊤

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
inl : ∀ (h : A = B), A = B
inr : ∀ (h : B = ⊤), A = B
⊢ A = B

Tactic:
obtain h | h := eq_self_or_eq_top_of_le hle

Premises used: ValuationSubring.eq_self_or_eq_top_of_le
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
h : A = B
⊢ A = B

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
h : B = ⊤
⊢ A = B

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
inl : ∀ (h : A = B), B = ⊤
inr : ∀ (h : B = ⊤), B = ⊤
⊢ B = ⊤

Tactic:
obtain h | h := eq_self_or_eq_top_of_le hle

Premises used: ValuationSubring.eq_self_or_eq_top_of_le
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
h : A = B
⊢ B = ⊤

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
h : B = ⊤
⊢ B = ⊤

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hlt : A < B
inl : ∀ (h : A = B), B = ⊤
inr : ∀ (h : B = ⊤), B = ⊤
⊢ B = ⊤

Tactic:
obtain h | h := eq_self_or_eq_top_of_le hlt.le

Premises used: LT.lt.le, ValuationSubring.eq_self_or_eq_top_of_le
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hlt : A < B
h : A = B
⊢ B = ⊤

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hlt : A < B
h : B = ⊤
⊢ B = ⊤

Tactic:
simp_all