awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
S' : Type u_4
T' : Type u_5
inst_3 : CommRing S'
inst_4 : CommRing T'
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R S'
inst_8 : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
h :
  Eq (α := S ⊗[R] T →ₐ[R] S' ⊗[R] T') (Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] S' ⊗[R] T')
    (AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : S ⊗[R] T' →ₐ[R] S' ⊗[R] T')
        (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : T' ⊗[R] S →ₐ[R] S ⊗[R] T')
            (AlgHom.comp (Algebra.TensorProduct.map g (AlgHom.id R S) : T ⊗[R] S →ₐ[R] T' ⊗[R] S)
              ((↑(Algebra.TensorProduct.comm R S T) : S ⊗[R] T →ₐ[R] T ⊗[R] S) : S ⊗[R] T →ₐ[R] T ⊗[R] S)) :
          S ⊗[R] T →ₐ[R] S ⊗[R] T') :
      S ⊗[R] T →ₐ[R] S' ⊗[R] T')
⊢ Eq (α := S ⊗[R] T →+* S' ⊗[R] T')
    (↑(Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] S' ⊗[R] T') : S ⊗[R] T →+* S' ⊗[R] T')
    (↑(AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : S ⊗[R] T' →ₐ[R] S' ⊗[R] T')
            (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : T' ⊗[R] S →ₐ[R] S ⊗[R] T')
                (AlgHom.comp (Algebra.TensorProduct.map g (AlgHom.id R S) : T ⊗[R] S →ₐ[R] T' ⊗[R] S)
                  ((↑(Algebra.TensorProduct.comm R S T) : S ⊗[R] T →ₐ[R] T ⊗[R] S) : S ⊗[R] T →ₐ[R] T ⊗[R] S)) :
              S ⊗[R] T →ₐ[R] S ⊗[R] T') :
          S ⊗[R] T →ₐ[R] S' ⊗[R] T') :
      S ⊗[R] T →+* S' ⊗[R] T')

Tactic:
congr
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
S' : Type u_4
T' : Type u_5
inst_3 : CommRing S'
inst_4 : CommRing T'
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R S'
inst_8 : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
h :
  ∀ (x : S),
    Eq (α := S' ⊗[R] T')
      (((AlgHom.comp (B := S ⊗[R] T) (Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] S' ⊗[R] T')
                (Algebra.TensorProduct.includeLeft : S →ₐ[R] S ⊗[R] T) :
              S →ₐ[R] S' ⊗[R] T') :
            (a : S) → S' ⊗[R] T')
          x :
        S' ⊗[R] T')
      (((AlgHom.comp
                (AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : S ⊗[R] T' →ₐ[R] S' ⊗[R] T')
                  (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : T' ⊗[R] S →ₐ[R] S ⊗[R] T')
                      (AlgHom.comp (Algebra.TensorProduct.map g (AlgHom.id R S) : T ⊗[R] S →ₐ[R] T' ⊗[R] S)
                        ((↑(Algebra.TensorProduct.comm R S T) : S ⊗[R] T →ₐ[R] T ⊗[R] S) : S ⊗[R] T →ₐ[R] T ⊗[R] S)) :
                    S ⊗[R] T →ₐ[R] S ⊗[R] T'))
                Algebra.TensorProduct.includeLeft :
              S →ₐ[R] S' ⊗[R] T') :
            (a : S) → S' ⊗[R] T')
          x :
        S' ⊗[R] T')
h₁ :
  ∀ (x : T),
    Eq (α := S' ⊗[R] T')
      ((AlgHom.comp (B := S ⊗[R] T)
              (AlgHom.restrictScalars R (Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] S' ⊗[R] T'))
              Algebra.TensorProduct.includeRight :
            (a : T) → S' ⊗[R] T')
          x :
        S' ⊗[R] T')
      ((AlgHom.comp
              (AlgHom.restrictScalars R
                (AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : S ⊗[R] T' →ₐ[R] S' ⊗[R] T')
                    (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : T' ⊗[R] S →ₐ[R] S ⊗[R] T')
                        (AlgHom.comp (Algebra.TensorProduct.map g (AlgHom.id R S) : T ⊗[R] S →ₐ[R] T' ⊗[R] S)
                          ((↑(Algebra.TensorProduct.comm R S T) : S ⊗[R] T →ₐ[R] T ⊗[R] S) : S ⊗[R] T →ₐ[R] T ⊗[R] S)) :
                      S ⊗[R] T →ₐ[R] S ⊗[R] T') :
                  S ⊗[R] T →ₐ[R] S' ⊗[R] T'))
              Algebra.TensorProduct.includeRight :
            (a : T) → S' ⊗[R] T')
          x :
        S' ⊗[R] T')
⊢ Eq (α := S ⊗[R] T →ₐ[R] S' ⊗[R] T') (Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] S' ⊗[R] T')
    (AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : S ⊗[R] T' →ₐ[R] S' ⊗[R] T')
        (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : T' ⊗[R] S →ₐ[R] S ⊗[R] T')
            (AlgHom.comp (Algebra.TensorProduct.map g (AlgHom.id R S) : T ⊗[R] S →ₐ[R] T' ⊗[R] S)
              ((↑(Algebra.TensorProduct.comm R S T) : S ⊗[R] T →ₐ[R] T ⊗[R] S) : S ⊗[R] T →ₐ[R] T ⊗[R] S)) :
          S ⊗[R] T →ₐ[R] S ⊗[R] T') :
      S ⊗[R] T →ₐ[R] S' ⊗[R] T')

Tactic:
ext
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
S' : Type u_4
T' : Type u_5
inst_3 : CommRing S'
inst_4 : CommRing T'
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R S'
inst_8 : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
x : S
⊢ Eq (α := S' ⊗[R] T')
    (((AlgHom.comp (B := S ⊗[R] T) (Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] S' ⊗[R] T')
              (Algebra.TensorProduct.includeLeft : S →ₐ[R] S ⊗[R] T) :
            S →ₐ[R] S' ⊗[R] T') :
          (a : S) → S' ⊗[R] T')
        x :
      S' ⊗[R] T')
    (((AlgHom.comp
              (AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : S ⊗[R] T' →ₐ[R] S' ⊗[R] T')
                (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : T' ⊗[R] S →ₐ[R] S ⊗[R] T')
                    (AlgHom.comp (Algebra.TensorProduct.map g (AlgHom.id R S) : T ⊗[R] S →ₐ[R] T' ⊗[R] S)
                      ((↑(Algebra.TensorProduct.comm R S T) : S ⊗[R] T →ₐ[R] T ⊗[R] S) : S ⊗[R] T →ₐ[R] T ⊗[R] S)) :
                  S ⊗[R] T →ₐ[R] S ⊗[R] T'))
              Algebra.TensorProduct.includeLeft :
            S →ₐ[R] S' ⊗[R] T') :
          (a : S) → S' ⊗[R] T')
        x :
      S' ⊗[R] T')

Tactic:
simp
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
S' : Type u_4
T' : Type u_5
inst_3 : CommRing S'
inst_4 : CommRing T'
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R S'
inst_8 : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
x : T
⊢ Eq (α := S' ⊗[R] T')
    ((AlgHom.comp (B := S ⊗[R] T) (AlgHom.restrictScalars R (Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] S' ⊗[R] T'))
            Algebra.TensorProduct.includeRight :
          (a : T) → S' ⊗[R] T')
        x :
      S' ⊗[R] T')
    ((AlgHom.comp
            (AlgHom.restrictScalars R
              (AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : S ⊗[R] T' →ₐ[R] S' ⊗[R] T')
                  (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : T' ⊗[R] S →ₐ[R] S ⊗[R] T')
                      (AlgHom.comp (Algebra.TensorProduct.map g (AlgHom.id R S) : T ⊗[R] S →ₐ[R] T' ⊗[R] S)
                        ((↑(Algebra.TensorProduct.comm R S T) : S ⊗[R] T →ₐ[R] T ⊗[R] S) : S ⊗[R] T →ₐ[R] T ⊗[R] S)) :
                    S ⊗[R] T →ₐ[R] S ⊗[R] T') :
                S ⊗[R] T →ₐ[R] S' ⊗[R] T'))
            Algebra.TensorProduct.includeRight :
          (a : T) → S' ⊗[R] T')
        x :
      S' ⊗[R] T')

Tactic:
simp
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing S
inst_3 : IsLocalHom (R := R) (S := S) f
⊢ f.SurjectiveOnStalks ↔ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
⟨fun H x ↦ ?_, fun h ↦ surjectiveOnStalks_of_surjective h⟩

Premises used: RingHom.surjectiveOnStalks_of_surjective, Iff.intro
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing S
inst_3 : IsLocalHom (R := R) (S := S) f
refine : ∀ (H : f.SurjectiveOnStalks) (x : S), ∃ (a : R), (f : (a : R) → S) a = x
⊢ f.SurjectiveOnStalks ↔ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
refine ⟨fun H x ↦ ?_, fun h ↦ surjectiveOnStalks_of_surjective h⟩
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing S
inst_3 : IsLocalHom (R := R) (S := S) f
H : f.SurjectiveOnStalks
x : S
obtain :
  ∀ (y r : R) (c : S) (hc : c ∉ IsLocalRing.maximalIdeal S)
    (hr : ((f : (a : R) → S) r : S) ∉ IsLocalRing.maximalIdeal S)
    (e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * x = HMul.hMul (β := S) c ((f : (a : R) → S) y : S)),
    ∃ (a : R), (f : (a : R) → S) a = x
⊢ ∃ (a : R), (f : (a : R) → S) a = x

Tactic:
obtain ⟨y, r, c, hc, hr, e⟩ :=
    (surjective_localRingHom_iff _).mp (H (IsLocalRing.maximalIdeal _) inferInstance) x

Premises used: IsLocalRing.maximalIdeal, inferInstance, Iff.mp, RingHom.surjective_localRingHom_iff
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing S
inst_3 : IsLocalHom (R := R) (S := S) f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
hc : c ∉ IsLocalRing.maximalIdeal S
hr : ((f : (a : R) → S) r : S) ∉ IsLocalRing.maximalIdeal S
e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * x = HMul.hMul (β := S) c ((f : (a : R) → S) y : S)
⊢ IsUnit c

Tactic:
simp only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, not_not] at hc hr

Premises used: Classical.not_not, mem_nonunits_iff, IsLocalRing.mem_maximalIdeal
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing S
inst_3 : IsLocalHom (R := R) (S := S) f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
hc : c ∉ IsLocalRing.maximalIdeal S
hr : ((f : (a : R) → S) r : S) ∉ IsLocalRing.maximalIdeal S
e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * x = HMul.hMul (β := S) c ((f : (a : R) → S) y : S)
hc₁ : IsUnit c
⊢ IsUnit.{u_2} (M := S) ((f : (a : R) → S) r : S)

Tactic:
simp only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, not_not] at hc hr

Premises used: Classical.not_not, mem_nonunits_iff, IsLocalRing.mem_maximalIdeal
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing S
inst_3 : IsLocalHom (R := R) (S := S) f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * x = HMul.hMul (β := S) c ((f : (a : R) → S) y : S)
hc : IsUnit c
hr : IsUnit.{u_2} (M := S) ((f : (a : R) → S) r : S)
⊢ ∃ (a : R), (f : (a : R) → S) a = x

Tactic:
⟨(isUnit_of_map_unit f r hr).unit⁻¹ * y, ?_⟩

Premises used: Units.val, HMul.hMul, isUnit_of_map_unit, Inv.inv, Exists.intro, IsUnit.unit
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing S
inst_3 : IsLocalHom (R := R) (S := S) f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * x = HMul.hMul (β := S) c ((f : (a : R) → S) y : S)
hc : IsUnit c
hr : IsUnit.{u_2} (M := S) ((f : (a : R) → S) r : S)
refine : (f : (a : R) → S) ((↑(IsUnit.unit ⋯)⁻¹ : R) * y) = x
⊢ ∃ (a : R), (f : (a : R) → S) a = x

Tactic:
refine ⟨(isUnit_of_map_unit f r hr).unit⁻¹ * y, ?_⟩
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing S
inst_3 : IsLocalHom (R := R) (S := S) f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * x = HMul.hMul (β := S) c ((f : (a : R) → S) y : S)
hc : IsUnit c
hr : IsUnit.{u_2} (M := S) ((f : (a : R) → S) r : S)
a :
  Eq.{u_2 + 1} (α := S)
    ((fun (x : S) ↦ HMul.hMul (α := S) ((f : (a : R) → S) r : S) x) ((f : (a : R) → S) ((↑(IsUnit.unit ⋯)⁻¹ : R) * y)))
    ((fun (x : S) ↦ HMul.hMul (α := S) ((f : (a : R) → S) r : S) x) x)
⊢ (f : (a : R) → S) ((↑(IsUnit.unit ⋯)⁻¹ : R) * y) = x

Tactic:
apply hr.mul_right_injective

Premises used: IsUnit.mul_right_injective
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing S
inst_3 : IsLocalHom (R := R) (S := S) f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * x = HMul.hMul (β := S) c ((f : (a : R) → S) y : S)
hc : IsUnit c
hr : IsUnit.{u_2} (M := S) ((f : (a : R) → S) r : S)
a :
  Eq.{u_2 + 1} (α := S)
    ((fun (x : S) ↦ c * x)
      ((fun (x : S) ↦ HMul.hMul (α := S) ((f : (a : R) → S) r : S) x)
        ((f : (a : R) → S) ((↑(IsUnit.unit ⋯)⁻¹ : R) * y))))
    ((fun (x : S) ↦ c * x) ((fun (x : S) ↦ HMul.hMul (α := S) ((f : (a : R) → S) r : S) x) x))
⊢ Eq.{u_2 + 1} (α := S)
    ((fun (x : S) ↦ HMul.hMul (α := S) ((f : (a : R) → S) r : S) x) ((f : (a : R) → S) ((↑(IsUnit.unit ⋯)⁻¹ : R) * y)))
    ((fun (x : S) ↦ HMul.hMul (α := S) ((f : (a : R) → S) r : S) x) x)

Tactic:
apply hc.mul_right_injective

Premises used: IsUnit.mul_right_injective
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing S
inst_3 : IsLocalHom (R := R) (S := S) f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * x = HMul.hMul (β := S) c ((f : (a : R) → S) y : S)
hc : IsUnit c
hr : IsUnit.{u_2} (M := S) ((f : (a : R) → S) r : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((fun (x : S) ↦ c * x)
      ((fun (x : S) ↦ HMul.hMul (α := S) ((f : (a : R) → S) r : S) x)
        ((f : (a : R) → S) ((↑(IsUnit.unit ⋯)⁻¹ : R) * y))))
    ((fun (x : S) ↦ c * x) ((fun (x : S) ↦ HMul.hMul (α := S) ((f : (a : R) → S) r : S) x) x))

Tactic:
simp only [← map_mul, ← mul_assoc, IsUnit.mul_val_inv, one_mul, e]

Premises used: IsUnit.mul_val_inv, mul_assoc, map_mul, one_mul
-- 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
x : Perfection (R ⧸ I) p
m : ℕ
zero : SModEq (R := R) (HPow.hPow (β := ℕ) I 0) (x.teichmullerAux 0) (x.teichmullerAux (HAdd.hAdd (α := ℕ) 0 1))
succ : ∀ (m : ℕ), SModEq (R := R) (I ^ (m + 1)) (x.teichmullerAux (m + 1)) (x.teichmullerAux (m + 1 + 1))
⊢ SModEq (R := R) (I ^ m) (x.teichmullerAux m) (x.teichmullerAux (m + 1))

Tactic:
obtain _ | m := m
-- 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
x : Perfection (R ⧸ I) p
⊢ SModEq (R := R) (HPow.hPow (β := ℕ) I 0) (x.teichmullerAux 0) (x.teichmullerAux (HAdd.hAdd (α := ℕ) 0 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
x : Perfection (R ⧸ I) p
m : ℕ
succ : SModEq (R := R) (I ^ (m + 1)) (x.teichmullerAux (m + 1 + 1)) (x.teichmullerAux (m + 1))
⊢ SModEq (R := R) (I ^ (m + 1)) (x.teichmullerAux (m + 1)) (x.teichmullerAux (m + 1 + 1))

Tactic:
symm
-- 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
x : Perfection (R ⧸ I) p
m : ℕ
succ :
  SModEq (R := R) (I ^ (m + 1))
    (HPow.hPow (α := R)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p (m + 1) : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
        p ^
      p ^ m)
    (x.teichmullerAux (m + 1))
⊢ SModEq (R := R) (I ^ (m + 1)) (x.teichmullerAux (m + 1 + 1)) (x.teichmullerAux (m + 1))

Tactic:
rw [teichmullerAux, pow_succ' p, pow_mul]

Premises used: Perfection.teichmullerAux, pow_mul, pow_succ'
-- 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
x : Perfection (R ⧸ I) p
m : ℕ
⊢ SModEq (R := R) I
    (HPow.hPow (α := R)
      (Quotient.out (s := Submodule.quotientRel (R := R) I)
        ((coeff (R ⧸ I) p (m + 1) : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
      p)
    (Quotient.out (s := Submodule.quotientRel (R := R) I) ((coeff (R ⧸ I) p m : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))

Tactic:
simp [SModEq.idealQuotientMk, coeff_pow_p']

Premises used: SModEq.idealQuotientMk, Perfection.coeff_pow_p'
-- 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
x : Perfection (R ⧸ I) p
m : ℕ
⊢ SModEq (R := R) (I ^ (m + 1))
    (HPow.hPow (α := R)
        (Quotient.out (s := Submodule.quotientRel (R := R) I)
          ((coeff (R ⧸ I) p (m + 1) : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
        p ^
      p ^ m)
    (x.teichmullerAux (m + 1))

Tactic:
exact .pow_pow_add_one (I.natCast_mem_of_charP_quotient p) (m := m) <| by
    simp [SModEq.idealQuotientMk, coeff_pow_p']
-- 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
x : Perfection (R ⧸ I) p
⊢ ∀ (n : ℕ),
    SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (x.teichmullerAux n) (x.teichmullerAux (n + 1))

Tactic:
simpa using teichmullerAux_sModEq x

Premises used: Perfection.teichmullerAux_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 : IsPrecomplete I R
x : Perfection (R ⧸ I) p
⊢ ∃ (y : R), ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) (x.teichmullerAux n) y

Tactic:
IsPrecomplete.prec' _ (teichmullerCauchy x).2

Premises used: Set.Mem, Perfection.teichmullerCauchy, IsPrecomplete.prec', Subtype.property
-- 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 : IsPrecomplete 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) (HSMul.hSMul (β := Ideal R) (I ^ (n + 1)) ⊤) (x.teichmullerAux (n + 1))
    (Exists.choose (p := fun (y : R) ↦
      ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) (x.teichmullerAux n) y) ⋯)

Tactic:
have := (exists_teichmullerFun x).choose_spec (n + 1)
-- 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 : IsPrecomplete 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)
this :
  SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ (n + 1)) ⊤) (x.teichmullerAux (n + 1))
    (Exists.choose (p := fun (y : R) ↦
      ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) (x.teichmullerAux n) y) ⋯)
⊢ SModEq (R := R) (I ^ (n + 1)) (x.teichmullerAux (n + 1))
    (Exists.choose (p := fun (y : R) ↦
      ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) (x.teichmullerAux n) y) ⋯)

Tactic:
rw [smul_eq_mul, Ideal.mul_top] at this

Premises used: smul_eq_mul, Ideal.mul_top
-- 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 : IsPrecomplete 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)
this :
  SModEq (R := R) (I ^ (n + 1)) (x.teichmullerAux (n + 1))
    (Exists.choose (p := fun (y : R) ↦
      ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) (x.teichmullerAux n) y) ⋯)
⊢ SModEq (R := R) I
    (Quotient.out (s := Submodule.quotientRel (R := R) I) ((coeff (R ⧸ I) p n : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
    y

Tactic:
simp [SModEq.idealQuotientMk, h]

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 : IsPrecomplete 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)
this :
  SModEq (R := R) (I ^ (n + 1)) (x.teichmullerAux (n + 1))
    (Exists.choose (p := fun (y : R) ↦
      ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) (x.teichmullerAux n) y) ⋯)
⊢ SModEq (R := R) (I ^ (n + 1)) x.teichmullerFun (y ^ p ^ n)

Tactic:
exact this.symm.trans <| .pow_pow_add_one (I.natCast_mem_of_charP_quotient p) (m := n) <| by
    simp [SModEq.idealQuotientMk, h]

Premises used: SModEq.symm, 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 : ℕ),
    ∀ 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
obtain :
  ∀ (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),
    x.teichmullerFun = y
⊢ x.teichmullerFun = y

Tactic:
obtain ⟨N, h⟩ := h
-- 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
⊢ x.teichmullerFun = y

Tactic:
(IsHausdorff.eq_iff_smodEq (I := I)).mpr fun n ↦ ?_

Premises used: Iff.mpr, IsHausdorff.eq_iff_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 : 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
refine : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) x.teichmullerFun y
⊢ x.teichmullerFun = y

Tactic:
refine (IsHausdorff.eq_iff_smodEq (I := I)).mpr fun n ↦ ?_

Premises used: Iff.mpr, IsHausdorff.eq_iff_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 : 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 : ℕ
rw : SModEq (R := R) (I ^ n) x.teichmullerFun y
⊢ SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) x.teichmullerFun y

Tactic:
rw [smul_eq_mul, Ideal.mul_top]

Premises used: smul_eq_mul, Ideal.mul_top