awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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).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 + g).domain = domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0

Tactic:
rcases h' with ⟨hdom, 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
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
hdom : (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)

Tactic:
rcases h' with ⟨hdom, 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
hf : x ∈ (-f).domain
hg : x ∈ g.domain
hdom : (f + g).domain = domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0
h' :
  ∀ ⦃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)
⊢ (f + g).domain = ⊤

Tactic:
rw [zero_domain] at hdom

Premises used: LinearPMap.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
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
hdom : (f + g).domain = domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0
h' :
  ∀ ⦃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)
hdom₁ : (f + g).domain = ⊤
⊢ ∀ ⦃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)

Tactic:
rw [zero_domain] at hdom

Premises used: LinearPMap.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
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
hdom : (f + g).domain = ⊤
h' :
  ∀ ⦃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⦄, (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x ⋯) = 0

Tactic:
simp only [hdom, zero_domain, mem_top, zero_apply, forall_true_left] at h'

Premises used: LinearPMap.zero_domain, forall_true_left, Submodule.mem_top, LinearPMap.zero_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
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
hdom : (f + g).domain = ⊤
h' : ∀ ⦃x : E⦄, (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x ⋯) = 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:
apply 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
σ_1 : 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
K : Type u_7
L : Type u_8
inst_9 : DivisionRing K
inst_10 : DivisionRing L
σ : K →+* L
inst_11 : Module K E
inst_12 : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
⊢ Disjoint f.domain (domain.{u_7, u_8, u_4, u_5} (S := L) (σ := σ) (mkSpanSingleton x y ⋯))

Tactic:
simpa [disjoint_span_singleton] using fun h ↦ False.elim <| hx h

Premises used: False.elim, Submodule.disjoint_span_singleton
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
E : Type u_4
inst : AddCommGroup E
F : Type u_5
inst_1 : AddCommGroup F
K : Type u_7
L : Type u_8
inst_2 : DivisionRing K
inst_3 : DivisionRing L
σ : K →+* L
inst_4 : Module K E
inst_5 : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
⊢ (f.supSpanSingleton x y hx).domain = f.domain ⊔ K ∙ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
E : Type u_4
inst : AddCommGroup E
F : Type u_5
inst_1 : AddCommGroup F
K : Type u_7
L : Type u_8
inst_2 : DivisionRing K
inst_3 : DivisionRing L
σ : K →+* L
inst_4 : Module K E
inst_5 : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
x' : ↥(f.supSpanSingleton x y hx).domain
hx' : (↑x' : E) ∈ f.domain
⊢ (↑(f.supSpanSingleton x y hx) : ↥(f.supSpanSingleton x y hx).domain → F) x' =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (↑x' : E) hx')

Tactic:
simpa using supSpanSingleton_apply_mk f x y hx x' hx' 0
-- 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
inl :
  ∀ (hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) ∅),
    ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (Set.image (α := E →ₛₗ.[σ] F) domain ∅))) F),
      Membership.mem (γ := Set (E →ₛₗ.[σ] F)) (upperBounds ∅)
        { domain := sSup (Set.image (α := E →ₛₗ.[σ] F) domain ∅), toFun := f : E →ₛₗ.[σ] F }
inr :
  ∀ (cne : c.Nonempty),
    ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
      { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c
⊢ ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
    { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c

Tactic:
rcases c.eq_empty_or_nonempty with rfl | cne

Premises used: Set.eq_empty_or_nonempty, 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
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) ∅
⊢ ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (Set.image (α := E →ₛₗ.[σ] F) domain ∅))) F),
    Membership.mem (γ := Set (E →ₛₗ.[σ] F)) (upperBounds ∅)
      { domain := sSup (Set.image (α := E →ₛₗ.[σ] F) domain ∅), toFun := f : E →ₛₗ.[σ] F }

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
cne : c.Nonempty
⊢ DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c)

Tactic:
have hdir : DirectedOn (· ≤ ·) (domain '' c) :=
    directedOn_image.2 (hc.mono @(domain_mono.monotone))
-- 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)
x : ↥(sSup (domain '' c))
h : ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
⊢ { p : (↑c : Type (max u_4 u_5)) // (↑x : E) ∈ (↑p : E →ₛₗ.[σ] F).domain }

Tactic:
apply Classical.indefiniteDescription

Premises used: Classical.indefiniteDescription
-- 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)
x : ↥(sSup (domain '' c))
⊢ ∃ y ∈ domain '' c, (↑x : E) ∈ y

Tactic:
have := (mem_sSup_of_directed (cne.image _) hdir).1 x.2
-- 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)
x : ↥(sSup (domain '' c))
this : ∃ y ∈ domain '' c, (↑x : E) ∈ y
h :
  ∀ (this : ∃ x_1 ∈ c, (↑x : E) ∈ x_1.domain),
    ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
h₁ :
  ∀ (this : ∃ (x_1 : E →ₛₗ.[σ] F) (_ : x_1 ∈ c), (↑x : E) ∈ x_1.domain),
    ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
h₂ h₃ h₄ h₅ :
  ∀ (this : ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain),
    ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
⊢ ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain

Tactic:
rwa [Set.exists_mem_image, ← bex_def, SetCoe.exists'] at this

Premises used: SetCoe.exists', bex_def, Set.exists_mem_image
-- 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)
inr :
  ∀ (P : (x : ↥(sSup (domain '' c))) → { p : (↑c : Type (max u_4 u_5)) // (↑x : E) ∈ (↑p : E →ₛₗ.[σ] F).domain }),
    ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
      { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c
⊢ ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
    { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c

Tactic:
have P : ∀ x : ↥(sSup (domain '' c)), { p : c // (x : E) ∈ p.val.domain } := by
    rintro x
    apply Classical.indefiniteDescription
    have := (mem_sSup_of_directed (cne.image _) hdir).1 x.2
    rwa [Set.exists_mem_image, ← bex_def, SetCoe.exists'] at this
-- 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) ⋯)
p : (↑c : Type (max u_4 u_5))
x : ↥(sSup (domain '' c))
y : ↥(↑p : E →ₛₗ.[σ] F).domain
hxy : (↑x : E) = (↑y : E)
rcases :
  ∀ (q : E →ₛₗ.[σ] F) (_hqc : q ∈ c) (hxq1 : (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain ≤ q.domain)
    (hxq2 :
      ∀ ⦃x_1 : ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain⦄ ⦃y : ↥q.domain⦄
        (_h : (↑x_1 : E) = (↑y : E)),
        (↑(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) :
              ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain → F)
            x_1 =
          (↑q : ↥q.domain → F) y)
    (hpq1 : (↑p : E →ₛₗ.[σ] F).domain ≤ q.domain)
    (hpq2 :
      ∀ ⦃x : ↥(↑p : E →ₛₗ.[σ] F).domain⦄ ⦃y : ↥q.domain⦄ (_h : (↑x : E) = (↑y : E)),
        (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) x = (↑q : ↥q.domain → F) y),
    f x = (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) y
⊢ f x = (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) y

Tactic:
rcases hc (P x).1.1 (P x).1.2 p.1 p.2 with ⟨q, _hqc, ⟨hxq1, hxq2⟩, ⟨hpq1, hpq2⟩⟩

Premises used: Subtype.val, Subtype.property
-- 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) ⋯)
p : (↑c : Type (max u_4 u_5))
x : ↥(sSup (domain '' c))
y : ↥(↑p : E →ₛₗ.[σ] F).domain
hxy : (↑x : E) = (↑y : E)
q : E →ₛₗ.[σ] F
_hqc : q ∈ c
hxq1 : (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain ≤ q.domain
hxq2 :
  ∀ ⦃x_1 : ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain⦄ ⦃y : ↥q.domain⦄ (_h : (↑x_1 : E) = (↑y : E)),
    (↑(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) :
          ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain → F)
        x_1 =
      (↑q : ↥q.domain → F) y
hpq1 : (↑p : E →ₛₗ.[σ] F).domain ≤ q.domain
hpq2 :
  ∀ ⦃x : ↥(↑p : E →ₛₗ.[σ] F).domain⦄ ⦃y : ↥q.domain⦄ (_h : (↑x : E) = (↑y : E)),
    (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) x = (↑q : ↥q.domain → F) y
⊢ f x = (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) y

Tactic:
(hxq2 (y := ⟨y, hpq1 y.2⟩) hxy).trans (hpq2 rfl).symm

Premises used: Eq.symm, Eq.trans
-- 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) ⋯)
p : (↑c : Type (max u_4 u_5))
x : ↥(sSup (domain '' c))
y : ↥(↑p : E →ₛₗ.[σ] F).domain
hxy : (↑x : E) = (↑y : E)
q : E →ₛₗ.[σ] F
_hqc : q ∈ c
hxq1 : (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain ≤ q.domain
hxq2 :
  ∀ ⦃x_1 : ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain⦄ ⦃y : ↥q.domain⦄ (_h : (↑x_1 : E) = (↑y : E)),
    (↑(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) :
          ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain → F)
        x_1 =
      (↑q : ↥q.domain → F) y
hpq1 : (↑p : E →ₛₗ.[σ] F).domain ≤ q.domain
hpq2 :
  ∀ ⦃x : ↥(↑p : E →ₛₗ.[σ] F).domain⦄ ⦃y : ↥q.domain⦄ (_h : (↑x : E) = (↑y : E)),
    (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) x = (↑q : ↥q.domain → F) y
⊢ f x = (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) y

Tactic:
exact (hxq2 (y := ⟨y, hpq1 y.2⟩) hxy).trans (hpq2 rfl).symm

Premises used: Eq.symm, Eq.trans
-- 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) ⋯)
⊢ ∀ (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

Tactic:
have f_eq : ∀ (p : c) (x : ↥(sSup (domain '' c))) (y : p.1.1) (_hxy : (x : E) = y),
      f x = p.1 y := by
    intro p x y hxy
    rcases hc (P x).1.1 (P x).1.2 p.1 p.2 with ⟨q, _hqc, ⟨hxq1, hxq2⟩, ⟨hpq1, hpq2⟩⟩
    exact (hxq2 (y := ⟨y, hpq1 y.2⟩) hxy).trans (hpq2 rfl).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
w : ∀ (x y : ↥(sSup (domain '' c))), f (x + y) = f x + f y
w₁ :
  ∀ (m : R) (x : ↥(sSup (domain '' c))),
    f (m • x) = HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) m : S) (f x)
h :
  { domain := sSup (domain '' c),
      toFun :=
        { toFun := f, map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F } } ∈
    upperBounds c
⊢ ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
    { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c

Tactic:
use { toFun := f, map_add' := ?_, map_smul' := ?_ }, ?_
-- 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
x y : ↥(sSup (domain '' c))
w :
  ∀ (p : E →ₛₗ.[σ] F) (hpc : p ∈ c) (hpx : (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) ≤ p)
    (hpy : (↑(↑(P y) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) ≤ p), f (x + y) = f x + f y
⊢ f (x + y) = f x + f y

Tactic:
rcases hc (P x).1.1 (P x).1.2 (P y).1.1 (P y).1.2 with ⟨p, hpc, hpx, hpy⟩

Premises used: Subtype.val, Subtype.property