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
ι : 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
r : R
x : M
h : 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)

Tactic:
AddSubmonoid.closure_induction ?_ ?_ ?_ hx

Premises used: AddSubmonoid.closure_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_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_1
r : R
x : M
h : 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
refine_4 :
  ∀ (x : M) (h : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(p i) : Set M)) x),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
refine_4₁ :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (HSMul.hSMul (β := M) r 0)
refine_4₂ :
  ∀ (x y : M) (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))) (r • x) →
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • y) →
        Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • (x + y))
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)

Tactic:
refine AddSubmonoid.closure_induction ?_ ?_ ?_ 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
r : R
x_2 : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_2
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x_2
x : M
i : ι
hix : x ∈ p i
apply : r • x ∈ (↑(p i) : Set M)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)

Tactic:
apply AddSubmonoid.subset_closure (Set.mem_iUnion.mpr ⟨i, _⟩)

Premises used: Iff.mpr, Set.mem_iUnion, AddSubmonoid.subset_closure, Exists.intro
-- 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
r : R
x_2 : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_2
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x_2
x : M
i : ι
hix : x ∈ p i
⊢ r • x ∈ (↑(p i) : Set M)

Tactic:
smul_mem _ r hix

Premises used: Submodule.smul_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
r : R
x_2 : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_2
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x_2
x : M
i : ι
hix : x ∈ p i
⊢ r • x ∈ (↑(p i) : Set M)

Tactic:
exact smul_mem _ r hix

Premises used: Submodule.smul_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
r : R
x : M
h : 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
refine_4 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) 0
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (HSMul.hSMul (β := M) r 0)

Tactic:
rw [smul_zero]

Premises used: smul_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
ι : 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
r : R
x : M
h : 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))) 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_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_1
r : R
x : M
h : 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))) 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
r : R
x_2 : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_2
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x_2
x y : M
refine_4 :
  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))) (r • x) →
        Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • y) →
          Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • (x + 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))) (r • x) →
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • y) →
        Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • (x + y))

Tactic:
_
-- 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
r : R
x_2 : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_2
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x_2
x y : M
hx_2 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
refine_4 :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) y →
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x) →
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • y) →
        Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • (x + y))
⊢ ∀ (hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) y),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x) →
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • y) →
        Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • (x + y))

Tactic:
_
-- 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
r : R
x_2 : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_2
hx_2 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x_2
x y : M
hx_3 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
hy_1 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) y
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • y)
refine_4 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x + r • y)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • (x + y))

Tactic:
rw [smul_add]

Premises used: smul_add
-- 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
r : R
x_2 : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_2
hx_2 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x_2
x y : M
hx_3 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
hy_1 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) y
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • y)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x + r • y)

Tactic:
AddSubmonoid.add_mem _ hx hy

Premises used: AddSubmonoid.add_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
r : R
x_2 : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_2
hx_2 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x_2
x y : M
hx_3 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
hy_1 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) y
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • y)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x + r • y)

Tactic:
exact AddSubmonoid.add_mem _ hx hy

Premises used: AddSubmonoid.add_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
motive : M → Prop
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (i : ι), (p i).toAddSubmonoid) x

Tactic:
rw [← mem_toAddSubmonoid, iSup_toAddSubmonoid] at hx

Premises used: Submodule.mem_toAddSubmonoid, Submodule.iSup_toAddSubmonoid
-- 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
motive : M → Prop
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
hx₁ : Membership.mem (γ := AddSubmonoid M) (⨆ (i : ι), (p i).toAddSubmonoid) x
⊢ ∀ (i : ι), ∀ x ∈ p i, motive x

Tactic:
rw [← mem_toAddSubmonoid, iSup_toAddSubmonoid] at hx

Premises used: Submodule.mem_toAddSubmonoid, Submodule.iSup_toAddSubmonoid
-- 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
motive : M → Prop
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
hx₁ : Membership.mem (γ := AddSubmonoid M) (⨆ (i : ι), (p i).toAddSubmonoid) x
mem₁ : ∀ (i : ι), ∀ x ∈ p i, motive x
⊢ motive 0

Tactic:
rw [← mem_toAddSubmonoid, iSup_toAddSubmonoid] at hx

Premises used: Submodule.mem_toAddSubmonoid, Submodule.iSup_toAddSubmonoid
-- 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
motive : M → Prop
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
hx₁ : Membership.mem (γ := AddSubmonoid M) (⨆ (i : ι), (p i).toAddSubmonoid) x
mem₁ : ∀ (i : ι), ∀ x ∈ p i, motive x
zero₁ : motive 0
⊢ ∀ (x y : M), motive x → motive y → motive (x + y)

Tactic:
rw [← mem_toAddSubmonoid, iSup_toAddSubmonoid] at hx

Premises used: Submodule.mem_toAddSubmonoid, Submodule.iSup_toAddSubmonoid
-- 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
motive : M → Prop
x : M
hx : Membership.mem (γ := AddSubmonoid M) (⨆ (i : ι), (p i).toAddSubmonoid) x
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive x

Tactic:
AddSubmonoid.iSup_induction (x := x) _ hx mem zero add

Premises used: AddSubmonoid.iSup_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
motive : M → Prop
x : M
hx : Membership.mem (γ := AddSubmonoid M) (⨆ (i : ι), (p i).toAddSubmonoid) x
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive x

Tactic:
exact AddSubmonoid.iSup_induction (x := x) _ hx mem zero add
-- 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
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
⊢ motive x hx

Tactic:
Exists.elim ?_ fun (hx : x ∈ ⨆ i, p i) (hc : motive x hx) => hc

Premises used: Exists.elim
-- 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
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
refine : ∃ (x_1 : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x x_1
⊢ motive x hx

Tactic:
refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, p i) (hc : motive x hx) => hc

Premises used: Exists.elim
-- 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
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
⊢ ∃ (x_1 : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x x_1

Tactic:
iSup_induction p (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, p i), motive x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_

Premises used: Submodule.iSup_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
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
refine_1 :
  ∀ (i : ι) (x : M) (hx : x ∈ p i),
    (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) x
refine_2 : ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) 0), motive 0 hx
refine_3 :
  ∀ (x y : M),
    (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) x →
      (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) y →
        (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) (x + y)
⊢ ∃ (x_1 : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x x_1

Tactic:
refine iSup_induction p (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, p i), motive x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_

Premises used: Submodule.iSup_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
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x_1
i : ι
x : M
hx : x ∈ p i
⊢ (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) x

Tactic:
⟨_, mem _ _ hx⟩

Premises used: Exists.intro
-- 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
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x_1
i : ι
x : M
hx : x ∈ p i
⊢ (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) x

Tactic:
exact ⟨_, mem _ _ 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
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
⊢ (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) 0

Tactic:
⟨_, zero⟩

Premises used: Exists.intro
-- 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
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
⊢ (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) 0

Tactic:
exact ⟨_, 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
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x_1 : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x_1
x y : M
w : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
Cx : motive x w
w_1 : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y
Cy : motive y w_1
⊢ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) (x + y)), motive (x + y) hx

Tactic:
⟨_, add _ _ _ _ Cx Cy⟩

Premises used: Exists.intro
-- 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
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x_1 : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x_1
x y : M
w : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
Cx : motive x w
w_1 : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y
Cy : motive y w_1
⊢ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) (x + y)), motive (x + y) hx

Tactic:
exact ⟨_, add _ _ _ _ Cx Cy⟩