-- Mathlib/LinearAlgebra/FreeModule/Basic.lean
lemma of_ringEquiv {R R' M M'} [Semiring R] [AddCommMonoid M] [Module R M]
    [Semiring R'] [AddCommMonoid M'] [Module R' M']
    (e₁ : R ≃+* R') (e₂ : M ≃ₛₗ[RingHomClass.toRingHom e₁] M') [Module.Free R M] :
    Module.Free R' M'

Proof state:
case ofRepr
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R'
inst✝² : AddCommMonoid M'
inst✝¹ : Module R' M'
e₁ : R ≃+* R'
e₂ : M ≃ₛₗ[↑e₁] M'
inst✝ : Free R M
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
he : ∀ (x : M'), e x = (Finsupp.mapRange.addEquiv e₁.toAddEquiv) (e₃ (e₂.symm x))
⊢ Free R' M'

Tactic:
let e' : M' ≃ₗ[R'] (I →₀ R') :=
  { __ := e, map_smul' := fun m x ↦ Finsupp.ext fun i ↦ by simp [he, map_smulₛₗ] }

Result:
case ofRepr
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R'
inst✝² : AddCommMonoid M'
inst✝¹ : Module R' M'
e₁ : R ≃+* R'
e₂ : M ≃ₛₗ[↑e₁] M'
inst✝ : Free R M
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
he : ∀ (x : M'), e x = (Finsupp.mapRange.addEquiv e₁.toAddEquiv) (e₃ (e₂.symm x))
e' : M' ≃ₗ[R'] I →₀ R' :=
  let __spread.0 := e;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Free R' M'

Proof state:
case ofRepr
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R'
inst✝² : AddCommMonoid M'
inst✝¹ : Module R' M'
e₁ : R ≃+* R'
e₂ : M ≃ₛₗ[↑e₁] M'
inst✝ : Free R M
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
⊢ Free R' M'

Tactic:
let e : M' ≃+ (I →₀ R') :=
  (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv (α := I) e₁.toAddEquiv)

Result:
case ofRepr
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R'
inst✝² : AddCommMonoid M'
inst✝¹ : Module R' M'
e₁ : R ≃+* R'
e₂ : M ≃ₛₗ[↑e₁] M'
inst✝ : Free R M
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
⊢ Free R' M'

Proof state:
case ofRepr
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R'
inst✝² : AddCommMonoid M'
inst✝¹ : Module R' M'
e₁ : R ≃+* R'
e₂ : M ≃ₛₗ[↑e₁] M'
inst✝ : Free R M
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
he : ∀ (x : M'), e x = (Finsupp.mapRange.addEquiv e₁.toAddEquiv) (e₃ (e₂.symm x))
e' : M' ≃ₗ[R'] I →₀ R' :=
  let __spread.0 := e;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Free R' M'

Tactic:
exact of_basis (.ofRepr e')

Result:
no goals

Proof state:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R'
inst✝² : AddCommMonoid M'
inst✝¹ : Module R' M'
e₁ : R ≃+* R'
e₂ : M ≃ₛₗ[↑e₁] M'
inst✝ : Free R M
⊢ Free R' M'

Tactic:
let I := Module.Free.ChooseBasisIndex R M

Result:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R'
inst✝² : AddCommMonoid M'
inst✝¹ : Module R' M'
e₁ : R ≃+* R'
e₂ : M ≃ₛₗ[↑e₁] M'
inst✝ : Free R M
I : Type u_4 := ChooseBasisIndex R M
⊢ Free R' M'

Proof state:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R'
inst✝² : AddCommMonoid M'
inst✝¹ : Module R' M'
e₁ : R ≃+* R'
e₂ : M ≃ₛₗ[↑e₁] M'
inst✝ : Free R M
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
he : ∀ (x : M'), e x = (Finsupp.mapRange.addEquiv e₁.toAddEquiv) (e₃ (e₂.symm x))
m : R'
x : M'
i : I
⊢ ({ toFun := __spread✝⁻⁰.toFun, map_add' := ⋯ }.toFun (m • x)) i =
    ((RingHom.id R') m • { toFun := __spread✝⁻⁰.toFun, map_add' := ⋯ }.toFun x) i

Tactic:
simp [he, map_smulₛₗ]

Result:
no goals

Proof state:
case ofRepr
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R'
inst✝² : AddCommMonoid M'
inst✝¹ : Module R' M'
e₁ : R ≃+* R'
e₂ : M ≃ₛₗ[↑e₁] M'
inst✝ : Free R M
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
⊢ Free R' M'

Tactic:
have he (x) : e x = Finsupp.mapRange.addEquiv (α := I) e₁.toAddEquiv (e₃ (e₂.symm x)) := rfl

Result:
case ofRepr
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R'
inst✝² : AddCommMonoid M'
inst✝¹ : Module R' M'
e₁ : R ≃+* R'
e₂ : M ≃ₛₗ[↑e₁] M'
inst✝ : Free R M
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
he : ∀ (x : M'), e x = (Finsupp.mapRange.addEquiv e₁.toAddEquiv) (e₃ (e₂.symm x))
⊢ Free R' M'

Proof state:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R'
inst✝² : AddCommMonoid M'
inst✝¹ : Module R' M'
e₁ : R ≃+* R'
e₂ : M ≃ₛₗ[↑e₁] M'
inst✝ : Free R M
I : Type u_4 := ChooseBasisIndex R M
⊢ Free R' M'

Tactic:
obtain ⟨e₃ : M ≃ₗ[R] I →₀ R⟩ := Module.Free.chooseBasis R M

Result:
case ofRepr
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R'
inst✝² : AddCommMonoid M'
inst✝¹ : Module R' M'
e₁ : R ≃+* R'
e₂ : M ≃ₛₗ[↑e₁] M'
inst✝ : Free R M
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
⊢ Free R' M'