awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
rw :
  span S
      (image (α := ↥q) (⇑q.subtype : (a : ↥q) → M)
        (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) =
    q
⊢ map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = q

Tactic:
rw [map_span]

Premises used: 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
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 : (⇑q.subtype : (a : ↥q) → M) '' (↑(inclusion h₁).range : Set ↥(restrictScalars R q)) = (↑p : Set M)
⊢ span S
      (image (α := ↥q) (⇑q.subtype : (a : ↥q) → M)
        (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) =
    q

Tactic:
this ▸ le_antisymm ?_ h₂

Premises used: setOf, Eq.rec, le_antisymm, Set.range, Eq.symm
-- 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 : (⇑q.subtype : (a : ↥q) → M) '' (↑(inclusion h₁).range : Set ↥(restrictScalars R q)) = (↑p : Set M)
refine : span S (↑p : Set M) ≤ q
⊢ span S
      (image (α := ↥q) (⇑q.subtype : (a : ↥q) → M)
        (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) =
    q

Tactic:
refine this ▸ le_antisymm ?_ 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
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
this : (⇑q.subtype : (a : ↥q) → M) '' (↑(inclusion h₁).range : Set ↥(restrictScalars R q)) = (↑p : Set M)
⊢ span S (↑p : Set M) ≤ q

Tactic:
simpa using span_mono (R := S) h₁

Premises used: Submodule.span_mono
-- 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 : (⇑q.subtype : (a : ↥q) → M) '' (↑(inclusion h₁).range : Set ↥(restrictScalars R q)) = (↑p : Set M)
⊢ span S
      (image (α := ↥q) (⇑q.subtype : (a : ↥q) → M)
        (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) =
    q

Tactic:
suffices q.subtype '' ((LinearMap.range (inclusion h₁)) : Set <| q.restrictScalars R) = p by
    refine this ▸ le_antisymm ?_ h₂
    simpa using span_mono (R := S) 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
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
h :
  ∀ (x : M),
    Membership.mem (γ := Set M) ((⇑q.subtype : (a : ↥q) → M) '' (↑(inclusion h₁).range : Set ↥(restrictScalars R q)))
        x ↔
      x ∈ (↑p : Set M)
⊢ (⇑q.subtype : (a : ↥q) → M) '' (↑(inclusion h₁).range : Set ↥(restrictScalars R q)) = (↑p : Set M)

Tactic:
ext x
-- 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)
x : M
⊢ Membership.mem (γ := Set M) ((⇑q.subtype : (a : ↥q) → M) '' (↑(inclusion h₁).range : Set ↥(restrictScalars R q))) x ↔
    x ∈ (↑p : Set M)

Tactic:
simpa [range_inclusion] using fun hx ↦ h₁ hx

Premises used: Submodule.range_inclusion
-- 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 S M) (span S s) (span S (↑(span R s) : Set M))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
x y : M
mp : Eq (α := Submodule R M) (R ∙ x) (R ∙ y) → ∃ (z : Rˣ), z • x = y
mpr : (∃ (z : Rˣ), z • x = y) → Eq (α := Submodule R M) (R ∙ x) (R ∙ y)
⊢ Eq (α := Submodule R M) (R ∙ x) (R ∙ y) ↔ ∃ (z : Rˣ), z • x = y

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
x y : M
mp : ((∃ (a : R), a • y = x) ∧ ∃ (a : R), a • x = y) → ∃ (z : Rˣ), z • x = y
⊢ Eq (α := Submodule R M) (R ∙ x) (R ∙ y) → ∃ (z : Rˣ), z • x = y

Tactic:
simp only [le_antisymm_iff, span_singleton_le_iff_mem, mem_span_singleton]

Premises used: Submodule.mem_span_singleton, le_antisymm_iff, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
mp : ∀ (hb : b • HSMul.hSMul (β := M) a 0 = 0), ∃ (z : Rˣ), z • HSMul.hSMul (β := M) a 0 = 0
mp₁ : ∀ (hy : y ≠ 0), ∃ (z : Rˣ), z • a • y = y
⊢ ∃ (z : Rˣ), z • a • y = y

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
a b : R
hb : b • HSMul.hSMul (β := M) a 0 = 0
⊢ ∃ (z : Rˣ), z • HSMul.hSMul (β := M) a 0 = 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ ∃ (z : Rˣ), z • a • y = y

Tactic:
⟨⟨b, a, ?_, ?_⟩, hb⟩

Premises used: Units.mk, Exists.intro
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
mp : b * a = 1
mp₁ : a * b = 1
⊢ ∃ (z : Rˣ), z • a • y = y

Tactic:
refine ⟨⟨b, a, ?_, ?_⟩, hb⟩
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
mp : Eq.{u_9 + 1} (α := M) ((fun (x : R) ↦ x • y) (b * a)) ((fun (x : R) ↦ x • y) 1)
⊢ b * a = 1

Tactic:
apply smul_left_injective R hy

Premises used: smul_left_injective
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ Eq.{u_9 + 1} (α := M) ((fun (x : R) ↦ x • y) (b * a)) ((fun (x : R) ↦ x • y) 1)

Tactic:
simpa only [mul_smul, one_smul]

Premises used: one_smul, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ b • a • y ≠ 0

Tactic:
rw [← hb] at hy
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : b • a • y ≠ 0
mp : Eq.{u_9 + 1} (α := M) ((fun (x : R) ↦ x • a • y) (a * b)) ((fun (x : R) ↦ x • a • y) 1)
⊢ a * b = 1

Tactic:
apply smul_left_injective R (smul_ne_zero_iff.1 hy).2

Premises used: smul_left_injective, smul_ne_zero_iff, And.right, Iff.mp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : b • a • y ≠ 0
⊢ Eq.{u_9 + 1} (α := M) ((fun (x : R) ↦ x • a • y) (a * b)) ((fun (x : R) ↦ x • a • y) 1)

Tactic:
simp only [mul_smul, one_smul, hb]

Premises used: one_smul, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
x : M
u : Rˣ
⊢ Eq (α := Submodule R M) (R ∙ x) (R ∙ u • x)

Tactic:
(span_singleton_group_smul_eq _ _ _).symm

Premises used: Eq.symm, Submodule.span_singleton_group_smul_eq
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
x : M
u : Rˣ
⊢ Eq (α := Submodule R M) (R ∙ x) (R ∙ u • x)

Tactic:
exact (span_singleton_group_smul_eq _ _ _).symm

Premises used: Eq.symm, Submodule.span_singleton_group_smul_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₂
s : Set M
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
⊢ span R₂ ((⇑f : (a : M) → M₂) '' s) = map f (span R s)

Tactic:
(map_span f s).symm

Premises used: Submodule.map_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₂
s : Set M
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] M₂
⊢ span R₂ ((⇑f : (a : M) → M₂) '' s) = map (↑f : M →ₛₗ[σ₁₂] M₂) (span R s)

Tactic:
span_image _

Premises used: Submodule.span_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₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
h : Membership.mem (γ := Submodule R M) (span R s) x
rw : Membership.mem (α := M₂) (map f (span R s)) ((f : (a : M) → M₂) x : M₂)
⊢ Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R₂ M₂) (span R₂ ((⇑f : (a : M) → M₂) '' s))
    ((f : (a : M) → M₂) x : M₂)

Tactic:
rw [Submodule.span_image]

Premises used: Submodule.span_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₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
h : Membership.mem (γ := Submodule R M) (span R s) x
⊢ Membership.mem (α := M₂) (map f (span R s)) ((f : (a : M) → M₂) x : M₂)

Tactic:
Submodule.mem_map_of_mem h

Premises used: Submodule.mem_map_of_mem
-- 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₂
x : M
s : Set M
h : Membership.mem (γ := Submodule R M) (span R s) x
⊢ Membership.mem (α := M₂) (map f (span R s)) ((f : (a : M) → M₂) x : M₂)

Tactic:
exact Submodule.mem_map_of_mem h

Premises used: Submodule.mem_map_of_mem
-- 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₂
x : M
s : Set M
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
rw : x ∈ comap f (span R₂ ((⇑f : (a : M) → M₂) '' s)) ↔ Membership.mem (γ := Submodule R M) (span R s) x
rw₁ : x ∈ comap f (map f (span R s)) ↔ Membership.mem (γ := Submodule R M) (span R s) x
rw₂ rw₃ : Membership.mem (γ := Submodule R M) (span R s) x ↔ Membership.mem (γ := Submodule R M) (span R s) x
⊢ Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R₂ M₂) (span R₂ ((⇑f : (a : M) → M₂) '' s))
      ((f : (a : M) → M₂) x : M₂) ↔
    Membership.mem (γ := Submodule R M) (span R s) x

Tactic:
rw [← Submodule.mem_comap, ← Submodule.map_span, Submodule.comap_map_eq_of_injective hf]

Premises used: Submodule.comap_map_eq_of_injective, Submodule.mem_comap, Submodule.map_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
p : Submodule R M
x : ↥p
⊢ map p.subtype (R ∙ x) = R ∙ (↑x : M)

Tactic:
simp [← span_image]

Premises used: Submodule.span_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₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
h : ((f : (a : M) → M₂) x : M₂) ∉ span R₂ ((⇑f : (a : M) → M₂) '' s)
⊢ x ∉ span R s

Tactic:
h.imp (apply_mem_span_image_of_mem_span f)

Premises used: Not.imp, Submodule.apply_mem_span_image_of_mem_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
α : Type u_8
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
a : α
s : Set M
⊢ HSMul.hSMul (β := Submodule R M) a (span R s) = span R (a • s)

Tactic:
map_span _ _

Premises used: Submodule.map_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
α : Type u_8
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
a : α
S : Submodule R M
⊢ a • S = span R (↑(a • S) : Set M)

Tactic:
simp [← smul_span]

Premises used: Submodule.smul_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
α : Type u_8
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
a : α
s : Set M
⊢ span R (a • s) = HSMul.hSMul (β := Submodule R M) a (span R s)

Tactic:
Eq.symm (span_image _).symm

Premises used: Submodule.span_image, 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
α : Type u_8
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
s : Set α
t : Set M
simp_rw : Eq (α := Submodule R M) (⨆ a ∈ s, HSMul.hSMul (β := Submodule R M) a (span R t)) (span R (s • t))
simp_rw₁ : Eq (α := Submodule R M) (⨆ a ∈ s, span R (a • t)) (span R (s • t))
simp_rw₂ : Eq (α := Submodule R M) (span R (⋃ i ∈ s, i • t)) (span R (s • t))
⊢ HSMul.hSMul (β := Submodule R M) s (span R t) = span R (s • t)

Tactic:
simp_rw [set_smul_eq_iSup, smul_span, iSup_span, Set.iUnion_smul_set]

Premises used: Submodule.iSup_span, Set.iUnion_smul_set, Submodule.set_smul_eq_iSup, Submodule.smul_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
α : Type u_8
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
s : Set α
t : Set M
⊢ span R (s • t) = HSMul.hSMul (β := Submodule R M) s (span R t)

Tactic:
(set_smul_span s t).symm

Premises used: Submodule.set_smul_span, 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
ι : Sort u_8
p : ι → Submodule R M
⊢ Eq.{u_4 + 1} (α := AddSubmonoid M) (toAddSubmonoid.{u_1, u_4} (R := R) (⨆ (i : ι), p i))
    (⨆ (i : ι), (p i).toAddSubmonoid)

Tactic:
le_antisymm (fun x => ?_) (iSup_le fun i => toAddSubmonoid_mono <| le_iSup _ i)

Premises used: le_iSup, Submodule.toAddSubmonoid_mono, le_antisymm, iSup_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
ι : Sort u_8
p : ι → Submodule R M
refine :
  ∀ (x : M),
    Membership.mem (γ := AddSubmonoid M) (toAddSubmonoid.{u_1, u_4} (R := R) (⨆ (i : ι), p i)) x →
      Membership.mem (γ := AddSubmonoid M) (⨆ (i : ι), (p i).toAddSubmonoid) x
⊢ Eq.{u_4 + 1} (α := AddSubmonoid M) (toAddSubmonoid.{u_1, u_4} (R := R) (⨆ (i : ι), p i))
    (⨆ (i : ι), (p i).toAddSubmonoid)

Tactic:
refine le_antisymm (fun x => ?_) (iSup_le fun i => toAddSubmonoid_mono <| le_iSup _ i)

Premises used: le_iSup, Submodule.toAddSubmonoid_mono, le_antisymm, iSup_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
ι : Sort u_8
p : ι → Submodule R M
x : M
simp_rw :
  Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x →
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
⊢ Membership.mem (γ := AddSubmonoid M) (toAddSubmonoid.{u_1, u_4} (R := R) (⨆ (i : ι), p i)) x →
    Membership.mem (γ := AddSubmonoid M) (⨆ (i : ι), (p i).toAddSubmonoid) x

Tactic:
simp_rw [iSup_eq_span, AddSubmonoid.iSup_eq_closure, mem_toAddSubmonoid, coe_toAddSubmonoid]

Premises used: Submodule.coe_toAddSubmonoid, Submodule.iSup_eq_span, Submodule.mem_toAddSubmonoid, AddSubmonoid.iSup_eq_closure
-- 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
ι : Sort u_8
p : ι → Submodule R M
x : M
hx : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x

Tactic:
Submodule.span_induction (fun x hx => ?_) ?_ (fun x y _ _ hx hy => ?_)
    (fun r x _ hx => ?_) hx

Premises used: Submodule.span_induction
-- 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
ι : Sort u_8
p : ι → Submodule R M
x : M
hx : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
refine_1 :
  ∀ (x : M) (hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(p i) : Set M)) x),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
refine_2 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) 0
refine_3 :
  ∀ (x y : M),
    Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x →
      Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) y →
        ∀ (hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x)
          (hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) y),
          Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (x + y)
refine_4 :
  ∀ (r : R) (x : M),
    Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x →
      ∀ (hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x),
        Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x

Tactic:
refine Submodule.span_induction (fun x hx => ?_) ?_ (fun x y _ _ hx hy => ?_)
    (fun r x _ hx => ?_) 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
ι : Sort u_8
p : ι → Submodule R M
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_1
x : M
hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(p i) : Set M)) x
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x

Tactic:
AddSubmonoid.subset_closure hx

Premises used: AddSubmonoid.subset_closure
-- 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
ι : Sort u_8
p : ι → Submodule R M
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_1
x : M
hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(p i) : Set M)) x
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x

Tactic:
exact AddSubmonoid.subset_closure hx

Premises used: AddSubmonoid.subset_closure
-- 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
ι : Sort u_8
p : ι → Submodule R M
x : M
hx : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) 0

Tactic:
AddSubmonoid.zero_mem _

Premises used: AddSubmonoid.zero_mem
-- 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
ι : Sort u_8
p : ι → Submodule R M
x : M
hx : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) 0

Tactic:
exact AddSubmonoid.zero_mem _

Premises used: AddSubmonoid.zero_mem
-- 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
ι : Sort u_8
p : ι → Submodule R M
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_1
x y : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
h_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) y
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) y
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (x + y)

Tactic:
AddSubmonoid.add_mem _ hx hy

Premises used: AddSubmonoid.add_mem, Set.Mem
-- 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
ι : Sort u_8
p : ι → Submodule R M
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_1
x y : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
h_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) y
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) y
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (x + y)

Tactic:
exact AddSubmonoid.add_mem _ hx hy

Premises used: AddSubmonoid.add_mem