awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
M : Type u_3
inst : AddCommMonoid M
⊢ Eq.{u_3 + 1} (α := (a : Submodule ℕ M) → AddSubmonoid M)
    (⇑(OrderIso.symm toNatSubmodule) : (a : Submodule ℕ M) → AddSubmonoid M) Submodule.toAddSubmonoid

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
M : Type u_3
inst : AddCommMonoid M
S : AddSubmonoid M
⊢ (↑((toNatSubmodule : (a : AddSubmonoid M) → Submodule ℕ M) S : Submodule ℕ M) : Set M) = (↑S : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
M : Type u_3
inst : AddCommMonoid M
S : AddSubmonoid M
⊢ Submodule.toAddSubmonoid (R := ℕ) ((toNatSubmodule : (a : AddSubmonoid M) → Submodule ℕ M) S) = S

Tactic:
AddSubmonoid.toNatSubmodule.symm_apply_apply S

Premises used: AddSubmonoid.toNatSubmodule, OrderIso.symm_apply_apply
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
M : Type u_3
inst : AddCommMonoid M
S : Submodule ℕ M
⊢ (AddSubmonoid.toNatSubmodule : (a : AddSubmonoid M) → Submodule ℕ M) S.toAddSubmonoid = S

Tactic:
AddSubmonoid.toNatSubmodule.apply_symm_apply S

Premises used: OrderIso.apply_symm_apply, AddSubmonoid.toNatSubmodule
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
M : Type u_3
inst : AddCommGroup M
⊢ Eq.{u_3 + 1} (α := (a : Submodule ℤ M) → AddSubgroup M)
    (⇑(OrderIso.symm toIntSubmodule) : (a : Submodule ℤ M) → AddSubgroup M) Submodule.toAddSubgroup

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
M : Type u_3
inst : AddCommGroup M
S : AddSubgroup M
⊢ (↑((toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) S : Submodule ℤ M) : Set M) = (↑S : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
M : Type u_3
inst : AddCommGroup M
S : AddSubgroup M
⊢ Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule M)
      ((toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) S) =
    S

Tactic:
AddSubgroup.toIntSubmodule.symm_apply_apply S

Premises used: OrderIso.symm_apply_apply, AddSubgroup.toIntSubmodule
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
M : Type u_3
inst : AddCommGroup M
S : Submodule ℤ M
⊢ (AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) S.toAddSubgroup = S

Tactic:
AddSubgroup.toIntSubmodule.apply_symm_apply S

Premises used: OrderIso.apply_symm_apply, AddSubgroup.toIntSubmodule
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_1
inst_3 : SetLike A M
inst_4 : AddSubmonoidClass A M
inst_5 : SMulMemClass A R M
S' : A
x : ↥S'
⊢ (SMulMemClass.subtype S' : (a : ↥S') → M) x = (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_1
inst_3 : SetLike A M
inst_4 : AddSubmonoidClass A M
inst_5 : SMulMemClass A R M
S' : A
⊢ Injective (α := ↥S') (β := M) (⇑(SMulMemClass.subtype S') : (a : ↥S') → M)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_1
inst_3 : SetLike A M
inst_4 : AddSubmonoidClass A M
inst_5 : SMulMemClass A R M
S' : A
⊢ Eq (α := (a : ↥S') → M) (⇑(SMulMemClass.subtype S') : (a : ↥S') → M) (Subtype.val (p := fun (x : M) ↦ x ∈ S'))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
⊢ ∀ (x y : ↥p), (↑(x + y) : M) = (↑x : M) + (↑y : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
⊢ ∀ (m : R) (x : ↥p), (↑(m • x) : M) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) (↑x : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x : ↥p
⊢ (p.subtype : (a : ↥p) → M) x = (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
⊢ Injective (α := ↥p) (β := M) (⇑p.subtype : (a : ↥p) → M)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
⊢ Eq (α := (a : ↥p) → M) (⇑p.subtype : (a : ↥p) → M) (Subtype.val (p := fun (x : M) ↦ x ∈ p))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x : ι → ↥p
s : Finset ι
⊢ Eq.{v + 1} (α := M) (↑(∑ i ∈ s, x i) : M) (∑ i ∈ s, (↑(x i) : M))

Tactic:
map_sum p.subtype _ _

Premises used: map_sum, Submodule.subtype
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
x : ↥p
⊢ Eq.{u_7 + 1} (α := M₂) ((f.domRestrict p : (a : ↥p) → M₂) x : M₂) ((f : (a : M) → M₂) (↑x : M) : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
⊢ Eq (α := (a : ↥p) → M₂) ((⇑(f.domRestrict p) : (a : ↥p) → M₂) : (a : ↥p) → M₂)
    ((↑p : Set M).restrict (π := fun (a : M) ↦ M₂) (⇑f : (a : M) → M₂) : (a : (↑(↑p : Set M) : Type u_5)) → M₂)

Tactic:
rfl

Premises used: Set.restrict, rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f_1 : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
p : Submodule R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
h : ∀ (c : M), Membership.mem (α := M₂) p ((f : (a : M) → M₂) c : M₂)
x x_1 : M
⊢ Subtype.mk (p := fun (x : M₂) ↦ x ∈ p) ((f : (a : M) → M₂) (x + x_1)) ⋯ =
    HAdd.hAdd (α := ↥p) (β := ↥p) (Subtype.mk (p := fun (x : M₂) ↦ x ∈ p) ((f : (a : M) → M₂) x) ⋯ : ↥p)
      (Subtype.mk (p := fun (x : M₂) ↦ x ∈ p) ((f : (a : M) → M₂) x_1) ⋯ : ↥p)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f_1 : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
p : Submodule R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
h : ∀ (c : M), Membership.mem (α := M₂) p ((f : (a : M) → M₂) c : M₂)
x : R
x_1 : M
⊢ Subtype.mk (p := fun (x : M₂) ↦ x ∈ p) ((f : (a : M) → M₂) (x • x_1)) ⋯ =
    HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := ↥p) ((σ₁₂ : (a : R) → R₂) x : R₂)
      (Subtype.mk (p := fun (x : M₂) ↦ x ∈ p) ((f : (a : M) → M₂) x_1) ⋯ : ↥p)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
h : ∀ (c : M), Membership.mem (α := M₂) p ((f : (a : M) → M₂) c : M₂)
x : M
⊢ Eq.{u_7 + 1} (α := M₂) ((↑((codRestrict p f h : (a : M) → ↥p) x) : M₂) : M₂) ((f : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
p : Submodule R₃ M₃
h : ∀ (b : M₂), Membership.mem (α := M₃) p ((g : (a : M₂) → M₃) b : M₃)
⊢ codRestrict p g h ∘ₛₗ f = codRestrict p (g ∘ₛₗ f) ⋯

Tactic:
ext fun _ => rfl

Premises used: LinearMap.ext, rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R₂ M₂
h : ∀ (b : M), Membership.mem (α := M₂) p ((f : (a : M) → M₂) b : M₂)
⊢ p.subtype ∘ₛₗ codRestrict p f h = f

Tactic:
ext fun _ => rfl

Premises used: LinearMap.ext, rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R₂ M₂
h : ∀ (c : M), Membership.mem (α := M₂) p ((f : (a : M) → M₂) c : M₂)
⊢ g.domRestrict p ∘ₛₗ codRestrict p f h = g ∘ₛₗ f

Tactic:
rfl

Premises used: LinearMap.domRestrict, rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst_12 : AddCommMonoid M₂'
inst_13 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
b c : M
a :
  Eq.{u_7 + 1} (α := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (b + c) : M₂)) ⋯) :
      M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) b : M₂)) ⋯ +
          Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯) :
      M₂)
⊢ Exists.choose (p := fun (y : M₂') ↦
      Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (b + c) : M₂)) ⋯ =
    Exists.choose (p := fun (y : M₂') ↦
        Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) b : M₂)) ⋯ +
      Exists.choose (p := fun (y : M₂') ↦
        Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯

Tactic:
apply hp
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst_12 : AddCommMonoid M₂'
inst_13 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
b c : M
a :
  (p : (a : M₂') → M₂)
      (Exists.choose (p := fun (y : M₂') ↦
        (p : (a : M₂') → M₂) y = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) b : M₂) ((f : (a : M) → M₂) c : M₂))
        ⋯) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((p : (a : M₂') → M₂)
          (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) b : M₂)) ⋯) :
        M₂)
      ((p : (a : M₂') → M₂)
          (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯) :
        M₂)
a₁ :
  (p : (a : M₂') → M₂)
      (Exists.choose (p := fun (y : M₂') ↦
        (p : (a : M₂') → M₂) y = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) b : M₂) ((f : (a : M) → M₂) c : M₂))
        ⋯) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) b : M₂) ((f : (a : M) → M₂) c : M₂)
a₂ :
  Eq.{u_7 + 1} (α := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (b + c) : M₂)) ⋯) :
      M₂)
    ((f : (a : M) → M₂) (b + c) : M₂)
⊢ Eq.{u_7 + 1} (α := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (b + c) : M₂)) ⋯) :
      M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) b : M₂)) ⋯ +
          Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯) :
      M₂)

Tactic:
simp_rw [map_add, (h _).choose_spec, ← map_add, (h _).choose_spec]

Premises used: Exists.choose_spec, map_add
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst_12 : AddCommMonoid M₂'
inst_13 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
r : R
c : M
a :
  Eq.{u_7 + 1} (α := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (r • c) : M₂)) ⋯) :
      M₂)
    ((p : (a : M₂') → M₂)
        (HSMul.hSMul.{u_3, u_10, u_10} (α := R₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
          (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯)) :
      M₂)
⊢ Exists.choose (p := fun (y : M₂') ↦
      Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (r • c) : M₂)) ⋯ =
    HSMul.hSMul.{u_3, u_10, u_10} (α := R₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      (Exists.choose (p := fun (y : M₂') ↦
        Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯)

Tactic:
apply hp
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst_12 : AddCommMonoid M₂'
inst_13 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
r : R
c : M
a :
  (p : (a : M₂') → M₂)
      (Exists.choose (p := fun (y : M₂') ↦
        Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (r • c) : M₂)) ⋯) =
    HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := M₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      ((p : (a : M₂') → M₂)
          (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯) :
        M₂)
a₁ :
  (f : (a : M) → M₂) (r • c) =
    HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := M₂) ((σ₁₂ : (a : R) → R₂) r : R₂) ((f : (a : M) → M₂) c : M₂)
⊢ Eq.{u_7 + 1} (α := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (r • c) : M₂)) ⋯) :
      M₂)
    ((p : (a : M₂') → M₂)
        (HSMul.hSMul.{u_3, u_10, u_10} (α := R₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
          (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯)) :
      M₂)

Tactic:
simp_rw [map_smul, (h _).choose_spec, map_smulₛₗ]

Premises used: Exists.choose_spec, MulActionSemiHomClass.map_smulₛₗ, map_smul
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
x : M
⊢ (f.codLift p hp h : (a : M) → M₂') x =
    Exists.choose (p := fun (y : M₂') ↦
      Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)) ⋯

Tactic:
rfl

Premises used: Classical.choose, rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
h₁ : ∀ (x : M), Eq.{u_7 + 1} (α := M₂) ((p ∘ₛₗ f.codLift p hp h : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)
⊢ p ∘ₛₗ f.codLift p hp h = f

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
x : M
h₁ :
  Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) ((f.codLift p hp h : (a : M) → M₂') x : M₂') : M₂)
    ((f : (a : M) → M₂) x : M₂)
h₂ :
  Eq.{u_7 + 1} (α := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)) ⋯) :
      M₂)
    ((f : (a : M) → M₂) x : M₂)
h₃ h₄ : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)
⊢ Eq.{u_7 + 1} (α := M₂) ((p ∘ₛₗ f.codLift p hp h : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)

Tactic:
rw [comp_apply, codLift_apply, (h x).choose_spec]

Premises used: Exists.choose_spec, LinearMap.comp_apply, LinearMap.codLift_apply
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
hf : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂)
x : ↥p
⊢ Eq.{u_7 + 1} (α := M₂) ((↑((f.restrict hf : (a : ↥p) → ↥q) x) : M₂) : M₂) ((f : (a : M) → M₂) (↑x : M) : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
hf : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂)
x : ↥p
⊢ Eq.{u_7 + 1} (α := ↥q) ((f.restrict hf : (a : ↥p) → ↥q) x : ↥q)
    (Subtype.mk (p := fun (x : M₂) ↦ x ∈ q) ((f : (a : M) → M₂) (↑x : M)) ⋯ : ↥q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst : Ring R
inst_1 : Ring R₂
σ₁₂ : R →+* R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
p : Submodule R M
q : Submodule R₂ M₂
f g : M →ₛₗ[σ₁₂] M₂
hf : MapsTo (⇑f : (a : M) → M₂) (↑p : Set M) (↑q : Set M₂)
hg : MapsTo (⇑g : (a : M) → M₂) (↑p : Set M) (↑q : Set M₂)
hfg : MapsTo (⇑(f - g) : (a : M) → M₂) (↑p : Set M) (↑q : Set M₂)
h :
  ∀ (x : ↥p),
    Eq.{u_13 + 1} (α := M₂) (↑((f.restrict hf - g.restrict hg : (a : ↥p) → ↥q) x) : M₂)
      (↑(((f - g).restrict hfg : (a : ↥p) → ↥q) x) : M₂)
⊢ f.restrict hf - g.restrict hg = (f - g).restrict hfg

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst : Ring R
inst_1 : Ring R₂
σ₁₂ : R →+* R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
p : Submodule R M
q : Submodule R₂ M₂
f g : M →ₛₗ[σ₁₂] M₂
hf : MapsTo (⇑f : (a : M) → M₂) (↑p : Set M) (↑q : Set M₂)
hg : MapsTo (⇑g : (a : M) → M₂) (↑p : Set M) (↑q : Set M₂)
hfg : MapsTo (⇑(f - g) : (a : M) → M₂) (↑p : Set M) (↑q : Set M₂)
x : ↥p
⊢ Eq.{u_13 + 1} (α := M₂) (↑((f.restrict hf - g.restrict hg : (a : ↥p) → ↥q) x) : M₂)
    (↑(((f - g).restrict hfg : (a : ↥p) → ↥q) x) : M₂)

Tactic:
simp