Theorem: mem_supportedFun_iff (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
⊢ x ∈ s.supportedFun R ↔ support x ⊆ s
Tactic:
simp only [supportedFun, LinearMap.mem_range, ne_eq]
State after:
α : 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
⊢ (∃ y, (LinearMap.extendSubtype R s) y = x) ↔ support x ⊆ s

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
⊢ (∃ y, (LinearMap.extendSubtype R s) y = x) ↔ support x ⊆ s
Tactic:
refine ⟨?_, fun h ↦ ?_⟩
State after:
case refine_1
α : 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
⊢ (∃ y, (LinearMap.extendSubtype R s) y = x) → support x ⊆ s

case refine_2
α : 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
h : support x ⊆ s
⊢ ∃ y, (LinearMap.extendSubtype R s) y = x

State before:
case refine_2
α : 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
h : support x ⊆ s
⊢ ∃ y, (LinearMap.extendSubtype R s) y = x
Tactic:
exact ⟨LinearMap.funSubtype R s x, LinearMap.extendSubtype_funSubtype_apply h⟩
State after:
no goals

State before:
case refine_1
α : 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
⊢ (∃ y, (LinearMap.extendSubtype R s) y = x) → support x ⊆ s
Tactic:
rintro ⟨y, rfl⟩ i hi
State after:
case refine_1.intro
α : 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 η
y : ↑s → R
i : η
hi : i ∈ support ((LinearMap.extendSubtype R s) y)
⊢ i ∈ s

State before:
case refine_1.intro
α : 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 η
y : ↑s → R
i : η
hi : i ∈ support ((LinearMap.extendSubtype R s) y)
⊢ i ∈ s
Tactic:
simp only [mem_support, ne_eq, LinearMap.extendSubtype_eq_ite, dite_eq_right_iff,
  not_forall] at hi
State after:
case refine_1.intro
α : 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 η
y : ↑s → R
i : η
hi : ∃ (x : i ∈ s), ¬y ⟨i, x⟩ = 0
⊢ i ∈ s

State before:
case refine_1.intro
α : 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 η
y : ↑s → R
i : η
hi : ∃ (x : i ∈ s), ¬y ⟨i, x⟩ = 0
⊢ i ∈ s
Tactic:
obtain ⟨h,-⟩ := hi
State after:
case refine_1.intro.intro
α : 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 η
y : ↑s → R
i : η
h : i ∈ s
⊢ i ∈ s

State before:
case refine_1.intro.intro
α : 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 η
y : ↑s → R
i : η
h : i ∈ s
⊢ i ∈ s
Tactic:
exact h
State after:
no goals