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)
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)
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)
⊢ 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:
contrapose! 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)
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)
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
⊢ Ne (α := ℝ≥0) (((val K v O hv p : Valuation (PreTilt O p) ℝ≥0) : (a : PreTilt O p) → ℝ≥0) (a * b) : ℝ≥0) (0 : ℝ≥0)

Tactic:
rw [Valuation.map_mul]

Premises used: Valuation.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)
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)
⊢ 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:
mul_ne_zero hfg.1 hfg.2

Premises used: And.right, And.left, mul_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)
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)
⊢ 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:
exact mul_ne_zero hfg.1 hfg.2

Premises used: And.right, And.left, mul_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)
hp : Nat.Prime p
this : Nontrivial.{u₂} (PreTilt O p)
⊢ 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⟩
-- 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_1 : Nontrivial.{u₂} (PreTilt O p)
this : NoZeroDivisors.{u₂} (PreTilt O p)
⊢ IsDomain.{u₂} (PreTilt O p)

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- 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_1 : Nontrivial.{u₂} (PreTilt O p)
this : NoZeroDivisors.{u₂} (PreTilt O p)
⊢ IsDomain.{u₂} (PreTilt O p)

Tactic:
exact NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.RingTheory.Perfectoid.BDeRham
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) (span {(↑p : R)}) R
⊢ IsUnit (M := Localization.Away (M := R) (↑p : R))
    ((RingHom.comp (algebraMap R (Localization.Away (M := R) (↑p : R))) (fontaineTheta R p) :
        (a : 𝕎 R♭) → Localization.Away (↑p : R))
      (↑p : 𝕎 R♭))

Tactic:
simpa using IsLocalization.Away.algebraMap_isUnit (p : R)

Premises used: Nat.cast, IsLocalization.Away.algebraMap_isUnit
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
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))
⊢ 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

Tactic:
simp only [RingHom.mem_ker, map_eq_zero_iff, RingHom.comp_apply]

Premises used: RingHom.mem_ker, WittVector.map_eq_zero_iff, RingHom.comp_apply
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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) 𝔭)
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))
⊢ 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 [ghostComponent]

Premises used: WittVector.ghostComponent
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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) 𝔭)
apply_fun :
  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)}))
⊢ 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:
apply_fun Ideal.quotEquivOfEq (Ideal.span_singleton_pow _ (n + 1))

Premises used: Ideal.quotEquivOfEq, HAdd.hAdd, OfNat.ofNat, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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) 𝔭)
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)}))
⊢ 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)}))

Tactic:
simp only [RingHom.coe_comp, Function.comp_apply, Pi.evalRingHom_apply, ghostMap_apply,
    quotEquivOfEq_mk, map_zero]

Premises used: Pi.evalRingHom_apply, Ideal.quotEquivOfEq_mk, map_zero, WittVector.ghostMap_apply, RingHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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) 𝔭)
simp :
  ∀ (h : ∀ (n : ℕ), (↑p : R) ∣ x.coeff n), HPow.hPow (α := R) (↑p : R) (n + 1) ∣ (ghostComponent n : (a : 𝕎 R) → R) x
⊢ 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 [eq_zero_iff_dvd] at h ⊢

Premises used: Ideal.Quotient.eq_zero_iff_dvd
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
h : ∀ (n : ℕ), (↑p : R) ∣ x.coeff n
⊢ HPow.hPow (α := R) (↑p : R) (n + 1) ∣ (ghostComponent n : (a : 𝕎 R) → R) x

Tactic:
pow_dvd_ghostComponent_of_dvd_coeff (fun _ _ ↦ h _)

Premises used: WittVector.pow_dvd_ghostComponent_of_dvd_coeff
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
h : ∀ (n : ℕ), (↑p : R) ∣ x.coeff n
⊢ HPow.hPow (α := R) (↑p : R) (n + 1) ∣ (ghostComponent n : (a : 𝕎 R) → R) x

Tactic:
exact pow_dvd_ghostComponent_of_dvd_coeff (fun _ _ ↦ h _)

Premises used: WittVector.pow_dvd_ghostComponent_of_dvd_coeff
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
⊢ Eq (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    ((ghostComponentModPPow n : (a : 𝕎 (R ⧸ 𝔭)) → R ⧸ 𝔭 ^ (n + 1))
        ((map (Ideal.Quotient.mk 𝔭) : (a : 𝕎 R) → 𝕎 (R ⧸ 𝔭)) x) :
      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))

Tactic:
RingHom.liftOfSurjective_comp_apply ..

Premises used: RingHom.liftOfSurjective_comp_apply, Submodule.Quotient.mk
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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) = 𝔭
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) 𝔭)
⊢ 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

Premises used: Ideal.Quotient.mk_surjective, WittVector.map_surjective
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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) = 𝔭
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:
simp [← hy, ghostComponent_apply]

Premises used: WittVector.ghostComponent_apply
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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 : ℕ
x : R♭
⊢ Eq (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    ((ghostComponentModPPow n : (a : 𝕎 (R ⧸ 𝔭)) → R ⧸ 𝔭 ^ (n + 1))
        ((teichmuller p : (a : R ⧸ 𝔭) → 𝕎 (R ⧸ 𝔭)) ((PreTilt.coeff n : (a : R♭) → ModP R p) x : ModP R p)) :
      R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1)) ((untilt : (a : R♭) → R) x) :
      R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))

Tactic:
simpa using ghostComponentModPPow_map_mk n
    (teichmuller p ((((_root_.frobeniusEquiv _ p).symm ^ n) x).untilt))

Premises used: frobeniusEquiv, HPow.hPow, PreTilt.untilt, DFunLike.coe, RingEquiv.symm, WittVector.teichmuller, WittVector.ghostComponentModPPow_map_mk
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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 : ℕ
x : R♭
⊢ Eq (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    ((fontaineThetaModPPow R p n : (a : 𝕎 R♭) → R ⧸ 𝔭 ^ (n + 1)) ((teichmuller p : (a : R♭) → 𝕎 R♭) x) :
      R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1)) ((untilt : (a : R♭) → R) x) :
      R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))

Tactic:
simp [fontaineThetaModPPow]

Premises used: WittVector.fontaineThetaModPPow
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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 : ℕ
hp : IsNilpotent.{u} (R := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1))
h :
  ∀ (x : R♭),
    Eq (α := 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)) :
            (a : 𝕎 R♭) → R ⧸ 𝔭 ^ (n + 1))
          ((teichmuller p : (a : R♭) → 𝕎 R♭) x) :
        R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
      ((fontaineThetaModPPow R p n : (a : 𝕎 R♭) → R ⧸ 𝔭 ^ (n + 1)) ((teichmuller p : (a : R♭) → 𝕎 R♭) x) :
        R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
⊢ 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))

Tactic:
apply eq_of_apply_teichmuller_eq ((factorPowSucc _ _).comp (fontaineThetaModPPow R p (n + 1)))
    (fontaineThetaModPPow R p n)

Premises used: WittVector.fontaineThetaModPPow, RingHom.comp, HAdd.hAdd, Ideal.Quotient.factorPowSucc, OfNat.ofNat, WittVector.eq_of_apply_teichmuller_eq
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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 : ℕ
h : HPow.hPow (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1)) (n + 1) = 0
⊢ IsNilpotent.{u} (R := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1))

Tactic:
use n + 1
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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 ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1))
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1)) (↑p : R))

Tactic:
simp [map_natCast]

Premises used: map_natCast
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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 ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1))
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1)) (↑p : R))

Tactic:
have : p = Ideal.Quotient.mk (𝔭 ^ (n + 1)) p := by
      simp [map_natCast]
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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 : ℕ
this :
  Eq (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1))
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1)) (↑p : R))
h : HPow.hPow (α := R) (↑p : R) (n + 1) ∈ HPow.hPow (α := Ideal R) 𝔭 (n + 1)
⊢ HPow.hPow (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1)) (n + 1) = 0

Tactic:
rw [this, ← map_pow, Ideal.Quotient.eq_zero_iff_mem]

Premises used: map_pow, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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 : ℕ
this :
  Eq (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1))
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1)) (↑p : R))
⊢ HPow.hPow (α := R) (↑p : R) (n + 1) ∈ HPow.hPow (α := Ideal R) 𝔭 (n + 1)

Tactic:
Ideal.pow_mem_pow (mem_span_singleton_self _) _

Premises used: Set.Mem, Ideal.pow_mem_pow, Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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 : ℕ
this :
  Eq (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1))
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1)) (↑p : R))
⊢ HPow.hPow (α := R) (↑p : R) (n + 1) ∈ HPow.hPow (α := Ideal R) 𝔭 (n + 1)

Tactic:
exact Ideal.pow_mem_pow (mem_span_singleton_self _) _

Premises used: Ideal.pow_mem_pow, Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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 : ℕ
⊢ ∀ (x : R♭),
    Eq (α := 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)) :
            (a : 𝕎 R♭) → R ⧸ 𝔭 ^ (n + 1))
          ((teichmuller p : (a : R♭) → 𝕎 R♭) x) :
        R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
      ((fontaineThetaModPPow R p n : (a : 𝕎 R♭) → R ⧸ 𝔭 ^ (n + 1)) ((teichmuller p : (a : R♭) → 𝕎 R♭) x) :
        R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))

Tactic:
simp [fontaineThetaModPPow]

Premises used: WittVector.fontaineThetaModPPow
-- Module: Mathlib.RingTheory.Perfectoid.FontaineTheta
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 : ℕ
x : 𝕎 R♭
⊢ Eq (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    (((factorPowSucc 𝔭 (n + 1) :
            R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1 + 1) →+* R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) :
          (a : R ⧸ 𝔭 ^ (n + 1 + 1)) → R ⧸ 𝔭 ^ (n + 1))
        ((fontaineThetaModPPow R p (n + 1) : (a : 𝕎 R♭) → R ⧸ 𝔭 ^ (n + 1 + 1)) x) :
      R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    ((fontaineThetaModPPow R p n : (a : 𝕎 R♭) → R ⧸ 𝔭 ^ (n + 1)) x : R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1))

Tactic:
simp [← factorPowSucc_comp_fontaineThetaModPPow n]

Premises used: WittVector.factorPowSucc_comp_fontaineThetaModPPow