awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
N : ℕ
h :
  ∀ n ≥ N,
    ∃ (z : R),
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I) ∧
        SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
n : ℕ
inl : ∀ (hn : n ≤ N), SModEq (R := R) (I ^ n) x.teichmullerFun y
inr : ∀ (hn : N ≤ n), SModEq (R := R) (I ^ n) x.teichmullerFun y
⊢ SModEq (R := R) (I ^ n) x.teichmullerFun y

Tactic:
obtain hn | hn := le_total n N

Premises used: le_total
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
N : ℕ
h :
  ∀ n ≥ N,
    ∃ (z : R),
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I) ∧
        SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
n : ℕ
hn : n ≤ N
inl :
  ∀ (z : R)
    (hz₁ :
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
        ((coeff (R ⧸ I) p N : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I))
    (hz₂ : SModEq (R := R) (I ^ (N + 1)) (z ^ p ^ N) y), SModEq (R := R) (I ^ n) x.teichmullerFun y
⊢ SModEq (R := R) (I ^ n) x.teichmullerFun y

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h N le_rfl

Premises used: le_rfl
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
N : ℕ
h :
  ∀ n ≥ N,
    ∃ (z : R),
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I) ∧
        SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
n : ℕ
hn : n ≤ N
z : R
hz₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
    ((coeff (R ⧸ I) p N : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I)
hz₂ : SModEq (R := R) (I ^ (N + 1)) (z ^ p ^ N) y
⊢ n ≤ N + 1

Tactic:
omega
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
N : ℕ
h :
  ∀ n ≥ N,
    ∃ (z : R),
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I) ∧
        SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
n : ℕ
hn : n ≤ N
z : R
hz₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
    ((coeff (R ⧸ I) p N : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I)
hz₂ : SModEq (R := R) (I ^ (N + 1)) (z ^ p ^ N) y
⊢ SModEq (R := R) (I ^ n) x.teichmullerFun y

Tactic:
exact ((teichmullerFun_sModEq hz₁).trans hz₂).mono <| Ideal.pow_le_pow_right (by omega)

Premises used: SModEq.mono, Perfection.teichmullerFun_sModEq, Ideal.pow_le_pow_right, SModEq.trans
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
N : ℕ
h :
  ∀ n ≥ N,
    ∃ (z : R),
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I) ∧
        SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
n : ℕ
hn : N ≤ n
inr :
  ∀ (z : R)
    (hz₁ :
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
        ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I))
    (hz₂ : SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y), SModEq (R := R) (I ^ n) x.teichmullerFun y
⊢ SModEq (R := R) (I ^ n) x.teichmullerFun y

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h n hn
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
N : ℕ
h :
  ∀ n ≥ N,
    ∃ (z : R),
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I) ∧
        SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
n : ℕ
hn : N ≤ n
z : R
hz₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
    ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I)
hz₂ : SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
⊢ n ≤ n + 1

Tactic:
omega
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
N : ℕ
h :
  ∀ n ≥ N,
    ∃ (z : R),
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I) ∧
        SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
n : ℕ
hn : N ≤ n
z : R
hz₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
    ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I)
hz₂ : SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
⊢ SModEq (R := R) (I ^ n) x.teichmullerFun y

Tactic:
exact ((teichmullerFun_sModEq hz₁).trans hz₂).mono <| Ideal.pow_le_pow_right (by omega)

Premises used: SModEq.mono, Perfection.teichmullerFun_sModEq, Ideal.pow_le_pow_right, SModEq.trans
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
h :
  ∀ (n : ℕ),
    ∃ (z : R),
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I) ∧
        SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
⊢ x.teichmullerFun = y

Tactic:
teichmullerFun_spec' ⟨0, fun n _ ↦ h n⟩

Premises used: Perfection.teichmullerFun_spec', Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : ℕ
⊢ Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) 1)
      ((coeff (R ⧸ I) p x : (a : Perfection (R ⧸ I) p) → R ⧸ I) 1) ∧
    SModEq (R := R) (I ^ (x + 1)) (HPow.hPow (α := R) 1 (p ^ x)) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
⊢ (x * y).teichmullerFun = x.teichmullerFun * y.teichmullerFun

Tactic:
teichmullerFun_spec fun n ↦ ?_

Premises used: Perfection.teichmullerFun_spec
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
refine :
  ∀ (n : ℕ),
    ∃ (z : R),
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) (x * y) : R ⧸ I) ∧
        SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) (x.teichmullerFun * y.teichmullerFun)
⊢ (x * y).teichmullerFun = x.teichmullerFun * y.teichmullerFun

Tactic:
refine teichmullerFun_spec fun n ↦ ?_

Premises used: Perfection.teichmullerFun_spec
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ Eq (α := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I)
        (HMul.hMul (α := R)
          (Quotient.out (s := Submodule.quotientRel (R := R) I)
            ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
          (Quotient.out (s := Submodule.quotientRel (R := R) I)
            ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) y))) :
      R ⧸ I)
    ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) (x * y) : R ⧸ I)

Tactic:
simp
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
refine :
  SModEq (R := R) (I ^ (n + 1))
    (HMul.hMul (α := R)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) y)) ^
      p ^ n)
    (x.teichmullerFun * y.teichmullerFun)
⊢ ∃ (z : R),
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
        ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) (x * y) : R ⧸ I) ∧
      SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) (x.teichmullerFun * y.teichmullerFun)

Tactic:
refine ⟨(coeff _ p n x).out * (coeff _ p n y).out, by simp, ?_⟩
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
rw :
  SModEq (R := R) (I ^ (n + 1))
    (HPow.hPow (α := R)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
        (p ^ n) *
      HPow.hPow (α := R)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) y))
        (p ^ n))
    (x.teichmullerFun * y.teichmullerFun)
⊢ SModEq (R := R) (I ^ (n + 1))
    (HMul.hMul (α := R)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) y)) ^
      p ^ n)
    (x.teichmullerFun * y.teichmullerFun)

Tactic:
rw [mul_pow]

Premises used: mul_pow
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ SModEq (R := R) (I ^ (n + 1))
    (HPow.hPow (α := R)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
        (p ^ n) *
      HPow.hPow (α := R)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) y))
        (p ^ n))
    (x.teichmullerFun * y.teichmullerFun)

Tactic:
(teichmullerFun_sModEq ?_).symm.mul (teichmullerFun_sModEq ?_).symm

Premises used: SModEq.mul, SModEq.symm, Perfection.teichmullerFun_sModEq
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
refine_1 :
  Eq (α := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x)) :
      R ⧸ I)
    ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I)
refine_2 :
  Eq (α := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) y)) :
      R ⧸ I)
    ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) y : R ⧸ I)
⊢ SModEq (R := R) (I ^ (n + 1))
    (HPow.hPow (α := R)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
        (p ^ n) *
      HPow.hPow (α := R)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) y))
        (p ^ n))
    (x.teichmullerFun * y.teichmullerFun)

Tactic:
refine (teichmullerFun_sModEq ?_).symm.mul (teichmullerFun_sModEq ?_).symm

Premises used: SModEq.mul, SModEq.symm, Perfection.teichmullerFun_sModEq
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ Eq (α := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x)) :
      R ⧸ I)
    ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I)

Tactic:
simp
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ Eq (α := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) y)) :
      R ⧸ I)
    ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) y : R ⧸ I)

Tactic:
simp
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
n : ℕ
h :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
    ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I)
⊢ SModEq (R := R) (I ^ (n + 1)) ((teichmuller p I : (a : Perfection (R ⧸ I) p) → R) x) (y ^ p ^ n)

Tactic:
teichmullerFun_sModEq h

Premises used: Perfection.teichmullerFun, Perfection.teichmullerFun_sModEq, Classical.choose
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
h :
  ∃ (N : ℕ),
    ∀ n ≥ N,
      ∃ (z : R),
        Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
            ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I) ∧
          SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
⊢ (teichmuller p I : (a : Perfection (R ⧸ I) p) → R) x = y

Tactic:
teichmullerFun_spec' h

Premises used: Perfection.teichmullerFun, Perfection.teichmullerFun_spec', Classical.choose
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
h :
  ∀ (n : ℕ),
    ∃ (z : R),
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I) ∧
        SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
⊢ (teichmuller p I : (a : Perfection (R ⧸ I) p) → R) x = y

Tactic:
teichmullerFun_spec h

Premises used: Perfection.teichmullerFun, Classical.choose, Perfection.teichmullerFun_spec
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
this : p ≠ 0
n : ℕ
⊢ Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) 0)
      ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) 0) ∧
    SModEq (R := R) (I ^ (n + 1)) (HPow.hPow (α := R) 0 (p ^ n)) 0

Tactic:
simp [zero_pow (pow_ne_zero n this)]

Premises used: pow_ne_zero, zero_pow
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
⊢ Eq (α := Perfection (R ⧸ I) p →* R) (teichmuller p I) (↑(teichmuller₀ p I) : Perfection (R ⧸ I) p →* R)

Tactic:
rfl

Premises used: Perfection.teichmullerFun, Perfection.teichmuller, Classical.choose, rfl
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
⊢ Eq (α := (a : Perfection (R ⧸ I) p) → R) (⇑(teichmuller p I) : (a : Perfection (R ⧸ I) p) → R)
    (⇑(teichmuller₀ p I) : (a : Perfection (R ⧸ I) p) → R)

Tactic:
rfl

Premises used: Perfection.teichmullerFun, Classical.choose, rfl
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
⊢ Eq (α := (x : Perfection (R ⧸ I) p) → R) teichmullerFun (⇑(teichmuller₀ p I) : (a : Perfection (R ⧸ I) p) → R)

Tactic:
rfl

Premises used: Perfection.teichmullerFun, Classical.choose, rfl
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
n : ℕ
h :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
    ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I)
⊢ SModEq (R := R) (I ^ (n + 1)) ((teichmuller₀ p I : (a : Perfection (R ⧸ I) p) → R) x) (y ^ p ^ n)

Tactic:
teichmullerFun_sModEq h

Premises used: Perfection.teichmullerFun, Perfection.teichmullerFun_sModEq, Classical.choose
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
h :
  ∃ (N : ℕ),
    ∀ n ≥ N,
      ∃ (z : R),
        Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
            ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I) ∧
          SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
⊢ (teichmuller₀ p I : (a : Perfection (R ⧸ I) p) → R) x = y

Tactic:
teichmullerFun_spec' h

Premises used: Perfection.teichmullerFun, Perfection.teichmullerFun_spec', Classical.choose
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
h :
  ∀ (n : ℕ),
    ∃ (z : R),
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) z : R ⧸ I)
          ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I) ∧
        SModEq (R := R) (I ^ (n + 1)) (z ^ p ^ n) y
⊢ (teichmuller₀ p I : (a : Perfection (R ⧸ I) p) → R) x = y

Tactic:
teichmullerFun_spec h

Premises used: Perfection.teichmullerFun, Classical.choose, Perfection.teichmullerFun_spec
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection R p
n : ℕ
⊢ Eq (α := R ⧸ I)
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) ((coeffMonoidHom R p n : (a : Perfection R p) → R) x) : R ⧸ I)
      ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I)
          ((mapMonoidHom p (↑(Ideal.Quotient.mk I) : R →* R ⧸ I) : (a : Perfection R p) → Perfection (R ⧸ I) p) x) :
        R ⧸ I) ∧
    SModEq (R := R) (I ^ (n + 1)) (HPow.hPow (α := R) ((coeffMonoidHom R p n : (a : Perfection R p) → R) x : R) (p ^ n))
      ((coeffMonoidHom R p 0 : (a : Perfection R p) → R) x)

Tactic:
simp
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
⊢ SModEq (R := R) (I ^ HAdd.hAdd (α := ℕ) 0 1) ((teichmuller p I : (a : Perfection (R ⧸ I) p) → R) x)
    (HPow.hPow (α := R)
      (Quotient.out (s := Submodule.quotientRel (R := R) I)
        ((coeff (R ⧸ I) p 0 : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
      (HPow.hPow (β := ℕ) p 0))

Tactic:
have := teichmuller_sModEq <| Ideal.Quotient.mk_out <| coeff _ p 0 x
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
this :
  SModEq (R := R) (I ^ HAdd.hAdd (α := ℕ) 0 1) ((teichmuller p I : (a : Perfection (R ⧸ I) p) → R) x)
    (HPow.hPow (α := R)
      (Quotient.out (s := Submodule.quotientRel (R := R) I)
        ((coeff (R ⧸ I) p 0 : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
      (HPow.hPow (β := ℕ) p 0))
⊢ SModEq (R := R) I ((teichmuller p I : (a : Perfection (R ⧸ I) p) → R) x)
    (HPow.hPow (α := R)
      (Quotient.out (s := Submodule.quotientRel (R := R) I)
        ((coeff (R ⧸ I) p 0 : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
      (HPow.hPow (β := ℕ) p 0))

Tactic:
simp_rw [zero_add, pow_one] at this

Premises used: zero_add, pow_one
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
this :
  SModEq (R := R) I ((teichmuller p I : (a : Perfection (R ⧸ I) p) → R) x)
    (HPow.hPow (α := R)
      (Quotient.out (s := Submodule.quotientRel (R := R) I)
        ((coeff (R ⧸ I) p 0 : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
      (HPow.hPow (β := ℕ) p 0))
⊢ Eq (α := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) ((teichmuller p I : (a : Perfection (R ⧸ I) p) → R) x) : R ⧸ I)
    ((coeff (R ⧸ I) p 0 : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I)

Tactic:
simpa [SModEq.idealQuotientMk] using this

Premises used: SModEq.idealQuotientMk
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
⊢ Eq (α := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) ((teichmuller₀ p I : (a : Perfection (R ⧸ I) p) → R) x) : R ⧸ I)
    ((coeff (R ⧸ I) p 0 : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I)

Tactic:
mk_teichmuller _

Premises used: Perfection.mk_teichmuller, Perfection.teichmullerFun, Classical.choose
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
⊢ Eq (α := Perfection (R ⧸ I) p →* R ⧸ I) (MonoidHom.comp (↑(Ideal.Quotient.mk I) : R →* R ⧸ I) (teichmuller p I))
    (↑(coeff (R ⧸ I) p 0) : Perfection (R ⧸ I) p →* R ⧸ I)

Tactic:
MonoidHom.ext mk_teichmuller

Premises used: Perfection.mk_teichmuller, MonoidHom.ext
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
⊢ Eq (α := Perfection (R ⧸ I) p →*₀ R ⧸ I)
    (MonoidWithZeroHom.comp (↑(Ideal.Quotient.mk I) : R →*₀ R ⧸ I) (teichmuller₀ p I))
    (↑(coeff (R ⧸ I) p 0) : Perfection (R ⧸ I) p →*₀ R ⧸ I)

Tactic:
MonoidWithZeroHom.ext mk_teichmuller

Premises used: MonoidWithZeroHom.ext, Perfection.mk_teichmuller
-- Module: Mathlib.RingTheory.Teichmuller
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
⊢ Eq (α := Perfection (R ⧸ I) p → R ⧸ I)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I)
      (⇑(teichmuller p I) : (a : Perfection (R ⧸ I) p) → R))
    (⇑(coeff (R ⧸ I) p 0) : (a : Perfection (R ⧸ I) p) → R ⧸ I)

Tactic:
funext mk_teichmuller

Premises used: Perfection.mk_teichmuller, funext