awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (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
⊢ map I f ∘ₗ ofTensorProduct I M = ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
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))
    ((↑(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)
have 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)
Tactic: ext i j k
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i j : ι
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)
have a : j = i → Eq.{u_1 + 1} (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ k) ⊤) 1 ((↑1 : (n : ℕ) → R ⧸ I ^ n • ⊤) k)
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
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)
⊢ 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)
have a₁ : ¬j = i → Eq.{u_1 + 1} (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ k) ⊤) 0 ((↑0 : (n : ℕ) → R ⧸ I ^ n • ⊤) k)
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
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)) ∘ₗ
        (↑(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)))
have 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)))
Tactic: rw [← piEquivOfFintype_comp_ofTensorProduct_eq I ι, ← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
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.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)))
have 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)))
Tactic: rw [LinearEquiv.coe_trans, LinearMap.comp_assoc, piEquivOfFintype_comp_ofTensorProduct_eq]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
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))
      (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
have 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
Tactic: rw [LinearEquiv.coe_trans, ofTensorProduct_eq, LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
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))
      (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
have 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
Tactic: nth_rw 2 [← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Finite ι
⊢ Function.Bijective (α := 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))) :
      (a : AdicCompletion I R ⊗[R] (ι → R)) → AdicCompletion I (ι → R))
have intro : ∀ (val : Fintype ι),
  Function.Bijective (α := 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))) :
      (a : AdicCompletion I R ⊗[R] (ι → R)) → AdicCompletion I (ι → R))
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Finite ι
⊢ Function.Bijective (α := 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))) :
      (a : AdicCompletion I R ⊗[R] (ι → R)) → AdicCompletion I (ι → R))
have intro : ∀ (val : Fintype ι),
  Function.Bijective (α := 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))) :
      (a : AdicCompletion I R ⊗[R] (ι → R)) → AdicCompletion I (ι → R))
Tactic: classical
  cases nonempty_fintype ι
  exact EquivLike.bijective (ofTensorProductEquivOfPiFintype I ι)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (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
inst_3 : Module.Finite R M
⊢ Function.Surjective (α := AdicCompletion I R ⊗[R] M) (β := AdicCompletion I M)
    (⇑(ofTensorProduct I M) : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M)
have obtain : ∀ (n : ℕ) (p : (Fin n → R) →ₗ[R] M)
  (hp : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑p : (a : Fin n → R) → M)),
  Function.Surjective (α := AdicCompletion I R ⊗[R] M) (β := AdicCompletion I M)
    (⇑(ofTensorProduct I M) : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M)
Tactic: obtain ⟨n, p, hp⟩ := Module.Finite.exists_fin' R M
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (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
inst_3 : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑p : (a : Fin n → R) → M)
f : LinearMap.{u_1, u_1, u_1, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
  (AdicCompletion I R ⊗[R] (Fin n → R)) (AdicCompletion I M) :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : LinearMap.{u_1, u_1, u_1, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
  (AdicCompletion I R ⊗[R] (Fin n → R)) (AdicCompletion I M) :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
⊢ f = g
have a : ∀ (i : Fin n) (n_1 : ℕ),
  Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n_1) ⊤)
    ((↑(((((AlgebraTensorModule.curry f :
                        LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R)
                          (LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) (Fin n → R) (AdicCompletion I M))) :
                      (a : AdicCompletion I R) → (Fin n → R) →ₗ[R] AdicCompletion I M)
                    1 ∘ₗ
                  LinearMap.single R (fun (i : Fin n) ↦ R) i :
                LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) R (AdicCompletion I M)) :
              (a : R) → AdicCompletion I M)
            1) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      n_1)
    ((↑(((((AlgebraTensorModule.curry g :
                        LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R)
                          (LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) (Fin n → R) (AdicCompletion I M))) :
                      (a : AdicCompletion I R) → (Fin n → R) →ₗ[R] AdicCompletion I M)
                    1 ∘ₗ
                  LinearMap.single R (fun (i : Fin n) ↦ R) i :
                LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) R (AdicCompletion I M)) :
              (a : R) → AdicCompletion I M)
            1) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      n_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑p : (a : Fin n → R) → M)
f : LinearMap.{u_1, u_1, u_1, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
  (AdicCompletion I R ⊗[R] (Fin n → R)) (AdicCompletion I M) :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : LinearMap.{u_1, u_1, u_1, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
  (AdicCompletion I R ⊗[R] (Fin n → R)) (AdicCompletion I M) :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
⊢ Function.Surjective (α := AdicCompletion I R ⊗[R] M) (β := AdicCompletion I M)
    (⇑(ofTensorProduct I M) : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M)
have hfg : f = g
Tactic: have hfg : f = g := by
    ext
    simp [f, g]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (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
inst_3 : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑p : (a : Fin n → R) → M)
f : LinearMap.{u_1, u_1, u_1, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
  (AdicCompletion I R ⊗[R] (Fin n → R)) (AdicCompletion I M) :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : LinearMap.{u_1, u_1, u_1, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
  (AdicCompletion I R ⊗[R] (Fin n → R)) (AdicCompletion I M) :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := AdicCompletion I R ⊗[R] (Fin n → R)) (β := AdicCompletion I M)
    (⇑f : (a : AdicCompletion I R ⊗[R] (Fin n → R)) → AdicCompletion I M)
have simp : Function.Surjective.{u_1 + 1, u_2 + 1} (α := AdicCompletion I R ⊗[R] (Fin n → R)) (β := AdicCompletion I M)
  (Function.comp (β := AdicCompletion I (Fin n → R))
    (⇑(map I p) : (a : AdicCompletion I (Fin n → R)) → AdicCompletion I M)
    (⇑(ofTensorProduct I (Fin n → R) :
          LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (Fin n → R))
            (AdicCompletion I (Fin n → R))) :
      (a : AdicCompletion I R ⊗[R] (Fin n → R)) → AdicCompletion I (Fin n → R)))
Tactic: simp only [hfg, LinearMap.coe_comp, g]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (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
inst_3 : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑p : (a : Fin n → R) → M)
f : LinearMap.{u_1, u_1, u_1, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
  (AdicCompletion I R ⊗[R] (Fin n → R)) (AdicCompletion I M) :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : LinearMap.{u_1, u_1, u_1, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
  (AdicCompletion I R ⊗[R] (Fin n → R)) (AdicCompletion I M) :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := AdicCompletion I R ⊗[R] (Fin n → R)) (β := AdicCompletion I M)
    (Function.comp (β := AdicCompletion I (Fin n → R))
      (⇑(map I p) : (a : AdicCompletion I (Fin n → R)) → AdicCompletion I M)
      (⇑(ofTensorProduct I (Fin n → R) :
            LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (Fin n → R))
              (AdicCompletion I (Fin n → R))) :
        (a : AdicCompletion I R ⊗[R] (Fin n → R)) → AdicCompletion I (Fin n → R)))
have hg : Function.Surjective.{u_1 + 1, u_2 + 1} (α := AdicCompletion I (Fin n → R)) (β := AdicCompletion I M)
  (⇑(map I p) : (a : AdicCompletion I (Fin n → R)) → AdicCompletion I M)
Tactic: apply Function.Surjective.comp
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (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
inst_3 : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑p : (a : Fin n → R) → M)
f : LinearMap.{u_1, u_1, u_1, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
  (AdicCompletion I R ⊗[R] (Fin n → R)) (AdicCompletion I M) :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : LinearMap.{u_1, u_1, u_1, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
  (AdicCompletion I R ⊗[R] (Fin n → R)) (AdicCompletion I M) :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
hg :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := AdicCompletion I (Fin n → R)) (β := AdicCompletion I M)
    (⇑(map I p) : (a : AdicCompletion I (Fin n → R)) → AdicCompletion I M)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := AdicCompletion I R ⊗[R] (Fin n → R)) (β := AdicCompletion I M)
    (Function.comp (β := AdicCompletion I (Fin n → R))
      (⇑(map I p) : (a : AdicCompletion I (Fin n → R)) → AdicCompletion I M)
      (⇑(ofTensorProduct I (Fin n → R) :
            LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (Fin n → R))
              (AdicCompletion I (Fin n → R))) :
        (a : AdicCompletion I R ⊗[R] (Fin n → R)) → AdicCompletion I (Fin n → R)))
have hf : Function.Surjective (α := AdicCompletion I R ⊗[R] (Fin n → R)) (β := AdicCompletion I (Fin n → R))
  (⇑(ofTensorProduct I (Fin n → R) :
        LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] (Fin n → R))
          (AdicCompletion I (Fin n → R))) :
    (a : AdicCompletion I R ⊗[R] (Fin n → R)) → AdicCompletion I (Fin n → R))
Tactic: apply Function.Surjective.comp