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 : ℕ
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 : ℝ)
⊢ (v : (a : K) → ℝ≥0) (↑p : K) ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
have pos : ∀ (hvp : Eq (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (0 : ℝ≥0)),
  (v : (a : K) → ℝ≥0) (↑p : K) ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
Tactic: by_cases hvp : v p = 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 : ℕ
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 : ℝ)
pos :
  ∀ (hvp : Eq (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (0 : ℝ≥0)),
    (v : (a : K) → ℝ≥0) (↑p : K) ≤
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
        HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
⊢ (v : (a : K) → ℝ≥0) (↑p : K) ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
have neg : ∀ (hvp : ¬Eq (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (0 : ℝ≥0)),
  (v : (a : K) → ℝ≥0) (↑p : K) ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
Tactic: by_cases hvp : v p = 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 : ℕ
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 : Eq (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (0 : ℝ≥0)
⊢ (v : (a : K) → ℝ≥0) (↑p : K) ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
have pos : 0 ≤ HPow.hPow (α := ℝ≥0) 0 (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) * HPow.hPow (α := ℝ≥0) 0 (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
Tactic: rw [hvp]
-- 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 : ℕ
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 : ¬Eq (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (0 : ℝ≥0)
⊢ (v : (a : K) → ℝ≥0) (↑p : K) ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
have hvp₁ : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
Tactic: replace hvp := zero_lt_iff.2 hvp
Cleared hypotheses: hvp
-- 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 : ℕ
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)
| (v : (a : K) → ℝ≥0) (↑p : K)
have rw : HPow.hPow (α := ℝ≥0) (β := ℝ) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) 1
Tactic: rw [← rpow_one (v p)]
-- 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 : ℕ
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)
⊢ (v : (a : K) → ℝ≥0) (↑p : K) ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
have neg : 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 : ℝ)) *
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
Tactic: conv_lhs => rw [← rpow_one (v p)]
-- 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 : ℕ
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)
⊢ 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 : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
have neg : 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: rw [← rpow_add (ne_of_gt hvp)]
-- 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 : ℕ
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)
⊢ 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 : ℝ))
have neg : HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) ≤ 1
Tactic: refine rpow_le_rpow_of_exponent_ge hvp (map_natCast (algebraMap O K) p ▸ hv.2 _) ?_
-- 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 : ℕ
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)
⊢ HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) ≤ 1
have neg : HAdd.hAdd (α := ℝ) 1 1 ≤ (↑p : ℝ)
Tactic: rw [← add_div, div_le_one (Nat.cast_pos.2 hp.1.pos : 0 < (p : ℝ))]
-- 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 : ℕ
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)
⊢ valAux K v O p f = ModP.preVal K v O p ((coeff n : (a : PreTilt O p) → ModP O p) f) ^ p ^ n
have h : ∃ (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⟩
-- 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 : ℕ
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)
⊢ valAux K v O p f = ModP.preVal K v O p ((coeff n : (a : PreTilt O p) → ModP O p) f) ^ p ^ n
have 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
Tactic: rw [valAux, dif_pos 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 : ℕ
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)
⊢ 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
have 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)
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Nat.find_min' h hfn)
Cleared hypotheses: n, hfn
-- 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 : ℕ
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)
⊢ 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
have 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)
Tactic: classical
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Nat.find_min' h hfn)
  induction k with
  | zero => rfl
  | succ k ih => ?_
  obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (coeff (Nat.find h + k + 1) f)
  have h1 : (Ideal.Quotient.mk _ x : ModP O p) ≠ 0 := hx.symm ▸ hfn
  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
  rw [ih (coeff_nat_find_add_ne_zero k), ← add_assoc, ← hx, ← coeff_pow_p, ← hx, ← map_pow,
    ModP.preVal_mk hv h1, ModP.preVal_mk hv h2, map_pow, v.map_pow, ← pow_mul, pow_succ']
Cleared hypotheses: n, hfn
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
⊢ ModP.preVal K v O p ((coeff 0 : (a : PreTilt O p) → ModP O p) 1 : ModP O p) ^ HPow.hPow (β := ℕ) p 0 = 1
have 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
Tactic: rw [pow_zero, pow_one, map_one, ← (Ideal.Quotient.mk _).map_one, ModP.preVal_mk hv,
      map_one, v.map_one]
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑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)}) 1) 0
have change : Ne.{u₂ + 1} (α := ModP O p) 1 0
Tactic: change (1 : ModP O p) ≠ 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f g : PreTilt O p
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
have inl : valAux K v O p (0 * g) = valAux K v O p 0 * valAux K v O p g
Tactic: obtain rfl | hf := eq_or_ne f 0
Cleared hypotheses: f
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f g : PreTilt O p
inl : valAux K v O p (0 * g) = valAux K v O p 0 * valAux K v O p g
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
have inr : ∀ (hf : f ≠ 0), valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
Tactic: obtain rfl | hf := eq_or_ne f 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f g : PreTilt O p
hf : f ≠ 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
have inr : valAux K v O p (f * 0) = valAux K v O p f * valAux K v O p 0
Tactic: obtain rfl | hg := eq_or_ne g 0
Cleared hypotheses: g
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f g : PreTilt O p
hf : f ≠ 0
inr : valAux K v O p (f * 0) = valAux K v O p f * valAux K v O p 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
have inr₁ : ∀ (hg : g ≠ 0), valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
Tactic: obtain rfl | hg := eq_or_ne g 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
have inr : ∀ (m : ℕ) (hm : Ne (α := ModP O p) ((coeff m : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)),
  valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
Tactic: obtain ⟨m, hm⟩ : ∃ n, coeff n f ≠ 0 := not_forall.1 fun h => hf <| Perfection.ext 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m : ℕ
hm : Ne (α := ModP O p) ((coeff m : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
have inr : ∀ (n : ℕ) (hn : Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) g : ModP O p) (0 : ModP O p)),
  valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
Tactic: obtain ⟨n, hn⟩ : ∃ n, coeff n g ≠ 0 := not_forall.1 fun h => hg <| Perfection.ext h
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m : ℕ
hm : Ne (α := ModP O p) ((coeff m : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
n : ℕ
hn : Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) g : ModP O p) (0 : ModP O p)
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
have hm₁ : Ne (α := ModP O p) ((Perfection.coeff (ModP O p) p (max m n) : (a : Perfection (ModP O p) p) → ModP O p) f : ModP O p)
  (0 : ModP O p)
Tactic: replace hm := coeff_ne_zero_of_le hm (le_max_left m n)
Cleared hypotheses: hm
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hn : Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) g : ModP O p) (0 : ModP O p)
hm :
  Ne (α := ModP O p) ((Perfection.coeff (ModP O p) p (max m n) : (a : Perfection (ModP O p) p) → ModP O p) f : ModP O p)
    (0 : ModP O p)
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
have hn₁ : Ne (α := ModP O p) ((Perfection.coeff (ModP O p) p (max m n) : (a : Perfection (ModP O p) p) → ModP O p) g : ModP O p)
  (0 : ModP O p)
Tactic: replace hn := coeff_ne_zero_of_le hn (le_max_right m n)
Cleared hypotheses: hn
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hm :
  Ne (α := ModP O p) ((Perfection.coeff (ModP O p) p (max m n) : (a : Perfection (ModP O p) p) → ModP O p) f : ModP O p)
    (0 : ModP O p)
hn :
  Ne (α := ModP O p) ((Perfection.coeff (ModP O p) p (max m n) : (a : Perfection (ModP O p) p) → ModP O p) g : ModP O p)
    (0 : ModP O p)
⊢ Ne (α := ModP O p) ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) (f * g) : ModP O p) (0 : ModP O p)
have rw : HMul.hMul (α := ModP O p) (β := ModP O p) ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f : ModP O p)
    ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g : ModP O p) ≠
  0
Tactic: rw [map_mul]