Theorem: orthSpace_orthSpace (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)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
⊢ (orthSpace U).orthSpace = U
Tactic:
refine (FiniteDimensional.eq_of_le_of_finrank_le (fun x hxU ↦ ?_) (le_of_eq ?_)).symm
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)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
x : η → K
hxU : x ∈ U
⊢ x ∈ (orthSpace U).orthSpace

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)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
⊢ FiniteDimensional.finrank K ↥(orthSpace U).orthSpace = FiniteDimensional.finrank K ↥U

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)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
⊢ FiniteDimensional.finrank K ↥(orthSpace U).orthSpace = FiniteDimensional.finrank K ↥U
Tactic:
rw [orthSpace_eq, orthSpace_eq, LinearEquiv.finrank_map_eq', LinearEquiv.dualAnnihilator_map_eq,
  LinearEquiv.finrank_map_eq', ← Subspace.finrank_dualCoannihilator_eq,
  Subspace.dualAnnihilator_dualCoannihilator_eq]
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)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
x : η → K
hxU : x ∈ U
⊢ x ∈ (orthSpace U).orthSpace
Tactic:
simp_rw [mem_orthSpace_iff']
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)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
x : η → K
hxU : x ∈ U
⊢ ∀ (y : η → K), (∀ y_1 ∈ U, ∑ i : η, y i * y_1 i = 0) → ∑ i : η, x i * y i = 0

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)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
x : η → K
hxU : x ∈ U
⊢ ∀ (y : η → K), (∀ y_1 ∈ U, ∑ i : η, y i * y_1 i = 0) → ∑ i : η, x i * y i = 0
Tactic:
intro y hy
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)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
x : η → K
hxU : x ∈ U
y : η → K
hy : ∀ y_1 ∈ U, ∑ i : η, y i * y_1 i = 0
⊢ ∑ i : η, x i * y i = 0

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)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
x : η → K
hxU : x ∈ U
y : η → K
hy : ∀ y_1 ∈ U, ∑ i : η, y i * y_1 i = 0
⊢ ∑ i : η, x i * y i = 0
Tactic:
simpa [mul_comm] using hy x hxU
State after:
no goals