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
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)
⊢ 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)
have 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)
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
-- 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)
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)
⊢ 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)
have 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)
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
-- 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
⊢ Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) f : ℝ≥0) (0 : ℝ≥0) ↔ f = 0
have 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
Tactic: by_cases hf0 : 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 : 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
⊢ Eq (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) f : ℝ≥0) (0 : ℝ≥0) ↔ f = 0
have 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
Tactic: by_cases hf0 : 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 : PreTilt O p
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
have 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
Tactic: rw [hf0]
-- 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
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
have 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
Tactic: obtain ⟨n, hn⟩ : ∃ n, coeff n f ≠ 0 := not_forall.1 fun h => hf0 <| 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 : 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
have 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)
Tactic: refine iff_of_false (fun hvf => hn ?_) hf0
-- 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
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
⊢ Eq (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
have hvf₁ : 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
Cleared hypotheses: hvf
-- 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
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
⊢ Eq (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
have hvf₁ : 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
Cleared hypotheses: hvf
-- 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
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
⊢ Eq (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
have 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)
Tactic: rwa [ModP.preVal_eq_zero hv] at hvf
Cleared hypotheses: hvf
-- 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)
⊢ IsDomain.{u₂} (PreTilt O p)
have hp : Nat.Prime p
Tactic: have hp : Nat.Prime p := Fact.out
-- 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)
hp : Nat.Prime p
⊢ IsDomain.{u₂} (PreTilt O p)
have this : Nontrivial.{u₂} (PreTilt O p)
Tactic: haveI : Nontrivial (PreTilt O p) := ⟨(CharP.nontrivial_of_char_ne_one hp.ne_one).1⟩
-- 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)
hp : Nat.Prime p
this : Nontrivial.{u₂} (PreTilt O p)
a b : PreTilt O p
hfg : a * b = 0
⊢ a = 0 ∨ b = 0
have 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)
Tactic: simp_rw [← map_eq_zero hv] 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)
hp : Nat.Prime p
this : Nontrivial.{u₂} (PreTilt O p)
a b : PreTilt O p
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)
have contrapose! : ∀
  (hfg :
    Ne (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) a : ℝ≥0) (0 : ℝ≥0) ∧
      Ne (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) b : ℝ≥0) (0 : ℝ≥0)),
  Ne (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) (a * b) : ℝ≥0) (0 : ℝ≥0)
Tactic: contrapose! 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)
hp : Nat.Prime p
this : Nontrivial.{u₂} (PreTilt O p)
a b : PreTilt O p
hfg :
  Ne (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) a : ℝ≥0) (0 : ℝ≥0) ∧
    Ne (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) b : ℝ≥0) (0 : ℝ≥0)
⊢ Ne (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) (a * b) : ℝ≥0) (0 : ℝ≥0)
have rw : HMul.hMul (α := ℝ≥0) (β := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) a : ℝ≥0)
    (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) b : ℝ≥0) ≠
  0
Tactic: rw [Valuation.map_mul]
-- 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)
hp : Nat.Prime p
this : Nontrivial.{u₂} (PreTilt O p)
⊢ IsDomain.{u₂} (PreTilt O p)
have this₁ : NoZeroDivisors.{u₂} (PreTilt O p)
Tactic: haveI : NoZeroDivisors (PreTilt O p) :=
    ⟨fun hfg => by
      simp_rw [← map_eq_zero hv] at hfg ⊢; contrapose! hfg; rw [Valuation.map_mul]
      exact mul_ne_zero hfg.1 hfg.2⟩
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (goal)
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
⊢ Membership.mem (γ := Submodule (𝕎 R) (𝕎 R))
      (RingHom.ker (F := 𝕎 R →+* 𝕎 HasQuotient.Quotient R (B := Ideal R) 𝔭) (map (Ideal.Quotient.mk 𝔭))) x →
    Membership.mem (γ := Submodule (𝕎 R) (𝕎 R))
      (RingHom.ker (F := 𝕎 R →+* R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
        (RingHom.comp (Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1))) (ghostComponent n)))
      x
have simp : (∀ (n : ℕ),
    Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
      ((Ideal.Quotient.mk 𝔭 : (a : R) → R ⧸ 𝔭) (x.coeff n) : HasQuotient.Quotient R (B := Ideal R) 𝔭)
      (0 : HasQuotient.Quotient R (B := Ideal R) 𝔭)) →
  Eq (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1))
        ((ghostComponent n : (a : 𝕎 R) → R) x) :
      R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    (0 : R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
Tactic: simp only [RingHom.mem_ker, map_eq_zero_iff, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (goal)
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
h :
  ∀ (n : ℕ),
    Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
      ((Ideal.Quotient.mk 𝔭 : (a : R) → R ⧸ 𝔭) (x.coeff n) : HasQuotient.Quotient R (B := Ideal R) 𝔭)
      (0 : HasQuotient.Quotient R (B := Ideal R) 𝔭)
⊢ Eq (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1))
        ((ghostComponent n : (a : 𝕎 R) → R) x) :
      R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    (0 : R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
have simp : Eq (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
  ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1))
      ((RingHom.comp (Pi.evalRingHom (fun (a : ℕ) ↦ R) n) ghostMap : (a : 𝕎 R) → R) x) :
    R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
  (0 : R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
Tactic: simp only [ghostComponent]
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (goal)
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
h :
  ∀ (n : ℕ),
    Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
      ((Ideal.Quotient.mk 𝔭 : (a : R) → R ⧸ 𝔭) (x.coeff n) : HasQuotient.Quotient R (B := Ideal R) 𝔭)
      (0 : HasQuotient.Quotient R (B := Ideal R) 𝔭)
⊢ Eq (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1))
        ((RingHom.comp (Pi.evalRingHom (fun (a : ℕ) ↦ R) n) ghostMap : (a : 𝕎 R) → R) x) :
      R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    (0 : R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
have apply_fun : Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (↑p : R) (n + 1)}))
  ((quotEquivOfEq sorry : (a : R ⧸ 𝔭 ^ (n + 1)) → R ⧸ span {(↑p : R) ^ (n + 1)})
      ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1))
        ((RingHom.comp (Pi.evalRingHom (fun (a : ℕ) ↦ R) n) ghostMap : (a : 𝕎 R) → R) x)) :
    HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (↑p : R) (n + 1)}))
  ((quotEquivOfEq sorry : (a : R ⧸ 𝔭 ^ (n + 1)) → R ⧸ span {(↑p : R) ^ (n + 1)}) 0 :
    HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (↑p : R) (n + 1)}))
Tactic: apply_fun Ideal.quotEquivOfEq (Ideal.span_singleton_pow _ (n + 1))
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (goal)
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
h :
  ∀ (n : ℕ),
    Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
      ((Ideal.Quotient.mk 𝔭 : (a : R) → R ⧸ 𝔭) (x.coeff n) : HasQuotient.Quotient R (B := Ideal R) 𝔭)
      (0 : HasQuotient.Quotient R (B := Ideal R) 𝔭)
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (↑p : R) (n + 1)}))
    ((quotEquivOfEq ⋯ : (a : R ⧸ 𝔭 ^ (n + 1)) → R ⧸ span {(↑p : R) ^ (n + 1)})
        ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1))
          ((RingHom.comp (Pi.evalRingHom (fun (a : ℕ) ↦ R) n) ghostMap : (a : 𝕎 R) → R) x)) :
      HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (↑p : R) (n + 1)}))
    ((quotEquivOfEq ⋯ : (a : R ⧸ 𝔭 ^ (n + 1)) → R ⧸ span {(↑p : R) ^ (n + 1)}) 0 :
      HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (↑p : R) (n + 1)}))
have simp : Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (↑p : R) (n + 1)}))
  ((Ideal.Quotient.mk (span {HPow.hPow (α := R) (↑p : R) (n + 1)}) : (a : R) → R ⧸ span {(↑p : R) ^ (n + 1)})
      ((ghostComponent n : (a : 𝕎 R) → R) x) :
    HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (↑p : R) (n + 1)}))
  (0 : HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (↑p : R) (n + 1)}))
Tactic: simp only [RingHom.coe_comp, Function.comp_apply, Pi.evalRingHom_apply, ghostMap_apply,
    quotEquivOfEq_mk, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (goal)
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
h :
  ∀ (n : ℕ),
    Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
      ((Ideal.Quotient.mk 𝔭 : (a : R) → R ⧸ 𝔭) (x.coeff n) : HasQuotient.Quotient R (B := Ideal R) 𝔭)
      (0 : HasQuotient.Quotient R (B := Ideal R) 𝔭)
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (↑p : R) (n + 1)}))
    ((Ideal.Quotient.mk (span {HPow.hPow (α := R) (↑p : R) (n + 1)}) : (a : R) → R ⧸ span {(↑p : R) ^ (n + 1)})
        ((ghostComponent n : (a : 𝕎 R) → R) x) :
      HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (↑p : R) (n + 1)}))
    (0 : HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (↑p : R) (n + 1)}))
have simp : ∀ (h : ∀ (n : ℕ), (↑p : R) ∣ x.coeff n), HPow.hPow (α := R) (↑p : R) (n + 1) ∣ (ghostComponent n : (a : 𝕎 R) → R) x
Tactic: simp only [eq_zero_iff_dvd] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (goal)
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
x : 𝕎 HasQuotient.Quotient R (B := Ideal R) 𝔭
h : HPow.hPow (α := Ideal R) 𝔭 (HAdd.hAdd (α := ℕ) 0 1) = 𝔭
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((quotEquivOfEq h : (a : R ⧸ 𝔭 ^ (0 + 1)) → R ⧸ 𝔭)
        ((ghostComponentModPPow 0 : (a : 𝕎 (R ⧸ 𝔭)) → R ⧸ 𝔭 ^ (0 + 1)) x) :
      HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((ghostComponent 0 : (a : 𝕎 (R ⧸ 𝔭)) → R ⧸ 𝔭) x : HasQuotient.Quotient R (B := Ideal R) 𝔭)
have obtain : ∀ (y : 𝕎 R) (hy : (map (Ideal.Quotient.mk 𝔭) : (a : 𝕎 R) → 𝕎 (R ⧸ 𝔭)) y = x),
  Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((quotEquivOfEq h : (a : R ⧸ 𝔭 ^ (0 + 1)) → R ⧸ 𝔭)
        ((ghostComponentModPPow 0 : (a : 𝕎 (R ⧸ 𝔭)) → R ⧸ 𝔭 ^ (0 + 1)) x) :
      HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((ghostComponent 0 : (a : 𝕎 (R ⧸ 𝔭)) → R ⧸ 𝔭) x : HasQuotient.Quotient R (B := Ideal R) 𝔭)
Tactic: obtain ⟨y, hy⟩ := map_surjective _ Ideal.Quotient.mk_surjective x
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (goal)
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Fact ¬IsUnit.{u} (M := R) (↑p : R)
inst_3 : IsAdicComplete (R := R) 𝔭 R
n : ℕ
⊢ Eq (α := 𝕎 R♭ →+* R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (factorPowSucc 𝔭 (n + 1) :
          R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1 + 1) →+* R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
        (fontaineThetaModPPow R p (n + 1) : 𝕎 R♭ →+* R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1 + 1)) :
      𝕎 R♭ →+* R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    (fontaineThetaModPPow R p n : 𝕎 R♭ →+* R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
have hp : IsNilpotent.{u} (R := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1))
Tactic: apply eq_of_apply_teichmuller_eq ((factorPowSucc _ _).comp (fontaineThetaModPPow R p (n + 1)))
    (fontaineThetaModPPow R p n)