Theorem: Set.mem_relOrthSpace_iff (Matroid/ForMathlib/LinearAlgebra/StdBasis.lean)

State before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ w ∈ s.relOrthSpace U ↔ ∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
Tactic:
rw [relOrthSpace, mem_inf, mem_orthSpace_iff'', mem_supportedFun_iff]
State after:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s ↔
    ∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0

State before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s ↔
    ∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
Tactic:
constructor
State after:
case mp
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s →
    ∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0

case mpr
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0) →
    (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s

State before:
case mpr
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0) →
    (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s
Tactic:
rintro ⟨l, rfl, hl⟩
State after:
case mpr.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ↥(Finsupp.supported R R s)
hl : ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
⊢ (∃ l_1, ⇑l_1 = ⇑↑l ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l_1 = 0) ∧ support ⇑↑l ⊆ s

State before:
case mpr.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ↥(Finsupp.supported R R s)
hl : ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
⊢ (∃ l_1, ⇑l_1 = ⇑↑l ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l_1 = 0) ∧ support ⇑↑l ⊆ s
Tactic:
refine ⟨⟨l, rfl, hl⟩, ?_⟩
State after:
case mpr.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ↥(Finsupp.supported R R s)
hl : ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
⊢ support ⇑↑l ⊆ s

State before:
case mpr.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ↥(Finsupp.supported R R s)
hl : ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
⊢ support ⇑↑l ⊆ s
Tactic:
rw [Finsupp.fun_support_eq]
State after:
case mpr.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ↥(Finsupp.supported R R s)
hl : ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
⊢ ↑(↑l).support ⊆ s

State before:
case mpr.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ↥(Finsupp.supported R R s)
hl : ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
⊢ ↑(↑l).support ⊆ s
Tactic:
exact l.2
State after:
no goals

State before:
case mp
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s →
    ∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
Tactic:
rintro ⟨⟨l, rfl, hl⟩, hsupp⟩
State after:
case mp.intro.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ι →₀ R
hl : ∀ y ∈ U, (Finsupp.total ι R R y) l = 0
hsupp : support ⇑l ⊆ s
⊢ ∃ l_1, ⇑↑l_1 = ⇑l ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l_1 = 0

State before:
case mp.intro.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ι →₀ R
hl : ∀ y ∈ U, (Finsupp.total ι R R y) l = 0
hsupp : support ⇑l ⊆ s
⊢ ∃ l_1, ⇑↑l_1 = ⇑l ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l_1 = 0
Tactic:
exact ⟨⟨l, by simpa using hsupp⟩, by simpa⟩
State after:
no goals

State before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ι →₀ R
hl : ∀ y ∈ U, (Finsupp.total ι R R y) l = 0
hsupp : support ⇑l ⊆ s
⊢ l ∈ Finsupp.supported R R s
Tactic:
simpa using hsupp
State after:
no goals

State before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ι →₀ R
hl : ∀ y ∈ U, (Finsupp.total ι R R y) l = 0
hsupp : support ⇑l ⊆ s
⊢ ⇑↑⟨l, ⋯⟩ = ⇑l ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑⟨l, ⋯⟩ = 0
Tactic:
simpa
State after:
no goals