awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
      (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:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Finite ι
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))
⊢ 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 ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Finite ι
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:
EquivLike.bijective (ofTensorProductEquivOfPiFintype I ι)

Premises used: AdicCompletion.ofTensorProductEquivOfPiFintype, EquivLike.bijective
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Finite ι
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:
exact EquivLike.bijective (ofTensorProductEquivOfPiFintype I ι)

Premises used: AdicCompletion.ofTensorProductEquivOfPiFintype, EquivLike.bijective
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
ι : Type u_4
inst_1 : Finite ι
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))
⊢ 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 ι)

Premises used: nonempty_fintype
-- 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
inst_3 : Module.Finite R M
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)
⊢ 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

Premises used: Module.Finite.exists_fin'
-- 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
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)
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)
⊢ f = g

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
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)
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:
simp [f, g]
-- 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
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

Tactic:
have hfg : f = g := by
    ext
    simp [f, g]
-- 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
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
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)))
⊢ 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)

Tactic:
simp only [hfg, LinearMap.coe_comp, g]

Premises used: LinearMap.coe_comp
-- 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
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)
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))
⊢ 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:
apply Function.Surjective.comp

Premises used: Function.Surjective.comp
-- 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
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 (Fin n → R)) (β := AdicCompletion I M)
    (⇑(map I p) : (a : AdicCompletion I (Fin n → R)) → AdicCompletion I M)

Tactic:
AdicCompletion.map_surjective I hp

Premises used: AdicCompletion.map_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
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 (Fin n → R)) (β := AdicCompletion I M)
    (⇑(map I p) : (a : AdicCompletion I (Fin n → R)) → AdicCompletion I M)

Tactic:
exact AdicCompletion.map_surjective I hp

Premises used: AdicCompletion.map_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
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 (α := 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:
(ofTensorProduct_bijective_of_pi_of_fintype I (Fin n)).surjective

Premises used: AdicCompletion.ofTensorProduct_bijective_of_pi_of_fintype, Function.Bijective.surjective, Fin
-- 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
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 (α := 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:
exact (ofTensorProduct_bijective_of_pi_of_fintype I (Fin n)).surjective

Premises used: AdicCompletion.ofTensorProduct_bijective_of_pi_of_fintype, Function.Bijective.surjective, Fin
-- 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
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)

Tactic:
have hf : Function.Surjective f := by
    simp only [hfg, LinearMap.coe_comp, g]
    apply Function.Surjective.comp
    · exact AdicCompletion.map_surjective I hp
    · exact (ofTensorProduct_bijective_of_pi_of_fintype I (Fin n)).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
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
hf :
  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)
⊢ Function.Surjective (α := AdicCompletion I R ⊗[R] M) (β := AdicCompletion I M)
    (⇑(ofTensorProduct I M) : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M)

Tactic:
Function.Surjective.of_comp hf

Premises used: Function.Surjective.of_comp
-- 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
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
hf :
  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)
⊢ Function.Surjective (α := AdicCompletion I R ⊗[R] M) (β := AdicCompletion I M)
    (⇑(ofTensorProduct I M) : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M)

Tactic:
exact Function.Surjective.of_comp hf

Premises used: Function.Surjective.of_comp
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective (α := ι → R) (β := M) (⇑f : (a : ι → R) → M)
⊢ Function.Exact (M := AdicCompletion I R ⊗[R] ↥f.ker) (N := AdicCompletion I R ⊗[R] (ι → R)) (P :=
    AdicCompletion I R ⊗[R] M)
    (⇑(lTensorKerIncl I M f) : (a : AdicCompletion I R ⊗[R] ↥f.ker) → AdicCompletion I R ⊗[R] (ι → R))
    (⇑(lTensorf I M f) : (a : AdicCompletion I R ⊗[R] (ι → R)) → AdicCompletion I R ⊗[R] M)

Tactic:
lTensor_exact (AdicCompletion I R) (f.exact_subtype_ker_map) hf

Premises used: lTensor_exact, LinearMap.exact_subtype_ker_map, AdicCompletion, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective (α := ι → R) (β := M) (⇑f : (a : ι → R) → M)
⊢ Function.Surjective (α := AdicCompletion I R ⊗[R] (ι → R)) (β := AdicCompletion I R ⊗[R] M)
    (⇑(lTensorf I M f) : (a : AdicCompletion I R ⊗[R] (ι → R)) → AdicCompletion I R ⊗[R] M)

Tactic:
LinearMap.lTensor_surjective (AdicCompletion I R) hf

Premises used: LinearMap.lTensor_surjective, AdicCompletion, TensorProduct.tmul, AddCon.toQuotient