awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : M
a : R
x : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
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)
mpr :
  HSMul.hSMul (β := N) a
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N) =
    HSMul.hSMul (β := N) a
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        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) (a • x) ⋯) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (a • x) ⋯) :
      N)

Tactic:
erw [f.map_smul a ⟨x, hx⟩, g.map_smul a ⟨x, hx⟩]

Premises used: Subtype.mk, LinearMap.map_smul
-- 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 : M
a : R
x : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
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)
mpr mpr₁ :
  HSMul.hSMul (β := N) a
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N) =
    HSMul.hSMul (β := N) a
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
⊢ HSMul.hSMul (β := N) a
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N) =
    HSMul.hSMul (β := N) a
      ((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:
rw [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
f g : M →ₗ[R] N
S : Set M
hM : Eq (α := Submodule R M) (span R S) ⊤
⊢ Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤) ↔
    ∀ (s : (↑S : Type u_4)),
      Eq.{u_8 + 1} (α := N)
        ((f ∘ₗ Submodule.subtype ⊤ : (a : ↥⊤) → N)
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) ⊤ x) (↑s : M) ⋯) :
          N)
        ((g ∘ₗ Submodule.subtype ⊤ : (a : ↥⊤) → N)
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) ⊤ x) (↑s : M) ⋯) :
          N)

Tactic:
linearMap_eq_iff_of_eq_span (f.comp (Submodule.subtype _)) (g.comp (Submodule.subtype _))
      hM.symm

Premises used: LinearMap.comp, Submodule.linearMap_eq_iff_of_eq_span, Submodule.subtype, Eq.symm
-- 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
f g : M →ₗ[R] N
S : Set M
hM : Eq (α := Submodule R M) (span R S) ⊤
h :
  f = g ↔
    Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤)
⊢ f = g ↔
    ∀ (s : (↑S : Type u_4)), Eq.{u_8 + 1} (α := N) ((f : (a : M) → N) (↑s : M) : N) ((g : (a : M) → N) (↑s : M) : N)

Tactic:
convert!
    linearMap_eq_iff_of_eq_span (f.comp (Submodule.subtype _)) (g.comp (Submodule.subtype _))
      hM.symm

Premises used: LinearMap.comp, Submodule.linearMap_eq_iff_of_eq_span, Submodule.subtype, Eq.symm
-- 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
f g : M →ₗ[R] N
S : Set M
hM : Eq (α := Submodule R M) (span R S) ⊤
h :
  f = g →
    Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤)
h₁ :
  Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤) →
    f = g
⊢ f = g ↔
    Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤)

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
f : M →ₗ[R] N
S : Set M
hM : Eq (α := Submodule R M) (span R S) ⊤
⊢ Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (f ∘ₗ Submodule.subtype ⊤)

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
f g : M →ₗ[R] N
S : Set M
hM : Eq (α := Submodule R M) (span R S) ⊤
h : Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤)
h₁ : ∀ (x : M), Eq.{u_8 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
⊢ f = g

Tactic:
ext x
-- 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
f g : M →ₗ[R] N
S : Set M
hM : Eq (α := Submodule R M) (span R S) ⊤
h : Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤)
x : M
⊢ Membership.mem (γ := Submodule R M) ⊤ x

Tactic:
simp
-- 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
f g : M →ₗ[R] N
S : Set M
hM : Eq (α := Submodule R M) (span R S) ⊤
h : Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤)
x : M
⊢ Eq.{u_8 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

Tactic:
exact DFunLike.congr_fun h ⟨x, by simp⟩

Premises used: DFunLike.congr_fun
-- 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
f : M →ₗ[R] N
S : Set M
hM : Eq (α := Submodule R M) (span R S) ⊤
⊢ f = 0 ↔ ∀ (s : (↑S : Type u_4)), Eq.{u_8 + 1} (α := N) ((f : (a : M) → N) (↑s : M) : N) (0 : N)

Tactic:
linearMap_eq_iff_of_span_eq_top f 0 hM

Premises used: Submodule.linearMap_eq_iff_of_span_eq_top, OfNat.ofNat
-- 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 : 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 : 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 : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥V) N
S : Set M
hV : V = span R S
⊢ f = 0 ↔
    ∀ (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) (0 : N)

Tactic:
linearMap_eq_iff_of_eq_span f 0 hV

Premises used: Submodule.linearMap_eq_iff_of_eq_span, OfNat.ofNat
-- 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
s : Set M
r : R
hr : IsUnit r
a : LE.le (α := Submodule R M) (span R (r • s)) (span R s)
a₁ : LE.le (α := Submodule R M) (span R s) (span R (r • s))
⊢ Eq (α := Submodule R M) (span R (r • s)) (span R s)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
s : Set M
r : R
hr : IsUnit r
⊢ LE.le (α := Submodule R M) (span R (r • s)) (span R s)

Tactic:
apply span_smul_le

Premises used: Submodule.span_smul_le
-- 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
s : Set M
r : R
hr : IsUnit r
⊢ LE.le (α := Submodule R M) (span R ((↑hr.unit⁻¹ : R) • r • s)) (span R (r • s))

Tactic:
span_smul_le (r • s) ((hr.unit⁻¹ :) : R)

Premises used: Units.val, Submodule.span_smul_le, Inv.inv, IsUnit.unit, HSMul.hSMul
-- 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
s : Set M
r : R
hr : IsUnit r
h : s = (↑hr.unit⁻¹ : R) • r • s
⊢ LE.le (α := Submodule R M) (span R s) (span R (r • s))

Tactic:
convert! span_smul_le (r • s) ((hr.unit⁻¹ :) : R)

Premises used: Units.val, Submodule.span_smul_le, Inv.inv, IsUnit.unit, HSMul.hSMul
-- 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
s : Set M
r : R
hr : IsUnit r
⊢ s = (↑hr.unit⁻¹ : R) • r • s

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- 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
⊢ OmegaCompletePartialOrder.ωScottContinuous (α := Submodule R M) SetLike.coe

Tactic:
OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup
    ⟨SetLike.coe_mono, fun _ ↦ coe_iSup_of_chain _⟩

Premises used: Exists.intro, OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup, OmegaCompletePartialOrder.Chain.toOrderHom, SetLike.coe_mono, Submodule.coe_iSup_of_chain
-- 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 : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x_1 : M
p_1 p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s t : Set M
inst_6 : Semiring S
inst_7 : SMul R S
inst_8 : Module S M
inst_9 : IsScalarTower R S M
p : Submodule R M
x y : ↥p
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule S M) (span S (↑p : Set M)) x) (↑(x + y) : M) ⋯ =
    HAdd.hAdd (α := ↥(span S (↑p : Set M)))
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule S M) (span S (↑p : Set M)) x) (↑x : M) ⋯)
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule S M) (span S (↑p : Set M)) x) (↑y : M) ⋯)

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 : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x_1 : M
p_1 p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s t_1 : Set M
inst_6 : Semiring S
inst_7 : SMul R S
inst_8 : Module S M
inst_9 : IsScalarTower R S M
p : Submodule R M
t : R
x : ↥p
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule S M) (span S (↑p : Set M)) x) (↑(t • x) : M) ⋯ =
    HSMul.hSMul (α := R) (β := ↥(span S (↑p : Set M))) ((RingHom.id R : (a : R) → R) t : R)
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule S M) (span S (↑p : Set M)) x) (↑x : M) ⋯)

Tactic:
simp
-- 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
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
x y : ↥p
hxy :
  Eq (α := ↥(span S (↑p : Set M))) ((inclusionSpan S p : (a : ↥p) → ↥(span S (↑p : Set M))) x : ↥(span S (↑p : Set M)))
    ((inclusionSpan S p : (a : ↥p) → ↥(span S (↑p : Set M))) y : ↥(span S (↑p : Set M)))
⊢ Eq.{u_4 + 1} (α := M) (↑((inclusionSpan S p : (a : ↥p) → ↥(span S (↑p : Set M))) x) : M)
    (↑((inclusionSpan S p : (a : ↥p) → ↥(span S (↑p : Set M))) y) : M)

Tactic:
rw [Subtype.ext_iff] at hxy

Premises used: Subtype.ext_iff
-- 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
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
x y : ↥p
hxy :
  Eq.{u_4 + 1} (α := M) (↑((inclusionSpan S p : (a : ↥p) → ↥(span S (↑p : Set M))) x) : M)
    (↑((inclusionSpan S p : (a : ↥p) → ↥(span S (↑p : Set M))) y) : M)
⊢ x = y

Tactic:
simpa using hxy
-- 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
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
h :
  ∀ (x : M),
    Membership.mem (γ := Set M)
        (image (α := ↥(span S (↑p : Set M)))
          (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
          (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))))
        x ↔
      x ∈ (↑p : Set M)
⊢ image (α := ↥(span S (↑p : Set M))) (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
      (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))) =
    (↑p : Set M)

Tactic:
ext
-- 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
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
x : M
⊢ Membership.mem (γ := Set M)
      (image (α := ↥(span S (↑p : Set M)))
        (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
        (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))))
      x ↔
    x ∈ (↑p : Set M)

Tactic:
simpa [Subtype.ext_iff] using fun h ↦ subset_span h

Premises used: Subtype.ext_iff, Submodule.subset_span
-- 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
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
⊢ image (α := ↥(span S (↑p : Set M))) (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
      (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))) =
    (↑p : Set M)

Tactic:
have : (span S (p : Set M)).subtype '' range (inclusionSpan S p) = p := by
    ext; simpa [Subtype.ext_iff] using fun h ↦ subset_span h
-- 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
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
this :
  image (α := ↥(span S (↑p : Set M))) (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
      (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))) =
    (↑p : Set M)
a :
  Eq (α := Submodule S M)
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M)))
      (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M))) ⊤)
⊢ Eq (α := Submodule S ↥(span S (↑p : Set M)))
    (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))) ⊤

Tactic:
apply map_injective_of_injective (span S (p : Set M)).injective_subtype

Premises used: Submodule.injective_subtype, SetLike.coe, Submodule.span, Submodule.map_injective_of_injective
-- 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
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
this :
  image (α := ↥(span S (↑p : Set M))) (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
      (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))) =
    (↑p : Set M)
a :
  Eq (α := Submodule S M)
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M)))
      (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
    (span S (↑p : Set M))
a₁ :
  Eq (α := Submodule S M)
    (span S
      (image (α := ↥(span S (↑p : Set M)))
        (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
        (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
    (span S (↑p : Set M))
a₂ a₃ : Eq (α := Submodule S M) (span S (↑p : Set M)) (span S (↑p : Set M))
⊢ Eq (α := Submodule S M)
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M)))
      (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M))) ⊤)

Tactic:
rw [map_subtype_top, map_span, this]

Premises used: Submodule.map_subtype_top, Submodule.map_span
-- 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
s : Set M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
⊢ LE.le (α := Submodule R M) (span R s) (restrictScalars R (span S s))

Tactic:
Submodule.span_le.2 Submodule.subset_span

Premises used: Iff.mpr, 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
s : Set M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
⊢ (↑(span R s) : Set M) ⊆ (↑(span S s) : Set M)

Tactic:
span_le_restrictScalars R S s

Premises used: iInf, Set.Mem, Set.iInter, setOf, Submodule.span_le_restrictScalars, Set.Subset
-- 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
s : Set M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
⊢ Eq (α := Submodule S M) (span S (↑(span R s) : Set M)) (span S s)

Tactic:
le_antisymm (span_le.2 <| span_subset_span R S s) (span_mono subset_span)

Premises used: Iff.mpr, Submodule.span_subset_span, le_antisymm, Submodule.span_mono, 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
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
⊢ Eq (α := Submodule S M) (span S s) ⊤

Tactic:
le_top.antisymm (hs.ge.trans (span_le_restrictScalars R S s))

Premises used: Eq.ge, Submodule.span_le_restrictScalars, LE.le.antisymm, le_top, LE.le.trans
-- 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
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
this : map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = q
a : map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = map q.subtype ⊤
⊢ Eq (α := Submodule S ↥(restrictScalars R q))
    (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) ⊤

Tactic:
apply map_injective_of_injective q.injective_subtype

Premises used: Submodule.injective_subtype, Submodule.map_injective_of_injective
-- 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
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
this : map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = q
a : q = map q.subtype ⊤
a₁ a₂ : q = q
⊢ map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = map q.subtype ⊤

Tactic:
rw [this, q.map_subtype_top]

Premises used: Submodule.map_subtype_top
-- 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
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
suffices : map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = q
⊢ Eq (α := Submodule S ↥(restrictScalars R q))
    (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) ⊤

Tactic:
suffices (span S (range (inclusion h₁))).map q.subtype = q by
    apply map_injective_of_injective q.injective_subtype
    rw [this, q.map_subtype_top]