awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
rw :
  Submodule.Quotient.mk ((↑r : ℕ → R) n • (↑x : ℕ → M) n) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
rw₁ :
  HSMul.hSMul (α := R ⧸ I ^ m) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) n) : R ⧸ I ^ m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
rw₂ :
  HSMul.hSMul (α := R ⧸ I ^ m) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) n) : R ⧸ I ^ m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
rw₃ :
  HSMul.hSMul (α := R ⧸ I ^ m) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) m) : R ⧸ I ^ m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
⊢ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) n)
      (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
have rw₄ : Submodule.Quotient.mk ((↑r : ℕ → R) m • (↑x : ℕ → M) m) =
  HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
Tactic: rw [← Submodule.Quotient.mk_smul, ← Module.Quotient.mk_smul_mk,
    AdicCauchySequence.mk_eq_mk hmn, Ideal.mk_eq_mk I hmn, Module.Quotient.mk_smul_mk,
    Submodule.Quotient.mk_smul]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
rw :
  Submodule.Quotient.mk ((↑r : ℕ → R) n • (↑x : ℕ → M) n) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
rw₁ :
  HSMul.hSMul (α := R ⧸ I ^ m) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) n) : R ⧸ I ^ m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
rw₂ :
  HSMul.hSMul (α := R ⧸ I ^ m) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) n) : R ⧸ I ^ m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
rw₃ :
  HSMul.hSMul (α := R ⧸ I ^ m) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) m) : R ⧸ I ^ m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
rw₄ :
  Submodule.Quotient.mk ((↑r : ℕ → R) m • (↑x : ℕ → M) m) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
⊢ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) n)
      (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
have rw₅ : HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
  HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
Tactic: rw [← Submodule.Quotient.mk_smul, ← Module.Quotient.mk_smul_mk,
    AdicCauchySequence.mk_eq_mk hmn, Ideal.mk_eq_mk I hmn, Module.Quotient.mk_smul_mk,
    Submodule.Quotient.mk_smul]
-- 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 ⧸ HSMul.hSMul (β := Ideal R) I ⊤
x : M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤
b₁ b₂ : R
h : b₁ ≈ b₂
⊢ Eq.{u_3 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) ((fun (x_1 : R) ↦ x_1 • x) b₁)
    ((fun (x_1 : R) ↦ x_1 • x) b₂)
have h₁ : ∀ (a : M),
  Eq.{u_3 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
    ((fun (x : R) ↦ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) x (Quotient.mk'' a)) b₁)
    ((fun (x : R) ↦ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) x (Quotient.mk'' a)) b₂)
Tactic: induction x using Quotient.inductionOn'
Cleared hypotheses: 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
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
r : R ⧸ HSMul.hSMul (β := Ideal R) I ⊤
b₁ b₂ : R
h : b₁ ≈ b₂
a : M
⊢ b₁ - b₂ ∈ I
have rwa : b₁ - b₂ ∈ HSMul.hSMul (β := Ideal R) I ⊤
Tactic: rwa [show I = I • ⊤ by simp, ← Submodule.quotientRel_def]
-- 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 ⧸ HSMul.hSMul (β := Ideal R) I ⊤
b₁ b₂ : R
h : b₁ ≈ b₂
a : M
rwa : b₁ - b₂ ∈ HSMul.hSMul (β := Ideal R) I ⊤
⊢ b₁ - b₂ ∈ I
have rwa₁ : (quotientRel (I • ⊤) : R → R → Prop) b₁ b₂
Tactic: rwa [show I = I • ⊤ by simp, ← Submodule.quotientRel_def]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (hypothesis)
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 ⧸ HSMul.hSMul (β := Ideal R) I ⊤
b₁ b₂ : R
h : b₁ ≈ b₂
a : M
⊢ Eq.{u_3 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
    ((fun (x : R) ↦ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) x (Quotient.mk'' a)) b₁)
    ((fun (x : R) ↦ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) x (Quotient.mk'' a)) b₂)
have h₁ : b₁ - b₂ ∈ I
Tactic: have h : b₁ - b₂ ∈ (I : Submodule R R) := by
        rwa [show I = I • ⊤ by simp, ← Submodule.quotientRel_def]
-- 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 ⧸ HSMul.hSMul (β := Ideal R) I ⊤
b₁ b₂ : R
h_1 : b₁ ≈ b₂
a : M
h : b₁ - b₂ ∈ I
⊢ Eq.{u_3 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
    ((fun (x : R) ↦ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) x (Quotient.mk'' a)) b₁)
    ((fun (x : R) ↦ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) x (Quotient.mk'' a)) b₂)
have h₁ : (b₁ - b₂) • a ∈ HSMul.hSMul (β := Submodule R M) I ⊤
Tactic: rw [← sub_eq_zero, ← sub_smul, Submodule.Quotient.mk''_eq_mk,
        ← Submodule.Quotient.mk_smul, Submodule.Quotient.mk_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
r : AdicCompletion I R
x : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
⊢ (↑r : (n : ℕ) → R ⧸ I ^ n • ⊤) n • x =
    HSMul.hSMul (α := R ⧸ I ^ n) ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) r : R ⧸ I ^ n) x
have h : ∀ (f : AdicCauchySequence I R),
  HSMul.hSMul.{u_1, u_3, u_3} (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
      ((↑((mk I R : (a : AdicCauchySequence I R) → AdicCompletion I R) f) : (n : ℕ) → R ⧸ I ^ n • ⊤) n) x =
    HSMul.hSMul (α := R ⧸ I ^ n)
      ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n)
          ((mk I R : (a : AdicCauchySequence I R) → AdicCompletion I R) f) :
        R ⧸ I ^ n)
      x
Tactic: induction r using induction_on
Cleared hypotheses: r
-- 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 : R ⧸ HSMul.hSMul (β := Ideal R) I ⊤
x : M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤
⊢ (r • s) • x = r • s • x
have h : ∀ (s : R) (x : M),
  HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
      (HSMul.hSMul (β := R ⧸ HSMul.hSMul (β := Ideal R) I ⊤) r (Quotient.mk'' s)) (Quotient.mk'' x) =
    r •
      HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Ideal R) I ⊤) (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
        (Quotient.mk'' s) (Quotient.mk'' x)
Tactic: induction s, x using Quotient.inductionOn₂' with | _ s x
Cleared hypotheses: s, 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
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
r s : R
x : M
⊢ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
      (HSMul.hSMul (β := R ⧸ HSMul.hSMul (β := Ideal R) I ⊤) r (Submodule.Quotient.mk s)) (Submodule.Quotient.mk x) =
    r •
      HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Ideal R) I ⊤) (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
        (Submodule.Quotient.mk s) (Submodule.Quotient.mk x)
have h : r • HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) s (Submodule.Quotient.mk x) =
  r •
    HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Ideal R) I ⊤) (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
      (Submodule.Quotient.mk s) (Submodule.Quotient.mk x)
Tactic: rw [← Submodule.Quotient.mk_smul, Ideal.Quotient.mk_eq_mk, mk_smul_mk, 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 : AdicCompletion I R
x : AdicCompletion I M
m n : ℕ
hmn : m ≤ n
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤)
      ((fun (n : ℕ) ↦
          HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β :=
            M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
            ((eval I R n : (a : AdicCompletion I R) → R ⧸ I ^ n • ⊤) r : R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
            ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤) x :
              M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
        n))
    ((fun (n : ℕ) ↦
        HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β :=
          M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
          ((eval I R n : (a : AdicCompletion I R) → R ⧸ I ^ n • ⊤) r : R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
          ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤) x : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      m)
have apply : ∀ (r : AdicCauchySequence I R),
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤)
      ((fun (n : ℕ) ↦
          HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β :=
            M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
            ((eval I R n : (a : AdicCompletion I R) → R ⧸ I ^ n • ⊤)
                ((mk I R : (a : AdicCauchySequence I R) → AdicCompletion I R) r) :
              R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
            ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤) x :
              M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
        n))
    ((fun (n : ℕ) ↦
        HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β :=
          M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
          ((eval I R n : (a : AdicCompletion I R) → R ⧸ I ^ n • ⊤)
              ((mk I R : (a : AdicCauchySequence I R) → AdicCompletion I R) r) :
            R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
          ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤) x : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      m)
Tactic: apply induction_on I R r (fun r ↦ ?_)
-- 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_1 : AdicCompletion I R
x : AdicCompletion I M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤)
      ((fun (n : ℕ) ↦
          HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β :=
            M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
            ((eval I R n : (a : AdicCompletion I R) → R ⧸ I ^ n • ⊤)
                ((mk I R : (a : AdicCauchySequence I R) → AdicCompletion I R) r) :
              R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
            ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤) x :
              M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
        n))
    ((fun (n : ℕ) ↦
        HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β :=
          M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
          ((eval I R n : (a : AdicCompletion I R) → R ⧸ I ^ n • ⊤)
              ((mk I R : (a : AdicCauchySequence I R) → AdicCompletion I R) r) :
            R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
          ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤) x : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      m)
have apply : ∀ (x : AdicCauchySequence I M),
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤)
      ((fun (n : ℕ) ↦
          HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β :=
            M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
            ((eval I R n : (a : AdicCompletion I R) → R ⧸ I ^ n • ⊤)
                ((mk I R : (a : AdicCauchySequence I R) → AdicCompletion I R) r) :
              R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
            ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤)
                ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) x) :
              M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
        n))
    ((fun (n : ℕ) ↦
        HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β :=
          M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
          ((eval I R n : (a : AdicCompletion I R) → R ⧸ I ^ n • ⊤)
              ((mk I R : (a : AdicCauchySequence I R) → AdicCompletion I R) r) :
            R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
          ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤)
              ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) x) :
            M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      m)
Tactic: apply induction_on I M x (fun 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
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
r_1 : AdicCompletion I R
x_1 : AdicCompletion I M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤)
      ((fun (n : ℕ) ↦
          HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β :=
            M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
            ((eval I R n : (a : AdicCompletion I R) → R ⧸ I ^ n • ⊤)
                ((mk I R : (a : AdicCauchySequence I R) → AdicCompletion I R) r) :
              R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
            ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤)
                ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) x) :
              M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
        n))
    ((fun (n : ℕ) ↦
        HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β :=
          M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
          ((eval I R n : (a : AdicCompletion I R) → R ⧸ I ^ n • ⊤)
              ((mk I R : (a : AdicCauchySequence I R) → AdicCompletion I R) r) :
            R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
          ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤)
              ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) x) :
            M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      m)
have simp : HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) n)
    (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
  HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
Tactic: simp only [coe_eval, mapQ_eq_factor, mk_apply_coe, mkQ_apply, Ideal.Quotient.mk_eq_mk,
        mk_smul_mk, map_smul, mapQ_apply, LinearMap.id_coe, id_eq]
-- 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_1 : AdicCompletion I R
x_1 : AdicCompletion I M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
⊢ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) n)
      (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
have rw : HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
  HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
Tactic: rw [smul_mk I hmn]
-- 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 s : AdicCompletion I R
x : AdicCompletion I M
⊢ (r * s) • x = r • s • x
have h : ∀ (n : ℕ), (↑((r * s) • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
Tactic: ext n
-- 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
b : AdicCompletion I M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := AdicCompletion I R) 1 b = b
have h : ∀ (n : ℕ),
  (↑(HSMul.hSMul.{u_1, u_3, u_3} (α := AdicCompletion I R) 1 b) : (n : ℕ) → M ⧸ I ^ n • ⊤) n =
    (↑b : (n : ℕ) → M ⧸ I ^ n • ⊤) n
Tactic: ext n
-- 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 : AdicCompletion I R
⊢ HSMul.hSMul (β := AdicCompletion I M) r 0 = 0
have h : ∀ (n : ℕ), (↑(HSMul.hSMul (β := AdicCompletion I M) r 0) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n
Tactic: ext n
-- 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 : AdicCompletion I R
x y : AdicCompletion I M
⊢ r • (x + y) = r • x + r • y
have h : ∀ (n : ℕ), (↑(r • (x + y)) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • x + r • y) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
Tactic: ext n
-- 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 s : AdicCompletion I R
x : AdicCompletion I M
⊢ (r + s) • x = r • x + s • x
have h : ∀ (n : ℕ), (↑((r + s) • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • x + s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
Tactic: ext n
-- 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
x : AdicCompletion I M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := AdicCompletion I R) 0 x = 0
have h : ∀ (n : ℕ),
  (↑(HSMul.hSMul.{u_1, u_3, u_3} (α := AdicCompletion I R) 0 x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n =
    (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n
Tactic: ext n
-- 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
⊢ (r • s) • x = r • s • x
have h : ∀ (n : ℕ), (↑((r • s) • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
Tactic: ext n
-- 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 : ℕ
⊢ (↑((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
⊢ (↑((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]