awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
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
var :
  Eq (α := relations₂.Solution N)
    (solution₂.postcomp
      (Solution.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
      (Solution.var
        (solution₁.postcomp
          (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f'))
        g₁))
⊢ Eq (α := M₂ →ₗ[A] N)
    (Solution.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.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 ?_

Premises used: Module.Relations.Solution.IsPresentation.postcomp_injective
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
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
var :
  ∀ (g₂ : relations₂.G),
    Eq.{w + 1} (α := N)
      (Solution.var
        (solution₂.postcomp
          (Solution.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₂)
      (Solution.var
        (solution₂.postcomp
          (Solution.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₂)
⊢ Eq (α := relations₂.Solution N)
    (solution₂.postcomp
      (Solution.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
      (Solution.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₂
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
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
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:
congr_var h ⟨g₁, g₂⟩

Premises used: Prod.mk, TensorProduct.tmul, Module.Relations.Solution.congr_var, AddCon.toQuotient
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
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
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:
exact congr_var h ⟨g₁, g₂⟩

Premises used: Prod.mk, Module.Relations.Solution.congr_var
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
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
⊢ (solution₁.tensor solution₂).IsPresentation

Tactic:
(isPresentationCoreTensor h₁ h₂).isPresentation

Premises used: Module.Relations.Solution.isPresentationCoreTensor, Module.Relations.Solution.IsPresentationCore.isPresentation
-- Module: Mathlib.Algebra.Module.Prod
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
snd : ((x + x_1) • x_2).2 = (x • x_2 + x_1 • x_2).2
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Prod
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).1 = (x • x_2 + x_1 • x_2).1

Tactic:
add_smul ..

Premises used: add_smul
-- Module: Mathlib.Algebra.Module.Prod
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).1 = (x • x_2 + x_1 • x_2).1

Tactic:
exact add_smul ..

Premises used: add_smul
-- Module: Mathlib.Algebra.Module.Prod
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).2 = (x • x_2 + x_1 • x_2).2

Tactic:
add_smul ..

Premises used: add_smul
-- Module: Mathlib.Algebra.Module.Prod
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).2 = (x • x_2 + x_1 • x_2).2

Tactic:
exact add_smul ..

Premises used: add_smul
-- Module: Mathlib.Algebra.Module.Prod
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
snd : (HSMul.hSMul (α := R) 0 x).2 = 0.2
⊢ HSMul.hSMul (α := R) 0 x = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Prod
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).1 = 0.1

Tactic:
zero_smul ..

Premises used: zero_smul
-- Module: Mathlib.Algebra.Module.Prod
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).1 = 0.1

Tactic:
exact zero_smul ..

Premises used: zero_smul
-- Module: Mathlib.Algebra.Module.Prod
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).2 = 0.2

Tactic:
zero_smul ..

Premises used: zero_smul
-- Module: Mathlib.Algebra.Module.Prod
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).2 = 0.2

Tactic:
exact zero_smul ..

Premises used: zero_smul
-- 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
⊢ Projective R P ↔
    ∃ (s : P →ₗ[R] P →₀ R),
      Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P) (⇑s : (a : P) → P →₀ R)

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: Module.Projective.mk, Iff.intro, Module.Projective.out
-- 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
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)
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)
⊢ Projective R P ↔ ∃ (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]

Premises used: Function.LeftInverse, LinearMap.id_apply, LinearMap.comp_apply, DFunLike.ext_iff, Module.projective_def
-- 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
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)
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
⊢ ∃ (h : P →ₗ[R] M), f ∘ₗ h = g

Tactic:
obtain ⟨s, hs⟩ := h.out

Premises used: Module.Projective.out
-- 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
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₁ : f ∘ₗ φ ∘ₗ s = g
⊢ ∃ (h : P →ₗ[R] M), f ∘ₗ h = g

Tactic:
use φ.comp s

Premises used: LinearMap.comp
-- 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
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 : P), Eq.{u_4 + 1} (α := N) ((f ∘ₗ φ ∘ₗ s : (a : P) → N) p : N) ((g : (a : P) → N) p : N)
⊢ f ∘ₗ φ ∘ₗ s = g

Tactic:
ext p
-- 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
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
rw : ((g : (a : P) → N) ((linearCombination R id : (a : P →₀ R) → P) ((s : (a : P) → P →₀ R) p : P →₀ R) : P) : N)
| ((g : (a : P) → N) p : N)

Tactic:
rw [← hs p]
-- 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
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
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)
⊢ Eq.{u_4 + 1} (α := N) ((f ∘ₗ φ ∘ₗ s : (a : P) → N) p : N) ((g : (a : P) → N) p : N)

Tactic:
conv_rhs => rw [← hs p]
-- 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
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) ((linearCombination R id : (a : P →₀ R) → P) ((s : (a : P) → P →₀ R) p : P →₀ R) : P) : N)

Tactic:
simp [φ, Finsupp.linearCombination_apply, Function.surjInv_eq hf, map_finsuppSum]

Premises used: Finsupp.linearCombination_apply, Function.surjInv_eq, map_finsuppSum
-- 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 P
f : M →ₗ[R] P
hf_surj : f.range = ⊤
⊢ ∃ (g : P →ₗ[R] M), f ∘ₗ g = LinearMap.id

Tactic:
projective_lifting_property f (.id : P →ₗ[R] P) (LinearMap.range_eq_top.1 hf_surj)

Premises used: LinearMap.id, LinearMap.range_eq_top, Iff.mp, Module.projective_lifting_property
-- 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
inst_7 : Projective R P
f : M →ₗ[R] P
hf_surj : Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
⊢ Surjective (β := N →ₗ[R] P) fun (g : N →ₗ[R] M) ↦ f ∘ₗ g

Tactic:
surjective_comp_left_of_exists_rightInverse <|
    f.exists_rightInverse_of_surjective <| range_eq_top_of_surjective f hf_surj

Premises used: LinearMap.range_eq_top_of_surjective, LinearMap.exists_rightInverse_of_surjective, LinearMap.surjective_comp_left_of_exists_rightInverse
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
huniv :
  ∀ (f : (P →₀ R) →ₗ[R] P),
    Function.Surjective (α := P →₀ R) (β := P) (⇑f : (a : P →₀ R) → P) → ∃ (h : P →ₗ[R] P →₀ R), f ∘ₗ h = LinearMap.id
⊢ Projective R P

Tactic:
projective_def'.2 <| huniv (Finsupp.linearCombination R (id : P → P))
    (linearCombination_surjective _ Function.surjective_id)

Premises used: Iff.mpr, id, Module.projective_def', Function.surjective_id, Finsupp.linearCombination_surjective, Finsupp.linearCombination
-- 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
inst_9 : Projective R P
inst_10 : Projective R Q
⊢ Projective R (P × Q)

Tactic:
.of_lifting_property'' fun f hf ↦ ?_

Premises used: Module.Projective.of_lifting_property''
-- 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
inst_9 : Projective R P
inst_10 : Projective R Q
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
⊢ Projective R (P × Q)

Tactic:
refine .of_lifting_property'' fun f hf ↦ ?_
-- 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
inst_9 : Projective R P
inst_10 : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective (α := P × Q →₀ R) (β := P × Q) (⇑f : (a : P × Q →₀ R) → P × Q)
rcases : ∀ (g₁ : P →ₗ[R] P × Q →₀ R) (hg₁ : f ∘ₗ g₁ = inl R P Q), ∃ (h : P × Q →ₗ[R] P × Q →₀ R), f ∘ₗ h = LinearMap.id
⊢ ∃ (h : P × Q →ₗ[R] P × Q →₀ R), f ∘ₗ h = LinearMap.id

Tactic:
rcases projective_lifting_property f (.inl _ _ _) hf with ⟨g₁, hg₁⟩

Premises used: LinearMap.inl, Module.projective_lifting_property
-- 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
inst_9 : Projective R P
inst_10 : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective (α := P × Q →₀ R) (β := P × Q) (⇑f : (a : P × Q →₀ R) → P × Q)
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
rcases : ∀ (g₂ : Q →ₗ[R] P × Q →₀ R) (hg₂ : f ∘ₗ g₂ = inr R P Q), ∃ (h : P × Q →ₗ[R] P × Q →₀ R), f ∘ₗ h = LinearMap.id
⊢ ∃ (h : P × Q →ₗ[R] P × Q →₀ R), f ∘ₗ h = LinearMap.id

Tactic:
rcases projective_lifting_property f (.inr _ _ _) hf with ⟨g₂, hg₂⟩

Premises used: Module.projective_lifting_property, LinearMap.inr
-- 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
inst_9 : Projective R P
inst_10 : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective (α := P × Q →₀ R) (β := P × Q) (⇑f : (a : P × Q →₀ R) → P × Q)
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : f ∘ₗ g₂ = inr R P Q
⊢ ∃ (h : P × Q →ₗ[R] P × Q →₀ R), f ∘ₗ h = LinearMap.id

Tactic:
⟨coprod g₁ g₂, ?_⟩

Premises used: LinearMap.coprod, Exists.intro
-- 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
inst_9 : Projective R P
inst_10 : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective (α := P × Q →₀ R) (β := P × Q) (⇑f : (a : P × Q →₀ R) → P × Q)
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : f ∘ₗ g₂ = inr R P Q
refine : f ∘ₗ g₁.coprod g₂ = LinearMap.id
⊢ ∃ (h : P × Q →ₗ[R] P × Q →₀ R), f ∘ₗ h = LinearMap.id

Tactic:
refine ⟨coprod g₁ g₂, ?_⟩
-- 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
inst_9 : Projective R P
inst_10 : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective (α := P × Q →₀ R) (β := P × Q) (⇑f : (a : P × Q →₀ R) → P × Q)
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : f ∘ₗ g₂ = inr R P Q
rw : (f ∘ₗ g₁).coprod (f ∘ₗ g₂) = LinearMap.id
rw₁ : coprod (inl R P Q) (f ∘ₗ g₂) = LinearMap.id
rw₂ : Eq (α := P × Q →ₗ[R] P × Q) (coprod (inl R P Q) (inr R P Q)) LinearMap.id
rw₃ rw₄ : Eq (α := P × Q →ₗ[R] P × Q) LinearMap.id LinearMap.id
⊢ f ∘ₗ g₁.coprod g₂ = LinearMap.id

Tactic:
rw [LinearMap.comp_coprod, hg₁, hg₂, LinearMap.coprod_inl_inr]

Premises used: LinearMap.coprod_inl_inr, LinearMap.comp_coprod
-- 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)
h : ∀ (i : ι), Projective.{u_1, u_7} R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf :
  Function.Surjective (α := (Π₀ (i : ι), A i) →₀ R) (β := Π₀ (i : ι), A i)
    (⇑f : (a : (Π₀ (i : ι), A i) →₀ R) → Π₀ (i : ι), A i)
choose :
  ∀ (g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R) (hg : ∀ (i : ι), f ∘ₗ g i = DFinsupp.lsingle (M := A) i),
    ∃ (h : (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) →₀ R), f ∘ₗ h = LinearMap.id
⊢ ∃ (h : (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) →₀ R), f ∘ₗ h = LinearMap.id

Tactic:
choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf

Premises used: Module.projective_lifting_property, DFinsupp.lsingle