awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : M →ₗ[R] Q
this : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N))
r : R
x : N
⊢ (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) (r • x) ⋯) =
    (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
      (HSMul.hSMul (α := R) (β := ↥(extensionOfMax f g).domain) ((RingHom.id R : (a : R) → R) r : R)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) x ⋯))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Module.Injective
Goal:
Q : Type v
inst : AddCommGroup Q
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
h : Baer ℤ Q
f : M →+ N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : M →+ Q
⊢ ∃ (h : N →+ Q), h.comp f = g

Tactic:
have ⟨g', hg'⟩ := h.extension_property f.toIntLinearMap hf g.toIntLinearMap
  ⟨g', congr(LinearMap.toAddMonoidHom $hg')⟩

Premises used: LinearMap.toAddMonoidHom, AddMonoidHomClass.toAddMonoidHom, Module.Baer.extension_property, congrArg, _private.0.Module.Baer.extension_property_addMonoidHom.match_1, Exists, id, Exists.intro, AddMonoidHom.toIntLinearMap, Eq, AddMonoidHom.comp
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
h : Baer R Q
X Y : Type v
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective (α := X) (β := Y) (⇑i : (a : X) → Y)
f : X →ₗ[R] Q
obtain :
  ∀ (h : Y →ₗ[R] Q) (H : h ∘ₗ i = f),
    ∃ (h : Y →ₗ[R] Q),
      ∀ (x_4 : X), Eq (α := Q) ((h : (a : Y) → Q) ((i : (a : X) → Y) x_4 : Y) : Q) ((f : (a : X) → Q) x_4 : Q)
⊢ ∃ (h : Y →ₗ[R] Q),
    ∀ (x_4 : X), Eq (α := Q) ((h : (a : Y) → Q) ((i : (a : X) → Y) x_4 : Y) : Q) ((f : (a : X) → Q) x_4 : Q)

Tactic:
obtain ⟨h, H⟩ := Module.Baer.extension_property h i hi f

Premises used: Module.Baer.extension_property
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
h_1 : Baer R Q
X Y : Type v
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective (α := X) (β := Y) (⇑i : (a : X) → Y)
f : X →ₗ[R] Q
h : Y →ₗ[R] Q
H : h ∘ₗ i = f
⊢ ∃ (h : Y →ₗ[R] Q),
    ∀ (x_4 : X), Eq (α := Q) ((h : (a : Y) → Q) ((i : (a : X) → Y) x_4 : Y) : Q) ((f : (a : X) → Q) x_4 : Q)

Tactic:
⟨h, DFunLike.congr_fun H⟩

Premises used: DFunLike.congr_fun, Exists.intro
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
h_1 : Baer R Q
X Y : Type v
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective (α := X) (β := Y) (⇑i : (a : X) → Y)
f : X →ₗ[R] Q
h : Y →ₗ[R] Q
H : h ∘ₗ i = f
⊢ ∃ (h : Y →ₗ[R] Q),
    ∀ (x_4 : X), Eq (α := Q) ((h : (a : Y) → Q) ((i : (a : X) → Y) x_4 : Y) : Q) ((f : (a : X) → Q) x_4 : Q)

Tactic:
exact ⟨h, DFunLike.congr_fun H⟩
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
inst_3 : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : LinearEquiv.{u, u, v, u} (RingHom.id R) (Shrink.{v, u} ↥I) ↥I := Shrink.linearEquiv R ↥I
eR : LinearEquiv.{u, u, v, u} (RingHom.id R) (Shrink.{v, u} R) R := Shrink.linearEquiv R R
obtain :
  ∀ (g' : Shrink.{v, u} R →ₗ[R] Q)
    (hg' :
      ∀ (x : Shrink.{v, u} ↥I),
        Eq (α := Q)
          ((g' : (a : Shrink.{v, u} R) → Q)
              (((↑eR.symm : R →ₗ[R] Shrink.{v, u} R) ∘ₗ Submodule.subtype I ∘ₗ (↑eI : Shrink.{v, u} ↥I →ₗ[R] ↥I) :
                    (a : Shrink.{v, u} ↥I) → Shrink.{v, u} R)
                  x :
                Shrink.{v, u} R) :
            Q)
          ((g ∘ₗ (↑eI : Shrink.{v, u} ↥I →ₗ[R] ↥I) : (a : Shrink.{v, u} ↥I) → Q) x : Q)),
    ∃ (g' : R →ₗ[R] Q),
      ∀ (x : R) (mem : x ∈ I),
        Eq.{v + 1} (α := Q) ((g' : (a : R) → Q) x : Q)
          ((g : (a : ↥I) → Q) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : Q)
⊢ ∃ (g' : R →ₗ[R] Q),
    ∀ (x : R) (mem : x ∈ I),
      Eq.{v + 1} (α := Q) ((g' : (a : R) → Q) x : Q)
        ((g : (a : ↥I) → Q) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : Q)

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)

Premises used: LinearEquiv.symm, Subtype.val_injective, LinearMap.comp, LinearEquiv.toLinearMap, Function.Injective.comp, Module.Injective.out, Submodule.subtype, LinearEquiv.injective
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
inst_3 : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : LinearEquiv.{u, u, v, u} (RingHom.id R) (Shrink.{v, u} ↥I) ↥I := Shrink.linearEquiv R ↥I
eR : LinearEquiv.{u, u, v, u} (RingHom.id R) (Shrink.{v, u} R) R := Shrink.linearEquiv R R
g' : Shrink.{v, u} R →ₗ[R] Q
hg' :
  ∀ (x : Shrink.{v, u} ↥I),
    Eq (α := Q)
      ((g' : (a : Shrink.{v, u} R) → Q)
          (((↑eR.symm : R →ₗ[R] Shrink.{v, u} R) ∘ₗ Submodule.subtype I ∘ₗ (↑eI : Shrink.{v, u} ↥I →ₗ[R] ↥I) :
                (a : Shrink.{v, u} ↥I) → Shrink.{v, u} R)
              x :
            Shrink.{v, u} R) :
        Q)
      ((g ∘ₗ (↑eI : Shrink.{v, u} ↥I →ₗ[R] ↥I) : (a : Shrink.{v, u} ↥I) → Q) x : Q)
x : R
mx : x ∈ I
⊢ Eq.{v + 1} (α := Q) ((g' ∘ₗ (↑eR.symm : R →ₗ[R] Shrink.{v, u} R) : (a : R) → Q) x : Q)
    ((g : (a : ↥I) → Q) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mx) : Q)

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

Premises used: Membership.mem, Subtype, Subtype.mk, equivShrink, DFunLike.coe
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
inst_3 : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : LinearEquiv.{u, u, v, u} (RingHom.id R) (Shrink.{v, u} ↥I) ↥I := Shrink.linearEquiv R ↥I
eR : LinearEquiv.{u, u, v, u} (RingHom.id R) (Shrink.{v, u} R) R := Shrink.linearEquiv R R
g' : Shrink.{v, u} R →ₗ[R] Q
hg' :
  ∀ (x : Shrink.{v, u} ↥I),
    Eq (α := Q)
      ((g' : (a : Shrink.{v, u} R) → Q)
          (((↑eR.symm : R →ₗ[R] Shrink.{v, u} R) ∘ₗ Submodule.subtype I ∘ₗ (↑eI : Shrink.{v, u} ↥I →ₗ[R] ↥I) :
                (a : Shrink.{v, u} ↥I) → Shrink.{v, u} R)
              x :
            Shrink.{v, u} R) :
        Q)
      ((g ∘ₗ (↑eI : Shrink.{v, u} ↥I →ₗ[R] ↥I) : (a : Shrink.{v, u} ↥I) → Q) x : Q)
⊢ ∃ (g' : R →ₗ[R] Q),
    ∀ (x : R) (mem : x ∈ I),
      Eq.{v + 1} (α := Q) ((g' : (a : R) → Q) x : Q)
        ((g : (a : ↥I) → Q) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : Q)

Tactic:
exact ⟨g' ∘ₗ eR.symm.toLinearMap, fun x mx ↦ by simpa [eI, eR] using hg' (equivShrink I ⟨x, mx⟩)⟩
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
inst_3 : Small.{v, u} R
⊢ Baer R Q ↔ Injective R Q

Tactic:
⟨Module.Baer.injective, Module.Baer.of_injective⟩

Premises used: Module.Baer.injective, Module.Baer.of_injective, Iff.intro
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v, u} R
inj : Injective R M
⊢ Injective R (ULift.{v', v} M)

Tactic:
Module.Baer.injective fun I g ↦
  have ⟨g', hg'⟩ := Module.Baer.iff_injective.mpr inj I (ULift.moduleEquiv.toLinearMap ∘ₗ g)
  ⟨ULift.moduleEquiv.symm.toLinearMap ∘ₗ g', fun r hr ↦ ULift.ext _ _ <| hg' r hr⟩

Premises used: Iff.mpr, _private.0.Module.ulift_injective_of_injective.match_1, LinearEquiv.symm, ULift.ext, Exists, Module.Baer.injective, Module.Baer.iff_injective, Subtype.mk, LinearMap.comp, LinearEquiv.toLinearMap, ULift.moduleEquiv, Exists.intro, DFunLike.coe
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inj : Injective R (ULift.{v', v} M)
X Y : Type v
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] M
eX : ULift.{v', v} X ≃ₗ[R] X := ULift.moduleEquiv
⊢ Function.Injective (α := ULift.{v', v} X) (β := ULift.{v', v} Y)
    (⇑((↑(LinearEquiv.symm ULift.moduleEquiv) : Y →ₗ[R] ULift.{v', v} Y) ∘ₗ f ∘ₗ (↑eX : ULift.{v', v} X →ₗ[R] X)) :
      (a : ULift.{v', v} X) → ULift.{v', v} Y)

Tactic:
ULift.moduleEquiv.symm.injective.comp <| hf.comp eX.injective

Premises used: LinearEquiv.symm, Function.Injective.comp, ULift.moduleEquiv, LinearEquiv.injective
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inj : Injective R (ULift.{v', v} M)
X Y : Type v
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] M
eX : ULift.{v', v} X ≃ₗ[R] X := ULift.moduleEquiv
⊢ Function.Injective (α := ULift.{v', v} X) (β := ULift.{v', v} Y)
    (⇑((↑(LinearEquiv.symm ULift.moduleEquiv) : Y →ₗ[R] ULift.{v', v} Y) ∘ₗ f ∘ₗ (↑eX : ULift.{v', v} X →ₗ[R] X)) :
      (a : ULift.{v', v} X) → ULift.{v', v} Y)

Tactic:
exact ULift.moduleEquiv.symm.injective.comp <| hf.comp eX.injective

Premises used: LinearEquiv.symm, Function.Injective.comp, ULift.moduleEquiv, LinearEquiv.injective
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inj : Injective R (ULift.{v', v} M)
X Y : Type v
x_1 : AddCommGroup X
x_2 : AddCommGroup Y
x_3 : Module R X
x_4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] M
eX : ULift.{v', v} X ≃ₗ[R] X := ULift.moduleEquiv
g' : ULift.{v', v} Y →ₗ[R] ULift.{v', v} M
hg' :
  ∀ (x : ULift.{v', v} X),
    Eq (α := ULift.{v', v} M)
      ((g' : (a : ULift.{v', v} Y) → ULift.{v', v} M)
          (((↑(LinearEquiv.symm ULift.moduleEquiv) : Y →ₗ[R] ULift.{v', v} Y) ∘ₗ f ∘ₗ (↑eX : ULift.{v', v} X →ₗ[R] X) :
              (a : ULift.{v', v} X) → ULift.{v', v} Y)
            x) :
        ULift.{v', v} M)
      (((↑(LinearEquiv.symm ULift.moduleEquiv) : M →ₗ[R] ULift.{v', v} M) ∘ₗ g ∘ₗ (↑eX : ULift.{v', v} X →ₗ[R] X) :
            (a : ULift.{v', v} X) → ULift.{v', v} M)
          x :
        ULift.{v', v} M)
x : X
⊢ Eq (α := M)
    (((↑ULift.moduleEquiv : ULift.{v', v} M →ₗ[R] M) ∘ₗ
            g' ∘ₗ (↑(LinearEquiv.symm ULift.moduleEquiv) : Y →ₗ[R] ULift.{v', v} Y) :
          (a : Y) → M)
        ((f : (a : X) → Y) x : Y) :
      M)
    ((g : (a : X) → M) x : M)

Tactic:
congr(ULift.down $(hg' ⟨x⟩))

Premises used: congrArg, id, ULift.up, ULift.down
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inj : Injective R (ULift.{v', v} M)
X Y : Type v
x_1 : AddCommGroup X
x_2 : AddCommGroup Y
x_3 : Module R X
x_4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] M
eX : ULift.{v', v} X ≃ₗ[R] X := ULift.moduleEquiv
g' : ULift.{v', v} Y →ₗ[R] ULift.{v', v} M
hg' :
  ∀ (x : ULift.{v', v} X),
    Eq (α := ULift.{v', v} M)
      ((g' : (a : ULift.{v', v} Y) → ULift.{v', v} M)
          (((↑(LinearEquiv.symm ULift.moduleEquiv) : Y →ₗ[R] ULift.{v', v} Y) ∘ₗ f ∘ₗ (↑eX : ULift.{v', v} X →ₗ[R] X) :
              (a : ULift.{v', v} X) → ULift.{v', v} Y)
            x) :
        ULift.{v', v} M)
      (((↑(LinearEquiv.symm ULift.moduleEquiv) : M →ₗ[R] ULift.{v', v} M) ∘ₗ g ∘ₗ (↑eX : ULift.{v', v} X →ₗ[R] X) :
            (a : ULift.{v', v} X) → ULift.{v', v} M)
          x :
        ULift.{v', v} M)
x : X
⊢ Eq (α := M)
    (((↑ULift.moduleEquiv : ULift.{v', v} M →ₗ[R] M) ∘ₗ
            g' ∘ₗ (↑(LinearEquiv.symm ULift.moduleEquiv) : Y →ₗ[R] ULift.{v', v} Y) :
          (a : Y) → M)
        ((f : (a : X) → Y) x : Y) :
      M)
    ((g : (a : X) → M) x : M)

Tactic:
exact congr(ULift.down $(hg' ⟨x⟩))
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v, u} R
⊢ Injective R M ↔ Injective R (ULift.{v', v} M)

Tactic:
⟨Module.ulift_injective_of_injective R,
   Module.injective_of_ulift_injective R⟩

Premises used: Module.ulift_injective_of_injective, Module.injective_of_ulift_injective, Iff.intro
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type uR
inst : Ring R
inst_1 : Small.{uM, uR} R
M : Type uM
inst_2 : AddCommGroup M
inst_3 : Module R M
inj : Injective R M
P : Type uP
inst_4 : AddCommGroup P
inst_5 : Module R P
P' : Type uP'
inst_6 : AddCommGroup P'
inst_7 : Module R P'
f : P →ₗ[R] P'
hf : Function.Injective.{uP + 1, uP' + 1} (α := P) (β := P') (⇑f : (a : P) → P')
g : P →ₗ[R] M
⊢ ∃ (h : P' →ₗ[R] M), h ∘ₗ f = g

Tactic:
(Module.Baer.of_injective inj).extension_property f hf g

Premises used: Module.Baer.extension_property, Module.Baer.of_injective
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R_1 : Type u
inst : Ring R_1
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R_1 Q
R : Type u
inst_3 : Ring R
ι : Type w
M : ι → Type v
inst_4 : Small.{v, u} R
inst_5 : (i : ι) → AddCommGroup (M i)
inst_6 : (i : ι) → Module.{u, v} R (M i)
inst_7 : ∀ (i : ι), Injective.{u, v} R (M i)
X Y : Type (max v w)
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] (i : ι) → M i
choose :
  ∀ (l : (i : ι) → Y →ₗ[R] M i) (hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj (φ := M) i ∘ₗ g),
    ∃ (h : Y →ₗ[R] (i : ι) → M i),
      ∀ (x_4 : X),
        Eq (α := (i : ι) → M i) ((h : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x_4 : Y) : (i : ι) → M i)
          ((g : (a : X) → (i : ι) → M i) x_4 : (i : ι) → M i)
⊢ ∃ (h : Y →ₗ[R] (i : ι) → M i),
    ∀ (x_4 : X),
      Eq (α := (i : ι) → M i) ((h : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x_4 : Y) : (i : ι) → M i)
        ((g : (a : X) → (i : ι) → M i) x_4 : (i : ι) → M i)

Tactic:
choose l hl using fun i ↦ extension_property R _ _ _ f hf ((LinearMap.proj i).comp g)

Premises used: Module.Injective.extension_property, LinearMap.proj, LinearMap.comp
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R_1 : Type u
inst : Ring R_1
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R_1 Q
R : Type u
inst_3 : Ring R
ι : Type w
M : ι → Type v
inst_4 : Small.{v, u} R
inst_5 : (i : ι) → AddCommGroup (M i)
inst_6 : (i : ι) → Module.{u, v} R (M i)
inst_7 : ∀ (i : ι), Injective.{u, v} R (M i)
X Y : Type (max v w)
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj (φ := M) i ∘ₗ g
⊢ ∃ (h : Y →ₗ[R] (i : ι) → M i),
    ∀ (x_4 : X),
      Eq (α := (i : ι) → M i) ((h : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x_4 : Y) : (i : ι) → M i)
        ((g : (a : X) → (i : ι) → M i) x_4 : (i : ι) → M i)

Tactic:
⟨LinearMap.pi l, fun x ↦ ?_⟩

Premises used: LinearMap.pi, Exists.intro
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R_1 : Type u
inst : Ring R_1
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R_1 Q
R : Type u
inst_3 : Ring R
ι : Type w
M : ι → Type v
inst_4 : Small.{v, u} R
inst_5 : (i : ι) → AddCommGroup (M i)
inst_6 : (i : ι) → Module.{u, v} R (M i)
inst_7 : ∀ (i : ι), Injective.{u, v} R (M i)
X Y : Type (max v w)
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj (φ := M) i ∘ₗ g
refine :
  ∀ (x_4 : X),
    Eq (α := (i : ι) → M i)
      ((LinearMap.pi (φ := M) l : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x_4 : Y) : (i : ι) → M i)
      ((g : (a : X) → (i : ι) → M i) x_4 : (i : ι) → M i)
⊢ ∃ (h : Y →ₗ[R] (i : ι) → M i),
    ∀ (x_4 : X),
      Eq (α := (i : ι) → M i) ((h : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x_4 : Y) : (i : ι) → M i)
        ((g : (a : X) → (i : ι) → M i) x_4 : (i : ι) → M i)

Tactic:
refine ⟨LinearMap.pi l, fun x ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R_1 : Type u
inst : Ring R_1
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R_1 Q
R : Type u
inst_3 : Ring R
ι : Type w
M : ι → Type v
inst_4 : Small.{v, u} R
inst_5 : (i : ι) → AddCommGroup (M i)
inst_6 : (i : ι) → Module.{u, v} R (M i)
inst_7 : ∀ (i : ι), Injective.{u, v} R (M i)
X Y : Type (max v w)
x_1 : AddCommGroup X
x_2 : AddCommGroup Y
x_3 : Module R X
x_4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj (φ := M) i ∘ₗ g
x : X
h :
  ∀ (i : ι),
    Eq.{v + 1} (α := M i) ((LinearMap.pi (φ := M) l : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x : Y) i : M i)
      ((g : (a : X) → (i : ι) → M i) x i : M i)
⊢ Eq (α := (i : ι) → M i)
    ((LinearMap.pi (φ := M) l : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x : Y) : (i : ι) → M i)
    ((g : (a : X) → (i : ι) → M i) x : (i : ι) → M i)

Tactic:
ext i
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R_1 : Type u
inst : Ring R_1
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R_1 Q
R : Type u
inst_3 : Ring R
ι : Type w
M : ι → Type v
inst_4 : Small.{v, u} R
inst_5 : (i : ι) → AddCommGroup (M i)
inst_6 : (i : ι) → Module.{u, v} R (M i)
inst_7 : ∀ (i : ι), Injective.{u, v} R (M i)
X Y : Type (max v w)
x_1 : AddCommGroup X
x_2 : AddCommGroup Y
x_3 : Module R X
x_4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj (φ := M) i ∘ₗ g
x : X
i : ι
⊢ Eq.{v + 1} (α := M i) ((LinearMap.pi (φ := M) l : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x : Y) i : M i)
    ((g : (a : X) → (i : ι) → M i) x i : M i)

Tactic:
DFunLike.congr_fun (hl i) x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R_1 : Type u
inst : Ring R_1
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R_1 Q
R : Type u
inst_3 : Ring R
ι : Type w
M : ι → Type v
inst_4 : Small.{v, u} R
inst_5 : (i : ι) → AddCommGroup (M i)
inst_6 : (i : ι) → Module.{u, v} R (M i)
inst_7 : ∀ (i : ι), Injective.{u, v} R (M i)
X Y : Type (max v w)
x_1 : AddCommGroup X
x_2 : AddCommGroup Y
x_3 : Module R X
x_4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj (φ := M) i ∘ₗ g
x : X
i : ι
⊢ Eq.{v + 1} (α := M i) ((LinearMap.pi (φ := M) l : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x : Y) i : M i)
    ((g : (a : X) → (i : ι) → M i) x i : M i)

Tactic:
exact DFunLike.congr_fun (hl i) x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
S : Type u'
inst_2 : Ring S
M : Type v
N : Type v'
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[(↑e₁ : R →+* S)] N
inj : Injective R M
apply :
  ∀ (I : Ideal S) (g : ↥I →ₗ[S] N),
    ∃ (g' : S →ₗ[S] N),
      ∀ (x : S) (mem : x ∈ I),
        Eq.{v' + 1} (α := N) ((g' : (a : S) → N) x : N)
          ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) x mem) : N)
⊢ Injective S N

Tactic:
apply Module.Baer.injective (fun I g ↦ ?_)

Premises used: Module.Baer.injective
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
S : Type u'
inst_2 : Ring S
M : Type v
N : Type v'
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[(↑e₁ : R →+* S)] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv : S →ₛₗ[(↑e₁.symm : S →+* R)] R) I
e : ↥I' ≃ₛₗ[(↑e₁ : R →+* S)] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := (↑e₂.symm : N →ₛₗ[(↑e₁.symm : S →+* R)] M) ∘ₛₗ g ∘ₛₗ (↑e : ↥I' →ₛₗ[(↑e₁ : R →+* S)] ↥I)
x : R
hx : x ∈ I'
⊢ Membership.mem (α := S) I ((e₁ : (a : R) → S) x : S)

Tactic:
simp_all [I']
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
S : Type u'
inst_2 : Ring S
M : Type v
N : Type v'
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[(↑e₁ : R →+* S)] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv : S →ₛₗ[(↑e₁.symm : S →+* R)] R) I
e : ↥I' ≃ₛₗ[(↑e₁ : R →+* S)] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := (↑e₂.symm : N →ₛₗ[(↑e₁.symm : S →+* R)] M) ∘ₛₗ g ∘ₛₗ (↑e : ↥I' →ₛₗ[(↑e₁ : R →+* S)] ↥I)
⊢ ∀ (x : R) (hx : x ∈ I'),
    Eq.{v + 1} (α := M) ((f : (a : ↥I') → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I') x hx) : M)
      ((e₂.symm : (a : N) → M)
          ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) ((e₁ : (a : R) → S) x) ⋯ : ↥I) : N) :
        M)

Tactic:
have hf (x) (hx : x ∈ I') : f ⟨x, hx⟩ = e₂.symm (g ⟨e₁ x, by simp_all [I']⟩) := rfl
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
S : Type u'
inst_2 : Ring S
M : Type v
N : Type v'
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[(↑e₁ : R →+* S)] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv : S →ₛₗ[(↑e₁.symm : S →+* R)] R) I
e : ↥I' ≃ₛₗ[(↑e₁ : R →+* S)] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := (↑e₂.symm : N →ₛₗ[(↑e₁.symm : S →+* R)] M) ∘ₛₗ g ∘ₛₗ (↑e : ↥I' →ₛₗ[(↑e₁ : R →+* S)] ↥I)
hf :
  ∀ (x : R) (hx : x ∈ I'),
    Eq.{v + 1} (α := M) ((f : (a : ↥I') → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I') x hx) : M)
      ((e₂.symm : (a : N) → M)
          ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) ((e₁ : (a : R) → S) x) ⋯ : ↥I) : N) :
        M)
obtain :
  ∀ (f' : R →ₗ[R] M)
    (hf' :
      ∀ (x : R) (mem : x ∈ I'),
        Eq.{v + 1} (α := M) ((f' : (a : R) → M) x : M)
          ((f : (a : ↥I') → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I') x mem) : M)),
    ∃ (g' : S →ₗ[S] N),
      ∀ (x : S) (mem : x ∈ I),
        Eq.{v' + 1} (α := N) ((g' : (a : S) → N) x : N)
          ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) x mem) : N)
⊢ ∃ (g' : S →ₗ[S] N),
    ∀ (x : S) (mem : x ∈ I),
      Eq.{v' + 1} (α := N) ((g' : (a : S) → N) x : N)
        ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) x mem) : N)

Tactic:
obtain ⟨f', hf'⟩ := Module.Baer.of_injective ‹_› I' f

Premises used: Module.Baer.of_injective