-- Mathlib/Algebra/Module/Injective.lean
theorem of_injective [Small.{v} R] (inj : Module.Injective R Q) : Module.Baer R Q

Proof state:
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv (↥I) R
eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
obtain ⟨g', hg'⟩ := Module.Injective.out (eR.symm.toLinearMap ∘ₗ I.subtype ∘ₗ eI.toLinearMap)
  (eR.symm.injective.comp <| Subtype.val_injective.comp eI.injective) (g ∘ₗ eI.toLinearMap)

Result:
case intro
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv (↥I) R
eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R
g' : Shrink.{v, u} R →ₗ[R] Q
hg' : ∀ (x : Shrink.{v, u} ↥I), g' ((↑eR.symm ∘ₗ Submodule.subtype I ∘ₗ ↑eI) x) = (g ∘ₗ ↑eI) x
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Proof state:
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
⊢ Baer R Q

Tactic:
intro I g

Result:
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Proof state:
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv (↥I) R
eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R
g' : Shrink.{v, u} R →ₗ[R] Q
hg' : ∀ (x : Shrink.{v, u} ↥I), g' ((↑eR.symm ∘ₗ Submodule.subtype I ∘ₗ ↑eI) x) = (g ∘ₗ ↑eI) x
x : R
mx : x ∈ I
⊢ (g' ∘ₗ ↑eR.symm) x = g ⟨x, mx⟩

Tactic:
simpa [eI, eR] using hg' (equivShrink I ⟨x, mx⟩)

Result:
no goals

Proof state:
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
let eI := Shrink.linearEquiv I R

Result:
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv (↥I) R
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Proof state:
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv (↥I) R
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
let eR := Shrink.linearEquiv R R

Result:
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv (↥I) R
eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Proof state:
case intro
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv (↥I) R
eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R
g' : Shrink.{v, u} R →ₗ[R] Q
hg' : ∀ (x : Shrink.{v, u} ↥I), g' ((↑eR.symm ∘ₗ Submodule.subtype I ∘ₗ ↑eI) x) = (g ∘ₗ ↑eI) x
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
exact ⟨g' ∘ₗ eR.symm.toLinearMap, fun x mx ↦ by simpa [eI, eR] using hg' (equivShrink I ⟨x, mx⟩)⟩

Result:
no goals