awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
h : I ^ m = HSMul.hSMul (β := Ideal R) (I ^ m) ⊤
⊢ Eq (α := R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)
    (Submodule.Quotient.mk ((↑r : ℕ → R) n) : R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)
    (Submodule.Quotient.mk ((↑r : ℕ → R) m) : R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)

Tactic:
(r.property hmn).symm

Premises used: Set.Mem, SModEq.symm, SModEq, Subtype.property
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
h : I ^ m = HSMul.hSMul (β := Ideal R) (I ^ m) ⊤
⊢ Eq (α := R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)
    (Submodule.Quotient.mk ((↑r : ℕ → R) n) : R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)
    (Submodule.Quotient.mk ((↑r : ℕ → R) m) : R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)

Tactic:
exact (r.property hmn).symm

Premises used: SModEq.symm, Subtype.property
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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) ⊤)
rw₅ 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) ⊤)
⊢ 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:
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]

Premises used: AdicCompletion.AdicCauchySequence.mk_eq_mk, Module.Quotient.mk_smul_mk, Submodule.Quotient.mk_smul, AdicCompletion.Ideal.mk_eq_mk
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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₂
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₂)
⊢ 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₂)

Tactic:
induction x using Quotient.inductionOn'
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
⊢ I = HSMul.hSMul (β := Ideal R) I ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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 ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : (quotientRel (I • ⊤) : R → R → Prop) b₁ b₂
⊢ b₁ - b₂ ∈ I

Tactic:
rwa [show I = I • ⊤ by simp, ← Submodule.quotientRel_def]

Premises used: Submodule.quotientRel_def
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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

Tactic:
have h : b₁ - b₂ ∈ (I : Submodule R R) := by
        rwa [show I = I • ⊤ by simp, ← Submodule.quotientRel_def]
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
h₁ : (b₁ - b₂) • a ∈ HSMul.hSMul (β := Submodule R M) 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₂)

Tactic:
rw [← sub_eq_zero, ← sub_smul, Submodule.Quotient.mk''_eq_mk,
        ← Submodule.Quotient.mk_smul, Submodule.Quotient.mk_eq_zero]

Premises used: sub_eq_zero, sub_smul, Submodule.Quotient.mk_smul, Submodule.Quotient.mk''_eq_mk, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
⊢ (b₁ - b₂) • a ∈ HSMul.hSMul (β := Submodule R M) I ⊤

Tactic:
Submodule.smul_mem_smul h mem_top

Premises used: Set.Mem, Submodule.smul_mem_smul, Submodule.mem_top
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
⊢ (b₁ - b₂) • a ∈ HSMul.hSMul (β := Submodule R M) I ⊤

Tactic:
exact Submodule.smul_mem_smul h mem_top

Premises used: Submodule.smul_mem_smul, Submodule.mem_top
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
x : M
⊢ HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Ideal R) I ⊤) (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
      ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal R) I ⊤) : (a : R) → R ⧸ I • ⊤) r :
        R ⧸ HSMul.hSMul (β := Ideal R) I ⊤)
      (Submodule.Quotient.mk x) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) r (Submodule.Quotient.mk x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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) ⊤
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
⊢ (↑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

Tactic:
induction r using induction_on

Premises used: AdicCompletion.induction_on
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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 : ℕ
x : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
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:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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 ⊤
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)
⊢ (r • s) • x = r • s • x

Tactic:
induction s, x using Quotient.inductionOn₂' with | _ s x
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
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)
⊢ 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)

Tactic:
rw [← Submodule.Quotient.mk_smul, Ideal.Quotient.mk_eq_mk, mk_smul_mk, smul_assoc]

Premises used: smul_assoc, Submodule.Quotient.mk_smul, AdicCompletion.mk_smul_mk, Ideal.Quotient.mk_eq_mk
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
⊢ 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:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
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)
⊢ 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)

Tactic:
apply induction_on I R r (fun r ↦ ?_)

Premises used: AdicCompletion.induction_on
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
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)
⊢ 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 M x (fun x ↦ ?_)

Premises used: AdicCompletion.induction_on
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
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) ⊤)
⊢ 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:
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]

Premises used: Submodule.mapQ_apply, LinearMap.id_coe, AdicCompletion.coe_eval, Submodule.mkQ_apply, AdicCompletion.mk_smul_mk, Submodule.mapQ_eq_factor, Ideal.Quotient.mk_eq_mk, AdicCompletion.mk_apply_coe, map_smul, id_eq
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
rw 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) ⊤)
⊢ 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:
rw [smul_mk I hmn]

Premises used: AdicCompletion.smul_mk
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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 : AdicCompletion I M
⊢ (↑(r • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑r : (n : ℕ) → R ⧸ I ^ n • ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
h : ∀ (n : ℕ), (↑((r * s) • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ (r * s) • x = r • s • x

Tactic:
ext n
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
n : ℕ
⊢ (↑((r * s) • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
simp only [smul_eval, val_mul, mul_smul]

Premises used: AdicCompletion.smul_eval, AdicCompletion.val_mul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := AdicCompletion I R) 1 b = b

Tactic:
ext n
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
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:
simp only [smul_eval, val_one, one_smul]

Premises used: AdicCompletion.smul_eval, one_smul, AdicCompletion.val_one
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
h :
  ∀ (n : ℕ),
    (↑(HSMul.hSMul (β := AdicCompletion I M) r 0) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ HSMul.hSMul (β := AdicCompletion I M) r 0 = 0

Tactic:
ext n
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
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
n : ℕ
⊢ (↑(HSMul.hSMul (β := AdicCompletion I M) r 0) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
simp