awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
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
⊢ 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')
have 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')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
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')
⊢ 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')
have 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')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
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)
have refine : ∀ (H : f.SurjectiveOnStalks) (x : S), ∃ (a : R), (f : (a : R) → S) a = x
Tactic: refine ⟨fun H x ↦ ?_, fun h ↦ surjectiveOnStalks_of_surjective h⟩
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
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
⊢ ∃ (a : R), (f : (a : R) → S) a = x
have 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
Tactic: obtain ⟨y, r, c, hc, hr, e⟩ :=
    (surjective_localRingHom_iff _).mp (H (IsLocalRing.maximalIdeal _) inferInstance) x
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (hypothesis)
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)
⊢ ∃ (a : R), (f : (a : R) → S) a = x
have hc₁ : IsUnit c
Tactic: simp only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, not_not] at hc hr
Cleared hypotheses: hc, hr
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (hypothesis)
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
⊢ ∃ (a : R), (f : (a : R) → S) a = x
have hr₁ : 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
Cleared hypotheses: hc, hr
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
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
have refine : (f : (a : R) → S) ((↑(IsUnit.unit sorry)⁻¹ : R) * y) = x
Tactic: refine ⟨(isUnit_of_map_unit f r hr).unit⁻¹ * y, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
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)
⊢ (f : (a : R) → S) ((↑(IsUnit.unit ⋯)⁻¹ : R) * y) = x
have 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 sorry)⁻¹ : R) * y)))
  ((fun (x : S) ↦ HMul.hMul (α := S) ((f : (a : R) → S) r : S) x) x)
Tactic: apply hr.mul_right_injective
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
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) ↦ 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)
have 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 sorry)⁻¹ : R) * y))))
  ((fun (x : S) ↦ c * x) ((fun (x : S) ↦ HMul.hMul (α := S) ((f : (a : R) → S) r : S) x) x))
Tactic: apply hc.mul_right_injective
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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) (x.teichmullerAux m) (x.teichmullerAux (m + 1))
have zero : SModEq (R := R) (HPow.hPow (β := ℕ) I 0) (x.teichmullerAux 0) (x.teichmullerAux (HAdd.hAdd (α := ℕ) 0 1))
Tactic: obtain _ | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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))
⊢ SModEq (R := R) (I ^ m) (x.teichmullerAux m) (x.teichmullerAux (m + 1))
have succ : ∀ (m : ℕ), SModEq (R := R) (I ^ (m + 1)) (x.teichmullerAux (m + 1)) (x.teichmullerAux (m + 1 + 1))
Tactic: obtain _ | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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)) (x.teichmullerAux (m + 1)) (x.teichmullerAux (m + 1 + 1))
have succ : SModEq (R := R) (I ^ (m + 1)) (x.teichmullerAux (m + 1 + 1)) (x.teichmullerAux (m + 1))
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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)) (x.teichmullerAux (m + 1 + 1)) (x.teichmullerAux (m + 1))
have 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))
Tactic: rw [teichmullerAux, pow_succ' p, pow_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (hypothesis)
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) (I ^ (n + 1)) x.teichmullerFun (y ^ p ^ n)
have 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) sorry)
Tactic: have := (exists_teichmullerFun x).choose_spec (n + 1)
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (hypothesis)
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.teichmullerFun (y ^ p ^ n)
have 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) sorry)
Tactic: rw [smul_eq_mul, Ideal.mul_top] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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
⊢ x.teichmullerFun = y
have 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
Tactic: obtain ⟨N, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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
have refine : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) x.teichmullerFun y
Tactic: refine (IsHausdorff.eq_iff_smodEq (I := I)).mpr fun n ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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 : ℕ
⊢ SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) x.teichmullerFun y
have rw : SModEq (R := R) (I ^ n) x.teichmullerFun y
Tactic: rw [smul_eq_mul, Ideal.mul_top]
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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 : ℕ
⊢ SModEq (R := R) (I ^ n) x.teichmullerFun y
have inl : ∀ (hn : n ≤ N), SModEq (R := R) (I ^ n) x.teichmullerFun y
Tactic: obtain hn | hn := le_total n N
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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
⊢ SModEq (R := R) (I ^ n) x.teichmullerFun y
have inr : ∀ (hn : N ≤ n), SModEq (R := R) (I ^ n) x.teichmullerFun y
Tactic: obtain hn | hn := le_total n N
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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
⊢ SModEq (R := R) (I ^ n) x.teichmullerFun y
have 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
Tactic: obtain ⟨z, hz₁, hz₂⟩ := h N le_rfl
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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
⊢ SModEq (R := R) (I ^ n) x.teichmullerFun y
have 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
Tactic: obtain ⟨z, hz₁, hz₂⟩ := h n hn
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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
have 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)
Tactic: refine teichmullerFun_spec fun n ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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 : ℕ
⊢ ∃ (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)
have 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)
Tactic: refine ⟨(coeff _ p n x).out * (coeff _ p n y).out, by simp, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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))
    (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)
have 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)
Tactic: rw [mul_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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)
have 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)
Tactic: refine (teichmullerFun_sModEq ?_).symm.mul (teichmullerFun_sModEq ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
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)
⊢ 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)
have 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)
Tactic: refine (teichmullerFun_sModEq ?_).symm.mul (teichmullerFun_sModEq ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (hypothesis)
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)
have 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))
Tactic: have := teichmuller_sModEq <| Ideal.Quotient.mk_out <| coeff _ p 0 x