awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst : AddMonoid ιA
inst_1 : AddAction ιA ιM
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝓐 : ιA → σ'
inst_5 : SetLike σ' A
𝓜 : ιM → σ
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : SetLike σ M
inst_9 : AddSubmonoidClass σ' A
inst_10 : AddSubmonoidClass σ M
inst_11 : SetLike.GradedMonoid 𝓐
inst_12 : SetLike.GradedSMul 𝓐 𝓜
inst_13 : DecidableEq ιA
inst_14 : DecidableEq ιM
inst_15 : GradedRing 𝓐
inst_16 : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
j : ιM
_hj :
  Membership.mem (γ := Finset ιM)
    (DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y)) j
⊢ (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
      (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M) =
    (↑(@GradedMonoid.GSMul.smul _ _ (fun (i : ιA) ↦ ↥(𝓐 i)) (fun (i : ιM) ↦ ↥(𝓜 i))
            (@AddSemigroupAction.toVAdd _ _ AddMonoid.toAddSemigroup _) _ _ _
            ((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i)
            ((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) :
          ↥(𝓜 (i +ᵥ j))) :
      M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Hom
Goal:
R : Type u_1
S_1 : Type u_2
M_1 : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst : Semiring S
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
simp_rw :
  Eq.{u_8 + 1} (α := M₂)
    ((f : (a : M) → M₂) (HSMul.hSMul (α := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) (s + s') : S) m) : M₂)
    ((f : (a : M) → M₂)
        (HAdd.hAdd (α := S) (β := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) s : S)
            ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) s' : S) •
          m) :
      M₂)
⊢ Eq.{u_8 + 1} (α := M₂) (((s + s') • f : (a : M) → M₂) m : M₂) ((s • f + s' • f : (a : M) → M₂) m : M₂)

Tactic:
simp_rw [AddMonoidHom.add_apply, DomMulAct.smul_addMonoidHom_apply, ← map_add, ← add_smul]

Premises used: DomMulAct.smul_addMonoidHom_apply, map_add, add_smul, AddMonoidHom.add_apply
-- Module: Mathlib.Algebra.Module.Hom
Goal:
R : Type u_1
S_1 : Type u_2
M_1 : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst : Semiring S
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
⊢ Eq.{u_8 + 1} (α := M₂)
    ((f : (a : M) → M₂) (HSMul.hSMul (α := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) (s + s') : S) m) : M₂)
    ((f : (a : M) → M₂)
        (HAdd.hAdd (α := S) (β := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) s : S)
            ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) s' : S) •
          m) :
      M₂)

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Hom
Goal:
R : Type u_1
S_1 : Type u_2
M_1 : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst : Semiring S
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module S M
x : M →+ M₂
x_1 : M
rw :
  Eq.{u_8 + 1} (α := M₂)
    ((x : (a : M) → M₂) (HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) 0 : S) x_1) :
      M₂)
    ((0 : (a : M) → M₂) x_1 : M₂)
⊢ Eq.{u_8 + 1} (α := M₂) ((HSMul.hSMul (α := Sᵈᵐᵃ) 0 x : (a : M) → M₂) x_1 : M₂) ((0 : (a : M) → M₂) x_1 : M₂)

Tactic:
rw [DomMulAct.smul_addMonoidHom_apply]

Premises used: DomMulAct.smul_addMonoidHom_apply
-- Module: Mathlib.Algebra.Module.Hom
Goal:
R : Type u_1
S_1 : Type u_2
M_1 : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst : Semiring S
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module S M
x : M →+ M₂
x_1 : M
⊢ Eq.{u_8 + 1} (α := M₂)
    ((x : (a : M) → M₂) (HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) 0 : S) x_1) :
      M₂)
    ((0 : (a : M) → M₂) x_1 : M₂)

Tactic:
simp [DomMulAct.mk, MulOpposite.opEquiv]

Premises used: MulOpposite.opEquiv, DomMulAct.mk
-- Module: Mathlib.Algebra.Module.Hom
Goal:
R : Type u_1
A : Type u_4
inst : Monoid R
inst_1 : AddCommMonoid A
inst_2 : DistribMulAction R A
r : R
f : AddMonoid.End A
⊢ (⇑(r • f) : (a : A) → A) = HSMul.hSMul (β := (a : A) → A) r (⇑f : (a : A) → A)

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, rfl
-- Module: Mathlib.Algebra.Module.Hom
Goal:
R : Type u_1
A : Type u_4
inst : Monoid R
inst_1 : AddCommMonoid A
inst_2 : DistribMulAction R A
r : R
f : AddMonoid.End A
x : A
⊢ (r • f : (a : A) → A) x = HSMul.hSMul (β := A) r ((f : (a : A) → A) x : A)

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, rfl
-- Module: Mathlib.Algebra.Module.Hom
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
A : Type u_4
B : Type u_5
inst : Monoid R
inst_1 : Monoid S
inst_2 : AddCommMonoid A
inst_3 : DistribMulAction R A
inst_4 : DistribMulAction S A
inst_5 : SMulCommClass R S A
⊢ SMulCommClass.{u_1, u_2, u_4} R S (AddMonoid.End A)

Tactic:
AddMonoidHom.instSMulCommClass

Premises used: AddMonoidHom.instSMulCommClass, AddMonoid.End
-- Module: Mathlib.Algebra.Module.Hom
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
A : Type u_4
B : Type u_5
inst : Monoid R
inst_1 : Monoid S
inst_2 : AddCommMonoid A
inst_3 : DistribMulAction R A
inst_4 : DistribMulAction S A
inst_5 : SMul R S
inst_6 : IsScalarTower R S A
⊢ IsScalarTower.{u_1, u_2, u_4} R S (AddMonoid.End A)

Tactic:
AddMonoidHom.instIsScalarTower

Premises used: AddMonoid.End, AddMonoidHom.instIsScalarTower
-- Module: Mathlib.Algebra.Module.Hom
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
A : Type u_4
B : Type u_5
inst : Monoid R
inst_1 : Monoid S
inst_2 : AddCommMonoid A
inst_3 : DistribMulAction R A
inst_4 : DistribMulAction S A
inst_5 : DistribMulAction.{u_1, u_4} Rᵐᵒᵖ A
inst_6 : IsCentralScalar R A
⊢ IsCentralScalar.{u_1, u_4} R (AddMonoid.End A)

Tactic:
AddMonoidHom.instIsCentralScalar

Premises used: AddMonoidHom.instIsCentralScalar, AddMonoid.End
-- Module: Mathlib.Algebra.Module.Hom
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := (a : R) → M →+ M) (⇑AddMonoidHom.smul : (a : R) → M →+ M) (DistribSMul.toAddMonoidHom M)

Tactic:
rfl

Premises used: DistribSMul.toAddMonoidHom, rfl
-- 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
inst_3 : AddCommGroup M
inst_4 : Module R M
e : Q ≃ₗ[R] M
h : Baer R Q
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] Q
h' :
  ∀ (x : R) (mem : x ∈ I),
    Eq.{v + 1} (α := Q) ((g' : (a : R) → Q) x : Q)
      (((↑e.symm : M →ₗ[R] Q) ∘ₗ g : (a : ↥I) → Q) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : Q)
⊢ ∀ (x : R) (mem : x ∈ I),
    Eq.{u_1 + 1} (α := M) (((↑e : Q →ₗ[R] M) ∘ₗ g' : (a : R) → M) x : M)
      ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)

Tactic:
simpa [LinearEquiv.eq_symm_apply] using h'

Premises used: LinearEquiv.eq_symm_apply
-- 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
inst_3 : AddCommGroup M
inst_4 : Module R M
e : Q ≃ₗ[R] M
⊢ Baer R Q ↔ Baer R M

Tactic:
⟨of_equiv e, of_equiv e.symm⟩

Premises used: LinearEquiv.symm, Module.Baer.of_equiv, Iff.intro
-- Module: Mathlib.Algebra.Module.Injective
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
⊢ Baer R M ↔
    ∀ (I : Ideal R),
      Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
        (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)

Tactic:
⟨fun h I g ↦ ?_, fun h I g ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Module.Injective
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
refine_1 :
  ∀ (h : Baer R M) (I : Ideal R) (g : ↥I →ₗ[R] M),
    ∃ (a : R →ₗ[R] M), (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) a = g
refine_2 :
  ∀
    (h :
      ∀ (I : Ideal R),
        Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
          (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M))
    (I : Ideal R) (g : ↥I →ₗ[R] M),
    ∃ (g' : R →ₗ[R] M),
      ∀ (x : R) (mem : x ∈ I),
        Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
          ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
⊢ Baer R M ↔
    ∀ (I : Ideal R),
      Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
        (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)

Tactic:
refine ⟨fun h I g ↦ ?_, fun h I g ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.Injective
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
h : Baer R M
I : Ideal R
g : ↥I →ₗ[R] M
refine_1 :
  ∀ (g' : R →ₗ[R] M)
    (hg' :
      ∀ (x : R) (mem : x ∈ I),
        Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
          ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)),
    ∃ (a : R →ₗ[R] M), (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) a = g
⊢ ∃ (a : R →ₗ[R] M), (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) a = g

Tactic:
rcases h I g with ⟨g', hg'⟩
-- Module: Mathlib.Algebra.Module.Injective
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
h : Baer R M
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' :
  ∀ (x : R) (mem : x ∈ I),
    Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
      ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
h₁ : (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g' = g
⊢ ∃ (a : R →ₗ[R] M), (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) a = g

Tactic:
use g'
-- Module: Mathlib.Algebra.Module.Injective
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
h : Baer R M
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' :
  ∀ (x : R) (mem : x ∈ I),
    Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
      ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
h₁ :
  ∀ (x : ↥I),
    Eq.{u_1 + 1} (α := M)
      ((((LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g' : ↥I →ₗ[R] M) : (a : ↥I) → M) x :
        M)
      ((g : (a : ↥I) → M) x : M)
⊢ (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g' = g

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Injective
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
h : Baer R M
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' :
  ∀ (x : R) (mem : x ∈ I),
    Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
      ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
x : ↥I
⊢ Eq.{u_1 + 1} (α := M)
    ((((LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g' : ↥I →ₗ[R] M) : (a : ↥I) → M) x :
      M)
    ((g : (a : ↥I) → M) x : M)

Tactic:
simp [hg']
-- Module: Mathlib.Algebra.Module.Injective
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
h :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
I : Ideal R
g : ↥I →ₗ[R] M
refine_2 :
  ∀ (g' : R →ₗ[R] M) (hg' : (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g' = g),
    ∃ (g' : R →ₗ[R] M),
      ∀ (x : R) (mem : x ∈ I),
        Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
          ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
⊢ ∃ (g' : R →ₗ[R] M),
    ∀ (x : R) (mem : x ∈ I),
      Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
        ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)

Tactic:
rcases h I g with ⟨g', hg'⟩
-- Module: Mathlib.Algebra.Module.Injective
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
h :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' : (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g' = g
h₁ :
  ∀ (x : R) (mem : x ∈ I),
    Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
      ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
⊢ ∃ (g' : R →ₗ[R] M),
    ∀ (x : R) (mem : x ∈ I),
      Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
        ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)

Tactic:
use g'
-- Module: Mathlib.Algebra.Module.Injective
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
h :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' : (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g' = g
x : R
hx : x ∈ I
⊢ Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M) ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x hx) : M)

Tactic:
simp [← hg']
-- 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
i : M →ₗ[R] N
f : M →ₗ[R] Q
a b : ExtensionOf i f
domain_eq : a.domain = b.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ a.domain⦄ ⦃hb : x ∈ b.domain⦄,
    (↑a.toLinearPMap : ↥a.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ a.domain) x ha) =
      (↑b.toLinearPMap : ↥b.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ b.domain) x hb)
rcases :
  ∀ (a : N →ₗ.[R] Q) (a_le : i.range ≤ a.domain)
    (e1 :
      ∀ (m : M),
        (f : (a : M) → Q) m =
          (↑a : ↥a.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ a.domain) ((i : (a : M) → N) m) ⋯))
    (domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain = b.domain)
    (to_fun_eq :
      ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain⦄
        ⦃hb : x ∈ b.domain⦄,
        (↑{ toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.toLinearPMap :
              ↥{ toLinearPMap := a, le := a_le, is_extension := e1 }.domain → Q)
            (Subtype.mk (p := fun (x : N) ↦
              x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain) x ha) =
          (↑b.toLinearPMap : ↥b.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ b.domain) x hb)),
    { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f } = b
⊢ a = b

Tactic:
rcases a with ⟨a, a_le, e1⟩
-- 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
i : M →ₗ[R] N
f : M →ₗ[R] Q
b : ExtensionOf i f
a : N →ₗ.[R] Q
a_le : i.range ≤ a.domain
e1 :
  ∀ (m : M),
    (f : (a : M) → Q) m = (↑a : ↥a.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ a.domain) ((i : (a : M) → N) m) ⋯)
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain = b.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain⦄
    ⦃hb : x ∈ b.domain⦄,
    (↑{ toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.toLinearPMap :
          ↥{ toLinearPMap := a, le := a_le, is_extension := e1 }.domain → Q)
        (Subtype.mk (p := fun (x : N) ↦
          x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain) x ha) =
      (↑b.toLinearPMap : ↥b.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ b.domain) x hb)
e_toLinearPMap : a = b.toLinearPMap
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f } = b

Tactic:
congr
-- 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
i : M →ₗ[R] N
f : M →ₗ[R] Q
b : ExtensionOf i f
a : N →ₗ.[R] Q
a_le : i.range ≤ a.domain
e1 :
  ∀ (m : M),
    (f : (a : M) → Q) m = (↑a : ↥a.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ a.domain) ((i : (a : M) → N) m) ⋯)
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain = b.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain⦄
    ⦃hb : x ∈ b.domain⦄,
    (↑{ toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.toLinearPMap :
          ↥{ toLinearPMap := a, le := a_le, is_extension := e1 }.domain → Q)
        (Subtype.mk (p := fun (x : N) ↦
          x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain) x ha) =
      (↑b.toLinearPMap : ↥b.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ b.domain) x hb)
⊢ a = b.toLinearPMap

Tactic:
LinearPMap.ext domain_eq to_fun_eq

Premises used: LinearPMap.ext
-- 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
i : M →ₗ[R] N
f : M →ₗ[R] Q
b : ExtensionOf i f
a : N →ₗ.[R] Q
a_le : i.range ≤ a.domain
e1 :
  ∀ (m : M),
    (f : (a : M) → Q) m = (↑a : ↥a.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ a.domain) ((i : (a : M) → N) m) ⋯)
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain = b.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain⦄
    ⦃hb : x ∈ b.domain⦄,
    (↑{ toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.toLinearPMap :
          ↥{ toLinearPMap := a, le := a_le, is_extension := e1 }.domain → Q)
        (Subtype.mk (p := fun (x : N) ↦
          x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain) x ha) =
      (↑b.toLinearPMap : ↥b.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ b.domain) x hb)
⊢ a = b.toLinearPMap

Tactic:
exact LinearPMap.ext domain_eq to_fun_eq

Premises used: LinearPMap.ext
-- 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
i : M →ₗ[R] N
f : M →ₗ[R] Q
a b : ExtensionOf i f
domain_eq : a.domain = b.domain
to_fun_eq :
  ∀ ⦃x : ↥a.domain⦄ ⦃y : ↥b.domain⦄,
    (↑x : N) = (↑y : N) → (↑a.toLinearPMap : ↥a.domain → Q) x = (↑b.toLinearPMap : ↥b.domain → Q) y
⊢ a = b

Tactic:
ext domain_eq fun _ _ _ ↦ to_fun_eq rfl

Premises used: Module.Baer.ExtensionOf.ext, rfl
-- 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
i : M →ₗ[R] N
f : M →ₗ[R] Q
a b : ExtensionOf i f
⊢ a = b ↔
    ∃ (_ : a.domain = b.domain),
      ∀ ⦃x : ↥a.domain⦄ ⦃y : ↥b.domain⦄,
        (↑x : N) = (↑y : N) → (↑a.toLinearPMap : ↥a.domain → Q) x = (↑b.toLinearPMap : ↥b.domain → Q) y

Tactic:
⟨fun r => r ▸ ⟨rfl, fun _ _ h => congr_arg a.toFun <| mod_cast h⟩, fun ⟨h1, h2⟩ =>
    ExtensionOf.dExt h1 h2⟩

Premises used: Module.Baer.ExtensionOf.dExt, cast, Eq.rec, _private.0.Module.Baer.ExtensionOf.dExt_iff.match_1, congr_arg, Module.Baer.ExtensionOf.toLinearPMap, LinearPMap.toFun, Iff.intro, Exists.intro, SetLike.coe_eq_coe._simp_1, Eq, DFunLike.coe, rfl
-- 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
i : M →ₗ[R] N
f : M →ₗ[R] Q
x x_1 : ExtensionOf i f
h : x.toLinearPMap = x_1.toLinearPMap
domain_eq : ∀ (x_2 : N), x_2 ∈ x.domain ↔ x_2 ∈ x_1.domain
to_fun_eq :
  ∀ ⦃x_2 : N⦄ ⦃ha : x_2 ∈ x.domain⦄ ⦃hb : x_2 ∈ x_1.domain⦄,
    (↑x.toLinearPMap : ↥x.domain → Q) (Subtype.mk (p := fun (x_3 : N) ↦ x_3 ∈ x.domain) x_2 ha) =
      (↑x_1.toLinearPMap : ↥x_1.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ x_1.domain) x_2 hb)
⊢ x = x_1

Tactic:
ext
-- 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
i : M →ₗ[R] N
f : M →ₗ[R] Q
x x_1 : ExtensionOf i f
h : x.toLinearPMap = x_1.toLinearPMap
x_2 : N
⊢ x_2 ∈ x.domain ↔ x_2 ∈ x_1.domain

Tactic:
congr!
-- 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
i : M →ₗ[R] N
f : M →ₗ[R] Q
x x_1 : ExtensionOf i f
h : x.toLinearPMap = x_1.toLinearPMap
x_2 : N
ha : x_2 ∈ x.domain
hb : x_2 ∈ x_1.domain
⊢ (↑x.toLinearPMap : ↥x.domain → Q) (Subtype.mk (p := fun (x_3 : N) ↦ x_3 ∈ x.domain) x_2 ha) =
    (↑x_1.toLinearPMap : ↥x_1.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ x_1.domain) x_2 hb)

Tactic:
congr!
-- 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
i : M →ₗ[R] N
f : M →ₗ[R] Q
X1 X2 : ExtensionOf i f
x : N
hx : x ∈ i.range
rcases : ∀ (x : M), Membership.mem (α := N) (X1.eqLocus X2.toLinearPMap) ((i : (a : M) → N) x : N)
⊢ x ∈ X1.eqLocus X2.toLinearPMap

Tactic:
rcases hx with ⟨x, rfl⟩

Premises used: rfl
-- 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
i : M →ₗ[R] N
f : M →ₗ[R] Q
X1 X2 : ExtensionOf i f
x : M
⊢ Membership.mem (α := N) (X1.eqLocus X2.toLinearPMap) ((i : (a : M) → N) x : N)

Tactic:
⟨X1.le (Set.mem_range_self _), X2.le (Set.mem_range_self _), ?_⟩

Premises used: Set.mem_range_self, Set.Mem, setOf, Exists.intro, Module.Baer.ExtensionOf.le
-- 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
i : M →ₗ[R] N
f : M →ₗ[R] Q
X1 X2 : ExtensionOf i f
x : M
refine :
  (↑X1.toLinearPMap : ↥X1.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ X1.domain) ((i : (a : M) → N) x) ⋯) =
    (↑X2.toLinearPMap : ↥X2.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ X2.domain) ((i : (a : M) → N) x) ⋯)
⊢ Membership.mem (α := N) (X1.eqLocus X2.toLinearPMap) ((i : (a : M) → N) x : N)

Tactic:
refine ⟨X1.le (Set.mem_range_self _), X2.le (Set.mem_range_self _), ?_⟩