Theorem: orthSpace_eq (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 η
U : Submodule R (η → R)
⊢ U.orthSpace = map (Module.piEquiv η R R).symm U.dualAnnihilator
Tactic:
ext x
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 η
U : Submodule R (η → R)
x : η → R
⊢ x ∈ U.orthSpace ↔ x ∈ map (Module.piEquiv η R R).symm U.dualAnnihilator

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 η
U : Submodule R (η → R)
x : η → R
⊢ x ∈ U.orthSpace ↔ x ∈ map (Module.piEquiv η R R).symm U.dualAnnihilator
Tactic:
simp only [mem_orthSpace_iff', mem_map, mem_dualAnnihilator]
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 η
U : Submodule R (η → R)
x : η → R
⊢ (∀ y ∈ U, ∑ i : η, x i * y i = 0) ↔ ∃ y, (∀ w ∈ U, y w = 0) ∧ (Module.piEquiv η R R).symm y = 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 η
U : Submodule R (η → R)
x : η → R
⊢ (∀ y ∈ U, ∑ i : η, x i * y i = 0) ↔ ∃ y, (∀ w ∈ U, y w = 0) ∧ (Module.piEquiv η R R).symm y = x
Tactic:
refine ⟨fun h ↦ ⟨Module.piEquiv η R R x, ?_, by simp⟩, fun h ↦ ?_⟩
State after:
case h.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 η
U : Submodule R (η → R)
x : η → R
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
⊢ ∀ w ∈ U, ((Module.piEquiv η R R) x) w = 0

case h.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 η
U : Submodule R (η → R)
x : η → R
h : ∃ y, (∀ w ∈ U, y w = 0) ∧ (Module.piEquiv η R R).symm y = x
⊢ ∀ y ∈ U, ∑ i : η, x i * y i = 0

State before:
case h.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 η
U : Submodule R (η → R)
x : η → R
h : ∃ y, (∀ w ∈ U, y w = 0) ∧ (Module.piEquiv η R R).symm y = x
⊢ ∀ y ∈ U, ∑ i : η, x i * y i = 0
Tactic:
obtain ⟨w, h, rfl⟩ := h
State after:
case h.refine_2.intro.intro
α : 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 η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
⊢ ∀ y ∈ U, ∑ i : η, (Module.piEquiv η R R).symm w i * y i = 0

State before:
case h.refine_2.intro.intro
α : 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 η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
⊢ ∀ y ∈ U, ∑ i : η, (Module.piEquiv η R R).symm w i * y i = 0
Tactic:
intro y hy
State after:
case h.refine_2.intro.intro
α : 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 η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ i : η, (Module.piEquiv η R R).symm w i * y i = 0

State before:
case h.refine_2.intro.intro
α : 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 η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ i : η, (Module.piEquiv η R R).symm w i * y i = 0
Tactic:
convert h y hy 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 η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ i : η, (Module.piEquiv η R R).symm w i * y i = w y

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 η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ i : η, (Module.piEquiv η R R).symm w i * y i = w y
Tactic:
simp [Module.piEquiv_apply_symm]
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 η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = w y

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 η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = w y
Tactic:
convert DFunLike.congr_fun ((Pi.basisFun R η).sum_dual_apply_smul_coord w) y 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 η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = (∑ x : η, w ((Pi.basisFun R η) x) • (Pi.basisFun R η).coord x) y

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 η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = (∑ x : η, w ((Pi.basisFun R η) x) • (Pi.basisFun R η).coord x) y
Tactic:
simp only [Pi.basisFun_apply, LinearMap.coeFn_sum, Finset.sum_apply, LinearMap.smul_apply,
  Basis.coord_apply, Pi.basisFun_repr, smul_eq_mul]
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 η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = ∑ x : η, w ((LinearMap.stdBasis R (fun x => R) x) 1) * 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
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = ∑ x : η, w ((LinearMap.stdBasis R (fun x => R) x) 1) * y x
Tactic:
rfl
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 η
U : Submodule R (η → R)
x : η → R
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
⊢ (Module.piEquiv η R R).symm ((Module.piEquiv η R R) x) = x
Tactic:
simp
State after:
no goals

State before:
case h.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 η
U : Submodule R (η → R)
x : η → R
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
⊢ ∀ w ∈ U, ((Module.piEquiv η R R) x) w = 0
Tactic:
simpa [Module.piEquiv_apply_apply, h, mul_comm]
State after:
no goals