-- Mathlib/RingTheory/OrzechProperty.lean
theorem injective_of_surjective_of_injective
    {N : Type w} [AddCommMonoid N] [Module R N]
    (i f : N →ₗ[R] M) (hi : Injective i) (hf : Surjective f) : Injective f

Proof state:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
⊢ Injective ⇑i'

Tactic:
simpa [i'] using hi

Result:
no goals

Proof state:
case intro.intro
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this : Small.{max u ?u.2014, v} M
⊢ Injective ⇑f

Tactic:
letI := Equiv.addCommMonoid (equivShrink M).symm

Result:
case intro.intro
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝ : Small.{max u ?u.2014, v} M
this : AddCommMonoid (Shrink.{max u ?u.2014, v} M) := (equivShrink M).symm.addCommMonoid
⊢ Injective ⇑f

Proof state:
case intro.intro
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
hi : Injective ⇑i'
⊢ Injective ⇑f

Tactic:
let f' := j.symm.toLinearMap ∘ₗ f ∘ₗ (LinearEquiv.ofInjective i' hi).symm.toLinearMap

Result:
case intro.intro
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
hi : Injective ⇑i'
f' : ↥(LinearMap.range i') →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ f ∘ₗ ↑(LinearEquiv.ofInjective i' hi).symm
⊢ Injective ⇑f

Proof state:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
⊢ Injective ⇑f

Tactic:
obtain ⟨n, g, hg⟩ := Module.Finite.exists_fin' R M

Result:
case intro.intro
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
⊢ Injective ⇑f

Proof state:
case intro.intro
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
hi : Injective ⇑i'
f' : ↥(LinearMap.range i') →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ f ∘ₗ ↑(LinearEquiv.ofInjective i' hi).symm
⊢ Injective ⇑f

Tactic:
replace hf : Surjective f' := by simpa [f'] using hf

Result:
case intro.intro
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
hi : Injective ⇑i'
f' : ↥(LinearMap.range i') →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ f ∘ₗ ↑(LinearEquiv.ofInjective i' hi).symm
hf : Surjective ⇑f'
⊢ Injective ⇑f

Proof state:
case intro.intro
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝¹ : Small.{u, v} M
this✝ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
⊢ Injective ⇑f

Tactic:
haveI := Module.Finite.equiv j.symm

Result:
case intro.intro
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
⊢ Injective ⇑f