-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
refine_1 :
  ∀ (x : M) (hx : x ∈ S),
    ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x
refine_2 : ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) 0
refine_3 :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x)
    (hy : Membership.mem (γ := Submodule R M) (span R S) y),
    (∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x) →
      (∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) y) →
        ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (x + y)
refine_4 :
  ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x),
    (∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x) →
      ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (a • x)
refine_2₁ : ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) 0
refine_3₁ :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x)
    (hy : Membership.mem (γ := Submodule R M) (span R S) y),
    (∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x) →
      (∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) y) →
        ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (x + y)
refine_4₁ :
  ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x),
    (∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x) →
      ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (a • x)
refine_3₂ :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x)
    (hy : Membership.mem (γ := Submodule R M) (span R S) y),
    (∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x) →
      (∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) y) →
        ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (x + y)
refine_4₂ refine_4₃ :
  ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x),
    (∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x) →
      ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (a • x)
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x

Tactic:
classical
  refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx
  · refine ⟨{x}, ?_, ?_⟩
    · rwa [Finset.coe_singleton, Set.singleton_subset_iff]
    · rw [Finset.coe_singleton]
      exact Submodule.mem_span_singleton_self x
  · use ∅
    simp
  · rintro x y - - ⟨X, hX, hxX⟩ ⟨Y, hY, hyY⟩
    refine ⟨X ∪ Y, ?_, ?_⟩
    · rw [Finset.coe_union]
      exact Set.union_subset hX hY
    rw [Finset.coe_union, span_union, mem_sup]
    exact ⟨x, hxX, y, hyY, rfl⟩
  · rintro a x - ⟨T, hT, h2⟩
    exact ⟨T, hT, smul_mem _ _ h2⟩

Premises used: Set.singleton_subset_iff, Finset.coe_singleton, Submodule.mem_span_singleton_self, Submodule.span_union, Submodule.mem_sup, Finset.coe_union