awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg : ∀ (i : ι), f ∘ₗ g i = DFinsupp.lsingle (M := A) i
⊢ ∀ (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)
-- 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)
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:
⟨DFinsupp.coprodMap g, ?_⟩

Premises used: DFinsupp.coprodMap, 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
ι : 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)
refine : f ∘ₗ DFinsupp.coprodMap (M := A) g = LinearMap.id
⊢ ∃ (h : (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) →₀ R), f ∘ₗ h = LinearMap.id

Tactic:
refine ⟨DFinsupp.coprodMap 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
ι : 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 : ι) (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
⊢ f ∘ₗ DFinsupp.coprodMap (M := A) g = LinearMap.id

Tactic:
ext i x j
-- 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)
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:
simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]

Premises used: DFinsupp.lsingle_apply, LinearMap.id_apply, LinearMap.comp_apply, DFinsupp.coprodMap_apply_single
-- 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
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₁ :
  ∀ (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
⊢ ∃ (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]

Premises used: DFinsupp.lsingle_apply, LinearMap.id_apply, LinearMap.comp_apply, DFinsupp.coprodMap_apply_single
-- 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
ι : Type u_8
b : Basis ι R P
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)
⊢ Projective R P

Tactic:
use b.constr ℕ fun i => Finsupp.single (b i) (1 : R)

Premises used: Nat, OfNat.ofNat, DFunLike.coe, Finsupp.single, Module.Basis.constr
-- 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
ι : Type u_8
b : Basis ι R P
m : P
h : (sum ((b.repr : (a : P) → ι →₀ R) m) fun (a : ι) (b_1 : R) ↦ HSMul.hSMul (β := P) b_1 ((b : (a : ι) → P) a : P)) = m
⊢ (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

Tactic:
simp only [b.constr_apply, mul_one, id, Finsupp.smul_single', Finsupp.linearCombination_single,
    map_finsuppSum]

Premises used: id, Finsupp.smul_single', Finsupp.linearCombination_single, map_finsuppSum, mul_one, Module.Basis.constr_apply
-- 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
ι : Type u_8
b : Basis ι R P
m : P
⊢ (sum ((b.repr : (a : P) → ι →₀ R) m) fun (a : ι) (b_1 : R) ↦ HSMul.hSMul (β := P) b_1 ((b : (a : ι) → P) a : P)) = m

Tactic:
b.linearCombination_repr m

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Module.Basis.linearCombination_repr, Finset.sum
-- 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
ι : Type u_8
b : Basis ι R P
m : P
⊢ (sum ((b.repr : (a : P) → ι →₀ R) m) fun (a : ι) (b_1 : R) ↦ HSMul.hSMul (β := P) b_1 ((b : (a : ι) → P) a : P)) = m

Tactic:
exact b.linearCombination_repr m

Premises used: Module.Basis.linearCombination_repr
-- 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)
inst_11 : Free R P
⊢ Projective R P

Tactic:
.of_basis <| Module.Free.chooseBasis R P

Premises used: Module.Projective.of_basis, Module.Free.chooseBasis
-- 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 M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
x : P
⊢ (linearCombination R id : (a : P →₀ R) → P) (Finsupp.single x 1) = x

Tactic:
simp
-- 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 M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
obtain : ∀ (g : M →ₗ[R] P →₀ R) (hg : linearCombination R id ∘ₗ g = s), Projective R P
⊢ Projective R P

Tactic:
obtain ⟨g, hg⟩ := projective_lifting_property (Finsupp.linearCombination R id) s
    (fun x ↦ ⟨Finsupp.single x 1, by simp⟩)

Premises used: id, Exists.intro, Module.projective_lifting_property, OfNat.ofNat, Finsupp.linearCombination, Finsupp.single
-- 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 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

Tactic:
⟨g.comp i, fun x ↦ ?_⟩

Premises used: Module.Projective.mk, LinearMap.comp, 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
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
refine : ∀ (x : P), (linearCombination R id : (a : P →₀ R) → P) ((g ∘ₗ i : (a : P) → P →₀ R) x : P →₀ R) = x
⊢ Projective R P

Tactic:
refine ⟨g.comp i, fun x ↦ ?_⟩
-- 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 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
rw₃ : (s ∘ₗ i : (a : P) → P) x = x
rw₄ : (LinearMap.id : (a : P) → P) x = x
rw₅ rw₆ : x = x
⊢ (linearCombination R id : (a : P →₀ R) → P) ((g ∘ₗ i : (a : P) → P →₀ R) x : P →₀ R) = x

Tactic:
rw [LinearMap.comp_apply, ← LinearMap.comp_apply, hg,
    ← LinearMap.comp_apply, H, LinearMap.id_apply]

Premises used: LinearMap.id_apply, LinearMap.comp_apply
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_8
S : Type u_9
inst : Semiring R
inst_1 : Semiring S
M : Type u_10
N : Type u_11
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module S N
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst_8 : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
obtain :
  ∀ (f : M →ₗ[R] M →₀ R)
    (hf :
      Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M)
        (⇑f : (a : M) → M →₀ R)),
    Projective S N
⊢ Projective S N

Tactic:
obtain ⟨f, hf⟩ := ‹Projective R M›

Premises used: Module.Projective
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_8
S : Type u_9
inst : Semiring R
inst_1 : Semiring S
M : Type u_10
N : Type u_11
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module S N
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst_8 : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑f : (a : M) → M →₀ R)
x y : N
h :
  ∀ (a : N),
    Eq.{u_9 + 1} (α := S)
      ((mapRange (⇑e₁ : (a : R) → S) ⋯
              ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
                ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) (x + y)))) :
            (a : N) → S)
          a :
        S)
      ((HAdd.hAdd (α := N →₀ S)
              (mapRange (⇑e₁ : (a : R) → S) ⋯
                ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
                  ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) x))))
              (mapRange (⇑e₁ : (a : R) → S) ⋯
                ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
                  ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) y)))) :
            (a : N) → S)
          a :
        S)
⊢ mapRange (⇑e₁ : (a : R) → S) ⋯
      ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
        ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) (x + y)))) =
    HAdd.hAdd (α := N →₀ S)
      (mapRange (⇑e₁ : (a : R) → S) ⋯
        ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
          ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) x))))
      (mapRange (⇑e₁ : (a : R) → S) ⋯
        ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
          ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) y))))

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_8
S : Type u_9
inst : Semiring R
inst_1 : Semiring S
M : Type u_10
N : Type u_11
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module S N
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst_8 : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑f : (a : M) → M →₀ R)
x y a : N
⊢ Eq.{u_9 + 1} (α := S)
    ((mapRange (⇑e₁ : (a : R) → S) ⋯
            ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
              ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) (x + y)))) :
          (a : N) → S)
        a :
      S)
    ((HAdd.hAdd (α := N →₀ S)
            (mapRange (⇑e₁ : (a : R) → S) ⋯
              ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
                ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) x))))
            (mapRange (⇑e₁ : (a : R) → S) ⋯
              ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
                ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) y)))) :
          (a : N) → S)
        a :
      S)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_8
S : Type u_9
inst : Semiring R
inst_1 : Semiring S
M : Type u_10
N : Type u_11
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module S N
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst_8 : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑f : (a : M) → M →₀ R)
r : S
v : N
h :
  ∀ (i : N),
    Eq.{u_9 + 1} (α := S)
      ((mapRange (⇑e₁ : (a : R) → S) ⋯
              ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
                ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) (r • v)))) :
            (a : N) → S)
          i :
        S)
      ((HSMul.hSMul (α := S) (β := N →₀ S) ((RingHom.id S : (a : S) → S) r : S)
              (mapRange (⇑e₁ : (a : R) → S) ⋯
                ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
                  ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) v)))) :
            (a : N) → S)
          i :
        S)
⊢ mapRange (⇑e₁ : (a : R) → S) ⋯
      ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
        ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) (r • v)))) =
    HSMul.hSMul (α := S) (β := N →₀ S) ((RingHom.id S : (a : S) → S) r : S)
      (mapRange (⇑e₁ : (a : R) → S) ⋯
        ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
          ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) v))))

Tactic:
ext i
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_8
S : Type u_9
inst : Semiring R
inst_1 : Semiring S
M : Type u_10
N : Type u_11
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module S N
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst_8 : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑f : (a : M) → M →₀ R)
r : S
v i : N
⊢ Eq.{u_9 + 1} (α := S)
    ((mapRange (⇑e₁ : (a : R) → S) ⋯
            ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
              ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) (r • v)))) :
          (a : N) → S)
        i :
      S)
    ((HSMul.hSMul (α := S) (β := N →₀ S) ((RingHom.id S : (a : S) → S) r : S)
            (mapRange (⇑e₁ : (a : R) → S) ⋯
              ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
                ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) v)))) :
          (a : N) → S)
        i :
      S)

Tactic:
simp [e₁, e₂.symm.map_smulₛₗ]

Premises used: LinearEquiv.symm, LinearEquiv.map_smulₛₗ
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_8
S : Type u_9
inst : Semiring R
inst_1 : Semiring S
M : Type u_10
N : Type u_11
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module S N
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst_8 : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑f : (a : M) → M →₀ R)
g : N →ₗ[S] N →₀ S :=
  {
    toFun := fun (x : N) ↦
      mapRange (⇑e₁ : (a : R) → S) ⋯
        ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
          ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) x))),
    map_add' := ⋯, map_smul' := ⋯ }
⊢ Projective S N

Tactic:
⟨⟨g, fun x ↦ ?_⟩⟩

Premises used: Module.Projective.mk, Exists.intro
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_8
S : Type u_9
inst : Semiring R
inst_1 : Semiring S
M : Type u_10
N : Type u_11
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module S N
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst_8 : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑f : (a : M) → M →₀ R)
g : N →ₗ[S] N →₀ S :=
  {
    toFun := fun (x : N) ↦
      mapRange (⇑e₁ : (a : R) → S) ⋯
        ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
          ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) x))),
    map_add' := ⋯, map_smul' := ⋯ }
refine : ∀ (x : N), (linearCombination S id : (a : N →₀ S) → N) ((g : (a : N) → N →₀ S) x : N →₀ S) = x
⊢ Projective S N

Tactic:
refine ⟨⟨g, fun x ↦ ?_⟩⟩
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u_8
S : Type u_9
inst : Semiring R
inst_1 : Semiring S
M : Type u_10
N : Type u_11
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module S N
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst_8 : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑f : (a : M) → M →₀ R)
g : N →ₗ[S] N →₀ S :=
  {
    toFun := fun (x : N) ↦
      mapRange (⇑e₁ : (a : R) → S) ⋯
        ((Finsupp.equivCongrLeft (↑e₂ : M ≃ N) : (a : M →₀ R) → N →₀ R)
          ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) x))),
    map_add' := ⋯, map_smul' := ⋯ }
x : N
⊢ Eq.{u_11 + 1} (α := N)
    ((e₂ : (a : M) → N)
        ((linearCombination R id : (a : M →₀ R) → M) ((f : (a : M) → M →₀ R) ((e₂.symm : (a : N) → M) x) : M →₀ R) :
          M) :
      N)
    ((e₂ : (a : M) → N) ((e₂.symm : (a : N) → M) x : M) : N)

Tactic:
replace hf := congr(e₂ $(hf (e₂.symm x)))