awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
x : P
rw : (linearCombination R id : (a : P →₀ R) → P) ((g : (a : M) → P →₀ R) ((i : (a : P) → M) x) : P →₀ R) = x
rw₁ : (linearCombination R id ∘ₗ g : (a : M) → P) ((i : (a : P) → M) x : M) = x
rw₂ : (s : (a : M) → P) ((i : (a : P) → M) x : M) = x
rw₃ : (s ∘ₗ i : (a : P) → P) x = x
⊢ (linearCombination R id : (a : P →₀ R) → P) ((g ∘ₗ i : (a : P) → P →₀ R) x : P →₀ R) = x
have rw₄ : (LinearMap.id : (a : P) → P) x = x
Tactic: rw [LinearMap.comp_apply, ← LinearMap.comp_apply, hg,
    ← LinearMap.comp_apply, H, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
x : P
rw : (linearCombination R id : (a : P →₀ R) → P) ((g : (a : M) → P →₀ R) ((i : (a : P) → M) x) : P →₀ R) = x
rw₁ : (linearCombination R id ∘ₗ g : (a : M) → P) ((i : (a : P) → M) x : M) = x
rw₂ : (s : (a : M) → P) ((i : (a : P) → M) x : M) = x
rw₃ : (s ∘ₗ i : (a : P) → P) x = x
rw₄ : (LinearMap.id : (a : P) → P) x = x
⊢ (linearCombination R id : (a : P →₀ R) → P) ((g ∘ₗ i : (a : P) → P →₀ R) x : P →₀ R) = x
have rw₅ : x = x
Tactic: rw [LinearMap.comp_apply, ← LinearMap.comp_apply, hg,
    ← LinearMap.comp_apply, H, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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 σ σ'
⊢ Projective S N
have obtain : ∀ (f : M →ₗ[R] M →₀ R)
  (hf :
    Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑f : (a : M) → M →₀ R)),
  Projective S N
Tactic: obtain ⟨f, hf⟩ := ‹Projective R M›
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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
hf : Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑f : (a : M) → M →₀ R)
x y : 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 + y)))) =
    HAdd.hAdd (α := N →₀ S)
      (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))))
      (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) y))))
have h : ∀ (a : N),
  Eq.{u_9 + 1} (α := S)
    ((mapRange (⇑e₁ : (a : R) → S) sorry
            ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
              ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) (x + y)))) :
          (a : N) → S)
        a :
      S)
    ((HAdd.hAdd (α := N →₀ S)
            (mapRange (⇑e₁ : (a : R) → S) sorry
              ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
                ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) x))))
            (mapRange (⇑e₁ : (a : R) → S) sorry
              ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
                ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) y)))) :
          (a : N) → S)
        a :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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
hf : Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑f : (a : M) → M →₀ R)
r : S
v : 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) (r • v)))) =
    HSMul.hSMul (α := S) (β := N →₀ S) ((RingHom.id S : (a : S) → S) r : S)
      (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) v))))
have h : ∀ (i : N),
  Eq.{u_9 + 1} (α := S)
    ((mapRange (⇑e₁ : (a : R) → S) sorry
            ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
              ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) (r • v)))) :
          (a : N) → S)
        i :
      S)
    ((HSMul.hSMul (α := S) (β := N →₀ S) ((RingHom.id S : (a : S) → S) r : S)
            (mapRange (⇑e₁ : (a : R) → S) sorry
              ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
                ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) v)))) :
          (a : N) → S)
        i :
      S)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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
hf : Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑f : (a : M) → 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' := ⋯ }
⊢ Projective S N
have refine : ∀ (x : N), (linearCombination S id : (a : N →₀ S) → N) ((g : (a : N) → N →₀ S) x : N →₀ S) = x
Tactic: refine ⟨⟨g, fun x ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (hypothesis)
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
hf : Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑f : (a : M) → 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
⊢ (linearCombination S id : (a : N →₀ S) → N) ((g : (a : N) → N →₀ S) x : N →₀ S) = x
have 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)
Tactic: replace hf := congr(e₂ $(hf (e₂.symm x)))
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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
have 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
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⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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)
⊢ (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
have 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)
Tactic: apply LinearMap.ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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 (α := 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)
have 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)
Tactic: simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, e.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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
⊢ Projective R (M ⊗[R₀] N)
have 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)
Tactic: obtain ⟨sM, hsM⟩ := hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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)
⊢ Projective R (M ⊗[R₀] N)
have 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)
Tactic: obtain ⟨sN, hsN⟩ := hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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₀))
have i : M ⊗[R₀] (N →₀ R₀) →ₗ[R] (M →₀ R) ⊗[R₀] (N →₀ R₀)
Tactic: fapply Projective.of_split (R := R) (M := ((M →₀ R) ⊗[R₀] (N →₀ R₀)))
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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₀)
⊢ Projective R (M ⊗[R₀] (N →₀ R₀))
have s : (M →₀ R) ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀)
Tactic: fapply Projective.of_split (R := R) (M := ((M →₀ R) ⊗[R₀] (N →₀ R₀)))
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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₀)
⊢ Projective R (M ⊗[R₀] (N →₀ R₀))
have 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₀))
Tactic: fapply Projective.of_split (R := R) (M := ((M →₀ R) ⊗[R₀] (N →₀ R₀)))
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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₀)
⊢ 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₀))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (hypothesis)
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)
have this : 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 _]
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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₀))
⊢ Projective R (M ⊗[R₀] N)
have i : M ⊗[R₀] N →ₗ[R] M ⊗[R₀] (N →₀ R₀)
Tactic: fapply Projective.of_split (R := R) (M := (M ⊗[R₀] (N →₀ R₀)))
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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₀)
⊢ Projective R (M ⊗[R₀] N)
have s : M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] N
Tactic: fapply Projective.of_split (R := R) (M := (M ⊗[R₀] (N →₀ R₀)))
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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
⊢ Projective R (M ⊗[R₀] N)
have 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)
Tactic: fapply Projective.of_split (R := R) (M := (M ⊗[R₀] (N →₀ R₀)))
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
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₀))
⊢ 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)
have H : ∀ (x : M) (x_1 : N),
  Eq (α := M ⊗[R₀] N)
    (((((AlgebraTensorModule.curry
                    ((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) :
                (a : M) → N →ₗ[R₀] M ⊗[R₀] N)
              x :
            N →ₗ[R₀] M ⊗[R₀] N) :
          (a : N) → M ⊗[R₀] N)
        x_1 :
      M ⊗[R₀] N)
    (((((AlgebraTensorModule.curry LinearMap.id : M →ₗ[R] N →ₗ[R₀] M ⊗[R₀] N) : (a : M) → N →ₗ[R₀] M ⊗[R₀] N) x :
            N →ₗ[R₀] M ⊗[R₀] N) :
          (a : N) → M ⊗[R₀] N)
        x_1 :
      M ⊗[R₀] N)
Tactic: ext