Theorem: LinearMap.extendSubtype_funSubtype_apply (Matroid/ForMathlib/LinearAlgebra/StdBasis.lean)

State before:
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
⊢ (extendSubtype R s) ((funSubtype R s) x) = x
Tactic:
classical
ext i
simp only [extendSubtype_eq_ite, fun_Subtype_apply, dite_eq_ite, ite_eq_left_iff]
exact fun his ↦ Eq.symm <| by simpa using mt (support_subset_iff.1 hx i) his
State after:
no goals

State before:
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
⊢ (extendSubtype R s) ((funSubtype R s) x) = x
Tactic:
ext i
State after:
case h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
i : η
⊢ (extendSubtype R s) ((funSubtype R s) x) i = x i

State before:
case h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
i : η
⊢ (extendSubtype R s) ((funSubtype R s) x) i = x i
Tactic:
simp only [extendSubtype_eq_ite, fun_Subtype_apply, dite_eq_ite, ite_eq_left_iff]
State after:
case h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
i : η
⊢ i ∉ s → 0 = x i

State before:
case h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
i : η
⊢ i ∉ s → 0 = x i
Tactic:
exact fun his ↦ Eq.symm <| by simpa using mt (support_subset_iff.1 hx i) his
State after:
no goals

State before:
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
i : η
his : i ∉ s
⊢ x i = 0
Tactic:
simpa using mt (support_subset_iff.1 hx i) his
State after:
no goals