awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
hp : IsNilpotent.{u} (R := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : 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))
have 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))
Tactic: apply eq_of_apply_teichmuller_eq ((factorPowSucc _ _).comp (fontaineThetaModPPow R p (n + 1)))
    (fontaineThetaModPPow R p n)
-- 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 : ℕ
⊢ IsNilpotent.{u} (R := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1))
have h : HPow.hPow (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1)) (n + 1) = 0
Tactic: use n + 1
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (hypothesis)
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 : ℕ
⊢ HPow.hPow (α := R ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1)) (n + 1) = 0
have 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))
Tactic: have : p = Ideal.Quotient.mk (𝔭 ^ (n + 1)) p := by
      simp [map_natCast]
-- 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 : ℕ
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 ⧸ HPow.hPow (α := Ideal R) 𝔭 (n + 1)) (↑p : R ⧸ 𝔭 ^ (n + 1)) (n + 1) = 0
have h : HPow.hPow (α := R) (↑p : R) (n + 1) ∈ HPow.hPow (α := Ideal R) 𝔭 (n + 1)
Tactic: rw [this, ← map_pow, Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (hypothesis)
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 (α := 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)
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (hypothesis)
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) 𝔭)
    ((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)
have this₁ : Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
  ((quotEquivOfEq sorry : (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 sorry : (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
Cleared hypotheses: this
-- 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
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) 𝔭)
    ((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)
have rw : Eq (α := HasQuotient.Quotient R (B := Ideal R) 𝔭)
  ((quotEquivOfEq sorry : (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: rw [this]
-- 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
x : R♭
⊢ Eq (α := R) ((fontaineTheta R p : (a : 𝕎 R♭) → R) ((teichmuller p : (a : R♭) → 𝕎 R♭) x : 𝕎 R♭) : R)
    ((untilt : (a : R♭) → R) x : R)
have 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)
Tactic: rw [IsHausdorff.eq_iff_smodEq (I := 𝔭)]
-- 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
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)
have 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)
Tactic: simp only [smul_eq_mul, mul_top]
-- 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
x : R♭
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)
have 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)
Tactic: cases n
Cleared hypotheses: n
-- 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
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)
⊢ 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)
have 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (hypothesis)
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)
⊢ Function.Surjective (α := 𝕎 R♭) (β := R) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R)
have this : 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]
-- 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
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
have rw : IsHausdorff (R := R) 𝔭 R
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (hypothesis)
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♭)})) 𝔭
⊢ Function.Surjective (α := 𝕎 R♭) (β := R) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R)
have x : 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
-- 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
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
⊢ Function.Surjective (α := 𝕎 R♭) (β := R) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R)
have 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♭)}))
Tactic: apply surjective_of_mk_map_comp_surjective (fontaineTheta R p) (I := span {(p : 𝕎 R♭)})
-- 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
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))
⊢ 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))
have 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))
Tactic: rwa [Ideal.map_span, Set.image_singleton, map_natCast]
-- 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
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))
⊢ 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))
have 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))
Tactic: rwa [Ideal.map_span, Set.image_singleton, map_natCast]
-- 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
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
⊢ 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))
have 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))
Tactic: suffices h : Function.Surjective (Ideal.Quotient.mk 𝔭 ∘ fontaineTheta R p) by
    rwa [Ideal.map_span, Set.image_singleton, map_natCast]
-- 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
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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Perfectoid.FontaineTheta (hypothesis)
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
⊢ Function.Surjective (α := 𝕎 R♭) (β := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
have 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)
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]
-- 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
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 (α := 𝕎 R♭) (β := HasQuotient.Quotient R (B := Ideal R) 𝔭)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk 𝔭) : (a : R) → R ⧸ 𝔭) (⇑(fontaineTheta R p) : (a : 𝕎 R♭) → R))
have 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)
Tactic: rw [this]
-- 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
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.{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)
have hg : Function.Surjective (β := HasQuotient.Quotient R (B := Ideal R) 𝔭) fun (x : R♭) ↦
  (PreTilt.coeff 0 : (a : R♭) → ModP R p) x
Tactic: apply Function.Surjective.comp