Theorem: mem_orthSpace_iff' (Matroid/ForMathlib/LinearAlgebra/StdBasis.lean)

State before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
⊢ x ∈ U.orthSpace ↔ ∀ y ∈ U, ∑ i : η, x i * y i = 0
Tactic:
simp only [orthSpace, orthSpace', mem_map, mem_comap, Finsupp.toDualLin_coe, mem_dualAnnihilator,
  Finsupp.toDual_apply, Finsupp.total_apply, Finsupp.sum, smul_eq_mul]
State after:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
⊢ (∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x) ↔ ∀ y ∈ U, ∑ i : η, x i * y i = 0

State before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
⊢ (∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x) ↔ ∀ y ∈ U, ∑ i : η, x i * y i = 0
Tactic:
refine ⟨fun h y hyU ↦ ?_, fun h ↦ ?_⟩
State after:
case refine_1
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x
y : η → R
hyU : y ∈ U
⊢ ∑ i : η, x i * y i = 0

case refine_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
⊢ ∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x

State before:
case refine_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
⊢ ∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x
Tactic:
refine ⟨Finsupp.equivFunOnFinite.2 x, fun w hw ↦ ?_, by ext; simp⟩
State after:
case refine_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ (Finsupp.equivFunOnFinite.invFun x).support, (Finsupp.equivFunOnFinite.invFun x) x_1 * w x_1 = 0

State before:
case refine_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ (Finsupp.equivFunOnFinite.invFun x).support, (Finsupp.equivFunOnFinite.invFun x) x_1 * w x_1 = 0
Tactic:
convert h w hw using 1
State after:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ (Finsupp.equivFunOnFinite.invFun x).support, (Finsupp.equivFunOnFinite.invFun x) x_1 * w x_1 =
    ∑ i : η, x i * w i

State before:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ (Finsupp.equivFunOnFinite.invFun x).support, (Finsupp.equivFunOnFinite.invFun x) x_1 * w x_1 =
    ∑ i : η, x i * w i
Tactic:
simp only [Equiv.invFun_as_coe, Finsupp.equivFunOnFinite_symm_apply_support,
  Finite.toFinset_setOf, ne_eq, Finset.mem_univ, forall_true_left, not_not,
  Finsupp.equivFunOnFinite_symm_apply_toFun]
State after:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ Finset.filter (fun x_1 => ¬x x_1 = 0) Finset.univ, x x_1 * w x_1 = ∑ i : η, x i * w i

State before:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ Finset.filter (fun x_1 => ¬x x_1 = 0) Finset.univ, x x_1 * w x_1 = ∑ i : η, x i * w i
Tactic:
apply Finset.sum_subset (Finset.subset_univ _)
State after:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∀ x_1 ∈ Finset.univ, x_1 ∉ Finset.filter (fun x_2 => ¬x x_2 = 0) Finset.univ → x x_1 * w x_1 = 0

State before:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∀ x_1 ∈ Finset.univ, x_1 ∉ Finset.filter (fun x_2 => ¬x x_2 = 0) Finset.univ → x x_1 * w x_1 = 0
Tactic:
simp only [Finset.mem_univ, forall_true_left, not_not, Finset.mem_filter, true_and]
State after:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∀ (x_1 : η), x x_1 = 0 → x x_1 * w x_1 = 0

State before:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∀ (x_1 : η), x x_1 = 0 → x x_1 * w x_1 = 0
Tactic:
exact fun x hx ↦ by simp [hx]
State after:
no goals

State before:
case refine_1
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x
y : η → R
hyU : y ∈ U
⊢ ∑ i : η, x i * y i = 0
Tactic:
obtain ⟨c, hc, rfl⟩ := h
State after:
case refine_1.intro.intro
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ i : η, Finsupp.lcoeFun c i * y i = 0

State before:
case refine_1.intro.intro
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ i : η, Finsupp.lcoeFun c i * y i = 0
Tactic:
simp only [Finsupp.lcoeFun_apply]
State after:
case refine_1.intro.intro
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ x : η, c x * y x = 0

State before:
case refine_1.intro.intro
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ x : η, c x * y x = 0
Tactic:
convert hc y hyU using 1
State after:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ x : η, c x * y x = ∑ x ∈ c.support, c x * y x

State before:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ x : η, c x * y x = ∑ x ∈ c.support, c x * y x
Tactic:
rw [eq_comm, Finset.sum_subset (Finset.subset_univ _)]
State after:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∀ x ∈ Finset.univ, x ∉ c.support → c x * y x = 0

State before:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∀ x ∈ Finset.univ, x ∉ c.support → c x * y x = 0
Tactic:
simp only [Finset.mem_univ, Finsupp.mem_support_iff, ne_eq, not_not, forall_true_left]
State after:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∀ (x : η), c x = 0 → c x * y x = 0

State before:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∀ (x : η), c x = 0 → c x * y x = 0
Tactic:
exact fun x hx ↦ by simp [hx]
State after:
no goals

State before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
x : η
hx : c x = 0
⊢ c x * y x = 0
Tactic:
simp [hx]
State after:
no goals

State before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
⊢ Finsupp.lcoeFun (Finsupp.equivFunOnFinite.invFun x) = x
Tactic:
ext
State after:
case h
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
x✝ : η
⊢ Finsupp.lcoeFun (Finsupp.equivFunOnFinite.invFun x) x✝ = x x✝

State before:
case h
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
x✝ : η
⊢ Finsupp.lcoeFun (Finsupp.equivFunOnFinite.invFun x) x✝ = x x✝
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x✝ : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x✝ i * y i = 0
w : η → R
hw : w ∈ U
x : η
hx : x✝ x = 0
⊢ x✝ x * w x = 0
Tactic:
simp [hx]
State after:
no goals