awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (n + 1)) : (a : R) → R ⧸ 𝔭 ^ (n + 1))
        ((fontaineTheta R p : (a : 𝕎 R♭) → R) 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:
Order.succ_strictMono.mk_liftRingHom 𝔭 _ (factorPowSucc_comp_fontaineThetaModPPow _) x

Premises used: IsAdicComplete.StrictMono.mk_liftRingHom, WittVector.factorPowSucc_comp_fontaineThetaModPPow, Order.succ, Order.succ_strictMono, Nat.cast, Ideal.span, Singleton.singleton
-- 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
x : 𝕎 R♭
⊢ Eq (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (HAdd.hAdd (α := ℕ) 0 1))
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) 𝔭 (HAdd.hAdd (α := ℕ) 0 1)) : (a : R) → R ⧸ 𝔭 ^ (0 + 1))
        ((fontaineTheta R p : (a : 𝕎 R♭) → R) x) :
      R ⧸ HPow.hPow (α := Ideal R) 𝔭 (HAdd.hAdd (α := ℕ) 0 1))
    ((fontaineThetaModPPow R p 0 : (a : 𝕎 R♭) → R ⧸ 𝔭 ^ (0 + 1)) x :
      R ⧸ HPow.hPow (α := Ideal R) 𝔭 (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
have := mk_pow_fontaineTheta 0 x
-- 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
x : 𝕎 R♭
this :
  Eq (α := R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) 𝔭 1)
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) (β := ℕ) 𝔭 1) : (a : R) → R ⧸ 𝔭 ^ 1)
        ((fontaineTheta R p : (a : 𝕎 R♭) → R) x) :
      R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) 𝔭 1)
    ((fontaineThetaModPPow R p 0 : (a : 𝕎 R♭) → R ⧸ 𝔭 ^ 1) x : R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) 𝔭 1)
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((quotEquivOfEq ⋯ : (a : R ⧸ 𝔭 ^ 1) → R ⧸ 𝔭)
        ((Ideal.Quotient.mk (HPow.hPow (α := Ideal R) (β := ℕ) 𝔭 1) : (a : R) → R ⧸ 𝔭 ^ 1)
          ((fontaineTheta R p : (a : 𝕎 R♭) → R) x)) :
      HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((quotEquivOfEq ⋯ : (a : R ⧸ 𝔭 ^ 1) → R ⧸ 𝔭) ((fontaineThetaModPPow R p 0 : (a : 𝕎 R♭) → R ⧸ 𝔭 ^ 1) x) :
      HasQuotient.Quotient R (B := Ideal R) 𝔭)

Tactic:
apply_fun Ideal.quotEquivOfEq (pow_one (p : R) ▸ Ideal.span_singleton_pow (p : R) 1) at this

Premises used: Ideal.quotEquivOfEq
-- 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
x : 𝕎 R♭
this :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((Ideal.Quotient.mk 𝔭 : (a : R) → R ⧸ 𝔭) ((fontaineTheta R p : (a : 𝕎 R♭) → R) x) :
      HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((quotEquivOfEq ⋯ : (a : R ⧸ 𝔭 ^ 1) → R ⧸ 𝔭) ((fontaineThetaModPPow R p 0 : (a : 𝕎 R♭) → R ⧸ 𝔭 ^ 1) x) :
      HasQuotient.Quotient R (B := Ideal R) 𝔭)
rw :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((quotEquivOfEq ⋯ : (a : R ⧸ 𝔭 ^ 1) → R ⧸ 𝔭) ((fontaineThetaModPPow R p 0 : (a : 𝕎 R♭) → R ⧸ 𝔭 ^ 1) x) :
      HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((PreTilt.coeff 0 : (a : R♭) → ModP R p) (x.coeff 0) : ModP R p)
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((Ideal.Quotient.mk 𝔭 : (a : R) → R ⧸ 𝔭) ((fontaineTheta R p : (a : 𝕎 R♭) → R) x) :
      HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((PreTilt.coeff 0 : (a : R♭) → ModP R p) (x.coeff 0) : ModP R p)

Tactic:
rw [this]
-- 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
x : 𝕎 R♭
this :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((Ideal.Quotient.mk 𝔭 : (a : R) → R ⧸ 𝔭) ((fontaineTheta R p : (a : 𝕎 R♭) → R) x) :
      HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((quotEquivOfEq ⋯ : (a : R ⧸ 𝔭 ^ 1) → R ⧸ 𝔭) ((fontaineThetaModPPow R p 0 : (a : 𝕎 R♭) → R ⧸ 𝔭 ^ 1) x) :
      HasQuotient.Quotient R (B := Ideal R) 𝔭)
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((quotEquivOfEq ⋯ : (a : R ⧸ 𝔭 ^ 1) → R ⧸ 𝔭) ((fontaineThetaModPPow R p 0 : (a : 𝕎 R♭) → R ⧸ 𝔭 ^ 1) x) :
      HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((PreTilt.coeff 0 : (a : R♭) → ModP R p) (x.coeff 0) : ModP R p)

Tactic:
simp [fontaineThetaModPPow, ghostComponent_apply, RingHom.one_def]

Premises used: WittVector.ghostComponent_apply, RingHom.one_def, 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
x : R♭
rw :
  ∀ (n : ℕ),
    SModEq (R := R) (M := R) (HSMul.hSMul (β := Submodule R R) (HPow.hPow (α := Ideal R) 𝔭 n) ⊤)
      ((fontaineTheta R p : (a : 𝕎 R♭) → R) ((teichmuller p : (a : R♭) → 𝕎 R♭) x : 𝕎 R♭) : R)
      ((untilt : (a : R♭) → R) x : R)
⊢ Eq (α := R) ((fontaineTheta R p : (a : 𝕎 R♭) → R) ((teichmuller p : (a : R♭) → 𝕎 R♭) x : 𝕎 R♭) : R)
    ((untilt : (a : R♭) → R) x : R)

Tactic:
rw [IsHausdorff.eq_iff_smodEq (I := 𝔭)]
-- 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
x : R♭
simp :
  ∀ (n : ℕ),
    SModEq (R := R) (M := R) (HPow.hPow (α := Ideal R) 𝔭 n)
      ((fontaineTheta R p : (a : 𝕎 R♭) → R) ((teichmuller p : (a : R♭) → 𝕎 R♭) x : 𝕎 R♭) : R)
      ((untilt : (a : R♭) → R) x : R)
⊢ ∀ (n : ℕ),
    SModEq (R := R) (M := R) (HSMul.hSMul (β := Submodule R R) (HPow.hPow (α := Ideal R) 𝔭 n) ⊤)
      ((fontaineTheta R p : (a : 𝕎 R♭) → R) ((teichmuller p : (a : R♭) → 𝕎 R♭) x : 𝕎 R♭) : R)
      ((untilt : (a : R♭) → R) x : R)

Tactic:
simp only [smul_eq_mul, mul_top]

Premises used: smul_eq_mul, Ideal.mul_top
-- 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
x : R♭
n : ℕ
zero :
  SModEq (R := R) (M := R) (HPow.hPow (α := Ideal R) (β := ℕ) 𝔭 0)
    ((fontaineTheta R p : (a : 𝕎 R♭) → R) ((teichmuller p : (a : R♭) → 𝕎 R♭) x : 𝕎 R♭) : R)
    ((untilt : (a : R♭) → R) x : R)
succ :
  ∀ (n : ℕ),
    SModEq (R := R) (M := R) (HPow.hPow (α := Ideal R) 𝔭 (n + 1))
      ((fontaineTheta R p : (a : 𝕎 R♭) → R) ((teichmuller p : (a : R♭) → 𝕎 R♭) x : 𝕎 R♭) : R)
      ((untilt : (a : R♭) → R) x : R)
⊢ SModEq (R := R) (M := R) (HPow.hPow (α := Ideal R) 𝔭 n)
    ((fontaineTheta R p : (a : 𝕎 R♭) → R) ((teichmuller p : (a : R♭) → 𝕎 R♭) x : 𝕎 R♭) : R)
    ((untilt : (a : R♭) → R) x : R)

Tactic:
cases n
-- 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
x : R♭
⊢ SModEq (R := R) (M := R) (HPow.hPow (α := Ideal R) (β := ℕ) 𝔭 0)
    ((fontaineTheta R p : (a : 𝕎 R♭) → R) ((teichmuller p : (a : R♭) → 𝕎 R♭) x : 𝕎 R♭) : R)
    ((untilt : (a : R♭) → R) x : R)

Tactic:
simp
-- 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
x : R♭
n : ℕ
⊢ SModEq (R := R) (M := R) (HPow.hPow (α := Ideal R) 𝔭 (n + 1))
    ((fontaineTheta R p : (a : 𝕎 R♭) → R) ((teichmuller p : (a : R♭) → 𝕎 R♭) x : 𝕎 R♭) : R)
    ((untilt : (a : R♭) → R) x : R)

Tactic:
simp [SModEq, mk_pow_fontaineTheta]

Premises used: WittVector.mk_pow_fontaineTheta, SModEq
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
⊢ Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭

Tactic:
simp [map_span]

Premises used: Ideal.map_span
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
⊢ Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭

Tactic:
have : Ideal.map (fontaineTheta R p) (span {(p : 𝕎 R♭)}) = 𝔭 := by
    simp [map_span]
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
rw : IsHausdorff (R := R) 𝔭 R
⊢ IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R

Tactic:
rw [this]
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
⊢ IsHausdorff (R := R) 𝔭 R

Tactic:
infer_instance
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
⊢ IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R

Tactic:
have _ : IsHausdorff ((span {(p : 𝕎 R♭)}).map (fontaineTheta R p)) R := by
    rw [this]
    infer_instance
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
h : IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R
apply :
  Function.Surjective (α := 𝕎 R♭) (β :=
    HasQuotient.Quotient R (B := Ideal R)
      (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})))
    (⇑(RingHom.comp
          (Ideal.Quotient.mk (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})))
          (fontaineTheta R p)) :
      (a : 𝕎 R♭) → R ⧸ Ideal.map (fontaineTheta R p) (span {(↑p : 𝕎 R♭)}))
⊢ Function.Surjective (α := 𝕎 R♭) (β := R) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R)

Tactic:
apply surjective_of_mk_map_comp_surjective (fontaineTheta R p) (I := span {(p : 𝕎 R♭)})
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
h_1 : IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R
h :
  Function.Surjective (α := 𝕎 R♭) (β := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
rwa :
  Function.Surjective (α := 𝕎 R♭) (β :=
    HasQuotient.Quotient R (B := Ideal R)
      (span (Set.image (α := 𝕎 R♭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R) {(↑p : 𝕎 R♭)})))
    (Function.comp (β := R)
      (⇑(Ideal.Quotient.mk (span (Set.image (α := 𝕎 R♭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R) {(↑p : 𝕎 R♭)}))) :
        (a : R) → R ⧸ span ((⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R) '' {(↑p : 𝕎 R♭)}))
      (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
rwa₁ :
  Function.Surjective (α := 𝕎 R♭) (β :=
    HasQuotient.Quotient R (B := Ideal R)
      (span (singleton (α := R) ((fontaineTheta R p : (a : 𝕎 R♭) → R) (↑p : 𝕎 R♭) : R))))
    (Function.comp (β := R)
      (⇑(Ideal.Quotient.mk (span (singleton (α := R) ((fontaineTheta R p : (a : 𝕎 R♭) → R) (↑p : 𝕎 R♭) : R)))) :
        (a : R) → R ⧸ span {(fontaineTheta R p : (a : 𝕎 R♭) → R) (↑p : 𝕎 R♭)})
      (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
rwa₂ rwa₃ rwa₄ rwa₅ :
  Function.Surjective (α := 𝕎 R♭) (β := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
⊢ Function.Surjective (α := 𝕎 R♭) (β :=
    HasQuotient.Quotient R (B := Ideal R)
      (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})))
    (Function.comp (β := R)
      (⇑(Ideal.Quotient.mk (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)}))) :
        (a : R) → R ⧸ Ideal.map (fontaineTheta R p) (span {(↑p : 𝕎 R♭)}))
      (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))

Tactic:
rwa [Ideal.map_span, Set.image_singleton, map_natCast]

Premises used: Set.image_singleton, Ideal.map_span, 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
h : IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R
suffices :
  Function.Surjective (α := 𝕎 R♭) (β := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
⊢ Function.Surjective (α := 𝕎 R♭) (β :=
    HasQuotient.Quotient R (B := Ideal R)
      (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})))
    (Function.comp (β := R)
      (⇑(Ideal.Quotient.mk (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)}))) :
        (a : R) → R ⧸ Ideal.map (fontaineTheta R p) (span {(↑p : 𝕎 R♭)}))
      (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))

Tactic:
suffices h : Function.Surjective (Ideal.Quotient.mk 𝔭 ∘ fontaineTheta R p) by
    rwa [Ideal.map_span, Set.image_singleton, 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
h_1 : IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R
h :
  ∀ (x : 𝕎 R♭),
    Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
      (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R) x)
      (((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0) x)
⊢ Eq (α := 𝕎 R♭ → HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
    ((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0)

Tactic:
ext
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
h : IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R
x : 𝕎 R♭
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R) x)
    (((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0) x)

Tactic:
simp [mk_fontaineTheta]

Premises used: WittVector.mk_fontaineTheta
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
h : IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R
⊢ Eq (α := 𝕎 R♭ → HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
    ((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0)

Tactic:
have : Ideal.Quotient.mk 𝔭 ∘ fontaineTheta R p = (fun x ↦
      PreTilt.coeff 0 x) ∘ fun (x : 𝕎 R♭) ↦ (x.coeff 0) := by
    ext
    simp [mk_fontaineTheta]
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this_1 : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
h : IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R
this :
  Eq (α := 𝕎 R♭ → HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
    ((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0)
rw :
  Function.Surjective.{u + 1, u + 1} (α := 𝕎 R♭) (β := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0)
⊢ Function.Surjective (α := 𝕎 R♭) (β := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))

Tactic:
rw [this]
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this_1 : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
h : IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R
this :
  Eq (α := 𝕎 R♭ → HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
    ((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0)
hg :
  Function.Surjective (β := HasQuotient.Quotient R (B := Ideal R) 𝔭) fun (x : R♭) ↦
    (PreTilt.coeff 0 : (a : R♭) → ModP R p) x
hf : Function.Surjective (β := R♭) fun (x : 𝕎 R♭) ↦ x.coeff 0
⊢ Function.Surjective.{u + 1, u + 1} (α := 𝕎 R♭) (β := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    ((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0)

Tactic:
apply Function.Surjective.comp

Premises used: Function.Surjective.comp
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this_1 : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
h : IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R
this :
  Eq (α := 𝕎 R♭ → HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
    ((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0)
⊢ Function.Surjective (β := HasQuotient.Quotient R (B := Ideal R) 𝔭) fun (x : R♭) ↦
    (PreTilt.coeff 0 : (a : R♭) → ModP R p) x

Tactic:
Perfection.coeff_surjective hF 0

Premises used: Perfection.coeff_surjective, PreTilt, OfNat.ofNat
-- 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
hF :
  Function.Surjective.{u + 1, u + 1} (α := ModP R p) (β := ModP R p)
    (⇑(_root_.frobenius (ModP R p) p) : (a : ModP R p) → ModP R p)
this_1 : Eq (α := Ideal R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) 𝔭
h : IsHausdorff (R := R) (Ideal.map (R := 𝕎 R♭) (F := 𝕎 R♭ →+* R) (fontaineTheta R p) (span {(↑p : 𝕎 R♭)})) R
this :
  Eq (α := 𝕎 R♭ → HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
    ((fun (x : R♭) ↦ (PreTilt.coeff 0 : (a : R♭) → ModP R p) x) ∘ fun (x : 𝕎 R♭) ↦ x.coeff 0)
⊢ Function.Surjective (β := HasQuotient.Quotient R (B := Ideal R) 𝔭) fun (x : R♭) ↦
    (PreTilt.coeff 0 : (a : R♭) → ModP R p) x

Tactic:
exact Perfection.coeff_surjective hF 0

Premises used: Perfection.coeff_surjective, OfNat.ofNat