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
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
x' : ↥f.domain
y' : ↥g.domain
z' : ↥(f.domain ⊔ g.domain)
H : (↑x' : E) + (↑y' : E) = (↑z' : E)
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z = (↑z : E) - y z
⊢ -(↑y' : E) + y z' = y z' - (↑y' : E)

Tactic:
apply neg_add_eq_sub

Premises used: neg_add_eq_sub
-- 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 g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
⊢ ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)) (_H : (↑x' : E) + (↑y' : E) = (↑z' : E)),
    fg z' = (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'

Tactic:
have fg_eq : ∀ (x' : f.domain) (y' : g.domain) (z' : ↥(f.domain ⊔ g.domain))
      (_H : (x' : E) + y' = z'), fg z' = f x' + g y' := by
    intro x' y' z' H
    dsimp [fg]
    rw [add_comm, ← sub_eq_sub_iff_add_eq_add, eq_comm, ← map_sub, ← map_sub]
    apply h
    simp only [← eq_sub_iff_add_eq] at hxy
    simp only [AddSubgroupClass.coe_sub, hxy, ← sub_add, ← sub_sub, sub_self,
      zero_sub, ← H]
    apply neg_add_eq_sub
-- 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 g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
fg_eq :
  ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)) (_H : (↑x' : E) + (↑y' : E) = (↑z' : E)),
    fg z' = (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'
w : ∀ (x y : ↥(f.domain ⊔ g.domain)), fg (x + y) = fg x + fg y
w₁ :
  ∀ (m : R) (x : ↥(f.domain ⊔ g.domain)),
    fg (m • x) = HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) m : S) (fg x)
⊢ ∃ (fg : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(f.domain ⊔ g.domain)) F),
    ∀ (x : ↥f.domain) (y : ↥g.domain) (z : ↥(f.domain ⊔ g.domain)),
      (↑x : E) + (↑y : E) = (↑z : E) →
        (fg : (a : ↥(f.domain ⊔ g.domain)) → F) z = (↑f : ↥f.domain → F) x + (↑g : ↥g.domain → F) y

Tactic:
use { toFun := fg, map_add' := ?_, map_smul' := ?_ }, fg_eq
-- 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 g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
fg_eq :
  ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)) (_H : (↑x' : E) + (↑y' : E) = (↑z' : E)),
    fg z' = (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
w :
  fg
      (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁ +
        Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) =
    (↑f : ↥f.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain)
            (x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁)) ⋯ +
          Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain)
            (x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) ⋯) +
      (↑g : ↥g.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain)
            (y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁)) ⋯ +
          Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain)
            (y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) ⋯)
⊢ fg
      (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁ +
        Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) =
    fg (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁) +
      fg (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)

Tactic:
rw [← add_assoc, add_right_comm (f _), ← map_add, add_assoc, ← map_add]

Premises used: add_assoc, add_right_comm, LinearPMap.map_add, 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 g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
fg_eq :
  ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)) (_H : (↑x' : E) + (↑y' : E) = (↑z' : E)),
    fg z' = (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
w :
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁))
              ⋯ +
            Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain)
              (x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) ⋯) :
        E) +
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain)
              (y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁)) ⋯ +
            Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain)
              (y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) ⋯) :
        E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁ +
          Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) :
      E)
⊢ fg
      (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁ +
        Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) =
    (↑f : ↥f.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain)
            (x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁)) ⋯ +
          Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain)
            (x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) ⋯) +
      (↑g : ↥g.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain)
            (y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁)) ⋯ +
          Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain)
            (y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) ⋯)

Tactic:
apply fg_eq
-- 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 g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
fg_eq :
  ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)) (_H : (↑x' : E) + (↑y' : E) = (↑z' : E)),
    fg z' = (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
w :
  x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁) +
          x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) +
        y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁) +
      y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) =
    z₁ + z₂
⊢ (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁))
              ⋯ +
            Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain)
              (x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) ⋯) :
        E) +
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain)
              (y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁)) ⋯ +
            Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain)
              (y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) ⋯) :
        E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁ +
          Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) :
      E)

Tactic:
simp only [coe_add, ← add_assoc]

Premises used: Submodule.coe_add, add_assoc
-- 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 g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
fg_eq :
  ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)) (_H : (↑x' : E) + (↑y' : E) = (↑z' : E)),
    fg z' = (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
w :
  x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁) +
          y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁) +
        x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) +
      y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) =
    z₁ + z₂
w₁ :
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁) : E) +
        x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) +
      y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) =
    z₁ + z₂
w₂ :
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁) : E) +
      (x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) +
        y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) =
    z₁ + z₂
w₃ :
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁) : E) +
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) : E) =
    z₁ + z₂
w₄ : z₁ + (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) : E) = z₁ + z₂
w₅ w₆ : z₁ + z₂ = z₁ + z₂
⊢ x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁) +
          x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) +
        y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁) +
      y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) =
    z₁ + z₂

Tactic:
rw [add_right_comm (x _), hxy, add_assoc, hxy, coe_mk, coe_mk]

Premises used: add_assoc, Submodule.coe_mk, add_right_comm
-- 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 g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
fg_eq :
  ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)) (_H : (↑x' : E) + (↑y' : E) = (↑z' : E)),
    fg z' = (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'
c : R
z : ↥(f.domain ⊔ g.domain)
w :
  fg (c • z) =
    (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
⊢ fg (c • z) = HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) (fg z)

Tactic:
rw [smul_add, ← map_smulₛₗ, ← map_smulₛₗ]

Premises used: LinearPMap.map_smulₛₗ, smul_add
-- 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 g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
fg_eq :
  ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)) (_H : (↑x' : E) + (↑y' : E) = (↑z' : E)),
    fg z' = (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'
c : R
z : ↥(f.domain ⊔ g.domain)
w :
  (↑(c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) : E) +
      (↑(c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯) : E) =
    (↑(c • z) : E)
⊢ fg (c • z) =
    (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)

Tactic:
apply fg_eq
-- 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 g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
fg_eq :
  ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)) (_H : (↑x' : E) + (↑y' : E) = (↑z' : E)),
    fg z' = (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'
c : R
z : ↥(f.domain ⊔ g.domain)
⊢ (↑(c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) : E) +
      (↑(c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯) : E) =
    (↑(c • z) : E)

Tactic:
simp only [coe_smul, ← smul_add, hxy]

Premises used: Submodule.coe_smul, smul_add
-- 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 g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
⊢ (f.sup g h).domain = f.domain ⊔ g.domain

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
f g : E →ₛₗ.[σ] F
H : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : ↥f.domain
y : ↥g.domain
z : ↥(f.domain ⊔ g.domain)
hz : (↑x : E) + (↑y : E) = (↑z : E)
⊢ (↑(f.sup g H) : ↥(f.sup g H).domain → F) sorry = (↑f : ↥f.domain → F) x + (↑g : ↥g.domain → F) y

Tactic:
Classical.choose_spec (sup_aux f g H) x y z hz

Premises used: Classical.choose_spec, _private.0.LinearPMap.sup_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
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
⊢ f ≤ f.sup g h

Tactic:
⟨le_sup_left, fun z₁ z₂ hz => ?_⟩

Premises used: And.intro
-- 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 g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
⊢ g ≤ f.sup g h

Tactic:
⟨le_sup_right, fun z₁ z₂ hz => ?_⟩

Premises used: And.intro
-- 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 g h : E →ₛₗ.[σ] F
H : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
fh : f ≤ h
gh : g ≤ h
⊢ f.sup g H ≤ h

Tactic:
have Hf : f ≤ f.sup g H ⊓ h := le_inf (f.left_le_sup g H) fh
  have Hg : g ≤ f.sup g H ⊓ h := le_inf (f.right_le_sup g H) gh
  le_of_eqLocus_ge <| sup_le Hf.1 Hg.1

Premises used: LinearPMap.left_le_sup, Unit.unit, sorryAx, Lean.Name.num, le_inf, Lean.Name.str, Lean.Name.anonymous, Bool.true, LinearPMap.right_le_sup, Function.const, Lean.Name, OfNat.ofNat, 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
f g : E →ₛₗ.[σ] F
h : Disjoint f.domain g.domain
x : ↥f.domain
y : ↥g.domain
hxy : (↑x : E) = (↑y : E)
rw :
  ∀ (h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0) (x : ↥f.domain) (y : ↥g.domain) (hxy : (↑x : E) = (↑y : E)),
    (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
⊢ (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y

Tactic:
rw [disjoint_def] at h

Premises used: Submodule.disjoint_def
-- 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 g : E →ₛₗ.[σ] F
h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0
x : ↥f.domain
y : ↥g.domain
hxy : (↑x : E) = (↑y : E)
⊢ y = 0

Tactic:
have hy : y = 0 := Subtype.ext (h y (hxy ▸ x.2) y.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
f g : E →ₛₗ.[σ] F
h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0
x : ↥f.domain
y : ↥g.domain
hxy : (↑x : E) = (↑y : E)
hy : y = 0
⊢ x = 0

Tactic:
have hx : x = 0 := Subtype.ext (hxy.trans <| congr_arg _ hy)
-- 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 g : E →ₛₗ.[σ] F
h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0
x : ↥f.domain
y : ↥g.domain
hxy : (↑x : E) = (↑y : E)
hy : y = 0
hx : x = 0
⊢ (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y

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
⊢ Eq.{u_4 + 1} (α := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) ⊤

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
x : ↥⊤
⊢ Eq.{u_5 + 1} (α := F) ((↑0 : ↥(domain 0) → F) x) 0

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
M : Type u_7
inst_6 : Monoid M
inst_7 : DistribMulAction M F
inst_8 : SMulCommClass S M F
a : M
f : E →ₛₗ.[σ] F
⊢ (a • f).domain = f.domain

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
M : Type u_7
inst_6 : Monoid M
inst_7 : DistribMulAction M F
inst_8 : SMulCommClass S M F
a : M
f : E →ₛₗ.[σ] F
x : ↥(a • f).domain
⊢ (↑(a • f) : ↥(a • f).domain → F) x = a • (↑f : ↥f.domain → F) x

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'