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
g : Submodule R (E × F)
hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
hy : (0, y₁ - y₂) ∈ g
⊢ y₁ = y₂

Tactic:
exact sub_eq_zero.mp (hg hy (by simp))

Premises used: sub_eq_zero, Iff.mp
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ (a, valFromGraph hg ha) ∈ g

Tactic:
(ExistsUnique.exists (existsUnique_from_graph @hg ha)).choose_spec

Premises used: Exists.choose_spec, ExistsUnique.exists, Set.Mem, Submodule.valFromGraph, Submodule.existsUnique_from_graph
-- 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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
⊢ (↑v : E) + (↑w : E) ∈ map (LinearMap.fst R E F) g

Tactic:
have hadd := (g.map (LinearMap.fst R E F)).add_mem v.2 w.2
-- 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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
hadd : (↑v : E) + (↑w : E) ∈ map (LinearMap.fst R E F) g
⊢ ((↑v : E) + (↑w : E), valFromGraph hg hadd) ∈ g

Tactic:
have hvw := valFromGraph_mem hg hadd
-- 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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
hadd : (↑v : E) + (↑w : E) ∈ map (LinearMap.fst R E F) g
hvw : ((↑v : E) + (↑w : E), valFromGraph hg hadd) ∈ g
⊢ ((↑v : E), valFromGraph hg ⋯) + ((↑w : E), valFromGraph hg ⋯) ∈ g

Tactic:
have hvw' := g.add_mem (valFromGraph_mem hg v.2) (valFromGraph_mem hg w.2)
-- 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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
hadd : (↑v : E) + (↑w : E) ∈ map (LinearMap.fst R E F) g
hvw : ((↑v : E) + (↑w : E), valFromGraph hg hadd) ∈ g
hvw' : ((↑v : E), valFromGraph hg ⋯) + ((↑w : E), valFromGraph hg ⋯) ∈ g
⊢ ((↑v : E) + (↑w : E), valFromGraph hg ⋯ + valFromGraph hg ⋯) ∈ g

Tactic:
rw [Prod.mk_add_mk] at hvw'

Premises used: Prod.mk_add_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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
hadd : (↑v : E) + (↑w : E) ∈ map (LinearMap.fst R E F) g
hvw : ((↑v : E) + (↑w : E), valFromGraph hg hadd) ∈ g
hvw' : ((↑v : E) + (↑w : E), valFromGraph hg ⋯ + valFromGraph hg ⋯) ∈ g
⊢ valFromGraph hg ⋯ = valFromGraph hg ⋯ + valFromGraph hg ⋯

Tactic:
(existsUnique_from_graph @hg hadd).unique hvw hvw'

Premises used: Submodule.existsUnique_from_graph, ExistsUnique.unique
-- 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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
hadd : (↑v : E) + (↑w : E) ∈ map (LinearMap.fst R E F) g
hvw : ((↑v : E) + (↑w : E), valFromGraph hg hadd) ∈ g
hvw' : ((↑v : E) + (↑w : E), valFromGraph hg ⋯ + valFromGraph hg ⋯) ∈ g
⊢ valFromGraph hg ⋯ = valFromGraph hg ⋯ + valFromGraph hg ⋯

Tactic:
exact (existsUnique_from_graph @hg hadd).unique hvw hvw'

Premises used: Submodule.existsUnique_from_graph, ExistsUnique.unique
-- 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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : R
v : ↥(map (LinearMap.fst R E F) g)
⊢ a • (↑v : E) ∈ map (LinearMap.fst R E F) g

Tactic:
have hsmul := (g.map (LinearMap.fst R E F)).smul_mem a v.2
-- 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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : R
v : ↥(map (LinearMap.fst R E F) g)
hsmul : a • (↑v : E) ∈ map (LinearMap.fst R E F) g
⊢ (a • (↑v : E), valFromGraph hg hsmul) ∈ g

Tactic:
have hav := valFromGraph_mem hg hsmul
-- 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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : R
v : ↥(map (LinearMap.fst R E F) g)
hsmul : a • (↑v : E) ∈ map (LinearMap.fst R E F) g
hav : (a • (↑v : E), valFromGraph hg hsmul) ∈ g
⊢ a • ((↑v : E), valFromGraph hg ⋯) ∈ g

Tactic:
have hav' := g.smul_mem a (valFromGraph_mem hg v.2)
-- 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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : R
v : ↥(map (LinearMap.fst R E F) g)
hsmul : a • (↑v : E) ∈ map (LinearMap.fst R E F) g
hav : (a • (↑v : E), valFromGraph hg hsmul) ∈ g
hav' : a • ((↑v : E), valFromGraph hg ⋯) ∈ g
⊢ (a • (↑v : E), a • valFromGraph hg ⋯) ∈ g

Tactic:
rw [Prod.smul_mk] at hav'

Premises used: Prod.smul_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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : R
v : ↥(map (LinearMap.fst R E F) g)
hsmul : a • (↑v : E) ∈ map (LinearMap.fst R E F) g
hav : (a • (↑v : E), valFromGraph hg hsmul) ∈ g
hav' : (a • (↑v : E), a • valFromGraph hg ⋯) ∈ g
⊢ valFromGraph hg ⋯ = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (valFromGraph hg ⋯)

Tactic:
(existsUnique_from_graph @hg hsmul).unique hav hav'

Premises used: Submodule.existsUnique_from_graph, ExistsUnique.unique
-- 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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : R
v : ↥(map (LinearMap.fst R E F) g)
hsmul : a • (↑v : E) ∈ map (LinearMap.fst R E F) g
hav : (a • (↑v : E), valFromGraph hg hsmul) ∈ g
hav' : (a • (↑v : E), a • valFromGraph hg ⋯) ∈ g
⊢ valFromGraph hg ⋯ = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (valFromGraph hg ⋯)

Tactic:
exact (existsUnique_from_graph @hg hsmul).unique hav hav'

Premises used: Submodule.existsUnique_from_graph, ExistsUnique.unique
-- 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
g : Submodule R (E × F)
⊢ g.toLinearPMap.domain = map (LinearMap.fst R E F) g

Tactic:
rfl

Premises used: Submodule.map, rfl
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
change :
  (if hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0 then g.toLinearPMapAux hg else 0 :
        (a : ↥(map (LinearMap.fst R E F) g)) → F)
      x =
    valFromGraph hg ⋯
⊢ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) x = valFromGraph hg ⋯

Tactic:
change (if hg : _ then g.toLinearPMapAux hg else 0) 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
rw : (g.toLinearPMapAux hg : (a : ↥(map (LinearMap.fst R E F) g)) → F) x = valFromGraph hg ⋯
hc : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
⊢ (if hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0 then g.toLinearPMapAux hg else 0 :
        (a : ↥(map (LinearMap.fst R E F) g)) → F)
      x =
    valFromGraph hg ⋯

Tactic:
rw [dif_pos]

Premises used: dif_pos
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (g.toLinearPMapAux hg : (a : ↥(map (LinearMap.fst R E F) g)) → F) x = valFromGraph hg ⋯

Tactic:
rfl
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0

Tactic:
hg
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0

Tactic:
exact hg
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
change :
  (if hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0 then g.toLinearPMapAux hg else 0 :
        (a : ↥(map (LinearMap.fst R E F) g)) → F)
      x =
    valFromGraph hg ⋯
change₁ : (g.toLinearPMapAux hg : (a : ↥(map (LinearMap.fst R E F) g)) → F) x = valFromGraph hg ⋯
hc hc₁ : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
⊢ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) x = valFromGraph hg ⋯

Tactic:
classical
  change (if hg : _ then g.toLinearPMapAux hg else 0) x = _
  rw [dif_pos]
  · rfl
  · exact hg

Premises used: dif_pos
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
rw : ((↑x : E), valFromGraph hg ⋯) ∈ g
⊢ ((↑x : E), (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) x) ∈ g

Tactic:
rw [toLinearPMap_apply_aux hg]

Premises used: Submodule.toLinearPMap_apply_aux
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ ((↑x : E), valFromGraph hg ⋯) ∈ g

Tactic:
valFromGraph_mem hg x.2

Premises used: Submodule.valFromGraph_mem, Subtype.property
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ ((↑x : E), valFromGraph hg ⋯) ∈ g

Tactic:
exact valFromGraph_mem hg x.2

Premises used: Submodule.valFromGraph_mem, Subtype.property
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
h : ∀ (x_fst : E) (x_snd : F), (x_fst, x_snd) ∈ g.toLinearPMap.graph ↔ (x_fst, x_snd) ∈ g
⊢ g.toLinearPMap.graph = g

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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ g.toLinearPMap.graph → (x_fst, x_snd) ∈ g
h₁ : (x_fst, x_snd) ∈ g → (x_fst, x_snd) ∈ g.toLinearPMap.graph
⊢ (x_fst, x_snd) ∈ g.toLinearPMap.graph ↔ (x_fst, x_snd) ∈ g

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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g.toLinearPMap.graph
⊢ ∃ (y : ↥g.toLinearPMap.domain),
    (↑y : E) = (x_fst, x_snd).1 ∧ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2

Tactic:
rw [LinearPMap.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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx :
  ∃ (y : ↥g.toLinearPMap.domain),
    (↑y : E) = (x_fst, x_snd).1 ∧ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2
h :
  ∀ (y : ↥g.toLinearPMap.domain) (hx1 : (↑y : E) = (x_fst, x_snd).1)
    (hx2 : (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2), (x_fst, x_snd) ∈ g
⊢ (x_fst, x_snd) ∈ g

Tactic:
rcases hx with ⟨y, hx1, hx2⟩
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
y : ↥g.toLinearPMap.domain
hx1 : (↑y : E) = (x_fst, x_snd).1
hx2 : (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2
⊢ ((↑y : E), (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y) ∈ g

Tactic:
g.mem_graph_toLinearPMap hg y

Premises used: Submodule.mem_graph_toLinearPMap
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
y : ↥g.toLinearPMap.domain
hx1 : (↑y : E) = (x_fst, x_snd).1
hx2 : (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2
h : (x_fst, x_snd) = ((↑y : E), (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y)
⊢ (x_fst, x_snd) ∈ g

Tactic:
convert! g.mem_graph_toLinearPMap hg y using 1

Premises used: Submodule.mem_graph_toLinearPMap
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
y : ↥g.toLinearPMap.domain
hx1 : (↑y : E) = (x_fst, x_snd).1
hx2 : (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) = ((↑y : E), (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y)

Tactic:
Prod.ext hx1.symm hx2.symm

Premises used: Prod.ext, Eq.symm
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
y : ↥g.toLinearPMap.domain
hx1 : (↑y : E) = (x_fst, x_snd).1
hx2 : (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) = ((↑y : E), (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y)

Tactic:
exact Prod.ext hx1.symm hx2.symm

Premises used: Prod.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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
h :
  ∃ (y : ↥g.toLinearPMap.domain),
    (↑y : E) = (x_fst, x_snd).1 ∧ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ g.toLinearPMap.graph

Tactic:
rw [LinearPMap.mem_graph_iff]

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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
simp : ∃ (x : F), (x_fst, x) ∈ g
⊢ x_fst ∈ map (LinearMap.fst R E F) g

Tactic:
simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]

Premises used: Submodule.mem_map, exists_eq_right, exists_and_right, LinearMap.fst_apply, 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ ∃ (x : F), (x_fst, x) ∈ g

Tactic:
⟨x_snd, hx⟩

Premises used: Exists.intro
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ ∃ (x : F), (x_fst, x) ∈ g

Tactic:
exact ⟨x_snd, 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ x_fst ∈ map (LinearMap.fst R E F) g

Tactic:
have hx_fst : x_fst ∈ g.map (LinearMap.fst R E F) := by
    simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
    exact ⟨x_snd, 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ ∃ (y : ↥g.toLinearPMap.domain),
    (↑y : E) = (x_fst, x_snd).1 ∧ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2

Tactic:
⟨⟨x_fst, hx_fst⟩, Subtype.coe_mk x_fst hx_fst, ?_⟩

Premises used: Subtype.coe_mk, Subtype.mk, And.intro, Exists.intro
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
h :
  (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ g.toLinearPMap.domain) x_fst hx_fst) =
    (x_fst, x_snd).2
⊢ ∃ (y : ↥g.toLinearPMap.domain),
    (↑y : E) = (x_fst, x_snd).1 ∧ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2

Tactic:
refine ⟨⟨x_fst, hx_fst⟩, Subtype.coe_mk x_fst hx_fst, ?_⟩
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
h : valFromGraph hg ⋯ = (x_fst, x_snd).2
⊢ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ g.toLinearPMap.domain) x_fst hx_fst) =
    (x_fst, x_snd).2

Tactic:
rw [toLinearPMap_apply_aux hg]

Premises used: Submodule.toLinearPMap_apply_aux
-- 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ valFromGraph hg ⋯ = (x_fst, x_snd).2

Tactic:
(existsUnique_from_graph @hg hx_fst).unique (valFromGraph_mem hg hx_fst) hx

Premises used: Submodule.existsUnique_from_graph, ExistsUnique.unique, Submodule.valFromGraph_mem