awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Perfection
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 :
  HMul.hMul (α := 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
rw :
  ∀
    (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)
⊢ preVal K v O p
      (HMul.hMul (α := 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)}))) =
    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_mul (Ideal.Quotient.mk (Ideal.span {↑p})) r s] at hxy0 ⊢

Premises used: Ideal.Quotient.mk, map_mul, Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.Perfection
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)
rw₄ 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)
⊢ 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)

Tactic:
rw [preVal_mk hv hx0, preVal_mk hv hy0, preVal_mk hv hxy0, map_mul, v.map_mul]

Premises used: ModP.preVal_mk, Valuation.map_mul, map_mul
-- Module: Mathlib.RingTheory.Perfection
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)
inr : ∀ (hx0 : x ≠ 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)

Tactic:
obtain rfl | hx0 := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Perfection
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
⊢ preVal K v O p (0 + y) ≤ max (preVal K v O p 0) (preVal K v O p y)

Tactic:
simp
-- Module: Mathlib.RingTheory.Perfection
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)
inr₁ : ∀ (hy0 : 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)

Tactic:
obtain rfl | hy0 := eq_or_ne y 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Perfection
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
hx0 : x ≠ 0
⊢ preVal K v O p (x + 0) ≤ max (preVal K v O p x) (preVal K v O p 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Perfection
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)
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)
⊢ 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
-- Module: Mathlib.RingTheory.Perfection
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)

Tactic:
simp [hxy0]
-- Module: Mathlib.RingTheory.Perfection
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
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)
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)

Tactic:
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Perfection
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
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))
⊢ 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 ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Perfection
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
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))
⊢ 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:
rw [← map_add (Ideal.Quotient.mk (Ideal.span {↑p})) r s] at hxy0 ⊢

Premises used: Ideal.Quotient.mk, map_add, Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.Perfection
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)
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)
⊢ 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 [preVal_mk hv hx0, preVal_mk hv hy0, preVal_mk hv hxy0, map_add]

Premises used: map_add, ModP.preVal_mk
-- Module: Mathlib.RingTheory.Perfection
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)
⊢ 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:
v.map_add _ _

Premises used: Valuation.map_add
-- Module: Mathlib.RingTheory.Perfection
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)
⊢ 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:
exact v.map_add _ _

Premises used: Valuation.map_add
-- Module: Mathlib.RingTheory.Perfection
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

Tactic:
aesop
-- Module: Mathlib.RingTheory.Perfection
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
refine : ∀ (h : x ≠ 0) (hp : preVal K v O p x ≤ (v : (a : K) → ℝ≥0) (↑p : K)), x = 0
⊢ (v : (a : K) → ℝ≥0) (↑p : K) < preVal K v O p x ↔ x ≠ 0

Tactic:
refine ⟨by aesop, fun h => lt_of_not_ge fun hp => h ?_⟩
-- Module: Mathlib.RingTheory.Perfection
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)
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)
⊢ x = 0

Tactic:
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Perfection
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)
⊢ (↑p : O) ∣ r

Tactic:
rw [preVal_mk hv h, ← map_natCast (algebraMap O K) p, hv.le_iff_dvd] at hp

Premises used: Algebra.algebraMap, Valuation.Integers.le_iff_dvd, ModP.preVal_mk, map_natCast
-- Module: Mathlib.RingTheory.Perfection
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 : (↑p : O) ∣ r
rw : (↑p : O) ∣ r
⊢ 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:
rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]

Premises used: Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Perfection
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 : (↑p : O) ∣ r
⊢ (↑p : O) ∣ r

Tactic:
hp
-- Module: Mathlib.RingTheory.Perfection
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 : (↑p : O) ∣ r
⊢ (↑p : O) ∣ r

Tactic:
exact hp
-- Module: Mathlib.RingTheory.Perfection
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
contrapose! : ∀ (h : x ≠ 0), preVal K v O p x ≠ 0
⊢ x = 0

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.Perfection
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
⊢ preVal K v O p x ≠ 0

Tactic:
((v_p_lt_preVal hv).2 h).ne_zero

Premises used: Iff.mpr, ModP.v_p_lt_preVal, LT.lt.ne_zero
-- Module: Mathlib.RingTheory.Perfection
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
⊢ preVal K v O p x ≠ 0

Tactic:
exact ((v_p_lt_preVal hv).2 h).ne_zero

Premises used: Iff.mpr, ModP.v_p_lt_preVal, LT.lt.ne_zero
-- Module: Mathlib.RingTheory.Perfection
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
hx : x = 0
⊢ preVal K v O p x = 0

Tactic:
simp [hx]