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)
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)
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)
⊢ 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
-- 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 : ∃ (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)
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)
⊢ 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
-- 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
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)
⊢ 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))
-- 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
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)
⊢ 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))
-- 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
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)
⊢ 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)
-- 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
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)
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)
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)

Tactic:
rw [valAux_eq hv hm, valAux_eq hv hn, valAux_eq hv hk, map_add]

Premises used: PreTilt.valAux_eq, map_add
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
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)
neg :
  ∀
    (h :
      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)) ≤
        ModP.preVal K v O p ((coeff (max (max m n) k) : (a : PreTilt O p) → ModP O p) f)),
    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)
neg₁ :
  ∀
    (h :
      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)) ≤
        ModP.preVal K v O p ((coeff (max (max m n) k) : (a : PreTilt O p) → ModP O p) g)),
    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)
⊢ 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:
rcases le_max_iff.1
      (ModP.preVal_add hv (coeff (max (max m n) k) f)
      (coeff (max (max m n) k) g)) with h | h

Premises used: PreTilt.coeff, Max.max, Iff.mp, ModP.preVal_add, le_max_iff, DFunLike.coe
-- 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
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)
h :
  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)) ≤
    ModP.preVal K v O p ((coeff (max (max m n) k) : (a : PreTilt O p) → ModP O p) f)
⊢ 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:
le_max_of_le_left (pow_le_pow_left' h _)

Premises used: le_max_of_le_left, pow_le_pow_left'
-- 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
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)
h :
  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)) ≤
    ModP.preVal K v O p ((coeff (max (max m n) k) : (a : PreTilt O p) → ModP O p) f)
⊢ 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:
exact le_max_of_le_left (pow_le_pow_left' h _)

Premises used: le_max_of_le_left, pow_le_pow_left'
-- 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
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)
h :
  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)) ≤
    ModP.preVal K v O p ((coeff (max (max m n) k) : (a : PreTilt O p) → ModP O p) g)
⊢ 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:
le_max_of_le_right (pow_le_pow_left' h _)

Premises used: le_max_of_le_right, pow_le_pow_left'
-- 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
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)
h :
  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)) ≤
    ModP.preVal K v O p ((coeff (max (max m n) k) : (a : PreTilt O p) → ModP O p) g)
⊢ 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:
exact le_max_of_le_right (pow_le_pow_left' h _)

Premises used: le_max_of_le_right, pow_le_pow_left'
-- 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
pos :
  ∀ (hf0 : f = 0),
    Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) f : ℝ≥0) (0 : ℝ≥0) ↔ f = 0
neg :
  ∀ (hf0 : ¬f = 0),
    Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) f : ℝ≥0) (0 : ℝ≥0) ↔ f = 0
⊢ Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) f : ℝ≥0) (0 : ℝ≥0) ↔ f = 0

Tactic:
by_cases hf0 : f = 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 : PreTilt O p
hf0 : f = 0
pos :
  Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) 0 : ℝ≥0) (0 : ℝ≥0) ↔
    Eq.{u₂ + 1} (α := PreTilt O p) 0 0
⊢ Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) f : ℝ≥0) (0 : ℝ≥0) ↔ f = 0

Tactic:
rw [hf0]
-- 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
hf0 : f = 0
⊢ Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) 0 : ℝ≥0) (0 : ℝ≥0) ↔
    Eq.{u₂ + 1} (α := PreTilt O p) 0 0

Tactic:
iff_of_true (Valuation.map_zero _) rfl

Premises used: iff_of_true, Valuation.map_zero, 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
hf0 : f = 0
⊢ Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) 0 : ℝ≥0) (0 : ℝ≥0) ↔
    Eq.{u₂ + 1} (α := PreTilt O p) 0 0

Tactic:
exact iff_of_true (Valuation.map_zero _) rfl

Premises used: iff_of_true, Valuation.map_zero, 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
hf0 : ¬f = 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 => hf0 <| 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 : PreTilt O p
hf0 : ¬f = 0
neg :
  ∀ (n : ℕ) (hn : Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)),
    Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) f : ℝ≥0) (0 : ℝ≥0) ↔ f = 0
⊢ Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) f : ℝ≥0) (0 : ℝ≥0) ↔ f = 0

Tactic:
obtain ⟨n, hn⟩ : ∃ n, coeff n f ≠ 0 := not_forall.1 fun h => hf0 <| 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 : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : 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 = 0 ↔ f = 0

Tactic:
iff_of_false (fun hvf => hn ?_) hf0

Premises used: iff_of_false
-- 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
hf0 : ¬f = 0
n : ℕ
hn : Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
neg :
  ∀ (hvf : valAux K v O p f = 0),
    Eq (α := 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 = 0 ↔ f = 0

Tactic:
refine iff_of_false (fun hvf => hn ?_) hf0

Premises used: iff_of_false
-- 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
hf0 : ¬f = 0
n : ℕ
hn : Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
hvf : valAux K v O p f = 0
⊢ ModP.preVal K v O p ((coeff n : (a : PreTilt O p) → ModP O p) f) ^ p ^ n = 0

Tactic:
rw [valAux_eq hv hn] at hvf

Premises used: PreTilt.valAux_eq
-- 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
hf0 : ¬f = 0
n : ℕ
hn : Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
hvf : ModP.preVal K v O p ((coeff n : (a : PreTilt O p) → ModP O p) f) ^ p ^ n = 0
⊢ ModP.preVal K v O p ((coeff n : (a : PreTilt O p) → ModP O p) f) = 0

Tactic:
replace hvf := eq_zero_of_pow_eq_zero hvf
-- 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
hf0 : ¬f = 0
n : ℕ
hn : Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
hvf : ModP.preVal K v O p ((coeff n : (a : PreTilt O p) → ModP O p) f) = 0
neg neg₁ neg₂ neg₃ :
  ∀ (hvf : Eq (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)),
    Eq (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
⊢ Eq (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)

Tactic:
rwa [ModP.preVal_eq_zero hv] at hvf

Premises used: ModP.preVal_eq_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)
⊢ Nat.Prime p

Tactic:
have hp : Nat.Prime p := 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)
hp : Nat.Prime p
⊢ Nontrivial.{u₂} (PreTilt O p)

Tactic:
haveI : Nontrivial (PreTilt O p) := ⟨(CharP.nontrivial_of_char_ne_one hp.ne_one).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)
hp : Nat.Prime p
this : Nontrivial.{u₂} (PreTilt O p)
a b : PreTilt O p
hfg : a * b = 0
simp_rw :
  ∀
    (hfg :
      Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) (a * b) : ℝ≥0)
        (0 : ℝ≥0)),
    Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) a : ℝ≥0) (0 : ℝ≥0) ∨
      Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) b : ℝ≥0) (0 : ℝ≥0)
⊢ a = 0 ∨ b = 0

Tactic:
simp_rw [← map_eq_zero hv] at hfg ⊢

Premises used: PreTilt.map_eq_zero