awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
s : O
hy0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
hxy0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s) :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r) *
      preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s)
have rw : preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
  HMul.hMul (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
    (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s))
Tactic: rw [preVal_mk hv hx0, preVal_mk hv hy0, preVal_mk hv hxy0, map_mul, v.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
s : O
hy0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
hxy0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s) :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
rw :
  preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    HMul.hMul (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s))
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r) *
      preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s)
have rw₁ : preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
  HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
    ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)
Tactic: rw [preVal_mk hv hx0, preVal_mk hv hy0, preVal_mk hv hxy0, map_mul, v.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
s : O
hy0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
hxy0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s) :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
rw :
  preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    HMul.hMul (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s))
rw₁ :
  preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r) *
      preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s)
have rw₂ : (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (r * s)) =
  HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
    ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)
Tactic: rw [preVal_mk hv hx0, preVal_mk hv hy0, preVal_mk hv hxy0, map_mul, v.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
s : O
hy0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
hxy0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s) :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
rw :
  preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    HMul.hMul (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s))
rw₁ :
  preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)
rw₂ :
  (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (r * s)) =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r) *
      preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s)
have rw₃ : (v : (a : K) → ℝ≥0)
    (HMul.hMul (α := K) (β := K) ((algebraMap O K : (a : O) → K) r : K) ((algebraMap O K : (a : O) → K) s : K)) =
  HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
    ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)
Tactic: rw [preVal_mk hv hx0, preVal_mk hv hy0, preVal_mk hv hxy0, map_mul, v.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
s : O
hy0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
hxy0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s) :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
rw :
  preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    HMul.hMul (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s))
rw₁ :
  preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)
rw₂ :
  (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (r * s)) =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)
rw₃ :
  (v : (a : K) → ℝ≥0)
      (HMul.hMul (α := K) (β := K) ((algebraMap O K : (a : O) → K) r : K) ((algebraMap O K : (a : O) → K) s : K)) =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r) *
      preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s)
have rw₄ : HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
    ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0) =
  HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
    ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)
Tactic: rw [preVal_mk hv hx0, preVal_mk hv hy0, preVal_mk hv hxy0, map_mul, v.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
have inl : preVal K v O p (0 + y) ≤ max (preVal K v O p 0) (preVal K v O p y)
Tactic: obtain rfl | hx0 := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
inl : preVal K v O p (0 + y) ≤ max (preVal K v O p 0) (preVal K v O p y)
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
have inr : ∀ (hx0 : x ≠ 0), preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
Tactic: obtain rfl | hx0 := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x ≠ 0
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
have inr : preVal K v O p (x + 0) ≤ max (preVal K v O p x) (preVal K v O p 0)
Tactic: obtain rfl | hy0 := eq_or_ne y 0
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x ≠ 0
inr : preVal K v O p (x + 0) ≤ max (preVal K v O p x) (preVal K v O p 0)
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
have inr₁ : ∀ (hy0 : y ≠ 0), preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
Tactic: obtain rfl | hy0 := eq_or_ne y 0
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x ≠ 0
hy0 : y ≠ 0
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
have pos : ∀ (hxy0 : x + y = 0), preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
Tactic: by_cases hxy0 : x + y = 0
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x ≠ 0
hy0 : y ≠ 0
pos : ∀ (hxy0 : x + y = 0), preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
have neg : ∀ (hxy0 : ¬x + y = 0), preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
Tactic: by_cases hxy0 : x + y = 0
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x ≠ 0
hy0 : y ≠ 0
hxy0 : ¬x + y = 0
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
have neg : ∀ (r : O)
  (hx0 :
    Ne (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      (0 : ModP O p))
  (hxy0 :
    ¬HAdd.hAdd (α := ModP O p)
          ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
            HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
          y =
        0),
  preVal K v O p
      (HAdd.hAdd (α := ModP O p)
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
        y) ≤
    max (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r))
      (preVal K v O p y)
Tactic: obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x, hx0, hxy0
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
y : ModP O p
hy0 : y ≠ 0
r : O
hx0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
hxy0 :
  ¬HAdd.hAdd (α := ModP O p)
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
        y =
      0
⊢ preVal K v O p
      (HAdd.hAdd (α := ModP O p)
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
        y) ≤
    max (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r))
      (preVal K v O p y)
have neg : ∀ (s : O)
  (hy0 :
    Ne (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      (0 : ModP O p))
  (hxy0 :
    ¬HAdd.hAdd (α := ModP O p) (β := ModP O p)
          ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
            HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
          ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
            HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)})) =
        0),
  preVal K v O p
      (HAdd.hAdd (α := ModP O p) (β := ModP O p)
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))) ≤
    max (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r))
      (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s))
Tactic: obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
Cleared hypotheses: y, hy0, hxy0
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
s : O
hy0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
hxy0 :
  ¬HAdd.hAdd (α := ModP O p) (β := ModP O p)
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)})) =
      0
⊢ preVal K v O p
      (HAdd.hAdd (α := ModP O p) (β := ModP O p)
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))) ≤
    max (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r))
      (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s))
have neg : ∀
  (hxy0 :
    ¬Eq (α := ModP O p)
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r + s) :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
        (0 : ModP O p)),
  preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r + s)) ≤
    max (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r))
      (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s))
Tactic: rw [← map_add (Ideal.Quotient.mk (Ideal.span {↑p})) r s] at hxy0 ⊢
Cleared hypotheses: hxy0
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
s : O
hy0 :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
hxy0 :
  ¬Eq (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r + s) :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      (0 : ModP O p)
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r + s)) ≤
    max (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r))
      (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s))
have neg : LE.le (α := ℝ≥0)
  ((v : (a : K) → ℝ≥0)
      (HAdd.hAdd (α := K) (β := K) ((algebraMap O K : (a : O) → K) r : K) ((algebraMap O K : (a : O) → K) s : K)) :
    ℝ≥0)
  (max ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r))
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)) :
    ℝ≥0)
Tactic: rw [preVal_mk hv hx0, preVal_mk hv hy0, preVal_mk hv hxy0, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
x : ModP O p
⊢ (v : (a : K) → ℝ≥0) (↑p : K) < preVal K v O p x ↔ x ≠ 0
have refine : ∀ (h : x ≠ 0) (hp : preVal K v O p x ≤ (v : (a : K) → ℝ≥0) (↑p : K)), x = 0
Tactic: refine ⟨by aesop, fun h => lt_of_not_ge fun hp => h ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
x : ModP O p
h : x ≠ 0
hp : preVal K v O p x ≤ (v : (a : K) → ℝ≥0) (↑p : K)
⊢ x = 0
have obtain : ∀ (r : O)
  (h :
    Ne (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      (0 : ModP O p))
  (hp :
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r) ≤
      (v : (a : K) → ℝ≥0) (↑p : K)),
  Eq (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
Tactic: obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x, h, hp
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (hypothesis)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
r : O
h :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
hp :
  preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r) ≤
    (v : (a : K) → ℝ≥0) (↑p : K)
⊢ Eq (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
have hp₁ : (↑p : O) ∣ r
Tactic: rw [preVal_mk hv h, ← map_natCast (algebraMap O K) p, hv.le_iff_dvd] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
x : ModP O p
h : preVal K v O p x = 0
⊢ x = 0
have contrapose! : ∀ (h : x ≠ 0), preVal K v O p x ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h