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
x : M
rw :
  ∀ (s : Set (Submodule R M)),
    s.Nonempty → DirectedOn (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) s → R ∙ x ≤ sSup s → ∃ x_1 ∈ s, R ∙ x ≤ x_1
⊢ IsCompactElement (α := Submodule R M) (R ∙ x)

Tactic:
rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]

Premises used: CompleteLattice.isCompactElement_iff_le_of_directed_sSup_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
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) d
hsup : R ∙ x ≤ sSup d
⊢ x ∈ sSup d

Tactic:
have : x ∈ (sSup d) := (SetLike.le_def.mp hsup) (mem_span_singleton_self 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
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) d
hsup : R ∙ x ≤ sSup d
this : x ∈ sSup d
obtain : ∀ (y : Submodule R M) (hyd : y ∈ d) (hxy : x ∈ y), ∃ x_1 ∈ d, R ∙ x ≤ x_1
⊢ ∃ x_1 ∈ d, R ∙ x ≤ x_1

Tactic:
obtain ⟨y, ⟨hyd, hxy⟩⟩ := (mem_sSup_of_directed hemp hdir).mp this

Premises used: Iff.mp, Submodule.mem_sSup_of_directed
-- 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
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) d
hsup : R ∙ x ≤ sSup d
this : x ∈ sSup d
y : Submodule R M
hyd : y ∈ d
hxy : x ∈ y
⊢ R ∙ x ≤ y

Tactic:
simpa only [span_le, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Submodule.span_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
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) d
hsup : R ∙ x ≤ sSup d
this : x ∈ sSup d
y : Submodule R M
hyd : y ∈ d
hxy : x ∈ y
⊢ ∃ x_1 ∈ d, R ∙ x ≤ x_1

Tactic:
exact ⟨y, ⟨hyd, by simpa only [span_le, singleton_subset_iff] ⟩⟩
-- 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 : Finset M
rw : IsCompactElement.{u_4} (α := Submodule R M) (⨆ x ∈ (↑S : Set M), R ∙ x)
⊢ IsCompactElement (α := Submodule R M) (span R (↑S : Set M))

Tactic:
rw [span_eq_iSup_of_singleton_spans]

Premises used: Submodule.span_eq_iSup_of_singleton_spans
-- 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 : Finset M
rw : IsCompactElement (α := Submodule R M) (S.sup fun (x : M) ↦ R ∙ x)
⊢ IsCompactElement.{u_4} (α := Submodule R M) (⨆ x ∈ S, R ∙ x)

Tactic:
rw [← Finset.sup_eq_iSup]

Premises used: Finset.sup_eq_iSup
-- 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 : Finset M
⊢ IsCompactElement (α := Submodule R M) (S.sup fun (x : M) ↦ R ∙ x)

Tactic:
CompleteLattice.isCompactElement_finsetSup S fun x _ => singleton_span_isCompactElement x

Premises used: CompleteLattice.isCompactElement_finsetSup, Submodule.singleton_span_isCompactElement
-- 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 : Finset M
⊢ IsCompactElement (α := Submodule R M) (S.sup fun (x : M) ↦ R ∙ x)

Tactic:
exact
    CompleteLattice.isCompactElement_finsetSup S fun x _ => singleton_span_isCompactElement x

Premises used: CompleteLattice.isCompactElement_finsetSup, Submodule.singleton_span_isCompactElement
-- 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
h : S.Finite
⊢ IsCompactElement (α := Submodule R M) (span R S)

Tactic:
Finite.coe_toFinset h ▸ finset_span_isCompactElement h.toFinset

Premises used: Eq.rec, Set.Finite.coe_toFinset, Set.Finite.toFinset, Submodule.finset_span_isCompactElement
-- 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 : M
p p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s_1 t_1 : Set M
s t : Submodule R M
ht : Membership.mem (γ := Set (Submodule R M)) ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) t
rcases :
  ∀ x ∈ (↑s : Set M),
    ∀ (ht : Membership.mem (γ := Set (Submodule R M)) ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) (R ∙ x)),
      IsCompactElement (α := Submodule R M) (R ∙ x)
⊢ IsCompactElement t

Tactic:
rcases (Set.mem_image _ _ _).1 ht with ⟨x, _, rfl⟩

Premises used: Set.mem_image, Iff.mp, rfl
-- 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 p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s_1 t : Set M
s : Submodule R M
x : M
left : x ∈ (↑s : Set M)
ht : Membership.mem (γ := Set (Submodule R M)) ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) (R ∙ x)
⊢ IsCompactElement (α := Submodule R M) (R ∙ x)

Tactic:
apply singleton_span_isCompactElement

Premises used: Submodule.singleton_span_isCompactElement
-- 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 : 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
s : Submodule R M
rw :
  ⨆ (a : Submodule R M),
      ⨆ (_ : Membership.mem (γ := Set (Submodule R M)) ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) a), a =
    s
rw₁ : ⨆ b ∈ (↑s : Set M), R ∙ b = s
rw₂ : span R (↑s : Set M) = s
rw₃ rw₄ : s = s
⊢ sSup ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) = s

Tactic:
rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, span_eq]

Premises used: iSup_image, Submodule.span_eq, sSup_eq_iSup, Submodule.span_eq_iSup_of_singleton_spans
-- 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 p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s t : Set M
M' : Type u_8
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
q₁ q₁' : Submodule R M'
a : R
x : M
y : M'
hx : (x, y).1 ∈ (↑p : Set M)
hy : (x, y).2 ∈ (↑q₁ : Set M')
⊢ a • (x, y) ∈ (↑p : Set M) ×ˢ (↑q₁ : Set M')

Tactic:
⟨smul_mem _ a hx, smul_mem _ a hy⟩

Premises used: Set.Mem, setOf, Set.prod, And.intro, Submodule.smul_mem
-- 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 p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s t : Set M
M' : Type u_8
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
q₁ q₁' : Submodule R M'
a : R
x : M
y : M'
hx : (x, y).1 ∈ (↑p : Set M)
hy : (x, y).2 ∈ (↑q₁ : Set M')
⊢ a • (x, y) ∈ (↑p : Set M) ×ˢ (↑q₁ : Set M')

Tactic:
exact ⟨smul_mem _ a hx, smul_mem _ a hy⟩
-- 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
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ : Submodule R M'
⊢ (↑(p.prod q₁) : Set (M × M')) = (↑p : Set M) ×ˢ (↑q₁ : Set M')

Tactic:
rfl

Premises used: setOf, Set.prod, 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
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
p : Submodule R M
q : Submodule R M'
x : M × M'
⊢ x ∈ p.prod q ↔ x.1 ∈ p ∧ x.2 ∈ q

Tactic:
Set.mem_prod

Premises used: Set.Mem, setOf, Set.prod, Set.mem_prod
-- 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
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
s : Set M
t : Set M'
⊢ LE.le (α := Submodule R (M × M')) (span R (s ×ˢ t)) (prod (span R s) (span R t))

Tactic:
span_le.2 <| Set.prod_mono subset_span subset_span

Premises used: Iff.mpr, Set.prod_mono, Submodule.subset_span, Submodule.span_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
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
h :
  ∀ (x : M × M'),
    Membership.mem (γ := Submodule R (M × M')) (prod ⊤ ⊤) x ↔ Membership.mem (γ := Submodule R (M × M')) ⊤ x
⊢ Eq (α := Submodule R (M × M')) (prod ⊤ ⊤) ⊤

Tactic:
ext
-- 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
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
x : M × M'
⊢ Membership.mem (γ := Submodule R (M × M')) (prod ⊤ ⊤) x ↔ Membership.mem (γ := Submodule R (M × 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
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
h :
  ∀ (x : M) (y : M'),
    Membership.mem (γ := Submodule R (M × M')) (prod ⊥ ⊥) (x, y) ↔ Membership.mem (γ := Submodule R (M × M')) ⊥ (x, y)
⊢ Eq (α := Submodule R (M × M')) (prod ⊥ ⊥) ⊥

Tactic:
ext ⟨x, y⟩
-- 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
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
x : M
y : M'
⊢ Membership.mem (γ := Submodule R (M × M')) (prod ⊥ ⊥) (x, y) ↔ Membership.mem (γ := Submodule R (M × M')) ⊥ (x, y)

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
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
p p' : Submodule R M
q q' : Submodule R M'
⊢ p ≤ p' → q ≤ q' → p.prod q ≤ p'.prod q'

Tactic:
Set.prod_mono

Premises used: Set.Mem, setOf, Set.prod, Set.Subset, Set.prod_mono
-- 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 p' : Submodule R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ q₁' : Submodule R M'
⊢ p.prod q₁ ⊓ p'.prod q₁' = (p ⊓ p').prod (q₁ ⊓ q₁')

Tactic:
SetLike.coe_injective Set.prod_inter_prod

Premises used: SetLike.coe_injective, Set.prod_inter_prod
-- 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 p' : Submodule R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ q₁' : Submodule R M'
⊢ p.prod q₁ ⊔ p'.prod q₁' = (p ⊔ p').prod (q₁ ⊔ q₁')

Tactic:
le_antisymm
    (sup_le (prod_mono le_sup_left le_sup_left) (prod_mono le_sup_right le_sup_right)) ?_

Premises used: le_sup_left, Submodule.prod_mono, le_sup_right, le_antisymm, sup_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
p p' : Submodule R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ q₁' : Submodule R M'
refine : (p ⊔ p').prod (q₁ ⊔ q₁') ≤ p.prod q₁ ⊔ p'.prod q₁'
⊢ p.prod q₁ ⊔ p'.prod q₁' = (p ⊔ p').prod (q₁ ⊔ q₁')

Tactic:
refine le_antisymm
    (sup_le (prod_mono le_sup_left le_sup_left) (prod_mono le_sup_right le_sup_right)) ?_

Premises used: le_sup_left, Submodule.prod_mono, le_sup_right, le_antisymm, sup_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
p p' : Submodule R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ q₁' : Submodule R M'
simp : ∀ (a : M) (b : M'), a ∈ p ⊔ p' → b ∈ q₁ ⊔ q₁' → (a, b) ∈ p.prod q₁ ⊔ p'.prod q₁'
⊢ (p ⊔ p').prod (q₁ ⊔ q₁') ≤ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
simp only [SetLike.le_def, mem_prod, and_imp, Prod.forall]

Premises used: Submodule.mem_prod, and_imp, SetLike.le_def, Prod.forall
-- 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 p' : Submodule R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ q₁' : Submodule R M'
xx : M
yy : M'
hxx : xx ∈ p ⊔ p'
hyy : yy ∈ q₁ ⊔ q₁'
rcases : ∀ (x : M) (hx : x ∈ p) (x' : M) (hx' : x' ∈ p') (hxx : x + x' ∈ p ⊔ p'), (x + x', yy) ∈ p.prod q₁ ⊔ p'.prod q₁'
⊢ (xx, yy) ∈ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
rcases mem_sup.1 hxx with ⟨x, hx, x', hx', rfl⟩

Premises used: Iff.mp, Submodule.mem_sup, 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
p p' : Submodule R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ q₁' : Submodule R M'
yy : M'
hyy : yy ∈ q₁ ⊔ q₁'
x : M
hx : x ∈ p
x' : M
hx' : x' ∈ p'
hxx : x + x' ∈ p ⊔ p'
rcases :
  ∀ (y : M') (hy : y ∈ q₁) (y' : M') (hy' : y' ∈ q₁') (hyy : y + y' ∈ q₁ ⊔ q₁'),
    (x + x', y + y') ∈ p.prod q₁ ⊔ p'.prod q₁'
⊢ (x + x', yy) ∈ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
rcases mem_sup.1 hyy with ⟨y, hy, y', hy', rfl⟩

Premises used: Iff.mp, Submodule.mem_sup, 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
p p' : Submodule R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ q₁' : Submodule R M'
x : M
hx : x ∈ p
x' : M
hx' : x' ∈ p'
hxx : x + x' ∈ p ⊔ p'
y : M'
hy : y ∈ q₁
y' : M'
hy' : y' ∈ q₁'
hyy : y + y' ∈ q₁ ⊔ q₁'
⊢ (x + x', y + y') ∈ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
mem_sup.2 ⟨(x, y), ⟨hx, hy⟩, (x', y'), ⟨hx', hy'⟩, rfl⟩

Premises used: Iff.mpr, Set.Mem, Prod.mk, And.intro, Exists.intro, Submodule.mem_sup, 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
p p' : Submodule R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ q₁' : Submodule R M'
x : M
hx : x ∈ p
x' : M
hx' : x' ∈ p'
hxx : x + x' ∈ p ⊔ p'
y : M'
hy : y ∈ q₁
y' : M'
hy' : y' ∈ q₁'
hyy : y + y' ∈ q₁ ⊔ q₁'
⊢ (x + x', y + y') ∈ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
exact mem_sup.2 ⟨(x, y), ⟨hx, hy⟩, (x', y'), ⟨hx', hy'⟩, rfl⟩
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
u : M
v : N
hu : u ∈ s
hv : v ∈ t
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)

Tactic:
hB u hu v hv
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
u : M
v : N
hu : u ∈ s
hv : v ∈ t
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)

Tactic:
exact hB u hu v hv
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y v : N
hv : Membership.mem (γ := Submodule R N) (span R t) v
⊢ Membership.mem (α := P) P' (((B : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) v : P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
u : M
hu : Membership.mem (γ := Submodule R M) (span R s) u
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) 0 : P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
u₁ u₂ : M
v : N
hu₁ : Membership.mem (γ := Submodule R M) (span R s) u₁
hu₂ : Membership.mem (γ := Submodule R M) (span R s) u₂
hv : Membership.mem (γ := Submodule R N) (span R t) v
huv₁ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u₁ : N →ₗ[R] P) : (a : N) → P) v : P)
huv₂ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u₂ : N →ₗ[R] P) : (a : N) → P) v : P)
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) (u₁ + u₂) : N →ₗ[R] P) : (a : N) → P) v : P)

Tactic:
simpa using add_mem huv₁ huv₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
u : M
v₁ v₂ : N
hu : Membership.mem (γ := Submodule R M) (span R s) u
hv₁ : Membership.mem (γ := Submodule R N) (span R t) v₁
hv₂ : Membership.mem (γ := Submodule R N) (span R t) v₂
huv₁ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v₁ : P)
huv₂ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v₂ : P)
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) (v₁ + v₂) : P)

Tactic:
simpa using add_mem huv₁ huv₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t_1 : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t_1, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
t : R
u : M
v : N
hu : Membership.mem (γ := Submodule R M) (span R s) u
hv : Membership.mem (γ := Submodule R N) (span R t_1) v
huv : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) (t • u) : N →ₗ[R] P) : (a : N) → P) v : P)

Tactic:
simpa using Submodule.smul_mem _ _ huv

Premises used: Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t_1 : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t_1, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
t : R
u : M
v : N
hu : Membership.mem (γ := Submodule R M) (span R s) u
hv : Membership.mem (γ := Submodule R N) (span R t_1) v
huv : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) (t • v) : P)

Tactic:
simpa using Submodule.smul_mem _ _ huv

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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
⊢ Eq.{u_4 + 1} (α := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)) ⊤

Tactic:
eq_top_iff.mpr fun ⟨x, hx⟩ _ ↦ ?_

Premises used: Iff.mpr, eq_top_iff, iSup, Membership.mem, Submodule.comap, Submodule.subtype, _private.0.Submodule.biSup_comap_subtype_eq_top.match_1
-- 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_9
s : Set ι
p : ι → Submodule R M
refine :
  ∀ (x : ↥(⨆ i ∈ s, p i)) (x : M) (hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x),
    Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx) →
      Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i))
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
⊢ Eq.{u_4 + 1} (α := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)) ⊤

Tactic:
refine eq_top_iff.mpr fun ⟨x, hx⟩ _ ↦ ?_

Premises used: Iff.mpr, eq_top_iff