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
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
⊢ (↑(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)
have 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₂
Tactic: simp only [coe_add, ← add_assoc]
-- 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
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
⊢ 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₂
have 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₂
Tactic: rw [add_right_comm (x _), hxy, add_assoc, hxy, coe_mk, coe_mk]
-- 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
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₂
⊢ 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₂
have 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₂
Tactic: rw [add_right_comm (x _), hxy, add_assoc, hxy, coe_mk, coe_mk]
-- 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
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₂
⊢ 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₂
have 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₂
Tactic: rw [add_right_comm (x _), hxy, add_assoc, hxy, coe_mk, coe_mk]
-- 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
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₂
⊢ 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₂
have 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₂
Tactic: rw [add_right_comm (x _), hxy, add_assoc, hxy, coe_mk, coe_mk]
-- 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
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₂
⊢ 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₂
have w₄ : z₁ + (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂) : E) = z₁ + z₂
Tactic: rw [add_right_comm (x _), hxy, add_assoc, hxy, coe_mk, coe_mk]
-- 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
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₂
⊢ 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₂
have w₅ : z₁ + z₂ = z₁ + z₂
Tactic: rw [add_right_comm (x _), hxy, add_assoc, hxy, coe_mk, coe_mk]
-- 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
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)
⊢ fg (c • z) = HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) (fg z)
have w : fg (c • z) =
  (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) sorry) +
    (↑g : ↥g.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) sorry)
Tactic: rw [smul_add, ← map_smulₛₗ, ← 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
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)
⊢ 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) ⋯)
have w : (↑(c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) sorry) : E) +
    (↑(c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) sorry) : E) =
  (↑(c • z) : E)
Tactic: apply fg_eq
-- 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
f g : E →ₛₗ.[σ] F
h : Disjoint f.domain g.domain
x : ↥f.domain
y : ↥g.domain
hxy : (↑x : E) = (↑y : E)
⊢ (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
have 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
Tactic: rw [disjoint_def] at h
Cleared hypotheses: h, x, y, hxy
-- 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
f g : E →ₛₗ.[σ] F
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
have hy : y = 0
Tactic: have hy : y = 0 := Subtype.ext (h y (hxy ▸ x.2) y.2)
-- 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
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
⊢ (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
have hx : x = 0
Tactic: have hx : x = 0 := Subtype.ext (hxy.trans <| congr_arg _ hy)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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 : E →ₛₗ.[σ] F
⊢ - -f = f
have h : ∀ (x : E), x ∈ (- -f).domain ↔ x ∈ f.domain
Tactic: ext x y hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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 : E →ₛₗ.[σ] F
h : ∀ (x : E), x ∈ (- -f).domain ↔ x ∈ f.domain
⊢ - -f = f
have h' : ∀ ⦃x : E⦄ ⦃y : x ∈ (- -f).domain⦄ ⦃hxy : x ∈ f.domain⦄,
  (↑(- -f) : ↥(- -f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (- -f).domain) x y) =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hxy)
Tactic: ext x y hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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 h : E →ₛₗ.[σ] F
⊢ f + g + h = f + (g + h)
have h₁ : ∀ (x : E), x ∈ (f + g + h).domain ↔ x ∈ (f + (g + h)).domain
Tactic: ext x y hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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 h : E →ₛₗ.[σ] F
h₁ : ∀ (x : E), x ∈ (f + g + h).domain ↔ x ∈ (f + (g + h)).domain
⊢ f + g + h = f + (g + h)
have h' : ∀ ⦃x : E⦄ ⦃y : x ∈ (f + g + h).domain⦄ ⦃hxy : x ∈ (f + (g + h)).domain⦄,
  (↑(f + g + h) : ↥(f + g + h).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g + h).domain) x y) =
    (↑(f + (g + h)) : ↥(f + (g + h)).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + (g + h)).domain) x hxy)
Tactic: ext x y hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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 : E →ₛₗ.[σ] F
⊢ 0 + f = f
have h : ∀ (x : E), x ∈ (0 + f).domain ↔ x ∈ f.domain
Tactic: ext x y hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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 : E →ₛₗ.[σ] F
h : ∀ (x : E), x ∈ (0 + f).domain ↔ x ∈ f.domain
⊢ 0 + f = f
have h' : ∀ ⦃x : E⦄ ⦃y : x ∈ (0 + f).domain⦄ ⦃hxy : x ∈ f.domain⦄,
  (↑(0 + f) : ↥(0 + f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (0 + f).domain) x y) =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hxy)
Tactic: ext x y hxy