-- Mathlib/Algebra/Module/Projective.lean
theorem Projective.of_ringEquiv {R S} [Semiring R] [Semiring S] {M N}
    [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N]
    (e₁ : R ≃+* S) (e₂ : M ≃ₛₗ[RingHomClass.toRingHom e₁] N)
    [Projective R M] : Projective S N

Proof state:
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
x y : N
⊢ (fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x)))) (x + y) =
    (fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x)))) x +
      (fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x)))) y

Tactic:
ext

Result:
case h
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
x y a✝ : N
⊢ ((fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x)))) (x + y)) a✝ =
    ((fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x)))) x +
        (fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x)))) y)
      a✝

Proof state:
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
⊢ Projective S N

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

Result:
case mk.intro
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
⊢ Projective S N

Proof state:
case h
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
r : S
v i : N
⊢ ({ toFun := fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯ }.toFun (r • v)) i =
    ((RingHom.id S) r •
        { toFun := fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯ }.toFun v)
      i

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

Result:
no goals

Proof state:
case mk.intro
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
g : N →ₗ[S] N →₀ S :=
  { toFun := fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯, map_smul' := ⋯ }
⊢ Projective S N

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

Result:
case mk.intro
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
g : N →ₗ[S] N →₀ S :=
  { toFun := fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯, map_smul' := ⋯ }
x : N
⊢ (linearCombination S id) (g x) = x

Proof state:
case mk.intro
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
⊢ Projective S N

Tactic:
let g : N →ₗ[S] N →₀ S :=
{ toFun := fun x ↦ (equivCongrLeft e₂ (f (e₂.symm x))).mapRange e₁ e₁.map_zero
  map_add' := fun x y ↦ by ext; simp
  map_smul' := fun r v ↦ by ext i; simp [e₂.symm.map_smulₛₗ] }

Result:
case mk.intro
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
g : N →ₗ[S] N →₀ S :=
  { toFun := fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯, map_smul' := ⋯ }
⊢ Projective S N

Proof state:
case mk.intro
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
g : N →ₗ[S] N →₀ S :=
  { toFun := fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯, map_smul' := ⋯ }
x : N
hf : e₂ ((linearCombination R id) (f (e₂.symm x))) = e₂ (e₂.symm x)
⊢ (linearCombination S id) (g x) = x

Tactic:
simpa [linearCombination_apply, sum_mapRange_index, g, map_finsupp_sum, e₂.map_smulₛₗ] using hf

Result:
no goals

Proof state:
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
r : S
v : N
⊢ { toFun := fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯ }.toFun (r • v) =
    (RingHom.id S) r •
      { toFun := fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯ }.toFun v

Tactic:
ext i

Result:
case h
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
r : S
v i : N
⊢ ({ toFun := fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯ }.toFun (r • v)) i =
    ((RingHom.id S) r •
        { toFun := fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯ }.toFun v)
      i

Proof state:
case mk.intro
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
g : N →ₗ[S] N →₀ S :=
  { toFun := fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯, map_smul' := ⋯ }
x : N
⊢ (linearCombination S id) (g x) = x

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

Result:
case mk.intro
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
g : N →ₗ[S] N →₀ S :=
  { toFun := fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯, map_smul' := ⋯ }
x : N
hf : e₂ ((linearCombination R id) (f (e₂.symm x))) = e₂ (e₂.symm x)
⊢ (linearCombination S id) (g x) = x