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
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
c : R
x : E
h :
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain),
        (↑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)}
    x
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
this :
  ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain),
    Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯ = c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx
rw :
  (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) ⋯)
rw₁ :
  (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
rw₂ :
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
      ((↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx)) =
    (↑g : ↥g.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
rw₃ :
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
      ((↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx)) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
      ((↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx))
⊢ (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) ⋯)
have rw₄ : HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
    ((↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)) =
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
    ((↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx))
Tactic: rw [this hfx, this hgx, f.map_smulₛₗ, g.map_smulₛₗ, hx]
-- 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 → f ≤ h → f ≤ { domain := g.eqLocus h, toFun := g.toFun ∘ₛₗ inclusion ⋯ }
have this : ∀ (fg_le : f.domain ≤ g.domain)
  (fg_eq :
    ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y),
  f ≤ h → f ≤ { domain := g.eqLocus h, toFun := g.toFun ∘ₛₗ inclusion sorry }
Tactic: ⟨fg_le, fg_eq⟩
-- 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
fg_le : f.domain ≤ g.domain
fg_eq : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
⊢ f ≤ h → f ≤ { domain := g.eqLocus h, toFun := g.toFun ∘ₛₗ inclusion ⋯ }
have this : ∀ (fh_le : f.domain ≤ h.domain)
  (fh_eq :
    ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥h.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑h : ↥h.domain → F) y),
  f ≤ { domain := g.eqLocus h, toFun := g.toFun ∘ₛₗ inclusion sorry }
Tactic: ⟨fh_le, fh_eq⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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
x : ↥(domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) ⊥)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
⊢ (↑⊥ : ↥⊥.domain → F) x = (↑f : ↥f.domain → F) y
have hx : x = 0
Tactic: have hx : x = 0 := Subtype.ext ((mem_bot R).1 x.2)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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
x : ↥(domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) ⊥)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
hx : x = 0
⊢ (↑⊥ : ↥⊥.domain → F) x = (↑f : ↥f.domain → F) y
have hy : y = 0
Tactic: have hy : y = 0 := Subtype.ext (h.symm.trans (congr_arg _ hx))
-- 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
x : ↥(domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) ⊥)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
hx : x = 0
hy : y = 0
⊢ (↑⊥ : ↥⊥.domain → F) x = (↑f : ↥f.domain → F) y
have rw : (↑⊥ : ↥⊥.domain → F) 0 = (↑f : ↥f.domain → F) y
Tactic: rw [hx, hy, map_zero, map_zero]
-- 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
x : ↥(domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) ⊥)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
hx : x = 0
hy : y = 0
rw : (↑⊥ : ↥⊥.domain → F) 0 = (↑f : ↥f.domain → F) y
⊢ (↑⊥ : ↥⊥.domain → F) x = (↑f : ↥f.domain → F) y
have rw₁ : (↑⊥ : ↥⊥.domain → F) 0 = (↑f : ↥f.domain → F) 0
Tactic: rw [hx, hy, map_zero, map_zero]
-- 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
x : ↥(domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) ⊥)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
hx : x = 0
hy : y = 0
rw : (↑⊥ : ↥⊥.domain → F) 0 = (↑f : ↥f.domain → F) y
rw₁ : (↑⊥ : ↥⊥.domain → F) 0 = (↑f : ↥f.domain → F) 0
⊢ (↑⊥ : ↥⊥.domain → F) x = (↑f : ↥f.domain → F) y
have rw₂ : 0 = (↑f : ↥f.domain → F) 0
Tactic: rw [hx, hy, map_zero, map_zero]
-- 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
x : ↥(domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) ⊥)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
hx : x = 0
hy : y = 0
rw : (↑⊥ : ↥⊥.domain → F) 0 = (↑f : ↥f.domain → F) y
rw₁ : (↑⊥ : ↥⊥.domain → F) 0 = (↑f : ↥f.domain → F) 0
rw₂ : 0 = (↑f : ↥f.domain → F) 0
⊢ (↑⊥ : ↥⊥.domain → F) x = (↑f : ↥f.domain → F) y
have rw₃ : Eq.{u_5 + 1} (α := F) 0 0
Tactic: rw [hx, hy, map_zero, map_zero]
-- 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
⊢ ∃ (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
have choose : ∀ (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 : 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: choose x hx y hy hxy using fun z : ↥(f.domain ⊔ g.domain) => mem_sup.1 z.prop
-- 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) ⋯)
x' : ↥f.domain
y' : ↥g.domain
z' : ↥(f.domain ⊔ g.domain)
H : (↑x' : E) + (↑y' : E) = (↑z' : E)
⊢ (↑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') ⋯) =
    (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'
have rw : (↑f : ↥f.domain → F) (x' - Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z') sorry) =
  (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z') sorry - y')
Tactic: rw [add_comm, ← sub_eq_sub_iff_add_eq_add, eq_comm, ← map_sub, ← map_sub]
-- 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) ⋯)
x' : ↥f.domain
y' : ↥g.domain
z' : ↥(f.domain ⊔ g.domain)
H : (↑x' : E) + (↑y' : E) = (↑z' : E)
⊢ (↑f : ↥f.domain → F) (x' - 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') ⋯ - y')
have a : (↑(x' - Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z') sorry) : E) =
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z') sorry - y') : E)
Tactic: apply h
-- 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) (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)
⊢ (↑(x' - Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z') ⋯) : E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z') ⋯ - y') : E)
have hxy₁ : ∀ (z : ↥(f.domain ⊔ g.domain)), x z = (↑z : E) - y z
Tactic: simp only [← eq_sub_iff_add_eq] at hxy
Cleared hypotheses: hxy
-- 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
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
⊢ (↑(x' - Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z') ⋯) : E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z') ⋯ - y') : E)
have a : -(↑y' : E) + y z' = y z' - (↑y' : E)
Tactic: simp only [AddSubgroupClass.coe_sub, hxy, ← sub_add, ← sub_sub, sub_self,
      zero_sub, ← H]
-- 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) (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 : 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
have 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'
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
-- 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'
⊢ ∃ (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
have w : ∀ (x y : ↥(f.domain ⊔ g.domain)), fg (x + y) = fg x + fg y
Tactic: use { toFun := fg, map_add' := ?_, map_smul' := ?_ }, 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 : ∀ (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
⊢ ∃ (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
have 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)
Tactic: use { toFun := fg, map_add' := ?_, map_smul' := ?_ }, 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 : ∀ (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
⊢ 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₂)
have 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₁))
          sorry +
        Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain)
          (x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) sorry) +
    (↑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₁))
          sorry +
        Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain)
          (y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) sorry)
Tactic: rw [← add_assoc, add_right_comm (f _), ← map_add, add_assoc, ← 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
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
⊢ 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₂)) ⋯)
have w : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁)) sorry +
          Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain)
            (x (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) sorry) :
      E) +
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₁ hz₁))
            sorry +
          Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain)
            (y (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain ⊔ g.domain) z₂ hz₂)) sorry) :
      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: apply fg_eq