awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
M : Type u_7
inst_6 : Monoid M
inst_7 : DistribMulAction M F
inst_8 : SMulCommClass S M F
a : M
f : E →ₛₗ.[σ] F
⊢ (↑(a • f) : ↥(a • f).domain → F) = a • (↑f : ↥f.domain → F)

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
M : Type u_7
N : Type u_8
inst_9 : Monoid M
inst_10 : DistribMulAction M F
inst_11 : SMulCommClass S M F
inst_12 : Monoid N
inst_13 : DistribMulAction N F
inst_14 : SMulCommClass S N F
inst_15 : SMulCommClass M N F
⊢ SMulCommClass M N (E →ₛₗ.[σ] F)

Tactic:
⟨fun a b f => ext' <| smul_comm a b f.toFun⟩

Premises used: LinearPMap.ext', LinearPMap.toFun, SMulCommClass.smul_comm, SMulCommClass.mk
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
M : Type u_7
N : Type u_8
inst_9 : Monoid M
inst_10 : DistribMulAction M F
inst_11 : SMulCommClass S M F
inst_12 : Monoid N
inst_13 : DistribMulAction N F
inst_14 : SMulCommClass S N F
inst_15 : SMul M N
inst_16 : IsScalarTower M N F
⊢ IsScalarTower M N (E →ₛₗ.[σ] F)

Tactic:
⟨fun a b f => ext' <| smul_assoc a b f.toFun⟩

Premises used: smul_assoc, LinearPMap.ext', LinearPMap.toFun, IsScalarTower.mk
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f : E →ₛₗ.[σ] F
⊢ (-f).domain = f.domain

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f : E →ₛₗ.[σ] F
x : ↥(-f).domain
⊢ (↑(-f) : ↥(-f).domain → F) x = -(↑f : ↥f.domain → F) x

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
h : ∀ (x : E), x ∈ (- -f).domain ↔ x ∈ f.domain
h' :
  ∀ ⦃x : E⦄ ⦃y : x ∈ (- -f).domain⦄ ⦃hxy : x ∈ f.domain⦄,
    (↑(- -f) : ↥(- -f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (- -f).domain) x y) =
      (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hxy)
⊢ - -f = f

Tactic:
ext x y hxy
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
x : E
⊢ x ∈ (- -f).domain ↔ x ∈ f.domain

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
x : E
y : x ∈ (- -f).domain
hxy : x ∈ f.domain
⊢ (↑(- -f) : ↥(- -f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (- -f).domain) x y) =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hxy)

Tactic:
simp only [neg_apply, neg_neg]

Premises used: LinearPMap.neg_apply, neg_neg
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f g : E →ₛₗ.[σ] F
⊢ (f + g).domain = f.domain ⊓ g.domain

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f g : E →ₛₗ.[σ] F
x : ↥(f.domain ⊓ g.domain)
⊢ (↑(f + g) : ↥(f + g).domain → F) x =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (↑x : E) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (↑x : E) ⋯)

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g h : E →ₛₗ.[σ] F
h₁ : ∀ (x : E), x ∈ (f + g + h).domain ↔ x ∈ (f + (g + h)).domain
h' :
  ∀ ⦃x : E⦄ ⦃y : x ∈ (f + g + h).domain⦄ ⦃hxy : x ∈ (f + (g + h)).domain⦄,
    (↑(f + g + h) : ↥(f + g + h).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g + h).domain) x y) =
      (↑(f + (g + h)) : ↥(f + (g + h)).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + (g + h)).domain) x hxy)
⊢ f + g + h = f + (g + h)

Tactic:
ext x y hxy
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g h : E →ₛₗ.[σ] F
x : E
⊢ x ∈ (f + g + h).domain ↔ x ∈ (f + (g + h)).domain

Tactic:
simp only [add_domain, inf_assoc]

Premises used: inf_assoc, LinearPMap.add_domain
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g h : E →ₛₗ.[σ] F
x : E
y : x ∈ (f + g + h).domain
hxy : x ∈ (f + (g + h)).domain
⊢ (↑(f + g + h) : ↥(f + g + h).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g + h).domain) x y) =
    (↑(f + (g + h)) : ↥(f + (g + h)).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + (g + h)).domain) x hxy)

Tactic:
simp only [add_apply, add_assoc]

Premises used: add_assoc, LinearPMap.add_apply
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
h : ∀ (x : E), x ∈ (0 + f).domain ↔ x ∈ f.domain
h' :
  ∀ ⦃x : E⦄ ⦃y : x ∈ (0 + f).domain⦄ ⦃hxy : x ∈ f.domain⦄,
    (↑(0 + f) : ↥(0 + f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (0 + f).domain) x y) =
      (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hxy)
⊢ 0 + f = f

Tactic:
ext x y hxy
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
x : E
⊢ x ∈ (0 + f).domain ↔ x ∈ f.domain

Tactic:
simp [add_domain]

Premises used: LinearPMap.add_domain
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
x : E
y : x ∈ (0 + f).domain
hxy : x ∈ f.domain
⊢ (↑(0 + f) : ↥(0 + f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (0 + f).domain) x y) =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hxy)

Tactic:
simp [add_apply]

Premises used: LinearPMap.add_apply
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
h : ∀ (x : E), x ∈ (f + 0).domain ↔ x ∈ f.domain
h' :
  ∀ ⦃x : E⦄ ⦃y : x ∈ (f + 0).domain⦄ ⦃hxy : x ∈ f.domain⦄,
    (↑(f + 0) : ↥(f + 0).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + 0).domain) x y) =
      (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hxy)
⊢ f + 0 = f

Tactic:
ext x y hxy
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
x : E
⊢ x ∈ (f + 0).domain ↔ x ∈ f.domain

Tactic:
simp [add_domain]

Premises used: LinearPMap.add_domain
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
x : E
y : x ∈ (f + 0).domain
hxy : x ∈ f.domain
⊢ (↑(f + 0) : ↥(f + 0).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + 0).domain) x y) =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hxy)

Tactic:
simp [add_apply]

Premises used: LinearPMap.add_apply
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
⊢ 0 + f = f

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
⊢ ∀ (a : E →ₛₗ.[σ] F), a + 0 = a

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
h : ∀ (x : E), x ∈ (f + g).domain ↔ x ∈ (g + f).domain
h' :
  ∀ ⦃x : E⦄ ⦃y : x ∈ (f + g).domain⦄ ⦃hxy : x ∈ (g + f).domain⦄,
    (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x y) =
      (↑(g + f) : ↥(g + f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (g + f).domain) x hxy)
⊢ f + g = g + f

Tactic:
ext x y hxy
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
x : E
⊢ x ∈ (f + g).domain ↔ x ∈ (g + f).domain

Tactic:
simp only [add_domain, inf_comm]

Premises used: inf_comm, LinearPMap.add_domain
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
x : E
y : x ∈ (f + g).domain
hxy : x ∈ (g + f).domain
⊢ (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x y) =
    (↑(g + f) : ↥(g + f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (g + f).domain) x hxy)

Tactic:
simp only [add_apply, add_comm]

Premises used: add_comm, LinearPMap.add_apply
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f : E →ₛₗ[σ] F
g : E →ₛₗ.[σ] F
⊢ (f +ᵥ g).domain = g.domain

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f : E →ₛₗ[σ] F
g : E →ₛₗ.[σ] F
x : ↥(f +ᵥ g).domain
⊢ (↑(f +ᵥ g) : ↥(f +ᵥ g).domain → F) x = HAdd.hAdd (α := F) ((f : (a : E) → F) (↑x : E) : F) ((↑g : ↥g.domain → F) x)

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f : E →ₛₗ[σ] F
g : E →ₛₗ.[σ] F
⊢ (↑(f +ᵥ g) : ↥(f +ᵥ g).domain → F) = (⇑(f ∘ₛₗ g.domain.subtype) : (a : ↥g.domain) → F) + (↑g : ↥g.domain → F)

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f g : E →ₛₗ.[σ] F
⊢ (f - g).domain = f.domain ⊓ g.domain

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f g : E →ₛₗ.[σ] F
x : ↥(f.domain ⊓ g.domain)
⊢ (↑(f - g) : ↥(f - g).domain → F) x =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (↑x : E) ⋯) -
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (↑x : E) ⋯)

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
h : ∀ (x : E), x ∈ (f - g).domain ↔ x ∈ (f + -g).domain
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ (f - g).domain⦄ ⦃h : x ∈ (f + -g).domain⦄,
    (↑(f - g) : ↥(f - g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f - g).domain) x hf) =
      (↑(f + -g) : ↥(f + -g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + -g).domain) x h)
⊢ f - g = f + -g

Tactic:
ext x _ h
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
x : E
⊢ x ∈ (f - g).domain ↔ x ∈ (f + -g).domain

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
x : E
hf : x ∈ (f - g).domain
h : x ∈ (f + -g).domain
⊢ (↑(f - g) : ↥(f - g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f - g).domain) x hf) =
    (↑(f + -g) : ↥(f + -g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + -g).domain) x h)

Tactic:
simp [sub_apply, add_apply, neg_apply, ← sub_eq_add_neg]

Premises used: LinearPMap.neg_apply, sub_eq_add_neg, LinearPMap.sub_apply, LinearPMap.add_apply
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
h : ∀ (x : E), x ∈ (-(f + g)).domain ↔ x ∈ (-g + -f).domain
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ (-(f + g)).domain⦄ ⦃h : x ∈ (-g + -f).domain⦄,
    (↑(-(f + g)) : ↥(-(f + g)).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (-(f + g)).domain) x hf) =
      (↑(-g + -f) : ↥(-g + -f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (-g + -f).domain) x h)
⊢ -(f + g) = -g + -f

Tactic:
ext x _ h
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
x : E
⊢ x ∈ (-(f + g)).domain ↔ x ∈ (-g + -f).domain

Tactic:
simp [add_domain, neg_domain, And.comm]

Premises used: And.comm, LinearPMap.neg_domain, LinearPMap.add_domain
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
x : E
hf : x ∈ (-(f + g)).domain
h : x ∈ (-g + -f).domain
⊢ (↑(-(f + g)) : ↥(-(f + g)).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (-(f + g)).domain) x hf) =
    (↑(-g + -f) : ↥(-g + -f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (-g + -f).domain) x h)

Tactic:
simp [add_apply, neg_apply, ← sub_eq_add_neg]

Premises used: LinearPMap.neg_apply, sub_eq_add_neg, LinearPMap.add_apply
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
h' : f + g = 0
h : ∀ (x : E), x ∈ (-f).domain ↔ x ∈ g.domain
h'₁ :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ (-f).domain⦄ ⦃hg : x ∈ g.domain⦄,
    (↑(-f) : ↥(-f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (-f).domain) x hf) =
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)
⊢ -f = g

Tactic:
ext x hf hg
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
h' : f + g = 0
x : E
⊢ Eq.{u_4 + 1} (α := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) ⊤

Tactic:
have : (0 : E →ₛₗ.[σ] F).domain = ⊤ := zero_domain
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
h' : f + g = 0
x : E
this : Eq.{u_4 + 1} (α := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) ⊤
⊢ f.domain = ⊤ ∧ g.domain = ⊤

Tactic:
simp only [← h', add_domain, inf_eq_top_iff] at this

Premises used: inf_eq_top_iff, LinearPMap.add_domain
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
h' : f + g = 0
x : E
this : f.domain = ⊤ ∧ g.domain = ⊤
h : x ∈ f.domain ↔ x ∈ g.domain
h₁ : Membership.mem (γ := Submodule R E) ⊤ x ↔ x ∈ g.domain
h₂ h₃ : Membership.mem (γ := Submodule R E) ⊤ x ↔ Membership.mem (γ := Submodule R E) ⊤ x
⊢ x ∈ (-f).domain ↔ x ∈ g.domain

Tactic:
rw [neg_domain, this.1, this.2]

Premises used: And.right, And.left, LinearPMap.neg_domain
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
h' : f + g = 0
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
h'₁ :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg) =
    0
⊢ (↑(-f) : ↥(-f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (-f).domain) x hf) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)

Tactic:
simp only [neg_domain, neg_apply, neg_eq_iff_add_eq_zero]

Premises used: LinearPMap.neg_apply, neg_eq_iff_add_eq_zero, LinearPMap.neg_domain
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
h' : f + g = 0
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
h'₁ :
  ∀
    (h' :
      (f + g).domain = domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0 ∧
        ∀ ⦃x : E⦄ ⦃hf : x ∈ (f + g).domain⦄
          ⦃hg : Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x⦄,
          (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x hf) =
            (↑0 : ↥(domain 0) → F)
              (Subtype.mk (p := fun (x : E) ↦
                Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x) x hg))
    ⦃x : E⦄ ⦃hf : x ∈ (-f).domain⦄ ⦃hg : x ∈ g.domain⦄,
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) +
        (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg) =
      0
⊢ (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg) =
    0

Tactic:
rw [ext_iff] at h'

Premises used: LinearPMap.ext_iff