Theorem: Set.supportedFunEquiv_apply_symm (Matroid/ForMathlib/LinearAlgebra/StdBasis.lean)

State before:
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : ↥(s.supportedFun R)
⊢ (s.supportedFunEquiv R).symm x = (LinearMap.funSubtype R s) ↑x
Tactic:
classical
obtain ⟨x, hx⟩ := x
rw [(s.supportedFunEquiv R).symm_apply_eq]
ext i
simp only [supportedFunEquiv_apply, LinearMap.extendSubtype_eq_ite, LinearMap.fun_Subtype_apply,
  dite_eq_ite]
rw [eq_comm, ite_eq_left_iff, not_imp_comm, eq_comm]
rw [mem_supportedFun_iff, support_subset_iff] at hx
apply hx
State after:
no goals

State before:
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : ↥(s.supportedFun R)
⊢ (s.supportedFunEquiv R).symm x = (LinearMap.funSubtype R s) ↑x
Tactic:
obtain ⟨x, hx⟩ := x
State after:
case mk
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
⊢ (s.supportedFunEquiv R).symm ⟨x, hx⟩ = (LinearMap.funSubtype R s) ↑⟨x, hx⟩

State before:
case mk
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
⊢ (s.supportedFunEquiv R).symm ⟨x, hx⟩ = (LinearMap.funSubtype R s) ↑⟨x, hx⟩
Tactic:
rw [(s.supportedFunEquiv R).symm_apply_eq]
State after:
case mk
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
⊢ ⟨x, hx⟩ = (s.supportedFunEquiv R) ((LinearMap.funSubtype R s) ↑⟨x, hx⟩)

State before:
case mk
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
⊢ ⟨x, hx⟩ = (s.supportedFunEquiv R) ((LinearMap.funSubtype R s) ↑⟨x, hx⟩)
Tactic:
ext i
State after:
case mk.a.h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ ↑⟨x, hx⟩ i = ↑((s.supportedFunEquiv R) ((LinearMap.funSubtype R s) ↑⟨x, hx⟩)) i

State before:
case mk.a.h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ ↑⟨x, hx⟩ i = ↑((s.supportedFunEquiv R) ((LinearMap.funSubtype R s) ↑⟨x, hx⟩)) i
Tactic:
simp only [supportedFunEquiv_apply, LinearMap.extendSubtype_eq_ite, LinearMap.fun_Subtype_apply,
  dite_eq_ite]
State after:
case mk.a.h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ x i = if i ∈ s then x i else 0

State before:
case mk.a.h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ x i = if i ∈ s then x i else 0
Tactic:
rw [eq_comm, ite_eq_left_iff, not_imp_comm, eq_comm]
State after:
case mk.a.h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ ¬x i = 0 → i ∈ s

State before:
case mk.a.h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ ¬x i = 0 → i ∈ s
Tactic:
rw [mem_supportedFun_iff, support_subset_iff] at hx
State after:
case mk.a.h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
i : η
⊢ ¬x i = 0 → i ∈ s

State before:
case mk.a.h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι : Type u_4
R✝ : Type u_5
η : Type u_6
inst✝¹ : Semiring R✝
s✝ : Set η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
i : η
⊢ ¬x i = 0 → i ∈ s
Tactic:
apply hx
State after:
no goals