Theorem: Set.mem_subtypeFunEquiv_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
U : Submodule R (↑s → R)
⊢ x ∈ ↑((s.subtypeFunEquiv R) U) ↔ support x ⊆ s ∧ s.restrict x ∈ U
Tactic:
change (x ∈ (MapSubtype.relIso _ _).1 ↔ _)
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
U : Submodule R (↑s → R)
⊢ x ∈
      ↑((MapSubtype.relIso (LinearMap.range (LinearMap.extendSubtype R s)))
          ((orderIsoMapComap (LinearEquiv.ofInjective (LinearMap.extendSubtype R s) ⋯)).toEquiv U)) ↔
    support x ⊆ s ∧ s.restrict x ∈ U

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
U : Submodule R (↑s → R)
⊢ x ∈
      ↑((MapSubtype.relIso (LinearMap.range (LinearMap.extendSubtype R s)))
          ((orderIsoMapComap (LinearEquiv.ofInjective (LinearMap.extendSubtype R s) ⋯)).toEquiv U)) ↔
    support x ⊆ s ∧ s.restrict x ∈ U
Tactic:
simp only [RelIso.coe_fn_toEquiv, orderIsoMapComap_apply, MapSubtype.relIso_apply, mem_map,
  coeSubtype, exists_exists_and_eq_and, LinearEquiv.ofInjective_apply, support_subset_iff,
  LinearMap.extendSubtype_eq_ite]
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
U : Submodule R (↑s → R)
⊢ (∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = x) ↔ (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U

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
U : Submodule R (↑s → R)
⊢ (∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = x) ↔ (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
Tactic:
refine ⟨?_, fun ⟨hxs, hxU⟩ ↦ ?_⟩
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
U : Submodule R (↑s → R)
⊢ (∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = x) → (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U

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
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
⊢ ∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = 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
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
⊢ ∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = x
Tactic:
refine ⟨_, hxU, ?_⟩
State after:
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
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
⊢ (fun i => if h : i ∈ s then s.restrict x ⟨i, h⟩ else 0) = 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
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
⊢ (fun i => if h : i ∈ s then s.restrict x ⟨i, h⟩ else 0) = x
Tactic:
ext i
State after:
case refine_2.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
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ (if h : i ∈ s then s.restrict x ⟨i, h⟩ else 0) = x i

State before:
case refine_2.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
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ (if h : i ∈ s then s.restrict x ⟨i, h⟩ else 0) = x i
Tactic:
simp_rw [restrict_apply, dite_eq_ite, ite_eq_left_iff, eq_comm (b := x i)]
State after:
case refine_2.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
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ i ∉ s → x i = 0

State before:
case refine_2.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
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ i ∉ s → x i = 0
Tactic:
rw [not_imp_comm]
State after:
case refine_2.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
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ ¬x i = 0 → i ∈ s

State before:
case refine_2.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
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ ¬x i = 0 → i ∈ s
Tactic:
apply hxs
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
U : Submodule R (↑s → R)
⊢ (∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = x) → (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
Tactic:
rintro ⟨a, ha, rfl⟩
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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (∀ (x : η), (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x ≠ 0 → x ∈ s) ∧
    (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) ∈ U

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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (∀ (x : η), (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x ≠ 0 → x ∈ s) ∧
    (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) ∈ U
Tactic:
constructor
State after:
case refine_1.intro.intro.left
α : 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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ ∀ (x : η), (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x ≠ 0 → x ∈ s

case refine_1.intro.intro.right
α : 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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) ∈ U

State before:
case refine_1.intro.intro.right
α : 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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) ∈ U
Tactic:
convert ha
State after:
case h.e'_4
α : 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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = a

State before:
case h.e'_4
α : 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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = a
Tactic:
ext
State after:
case h.e'_4.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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
x✝ : ↑s
⊢ s.restrict (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x✝ = a x✝

State before:
case h.e'_4.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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
x✝ : ↑s
⊢ s.restrict (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x✝ = a x✝
Tactic:
simp
State after:
no goals

State before:
case refine_1.intro.intro.left
α : 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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ ∀ (x : η), (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x ≠ 0 → x ∈ s
Tactic:
simp only [ne_eq, dite_eq_right_iff, not_forall, forall_exists_index]
State after:
case refine_1.intro.intro.left
α : 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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ ∀ (x : η) (x_1 : x ∈ s), ¬a ⟨x, x_1⟩ = 0 → x ∈ s

State before:
case refine_1.intro.intro.left
α : 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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ ∀ (x : η) (x_1 : x ∈ s), ¬a ⟨x, x_1⟩ = 0 → x ∈ s
Tactic:
exact fun i hi _ ↦ hi
State after:
no goals