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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
hvp : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
neg : HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) ≤ 1
⊢ HPow.hPow (α := ℝ≥0) (β := ℝ) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) 1 ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
      (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))

Tactic:
refine rpow_le_rpow_of_exponent_ge hvp (map_natCast (algebraMap O K) p ▸ hv.2 _) ?_

Premises used: Algebra.algebraMap, Valuation.Integers.map_le_one, NNReal.rpow_le_rpow_of_exponent_ge, Eq.rec, 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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
hvp : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
neg : HAdd.hAdd (α := ℝ) 1 1 ≤ (↑p : ℝ)
⊢ HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) ≤ 1

Tactic:
rw [← add_div, div_le_one (Nat.cast_pos.2 hp.1.pos : 0 < (p : ℝ))]

Premises used: Iff.mpr, Nat.cast_pos, Nat.Prime.pos, div_le_one, Fact.out, add_div
-- 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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
hvp : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
⊢ HAdd.hAdd (α := ℝ) 1 1 ≤ (↑p : ℝ)

Tactic:
mod_cast hp.1.two_le

Premises used: congrArg, Nat.cast_add._simp_1, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, HAdd.hAdd, congr, Nat.Prime.two_le, congrFun', OfNat.ofNat, Eq.symm, Nat.cast_one, Fact.out, Eq.trans
-- 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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
hvp : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
⊢ HAdd.hAdd (α := ℝ) 1 1 ≤ (↑p : ℝ)

Tactic:
exact mod_cast hp.1.two_le

Premises used: Nat.Prime.two_le, Fact.out
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
⊢ CharP.{u₂} (PreTilt O p) p

Tactic:
inferInstanceAs <| CharP (Perfection _ _) _

Premises used: _private.0.PreTilt.instCharP._proof_1
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
⊢ PerfectRing.{u₂} (PreTilt O p) p

Tactic:
inferInstanceAs <| PerfectRing (Perfection _ _) p

Premises used: _private.0.PreTilt.instPerfectRing._proof_1
-- Module: Mathlib.RingTheory.Perfection
Goal:
O : Type u₂
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
n : ℕ
x : PreTilt O p
⊢ Eq (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) x : ModP O p)
    ((Perfection.coeff (ModP O p) p n : (a : Perfection (ModP O p) p) → ModP O p) x : ModP O p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
O : Type u₂
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
n : ℕ
x : PreTilt O p
⊢ Eq (α := ModP O p)
    ((coeff (n + 1) : (a : PreTilt O p) → ModP O p) ((frobenius (PreTilt O p) p : (a : PreTilt O p) → PreTilt O p) x) :
      ModP O p)
    ((coeff n : (a : PreTilt O p) → ModP O p) x : ModP O p)

Tactic:
simp [PreTilt, coeff]

Premises used: PreTilt.coeff, PreTilt
-- Module: Mathlib.RingTheory.Perfection
Goal:
O : Type u₂
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
m n : ℕ
x : PreTilt O p
⊢ Eq (α := ModP O p)
    ((coeff (m + n) : (a : PreTilt O p) → ModP O p)
        ((⇑(frobenius (PreTilt O p) p) : (a : PreTilt O p) → PreTilt O p)^[n] x) :
      ModP O p)
    ((coeff m : (a : PreTilt O p) → ModP O p) x : ModP O p)

Tactic:
simp [PreTilt, coeff]

Premises used: PreTilt.coeff, PreTilt
-- Module: Mathlib.RingTheory.Perfection
Goal:
O : Type u₂
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
x : PreTilt O p
m n : ℕ
hmn : m ≤ n
⊢ Eq (α := ModP O p)
    ((coeff n : (a : PreTilt O p) → ModP O p) ((⇑(frobenius (PreTilt O p) p) : (a : PreTilt O p) → PreTilt O p)^[m] x) :
      ModP O p)
    ((coeff (n - m) : (a : PreTilt O p) → ModP O p) x : ModP O p)

Tactic:
Perfection.coeff_iterate_frobenius' _ _ _ hmn

Premises used: PreTilt, Perfection.coeff_iterate_frobenius'
-- Module: Mathlib.RingTheory.Perfection
Goal:
O : Type u₂
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
x : PreTilt O p
n : ℕ
⊢ HPow.hPow (α := ModP O p) ((coeff (n + 1) : (a : PreTilt O p) → ModP O p) x : ModP O p) p =
    (coeff n : (a : PreTilt O p) → ModP O p) x

Tactic:
Perfection.coeff_pow_p x n

Premises used: Perfection.coeff_pow_p
-- Module: Mathlib.RingTheory.Perfection
Goal:
O : Type u₂
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
n : ℕ
x : PreTilt O p
⊢ Eq (α := ModP O p)
    ((coeff n : (a : PreTilt O p) → ModP O p)
        ((RingEquiv.symm (frobeniusEquiv (PreTilt O p) p) : (a : PreTilt O p) → PreTilt O p) x) :
      ModP O p)
    ((coeff (n + 1) : (a : PreTilt O p) → ModP O p) x : ModP O p)

Tactic:
simp [PreTilt, coeff]

Premises used: PreTilt.coeff, PreTilt
-- Module: Mathlib.RingTheory.Perfection
Goal:
O : Type u₂
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
m n : ℕ
x : PreTilt O p
⊢ Eq (α := ModP O p)
    ((coeff m : (a : PreTilt O p) → ModP O p)
        ((⇑(RingEquiv.symm (frobeniusEquiv (PreTilt O p) p)) : (a : PreTilt O p) → PreTilt O p)^[n] x) :
      ModP O p)
    ((coeff (m + n) : (a : PreTilt O p) → ModP O p) x : ModP O p)

Tactic:
simp [PreTilt, coeff]

Premises used: PreTilt.coeff, PreTilt
-- Module: Mathlib.RingTheory.Perfection
Goal:
O : Type u₂
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f : PreTilt O p
h : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
k : ℕ
⊢ Ne (α := ModP O p)
    ((coeff
            (Nat.find (p := fun (n : ℕ) ↦
                Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
              k) :
          (a : PreTilt O p) → ModP O p)
        f :
      ModP O p)
    (0 : ModP O p)

Tactic:
coeff_add_ne_zero (Nat.find_spec h) k

Premises used: Perfection.coeff_add_ne_zero, Nat.find_spec
-- 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
p : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
⊢ valAux K v O p 0 = 0

Tactic:
dif_neg fun ⟨_, hn⟩ => hn rfl

Premises used: dif_neg, PreTilt.valAux
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f : PreTilt O p
n : ℕ
hfn : Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
⊢ ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)

Tactic:
have h : ∃ n, coeff n f ≠ 0 := ⟨n, hfn⟩
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f : PreTilt O p
n : ℕ
hfn : Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
h : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
rw :
  ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        Nat.find (p := fun (n : ℕ) ↦
          Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h =
    ModP.preVal K v O p ((coeff n : (a : PreTilt O p) → ModP O p) f) ^ p ^ n
⊢ valAux K v O p f = ModP.preVal K v O p ((coeff n : (a : PreTilt O p) → ModP O p) f) ^ p ^ n

Tactic:
rw [valAux, dif_pos h]

Premises used: dif_pos, PreTilt.valAux
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f : PreTilt O p
n : ℕ
hfn : Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
h : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
obtain :
  ∀ (k : ℕ)
    (hfn :
      Ne (α := ModP O p)
        ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                    Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                  k) :
              (a : PreTilt O p) → ModP O p)
            f :
          ModP O p)
        (0 : ModP O p)),
    ModP.preVal K v O p
          ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h) :
              (a : PreTilt O p) → ModP O p)
            f) ^
        p ^
          Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h =
      ModP.preVal K v O p
          ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                    Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                  k) :
              (a : PreTilt O p) → ModP O p)
            f) ^
        p ^
          (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k)
⊢ ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        Nat.find (p := fun (n : ℕ) ↦
          Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h =
    ModP.preVal K v O p ((coeff n : (a : PreTilt O p) → ModP O p) f) ^ p ^ n

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Nat.find_min' h hfn)

Premises used: Nat.exists_eq_add_of_le, Nat.find_min', 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f : PreTilt O p
h : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
hfn :
  Ne (α := ModP O p)
    ((coeff
            (Nat.find (p := fun (n : ℕ) ↦
                Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
              0) :
          (a : PreTilt O p) → ModP O p)
        f :
      ModP O p)
    (0 : ModP O p)
⊢ ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        Nat.find (p := fun (n : ℕ) ↦
          Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h =
    ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                0) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          0)

Tactic:
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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f : PreTilt O p
h : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
k : ℕ
ih :
  ∀
    (hfn :
      Ne (α := ModP O p)
        ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                    Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                  k) :
              (a : PreTilt O p) → ModP O p)
            f :
          ModP O p)
        (0 : ModP O p)),
    ModP.preVal K v O p
          ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h) :
              (a : PreTilt O p) → ModP O p)
            f) ^
        p ^
          Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h =
      ModP.preVal K v O p
          ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                    Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                  k) :
              (a : PreTilt O p) → ModP O p)
            f) ^
        p ^
          (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k)
hfn :
  Ne (α := ModP O p)
    ((coeff
            (Nat.find (p := fun (n : ℕ) ↦
                Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
              (k + 1)) :
          (a : PreTilt O p) → ModP O p)
        f :
      ModP O p)
    (0 : ModP O p)
⊢ ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        Nat.find (p := fun (n : ℕ) ↦
          Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h =
    ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                (k + 1)) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          (k + 1))

Tactic:
?_
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f : PreTilt O p
h : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
k : ℕ
ih :
  ∀
    (hfn :
      Ne (α := ModP O p)
        ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                    Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                  k) :
              (a : PreTilt O p) → ModP O p)
            f :
          ModP O p)
        (0 : ModP O p)),
    ModP.preVal K v O p
          ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h) :
              (a : PreTilt O p) → ModP O p)
            f) ^
        p ^
          Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h =
      ModP.preVal K v O p
          ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                    Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                  k) :
              (a : PreTilt O p) → ModP O p)
            f) ^
        p ^
          (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k)
hfn :
  Ne (α := ModP O p)
    ((coeff
            (Nat.find (p := fun (n : ℕ) ↦
                Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
              (k + 1)) :
          (a : PreTilt O p) → ModP O p)
        f :
      ModP O p)
    (0 : ModP O p)
x : O
hx :
  Eq (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((coeff
            (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                k +
              1) :
          (a : PreTilt O p) → ModP O p)
        f :
      ModP O p)
⊢ Ne (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))

Tactic:
have h1 : (Ideal.Quotient.mk _ x : ModP O p) ≠ 0 := hx.symm ▸ hfn
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f : PreTilt O p
h : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
k : ℕ
ih :
  ∀
    (hfn :
      Ne (α := ModP O p)
        ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                    Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                  k) :
              (a : PreTilt O p) → ModP O p)
            f :
          ModP O p)
        (0 : ModP O p)),
    ModP.preVal K v O p
          ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h) :
              (a : PreTilt O p) → ModP O p)
            f) ^
        p ^
          Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h =
      ModP.preVal K v O p
          ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                    Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                  k) :
              (a : PreTilt O p) → ModP O p)
            f) ^
        p ^
          (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k)
hfn :
  Ne (α := ModP O p)
    ((coeff
            (Nat.find (p := fun (n : ℕ) ↦
                Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
              (k + 1)) :
          (a : PreTilt O p) → ModP O p)
        f :
      ModP O p)
    (0 : ModP O p)
x : O
hx :
  Eq (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((coeff
            (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                k +
              1) :
          (a : PreTilt O p) → ModP O p)
        f :
      ModP O p)
h1 :
  Ne (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
⊢ Ne (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (x ^ p) :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))

Tactic:
have h2 : (Ideal.Quotient.mk _ (x ^ p) : ModP O p) ≠ 0 := by
    rw [map_pow, hx, coeff_pow_p]
    exact coeff_nat_find_add_ne_zero k
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
rw :
  Ne (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) 1) 0
⊢ ModP.preVal K v O p ((coeff 0 : (a : PreTilt O p) → ModP O p) 1 : ModP O p) ^ HPow.hPow (β := ℕ) p 0 = 1

Tactic:
rw [pow_zero, pow_one, map_one, ← (Ideal.Quotient.mk _).map_one, ModP.preVal_mk hv,
      map_one, v.map_one]

Premises used: Ideal.Quotient.mk, RingHom.map_one, ModP.preVal_mk, pow_zero, Valuation.map_one, map_one, pow_one
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
change : Ne.{u₂ + 1} (α := ModP O p) 1 0
⊢ Ne (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) 1) 0

Tactic:
change (1 : ModP O p) ≠ 0

Premises used: OfNat.ofNat