Theorem: eq_orthSpace_comm (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 : Subspace K (η → K)
h : U = orthSpace V
⊢ V = orthSpace U
Tactic:
rw [h, orthSpace_orthSpace]
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)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U V : Subspace K (η → K)
h : V = orthSpace U
⊢ U = orthSpace V
Tactic:
rw [h, orthSpace_orthSpace]
State after:
no goals