awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
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
⊢ False
have h₁ : Eq.{u + 1} (α := A.ValueGroup) 0 1
Tactic: rw [c, A.valuation.map_zero] at h
Cleared hypotheses: h, c
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
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)
⊢ IsUnit a
have ha : (↑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
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
have rw : LE.le (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K)⁻¹ : A.ValueGroup) (1 : A.ValueGroup)
Tactic: rw [← valuation_le_one_iff, map_inv₀, h, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ (↑a : K)⁻¹ ∈ A
have rw₁ : LE.le (α := A.ValueGroup) (((A.valuation : (a : K) → A.ValueGroup) (↑a : K))⁻¹ : A.ValueGroup) (1 : A.ValueGroup)
Tactic: rw [← valuation_le_one_iff, map_inv₀, h, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ (↑a : K)⁻¹ ∈ A
have rw₂ : LE.le.{u} (α := A.ValueGroup) 1⁻¹ 1
Tactic: rw [← valuation_le_one_iff, map_inv₀, h, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
⊢ (↑a : K)⁻¹ ∈ A
have rw₃ : LE.le.{u} (α := A.ValueGroup) 1 1
Tactic: rw [← valuation_le_one_iff, map_inv₀, h, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
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
⊢ IsUnit a
have ha' : (↑a : K)⁻¹ ∈ A
Tactic: have ha' : (a : K)⁻¹ ∈ A := by rw [← valuation_le_one_iff, map_inv₀, h, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
have refine : a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑a : K)⁻¹ ha' = 1
Tactic: refine .of_mul_eq_one ⟨a⁻¹, ha'⟩ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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' = 1
have a₁ : (↑(a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑a : K)⁻¹ ha') : K) = (↑1 : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A
⊢ ¬IsUnit a ↔
    LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑a : K) : A.ValueGroup) (1 : A.ValueGroup)
have 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)
Tactic: rw [valuation_eq_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ A.idealOfLE ⊤ ⋯ = ⊥
have hf : Function.Injective (α := ↥A) (β := ↥⊤) (⇑(A.inclusion ⊤ sorry) : (a : ↥A) → ↥⊤)
Tactic: rw [ValuationSubring.idealOfLE, IsLocalRing.maximalIdeal_eq_bot, Ideal.comap_bot_of_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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) ↔
    x ∈ P.primeCompl
have 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
Tactic: rw [← IsLocalization.AtPrime.isUnit_to_map_iff (A.ofPrime P) P x, valuation_eq_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : Ideal ↥A
inst_1 : P.IsPrime
⊢ A.idealOfLE (A.ofPrime P) ⋯ = P
have refine : ∀ (x : ↥A), x ∈ A.idealOfLE (A.ofPrime P) sorry ↔ x ∈ P
Tactic: refine Ideal.ext (fun x => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : Ideal ↥A
inst_1 : P.IsPrime
x : ↥A
⊢ x ∈ A.idealOfLE (A.ofPrime P) ⋯ ↔ x ∈ P
have h : optParam (IsLocalRing.{u} ↥(A.ofPrime P)) sorry
Tactic: apply IsLocalization.AtPrime.to_map_mem_maximal_iff
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
⊢ R.ofPrime (R.idealOfLE S h) = S
have h₁ : ∀ (x : K), x ∈ R.ofPrime (R.idealOfLE S h) ↔ x ∈ S
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ x ∈ R.ofPrime (R.idealOfLE S h) ↔ x ∈ S
have h₁ : x ∈ R.ofPrime (R.idealOfLE S h) → x ∈ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
⊢ x ∈ R.ofPrime (R.idealOfLE S h) ↔ x ∈ S
have h₂ : x ∈ S → x ∈ R.ofPrime (R.idealOfLE S h)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ HMul.hMul (α := K) (β := K) ((algebraMap (↥R) K : (a : ↥R) → K) a : K)
      (((algebraMap (↥R) K : (a : ↥R) → K) r)⁻¹ : K) ∈
    S
have h₁ : Membership.mem (α := K) S ((algebraMap (↥R) K : (a : ↥R) → K) a : K)
Tactic: apply mul_mem
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ HMul.hMul (α := K) (β := K) ((algebraMap (↥R) K : (a : ↥R) → K) a : K)
      (((algebraMap (↥R) K : (a : ↥R) → K) r)⁻¹ : K) ∈
    S
have h₂ : Membership.mem (α := K) S (((algebraMap (↥R) K : (a : ↥R) → K) r)⁻¹ : K)
Tactic: apply mul_mem
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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) r)⁻¹ : K)
have h₁ : LE.le (α := S.ValueGroup) (1 : S.ValueGroup)
  ((S.valuation : (a : K) → S.ValueGroup) ((algebraMap (↥R) K : (a : ↥R) → K) r) : S.ValueGroup)
Tactic: rw [← valuation_le_one_iff, map_inv₀, ← inv_one, inv_le_inv₀]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ Membership.mem (α := K) S (((algebraMap (↥R) K : (a : ↥R) → K) r)⁻¹ : K)
have h₂ : LT.lt (α := S.ValueGroup) (0 : S.ValueGroup)
  ((S.valuation : (a : K) → S.ValueGroup) ((algebraMap (↥R) K : (a : ↥R) → K) r) : S.ValueGroup)
Tactic: rw [← valuation_le_one_iff, map_inv₀, ← inv_one, inv_le_inv₀]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ Membership.mem (α := K) S (((algebraMap (↥R) K : (a : ↥R) → K) r)⁻¹ : K)
have h₃ : LT.lt.{u} (α := S.ValueGroup) 0 1
Tactic: rw [← valuation_le_one_iff, map_inv₀, ← inv_one, inv_le_inv₀]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
⊢ x ∈ R.ofPrime (R.idealOfLE S h)
have pos : ∀ (hr : x ∈ R), x ∈ R.ofPrime (R.idealOfLE S h)
Tactic: by_cases hr : x ∈ R
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ x ∈ R.ofPrime (R.idealOfLE S h)
have neg : ∀ (hr : x ∉ R), x ∈ R.ofPrime (R.idealOfLE S h)
Tactic: by_cases hr : x ∈ R
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
⊢ x ∈ R
have rw : 0 ∈ R
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
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)
have this : x ≠ 0
Tactic: have : x ≠ 0 := fun h => hr (by rw [h]; exact R.zero_mem)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
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.ofPrime (R.idealOfLE S h)
have hr₁ : x⁻¹ ∈ R
Tactic: replace hr := (R.mem_or_inv_mem x).resolve_left hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
have neg : Subtype.mk (p := fun (x : K) ↦ x ∈ R) x⁻¹ hr ∈ (R.idealOfLE S h).primeCompl
Tactic: refine ⟨1, ⟨x⁻¹, hr⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
⊢ x ∈ R.ofPrime (R.idealOfLE S h)
have 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)
Tactic: refine ⟨1, ⟨x⁻¹, hr⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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 ∈ R) x⁻¹ hr ∈ (R.idealOfLE S h).primeCompl
have neg : IsUnit (M := ↥S) ((R.inclusion S h : (a : ↥R) → ↥S) (Subtype.mk (p := fun (x : K) ↦ x ∈ R) x⁻¹ hr) : ↥S)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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 (M := ↥S) ((R.inclusion S h : (a : ↥R) → ↥S) (Subtype.mk (p := fun (x : K) ↦ x ∈ R) x⁻¹ hr) : ↥S)
have neg : IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ S) x⁻¹ sorry)
Tactic: change IsUnit (⟨x⁻¹, h hr⟩ : S)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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⁻¹ ⋯)
have neg : Subtype.mk (p := fun (x : K) ↦ x ∈ S) x⁻¹ sorry * Subtype.mk (p := fun (x : K) ↦ x ∈ S) x hx = 1
Tactic: refine .of_mul_eq_one (⟨x, hx⟩ : S) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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 = 1
have neg : (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ S) x⁻¹ sorry * Subtype.mk (p := fun (x : K) ↦ x ∈ S) x hx) : K) = (↑1 : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
⊢ LT.lt (α := R.ValueGroup) ((R.valuation : (a : K) → R.ValueGroup) (↑((A.inclusion R hR : (a : ↥A) → ↥R) x) : K)) 1
have by_contra! : ∀
  (c :
    LE.le (α := R.ValueGroup) 1 ((R.valuation : (a : K) → R.ValueGroup) (↑((A.inclusion R hR : (a : ↥A) → ↥R) x) : K))),
  False
Tactic: by_contra! c
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
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))
⊢ False
have 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)))
Tactic: replace c := monotone_mapOfLE R S h c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
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)))
⊢ False
have c₁ : 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
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
P : PrimeSpectrum ↥A
⊢ (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
have asIdeal : PrimeSpectrum.asIdeal
    ((fun (S : { S : ValuationSubring K // A ≤ S }) ↦
        { asIdeal := A.idealOfLE (↑S : ValuationSubring K) sorry, isPrime := sorry : PrimeSpectrum ↥A })
      ((fun (P : PrimeSpectrum ↥A) ↦ Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime P.asIdeal) sorry)
        P)) =
  P.asIdeal
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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) =
    S
have a : (↑((fun (P : PrimeSpectrum ↥A) ↦ Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime P.asIdeal) sorry)
        ((fun (S : { S : ValuationSubring K // A ≤ S }) ↦
            { asIdeal := A.idealOfLE (↑S : ValuationSubring K) sorry, isPrime := sorry : PrimeSpectrum ↥A })
          S)) :
    ValuationSubring K) =
  (↑S : ValuationSubring K)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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 })
⊢ LE.le (α := (PrimeSpectrum ↥A)ᵒᵈ)
    ((OrderDual.toDual : (a : PrimeSpectrum ↥A) → (PrimeSpectrum ↥A)ᵒᵈ) a : (PrimeSpectrum ↥A)ᵒᵈ)
    ((OrderDual.toDual : (a : PrimeSpectrum ↥A) → (PrimeSpectrum ↥A)ᵒᵈ) b : (PrimeSpectrum ↥A)ᵒᵈ)
have simp : b ≤ a
Tactic: simp only [OrderDual.toDual_le_toDual]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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) ⋯
⊢ b ≤ a
have refine_3 : ∀
  (this :
    A.idealOfLE (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) sorry) : ValuationSubring K)
        sorry ≤
      A.idealOfLE
        (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) sorry) : ValuationSubring K) sorry),
  b ≤ a
Tactic: have := idealOfLE_le_of_le A _ _ ?_ ?_ h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
⊢ b ≤ a
have refine_1 : A ≤ (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) sorry) : ValuationSubring K)
Tactic: have := idealOfLE_le_of_le A _ _ ?_ ?_ h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
⊢ b ≤ a
have refine_2 : A ≤ (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime b.asIdeal) sorry) : ValuationSubring K)
Tactic: have := idealOfLE_le_of_le A _ _ ?_ ?_ h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)
      ⋯
⊢ b ≤ a
have refine_3 : ∀
  (this :
    b.asIdeal ≤
      A.idealOfLE
        (↑(Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) (A.ofPrime a.asIdeal) sorry) : ValuationSubring K) sorry),
  b ≤ a
Tactic: rwa [idealOfLE_ofPrime, idealOfLE_ofPrime] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
⊢ b ≤ a
have refine_3₁ : ∀ (this : b.asIdeal ≤ a.asIdeal), b ≤ a
Tactic: rwa [idealOfLE_ofPrime, idealOfLE_ofPrime] at this
Cleared hypotheses: this