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_dom : Submodule R E
f g : LinearMap.{u_1, u_2, u_4, u_5} σ (↥f_dom) F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain⦄
    ⦃hg : x ∈ { domain := f_dom, toFun := g : E →ₛₗ.[σ] F }.domain⦄,
    (↑{ domain := f_dom, toFun := f : E →ₛₗ.[σ] F } : ↥{ domain := f_dom, toFun := f }.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain) x hf) =
      (↑{ domain := f_dom, toFun := g : E →ₛₗ.[σ] F } : ↥{ domain := f_dom, toFun := g }.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := f_dom, toFun := g : E →ₛₗ.[σ] F }.domain) x hg)
x : ↥f_dom
⊢ Eq.{u_5 + 1} (α := F) ((f : (a : ↥f_dom) → F) x : F) ((g : (a : ↥f_dom) → F) x : F)

Tactic:
apply h'
-- 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 : f.domain = g.domain
h' : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
⊢ f = g

Tactic:
ext h fun _ _ _ ↦ h' rfl

Premises used: LinearPMap.ext, 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 : E →ₛₗ.[σ] F
⊢ (↑f : ↥f.domain → F) 0 = 0

Tactic:
f.toFun.map_zero

Premises used: LinearMap.map_zero, LinearPMap.toFun, 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 : E →ₛₗ.[σ] F
⊢ f.domain = f.domain ∧
    ∀ ⦃x : E⦄ ⦃hf hg : x ∈ f.domain⦄,
      (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) =
        (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hg)

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
f g : E →ₛₗ.[σ] F
EQ : f = g
x y : ↥f.domain
h : (↑x : E) = (↑y : E)
e_a : x = y
⊢ (↑f : ↥f.domain → F) x = (↑f : ↥f.domain → F) y

Tactic:
congr
-- 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
EQ : f = g
x y : ↥f.domain
h : (↑x : E) = (↑y : E)
⊢ x = y

Tactic:
mod_cast h

Premises used: cast, SetLike.coe_eq_coe._simp_1
-- 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
EQ : f = g
x y : ↥f.domain
h : (↑x : E) = (↑y : E)
⊢ x = y

Tactic:
exact mod_cast h
-- 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
s : Submodule R E
f g : LinearMap.{u_1, u_2, u_4, u_5} σ (↥s) F
h : f = g
⊢ { domain := s, toFun := f : E →ₛₗ.[σ] F } = { domain := s, toFun := g }

Tactic:
h ▸ rfl

Premises used: Eq.rec, 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 : E →ₛₗ.[σ] F
x y : ↥f.domain
⊢ (↑f : ↥f.domain → F) (x + y) = (↑f : ↥f.domain → F) x + (↑f : ↥f.domain → F) y

Tactic:
f.toFun.map_add x y

Premises used: LinearMap.map_add, LinearPMap.toFun, 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 : E →ₛₗ.[σ] F
x : ↥f.domain
⊢ (↑f : ↥f.domain → F) (-x) = -(↑f : ↥f.domain → F) x

Tactic:
f.toFun.map_neg x

Premises used: LinearMap.map_neg, LinearPMap.toFun, 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 : E →ₛₗ.[σ] F
x y : ↥f.domain
⊢ (↑f : ↥f.domain → F) (x - y) = (↑f : ↥f.domain → F) x - (↑f : ↥f.domain → F) y

Tactic:
f.toFun.map_sub x y

Premises used: LinearPMap.toFun, LinearMap.map_sub, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
c : R
x : ↥f.domain
⊢ (↑f : ↥f.domain → F) (c • x) = c • (↑f : ↥f.domain → F) x

Tactic:
f.toFun.map_smulₛₗ c x

Premises used: LinearPMap.toFun, LinearMap.map_smulₛₗ, 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 : E →ₛₗ.[σ] F
c : R
x : ↥f.domain
⊢ (↑f : ↥f.domain → F) (c • x) = HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) ((↑f : ↥f.domain → F) x)

Tactic:
f.toFun.map_smulₛₗ c x

Premises used: LinearPMap.toFun, LinearMap.map_smulₛₗ, 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
p : Submodule R E
f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥p) F
x : ↥p
⊢ (↑{ domain := p, toFun := f : E →ₛₗ.[σ] F } : ↥{ domain := p, toFun := f }.domain → F) x = (f : (a : ↥p) → F) x

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c₁ c₂ : R
h : c₁ • x = c₂ • x
rw :
  ∀ (h : (c₁ - c₂) • x = 0), HSub.hSub (α := S) (β := S) ((σ : (a : R) → S) c₁ : S) ((σ : (a : R) → S) c₂ : S) • y = 0
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y

Tactic:
rw [← sub_eq_zero, ← sub_smul] at h ⊢

Premises used: sub_eq_zero, sub_smul
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c₁ c₂ : R
h : (c₁ - c₂) • x = 0
rw : HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) (c₁ - c₂) : S) y = 0
⊢ HSub.hSub (α := S) (β := S) ((σ : (a : R) → S) c₁ : S) ((σ : (a : R) → S) c₂ : S) • y = 0

Tactic:
rw [← RingHom.map_sub]

Premises used: RingHom.map_sub
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c₁ c₂ : R
h : (c₁ - c₂) • x = 0
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) (c₁ - c₂) : S) y = 0

Tactic:
H _ h
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c₁ c₂ : R
h : (c₁ - c₂) • x = 0
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) (c₁ - c₂) : S) y = 0

Tactic:
exact H _ h
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
x : E
y : F
H_1 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
H :
  ∀ (c₁ c₂ : R),
    c₁ • x = c₂ • x →
      HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
        HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y
y' z' : ↥(R ∙ x)
a :
  Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(y' + z') : E)) ⋯ • x =
    (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑y' : E)) ⋯ +
        Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z' : E)) ⋯) •
      x
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S)
      ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(y' + z') : E)) ⋯) : S) y =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S)
        ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑y' : E)) ⋯) : S) y +
      HSMul.hSMul.{u_2, u_5, u_5} (α := S)
        ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z' : E)) ⋯) : S) y

Tactic:
rw [← add_smul, ← RingHom.map_add, H]

Premises used: add_smul, RingHom.map_add
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
x : E
y : F
H_1 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
H :
  ∀ (c₁ c₂ : R),
    c₁ • x = c₂ • x →
      HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
        HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y
y' z' : ↥(R ∙ x)
⊢ ∀ (w : ↥(R ∙ x)), Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑w : E)) ⋯ • x = (↑w : E)

Tactic:
have (w : R ∙ x) := Classical.choose_spec (mem_span_singleton.1 w.prop)
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
x : E
y : F
H_1 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
H :
  ∀ (c₁ c₂ : R),
    c₁ • x = c₂ • x →
      HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
        HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y
y' z' : ↥(R ∙ x)
this : ∀ (w : ↥(R ∙ x)), Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑w : E)) ⋯ • x = (↑w : E)
⊢ Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(y' + z') : E)) ⋯ • x =
    (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑y' : E)) ⋯ +
        Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z' : E)) ⋯) •
      x

Tactic:
simp only [add_smul, this, ← coe_add]

Premises used: Submodule.coe_add, add_smul
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
x : E
y : F
H_1 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
H :
  ∀ (c₁ c₂ : R),
    c₁ • x = c₂ • x →
      HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
        HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y
c : R
z : ↥(R ∙ x)
a :
  Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(c • z) : E)) ⋯ • x =
    (c * Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z : E)) ⋯) • x
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S)
      ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(c • z) : E)) ⋯) : S) y =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
      (HSMul.hSMul.{u_2, u_5, u_5} (α := S)
        ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z : E)) ⋯) : S) y)

Tactic:
rw [smul_smul, ← RingHom.map_mul, H]

Premises used: smul_smul, RingHom.map_mul
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
x : E
y : F
H_1 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
H :
  ∀ (c₁ c₂ : R),
    c₁ • x = c₂ • x →
      HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
        HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y
c : R
z : ↥(R ∙ x)
⊢ ∀ (w : ↥(R ∙ x)), Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑w : E)) ⋯ • x = (↑w : E)

Tactic:
have (w : R ∙ x) := Classical.choose_spec (mem_span_singleton.1 w.prop)
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
x : E
y : F
H_1 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
H :
  ∀ (c₁ c₂ : R),
    c₁ • x = c₂ • x →
      HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
        HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y
c : R
z : ↥(R ∙ x)
this : ∀ (w : ↥(R ∙ x)), Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑w : E)) ⋯ • x = (↑w : E)
a : (↑(c • z) : E) = c • (↑z : E)
⊢ Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(c • z) : E)) ⋯ • x =
    (c * Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z : E)) ⋯) • x

Tactic:
simp only [mul_smul, this]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
x : E
y : F
H_1 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
H :
  ∀ (c₁ c₂ : R),
    c₁ • x = c₂ • x →
      HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
        HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y
c : R
z : ↥(R ∙ x)
this : ∀ (w : ↥(R ∙ x)), Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑w : E)) ⋯ • x = (↑w : E)
⊢ (↑(c • z) : E) = c • (↑z : E)

Tactic:
apply coe_smul

Premises used: Submodule.coe_smul
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
⊢ (mkSpanSingleton' x y H).domain = R ∙ x

Tactic:
rfl

Premises used: Submodule.span, 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 : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
dsimp :
  HSMul.hSMul.{u_2, u_5, u_5} (α := S)
      ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) ⋯) : S) y =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y
⊢ (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) (c • x) h) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y

Tactic:
dsimp [mkSpanSingleton']

Premises used: LinearPMap.mkSpanSingleton'
-- 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 : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
rw :
  HSMul.hSMul.{u_2, u_5, u_5} (α := S)
      ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) ⋯ - c) : S) y =
    0
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S)
      ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) ⋯) : S) y =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y

Tactic:
rw [← sub_eq_zero, ← sub_smul, ← RingHom.map_sub]

Premises used: sub_eq_zero, sub_smul, RingHom.map_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
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
a : (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) ⋯ - c) • x = 0
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S)
      ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) ⋯ - c) : S) y =
    0

Tactic:
apply H
-- 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 : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
a : Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) ⋯ • x = c • x
⊢ (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) ⋯ - c) • x = 0

Tactic:
simp only [sub_smul, sub_eq_zero]

Premises used: sub_eq_zero, sub_smul
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) ⋯ • x = c • x

Tactic:
apply Classical.choose_spec (mem_span_singleton.1 h)

Premises used: Submodule.mem_span_singleton, Classical.choose_spec, Iff.mp
-- 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 : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
rw : HSMul.hSMul.{u_2, u_5, u_5} (α := S) 1 y
| y

Tactic:
rw [← one_smul S y]

Premises used: one_smul
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
conv_rhs :
  (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) x h) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) 1 y
⊢ (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) x h) =
    y

Tactic:
conv_rhs => rw [← one_smul S y]

Premises used: one_smul
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
rw :
  (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) x h) =
    (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain)
        (HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 x) ⋯)
rw₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 x ∈ (mkSpanSingleton' x y H).domain
⊢ (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) x h) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) 1 y

Tactic:
rw [← RingHom.map_one, ← mkSpanSingleton'_apply x y H 1 ?_]

Premises used: RingHom.map_one, LinearPMap.mkSpanSingleton'_apply, OfNat.ofNat
-- 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 : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
e_a : x = HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 x
⊢ (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) x h) =
    (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain)
        (HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 x) ⋯)

Tactic:
congr
-- 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 : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
e_a e_a₁ : x = x
⊢ x = HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 x

Tactic:
rw [one_smul]

Premises used: one_smul