awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
A : Type u_4
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := A) (⇑f : (a : S) → A)
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := AdicCompletion (RingHom.ker f) S) (β := A)
    (Function.comp (β := HasQuotient.Quotient S (B := Ideal S) (RingHom.ker f))
      (⇑(Ideal.quotientKerAlgEquivOfSurjective hf) : (a : S ⧸ RingHom.ker f) → A)
      (⇑(evalOneₐ (RingHom.ker f)) : (a : AdicCompletion (RingHom.ker f) S) → S ⧸ RingHom.ker f))

Tactic:
(AlgEquiv.surjective _).comp (evalOneₐ_surjective _)

Premises used: Function.Surjective.comp, AdicCompletion.evalOneₐ_surjective, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
A : Type u_4
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := A) (⇑f : (a : S) → A)
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := AdicCompletion (RingHom.ker f) S) (β := A)
    (Function.comp (β := HasQuotient.Quotient S (B := Ideal S) (RingHom.ker f))
      (⇑(Ideal.quotientKerAlgEquivOfSurjective hf) : (a : S ⧸ RingHom.ker f) → A)
      (⇑(evalOneₐ (RingHom.ker f)) : (a : AdicCompletion (RingHom.ker f) S) → S ⧸ RingHom.ker f))

Tactic:
exact (AlgEquiv.surjective _).comp (evalOneₐ_surjective _)

Premises used: Function.Surjective.comp, AdicCompletion.evalOneₐ_surjective, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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
r x : AdicCompletion I R
⊢ ∀ (x_1 : M),
    Eq (α := AdicCompletion I M)
      (((↑R :
                  {S : Type u_1} →
                    {M M₂ : Type u_2} →
                      [inst : Semiring R] →
                        [inst_5 : Semiring S] →
                          [inst_6 : AddCommMonoid M] →
                            [inst_7 : AddCommMonoid M₂] →
                              [inst_8 : Module R M] →
                                [inst_9 : Module R M₂] →
                                  [inst_10 : Module S M] →
                                    [inst_11 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (S := AdicCompletion I R)
                ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M) :
                    (a : AdicCompletion I R) → AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I M)
                  (r • x)) ∘ₗ
              of I M :
            (a : M) → AdicCompletion I M)
          x_1 :
        AdicCompletion I M)
      ((HSMul.hSMul (α := AdicCompletion I R) (β := M →ₗ[R] AdicCompletion I M)
              ((RingHom.id (AdicCompletion I R) : (a : AdicCompletion I R) → AdicCompletion I R) r : AdicCompletion I R)
              ((↑R :
                    {S : Type u_1} →
                      {M M₂ : Type u_2} →
                        [inst : Semiring R] →
                          [inst_5 : Semiring S] →
                            [inst_6 : AddCommMonoid M] →
                              [inst_7 : AddCommMonoid M₂] →
                                [inst_8 : Module R M] →
                                  [inst_9 : Module R M₂] →
                                    [inst_10 : Module S M] →
                                      [inst_11 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (S := AdicCompletion I R)
                  ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M) :
                      (a : AdicCompletion I R) → AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I M)
                    x) ∘ₗ
                of I M) :
            (a : M) → AdicCompletion I M)
          x_1 :
        AdicCompletion I M)

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
r : AdicCompletion I R
x : M
⊢ (ofTensorProduct I M : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M) (r ⊗ₜ[R] x) =
    HSMul.hSMul (β := AdicCompletion I M) r ((of I M : (a : M) → AdicCompletion I M) x : AdicCompletion I M)

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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
a :
  ∀ (x : M) (n : ℕ),
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      ((↑((((AlgebraTensorModule.curry (map I f ∘ₗ ofTensorProduct I M) :
                      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R)
                        (LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (AdicCompletion I N))) :
                    (a : AdicCompletion I R) → M →ₗ[R] AdicCompletion I N)
                  1 :
                (a : M) → AdicCompletion I N)
              x) :
          (n : ℕ) → N ⧸ I ^ n • ⊤)
        n)
      ((↑((((AlgebraTensorModule.curry (ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f) :
                      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R)
                        (LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (AdicCompletion I N))) :
                    (a : AdicCompletion I R) → M →ₗ[R] AdicCompletion I N)
                  1 :
                (a : M) → AdicCompletion I N)
              x) :
          (n : ℕ) → N ⧸ I ^ n • ⊤)
        n)
⊢ map I f ∘ₗ ofTensorProduct I M = ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f

Tactic:
ext
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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 : M
n : ℕ
⊢ Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((↑((((AlgebraTensorModule.curry (map I f ∘ₗ ofTensorProduct I M) :
                    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R)
                      (LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (AdicCompletion I N))) :
                  (a : AdicCompletion I R) → M →ₗ[R] AdicCompletion I N)
                1 :
              (a : M) → AdicCompletion I N)
            x) :
        (n : ℕ) → N ⧸ I ^ n • ⊤)
      n)
    ((↑((((AlgebraTensorModule.curry (ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f) :
                    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R)
                      (LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (AdicCompletion I N))) :
                  (a : AdicCompletion I R) → M →ₗ[R] AdicCompletion I N)
                1 :
              (a : M) → AdicCompletion I N)
            x) :
        (n : ℕ) → N ⧸ I ^ n • ⊤)
      n)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
a :
  ∀ (i j : ι) (k : ℕ),
    Eq.{u_1 + 1} (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ k) ⊤)
      ((↑(((((AlgebraTensorModule.curry
                            ((↑(piEquivOfFintype I fun (x : ι) ↦ R) :
                                AdicCompletion I ((j : ι) → R) →ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I R) ∘ₗ
                              ofTensorProduct I (ι → R)) :
                          LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R)
                            ((ι → R) →ₗ[R] ι → AdicCompletion I R)) :
                        (a : AdicCompletion I R) → (ι → R) →ₗ[R] ι → AdicCompletion I R)
                      1 ∘ₗ
                    LinearMap.single R (fun (i : ι) ↦ R) i :
                  R →ₗ[R] ι → AdicCompletion I R) :
                (a : R) → ι → AdicCompletion I R)
              1 j) :
          (n : ℕ) → R ⧸ I ^ n • ⊤)
        k)
      ((↑(((((AlgebraTensorModule.curry
                            (↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) :
                              AdicCompletion I R ⊗[R] (ι → R) →ₗ[AdicCompletion I R] ι → AdicCompletion I R) :
                          LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R)
                            ((ι → R) →ₗ[R] ι → AdicCompletion I R)) :
                        (a : AdicCompletion I R) → (ι → R) →ₗ[R] ι → AdicCompletion I R)
                      1 ∘ₗ
                    LinearMap.single R (fun (i : ι) ↦ R) i :
                  R →ₗ[R] ι → AdicCompletion I R) :
                (a : R) → ι → AdicCompletion I R)
              1 j) :
          (n : ℕ) → R ⧸ I ^ n • ⊤)
        k)
⊢ Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
      (ι → AdicCompletion I R))
    ((↑(piEquivOfFintype I fun (x : ι) ↦ R) :
        AdicCompletion I ((j : ι) → R) →ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I R) ∘ₗ
      ofTensorProduct I (ι → R))
    (↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) :
      AdicCompletion I R ⊗[R] (ι → R) →ₗ[AdicCompletion I R] ι → AdicCompletion I R)

Tactic:
ext i j k
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i j : ι
k : ℕ
h :
  Eq.{u_1 + 1} (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ k) ⊤) (if j = i then 1 else 0)
    ((↑(if j = i then 1 else 0) : (n : ℕ) → R ⧸ I ^ n • ⊤) k)
⊢ Eq.{u_1 + 1} (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ k) ⊤)
    ((↑(((((AlgebraTensorModule.curry
                          ((↑(piEquivOfFintype I fun (x : ι) ↦ R) :
                              AdicCompletion I ((j : ι) → R) →ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I R) ∘ₗ
                            ofTensorProduct I (ι → R)) :
                        LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R)
                          ((ι → R) →ₗ[R] ι → AdicCompletion I R)) :
                      (a : AdicCompletion I R) → (ι → R) →ₗ[R] ι → AdicCompletion I R)
                    1 ∘ₗ
                  LinearMap.single R (fun (i : ι) ↦ R) i :
                R →ₗ[R] ι → AdicCompletion I R) :
              (a : R) → ι → AdicCompletion I R)
            1 j) :
        (n : ℕ) → R ⧸ I ^ n • ⊤)
      k)
    ((↑(((((AlgebraTensorModule.curry
                          (↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) :
                            AdicCompletion I R ⊗[R] (ι → R) →ₗ[AdicCompletion I R] ι → AdicCompletion I R) :
                        LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R)
                          ((ι → R) →ₗ[R] ι → AdicCompletion I R)) :
                      (a : AdicCompletion I R) → (ι → R) →ₗ[R] ι → AdicCompletion I R)
                    1 ∘ₗ
                  LinearMap.single R (fun (i : ι) ↦ R) i :
                R →ₗ[R] ι → AdicCompletion I R) :
              (a : R) → ι → AdicCompletion I R)
            1 j) :
        (n : ℕ) → R ⧸ I ^ n • ⊤)
      k)

Tactic:
simpa [Pi.single_apply, -smul_eq_mul]

Premises used: Pi.single_apply, smul_eq_mul
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i j : ι
k : ℕ
a : j = i → Eq.{u_1 + 1} (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ k) ⊤) 1 ((↑1 : (n : ℕ) → R ⧸ I ^ n • ⊤) k)
a₁ : ¬j = i → Eq.{u_1 + 1} (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ k) ⊤) 0 ((↑0 : (n : ℕ) → R ⧸ I ^ n • ⊤) k)
⊢ Eq.{u_1 + 1} (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ k) ⊤) (if j = i then 1 else 0)
    ((↑(if j = i then 1 else 0) : (n : ℕ) → R ⧸ I ^ n • ⊤) k)

Tactic:
split
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i j : ι
k : ℕ
h : j = i
⊢ Eq.{u_1 + 1} (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ k) ⊤) 1 ((↑1 : (n : ℕ) → R ⧸ I ^ n • ⊤) k)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i j : ι
k : ℕ
h : ¬j = i
⊢ Eq.{u_1 + 1} (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ k) ⊤) 0 ((↑0 : (n : ℕ) → R ⧸ I ^ n • ⊤) k)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
rw :
  Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
      (AdicCompletion I (ι → R)))
    (ofTensorProduct I (ι → R) :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
        (AdicCompletion I (ι → R)))
    (((↑(LinearEquiv.symm (piEquivOfFintype I fun (x : ι) ↦ R)) :
            ((j : ι) → AdicCompletion I R) →ₗ[AdicCompletion I R] AdicCompletion I ((j : ι) → R)) ∘ₗ
          (↑(piEquivOfFintype I fun (x : ι) ↦ R) :
            AdicCompletion I ((j : ι) → R) →ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I R)) ∘ₗ
        ofTensorProduct I (ι → R) :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
        (AdicCompletion I ((j : ι) → R)))
⊢ Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
      (AdicCompletion I (ι → R)))
    (ofTensorProduct I (ι → R) :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
        (AdicCompletion I (ι → R)))
    ((↑(LinearEquiv.symm (piEquivOfFintype I fun (x : ι) ↦ R)) :
          ((j : ι) → AdicCompletion I R) →ₗ[AdicCompletion I R] AdicCompletion I ((j : ι) → R)) ∘ₗ
        (↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) :
          AdicCompletion I R ⊗[R] (ι → R) →ₗ[AdicCompletion I R] ι → AdicCompletion I R) :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
        (AdicCompletion I ((j : ι) → R)))

Tactic:
rw [← piEquivOfFintype_comp_ofTensorProduct_eq I ι, ← LinearMap.comp_assoc]

Premises used: LinearMap.comp_assoc, _private.0.AdicCompletion.piEquivOfFintype_comp_ofTensorProduct_eq
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
⊢ Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
      (AdicCompletion I (ι → R)))
    (ofTensorProduct I (ι → R) :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
        (AdicCompletion I (ι → R)))
    (((↑(LinearEquiv.symm (piEquivOfFintype I fun (x : ι) ↦ R)) :
            ((j : ι) → AdicCompletion I R) →ₗ[AdicCompletion I R] AdicCompletion I ((j : ι) → R)) ∘ₗ
          (↑(piEquivOfFintype I fun (x : ι) ↦ R) :
            AdicCompletion I ((j : ι) → R) →ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I R)) ∘ₗ
        ofTensorProduct I (ι → R) :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
        (AdicCompletion I ((j : ι) → R)))

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
rw :
  Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
      (AdicCompletion I R ⊗[R] (ι → R)))
    ((↑(LinearEquiv.symm (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)) :
          ((j : ι) → AdicCompletion I R) →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] (ι → R)) ∘ₗ
        (↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) :
          AdicCompletion I R ⊗[R] (ι → R) →ₗ[AdicCompletion I R] ι → AdicCompletion I R) :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
        (AdicCompletion I R ⊗[R] (ι → R)))
    (LinearMap.id :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
        (AdicCompletion I R ⊗[R] (ι → R)))
⊢ Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
      (AdicCompletion I R ⊗[R] (ι → R)))
    ((↑(LinearEquiv.trans (piEquivOfFintype I fun (x : ι) ↦ R)
              (LinearEquiv.symm (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι))) :
          AdicCompletion I (ι → R) →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] (ι → R)) ∘ₗ
        ofTensorProduct I (ι → R) :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
        (AdicCompletion I R ⊗[R] (ι → R)))
    (LinearMap.id :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
        (AdicCompletion I R ⊗[R] (ι → R)))

Tactic:
rw [LinearEquiv.coe_trans, LinearMap.comp_assoc, piEquivOfFintype_comp_ofTensorProduct_eq]

Premises used: LinearMap.comp_assoc, _private.0.AdicCompletion.piEquivOfFintype_comp_ofTensorProduct_eq, LinearEquiv.coe_trans
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
⊢ Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
      (AdicCompletion I R ⊗[R] (ι → R)))
    ((↑(LinearEquiv.symm (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)) :
          ((j : ι) → AdicCompletion I R) →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] (ι → R)) ∘ₗ
        (↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) :
          AdicCompletion I R ⊗[R] (ι → R) →ₗ[AdicCompletion I R] ι → AdicCompletion I R) :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
        (AdicCompletion I R ⊗[R] (ι → R)))
    (LinearMap.id :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
        (AdicCompletion I R ⊗[R] (ι → R)))

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
rw :
  Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I (ι → R))
      (AdicCompletion I (ι → R)))
    ((↑(LinearEquiv.symm (piEquivOfFintype I fun (x : ι) ↦ R)) :
        ((j : ι) → AdicCompletion I R) →ₗ[AdicCompletion I R] AdicCompletion I ((j : ι) → R)) ∘ₗ
      ((↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) :
            LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
              (ι → AdicCompletion I R)) :
          LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
            (ι → AdicCompletion I R)) ∘ₗ
        ((↑(LinearEquiv.symm (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)) :
              ((j : ι) → AdicCompletion I R) →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] (ι → R)) ∘ₗ
            (↑(piEquivOfFintype I fun (x : ι) ↦ R) :
              AdicCompletion I (ι → R) →ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I R) :
          LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I (ι → R))
            (AdicCompletion I R ⊗[R] (ι → R))))
    LinearMap.id
⊢ Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I (ι → R))
      (AdicCompletion I (ι → R)))
    (ofTensorProduct I (ι → R) ∘ₗ
      (↑(LinearEquiv.trans (piEquivOfFintype I fun (x : ι) ↦ R)
            (LinearEquiv.symm (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι))) :
        AdicCompletion I (ι → R) →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] (ι → R)))
    LinearMap.id

Tactic:
rw [LinearEquiv.coe_trans, ofTensorProduct_eq, LinearMap.comp_assoc]

Premises used: LinearMap.comp_assoc, _private.0.AdicCompletion.ofTensorProduct_eq, LinearEquiv.coe_trans
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
nth_rw :
  Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I (ι → R))
      (AdicCompletion I (ι → R)))
    ((↑(LinearEquiv.symm (piEquivOfFintype I fun (x : ι) ↦ R)) :
        ((j : ι) → AdicCompletion I R) →ₗ[AdicCompletion I R] AdicCompletion I ((j : ι) → R)) ∘ₗ
      (((↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) :
              LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
                (ι → AdicCompletion I R)) :
            LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
              (ι → AdicCompletion I R)) ∘ₗ
          ((↑(LinearEquiv.symm (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)) :
              LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) ((j : ι) → AdicCompletion I R)
                (AdicCompletion I R ⊗[R] (ι → R))) :
            LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) ((j : ι) → AdicCompletion I R)
              (AdicCompletion I R ⊗[R] (ι → R)))) ∘ₗ
        (↑(piEquivOfFintype I fun (x : ι) ↦ R) :
          AdicCompletion I (ι → R) →ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I R))
    LinearMap.id
⊢ Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I (ι → R))
      (AdicCompletion I (ι → R)))
    ((↑(LinearEquiv.symm (piEquivOfFintype I fun (x : ι) ↦ R)) :
        ((j : ι) → AdicCompletion I R) →ₗ[AdicCompletion I R] AdicCompletion I ((j : ι) → R)) ∘ₗ
      ((↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) :
            LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
              (ι → AdicCompletion I R)) :
          LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (ι → R))
            (ι → AdicCompletion I R)) ∘ₗ
        ((↑(LinearEquiv.symm (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)) :
              ((j : ι) → AdicCompletion I R) →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] (ι → R)) ∘ₗ
            (↑(piEquivOfFintype I fun (x : ι) ↦ R) :
              AdicCompletion I (ι → R) →ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I R) :
          LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I (ι → R))
            (AdicCompletion I R ⊗[R] (ι → R))))
    LinearMap.id

Tactic:
nth_rw 2 [← LinearMap.comp_assoc]

Premises used: LinearMap.comp_assoc