awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
r : R
s : AdicCompletion I R
x : AdicCompletion I M
n : ℕ
h :
  (↑(r • s) : (n : ℕ) → R ⧸ I ^ n • ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
h₁ :
  (r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n) • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ (↑((r • s) • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
have h₂ : (r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n) • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = r • (↑(s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
Tactic: rw [smul_eval, val_smul_apply, val_smul_apply, smul_eval, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
r : R
s : AdicCompletion I R
x : AdicCompletion I M
n : ℕ
h :
  (↑(r • s) : (n : ℕ) → R ⧸ I ^ n • ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
h₁ :
  (r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n) • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
h₂ :
  (r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n) • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = r • (↑(s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ (↑((r • s) • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
have h₃ : (r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n) • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n =
  r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n
Tactic: rw [smul_eval, val_smul_apply, val_smul_apply, smul_eval, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
r : R
s : AdicCompletion I R
x : AdicCompletion I M
n : ℕ
h :
  (↑(r • s) : (n : ℕ) → R ⧸ I ^ n • ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
h₁ :
  (r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n) • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
h₂ :
  (r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n) • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = r • (↑(s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
h₃ :
  (r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n) • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n =
    r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ (↑((r • s) • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
have h₄ : r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n =
  r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n
Tactic: rw [smul_eval, val_smul_apply, val_smul_apply, smul_eval, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R
inst_5 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
⊢ Eq.{u_5 + 1} (α := AdicCompletion I S)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) 1)) ⋯)
    1
have simp : Eq.{u_5 + 1} (α := AdicCompletion I S)
  (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
    ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
    (fun (n : ℕ) ↦ (factor sorry : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) 1) sorry)
  1
Tactic: simp only [map_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R
inst_5 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
⊢ Eq.{u_5 + 1} (α := AdicCompletion I S)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) 1) ⋯)
    1
have h : ∀ (n : ℕ),
  Eq.{u_5 + 1} (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
    ((↑(Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
              ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
              (fun (n : ℕ) ↦ (factor sorry : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) 1) sorry) :
          (n : ℕ) → S ⧸ I ^ n • ⊤)
        n :
      S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
    ((↑1 : (n : ℕ) → S ⧸ I ^ n • ⊤) n : S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R
inst_5 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
x y : R
⊢ Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) (x * y))) ⋯ =
    HMul.hMul (α := AdicCompletion I S)
      (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x)) ⋯)
      (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y)) ⋯)
have simp : Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
    ∀ {m n : ℕ} (hmn : m ≤ n), (Ideal.Quotient.factor sorry : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
    (fun (n : ℕ) ↦
      HMul.hMul (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) (β :=
        S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
        ((Ideal.Quotient.factor sorry : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x) :
          S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
        ((Ideal.Quotient.factor sorry : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y) :
          S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤))
    sorry =
  HMul.hMul (α := AdicCompletion I S)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (Ideal.Quotient.factor sorry : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (Ideal.Quotient.factor sorry : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x)) sorry)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (Ideal.Quotient.factor sorry : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (Ideal.Quotient.factor sorry : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y)) sorry)
Tactic: simp only [mapQ_eq_factor, factor_eq_factor, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R
inst_5 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
⊢ Eq.{u_5 + 1} (α := AdicCompletion I S)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) 0)) ⋯)
    0
have simp : Eq.{u_5 + 1} (α := AdicCompletion I S)
  (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
    ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
    (fun (n : ℕ) ↦ 0) sorry)
  0
Tactic: simp only [map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R
inst_5 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
⊢ Eq.{u_5 + 1} (α := AdicCompletion I S)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ 0) ⋯)
    0
have h : ∀ (n : ℕ),
  Eq.{u_5 + 1} (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
    ((↑(Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
              ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
              (fun (n : ℕ) ↦ 0) sorry) :
          (n : ℕ) → S ⧸ I ^ n • ⊤)
        n :
      S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
    ((↑0 : (n : ℕ) → S ⧸ I ^ n • ⊤) n : S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R
inst_5 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
x y : R
⊢ Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) (x + y))) ⋯ =
    HAdd.hAdd (α := AdicCompletion I S)
      (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x)) ⋯)
      (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y)) ⋯)
have simp : Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
    ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
    (fun (n : ℕ) ↦
      HAdd.hAdd (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) (β :=
        S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
        ((factor sorry : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x) :
          S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
        ((factor sorry : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y) :
          S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤))
    sorry =
  HAdd.hAdd (α := AdicCompletion I S)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor sorry : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x)) sorry)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor sorry : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y)) sorry)
Tactic: simp only [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
n : ℕ
x : R
⊢ Eq (α := S ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I S) → S ⧸ I ^ n) ((liftRingHom I f ⋯ : (a : R) → AdicCompletion I S) x) :
      S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)
have rw : Eq (α := S ⧸ I ^ n)
  ((factor sorry : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ n)
      ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤) ((liftRingHom I f sorry : (a : R) → AdicCompletion I S) x)) :
    S ⧸ I ^ n)
  ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)
Tactic: rw [← factor_eval_eq_evalₐ I _ (le_of_eq (Ideal.mul_top _))]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
n : ℕ
⊢ RingHom.comp (↑(evalₐ I n) : AdicCompletion I S →+* S ⧸ I ^ n) (liftRingHom I f ⋯) = f n
have a : ∀ (x : R),
  Eq.{u_5 + 1} (α := S ⧸ I ^ n)
    (((RingHom.comp (↑(evalₐ I n) : AdicCompletion I S →+* S ⧸ I ^ n) (liftRingHom I f sorry) :
            RingHom.{u_4, u_5} R (S ⧸ I ^ n)) :
          (a : R) → S ⧸ I ^ n)
        x :
      S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R_2 : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R_2
inst_5 : CommRing S
I : Ideal S
f_1 : (n : ℕ) → RingHom.{u_4, u_5} R_2 (S ⧸ I ^ n)
hf_1 : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f_1 n) = f_1 m
R : Type u_6
A : Type u_7
inst_6 : CommRing R
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
m n : ℕ
hle : m ≤ n
⊢ Eq (α := RingHom.{u_7, u_5} A (S ⧸ I ^ m))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factorPow I hle : S ⧸ I ^ n →+* S ⧸ I ^ m)
        ((fun (n : ℕ) ↦ (f n).toRingHom) n : RingHom.{u_7, u_5} A (S ⧸ I ^ n)) :
      RingHom.{u_7, u_5} A (S ⧸ I ^ m))
    ((fun (n : ℕ) ↦ (f n).toRingHom) m : RingHom.{u_7, u_5} A (S ⧸ I ^ m))
have a : ∀ (x : A),
  Eq.{u_5 + 1} (α := S ⧸ I ^ m)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factorPow I hle : S ⧸ I ^ n →+* S ⧸ I ^ m)
              ((fun (n : ℕ) ↦ (f n).toRingHom) n : RingHom.{u_7, u_5} A (S ⧸ I ^ n)) :
            RingHom.{u_7, u_5} A (S ⧸ I ^ m)) :
          (a : A) → S ⧸ I ^ m)
        x :
      S ⧸ I ^ m)
    ((((fun (n : ℕ) ↦ (f n).toRingHom) m : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : (a : A) → S ⧸ I ^ m) x : S ⧸ I ^ m)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R_2 : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R_2
inst_5 : CommRing S
I : Ideal S
f_1 : (n : ℕ) → RingHom.{u_4, u_5} R_2 (S ⧸ I ^ n)
hf_1 : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f_1 n) = f_1 m
R : Type u_6
A : Type u_7
inst_6 : CommRing R
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
r : R
n m n_1 : ℕ
hle : m ≤ n_1
⊢ Eq (α := RingHom.{u_7, u_5} A (S ⧸ I ^ m))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factorPow I hle : S ⧸ I ^ n_1 →+* S ⧸ I ^ m)
        ((↑(f n_1) : RingHom.{u_7, u_5} A (S ⧸ I ^ n_1)) : RingHom.{u_7, u_5} A (S ⧸ I ^ n_1)) :
      RingHom.{u_7, u_5} A (S ⧸ I ^ m))
    ((↑(f m) : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : RingHom.{u_7, u_5} A (S ⧸ I ^ m))
have a : ∀ (x : A),
  Eq.{u_5 + 1} (α := S ⧸ I ^ m)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factorPow I hle : S ⧸ I ^ n_1 →+* S ⧸ I ^ m)
              ((↑(f n_1) : RingHom.{u_7, u_5} A (S ⧸ I ^ n_1)) : RingHom.{u_7, u_5} A (S ⧸ I ^ n_1)) :
            RingHom.{u_7, u_5} A (S ⧸ I ^ m)) :
          (a : A) → S ⧸ I ^ m)
        x :
      S ⧸ I ^ m)
    ((((↑(f m) : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : (a : A) → S ⧸ I ^ m) x :
      S ⧸ I ^ m)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
R : Type u_6
A : Type u_7
inst_1 : CommRing R
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
n : ℕ
x : A
m n_1 : ℕ
hle : m ≤ n_1
⊢ RingHom.comp (Ideal.Quotient.factorPow I hle) (f n_1).toRingHom = (f m).toRingHom
have a : ∀ (x : A),
  Eq.{u_5 + 1} (α := S ⧸ I ^ m)
    (((RingHom.comp (Ideal.Quotient.factorPow I hle) (f n_1).toRingHom : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) :
          (a : A) → S ⧸ I ^ m)
        x :
      S ⧸ I ^ m)
    (((f m).toRingHom : (a : A) → S ⧸ I ^ m) x : S ⧸ I ^ m)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R
inst_5 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
inst_6 : IsAdicComplete I S
x x_1 : S
⊢ AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) (x * x_1) =
    HMul.hMul (α := AdicCompletion I S)
      (AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) x)
      (AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) x_1)
have h : ∀ (n : ℕ),
  (↑(AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) (x * x_1)) :
        (n : ℕ) → S ⧸ I ^ n • ⊤)
      n =
    (↑(HMul.hMul (α := AdicCompletion I S)
            (AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) x)
            (AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) x_1)) :
        (n : ℕ) → S ⧸ I ^ n • ⊤)
      n
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
inst_1 : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ Eq (α := S ⧸ HSMul.hSMul (β := Ideal S) (I ^ n) ⊤)
    ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal S) (I ^ n) ⊤) : (a : S) → S ⧸ I ^ n • ⊤)
        (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
      S ⧸ HSMul.hSMul (β := Ideal S) (I ^ n) ⊤)
    ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤) x : S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
have nth_rw : Eq (α := S ⧸ HSMul.hSMul (β := Ideal S) (I ^ n) ⊤)
  ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal S) (I ^ n) ⊤) : (a : S) → S ⧸ I ^ n • ⊤)
      (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
    S ⧸ HSMul.hSMul (β := Ideal S) (I ^ n) ⊤)
  ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤)
      ((of I S : (a : S) → AdicCompletion I S) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x)) :
    S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
Tactic: nth_rw 2 [← of_ofAlgEquiv_symm I x]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
inst_1 : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ Eq (α := S ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
      S ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I S) → S ⧸ I ^ n) x : S ⧸ I ^ n)
have simp : Eq (α := S ⧸ I ^ n)
  ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
    S ⧸ I ^ n)
  (((↑(Ideal.quotientEquivAlgOfEq S sorry) : S ⧸ I ^ n • ⊤ →ₐ[S] S ⧸ I ^ n) : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ n)
      ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤) x) :
    S ⧸ I ^ n)
Tactic: simp only [evalₐ, AlgHom.coe_comp, Function.comp_apply, AlgHom.ofLinearMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
inst_1 : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ Eq (α := S ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
      S ⧸ I ^ n)
    (((↑(Ideal.quotientEquivAlgOfEq S ⋯) : S ⧸ I ^ n • ⊤ →ₐ[S] S ⧸ I ^ n) : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ n)
        ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤) x) :
      S ⧸ I ^ n)
have rw : Eq (α := S ⧸ I ^ n)
  ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
    S ⧸ I ^ n)
  (((↑(Ideal.quotientEquivAlgOfEq S sorry) : S ⧸ I ^ n • ⊤ →ₐ[S] S ⧸ I ^ n) : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ n)
      ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal S) (I ^ n) ⊤) : (a : S) → S ⧸ I ^ n • ⊤)
        (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x)) :
    S ⧸ I ^ n)
Tactic: rw [← mk_smul_top_ofAlgEquiv_symm I n x]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
A : Type u_4
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := A) (⇑f : (a : S) → A)
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := AdicCompletion (RingHom.ker f) S) (β := A)
    (⇑(kerProj hf) : (a : AdicCompletion (RingHom.ker f) S) → A)
have dsimp : Function.Surjective.{u_2 + 1, u_4 + 1} (α := AdicCompletion (RingHom.ker f) S) (β := A)
  (Function.comp (β := HasQuotient.Quotient S (B := Ideal S) (RingHom.ker f))
    (⇑(Ideal.quotientKerAlgEquivOfSurjective hf) : (a : S ⧸ RingHom.ker f) → A)
    (⇑(evalOneₐ (RingHom.ker f)) : (a : AdicCompletion (RingHom.ker f) S) → S ⧸ RingHom.ker f))
Tactic: dsimp [kerProj]