Theorem: Set.Finite.relOrthSpace_relOrthSpace (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 ι
hs : s.Finite
U : Submodule K (ι → K)
hU : U ≤ s.supportedFun K
⊢ s.relOrthSpace (s.relOrthSpace U) = U
Tactic:
set U' : {U : Submodule K (ι → K) // U ≤ s.supportedFun K} := ⟨U,hU⟩
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 ι
hs : s.Finite
U : Submodule K (ι → K)
hU : U ≤ s.supportedFun K
U' : { U // U ≤ s.supportedFun K } := ⟨U, hU⟩
⊢ s.relOrthSpace (s.relOrthSpace U) = U

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 ι
hs : s.Finite
U : Submodule K (ι → K)
hU : U ≤ s.supportedFun K
U' : { U // U ≤ s.supportedFun K } := ⟨U, hU⟩
⊢ s.relOrthSpace (s.relOrthSpace U) = U
Tactic:
have := hs.fintype
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 ι
hs : s.Finite
U : Submodule K (ι → K)
hU : U ≤ s.supportedFun K
U' : { U // U ≤ s.supportedFun K } := ⟨U, hU⟩
this : Fintype ↑s
⊢ s.relOrthSpace (s.relOrthSpace U) = U

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 ι
hs : s.Finite
U : Submodule K (ι → K)
hU : U ≤ s.supportedFun K
U' : { U // U ≤ s.supportedFun K } := ⟨U, hU⟩
this : Fintype ↑s
⊢ s.relOrthSpace (s.relOrthSpace U) = U
Tactic:
rw [(show U = U' from rfl), ← Subtype.val_inj.2 <| (s.subtypeFunEquiv K).apply_symm_apply U',
  s.relOrthSpace_subtypeFunEquiv, s.relOrthSpace_subtypeFunEquiv, orthSpace_orthSpace]
State after:
no goals