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
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)
⊢ ∃ (h : P × Q →ₗ[R] P × Q →₀ R), f ∘ₗ h = LinearMap.id
have 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
Tactic: rcases projective_lifting_property f (.inl _ _ _) hf with ⟨g₁, hg₁⟩
-- 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
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
⊢ ∃ (h : P × Q →ₗ[R] P × Q →₀ R), f ∘ₗ h = LinearMap.id
have 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
Tactic: rcases projective_lifting_property f (.inr _ _ _) hf with ⟨g₂, hg₂⟩
-- 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
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
have refine : f ∘ₗ g₁.coprod g₂ = LinearMap.id
Tactic: refine ⟨coprod g₁ g₂, ?_⟩
-- 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
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
⊢ f ∘ₗ g₁.coprod g₂ = LinearMap.id
have rw : (f ∘ₗ g₁).coprod (f ∘ₗ g₂) = LinearMap.id
Tactic: rw [LinearMap.comp_coprod, hg₁, hg₂, LinearMap.coprod_inl_inr]
-- 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
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
⊢ f ∘ₗ g₁.coprod g₂ = LinearMap.id
have rw₁ : coprod (inl R P Q) (f ∘ₗ g₂) = LinearMap.id
Tactic: rw [LinearMap.comp_coprod, hg₁, hg₂, LinearMap.coprod_inl_inr]
-- 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
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
⊢ f ∘ₗ g₁.coprod g₂ = LinearMap.id
have rw₂ : Eq (α := P × Q →ₗ[R] P × Q) (coprod (inl R P Q) (inr R P Q)) LinearMap.id
Tactic: rw [LinearMap.comp_coprod, hg₁, hg₂, LinearMap.coprod_inl_inr]
-- 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
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
⊢ f ∘ₗ g₁.coprod g₂ = LinearMap.id
have rw₃ : Eq (α := P × Q →ₗ[R] P × Q) LinearMap.id LinearMap.id
Tactic: rw [LinearMap.comp_coprod, hg₁, hg₂, LinearMap.coprod_inl_inr]
-- 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
ι : 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)
⊢ ∃ (h : (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) →₀ R), f ∘ₗ h = LinearMap.id
have 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
Tactic: choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (hypothesis)
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)
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
have hg₁ : ∀ (i : ι) (x : A i),
  Eq (α := Π₀ (i : ι), A i)
    ((f : (a : (Π₀ (i : ι), A i) →₀ R) → Π₀ (i : ι), A i) ((g i : (a : A i) → (Π₀ (i : ι), A i) →₀ R) x) :
      Π₀ (i : ι), A i)
    (DFinsupp.single (β := A) i x : Π₀ (i : ι), A i)
Tactic: replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ DFunLike.congr_fun (hg i)
Cleared hypotheses: hg
-- 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
ι : 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)
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg :
  ∀ (i : ι) (x : A i),
    Eq (α := Π₀ (i : ι), A i)
      ((f : (a : (Π₀ (i : ι), A i) →₀ R) → Π₀ (i : ι), A i) ((g i : (a : A i) → (Π₀ (i : ι), A i) →₀ R) x) :
        Π₀ (i : ι), A i)
      (DFinsupp.single (β := A) i x : Π₀ (i : ι), A i)
⊢ ∃ (h : (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) →₀ R), f ∘ₗ h = LinearMap.id
have refine : f ∘ₗ DFinsupp.coprodMap (M := A) g = LinearMap.id
Tactic: refine ⟨DFinsupp.coprodMap g, ?_⟩
-- 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
ι : 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)
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg :
  ∀ (i : ι) (x : A i),
    Eq (α := Π₀ (i : ι), A i)
      ((f : (a : (Π₀ (i : ι), A i) →₀ R) → Π₀ (i : ι), A i) ((g i : (a : A i) → (Π₀ (i : ι), A i) →₀ R) x) :
        Π₀ (i : ι), A i)
      (DFinsupp.single (β := A) i x : Π₀ (i : ι), A i)
⊢ f ∘ₗ DFinsupp.coprodMap (M := A) g = LinearMap.id
have h₁ : ∀ (i : ι) (x : A i) (j : ι),
  ((((f ∘ₗ DFinsupp.coprodMap (M := A) g) ∘ₗ DFinsupp.lsingle (M := A) i : (a : A i) → Π₀ (i : ι), A i) x :
          Π₀ (i : ι), A i) :
        (a : ι) → A a)
      j =
    (((LinearMap.id ∘ₗ DFinsupp.lsingle (M := A) i : (a : A i) → Π₀ (i : ι), A i) x : Π₀ (i : ι), A i) : (a : ι) → A a)
      j
Tactic: ext i x j
-- 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
ι : 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)
⊢ ∃ (h : (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) →₀ R), f ∘ₗ h = LinearMap.id
have 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
Tactic: classical
      choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
      replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ DFunLike.congr_fun (hg i)
      refine ⟨DFinsupp.coprodMap g, ?_⟩
      ext i x j
      simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]
-- 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
ι : 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
have choose₁ : ∀ (g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R)
  (hg :
    ∀ (i : ι) (x : A i),
      Eq (α := Π₀ (i : ι), A i)
        ((f : (a : (Π₀ (i : ι), A i) →₀ R) → Π₀ (i : ι), A i) ((g i : (a : A i) → (Π₀ (i : ι), A i) →₀ R) x) :
          Π₀ (i : ι), A i)
        (DFinsupp.single (β := A) i x : Π₀ (i : ι), A i)),
  ∃ (h : (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) →₀ R), f ∘ₗ h = LinearMap.id
Tactic: classical
      choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
      replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ DFunLike.congr_fun (hg i)
      refine ⟨DFinsupp.coprodMap g, ?_⟩
      ext i x j
      simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]
-- 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
ι : 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
choose₁ :
  ∀ (g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R)
    (hg :
      ∀ (i : ι) (x : A i),
        Eq (α := Π₀ (i : ι), A i)
          ((f : (a : (Π₀ (i : ι), A i) →₀ R) → Π₀ (i : ι), A i) ((g i : (a : A i) → (Π₀ (i : ι), A i) →₀ R) x) :
            Π₀ (i : ι), A i)
          (DFinsupp.single (β := A) i x : Π₀ (i : ι), 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
have choose₂ : ∀ (g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R)
  (hg :
    ∀ (i : ι) (x : A i),
      Eq (α := Π₀ (i : ι), A i)
        ((f : (a : (Π₀ (i : ι), A i) →₀ R) → Π₀ (i : ι), A i) ((g i : (a : A i) → (Π₀ (i : ι), A i) →₀ R) x) :
          Π₀ (i : ι), A i)
        (DFinsupp.single (β := A) i x : Π₀ (i : ι), A i)),
  f ∘ₗ DFinsupp.coprodMap (M := A) g = LinearMap.id
Tactic: classical
      choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
      replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ DFunLike.congr_fun (hg i)
      refine ⟨DFinsupp.coprodMap g, ?_⟩
      ext i x j
      simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]
-- 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
ι : 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
choose₁ :
  ∀ (g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R)
    (hg :
      ∀ (i : ι) (x : A i),
        Eq (α := Π₀ (i : ι), A i)
          ((f : (a : (Π₀ (i : ι), A i) →₀ R) → Π₀ (i : ι), A i) ((g i : (a : A i) → (Π₀ (i : ι), A i) →₀ R) x) :
            Π₀ (i : ι), A i)
          (DFinsupp.single (β := A) i x : Π₀ (i : ι), A i)),
    ∃ (h : (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) →₀ R), f ∘ₗ h = LinearMap.id
choose₂ :
  ∀ (g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R)
    (hg :
      ∀ (i : ι) (x : A i),
        Eq (α := Π₀ (i : ι), A i)
          ((f : (a : (Π₀ (i : ι), A i) →₀ R) → Π₀ (i : ι), A i) ((g i : (a : A i) → (Π₀ (i : ι), A i) →₀ R) x) :
            Π₀ (i : ι), A i)
          (DFinsupp.single (β := A) i x : Π₀ (i : ι), A i)),
    f ∘ₗ DFinsupp.coprodMap (M := A) g = LinearMap.id
⊢ ∃ (h : (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) →₀ R), f ∘ₗ h = LinearMap.id
have h₁ : ∀ (g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R)
  (hg :
    ∀ (i : ι) (x : A i),
      Eq (α := Π₀ (i : ι), A i)
        ((f : (a : (Π₀ (i : ι), A i) →₀ R) → Π₀ (i : ι), A i) ((g i : (a : A i) → (Π₀ (i : ι), A i) →₀ R) x) :
          Π₀ (i : ι), A i)
        (DFinsupp.single (β := A) i x : Π₀ (i : ι), A i))
  (i : ι) (x : A i) (j : ι),
  ((((f ∘ₗ DFinsupp.coprodMap (M := A) g) ∘ₗ DFinsupp.lsingle (M := A) i : (a : A i) → Π₀ (i : ι), A i) x :
          Π₀ (i : ι), A i) :
        (a : ι) → A a)
      j =
    (((LinearMap.id ∘ₗ DFinsupp.lsingle (M := A) i : (a : A i) → Π₀ (i : ι), A i) x : Π₀ (i : ι), A i) : (a : ι) → A a)
      j
Tactic: classical
      choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
      replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ DFunLike.congr_fun (hg i)
      refine ⟨DFinsupp.coprodMap g, ?_⟩
      ext i x j
      simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]
-- 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
ι : Type u_8
b : Basis ι R P
⊢ Projective R P
have h : Function.LeftInverse (α := P) (β := P →₀ R) (⇑(linearCombination R id) : (a : P →₀ R) → P)
  (⇑((b.constr ℕ : (a : ι → P →₀ R) → P →ₗ[R] P →₀ R) fun (i : ι) ↦ Finsupp.single ((b : (a : ι) → P) i) 1) :
    (a : P) → P →₀ R)
Tactic: use b.constr ℕ fun i => Finsupp.single (b i) (1 : R)
-- 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
ι : Type u_8
b : Basis ι R P
m : P
⊢ (linearCombination R id : (a : P →₀ R) → P)
      (((b.constr ℕ : (a : ι → P →₀ R) → P →ₗ[R] P →₀ R) fun (i : ι) ↦ Finsupp.single ((b : (a : ι) → P) i) 1 :
            (a : P) → P →₀ R)
          m :
        P →₀ R) =
    m
have h : (sum ((b.repr : (a : P) → ι →₀ R) m) fun (a : ι) (b_1 : R) ↦ HSMul.hSMul (β := P) b_1 ((b : (a : ι) → P) a : P)) = m
Tactic: simp only [b.constr_apply, mul_one, id, Finsupp.smul_single', Finsupp.linearCombination_single,
    map_finsuppSum]
-- 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
⊢ Projective R P
have obtain : ∀ (g : M →ₗ[R] P →₀ R) (hg : linearCombination R id ∘ₗ g = s), Projective R P
Tactic: obtain ⟨g, hg⟩ := projective_lifting_property (Finsupp.linearCombination R id) s
    (fun x ↦ ⟨Finsupp.single x 1, by simp⟩)
-- 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
⊢ Projective R P
have refine : ∀ (x : P), (linearCombination R id : (a : P →₀ R) → P) ((g ∘ₗ i : (a : P) → P →₀ R) x : P →₀ R) = x
Tactic: refine ⟨g.comp i, fun x ↦ ?_⟩
-- 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
⊢ (linearCombination R id : (a : P →₀ R) → P) ((g ∘ₗ i : (a : P) → P →₀ R) x : P →₀ R) = x
have rw : (linearCombination R id : (a : P →₀ R) → P) ((g : (a : M) → P →₀ R) ((i : (a : P) → M) x) : P →₀ R) = 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
⊢ (linearCombination R id : (a : P →₀ R) → P) ((g ∘ₗ i : (a : P) → P →₀ R) x : P →₀ R) = x
have rw₁ : (linearCombination R id ∘ₗ g : (a : M) → P) ((i : (a : P) → M) x : M) = 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
⊢ (linearCombination R id : (a : P →₀ R) → P) ((g ∘ₗ i : (a : P) → P →₀ R) x : P →₀ R) = x
have rw₂ : (s : (a : M) → P) ((i : (a : P) → M) x : M) = 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
⊢ (linearCombination R id : (a : P →₀ R) → P) ((g ∘ₗ i : (a : P) → P →₀ R) x : P →₀ R) = x
have rw₃ : (s ∘ₗ i : (a : P) → P) x = x
Tactic: rw [LinearMap.comp_apply, ← LinearMap.comp_apply, hg,
    ← LinearMap.comp_apply, H, LinearMap.id_apply]