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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
⊢ Ne.{u₂ + 1} (α := ModP O p) 1 0

Tactic:
one_ne_zero

Premises used: one_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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
⊢ Ne.{u₂ + 1} (α := ModP O p) 1 0

Tactic:
exact one_ne_zero

Premises used: one_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 : ℕ
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
inr : ∀ (hf : f ≠ 0), valAux K v O p (f * g) = valAux K v O p f * 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

Tactic:
obtain rfl | hf := eq_or_ne f 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
g : PreTilt O p
⊢ valAux K v O p (0 * g) = valAux K v O p 0 * valAux K v O p g

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 : ℕ
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
inr₁ : ∀ (hg : g ≠ 0), valAux K v O p (f * g) = valAux K v O p f * 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

Tactic:
obtain rfl | hg := eq_or_ne g 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f : PreTilt O p
hf : f ≠ 0
⊢ valAux K v O p (f * 0) = valAux K v O p f * valAux 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 : ℕ
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
⊢ ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)

Tactic:
not_forall.1 fun h => hf <| Perfection.ext h

Premises used: Perfection.ext, Iff.mp, Classical.not_forall
-- 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 g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
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
⊢ 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

Premises used: Perfection.ext, Iff.mp, Classical.not_forall
-- 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 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 : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) g : ModP O p) (0 : ModP O p)

Tactic:
not_forall.1 fun h => hg <| Perfection.ext h

Premises used: Perfection.ext, Iff.mp, Classical.not_forall
-- 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 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)
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
⊢ 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

Premises used: Perfection.ext, Iff.mp, Classical.not_forall
-- 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 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)
⊢ 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)
-- 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 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)
⊢ 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)
-- 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 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)
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
⊢ 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:
rw [map_mul]

Premises used: 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 : ℕ
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

Tactic:
ModP.mul_ne_zero_of_pow_p_ne_zero (hv := hv) ?_ ?_

Premises used: ModP.mul_ne_zero_of_pow_p_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 : ℕ
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
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
⊢ 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:
refine ModP.mul_ne_zero_of_pow_p_ne_zero (hv := hv) ?_ ?_

Premises used: ModP.mul_ne_zero_of_pow_p_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 : ℕ
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 : Ne (α := ModP O p) ((coeff (max m n) : (a : PreTilt O p) → ModP O p) f : 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

Tactic:
rw [coeff_pow_p f]

Premises used: PreTilt.coeff_pow_p
-- 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 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) : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)

Tactic:
assumption
-- 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 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_2 : Ne (α := ModP O p) ((coeff (max m n) : (a : PreTilt O 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

Tactic:
rw [coeff_pow_p g]

Premises used: PreTilt.coeff_pow_p
-- 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 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) : (a : PreTilt O p) → ModP O p) g : ModP O p) (0 : ModP O p)

Tactic:
assumption
-- 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 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)

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
-- 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 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)
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)
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
rw [valAux_eq hv (coeff_add_ne_zero hm 1),
      valAux_eq hv (coeff_add_ne_zero hn 1), valAux_eq hv hfg]

Premises used: PreTilt.valAux_eq, Perfection.coeff_add_ne_zero, OfNat.ofNat
-- 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 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)
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)
⊢ 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 [map_mul] at hfg ⊢

Premises used: 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 : ℕ
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)
inr₁ 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)
⊢ 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 [ModP.preVal_mul hv hfg, mul_pow]

Premises used: ModP.preVal_mul, mul_pow
-- 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 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)
inr : ∀ (hf : f ≠ 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)

Tactic:
obtain rfl | hf := eq_or_ne f 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
g : PreTilt O p
⊢ valAux K v O p (0 + g) ≤ max (valAux K v O p 0) (valAux K v O p g)

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 : ℕ
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)
inr₁ : ∀ (hg : 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)

Tactic:
obtain rfl | hg := eq_or_ne g 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 : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f : PreTilt O p
hf : f ≠ 0
⊢ valAux K v O p (f + 0) ≤ max (valAux K v O p f) (valAux 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 : ℕ
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)
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)
⊢ 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
-- 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 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)

Tactic:
simp [hfg]
-- 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 g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
hfg : ¬f + g = 0
⊢ ∃ (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
-- 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 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)
⊢ ∃ (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
-- 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 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)
⊢ ∃ (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
-- 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 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)
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)
⊢ 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