Theorem: LinearMap.extendSubtype_support_subset (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 α
x : ↑s → R
⊢ support ((extendSubtype R s) x) ⊆ s
Tactic:
classical
refine fun i (hi : _ ≠ 0) ↦ by_contra fun his ↦ ?_
simp_rw [LinearMap.extendSubtype_eq_ite, dif_neg his] at hi
exact hi rfl
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 α
x : ↑s → R
⊢ support ((extendSubtype R s) x) ⊆ s
Tactic:
refine fun i (hi : _ ≠ 0) ↦ by_contra fun his ↦ ?_
State after:
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
i : α
hi : (extendSubtype R s) x i ≠ 0
his : i ∉ s
⊢ False

State before:
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
i : α
hi : (extendSubtype R s) x i ≠ 0
his : i ∉ s
⊢ False
Tactic:
simp_rw [LinearMap.extendSubtype_eq_ite, dif_neg his] at hi
State after:
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
i : α
his : i ∉ s
hi : 0 ≠ 0
⊢ False

State before:
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
i : α
his : i ∉ s
hi : 0 ≠ 0
⊢ False
Tactic:
exact hi rfl
State after:
no goals