-- Mathlib/Algebra/Module/Projective.lean
theorem projective_lifting_property [h : Projective R P] (f : M →ₗ[R] N) (g : P →ₗ[R] N)
    (hf : Function.Surjective f) : ∃ h : P →ₗ[R] M, f ∘ₗ h = g

Proof state:
case h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p => Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
⊢ f ∘ₗ φ ∘ₗ s = g

Tactic:
ext p

Result:
case h.h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p => Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
p : P
⊢ (f ∘ₗ φ ∘ₗ s) p = g p

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ ∃ h, f ∘ₗ h = g

Tactic:
let φ : (P →₀ R) →ₗ[R] M := Finsupp.linearCombination _ fun p => Function.surjInv hf (g p)

Result:
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p => Function.surjInv hf (g p)
⊢ ∃ h, f ∘ₗ h = g

Proof state:
case h.h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p => Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
p : P
⊢ (f ∘ₗ φ ∘ₗ s) p = g ((linearCombination R id) (s p))

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

Result:
no goals

Proof state:
case h.h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p => Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
p : P
⊢ (f ∘ₗ φ ∘ₗ s) p = g p

Tactic:
conv_rhs => rw [← hs p]

Result:
case h.h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p => Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
p : P
⊢ (f ∘ₗ φ ∘ₗ s) p = g ((linearCombination R id) (s p))

Proof state:
case intro
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p => Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
⊢ ∃ h, f ∘ₗ h = g

Tactic:
use φ.comp s

Result:
case h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p => Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
⊢ f ∘ₗ φ ∘ₗ s = g

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p => Function.surjInv hf (g p)
⊢ ∃ h, f ∘ₗ h = g

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

Result:
case intro
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p => Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
⊢ ∃ h, f ∘ₗ h = g