awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_8
S : Type u_9
inst : Semiring R
inst_1 : Semiring S
M : Type u_10
N : Type u_11
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module S N
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst_8 : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
g : N →ₗ[S] N →₀ S :=
  {
    toFun := fun (x : N) ↦
      mapRange (⇑e₁ : (a : R) → S) ⋯
        ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
          ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) x))),
    map_add' := ⋯, map_smul' := ⋯ }
x : N
hf :
  Eq.{u_11 + 1} (α := N)
    ((e₂ : (a : M) → N)
        ((linearCombination R id : (a : M →₀ R) → M) ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) x) : M →₀ R) :
          M) :
      N)
    ((e₂ : (a : M) → N) ((e₂.symm : (a : N) → M) x : M) : N)
⊢ (linearCombination S id : (a : N →₀ S) → N) ((g : (a : N) → N →₀ S) x : N →₀ S) = x

Tactic:
simpa [linearCombination_apply, sum_mapRange_index, g, map_finsuppSum, e₂.map_smulₛₗ] using hf

Premises used: LinearEquiv.map_smulₛₗ, Finsupp.linearCombination_apply, map_finsuppSum, Finsupp.sum_mapRange_index
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_1
inst : Semiring R
P : Type u_2
inst_1 : AddCommMonoid P
inst_2 : Module R P
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Projective R M
e : M ≃ₗ[R] P
⊢ Projective R P

Tactic:
.of_equiv e

Premises used: Module.Projective.of_equiv
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_1
inst : Semiring R
P : Type u_2
inst_1 : AddCommMonoid P
inst_2 : Module R P
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
Q : Type u_5
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
ι : Type u_6
A : ι → Type u_7
inst_9 : (i : ι) → AddCommMonoid (A i)
inst_10 : (i : ι) → Module.{u_1, u_7} R (A i)
inst_11 : Projective R M
⊢ Projective R (ULift.{w, u_3} M)

Tactic:
Projective.of_equiv' ULift.moduleEquiv.symm

Premises used: LinearEquiv.symm, ULift.moduleEquiv, Module.Projective.of_equiv'
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_1
inst : Semiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Projective R (ULift.{w, u_3} M)
⊢ Projective R M

Tactic:
Projective.of_equiv' ULift.moduleEquiv

Premises used: ULift.moduleEquiv, Module.Projective.of_equiv'
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_1
inst : Semiring R
P : Type u_2
inst_1 : AddCommMonoid P
inst_2 : Module R P
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
Q : Type u_5
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
ι : Type u_6
A : ι → Type u_7
inst_9 : (i : ι) → AddCommMonoid (A i)
inst_10 : (i : ι) → Module.{u_1, u_7} R (A i)
inst_11 : Small.{w, u_3} M
inst_12 : Projective R M
⊢ Projective.{u_1, w} R (Shrink.{w, u_3} M)

Tactic:
Projective.of_equiv' (Shrink.linearEquiv R M).symm

Premises used: LinearEquiv.symm, Module.Projective.of_equiv', Shrink.linearEquiv
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_1
inst : Semiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{w, u_3} M
inst_4 : Projective.{u_1, w} R (Shrink.{w, u_3} M)
⊢ Projective R M

Tactic:
Projective.of_equiv' (Shrink.linearEquiv R M)

Premises used: Module.Projective.of_equiv', Shrink.linearEquiv
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_1
inst : Semiring R
P : Type u_2
inst_1 : AddCommMonoid P
inst_2 : Module R P
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Projective R M
s : M →ₗ[R] P
hs : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := P) (⇑s : (a : M) → P)
⊢ Projective R P ↔ ∃ (i : P →ₗ[R] M), s ∘ₗ i = LinearMap.id

Tactic:
⟨fun _ ↦ projective_lifting_property _ _ hs, fun ⟨i, H⟩ ↦ Projective.of_split i s H⟩

Premises used: LinearMap.id, Module.Projective, _private.0.Module.Projective.iff_split_of_projective.match_1, Iff.intro, Module.projective_lifting_property, Module.Projective.of_split
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{w, u} R
inst_4 : Small.{w, v} P
e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
  mapDomain.linearEquiv (Shrink.{w, u} R) R (Equiv.symm (equivShrink P)) ≪≫ₗ
    mapRange.linearEquiv (Shrink.linearEquiv R R)
⊢ Projective R P ↔
    ∃ (M : Type w) (x : AddCommMonoid M) (x_1 : Module R M) (_ : Free R M) (i : P →ₗ[R] M) (s : M →ₗ[R] P),
      s ∘ₗ i = LinearMap.id

Tactic:
⟨fun ⟨i, hi⟩ ↦ ⟨(Shrink.{w} P) →₀ (Shrink.{w} R), _, _, Free.of_basis ⟨e⟩,
    e.symm.toLinearMap ∘ₗ i, (linearCombination R id) ∘ₗ e.toLinearMap, ?_⟩,
      fun ⟨_, _, _, _, i, s, H⟩ ↦ Projective.of_split i s H⟩

Premises used: LinearMap.id, Module.Basis.ofRepr, _private.0.Module.Projective.iff_split'.match_1, LinearEquiv.symm, Finsupp.module, Module.Projective, Exists, id, _private.0.Module.Projective.iff_split'.match_2, Finsupp.instAddCommMonoid, LinearMap.comp, Module.Free.of_basis, LinearEquiv.toLinearMap, Iff.intro, Exists.intro, Shrink, Module.Projective.of_split, Finsupp.linearCombination, Eq, Finsupp
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{w, u} R
inst_4 : Small.{w, v} P
e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
  mapDomain.linearEquiv (Shrink.{w, u} R) R (Equiv.symm (equivShrink P)) ≪≫ₗ
    mapRange.linearEquiv (Shrink.linearEquiv R R)
refine :
  Projective R P →
    ∀ (i : P →ₗ[R] P →₀ R)
      (hi :
        Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P)
          (⇑i : (a : P) → P →₀ R)),
      (linearCombination R id ∘ₗ (↑e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) →ₗ[R] P →₀ R)) ∘ₗ
          (↑e.symm : (P →₀ R) →ₗ[R] Shrink.{w, v} P →₀ Shrink.{w, u} R) ∘ₗ i =
        LinearMap.id
⊢ Projective R P ↔
    ∃ (M : Type w) (x : AddCommMonoid M) (x_1 : Module R M) (_ : Free R M) (i : P →ₗ[R] M) (s : M →ₗ[R] P),
      s ∘ₗ i = LinearMap.id

Tactic:
refine ⟨fun ⟨i, hi⟩ ↦ ⟨(Shrink.{w} P) →₀ (Shrink.{w} R), _, _, Free.of_basis ⟨e⟩,
    e.symm.toLinearMap ∘ₗ i, (linearCombination R id) ∘ₗ e.toLinearMap, ?_⟩,
      fun ⟨_, _, _, _, i, s, H⟩ ↦ Projective.of_split i s H⟩
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{w, u} R
inst_4 : Small.{w, v} P
e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
  mapDomain.linearEquiv (Shrink.{w, u} R) R (Equiv.symm (equivShrink P)) ≪≫ₗ
    mapRange.linearEquiv (Shrink.linearEquiv R R)
h_1 : Projective R P
i : P →ₗ[R] P →₀ R
hi : Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P) (⇑i : (a : P) → P →₀ R)
h :
  ∀ (x : P),
    Eq (α := P)
      (((linearCombination R id ∘ₗ (↑e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) →ₗ[R] P →₀ R)) ∘ₗ
              (↑e.symm : (P →₀ R) →ₗ[R] Shrink.{w, v} P →₀ Shrink.{w, u} R) ∘ₗ i :
            (a : P) → P)
          x :
        P)
      ((LinearMap.id : (a : P) → P) x : P)
⊢ (linearCombination R id ∘ₗ (↑e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) →ₗ[R] P →₀ R)) ∘ₗ
      (↑e.symm : (P →₀ R) →ₗ[R] Shrink.{w, v} P →₀ Shrink.{w, u} R) ∘ₗ i =
    LinearMap.id

Tactic:
apply LinearMap.ext

Premises used: LinearMap.ext
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{w, u} R
inst_4 : Small.{w, v} P
e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
  mapDomain.linearEquiv (Shrink.{w, u} R) R (Equiv.symm (equivShrink P)) ≪≫ₗ
    mapRange.linearEquiv (Shrink.linearEquiv R R)
h_1 : Projective R P
i : P →ₗ[R] P →₀ R
hi : Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P) (⇑i : (a : P) → P →₀ R)
h :
  ∀ (x : P),
    Eq.{v + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) ((i : (a : P) → P →₀ R) x : P →₀ R) : P)
      ((LinearMap.id : (a : P) → P) x : P)
⊢ ∀ (x : P),
    Eq (α := P)
      (((linearCombination R id ∘ₗ (↑e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) →ₗ[R] P →₀ R)) ∘ₗ
              (↑e.symm : (P →₀ R) →ₗ[R] Shrink.{w, v} P →₀ Shrink.{w, u} R) ∘ₗ i :
            (a : P) → P)
          x :
        P)
      ((LinearMap.id : (a : P) → P) x : P)

Tactic:
simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, e.apply_symm_apply]

Premises used: LinearMap.coe_comp, LinearEquiv.apply_symm_apply, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{w, u} R
inst_4 : Small.{w, v} P
e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
  mapDomain.linearEquiv (Shrink.{w, u} R) R (Equiv.symm (equivShrink P)) ≪≫ₗ
    mapRange.linearEquiv (Shrink.linearEquiv R R)
h : Projective R P
i : P →ₗ[R] P →₀ R
hi : Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P) (⇑i : (a : P) → P →₀ R)
⊢ ∀ (x : P),
    Eq.{v + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) ((i : (a : P) → P →₀ R) x : P →₀ R) : P)
      ((LinearMap.id : (a : P) → P) x : P)

Tactic:
hi

Premises used: Function.LeftInverse
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{w, u} R
inst_4 : Small.{w, v} P
e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
  mapDomain.linearEquiv (Shrink.{w, u} R) R (Equiv.symm (equivShrink P)) ≪≫ₗ
    mapRange.linearEquiv (Shrink.linearEquiv R R)
h : Projective R P
i : P →ₗ[R] P →₀ R
hi : Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P) (⇑i : (a : P) → P →₀ R)
⊢ ∀ (x : P),
    Eq.{v + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) ((i : (a : P) → P →₀ R) x : P →₀ R) : P)
      ((LinearMap.id : (a : P) → P) x : P)

Tactic:
exact hi
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
⊢ Projective R P ↔
    ∃ (M : Type (max u v)) (x : AddCommMonoid M) (x_1 : Module R M) (_ : Free R M) (i : P →ₗ[R] M) (s : M →ₗ[R] P),
      s ∘ₗ i = LinearMap.id

Tactic:
Projective.iff_split'.{max u v}

Premises used: Module.Projective.iff_split'
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
hM : Projective R M
hN : Projective R₀ N
obtain :
  ∀ (sM : M →ₗ[R] M →₀ R)
    (hsM :
      Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M)
        (⇑sM : (a : M) → M →₀ R)),
    Projective R (M ⊗[R₀] N)
⊢ Projective R (M ⊗[R₀] N)

Tactic:
obtain ⟨sM, hsM⟩ := hM
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
hN : Projective R₀ N
sM : M →ₗ[R] M →₀ R
hsM :
  Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑sM : (a : M) → M →₀ R)
obtain :
  ∀ (sN : N →ₗ[R₀] N →₀ R₀)
    (hsN :
      Function.LeftInverse (α := N) (β := N →₀ R₀) (⇑(linearCombination R₀ id) : (a : N →₀ R₀) → N)
        (⇑sN : (a : N) → N →₀ R₀)),
    Projective R (M ⊗[R₀] N)
⊢ Projective R (M ⊗[R₀] N)

Tactic:
obtain ⟨sN, hsN⟩ := hN
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM :
  Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑sM : (a : M) → M →₀ R)
sN : N →ₗ[R₀] N →₀ R₀
hsN :
  Function.LeftInverse (α := N) (β := N →₀ R₀) (⇑(linearCombination R₀ id) : (a : N →₀ R₀) → N)
    (⇑sN : (a : N) → N →₀ R₀)
i : M ⊗[R₀] (N →₀ R₀) →ₗ[R] (M →₀ R) ⊗[R₀] (N →₀ R₀)
s : (M →₀ R) ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀)
H :
  Eq (α := M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀))
    ((AlgebraTensorModule.map (linearCombination R id) LinearMap.id :
          (M →₀ R) ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀)) ∘ₗ
        (AlgebraTensorModule.map sM LinearMap.id : M ⊗[R₀] (N →₀ R₀) →ₗ[R] (M →₀ R) ⊗[R₀] (N →₀ R₀)) :
      M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀))
    (LinearMap.id : M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀))
⊢ Projective R (M ⊗[R₀] (N →₀ R₀))

Tactic:
fapply Projective.of_split (R := R) (M := ((M →₀ R) ⊗[R₀] (N →₀ R₀)))

Premises used: Module.Projective.of_split
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM :
  Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑sM : (a : M) → M →₀ R)
sN : N →ₗ[R₀] N →₀ R₀
hsN :
  Function.LeftInverse (α := N) (β := N →₀ R₀) (⇑(linearCombination R₀ id) : (a : N →₀ R₀) → N)
    (⇑sN : (a : N) → N →₀ R₀)
⊢ M ⊗[R₀] (N →₀ R₀) →ₗ[R] (M →₀ R) ⊗[R₀] (N →₀ R₀)

Tactic:
exact (AlgebraTensorModule.map sM (LinearMap.id (R := R₀) (M := N →₀ R₀)))

Premises used: LinearMap.id, TensorProduct.AlgebraTensorModule.map
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM :
  Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑sM : (a : M) → M →₀ R)
sN : N →ₗ[R₀] N →₀ R₀
hsN :
  Function.LeftInverse (α := N) (β := N →₀ R₀) (⇑(linearCombination R₀ id) : (a : N →₀ R₀) → N)
    (⇑sN : (a : N) → N →₀ R₀)
⊢ (M →₀ R) ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀)

Tactic:
exact (AlgebraTensorModule.map
        (Finsupp.linearCombination R id) (LinearMap.id (R := R₀) (M := N →₀ R₀)))

Premises used: LinearMap.id, id, Finsupp.linearCombination, TensorProduct.AlgebraTensorModule.map
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM :
  Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑sM : (a : M) → M →₀ R)
sN : N →ₗ[R₀] N →₀ R₀
hsN :
  Function.LeftInverse (α := N) (β := N →₀ R₀) (⇑(linearCombination R₀ id) : (a : N →₀ R₀) → N)
    (⇑sN : (a : N) → N →₀ R₀)
H :
  ∀ (x : M) (a : N),
    Eq (α := M ⊗[R₀] (N →₀ R₀))
      ((((AlgebraTensorModule.curry
                    ((AlgebraTensorModule.map (linearCombination R id) LinearMap.id :
                        (M →₀ R) ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀)) ∘ₗ
                      (AlgebraTensorModule.map sM LinearMap.id : M ⊗[R₀] (N →₀ R₀) →ₗ[R] (M →₀ R) ⊗[R₀] (N →₀ R₀))) :
                  M →ₗ[R] (N →₀ R₀) →ₗ[R₀] M ⊗[R₀] (N →₀ R₀)) :
                (a : M) → (N →₀ R₀) →ₗ[R₀] M ⊗[R₀] (N →₀ R₀))
              x ∘ₗ
            lsingle a :
          (a : R₀) → M ⊗[R₀] (N →₀ R₀))
        1)
      ((((AlgebraTensorModule.curry LinearMap.id : M →ₗ[R] (N →₀ R₀) →ₗ[R₀] M ⊗[R₀] (N →₀ R₀)) :
                (a : M) → (N →₀ R₀) →ₗ[R₀] M ⊗[R₀] (N →₀ R₀))
              x ∘ₗ
            lsingle a :
          (a : R₀) → M ⊗[R₀] (N →₀ R₀))
        1)
⊢ Eq (α := M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀))
    ((AlgebraTensorModule.map (linearCombination R id) LinearMap.id :
          (M →₀ R) ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀)) ∘ₗ
        (AlgebraTensorModule.map sM LinearMap.id : M ⊗[R₀] (N →₀ R₀) →ₗ[R] (M →₀ R) ⊗[R₀] (N →₀ R₀)) :
      M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀))
    (LinearMap.id : M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀))

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM :
  Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑sM : (a : M) → M →₀ R)
sN : N →ₗ[R₀] N →₀ R₀
hsN :
  Function.LeftInverse (α := N) (β := N →₀ R₀) (⇑(linearCombination R₀ id) : (a : N →₀ R₀) → N)
    (⇑sN : (a : N) → N →₀ R₀)
x : M
a : N
⊢ Eq (α := M ⊗[R₀] (N →₀ R₀))
    ((((AlgebraTensorModule.curry
                  ((AlgebraTensorModule.map (linearCombination R id) LinearMap.id :
                      (M →₀ R) ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀)) ∘ₗ
                    (AlgebraTensorModule.map sM LinearMap.id : M ⊗[R₀] (N →₀ R₀) →ₗ[R] (M →₀ R) ⊗[R₀] (N →₀ R₀))) :
                M →ₗ[R] (N →₀ R₀) →ₗ[R₀] M ⊗[R₀] (N →₀ R₀)) :
              (a : M) → (N →₀ R₀) →ₗ[R₀] M ⊗[R₀] (N →₀ R₀))
            x ∘ₗ
          lsingle a :
        (a : R₀) → M ⊗[R₀] (N →₀ R₀))
      1)
    ((((AlgebraTensorModule.curry LinearMap.id : M →ₗ[R] (N →₀ R₀) →ₗ[R₀] M ⊗[R₀] (N →₀ R₀)) :
              (a : M) → (N →₀ R₀) →ₗ[R₀] M ⊗[R₀] (N →₀ R₀))
            x ∘ₗ
          lsingle a :
        (a : R₀) → M ⊗[R₀] (N →₀ R₀))
      1)

Tactic:
simp [hsM _]
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM :
  Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑sM : (a : M) → M →₀ R)
sN : N →ₗ[R₀] N →₀ R₀
hsN :
  Function.LeftInverse (α := N) (β := N →₀ R₀) (⇑(linearCombination R₀ id) : (a : N →₀ R₀) → N)
    (⇑sN : (a : N) → N →₀ R₀)
⊢ Projective R (M ⊗[R₀] (N →₀ R₀))

Tactic:
have : Module.Projective R (M ⊗[R₀] (N →₀ R₀)) := by
    fapply Projective.of_split (R := R) (M := ((M →₀ R) ⊗[R₀] (N →₀ R₀)))
    · exact (AlgebraTensorModule.map sM (LinearMap.id (R := R₀) (M := N →₀ R₀)))
    · exact (AlgebraTensorModule.map
        (Finsupp.linearCombination R id) (LinearMap.id (R := R₀) (M := N →₀ R₀)))
    · ext; simp [hsM _]
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM :
  Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑sM : (a : M) → M →₀ R)
sN : N →ₗ[R₀] N →₀ R₀
hsN :
  Function.LeftInverse (α := N) (β := N →₀ R₀) (⇑(linearCombination R₀ id) : (a : N →₀ R₀) → N)
    (⇑sN : (a : N) → N →₀ R₀)
this : Projective R (M ⊗[R₀] (N →₀ R₀))
i : M ⊗[R₀] N →ₗ[R] M ⊗[R₀] (N →₀ R₀)
s : M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] N
H :
  Eq (α := M ⊗[R₀] N →ₗ[R] M ⊗[R₀] N)
    ((AlgebraTensorModule.map LinearMap.id (linearCombination R₀ id) : M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] N) ∘ₗ
        (AlgebraTensorModule.map LinearMap.id sN : M ⊗[R₀] N →ₗ[R] M ⊗[R₀] (N →₀ R₀)) :
      M ⊗[R₀] N →ₗ[R] M ⊗[R₀] N)
    (LinearMap.id : M ⊗[R₀] N →ₗ[R] M ⊗[R₀] N)
⊢ Projective R (M ⊗[R₀] N)

Tactic:
fapply Projective.of_split (R := R) (M := (M ⊗[R₀] (N →₀ R₀)))

Premises used: Module.Projective.of_split
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM :
  Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑sM : (a : M) → M →₀ R)
sN : N →ₗ[R₀] N →₀ R₀
hsN :
  Function.LeftInverse (α := N) (β := N →₀ R₀) (⇑(linearCombination R₀ id) : (a : N →₀ R₀) → N)
    (⇑sN : (a : N) → N →₀ R₀)
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ M ⊗[R₀] N →ₗ[R] M ⊗[R₀] (N →₀ R₀)

Tactic:
exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) sN)

Premises used: LinearMap.id, TensorProduct.AlgebraTensorModule.map
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM :
  Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑sM : (a : M) → M →₀ R)
sN : N →ₗ[R₀] N →₀ R₀
hsN :
  Function.LeftInverse (α := N) (β := N →₀ R₀) (⇑(linearCombination R₀ id) : (a : N →₀ R₀) → N)
    (⇑sN : (a : N) → N →₀ R₀)
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] N

Tactic:
exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) (linearCombination R₀ id))

Premises used: LinearMap.id, id, Finsupp.linearCombination, TensorProduct.AlgebraTensorModule.map