awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
⊢ Eq.{w + 1} (α := N)
    (var
      (solution₂.postcomp
        ((Finsupp.linearCombination A fun (g₁ : relations₁.G) ↦
              h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ } :
            (a : relations₁.G →₀ A) → M₂ →ₗ[A] N)
          (relations₁.relation r₁)))
      g₂)
    (var (solution₂.postcomp 0) g₂)
have var : Eq.{w + 1} (α := N)
  ((((Finsupp.linearCombination A fun (g₁ : relations₁.G) ↦
                h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := sorry } :
              (a : relations₁.G →₀ A) → M₂ →ₗ[A] N)
            (relations₁.relation r₁) :
          M₂ →ₗ[A] N) :
        (a : M₂) → N)
      (solution₂.var g₂) :
    N)
  (0 : N)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
⊢ Eq.{w + 1} (α := N)
    ((((Finsupp.linearCombination A fun (g₁ : relations₁.G) ↦
                  h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ } :
                (a : relations₁.G →₀ A) → M₂ →ₗ[A] N)
              (relations₁.relation r₁) :
            M₂ →ₗ[A] N) :
          (a : M₂) → N)
        (solution₂.var g₂) :
      N)
    (0 : N)
have var : Eq.{w + 1} (α := N)
  ((Finsupp.linearCombination A
          (Function.comp (β := M₂ →ₗ[A] N)
            (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
              (a : M₂ →ₗ[A] N) → N)
            fun (g₁ : relations₁.G) ↦
            h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := sorry }) :
        (a : relations₁.G →₀ A) → N)
      (relations₁.relation r₁) :
    N)
  (0 : N)
Tactic: erw [Finsupp.apply_linearCombination A (LinearMap.applyₗ (solution₂.var g₂))]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (hypothesis)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (Function.comp (β := M₂ →ₗ[A] N)
              (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
                (a : M₂ →ₗ[A] N) → N)
              fun (g₁ : relations₁.G) ↦
              h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)
have this : Eq.{w + 1} (α := N)
  ((Finsupp.linearCombination A s.var : (a : (relations₁.tensor relations₂).G →₀ A) → N)
      ((relations₁.tensor relations₂).relation (Sum.inl (r₁, g₂))) :
    N)
  (0 : N)
Tactic: have := s.linearCombination_var_relation (.inl ⟨r₁, g₂⟩)
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (hypothesis)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
this :
  Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A s.var : (a : (relations₁.tensor relations₂).G →₀ A) → N)
        ((relations₁.tensor relations₂).relation (Sum.inl (r₁, g₂))) :
      N)
    (0 : N)
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (Function.comp (β := M₂ →ₗ[A] N)
              (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
                (a : M₂ →ₗ[A] N) → N)
              fun (g₁ : relations₁.G) ↦
              h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)
have this₁ : Eq.{w + 1} (α := N)
  ((Finsupp.linearCombination A
          (s.var ∘
            (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G)) :
        (a : relations₁.G →₀ A) → N)
      (relations₁.relation r₁) :
    N)
  (0 : N)
Tactic: erw [Finsupp.linearCombination_embDomain] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
this :
  Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (s.var ∘
              (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G)) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (Function.comp (β := M₂ →ₗ[A] N)
              (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
                (a : M₂ →ₗ[A] N) → N)
              fun (g₁ : relations₁.G) ↦
              h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)
have h : Eq (α := relations₁.G → N)
  (Function.comp (β := M₂ →ₗ[A] N)
    (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
      (a : M₂ →ₗ[A] N) → N)
    fun (g₁ : relations₁.G) ↦
    h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := sorry })
  (s.var ∘ (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G))
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
this :
  Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (s.var ∘
              (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G)) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)
⊢ Eq (α := relations₁.G → N)
    (Function.comp (β := M₂ →ₗ[A] N)
      (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
        (a : M₂ →ₗ[A] N) → N)
      fun (g₁ : relations₁.G) ↦
      h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ })
    (s.var ∘ (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G))
have h : ∀ (g₁ : relations₁.G),
  Function.comp (β := M₂ →ₗ[A] N)
      (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
        (a : M₂ →ₗ[A] N) → N)
      (fun (g₁ : relations₁.G) ↦
        h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := sorry })
      g₁ =
    (s.var ∘ (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G)) g₁
Tactic: ext g₁
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
f f' : M₁ ⊗[A] M₂ →ₗ[A] N
h : (solution₁.tensor solution₂).postcomp f = (solution₁.tensor solution₂).postcomp f'
⊢ Eq (α := relations₁.Solution (M₂ →ₗ[A] N))
    (solution₁.postcomp
      (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f))
    (solution₁.postcomp
      (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f'))
have var : ∀ (g₁ : relations₁.G),
  Eq (α := M₂ →ₗ[A] N)
    (var
      (solution₁.postcomp
        (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f))
      g₁)
    (var
      (solution₁.postcomp
        (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f'))
      g₁)
Tactic: ext g₁ : 2
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
f f' : M₁ ⊗[A] M₂ →ₗ[A] N
h : (solution₁.tensor solution₂).postcomp f = (solution₁.tensor solution₂).postcomp f'
g₁ : relations₁.G
⊢ Eq (α := M₂ →ₗ[A] N)
    (var
      (solution₁.postcomp
        (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f))
      g₁)
    (var
      (solution₁.postcomp
        (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f'))
      g₁)
have var : Eq (α := relations₂.Solution N)
  (solution₂.postcomp
    (var
      (solution₁.postcomp
        (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f))
      g₁))
  (solution₂.postcomp
    (var
      (solution₁.postcomp
        (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f'))
      g₁))
Tactic: refine h₂.postcomp_injective ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
f f' : M₁ ⊗[A] M₂ →ₗ[A] N
h : (solution₁.tensor solution₂).postcomp f = (solution₁.tensor solution₂).postcomp f'
g₁ : relations₁.G
⊢ Eq (α := relations₂.Solution N)
    (solution₂.postcomp
      (var
        (solution₁.postcomp
          (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f))
        g₁))
    (solution₂.postcomp
      (var
        (solution₁.postcomp
          (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f'))
        g₁))
have var : ∀ (g₂ : relations₂.G),
  Eq.{w + 1} (α := N)
    (var
      (solution₂.postcomp
        (var
          (solution₁.postcomp
            (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f))
          g₁))
      g₂)
    (var
      (solution₂.postcomp
        (var
          (solution₁.postcomp
            (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f'))
          g₁))
      g₂)
Tactic: ext g₂
-- Lean 4 proof step from Mathlib.Algebra.Module.Prod (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x x_1 : R
x_2 : M × N
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2
have fst : ((x + x_1) • x_2).1 = (x • x_2 + x_1 • x_2).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Prod (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x x_1 : R
x_2 : M × N
fst : ((x + x_1) • x_2).1 = (x • x_2 + x_1 • x_2).1
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2
have snd : ((x + x_1) • x_2).2 = (x • x_2 + x_1 • x_2).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Prod (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : M × N
⊢ HSMul.hSMul (α := R) 0 x = 0
have fst : (HSMul.hSMul (α := R) 0 x).1 = 0.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Prod (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : M × N
fst : (HSMul.hSMul (α := R) 0 x).1 = 0.1
⊢ HSMul.hSMul (α := R) 0 x = 0
have snd : (HSMul.hSMul (α := R) 0 x).2 = 0.2
Tactic: ext
-- 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
⊢ Projective R P ↔ ∃ (s : P →ₗ[R] P →₀ R), linearCombination R id ∘ₗ s = LinearMap.id
have simp_rw : (∃ (s : P →ₗ[R] P →₀ R),
    Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P)
      (⇑s : (a : P) → P →₀ R)) ↔
  ∃ (s : P →ₗ[R] P →₀ R), linearCombination R id ∘ₗ s = LinearMap.id
Tactic: simp_rw [projective_def, DFunLike.ext_iff, Function.LeftInverse, comp_apply, 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
simp_rw :
  (∃ (s : P →ₗ[R] P →₀ R),
      Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P)
        (⇑s : (a : P) → P →₀ R)) ↔
    ∃ (s : P →ₗ[R] P →₀ R), linearCombination R id ∘ₗ s = LinearMap.id
⊢ Projective R P ↔ ∃ (s : P →ₗ[R] P →₀ R), linearCombination R id ∘ₗ s = LinearMap.id
have simp_rw₁ : (∃ (s : P →ₗ[R] P →₀ R),
    Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P)
      (⇑s : (a : P) → P →₀ R)) ↔
  ∃ (s : P →ₗ[R] P →₀ R),
    ∀ (x : P), Eq (α := P) ((linearCombination R id ∘ₗ s : (a : P) → P) x : P) ((LinearMap.id : (a : P) → P) x : P)
Tactic: simp_rw [projective_def, DFunLike.ext_iff, Function.LeftInverse, comp_apply, 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
simp_rw :
  (∃ (s : P →ₗ[R] P →₀ R),
      Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P)
        (⇑s : (a : P) → P →₀ R)) ↔
    ∃ (s : P →ₗ[R] P →₀ R), linearCombination R id ∘ₗ s = LinearMap.id
simp_rw₁ :
  (∃ (s : P →ₗ[R] P →₀ R),
      Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P)
        (⇑s : (a : P) → P →₀ R)) ↔
    ∃ (s : P →ₗ[R] P →₀ R),
      ∀ (x : P), Eq (α := P) ((linearCombination R id ∘ₗ s : (a : P) → P) x : P) ((LinearMap.id : (a : P) → P) x : P)
⊢ Projective R P ↔ ∃ (s : P →ₗ[R] P →₀ R), linearCombination R id ∘ₗ s = LinearMap.id
have simp_rw₂ : (∃ (s : P →ₗ[R] P →₀ R),
    ∀ (x : P), (linearCombination R id : (a : P →₀ R) → P) ((s : (a : P) → P →₀ R) x : P →₀ R) = x) ↔
  ∃ (s : P →ₗ[R] P →₀ R),
    ∀ (x : P), Eq (α := P) ((linearCombination R id ∘ₗ s : (a : P) → P) x : P) ((LinearMap.id : (a : P) → P) x : P)
Tactic: simp_rw [projective_def, DFunLike.ext_iff, Function.LeftInverse, comp_apply, 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
simp_rw :
  (∃ (s : P →ₗ[R] P →₀ R),
      Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P)
        (⇑s : (a : P) → P →₀ R)) ↔
    ∃ (s : P →ₗ[R] P →₀ R), linearCombination R id ∘ₗ s = LinearMap.id
simp_rw₁ :
  (∃ (s : P →ₗ[R] P →₀ R),
      Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P)
        (⇑s : (a : P) → P →₀ R)) ↔
    ∃ (s : P →ₗ[R] P →₀ R),
      ∀ (x : P), Eq (α := P) ((linearCombination R id ∘ₗ s : (a : P) → P) x : P) ((LinearMap.id : (a : P) → P) x : P)
simp_rw₂ :
  (∃ (s : P →ₗ[R] P →₀ R),
      ∀ (x : P), (linearCombination R id : (a : P →₀ R) → P) ((s : (a : P) → P →₀ R) x : P →₀ R) = x) ↔
    ∃ (s : P →ₗ[R] P →₀ R),
      ∀ (x : P), Eq (α := P) ((linearCombination R id ∘ₗ s : (a : P) → P) x : P) ((LinearMap.id : (a : P) → P) x : P)
⊢ Projective R P ↔ ∃ (s : P →ₗ[R] P →₀ R), linearCombination R id ∘ₗ s = LinearMap.id
have simp_rw₃ : (∃ (s : P →ₗ[R] P →₀ R),
    ∀ (x : P), (linearCombination R id : (a : P →₀ R) → P) ((s : (a : P) → P →₀ R) x : P →₀ R) = x) ↔
  ∃ (s : P →ₗ[R] P →₀ R),
    ∀ (x : P),
      Eq.{u_2 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) ((s : (a : P) → P →₀ R) x : P →₀ R) : P)
        ((LinearMap.id : (a : P) → P) x : P)
Tactic: simp_rw [projective_def, DFunLike.ext_iff, Function.LeftInverse, comp_apply, 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
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun (p : P) ↦ Function.surjInv hf ((g : (a : P) → N) p)
⊢ ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
have obtain : ∀ (s : P →ₗ[R] P →₀ R)
  (hs :
    Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P) (⇑s : (a : P) → P →₀ R)),
  ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
Tactic: obtain ⟨s, hs⟩ := h.out
-- 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
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun (p : P) ↦ Function.surjInv hf ((g : (a : P) → N) p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P) (⇑s : (a : P) → P →₀ R)
⊢ ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
have h₁ : f ∘ₗ φ ∘ₗ s = g
Tactic: use φ.comp s
-- 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
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun (p : P) ↦ Function.surjInv hf ((g : (a : P) → N) p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P) (⇑s : (a : P) → P →₀ R)
⊢ f ∘ₗ φ ∘ₗ s = g
have h₁ : ∀ (p : P), Eq.{u_4 + 1} (α := N) ((f ∘ₗ φ ∘ₗ s : (a : P) → N) p : N) ((g : (a : P) → N) p : N)
Tactic: ext p
-- 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
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun (p : P) ↦ Function.surjInv hf ((g : (a : P) → N) p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P) (⇑s : (a : P) → P →₀ R)
p : P
| ((g : (a : P) → N) p : N)
have rw : ((g : (a : P) → N) ((linearCombination R id : (a : P →₀ R) → P) ((s : (a : P) → P →₀ R) p : P →₀ R) : P) : N)
Tactic: rw [← hs p]
-- 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
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun (p : P) ↦ Function.surjInv hf ((g : (a : P) → N) p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P) (⇑s : (a : P) → P →₀ R)
p : P
⊢ Eq.{u_4 + 1} (α := N) ((f ∘ₗ φ ∘ₗ s : (a : P) → N) p : N) ((g : (a : P) → N) p : N)
have h₁ : Eq.{u_4 + 1} (α := N) ((f ∘ₗ φ ∘ₗ s : (a : P) → N) p : N)
  ((g : (a : P) → N) ((linearCombination R id : (a : P →₀ R) → P) ((s : (a : P) → P →₀ R) p : P →₀ R) : P) : N)
Tactic: conv_rhs => rw [← hs p]
-- 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
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
inst_9 : Projective R P
inst_10 : Projective R Q
⊢ Projective R (P × Q)
have refine : ∀ (f : (P × Q →₀ R) →ₗ[R] P × Q)
  (hf : Function.Surjective (α := P × Q →₀ R) (β := P × Q) (⇑f : (a : P × Q →₀ R) → P × Q)),
  ∃ (h : P × Q →ₗ[R] P × Q →₀ R), f ∘ₗ h = LinearMap.id
Tactic: refine .of_lifting_property'' fun f hf ↦ ?_