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
c_1 : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c_1
cne : c_1.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c_1)
P : (x : ↥(sSup (domain '' c_1))) → { p : (↑c_1 : Type (max u_4 u_5)) // (↑x : E) ∈ (↑p : E →ₛₗ.[σ] F).domain }
f : ↥(sSup (domain '' c_1)) → F :=
  fun (x : ↥(sSup (domain '' c_1))) ↦
    (↑(↑(↑(P x) : (↑c_1 : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) :
        ↥(↑(↑(P x) : (↑c_1 : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c_1 : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E)
        ⋯)
f_eq :
  ∀ (p : (↑c_1 : Type (max u_4 u_5))) (x : ↥(sSup (domain '' c_1))) (y : ↥(↑p : E →ₛₗ.[σ] F).domain)
    (_hxy : (↑x : E) = (↑y : E)), f x = (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) y
c : R
x : ↥(sSup (domain '' c_1))
w :
  (↑(↑(↑(P x) : (↑c_1 : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) :
        ↥(↑(↑(P x) : (↑c_1 : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain → F)
      (c •
        Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c_1 : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E)
          ⋯) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) (f x)
w₁ w₂ :
  (↑(↑(↑(P x) : (↑c_1 : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) :
        ↥(↑(↑(P x) : (↑c_1 : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain → F)
      (c •
        Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c_1 : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E)
          ⋯) =
    (↑(↑(↑(P x) : (↑c_1 : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) :
        ↥(↑(↑(P x) : (↑c_1 : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain → F)
      (c •
        Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c_1 : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E)
          ⋯)
⊢ f (c • x) = HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) (f x)

Tactic:
rw [f_eq (P x).1 (c • x) (c • ⟨x, (P x).2⟩) rfl, ← map_smulₛₗ]

Premises used: LinearPMap.map_smulₛₗ, HSMul.hSMul, Subtype.val
-- 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p : (↑c : Type (max u_4 u_5)) // (↑x : E) ∈ (↑p : E →ₛₗ.[σ] F).domain }
f : ↥(sSup (domain '' c)) → F :=
  fun (x : ↥(sSup (domain '' c))) ↦
    (↑(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) :
        ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E) ⋯)
f_eq :
  ∀ (p : (↑c : Type (max u_4 u_5))) (x : ↥(sSup (domain '' c))) (y : ↥(↑p : E →ₛₗ.[σ] F).domain)
    (_hxy : (↑x : E) = (↑y : E)), f x = (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) y
p : E →ₛₗ.[σ] F
hpc : p ∈ c
⊢ p ≤
    { domain := sSup (domain '' c),
      toFun :=
        { toFun := f, map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F } }

Tactic:
⟨le_sSup <| Set.mem_image_of_mem domain hpc, fun x y hxy => Eq.symm ?_⟩

Premises used: Set.mem_image_of_mem, And.intro, le_sSup, Eq.symm, LinearPMap.domain
-- 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p : (↑c : Type (max u_4 u_5)) // (↑x : E) ∈ (↑p : E →ₛₗ.[σ] F).domain }
f : ↥(sSup (domain '' c)) → F :=
  fun (x : ↥(sSup (domain '' c))) ↦
    (↑(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) :
        ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E) ⋯)
f_eq :
  ∀ (p : (↑c : Type (max u_4 u_5))) (x : ↥(sSup (domain '' c))) (y : ↥(↑p : E →ₛₗ.[σ] F).domain)
    (_hxy : (↑x : E) = (↑y : E)), f x = (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) y
p : E →ₛₗ.[σ] F
hpc : p ∈ c
h :
  ∀ (x : ↥p.domain)
    (y :
      ↥(domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ)
          { domain := sSup (domain '' c),
            toFun :=
              { toFun := f, map_add' := ⋯, map_smul' := ⋯ :
                LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F } :
            E →ₛₗ.[σ] F }))
    (hxy : (↑x : E) = (↑y : E)),
    (↑{ domain := sSup (domain '' c),
              toFun :=
                { toFun := f, map_add' := ⋯, map_smul' := ⋯ :
                  LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F } :
              E →ₛₗ.[σ] F } :
          ↥{ domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } }.domain → F)
        y =
      (↑p : ↥p.domain → F) x
⊢ p ≤
    { domain := sSup (domain '' c),
      toFun :=
        { toFun := f, map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F } }

Tactic:
refine ⟨le_sSup <| Set.mem_image_of_mem domain hpc, fun x y hxy => Eq.symm ?_⟩
-- 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p : (↑c : Type (max u_4 u_5)) // (↑x : E) ∈ (↑p : E →ₛₗ.[σ] F).domain }
f : ↥(sSup (domain '' c)) → F :=
  fun (x : ↥(sSup (domain '' c))) ↦
    (↑(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) :
        ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E) ⋯)
f_eq :
  ∀ (p : (↑c : Type (max u_4 u_5))) (x : ↥(sSup (domain '' c))) (y : ↥(↑p : E →ₛₗ.[σ] F).domain)
    (_hxy : (↑x : E) = (↑y : E)), f x = (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) y
p : E →ₛₗ.[σ] F
hpc : p ∈ c
x : ↥p.domain
y :
  ↥(domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ)
      { domain := sSup (domain '' c),
        toFun :=
          { toFun := f, map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F } :
        E →ₛₗ.[σ] F })
hxy : (↑x : E) = (↑y : E)
⊢ (↑{ domain := sSup (domain '' c),
            toFun :=
              { toFun := f, map_add' := ⋯, map_smul' := ⋯ :
                LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F } :
            E →ₛₗ.[σ] F } :
        ↥{ domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } }.domain → F)
      y =
    (↑p : ↥p.domain → F) x

Tactic:
f_eq ⟨p, hpc⟩ _ _ hxy.symm

Premises used: iInf, Set.iInter, setOf, Subtype.mk, Eq.symm, 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p : (↑c : Type (max u_4 u_5)) // (↑x : E) ∈ (↑p : E →ₛₗ.[σ] F).domain }
f : ↥(sSup (domain '' c)) → F :=
  fun (x : ↥(sSup (domain '' c))) ↦
    (↑(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) :
        ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E) ⋯)
f_eq :
  ∀ (p : (↑c : Type (max u_4 u_5))) (x : ↥(sSup (domain '' c))) (y : ↥(↑p : E →ₛₗ.[σ] F).domain)
    (_hxy : (↑x : E) = (↑y : E)), f x = (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) y
p : E →ₛₗ.[σ] F
hpc : p ∈ c
x : ↥p.domain
y :
  ↥(domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ)
      { domain := sSup (domain '' c),
        toFun :=
          { toFun := f, map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F } :
        E →ₛₗ.[σ] F })
hxy : (↑x : E) = (↑y : E)
⊢ (↑{ domain := sSup (domain '' c),
            toFun :=
              { toFun := f, map_add' := ⋯, map_smul' := ⋯ :
                LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F } :
            E →ₛₗ.[σ] F } :
        ↥{ domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } }.domain → F)
      y =
    (↑p : ↥p.domain → F) x

Tactic:
exact f_eq ⟨p, hpc⟩ _ _ hxy.symm

Premises used: Subtype.mk, Eq.symm
-- 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
⊢ (LinearPMap.sSup c hc).domain = sSup (domain '' c)

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
c : Set (E →ₛₗ.[σ] F)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
x : E
rw : (∃ y ∈ domain '' c, x ∈ y) ↔ ∃ f ∈ c, x ∈ f.domain
⊢ x ∈ (LinearPMap.sSup c hc).domain ↔ ∃ f ∈ c, x ∈ f.domain

Tactic:
rw [domain_sSup, Submodule.mem_sSup_of_directed (hnonempty.image _)
    (DirectedOn.mono_comp LinearPMap.domain_mono.monotone hc)]

Premises used: StrictMono.monotone, DirectedOn.mono_comp, LinearPMap.domain_sSup, Set.Nonempty.image, Submodule.mem_sSup_of_directed, LinearPMap.domain_mono
-- 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
c : Set (E →ₛₗ.[σ] F)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
x : E
⊢ (∃ y ∈ domain '' c, x ∈ y) ↔ ∃ f ∈ c, x ∈ f.domain

Tactic:
simp
-- 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
f : E →ₛₗ.[σ] F
hf : f ∈ c
⊢ f ≤ LinearPMap.sSup c hc

Tactic:
Classical.choose_spec (sSup_aux c hc) hf

Premises used: Classical.choose_spec, _private.0.LinearPMap.sSup_aux
-- 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
g : E →ₛₗ.[σ] F
hg : ∀ f ∈ c, f ≤ g
⊢ LinearPMap.sSup c hc ≤ g

Tactic:
le_of_eqLocus_ge <|
    sSup_le fun _ ⟨f, hf, Eq⟩ =>
      Eq ▸
        have : f ≤ LinearPMap.sSup c hc ⊓ g := le_inf (LinearPMap.le_sSup _ hf) (hg f hf)
        this.1

Premises used: LinearPMap.le_of_eqLocus_ge
-- 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
l : E →ₛₗ.[σ] F
hl : l ∈ c
x : ↥l.domain
symm :
  (↑l : ↥l.domain → F) x =
    (↑(LinearPMap.sSup c hc) : ↥(LinearPMap.sSup c hc).domain → F)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hc).domain) (↑x : E) ⋯)
⊢ (↑(LinearPMap.sSup c hc) : ↥(LinearPMap.sSup c hc).domain → F)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hc).domain) (↑x : E) ⋯) =
    (↑l : ↥l.domain → F) x

Tactic:
symm
-- 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
p : Submodule R E
x : ↥p
⊢ (↑(f.toPMap p) : ↥(f.toPMap p).domain → F) x = (f : (a : E) → F) (↑x : E)

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
p : Submodule R E
⊢ (f.toPMap p).domain = p

Tactic:
rfl

Premises used: 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
g : F →ₛₗ[τ] G
f : E →ₛₗ.[σ] F
x : ↥(g.compPMap f).domain
⊢ (↑(g.compPMap f) : ↥(g.compPMap f).domain → G) x = (g : (a : F) → G) ((↑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
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
G : Type u_6
inst_5 : AddCommGroup G
inst_6 : Module R F
inst_7 : Module S G
f : E →ₛₗ.[σ] G
g : F →ₛₗ.[σ] G
x : ↥(f.coprod g).domain
⊢ (↑(f.coprod g) : ↥(f.coprod g).domain → G) x =
    (↑f : ↥f.domain → G) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (↑x : E × F).1 ⋯) +
      (↑g : ↥g.domain → G) (Subtype.mk (p := fun (x : F) ↦ x ∈ g.domain) (↑x : E × F).2 ⋯)

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S_1 : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S_1
inst_2 : Ring T
σ : R →+* S_1
τ : S_1 →+* 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_1 F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
S : Submodule R E
⊢ S ⊓ f.domain ≤ f.domain

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S_1 : Type u_2
inst : Ring R
inst_1 : Ring S_1
σ : R →+* S_1
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_1 F
f : E →ₛₗ.[σ] F
S : Submodule R E
⊢ (f.domRestrict S).domain = S ⊓ f.domain

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S_1 : Type u_2
inst : Ring R
inst_1 : Ring S_1
σ : R →+* S_1
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_1 F
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
⊢ S ⊓ f.domain ≤ f.domain

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S_1 : Type u_2
inst : Ring R
inst_1 : Ring S_1
σ : R →+* S_1
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_1 F
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
a : (↑((Submodule.inclusion ⋯ : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x) : E) = (↑y : E)
⊢ (Submodule.inclusion ⋯ : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x = y

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S_1 : Type u_2
inst : Ring R
inst_1 : Ring S_1
σ : R →+* S_1
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_1 F
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
⊢ (↑((Submodule.inclusion ⋯ : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x) : E) = (↑y : E)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S_1 : Type u_2
inst : Ring R
inst_1 : Ring S_1
σ : R →+* S_1
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_1 F
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
⊢ (Submodule.inclusion ⋯ : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x = y

Tactic:
have : Submodule.inclusion (by simp) x = y := by
    ext
    simp [h]
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S_1 : Type u_2
inst : Ring R
inst_1 : Ring S_1
σ : R →+* S_1
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_1 F
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
this : (Submodule.inclusion ⋯ : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x = y
rw :
  (↑(f.domRestrict S) : ↥(f.domRestrict S).domain → F) x =
    (↑f : ↥f.domain → F) ((Submodule.inclusion ⋯ : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x)
⊢ (↑(f.domRestrict S) : ↥(f.domRestrict S).domain → F) x = (↑f : ↥f.domain → F) y

Tactic:
rw [← this]
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S_1 : Type u_2
inst : Ring R
inst_1 : Ring S_1
σ : R →+* S_1
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_1 F
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
this : (Submodule.inclusion ⋯ : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x = y
⊢ (↑(f.domRestrict S) : ↥(f.domRestrict S).domain → F) x =
    (↑f : ↥f.domain → F) ((Submodule.inclusion ⋯ : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x)

Tactic:
LinearPMap.mk_apply _ _ _

Premises used: LinearPMap.mk_apply, LinearPMap.domRestrict, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S_1 : Type u_2
inst : Ring R
inst_1 : Ring S_1
σ : R →+* S_1
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_1 F
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
this : (Submodule.inclusion ⋯ : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x = y
⊢ (↑(f.domRestrict S) : ↥(f.domRestrict S).domain → F) x =
    (↑f : ↥f.domain → F) ((Submodule.inclusion ⋯ : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x)

Tactic:
exact LinearPMap.mk_apply _ _ _

Premises used: LinearPMap.mk_apply
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S_1 : Type u_2
inst : Ring R
inst_1 : Ring S_1
σ : R →+* S_1
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_1 F
f : E →ₛₗ.[σ] F
S : Submodule R E
⊢ (f.domRestrict S).domain ≤ f.domain

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
inst_4 : Module R F
f : E →ₗ.[R] F
x : E × F
⊢ x ∈ f.graph ↔ ∃ (y : ↥f.domain), ((↑y : E), (↑f : ↥f.domain → F) y) = x

Tactic:
simp [graph]

Premises used: LinearPMap.graph
-- 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 × F
mk :
  ∀ (fst : E) (snd : F),
    (fst, snd) ∈ f.graph ↔ ∃ (y : ↥f.domain), (↑y : E) = (fst, snd).1 ∧ (↑f : ↥f.domain → F) y = (fst, snd).2
⊢ x ∈ f.graph ↔ ∃ (y : ↥f.domain), (↑y : E) = x.1 ∧ (↑f : ↥f.domain → F) y = x.2

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
fst : E
snd : F
mk mk₁ : (fst, snd) ∈ f.graph ↔ ∃ (y : ↥f.domain), (↑y : E) = fst ∧ (↑f : ↥f.domain → F) y = snd
mk₂ :
  (∃ (y : ↥f.domain), ((↑y : E), (↑f : ↥f.domain → F) y) = (fst, snd)) ↔
    ∃ (y : ↥f.domain), (↑y : E) = fst ∧ (↑f : ↥f.domain → F) y = snd
⊢ (fst, snd) ∈ f.graph ↔ ∃ (y : ↥f.domain), (↑y : E) = (fst, snd).1 ∧ (↑f : ↥f.domain → F) y = (fst, snd).2

Tactic:
simp_rw [mem_graph_iff', Prod.mk_inj]

Premises used: Prod.mk_inj, 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 : ↥f.domain
⊢ ((↑x : E), (↑f : ↥f.domain → F) x) ∈ f.graph

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
inst_4 : Module R F
f : E →ₗ.[R] F
h : ∀ (x : E), x ∈ Submodule.map (LinearMap.fst R E F) f.graph ↔ x ∈ f.domain
⊢ Submodule.map (LinearMap.fst R E F) f.graph = f.domain

Tactic:
ext 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 : E
h :
  (∃ (x_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) = x_1) ↔
    x ∈ f.domain
⊢ x ∈ Submodule.map (LinearMap.fst R E F) f.graph ↔ x ∈ f.domain

Tactic:
simp only [Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left,
    LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]

Premises used: Submodule.mem_map, Subtype.exists, exists_eq_right, exists_and_left, exists_eq_left, exists_and_right, LinearPMap.mem_graph_iff, 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
f : E →ₗ.[R] F
x : E
h :
  (∃ (x_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) = x_1) →
    x ∈ f.domain
h₁ :
  x ∈ f.domain →
    ∃ (x_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) = x_1
⊢ (∃ (x_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) = x_1) ↔
    x ∈ f.domain

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_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) = x_1
h₁ :
  ∀ (x_1 : F) (hx : x ∈ f.domain),
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) = x_1 → x ∈ f.domain
⊢ x ∈ f.domain

Tactic:
rcases h with ⟨x, 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_1 : E
x : F
hx : x_1 ∈ f.domain
h : (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x_1 ⋯) = x
⊢ x_1 ∈ f.domain

Tactic:
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_1 : E
x : F
hx : x_1 ∈ f.domain
h : (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x_1 ⋯) = x
⊢ x_1 ∈ f.domain

Tactic:
exact hx