-- Mathlib/Algebra/Category/ModuleCat/Projective.lean
theorem IsProjective.iff_projective {R : Type u} [Ring R] {P : Type max u v} [AddCommGroup P]
    [Module R P] : Module.Projective R P ↔ Projective (ModuleCat.of R P)

Proof state:
case refine_1.intro
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h✝ : Module.Projective R P
this : Module.Projective R ↑(of R P) := h✝
E✝ X✝ : ModuleCat R
E : of R P ⟶ X✝
X : E✝ ⟶ X✝
epi : Epi X
f : ↑(of R P) →ₗ[R] ↑E✝
h : Hom.hom X ∘ₗ f = Hom.hom E
⊢ ∃ f', f' ≫ X = E

Tactic:
exact ⟨ofHom f, hom_ext h⟩

Result:
no goals

Proof state:
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
⊢ Module.Projective R P ↔ Projective (of R P)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Module.Projective R P
⊢ Projective (of R P)

case refine_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
⊢ Module.Projective R P

Proof state:
case refine_1
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Module.Projective R P
this : Module.Projective R ↑(of R P) := h
E✝ X✝ : ModuleCat R
E : of R P ⟶ X✝
X : E✝ ⟶ X✝
epi : Epi X
⊢ ∃ f', f' ≫ X = E

Tactic:
obtain ⟨f, h⟩ := Module.projective_lifting_property X.hom E.hom
  ((ModuleCat.epi_iff_surjective _).mp epi)

Result:
case refine_1.intro
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h✝ : Module.Projective R P
this : Module.Projective R ↑(of R P) := h✝
E✝ X✝ : ModuleCat R
E : of R P ⟶ X✝
X : E✝ ⟶ X✝
epi : Epi X
f : ↑(of R P) →ₗ[R] ↑E✝
h : Hom.hom X ∘ₗ f = Hom.hom E
⊢ ∃ f', f' ≫ X = E

Proof state:
case refine_1
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Module.Projective R P
this : Module.Projective R ↑(of R P) := h
⊢ Projective (of R P)

Tactic:
refine ⟨fun E X epi => ?_⟩

Result:
case refine_1
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Module.Projective R P
this : Module.Projective R ↑(of R P) := h
E✝ X✝ : ModuleCat R
E : of R P ⟶ X✝
X : E✝ ⟶ X✝
epi : Epi X
⊢ ∃ f', f' ≫ X = E

Proof state:
case refine_1
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Module.Projective R P
⊢ Projective (of R P)

Tactic:
letI : Module.Projective R (ModuleCat.of R P) := h

Result:
case refine_1
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Module.Projective R P
this : Module.Projective R ↑(of R P) := h
⊢ Projective (of R P)

Proof state:
case refine_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
⊢ Module.Projective R P

Tactic:
refine Module.Projective.of_lifting_property.{u,v} ?_

Result:
case refine_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
⊢ ∀ {M : Type (max v u)} {N : Type (max u v)} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Module R M]
    [inst_3 : Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g

Proof state:
case refine_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
E : Type (max v u)
X : Type (max u v)
mE : AddCommGroup E
mX : AddCommGroup X
sE : Module R E
sX : Module R X
f : E →ₗ[R] X
g : P →ₗ[R] X
s : Function.Surjective ⇑f
this : Epi (↟f)
⊢ ∃ h, f ∘ₗ h = g

Tactic:
letI : Projective (ModuleCat.of R P) := h

Result:
case refine_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
E : Type (max v u)
X : Type (max u v)
mE : AddCommGroup E
mX : AddCommGroup X
sE : Module R E
sX : Module R X
f : E →ₗ[R] X
g : P →ₗ[R] X
s : Function.Surjective ⇑f
this✝ : Epi (↟f)
this : Projective (of R P) := h
⊢ ∃ h, f ∘ₗ h = g

Proof state:
case refine_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
E : Type (max v u)
X : Type (max u v)
mE : AddCommGroup E
mX : AddCommGroup X
sE : Module R E
sX : Module R X
f : E →ₗ[R] X
g : P →ₗ[R] X
s : Function.Surjective ⇑f
⊢ ∃ h, f ∘ₗ h = g

Tactic:
haveI : Epi (↟f) := (ModuleCat.epi_iff_surjective (↟f)).mpr s

Result:
case refine_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
E : Type (max v u)
X : Type (max u v)
mE : AddCommGroup E
mX : AddCommGroup X
sE : Module R E
sX : Module R X
f : E →ₗ[R] X
g : P →ₗ[R] X
s : Function.Surjective ⇑f
this : Epi (↟f)
⊢ ∃ h, f ∘ₗ h = g

Proof state:
case refine_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
⊢ ∀ {M : Type (max v u)} {N : Type (max u v)} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Module R M]
    [inst_3 : Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g

Tactic:
intro E X mE mX sE sX f g s

Result:
case refine_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
E : Type (max v u)
X : Type (max u v)
mE : AddCommGroup E
mX : AddCommGroup X
sE : Module R E
sX : Module R X
f : E →ₗ[R] X
g : P →ₗ[R] X
s : Function.Surjective ⇑f
⊢ ∃ h, f ∘ₗ h = g

Proof state:
case refine_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
E : Type (max v u)
X : Type (max u v)
mE : AddCommGroup E
mX : AddCommGroup X
sE : Module R E
sX : Module R X
f : E →ₗ[R] X
g : P →ₗ[R] X
s : Function.Surjective ⇑f
this✝ : Epi (↟f)
this : Projective (of R P) := h
⊢ ∃ h, f ∘ₗ h = g

Tactic:
exact ⟨(Projective.factorThru (↟g) (↟f)).hom,
  ModuleCat.hom_ext_iff.mp <| Projective.factorThru_comp (↟g) (↟f)⟩

Result:
no goals