awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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)
⊢ ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
    { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c
have 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
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
have 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
Tactic: rcases hc (P x).1.1 (P x).1.2 p.1 p.2 with ⟨q, _hqc, ⟨hxq1, hxq2⟩, ⟨hpq1, hpq2⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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 : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
    { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c
have 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
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
    { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c
have w : ∀ (x y : ↥(sSup (domain '' c))), f (x + y) = f x + f y
Tactic: use { toFun := f, map_add' := ?_, map_smul' := ?_ }, ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
    { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c
have 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)
Tactic: use { toFun := f, map_add' := ?_, map_smul' := ?_ }, ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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)
⊢ ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
    { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c
have h : { domain := sSup (domain '' c),
    toFun :=
      { toFun := f, map_add' := sorry, map_smul' := sorry : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F } } ∈
  upperBounds c
Tactic: use { toFun := f, map_add' := ?_, map_smul' := ?_ }, ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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))
⊢ f (x + y) = f x + f y
have 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
Tactic: rcases hc (P x).1.1 (P x).1.2 (P y).1.1 (P y).1.2 with ⟨p, hpc, hpx, hpy⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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))
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
x' : ↥p.domain :=
  (inclusion ⋯ : (a : ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) → ↥p.domain)
    (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E) ⋯)
y' : ↥p.domain :=
  (inclusion ⋯ : (a : ↥(↑(↑(P y) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) → ↥p.domain)
    (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑(↑(P y) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑y : E) ⋯)
⊢ f (x + y) = f x + f y
have w : f (x + y) =
  (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
      x' +
    f y
Tactic: rw [f_eq ⟨p, hpc⟩ x x' rfl, f_eq ⟨p, hpc⟩ y y' rfl, f_eq ⟨p, hpc⟩ (x + y) (x' + y') rfl,
      map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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))
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
x' : ↥p.domain :=
  (inclusion ⋯ : (a : ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) → ↥p.domain)
    (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E) ⋯)
y' : ↥p.domain :=
  (inclusion ⋯ : (a : ↥(↑(↑(P y) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) → ↥p.domain)
    (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑(↑(P y) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑y : E) ⋯)
w :
  f (x + y) =
    (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
        x' +
      f y
⊢ f (x + y) = f x + f y
have w₁ : f (x + y) =
  (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
      x' +
    (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
      y'
Tactic: rw [f_eq ⟨p, hpc⟩ x x' rfl, f_eq ⟨p, hpc⟩ y y' rfl, f_eq ⟨p, hpc⟩ (x + y) (x' + y') rfl,
      map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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))
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
x' : ↥p.domain :=
  (inclusion ⋯ : (a : ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) → ↥p.domain)
    (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E) ⋯)
y' : ↥p.domain :=
  (inclusion ⋯ : (a : ↥(↑(↑(P y) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) → ↥p.domain)
    (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑(↑(P y) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑y : E) ⋯)
w :
  f (x + y) =
    (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
        x' +
      f y
w₁ :
  f (x + y) =
    (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
        x' +
      (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) :
          ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
        y'
⊢ f (x + y) = f x + f y
have w₂ : (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
    (x' + y') =
  (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
      x' +
    (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
      y'
Tactic: rw [f_eq ⟨p, hpc⟩ x x' rfl, f_eq ⟨p, hpc⟩ y y' rfl, f_eq ⟨p, hpc⟩ (x + y) (x' + y') rfl,
      map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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))
⊢ f (c • x) = HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) (f x)
have 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)
        sorry) =
  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ₛₗ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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)
⊢ f (c • x) = HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) (f x)
have 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)
        sorry) =
  (↑(↑(↑(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) sorry)
Tactic: rw [f_eq (P x).1 (c • x) (c • ⟨x, (P x).2⟩) rfl, ← map_smulₛₗ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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 } }
have 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' := sorry, map_smul' := sorry : 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' := sorry, map_smul' := sorry :
                LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F } :
            E →ₛₗ.[σ] F } :
        ↥{ domain := sSup (domain '' c), toFun := { toFun := f, map_add' := sorry, map_smul' := sorry } }.domain → F)
      y =
    (↑p : ↥p.domain → F) x
Tactic: refine ⟨le_sSup <| Set.mem_image_of_mem domain hpc, fun x y hxy => Eq.symm ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ x ∈ (LinearPMap.sSup c hc).domain ↔ ∃ f ∈ c, x ∈ f.domain
have rw : (∃ y ∈ domain '' c, x ∈ y) ↔ ∃ f ∈ c, x ∈ f.domain
Tactic: rw [domain_sSup, Submodule.mem_sSup_of_directed (hnonempty.image _)
    (DirectedOn.mono_comp LinearPMap.domain_mono.monotone hc)]