awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : AdicCompletion I N
⊢ Eq.{u_2 + 1} (α := AdicCompletion I M)
    (((congr I f).symm : (a : AdicCompletion I N) → AdicCompletion I M) x : AdicCompletion I M)
    ((map I (↑f.symm : N →ₗ[R] M) : (a : AdicCompletion I N) → AdicCompletion I M) x : AdicCompletion I M)

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 ι
j : ι
x : AdicCompletion I (M j)
⊢ Eq (α := AdicCompletion I (⨁ (j : ι), M j))
    ((sum I M : (a : ⨁ (j : ι), AdicCompletion I (M j)) → AdicCompletion I (⨁ (j : ι), M j))
        (((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)) → ⨁ (i : ι), AdicCompletion I (M i))
          x) :
      AdicCompletion I (⨁ (j : ι), M j))
    ((map I (lof R ι M j) : (a : AdicCompletion I (M j)) → AdicCompletion I (⨁ (i : ι), M i)) x :
      AdicCompletion I (⨁ (i : ι), M i))

Tactic:
simp [sum]

Premises used: AdicCompletion.sum
-- 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 ι
j : ι
x : AdicCompletion I (M j)
rw :
  Eq (α := AdicCompletion I (⨁ (j : ι), M j))
    ((sum I M : (a : ⨁ (j : ι), AdicCompletion I (M j)) → AdicCompletion I (⨁ (j : ι), M j))
        (((lof.{u_1, u_6, u_7} R ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
              AdicCompletion I (M j) →ₗ[R] ⨁ (i : ι), AdicCompletion I (M i)) :
            (a : AdicCompletion I (M j)) → ⨁ (i : ι), AdicCompletion I (M i))
          x) :
      AdicCompletion I (⨁ (j : ι), M j))
    ((map I (lof R ι M j) : (a : AdicCompletion I (M j)) → AdicCompletion I (⨁ (i : ι), M i)) x :
      AdicCompletion I (⨁ (i : ι), M i))
⊢ Eq (α := AdicCompletion I (⨁ (j : ι), M j))
    ((sum I M : (a : ⨁ (j : ι), AdicCompletion I (M j)) → AdicCompletion I (⨁ (j : ι), M j))
        (((DirectSum.of.{u_6, u_7} (fun (i : ι) ↦ AdicCompletion I (M i)) j :
              AdicCompletion I (M j) →+ ⨁ (i : ι), AdicCompletion I (M i)) :
            (a : AdicCompletion I (M j)) → ⨁ (i : ι), AdicCompletion I (M i))
          x) :
      AdicCompletion I (⨁ (j : ι), M j))
    ((map I (lof R ι M j) : (a : AdicCompletion I (M j)) → AdicCompletion I (⨁ (i : ι), M i)) x :
      AdicCompletion I (⨁ (i : ι), M i))

Tactic:
rw [← lof_eq_of R]

Premises used: DirectSum.lof_eq_of
-- 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 ι
j : ι
x : AdicCompletion I (M j)
⊢ Eq (α := AdicCompletion I (⨁ (j : ι), M j))
    ((sum I M : (a : ⨁ (j : ι), AdicCompletion I (M j)) → AdicCompletion I (⨁ (j : ι), M j))
        (((lof.{u_1, u_6, u_7} R ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
              AdicCompletion I (M j) →ₗ[R] ⨁ (i : ι), AdicCompletion I (M i)) :
            (a : AdicCompletion I (M j)) → ⨁ (i : ι), AdicCompletion I (M i))
          x) :
      AdicCompletion I (⨁ (j : ι), M j))
    ((map I (lof R ι M j) : (a : AdicCompletion I (M j)) → AdicCompletion I (⨁ (i : ι), M i)) x :
      AdicCompletion I (⨁ (i : ι), M i))

Tactic:
apply sum_lof

Premises used: AdicCompletion.sum_lof
-- 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 ι
x : AdicCompletion I (⨁ (j : ι), M j)
j : ι
apply :
  ∀ (x : AdicCauchySequence I (⨁ (j : ι), M j)),
    Eq.{u_7 + 1} (α := AdicCompletion I (M j))
      ((component (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
            (a : ⨁ (i : ι), AdicCompletion I (M i)) → AdicCompletion I (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))
              x)) :
        AdicCompletion I (M j))
      ((map I (component R ι M j) : (a : AdicCompletion I (⨁ (j : ι), M j)) → AdicCompletion I (M j))
          ((mk I (⨁ (j : ι), M j) : (a : AdicCauchySequence I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j))
            x) :
        AdicCompletion I (M j))
⊢ Eq.{u_7 + 1} (α := AdicCompletion I (M j))
    ((component (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
          (a : ⨁ (i : ι), AdicCompletion I (M i)) → AdicCompletion I (M j))
        ((sumInv I M : (a : AdicCompletion I (⨁ (j : ι), M j)) → ⨁ (j : ι), AdicCompletion I (M j)) x) :
      AdicCompletion I (M j))
    ((map I (component R ι M j) : (a : AdicCompletion I (⨁ (j : ι), M j)) → AdicCompletion I (M j)) x :
      AdicCompletion I (M j))

Tactic:
apply induction_on I _ x (fun x ↦ ?_)

Premises used: AdicCompletion.induction_on
-- 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 ι
x_1 : AdicCompletion I (⨁ (j : ι), M j)
j : ι
x : AdicCauchySequence I (⨁ (j : ι), M j)
⊢ Eq.{u_7 + 1} (α := AdicCompletion I (M j))
    ((component (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I (M i)) j :
          (a : ⨁ (i : ι), AdicCompletion I (M i)) → AdicCompletion I (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))
            x)) :
      AdicCompletion I (M j))
    ((map I (component R ι M j) : (a : AdicCompletion I (⨁ (j : ι), M j)) → AdicCompletion I (M j))
        ((mk I (⨁ (j : ι), M j) : (a : AdicCauchySequence I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j)) x) :
      AdicCompletion I (M j))

Tactic:
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 ι
x : AdicCompletion I (⨁ (j : ι), M j)
j : ι
apply :
  ∀ (x : AdicCauchySequence 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))
                x) :
            ⨁ (j : ι), AdicCompletion I (M j)) :
          (a : ι) → AdicCompletion I (M a))
        j =
      (map I (component R ι M j) : (a : AdicCompletion I (⨁ (j : ι), M j)) → AdicCompletion I (M j))
        ((mk I (⨁ (j : ι), M j) : (a : AdicCauchySequence I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j)) x)
⊢ (((sumInv I M : (a : AdicCompletion I (⨁ (j : ι), M j)) → ⨁ (j : ι), AdicCompletion I (M j)) x :
          ⨁ (j : ι), AdicCompletion I (M j)) :
        (a : ι) → AdicCompletion I (M a))
      j =
    (map I (component R ι M j) : (a : AdicCompletion I (⨁ (j : ι), M j)) → AdicCompletion I (M j)) x

Tactic:
apply induction_on I _ x (fun x ↦ ?_)

Premises used: AdicCompletion.induction_on
-- 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 ι
x_1 : AdicCompletion I (⨁ (j : ι), M j)
j : ι
x : AdicCauchySequence 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))
              x) :
          ⨁ (j : ι), AdicCompletion I (M j)) :
        (a : ι) → AdicCompletion I (M a))
      j =
    (map I (component R ι M j) : (a : AdicCompletion I (⨁ (j : ι), M j)) → AdicCompletion I (M j))
      ((mk I (⨁ (j : ι), M j) : (a : AdicCauchySequence I (⨁ (j : ι), M j)) → AdicCompletion I (⨁ (j : ι), M j)) x)

Tactic:
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 ι
H :
  ∀ (j : ι) (x : AdicCauchySequence I (M j)),
    Eq (α := ⨁ (j : ι), AdicCompletion I (M j))
      (((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) :
        ⨁ (j : ι), AdicCompletion I (M j))
      (((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) :
        ⨁ (j : ι), AdicCompletion I (M j))
⊢ Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (⨁ (j : ι), AdicCompletion I (M j))
      (⨁ (j : ι), AdicCompletion I (M j)))
    (sumInv I M ∘ₗ sum I M) LinearMap.id

Tactic:
ext j x : 2
-- 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)
apply :
  ∀ (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))
⊢ Eq (α := ⨁ (j : ι), AdicCompletion I (M j))
    (((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) :
      ⨁ (j : ι), AdicCompletion I (M j))
    (((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) :
      ⨁ (j : ι), AdicCompletion I (M j))

Tactic:
apply DirectSum.ext_component (AdicCompletion I R) (fun i ↦ ?_)

Premises used: AdicCompletion, DirectSum.ext_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 ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
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)
⊢ 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))

Tactic:
ext 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 ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
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) ⊤)
⊢ 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:
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]

Premises used: AdicCompletion.sum_lof, Submodule.mkQ_apply, AdicCompletion.map_mk, AdicCompletion.AdicCauchySequence.map_apply_coe, LinearMap.coe_comp, Function.comp_apply, AdicCompletion.component_sumInv, AdicCompletion.mk_apply_coe, LinearMap.id_comp
-- 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 :
  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)
⊢ 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:
rw [DirectSum.component.of, DirectSum.component.of]

Premises used: DirectSum.component.of
-- 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 :
  ∀ (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) ⊤)
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)
⊢ 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:
split
-- 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
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) ⋯ ((↑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)) ⋯
              ((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) ⊤)
⊢ 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:
subst h
-- 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)
n : ℕ
⊢ 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) ⋯ ((↑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)) ⋯
              ((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:
simp