awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_1, u_7} R (M i)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
h : ¬j = i
⊢ Eq.{u_7 + 1} (α := M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤) (Submodule.Quotient.mk 0)
    ((↑0 : (n : ℕ) → M i ⧸ I ^ n • ⊤) n)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_1, u_7} R (M i)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
h :
  ∀ (f : AdicCauchySequence I (⨁ (j : ι), M j)) (n : ℕ),
    Eq (α := (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
      ((↑((sum I M ∘ₗ sumInv I M : (a : AdicCompletion I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
              ((mk I (⨁ (j : ι), M j) : (a : AdicCauchySequence I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
                f)) :
          (n : ℕ) → (⨁ (j : ι), M j) ⧸ I ^ n • ⊤)
        n)
      ((↑((LinearMap.id : (a : AdicCompletion I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
              ((mk I (⨁ (j : ι), M j) : (a : AdicCauchySequence I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
                f)) :
          (n : ℕ) → (⨁ (j : ι), M j) ⧸ I ^ n • ⊤)
        n)
⊢ Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I (⨁ (j : ι), M j))
      (AdicCompletion I (⨁ (j : ι), M j)))
    (sum I M ∘ₗ sumInv I M) LinearMap.id

Tactic:
ext f n
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_1, u_7} R (M i)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
h :
  Eq (α := (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
    ((↑((sum I M : (a : ⨁ (j : ι), AdicCompletion I (M j)) → AdicCompletion I (⨁ (j : ι), M j))
              ((sumInv I M : (a : AdicCompletion I (⨁ (j : ι), M j)) → ⨁ (j : ι), AdicCompletion I (M j))
                ((mk I (⨁ (j : ι), M j) :
                    (a : AdicCauchySequence I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
                  f))) :
          (n : ℕ) → (⨁ (j : ι), M j) ⧸ I ^ n • ⊤)
        n :
      (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((↑f : ℕ → ⨁ (j : ι), M j) n) :
      (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
⊢ Eq (α := (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
    ((↑((sum I M ∘ₗ sumInv I M : (a : AdicCompletion I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
            ((mk I (⨁ (j : ι), M j) : (a : AdicCauchySequence I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
              f)) :
        (n : ℕ) → (⨁ (j : ι), M j) ⧸ I ^ n • ⊤)
      n)
    ((↑((LinearMap.id : (a : AdicCompletion I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
            ((mk I (⨁ (j : ι), M j) : (a : AdicCauchySequence I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
              f)) :
        (n : ℕ) → (⨁ (j : ι), M j) ⧸ I ^ n • ⊤)
      n)

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq, mk_apply_coe,
    Submodule.mkQ_apply]

Premises used: LinearMap.id_coe, Submodule.mkQ_apply, LinearMap.coe_comp, Function.comp_apply, AdicCompletion.mk_apply_coe, id_eq
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_1, u_7} R (M i)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
h :
  Eq (α := (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
    ((↑((sum I M : (a : ⨁ (j : ι), AdicCompletion I (M j)) → AdicCompletion I (⨁ (j : ι), M j))
              (∑ i : ι,
                ((DirectSum.of.{u_6, u_7} (fun (i : ι) ↦ AdicCompletion I (M i)) i :
                      AdicCompletion I (M i) →+ ⨁ (i : ι), AdicCompletion I (M i)) :
                    (a : AdicCompletion I (M i)) → ⨁ (i : ι), AdicCompletion I (M i))
                  ((((sumInv I M : (a : AdicCompletion I (⨁ (j : ι), M j)) → ⨁ (j : ι), AdicCompletion I (M j))
                          ((mk I (⨁ (j : ι), M j) :
                              (a : AdicCauchySequence I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
                            f) :
                        ⨁ (j : ι), AdicCompletion I (M j)) :
                      (a : ι) → AdicCompletion I (M a))
                    i))) :
          (n : ℕ) → (⨁ (j : ι), M j) ⧸ I ^ n • ⊤)
        n :
      (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((↑f : ℕ → ⨁ (j : ι), M j) n) :
      (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
⊢ Eq (α := (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
    ((↑((sum I M : (a : ⨁ (j : ι), AdicCompletion I (M j)) → AdicCompletion I (⨁ (j : ι), M j))
              ((sumInv I M : (a : AdicCompletion I (⨁ (j : ι), M j)) → ⨁ (j : ι), AdicCompletion I (M j))
                ((mk I (⨁ (j : ι), M j) :
                    (a : AdicCauchySequence I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
                  f))) :
          (n : ℕ) → (⨁ (j : ι), M j) ⧸ I ^ n • ⊤)
        n :
      (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((↑f : ℕ → ⨁ (j : ι), M j) n) :
      (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)

Tactic:
rw [← DirectSum.sum_univ_of (((sumInv I M) ((AdicCompletion.mk I (⨁ (j : ι), M j)) f)))]

Premises used: AdicCompletion.sumInv, DirectSum.sum_univ_of, AdicCompletion.mk, DirectSum, DFunLike.coe
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_1, u_7} R (M i)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
h :
  Eq (α := (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
    (∑ x : ι,
        ((HSMul.hSMul (β := Submodule R (⨁ (i : ι), M i)) (I ^ n) ⊤).mkQ :
            (a : ⨁ (i : ι), M i) → (⨁ (i : ι), M i) ⧸ I ^ n • ⊤)
          ((lof R ι M x : (a : M x) → ⨁ (i : ι), M i)
            ((component R ι M x : (a : ⨁ (j : ι), M j) → M x) ((↑f : ℕ → ⨁ (j : ι), M j) n))) :
      (⨁ (i : ι), M i) ⧸ HSMul.hSMul (β := Submodule R (⨁ (i : ι), M i)) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((↑f : ℕ → ⨁ (j : ι), M j) n) :
      (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
⊢ Eq (α := (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
    ((↑((sum I M : (a : ⨁ (j : ι), AdicCompletion I (M j)) → AdicCompletion I (⨁ (j : ι), M j))
              (∑ i : ι,
                ((DirectSum.of.{u_6, u_7} (fun (i : ι) ↦ AdicCompletion I (M i)) i :
                      AdicCompletion I (M i) →+ ⨁ (i : ι), AdicCompletion I (M i)) :
                    (a : AdicCompletion I (M i)) → ⨁ (i : ι), AdicCompletion I (M i))
                  ((((sumInv I M : (a : AdicCompletion I (⨁ (j : ι), M j)) → ⨁ (j : ι), AdicCompletion I (M j))
                          ((mk I (⨁ (j : ι), M j) :
                              (a : AdicCauchySequence I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
                            f) :
                        ⨁ (j : ι), AdicCompletion I (M j)) :
                      (a : ι) → AdicCompletion I (M a))
                    i))) :
          (n : ℕ) → (⨁ (j : ι), M j) ⧸ I ^ n • ⊤)
        n :
      (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((↑f : ℕ → ⨁ (j : ι), M j) n) :
      (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)

Tactic:
simp only [sumInv_apply, map_mk, map_sum, sum_of, val_sum_apply, mk_apply_coe,
    AdicCauchySequence.map_apply_coe]

Premises used: AdicCompletion.sumInv_apply, map_sum, AdicCompletion.map_mk, AdicCompletion.sum_of, AdicCompletion.AdicCauchySequence.map_apply_coe, AdicCompletion.mk_apply_coe, AdicCompletion.val_sum_apply
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_1, u_7} R (M i)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ Eq (α := (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)
    (∑ x : ι,
        ((HSMul.hSMul (β := Submodule R (⨁ (i : ι), M i)) (I ^ n) ⊤).mkQ :
            (a : ⨁ (i : ι), M i) → (⨁ (i : ι), M i) ⧸ I ^ n • ⊤)
          ((lof R ι M x : (a : M x) → ⨁ (i : ι), M i)
            ((component R ι M x : (a : ⨁ (j : ι), M j) → M x) ((↑f : ℕ → ⨁ (j : ι), M j) n))) :
      (⨁ (i : ι), M i) ⧸ HSMul.hSMul (β := Submodule R (⨁ (i : ι), M i)) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((↑f : ℕ → ⨁ (j : ι), M j) n) :
      (⨁ (j : ι), M j) ⧸ HSMul.hSMul (β := Submodule R (⨁ (j : ι), M j)) (I ^ n) ⊤)

Tactic:
simp only [← Submodule.mkQ_apply, ← map_sum, ← apply_eq_component, lof_eq_of,
    DirectSum.sum_univ_of]

Premises used: DirectSum.sum_univ_of, DirectSum.lof_eq_of, Submodule.mkQ_apply, map_sum, DirectSum.apply_eq_component
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_1, u_7} R (M i)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
x : ⨁ (j : ι), AdicCompletion I (M j)
⊢ Eq (α := AdicCompletion I (⨁ (j : ι), M j))
    ((sumEquivOfFintype I M : (a : ⨁ (j : ι), AdicCompletion I (M j)) → AdicCompletion I (⨁ (j : ι), M j)) x :
      AdicCompletion I (⨁ (j : ι), M j))
    ((sum I M : (a : ⨁ (j : ι), AdicCompletion I (M j)) → AdicCompletion I (⨁ (j : ι), M j)) x :
      AdicCompletion I (⨁ (j : ι), M j))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_1, u_7} R (M i)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
x : AdicCompletion I (⨁ (j : ι), M j)
⊢ Eq (α := ⨁ (j : ι), AdicCompletion I (M j))
    ((LinearEquiv.symm (sumEquivOfFintype I M) :
          (a : AdicCompletion I (⨁ (j : ι), M j)) → ⨁ (j : ι), AdicCompletion I (M j))
        x :
      ⨁ (j : ι), AdicCompletion I (M j))
    ((sumInv I M : (a : AdicCompletion I (⨁ (j : ι), M j)) → ⨁ (j : ι), AdicCompletion I (M j)) x :
      ⨁ (j : ι), AdicCompletion I (M j))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_1, u_7} R (M i)
inst_3 : DecidableEq ι
inst_4 : Fintype ι
x : AdicCompletion I ((j : ι) → M j)
⊢ Eq (α := (j : ι) → AdicCompletion I (M j))
    ((piEquivOfFintype I M : (a : AdicCompletion I ((j : ι) → M j)) → (j : ι) → AdicCompletion I (M j)) x :
      (j : ι) → AdicCompletion I (M j))
    ((pi I M : (a : AdicCompletion I ((j : ι) → M j)) → (j : ι) → AdicCompletion I (M j)) x :
      (j : ι) → AdicCompletion I (M j))

Tactic:
simp [piEquivOfFintype, sumInv, map_comp_apply]

Premises used: AdicCompletion.sumInv, AdicCompletion.map_comp_apply, AdicCompletion.piEquivOfFintype
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : AdicCompletion I (Fin n → R)
⊢ Eq (α := Fin n → AdicCompletion I R)
    ((piEquivFin I n : (a : AdicCompletion I (Fin n → R)) → Fin n → AdicCompletion I R) x : Fin n → AdicCompletion I R)
    ((pi I fun (x : Fin n) ↦ R : (a : AdicCompletion I ((j : Fin n) → R)) → (j : Fin n) → AdicCompletion I R) x :
      (j : Fin n) → AdicCompletion I R)

Tactic:
simp only [piEquivFin, piEquivOfFintype_apply]

Premises used: AdicCompletion.piEquivOfFintype_apply, AdicCompletion.piEquivFin
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y_1 : N
n : ℕ
r : R
hr : r ∈ I ^ n
y : N
hn : Membership.mem (γ := Submodule R N) ⊤ y
smul :
  ∀ (x : M)
    (hx :
      Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
        (((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f : (a : M) → N ⧸ I • ⊤) x :
          N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
        (((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ : (a : N) → N ⧸ I • ⊤) y :
          N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)),
    ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
      (f : (a : M) → N) x ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]

Tactic:
obtain ⟨x, hx⟩ := h (mkQ _ y)

Premises used: Submodule.mkQ, DFunLike.coe
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y_1 : N
n : ℕ
r : R
hr : r ∈ I ^ n
y : N
hn : Membership.mem (γ := Submodule R N) ⊤ y
x : M
hx :
  Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f : (a : M) → N ⧸ I • ⊤) x :
      N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ : (a : N) → N ⧸ I • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
right : (f : (a : M) → N) (r • x) ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]

Tactic:
use r • x, smul_mem_smul hr mem_top

Premises used: Submodule.smul_mem_smul, Submodule.mem_top
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y_1 : N
n : ℕ
r : R
hr : r ∈ I ^ n
y : N
hn : Membership.mem (γ := Submodule R N) ⊤ y
x : M
hx :
  Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f : (a : M) → N ⧸ I • ⊤) x :
      N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ : (a : N) → N ⧸ I • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
right :
  ∀ (hx : (f : (a : M) → N) x ≡ y [SMOD HSMul.hSMul (β := Submodule R N) I ⊤]),
    HSMul.hSMul (β := N) r ((f : (a : M) → N) x : N) ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ (f : (a : M) → N) (r • x) ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]

Tactic:
simp only [coe_comp, Function.comp_apply, mkQ_apply, ← SModEq.def, map_smul] at ⊢ hx

Premises used: SModEq.def, Submodule.mkQ_apply, LinearMap.coe_comp, Function.comp_apply, map_smul
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y_1 : N
n : ℕ
r : R
hr : r ∈ I ^ n
y : N
hn : Membership.mem (γ := Submodule R N) ⊤ y
x : M
hx : (f : (a : M) → N) x ≡ y [SMOD HSMul.hSMul (β := Submodule R N) I ⊤]
right : HSMul.hSMul (β := N) r ((f : (a : M) → N) x : N) ≡ r • y [SMOD I ^ n • HSMul.hSMul (β := Submodule R N) I ⊤]
⊢ HSMul.hSMul (β := N) r ((f : (a : M) → N) x : N) ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]

Tactic:
rw [pow_succ, ← smul_smul]

Premises used: pow_succ, smul_smul
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y_1 : N
n : ℕ
r : R
hr : r ∈ I ^ n
y : N
hn : Membership.mem (γ := Submodule R N) ⊤ y
x : M
hx : (f : (a : M) → N) x ≡ y [SMOD HSMul.hSMul (β := Submodule R N) I ⊤]
⊢ HSMul.hSMul (β := N) r ((f : (a : M) → N) x : N) ≡ r • y [SMOD I ^ n • HSMul.hSMul (β := Submodule R N) I ⊤]

Tactic:
SModEq.smul' hx hr

Premises used: Set.Mem, SModEq.smul'
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y_1 : N
n : ℕ
r : R
hr : r ∈ I ^ n
y : N
hn : Membership.mem (γ := Submodule R N) ⊤ y
x : M
hx : (f : (a : M) → N) x ≡ y [SMOD HSMul.hSMul (β := Submodule R N) I ⊤]
⊢ HSMul.hSMul (β := N) r ((f : (a : M) → N) x : N) ≡ r • y [SMOD I ^ n • HSMul.hSMul (β := Submodule R N) I ⊤]

Tactic:
exact SModEq.smul' hx hr

Premises used: SModEq.smul'
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
n : ℕ
y1 : N
hy1 : y1 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y2 : N
hy2 : y2 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
ih1 :
  ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y1 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
ih2 :
  ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
add :
  ∀ (x1 : M) (hx1 : x1 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (hx1' : (f : (a : M) → N) x1 ≡ y1 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]),
    ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
      (f : (a : M) → N) x ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]

Tactic:
obtain ⟨x1, hx1, hx1'⟩ := ih1
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
n : ℕ
y1 : N
hy1 : y1 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y2 : N
hy2 : y2 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
ih2 :
  ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
x1 : M
hx1 : x1 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hx1' : (f : (a : M) → N) x1 ≡ y1 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
add :
  ∀ (x2 : M) (hx2 : x2 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (hx2' : (f : (a : M) → N) x2 ≡ y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]),
    ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
      (f : (a : M) → N) x ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]

Tactic:
obtain ⟨x2, hx2, hx2'⟩ := ih2
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
n : ℕ
y1 : N
hy1 : y1 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y2 : N
hy2 : y2 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
x1 : M
hx1 : x1 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hx1' : (f : (a : M) → N) x1 ≡ y1 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
x2 : M
hx2 : x2 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hx2' : (f : (a : M) → N) x2 ≡ y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
right : (f : (a : M) → N) (x1 + x2) ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]

Tactic:
use x1 + x2, add_mem hx1 hx2

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
n : ℕ
y1 : N
hy1 : y1 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y2 : N
hy2 : y2 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
x1 : M
hx1 : x1 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hx1' : (f : (a : M) → N) x1 ≡ y1 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
x2 : M
hx2 : x2 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hx2' : (f : (a : M) → N) x2 ≡ y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
right :
  HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) x1 : N) ((f : (a : M) → N) x2 : N) ≡ y1 + y2 [SMOD
    HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ (f : (a : M) → N) (x1 + x2) ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]

Tactic:
simp only [map_add]

Premises used: map_add