awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
h₁ :
  ∃ (h_1 : x ∈ f.domain),
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) =
      (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x h)
⊢ ∃ (x_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) = x_1

Tactic:
use f ⟨x, h⟩

Premises used: Subtype.mk, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ (h_1 : x ∈ f.domain),
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) =
      (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x h)

Tactic:
simp only [h, exists_const]

Premises used: exists_const
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
h : ∀ (x : F), x ∈ Submodule.map (LinearMap.snd R E F) f.graph ↔ x ∈ f.toFun.range
⊢ Submodule.map (LinearMap.snd R E F) f.graph = f.toFun.range

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x : F
⊢ x ∈ Submodule.map (LinearMap.snd R E F) f.graph ↔ x ∈ f.toFun.range

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
h :
  ∀ (x_fst : E) (x_snd : F),
    (x_fst, x_snd) ∈ (z • f).graph ↔
      (x_fst, x_snd) ∈
        Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
⊢ (z • f).graph = Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph

Tactic:
ext ⟨x_fst, x_snd⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h :
  (x_fst, x_snd) ∈ (z • f).graph →
    (x_fst, x_snd) ∈
      Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
h₁ :
  (x_fst, x_snd) ∈
      Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph →
    (x_fst, x_snd) ∈ (z • f).graph
⊢ (x_fst, x_snd) ∈ (z • f).graph ↔
    (x_fst, x_snd) ∈
      Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ (z • f).graph
⊢ ∃ (y : ↥(z • f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2

Tactic:
rw [mem_graph_iff] at h

Premises used: LinearPMap.mem_graph_iff
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h : ∃ (y : ↥(z • f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2
h₁ :
  ∀ (y : ↥(z • f).domain) (hy : (↑y : E) = (x_fst, x_snd).1)
    (h : (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2),
    (x_fst, x_snd) ∈
      Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph

Tactic:
rcases h with ⟨y, hy, h⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2
⊢ z • (↑f : ↥f.domain → F) y = (x_fst, x_snd).2

Tactic:
rw [LinearPMap.smul_apply] at h

Premises used: LinearPMap.smul_apply
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : z • (↑f : ↥f.domain → F) y = (x_fst, x_snd).2
h₁ : ∃ (a : E) (a_1 : ↥f.domain), (↑a_1 : E) = a ∧ a = x_fst ∧ z • (↑f : ↥f.domain → F) a_1 = x_snd
⊢ ∃ y ∈ f.graph,
    (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id) : (a : E × F) → E × F) y =
      (x_fst, x_snd)

Tactic:
simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id,
      LinearMap.smul_apply, Prod.mk_inj, Prod.exists, exists_exists_and_eq_and]

Premises used: LinearMap.prodMap_apply, LinearMap.smul_apply, LinearMap.id_coe, Prod.mk_inj, id, LinearPMap.mem_graph_iff, exists_exists_and_eq_and, Prod.exists
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : z • (↑f : ↥f.domain → F) y = (x_fst, x_snd).2
w : E
w₁ : ↥f.domain
left : (↑y : E) = x_fst
right : x_fst = x_fst ∧ z • (↑f : ↥f.domain → F) y = x_snd
⊢ ∃ (a : E) (a_1 : ↥f.domain), (↑a_1 : E) = a ∧ a = x_fst ∧ z • (↑f : ↥f.domain → F) a_1 = x_snd

Tactic:
use x_fst, y, hy
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h :
  (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
⊢ ∃ y ∈ f.graph,
    (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id) : (a : E × F) → E × F) y =
      (x_fst, x_snd)

Tactic:
rw [Submodule.mem_map] at h

Premises used: Submodule.mem_map
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h :
  ∃ y ∈ f.graph,
    (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id) : (a : E × F) → E × F) y =
      (x_fst, x_snd)
h₁ :
  ∀ (x' : E × F) (hx' : x' ∈ f.graph)
    (h :
      (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id) : (a : E × F) → E × F) x' =
        (x_fst, x_snd)),
    (x_fst, x_snd) ∈ (z • f).graph
⊢ (x_fst, x_snd) ∈ (z • f).graph

Tactic:
rcases h with ⟨x', hx', h⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
x' : E × F
hx' : x' ∈ f.graph
h :
  (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id) : (a : E × F) → E × F) x' =
    (x_fst, x_snd)
h₁ :
  ∀ (fst : E) (snd : F) (hx' : (fst, snd) ∈ f.graph)
    (h :
      (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id) : (a : E × F) → E × F) (fst, snd) =
        (x_fst, x_snd)),
    (x_fst, x_snd) ∈ (z • f).graph
⊢ (x_fst, x_snd) ∈ (z • f).graph

Tactic:
cases x'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst : E
snd : F
hx' : (fst, snd) ∈ f.graph
h :
  (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id) : (a : E × F) → E × F) (fst, snd) =
    (x_fst, x_snd)
⊢ fst = x_fst ∧ z • snd = x_snd

Tactic:
simp only [LinearMap.prodMap_apply, LinearMap.id_coe, id, LinearMap.smul_apply,
    Prod.mk_inj] at h

Premises used: LinearMap.prodMap_apply, LinearMap.smul_apply, LinearMap.id_coe, Prod.mk_inj, id
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst : E
snd : F
hx' : (fst, snd) ∈ f.graph
h : fst = x_fst ∧ z • snd = x_snd
h₁ :
  ∀ (hx' : ∃ (y : ↥f.domain), (↑y : E) = (fst, snd).1 ∧ (↑f : ↥f.domain → F) y = (fst, snd).2)
    (h : fst = x_fst ∧ z • snd = x_snd),
    ∃ (y : ↥(z • f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ (z • f).graph

Tactic:
rw [mem_graph_iff] at hx' ⊢

Premises used: LinearPMap.mem_graph_iff
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst : E
snd : F
hx' : ∃ (y : ↥f.domain), (↑y : E) = (fst, snd).1 ∧ (↑f : ↥f.domain → F) y = (fst, snd).2
h : fst = x_fst ∧ z • snd = x_snd
h₁ :
  ∀ (y : ↥f.domain) (hy : (↑y : E) = (fst, snd).1) (hx' : (↑f : ↥f.domain → F) y = (fst, snd).2),
    ∃ (y : ↥(z • f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2
⊢ ∃ (y : ↥(z • f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2

Tactic:
rcases hx' with ⟨y, hy, hx'⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst : E
snd : F
h : fst = x_fst ∧ z • snd = x_snd
y : ↥f.domain
hy : (↑y : E) = (fst, snd).1
hx' : (↑f : ↥f.domain → F) y = (fst, snd).2
h₁ : (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2
⊢ ∃ (y : ↥(z • f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2

Tactic:
use y
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst : E
snd : F
h : fst = x_fst ∧ z • snd = x_snd
y : ↥f.domain
hy : (↑y : E) = (fst, snd).1
hx' : (↑f : ↥f.domain → F) y = (fst, snd).2
h₁ : (↑y : E) = (fst, z • snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (fst, z • snd).2
⊢ (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2

Tactic:
rw [← h.1, ← h.2]

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst : E
snd : F
h : fst = x_fst ∧ z • snd = x_snd
y : ↥f.domain
hy : (↑y : E) = (fst, snd).1
hx' : (↑f : ↥f.domain → F) y = (fst, snd).2
⊢ (↑y : E) = (fst, z • snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (fst, z • snd).2

Tactic:
simp [hy, hx']
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
h :
  ∀ (x_fst : E) (x_snd : F),
    (x_fst, x_snd) ∈ (-f).graph ↔
      (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph
⊢ (-f).graph = Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph

Tactic:
ext ⟨x_fst, x_snd⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
h :
  (x_fst, x_snd) ∈ (-f).graph → (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph
h₁ :
  (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph → (x_fst, x_snd) ∈ (-f).graph
⊢ (x_fst, x_snd) ∈ (-f).graph ↔ (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ (-f).graph
⊢ ∃ (y : ↥(-f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2

Tactic:
rw [mem_graph_iff] at h

Premises used: LinearPMap.mem_graph_iff
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
h : ∃ (y : ↥(-f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2
h₁ :
  ∀ (y : ↥(-f).domain) (hy : (↑y : E) = (x_fst, x_snd).1) (h : (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2),
    (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph

Tactic:
rcases h with ⟨y, hy, h⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
y : ↥(-f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2
⊢ -(↑f : ↥f.domain → F) y = (x_fst, x_snd).2

Tactic:
rw [LinearPMap.neg_apply] at h

Premises used: LinearPMap.neg_apply
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
y : ↥(-f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : -(↑f : ↥f.domain → F) y = (x_fst, x_snd).2
h₁ : ∃ (a : E) (a_1 : ↥f.domain), (↑a_1 : E) = a ∧ a = x_fst ∧ -(↑f : ↥f.domain → F) a_1 = x_snd
⊢ ∃ y ∈ f.graph, (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) y = (x_fst, x_snd)

Tactic:
simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id,
      LinearMap.neg_apply, Prod.mk_inj, Prod.exists, exists_exists_and_eq_and]

Premises used: LinearMap.prodMap_apply, LinearMap.id_coe, Prod.mk_inj, LinearMap.neg_apply, id, LinearPMap.mem_graph_iff, exists_exists_and_eq_and, Prod.exists
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
y : ↥(-f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : -(↑f : ↥f.domain → F) y = (x_fst, x_snd).2
w : E
w₁ : ↥f.domain
left : (↑y : E) = x_fst
right : x_fst = x_fst ∧ -(↑f : ↥f.domain → F) y = x_snd
⊢ ∃ (a : E) (a_1 : ↥f.domain), (↑a_1 : E) = a ∧ a = x_fst ∧ -(↑f : ↥f.domain → F) a_1 = x_snd

Tactic:
use x_fst, y, hy
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph
⊢ ∃ y ∈ f.graph, (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) y = (x_fst, x_snd)

Tactic:
rw [Submodule.mem_map] at h

Premises used: Submodule.mem_map
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
h : ∃ y ∈ f.graph, (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) y = (x_fst, x_snd)
h₁ :
  ∀ (x' : E × F) (hx' : x' ∈ f.graph)
    (h : (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) x' = (x_fst, x_snd)),
    (x_fst, x_snd) ∈ (-f).graph
⊢ (x_fst, x_snd) ∈ (-f).graph

Tactic:
rcases h with ⟨x', hx', h⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
x' : E × F
hx' : x' ∈ f.graph
h : (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) x' = (x_fst, x_snd)
h₁ :
  ∀ (fst : E) (snd : F) (hx' : (fst, snd) ∈ f.graph)
    (h : (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) (fst, snd) = (x_fst, x_snd)),
    (x_fst, x_snd) ∈ (-f).graph
⊢ (x_fst, x_snd) ∈ (-f).graph

Tactic:
cases x'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
fst : E
snd : F
hx' : (fst, snd) ∈ f.graph
h : (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) (fst, snd) = (x_fst, x_snd)
⊢ fst = x_fst ∧ -snd = x_snd

Tactic:
simp only [LinearMap.prodMap_apply, LinearMap.id_coe, id, LinearMap.neg_apply,
    Prod.mk_inj] at h

Premises used: LinearMap.prodMap_apply, LinearMap.id_coe, Prod.mk_inj, LinearMap.neg_apply, id
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
fst : E
snd : F
hx' : (fst, snd) ∈ f.graph
h : fst = x_fst ∧ -snd = x_snd
h₁ :
  ∀ (hx' : ∃ (y : ↥f.domain), (↑y : E) = (fst, snd).1 ∧ (↑f : ↥f.domain → F) y = (fst, snd).2)
    (h : fst = x_fst ∧ -snd = x_snd),
    ∃ (y : ↥(-f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ (-f).graph

Tactic:
rw [mem_graph_iff] at hx' ⊢

Premises used: LinearPMap.mem_graph_iff
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
fst : E
snd : F
hx' : ∃ (y : ↥f.domain), (↑y : E) = (fst, snd).1 ∧ (↑f : ↥f.domain → F) y = (fst, snd).2
h : fst = x_fst ∧ -snd = x_snd
h₁ :
  ∀ (y : ↥f.domain) (hy : (↑y : E) = (fst, snd).1) (hx' : (↑f : ↥f.domain → F) y = (fst, snd).2),
    ∃ (y : ↥(-f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2
⊢ ∃ (y : ↥(-f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2

Tactic:
rcases hx' with ⟨y, hy, hx'⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
fst : E
snd : F
h : fst = x_fst ∧ -snd = x_snd
y : ↥f.domain
hy : (↑y : E) = (fst, snd).1
hx' : (↑f : ↥f.domain → F) y = (fst, snd).2
h₁ : (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2
⊢ ∃ (y : ↥(-f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2

Tactic:
use y
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
fst : E
snd : F
h : fst = x_fst ∧ -snd = x_snd
y : ↥f.domain
hy : (↑y : E) = (fst, snd).1
hx' : (↑f : ↥f.domain → F) y = (fst, snd).2
h₁ : (↑y : E) = (fst, -snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (fst, -snd).2
⊢ (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2

Tactic:
rw [← h.1, ← h.2]

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
fst : E
snd : F
h : fst = x_fst ∧ -snd = x_snd
y : ↥f.domain
hy : (↑y : E) = (fst, snd).1
hx' : (↑f : ↥f.domain → F) y = (fst, snd).2
⊢ (↑y : E) = (fst, -snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (fst, -snd).2

Tactic:
simp [hy, hx']
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x y : E
x' y' : F
hx : (x, x') ∈ f.graph
hy : (y, y') ∈ f.graph
hxy : x = y
⊢ x' = y'

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x y : E × F
hx : x ∈ f.graph
hy : y ∈ f.graph
hxy : x.1 = y.1
⊢ x.2 = y.2

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x : E
x' : F
h : (x, x') ∈ f.graph
hx : x = 0
⊢ x' = 0

Tactic:
f.mem_graph_snd_inj h f.graph.zero_mem hx

Premises used: Submodule.zero_mem, LinearPMap.graph, LinearPMap.mem_graph_snd_inj
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x : E
mp : x ∈ f.domain → ∃ (y : F), (x, y) ∈ f.graph
mpr : (∃ (y : F), (x, y) ∈ f.graph) → x ∈ f.domain
⊢ x ∈ f.domain ↔ ∃ (y : F), (x, y) ∈ f.graph

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
h₁ : (x, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x h)) ∈ f.graph
⊢ ∃ (y : F), (x, y) ∈ f.graph

Tactic:
use f ⟨x, h⟩

Premises used: Subtype.mk, LinearPMap.toFun'