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 : ℕ
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)
⊢ 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
have refine_1 : HPow.hPow (α := ModP O p) ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f : ModP O p) p ≠ 0
Tactic: refine ModP.mul_ne_zero_of_pow_p_ne_zero (hv := hv) ?_ ?_
-- 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)
refine_1 : HPow.hPow (α := ModP O p) ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f : ModP O p) p ≠ 0
⊢ 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
have refine_2 : HPow.hPow (α := ModP O p) ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g : ModP O p) p ≠ 0
Tactic: refine ModP.mul_ne_zero_of_pow_p_ne_zero (hv := hv) ?_ ?_
-- 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)
⊢ HPow.hPow (α := ModP O p) ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f : ModP O p) p ≠ 0
have refine_1 : Ne (α := ModP O p) ((coeff (max m n) : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
Tactic: rw [coeff_pow_p 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
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)
⊢ HPow.hPow (α := ModP O p) ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g : ModP O p) p ≠ 0
have refine_2 : Ne (α := ModP O p) ((coeff (max m n) : (a : PreTilt O p) → ModP O p) g : ModP O p) (0 : ModP O p)
Tactic: rw [coeff_pow_p g]
-- 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 : ℕ
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)
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
have hfg : 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)
Tactic: have hfg : coeff (max m n + 1) (f * g) ≠ 0 := by
    rw [map_mul]
    refine ModP.mul_ne_zero_of_pow_p_ne_zero (hv := hv) ?_ ?_
    · rw [coeff_pow_p f]; assumption
    · rw [coeff_pow_p g]; assumption
-- 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)
hfg : 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)
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
have inr : ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) (f * g)) ^ p ^ (max m n + 1) =
  ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f) ^ p ^ (max m n + 1) *
    ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g) ^ p ^ (max m n + 1)
Tactic: rw [valAux_eq hv (coeff_add_ne_zero hm 1),
      valAux_eq hv (coeff_add_ne_zero hn 1), valAux_eq hv hfg]
-- 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)
hfg : 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)
⊢ ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) (f * g)) ^ p ^ (max m n + 1) =
    ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f) ^ p ^ (max m n + 1) *
      ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g) ^ p ^ (max m n + 1)
have inr : ∀
  (hfg :
    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),
  ModP.preVal K v O p
        (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)) ^
      p ^ (max m n + 1) =
    ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f) ^ p ^ (max m n + 1) *
      ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g) ^ p ^ (max m n + 1)
Tactic: rw [map_mul] at hfg ⊢
Cleared hypotheses: hfg
-- 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)
hfg :
  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
⊢ ModP.preVal K v O p
        (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)) ^
      p ^ (max m n + 1) =
    ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f) ^ p ^ (max m n + 1) *
      ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g) ^ p ^ (max m n + 1)
have inr : (ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f) *
      ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g)) ^
    p ^ (max m n + 1) =
  ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f) ^ p ^ (max m n + 1) *
    ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g) ^ p ^ (max m n + 1)
Tactic: rw [ModP.preVal_mul hv hfg, mul_pow]
-- 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)
hfg :
  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
inr :
  (ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f) *
        ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g)) ^
      p ^ (max m n + 1) =
    ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f) ^ p ^ (max m n + 1) *
      ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g) ^ p ^ (max m n + 1)
⊢ ModP.preVal K v O p
        (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)) ^
      p ^ (max m n + 1) =
    ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f) ^ p ^ (max m n + 1) *
      ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g) ^ p ^ (max m n + 1)
have inr₁ : ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f) ^ p ^ (max m n + 1) *
    ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g) ^ p ^ (max m n + 1) =
  ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) f) ^ p ^ (max m n + 1) *
    ModP.preVal K v O p ((coeff (max m n + 1) : (a : PreTilt O p) → ModP O p) g) ^ p ^ (max m n + 1)
Tactic: rw [ModP.preVal_mul hv hfg, mul_pow]
-- 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) ≤ max (valAux K v O p f) (valAux K v O p g)
have inl : valAux K v O p (0 + g) ≤ max (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) ≤ max (valAux K v O p 0) (valAux K v O p g)
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
have inr : ∀ (hf : f ≠ 0), valAux K v O p (f + g) ≤ max (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) ≤ max (valAux K v O p f) (valAux K v O p g)
have inr : valAux K v O p (f + 0) ≤ max (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) ≤ max (valAux K v O p f) (valAux K v O p 0)
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
have inr₁ : ∀ (hg : g ≠ 0), valAux K v O p (f + g) ≤ max (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) ≤ max (valAux K v O p f) (valAux K v O p g)
have pos : ∀ (hfg : f + g = 0), valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
Tactic: by_cases hfg : f + 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
pos : ∀ (hfg : f + g = 0), valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
have neg : ∀ (hfg : ¬f + g = 0), valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
Tactic: by_cases hfg : f + g = 0
-- 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
hfg : ¬f + g = 0
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
have hf₁ : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
Tactic: replace hf : ∃ n, coeff n f ≠ 0 := not_forall.1 fun h => hf <| Perfection.ext h
Cleared hypotheses: hf
-- 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
hg : g ≠ 0
hfg : ¬f + g = 0
hf : ∃ (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 + g) ≤ max (valAux K v O p f) (valAux K v O p g)
have hg₁ : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) g : ModP O p) (0 : ModP O p)
Tactic: replace hg : ∃ n, coeff n g ≠ 0 := not_forall.1 fun h => hg <| Perfection.ext h
Cleared hypotheses: hg
-- 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
hfg : ¬f + g = 0
hf : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
hg : ∃ (n : ℕ), 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) ≤ max (valAux K v O p f) (valAux K v O p g)
have hfg₁ : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) (f + g) : ModP O p) (0 : ModP O p)
Tactic: replace hfg : ∃ n, coeff n (f + g) ≠ 0 := not_forall.1 fun h => hfg <| Perfection.ext h
Cleared hypotheses: hfg
-- 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 : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
hg : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) g : ModP O p) (0 : ModP O p)
hfg : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) (f + g) : ModP O p) (0 : ModP O p)
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
have neg : ∀ (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) ≤ max (valAux K v O p f) (valAux K v O p g)
Tactic: obtain ⟨m, hm⟩ := hf
Cleared hypotheses: hf
-- 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
hg : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) g : ModP O p) (0 : ModP O p)
hfg : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) (f + g) : ModP O p) (0 : ModP O p)
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) ≤ max (valAux K v O p f) (valAux K v O p g)
have neg : ∀ (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) ≤ max (valAux K v O p f) (valAux K v O p g)
Tactic: obtain ⟨n, hn⟩ := hg
Cleared hypotheses: hg
-- 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
hfg : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) (f + g) : ModP O p) (0 : ModP O p)
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) ≤ max (valAux K v O p f) (valAux K v O p g)
have neg : ∀ (k : ℕ) (hk : Ne (α := ModP O p) ((coeff k : (a : PreTilt O p) → ModP O p) (f + g) : ModP O p) (0 : ModP O p)),
  valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
Tactic: obtain ⟨k, hk⟩ := hfg
Cleared hypotheses: hfg
-- 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
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)
k : ℕ
hk : Ne (α := ModP O p) ((coeff k : (a : PreTilt O p) → ModP O p) (f + g) : ModP O p) (0 : ModP O p)
⊢ valAux K v O p (f + g) ≤ max (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 (max m n) k) : (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_trans (le_max_left m n) (le_max_left _ k))
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
m n : ℕ
hn : Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) g : ModP O p) (0 : ModP O p)
k : ℕ
hk : Ne (α := ModP O p) ((coeff k : (a : PreTilt O p) → ModP O p) (f + g) : ModP O p) (0 : ModP O p)
hm :
  Ne (α := ModP O p)
    ((Perfection.coeff (ModP O p) p (max (max m n) k) : (a : Perfection (ModP O p) p) → ModP O p) f : ModP O p)
    (0 : ModP O p)
⊢ valAux K v O p (f + g) ≤ max (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 (max m n) k) : (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_trans (le_max_right m n) (le_max_left _ k))
Cleared hypotheses: hn
-- 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
m n k : ℕ
hk : Ne (α := ModP O p) ((coeff k : (a : PreTilt O p) → ModP O p) (f + g) : ModP O p) (0 : ModP O p)
hm :
  Ne (α := ModP O p)
    ((Perfection.coeff (ModP O p) p (max (max m n) k) : (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 (max m n) k) : (a : Perfection (ModP O p) p) → ModP O p) g : ModP O p)
    (0 : ModP O p)
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
have hk₁ : Ne (α := ModP O p)
  ((Perfection.coeff (ModP O p) p (max (max m n) k) : (a : Perfection (ModP O p) p) → ModP O p) (f + g) : ModP O p)
  (0 : ModP O p)
Tactic: replace hk := coeff_ne_zero_of_le hk (le_max_right (max m n) k)
Cleared hypotheses: hk
-- 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
m n k : ℕ
hm :
  Ne (α := ModP O p)
    ((Perfection.coeff (ModP O p) p (max (max m n) k) : (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 (max m n) k) : (a : Perfection (ModP O p) p) → ModP O p) g : ModP O p)
    (0 : ModP O p)
hk :
  Ne (α := ModP O p)
    ((Perfection.coeff (ModP O p) p (max (max m n) k) : (a : Perfection (ModP O p) p) → ModP O p) (f + g) : ModP O p)
    (0 : ModP O p)
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
have neg : ModP.preVal K v O p
      (HAdd.hAdd (α := ModP O p) (β := ModP O p) ((coeff (max (max m n) k) : (a : PreTilt O p) → ModP O p) f : ModP O p)
        ((coeff (max (max m n) k) : (a : PreTilt O p) → ModP O p) g : ModP O p)) ^
    p ^ max (max m n) k ≤
  max (ModP.preVal K v O p ((coeff (max (max m n) k) : (a : PreTilt O p) → ModP O p) f) ^ p ^ max (max m n) k)
    (ModP.preVal K v O p ((coeff (max (max m n) k) : (a : PreTilt O p) → ModP O p) g) ^ p ^ max (max m n) k)
Tactic: rw [valAux_eq hv hm, valAux_eq hv hn, valAux_eq hv hk, map_add]