awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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 : ι
⊢ Eq.{u_7 + 1} (α := AdicCompletion I (M i))
    ((component (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) i :
          (a : ⨁ (i : ι), AdicCompletion I (M i)) → AdicCompletion I (M i))
        (((sumInv I M ∘ₗ sum I M) ∘ₗ
              lof.{u_1, u_6, u_7} (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
            (a : AdicCompletion I (M j)) → ⨁ (j : ι), AdicCompletion I (M j))
          ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x)) :
      AdicCompletion I (M i))
    ((component (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) i :
          (a : ⨁ (i : ι), AdicCompletion I (M i)) → AdicCompletion I (M i))
        (((LinearMap.id ∘ₗ lof.{u_1, u_6, u_7} (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
              LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I (M j))
                (⨁ (j : ι), AdicCompletion I (M j))) :
            (a : AdicCompletion I (M j)) → ⨁ (j : ι), AdicCompletion I (M j))
          ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x)) :
      AdicCompletion I (M i))
have h : ∀ (n : ℕ),
  Eq.{u_7 + 1} (α := M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
    ((↑((component (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) i :
              (a : ⨁ (i : ι), AdicCompletion I (M i)) → AdicCompletion I (M i))
            (((sumInv I M ∘ₗ sum I M) ∘ₗ
                  lof.{u_1, u_6, u_7} (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
                (a : AdicCompletion I (M j)) → ⨁ (j : ι), AdicCompletion I (M j))
              ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x))) :
        (n : ℕ) → M i ⧸ I ^ n • ⊤)
      n)
    ((↑((component (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) i :
              (a : ⨁ (i : ι), AdicCompletion I (M i)) → AdicCompletion I (M i))
            (((LinearMap.id ∘ₗ lof.{u_1, u_6, u_7} (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
                  LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I (M j))
                    (⨁ (j : ι), AdicCompletion I (M j))) :
                (a : AdicCompletion I (M j)) → ⨁ (j : ι), AdicCompletion I (M j))
              ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x))) :
        (n : ℕ) → M i ⧸ I ^ n • ⊤)
      n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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 : ℕ
⊢ Eq.{u_7 + 1} (α := M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
    ((↑((component (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) i :
              (a : ⨁ (i : ι), AdicCompletion I (M i)) → AdicCompletion I (M i))
            (((sumInv I M ∘ₗ sum I M) ∘ₗ
                  lof.{u_1, u_6, u_7} (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
                (a : AdicCompletion I (M j)) → ⨁ (j : ι), AdicCompletion I (M j))
              ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x))) :
        (n : ℕ) → M i ⧸ I ^ n • ⊤)
      n)
    ((↑((component (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) i :
              (a : ⨁ (i : ι), AdicCompletion I (M i)) → AdicCompletion I (M i))
            (((LinearMap.id ∘ₗ lof.{u_1, u_6, u_7} (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
                  LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I (M j))
                    (⨁ (j : ι), AdicCompletion I (M j))) :
                (a : AdicCompletion I (M j)) → ⨁ (j : ι), AdicCompletion I (M j))
              ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x))) :
        (n : ℕ) → M i ⧸ I ^ n • ⊤)
      n)
have h : Eq.{u_7 + 1} (α := M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
  (Submodule.Quotient.mk
      ((component R ι M i : (a : ⨁ (j : ι), M j) → M i)
        ((lof R ι M j : (a : M j) → ⨁ (i : ι), M i) ((↑x : ℕ → M j) n))) :
    M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
  ((↑((component (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) i :
              (a : ⨁ (i : ι), AdicCompletion I (M i)) → AdicCompletion I (M i))
            (((lof.{u_1, u_6, u_7} (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
                  LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I (M j))
                    (⨁ (i : ι), AdicCompletion I (M i))) :
                (a : AdicCompletion I (M j)) → ⨁ (j : ι), AdicCompletion I (M j))
              ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x))) :
        (n : ℕ) → M i ⧸ I ^ n • ⊤)
      n :
    M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
Tactic: simp only [LinearMap.coe_comp, Function.comp_apply, sum_lof, map_mk, component_sumInv,
    mk_apply_coe, AdicCauchySequence.map_apply_coe, Submodule.mkQ_apply, LinearMap.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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 : ℕ
⊢ Eq.{u_7 + 1} (α := M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
    (Submodule.Quotient.mk
        ((component R ι M i : (a : ⨁ (j : ι), M j) → M i)
          ((lof R ι M j : (a : M j) → ⨁ (i : ι), M i) ((↑x : ℕ → M j) n))) :
      M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
    ((↑((component (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) i :
                (a : ⨁ (i : ι), AdicCompletion I (M i)) → AdicCompletion I (M i))
              (((lof.{u_1, u_6, u_7} (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
                    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I (M j))
                      (⨁ (i : ι), AdicCompletion I (M i))) :
                  (a : AdicCompletion I (M j)) → ⨁ (j : ι), AdicCompletion I (M j))
                ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x))) :
          (n : ℕ) → M i ⧸ I ^ n • ⊤)
        n :
      M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
have h : Eq.{u_7 + 1} (α := M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
  (Submodule.Quotient.mk
    (if h : j = i then Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ M x) h ((↑x : ℕ → M j) n) else 0))
  ((↑(if h : j = i then
          Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ AdicCompletion I (M x)) h
            ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x)
        else 0) :
      (n : ℕ) → M i ⧸ I ^ n • ⊤)
    n)
Tactic: rw [DirectSum.component.of, DirectSum.component.of]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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 : ℕ
⊢ Eq.{u_7 + 1} (α := M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
    (Submodule.Quotient.mk
      (if h : j = i then Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ M x) h ((↑x : ℕ → M j) n) else 0))
    ((↑(if h : j = i then
            Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ AdicCompletion I (M x)) h
              ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x)
          else 0) :
        (n : ℕ) → M i ⧸ I ^ n • ⊤)
      n)
have h : ∀ (h : j = i),
  Eq.{u_7 + 1} (α := M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
    (Submodule.Quotient.mk (Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ M x) h ((↑x : ℕ → M j) n)) :
      M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
    ((↑(Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ AdicCompletion I (M x)) h
              ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x)) :
          (n : ℕ) → M i ⧸ I ^ n • ⊤)
        n :
      M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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 :
  ∀ (h : j = i),
    Eq.{u_7 + 1} (α := M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
      (Submodule.Quotient.mk (Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ M x) h ((↑x : ℕ → M j) n)) :
        M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
      ((↑(Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ AdicCompletion I (M x)) h
                ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x)) :
            (n : ℕ) → M i ⧸ I ^ n • ⊤)
          n :
        M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
⊢ Eq.{u_7 + 1} (α := M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
    (Submodule.Quotient.mk
      (if h : j = i then Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ M x) h ((↑x : ℕ → M j) n) else 0))
    ((↑(if h : j = i then
            Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ AdicCompletion I (M x)) h
              ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x)
          else 0) :
        (n : ℕ) → M i ⧸ I ^ n • ⊤)
      n)
have 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: split
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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 (Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ M x) h ((↑x : ℕ → M j) n)) :
      M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
    ((↑(Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ AdicCompletion I (M x)) h
              ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x)) :
          (n : ℕ) → M i ⧸ I ^ n • ⊤)
        n :
      M i ⧸ HSMul.hSMul (β := Submodule R (M i)) (I ^ n) ⊤)
have subst : Eq.{u_7 + 1} (α := M j ⧸ HSMul.hSMul (β := Submodule R (M j)) (I ^ n) ⊤)
  (Submodule.Quotient.mk (Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ M x) sorry ((↑x : ℕ → M j) n)) :
    M j ⧸ HSMul.hSMul (β := Submodule R (M j)) (I ^ n) ⊤)
  ((↑(Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ AdicCompletion I (M x)) sorry
            ((mk I (M j) : (a : AdicCauchySequence I (M j)) → AdicCompletion I (M j)) x)) :
        (n : ℕ) → M j ⧸ I ^ n • ⊤)
      n :
    M j ⧸ HSMul.hSMul (β := Submodule R (M j)) (I ^ n) ⊤)
Tactic: subst h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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 ι
⊢ 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
have 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)
Tactic: ext f n
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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) ⊤)
    ((↑((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)
have 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) ⊤)
Tactic: simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq, mk_apply_coe,
    Submodule.mkQ_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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) ⊤)
    ((↑((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) ⊤)
have 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) ⊤)
Tactic: rw [← DirectSum.sum_univ_of (((sumInv I M) ((AdicCompletion.mk I (⨁ (j : ι), M j)) f)))]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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) ⊤)
    ((↑((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) ⊤)
have 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) ⊤)
Tactic: simp only [sumInv_apply, map_mk, map_sum, sum_of, val_sum_apply, mk_apply_coe,
    AdicCauchySequence.map_apply_coe]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have 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)) ⊤]
Tactic: obtain ⟨x, hx⟩ := h (mkQ _ y)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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 ⊤)
⊢ ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have right : (f : (a : M) → N) (r • x) ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
Tactic: use r • x, smul_mem_smul hr mem_top
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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 ⊤)
⊢ (f : (a : M) → N) (r • x) ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have 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)) ⊤]
Tactic: simp only [coe_comp, Function.comp_apply, mkQ_apply, ← SModEq.def, map_smul] at ⊢ hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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 HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have right : HSMul.hSMul (β := N) r ((f : (a : M) → N) x : N) ≡ r • y [SMOD I ^ n • HSMul.hSMul (β := Submodule R N) I ⊤]
Tactic: rw [pow_succ, ← smul_smul]