awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x : n → R
⊢ LE.le.{u_4} (α := R) (0 : R)
    ((((B : (a : M) → M →ₗ[R] R) ((b.equivFun.symm : (a : n → R) → M) x) : M →ₗ[R] R) : (a : M) → R)
        ((b.equivFun.symm : (a : n → R) → M) x : M) :
      R)

Tactic:
exact h _
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
x : M
refine_2 :
  LE.le.{u_4} (α := R) 0
    (dotProduct.{u_4, u_3} (m := n) (star (⇑((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R))
      (Matrix.mulVec (n := n) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B)
        (⇑((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R)))
⊢ LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
rw [apply_eq_star_dotProduct_toMatrix₂_mulVec b]

Premises used: apply_eq_star_dotProduct_toMatrix₂_mulVec
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
x : M
⊢ LE.le.{u_4} (α := R) 0
    (dotProduct.{u_4, u_3} (m := n) (star (⇑((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R))
      (Matrix.mulVec (n := n) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B)
        (⇑((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R)))

Tactic:
h _
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
x : M
⊢ LE.le.{u_4} (α := R) 0
    (dotProduct.{u_4, u_3} (m := n) (star (⇑((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R))
      (Matrix.mulVec (n := n) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B)
        (⇑((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R)))

Tactic:
exact h _
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
M : Type u_4
inst : AddCommMonoid M
s : Set M
⊢ Eq (α := Submodule ℕ M)
    ((AddSubmonoid.toNatSubmodule : (a : AddSubmonoid M) → Submodule ℕ M) (AddSubmonoid.closure s) : Submodule ℕ M)
    (span ℕ s : Submodule ℕ M)

Tactic:
(Submodule.span_le.mpr AddSubmonoid.subset_closure).antisymm'
    ((Submodule.span ℕ s).toAddSubmonoid.closure_le.mpr Submodule.subset_span)

Premises used: Iff.mpr, LE.le.antisymm', AddSubmonoid.closure_le, Submodule.subset_span, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
inst_3 : Semiring S
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
⊢ Eq (α := Submodule S M) (span S (↑p : Set M)) (restrictScalars S p)

Tactic:
span_eq (p.restrictScalars S)

Premises used: Submodule.restrictScalars, Submodule.span_eq
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
s : Set M
N : Submodule R₂ M₂
⊢ (⇑f : (a : M) → M₂) '' (↑(span R s) : Set M) ⊆ (↑N : Set M₂) ↔
    ∀ m ∈ s, Membership.mem (α := M₂) N ((f : (a : M) → M₂) m : M₂)

Tactic:
image_subset_iff.trans <| span_le (p := N.comap f)

Premises used: Iff.trans, Set.image_subset_iff, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
s : Set M
⊢ (⇑f : (a : M) → M₂) '' (↑(span R s) : Set M) ⊆ (↑(span R₂ ((⇑f : (a : M) → M₂) '' s)) : Set M₂)

Tactic:
(image_span_subset f s _).2 fun x hx ↦ subset_span ⟨x, hx, rfl⟩

Premises used: Iff.mpr, Submodule.image_span_subset, And.intro, Exists.intro, Submodule.subset_span, rfl
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
s : Set M
⊢ map f (span R s) = span R₂ ((⇑f : (a : M) → M₂) '' s)

Tactic:
Eq.symm <| span_eq_of_le _ (Set.image_mono subset_span) (image_span_subset_span f s)

Premises used: Submodule.span_eq_of_le, Set.image_mono, Submodule.image_span_subset_span, Submodule.subset_span, Eq.symm
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
s : Set M
N : Submodule R₂ M₂
⊢ map f (span R s) ≤ N ↔ ∀ m ∈ s, Membership.mem (α := M₂) N ((f : (a : M) → M₂) m : M₂)

Tactic:
image_span_subset f s N

Premises used: Set.Mem, setOf, Set.Subset, Submodule.image_span_subset, Set.image
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
s : Set M₂
rw : Subset.{u_4} (α := Set M) ((⇑f : (a : M) → M₂) ⁻¹' s) ((⇑f : (a : M) → M₂) ⁻¹' (↑(span R₂ s) : Set M₂))
⊢ span R ((⇑f : (a : M) → M₂) ⁻¹' s) ≤ comap f (span R₂ s)

Tactic:
rw [span_le, comap_coe]

Premises used: Submodule.comap_coe, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
s : Set M₂
⊢ Subset.{u_4} (α := Set M) ((⇑f : (a : M) → M₂) ⁻¹' s) ((⇑f : (a : M) → M₂) ⁻¹' (↑(span R₂ s) : Set M₂))

Tactic:
preimage_mono subset_span

Premises used: Set.preimage_mono, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
s : Set M₂
⊢ Subset.{u_4} (α := Set M) ((⇑f : (a : M) → M₂) ⁻¹' s) ((⇑f : (a : M) → M₂) ⁻¹' (↑(span R₂ s) : Set M₂))

Tactic:
exact preimage_mono subset_span

Premises used: Set.preimage_mono, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
s : Set M
t : Set M₂
h : MapsTo (⇑f : (a : M) → M₂) s t
⊢ MapsTo (⇑f : (a : M) → M₂) (↑(span R s) : Set M) (↑(span R₂ t) : Set M₂)

Tactic:
(span_mono h).trans (span_preimage_le (σ₁₂ := σ₁₂) f t)

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.preimage, Set.MapsTo, Submodule.span_mono, LE.le.trans, Submodule.span_preimage_le
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V_1 : Type u_6
S_1 : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
p p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s_1 t : Set M
N : Type u_8
inst_6 : AddCommMonoid N
inst_7 : Module R N
V : Submodule R M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥V) N
S : Set M
hV : V = span R S
s : (↑S : Type u_4)
⊢ (↑s : M) ∈ S

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V_1 : Type u_6
S_1 : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
p p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s_1 t : Set M
N : Type u_8
inst_6 : AddCommMonoid N
inst_7 : Module R N
V : Submodule R M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥V) N
S : Set M
hV : V = span R S
s : (↑S : Type u_4)
⊢ (↑s : M) ∈ V

Tactic:
simpa only [hV] using subset_span (by simp)

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
V : Submodule R M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥V) N
S : Set M
hV : V = span R S
mp :
  f = g →
    ∀ (s : (↑S : Type u_4)),
      Eq.{u_8 + 1} (α := N) ((f : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
        ((g : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
mpr :
  (∀ (s : (↑S : Type u_4)),
      Eq.{u_8 + 1} (α := N) ((f : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
        ((g : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)) →
    f = g
⊢ f = g ↔
    ∀ (s : (↑S : Type u_4)),
      Eq.{u_8 + 1} (α := N) ((f : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
        ((g : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
V : Submodule R M
f : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥V) N
S : Set M
hV : V = span R S
s : (↑S : Type u_4)
⊢ Eq.{u_8 + 1} (α := N) ((f : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
    ((f : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
V : Submodule R M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥V) N
S : Set M
hV : V = span R S
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N) ((f : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
      ((g : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
mpr :
  ∀ (f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N)
    (h :
      ∀ (s : (↑S : Type u_4)),
        Eq.{u_8 + 1} (α := N)
          ((f : (a : ↥(span R S)) → N)
              (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
            N)
          ((g : (a : ↥(span R S)) → N)
              (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
            N)),
    f = g
⊢ f = g

Tactic:
subst hV
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
this :
  ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
h₁ :
  ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
⊢ f = g

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
this :
  ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
x : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
⊢ Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)

Tactic:
this x hx
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
this :
  ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
x : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
⊢ Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)

Tactic:
exact this x hx
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
mpr :
  ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
⊢ f = g

Tactic:
suffices ∀ (x : M) (hx : x ∈ span R S), f ⟨x, hx⟩ = g ⟨x, hx⟩ by
      ext ⟨x, hx⟩
      exact this x hx
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
x_1 x : M
hx : x ∈ S
⊢ Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x ⋯) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x ⋯) :
      N)

Tactic:
h ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
x_1 x : M
hx : x ∈ S
⊢ Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x ⋯) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x ⋯) :
      N)

Tactic:
exact h ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
x : M
mpr :
  Eq.{u_8 + 1} (α := N) (0 : N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) 0 ⋯) :
      N)
mpr₁ mpr₂ : Eq.{u_8 + 1} (α := N) 0 0
⊢ Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) 0 ⋯) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) 0 ⋯) :
      N)

Tactic:
erw [map_zero, map_zero]

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
x_1 x y : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
hy : Membership.mem (γ := Submodule R M) (span R S) y
hx' :
  Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
hy' :
  Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N)
mpr :
  HAdd.hAdd (α := N) (β := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
        N) =
    HAdd.hAdd (α := N) (β := N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
        N)
⊢ Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (x + y) ⋯) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (x + y) ⋯) :
      N)

Tactic:
erw [f.map_add ⟨x, hx⟩ ⟨y, hy⟩, g.map_add ⟨x, hx⟩ ⟨y, hy⟩]

Premises used: LinearMap.map_add, Subtype.mk