Theorem: RankMatroid.indep_subset (Matroid/Constructions/RankAxioms.lean)

State before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hJ : M.Indep J
rIJ : I ⊆ J
⊢ M.Indep I
Tactic:
refine M.indep_iff'.mpr ⟨rIJ.trans hJ.subset_ground, fun x hx ↦ ?_⟩
State after:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hJ : M.Indep J
rIJ : I ⊆ J
x : α
hx : x ∈ I
⊢ M.relRank (I \ {x}) I > 0

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hJ : M.Indep J
rIJ : I ⊆ J
x : α
hx : x ∈ I
⊢ M.relRank (I \ {x}) I > 0
Tactic:
have hJ := hJ.relRank_pos_of_sub_mem (rIJ hx)
State after:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
rIJ : I ⊆ J
x : α
hx : x ∈ I
hJ : M.relRank (J \ {x}) J > 0
⊢ M.relRank (I \ {x}) I > 0

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
rIJ : I ⊆ J
x : α
hx : x ∈ I
hJ : M.relRank (J \ {x}) J > 0
⊢ M.relRank (I \ {x}) I > 0
Tactic:
set A := I
State after:
α : Type u_1
A✝ B I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
hJ : M.relRank (J \ {x}) J > 0
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
⊢ M.relRank (A \ {x}) A > 0

State before:
α : Type u_1
A✝ B I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
hJ : M.relRank (J \ {x}) J > 0
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
⊢ M.relRank (A \ {x}) A > 0
Tactic:
set B := J \ {x}
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
⊢ M.relRank (A \ {x}) A > 0

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
⊢ M.relRank (A \ {x}) A > 0
Tactic:
have hAUB : J = I ∪ (J \ {x}) :=
  (Set.union_diff_cancel' (Set.singleton_subset_iff.mpr hx) rIJ).symm
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
⊢ M.relRank (A \ {x}) A > 0

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
hAIB : I \ {x} = I ∩ (J \ {x})
⊢ M.relRank (A \ {x}) A > 0
Tactic:
rw [hAUB] at hJ
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B (I ∪ J \ {x}) > 0
hAUB : J = I ∪ J \ {x}
hAIB : I \ {x} = I ∩ (J \ {x})
⊢ M.relRank (A \ {x}) A > 0

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B (I ∪ J \ {x}) > 0
hAUB : J = I ∪ J \ {x}
hAIB : I \ {x} = I ∩ (J \ {x})
⊢ M.relRank (A \ {x}) A > 0
Tactic:
rw [hAIB]
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B (I ∪ J \ {x}) > 0
hAUB : J = I ∪ J \ {x}
hAIB : I \ {x} = I ∩ (J \ {x})
⊢ M.relRank (I ∩ (J \ {x})) A > 0

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B (I ∪ J \ {x}) > 0
hAUB : J = I ∪ J \ {x}
hAIB : I \ {x} = I ∩ (J \ {x})
⊢ M.relRank (I ∩ (J \ {x})) A > 0
Tactic:
exact hJ.trans_le (M.relRank_union_le_relRank_inter A B)
State after:
no goals

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
⊢ I \ {x} = I ∩ (J \ {x})
Tactic:
ext y
State after:
case h
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
⊢ y ∈ I \ {x} ↔ y ∈ I ∩ (J \ {x})

State before:
case h
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
⊢ y ∈ I \ {x} ↔ y ∈ I ∩ (J \ {x})
Tactic:
refine ⟨fun hY ↦ ?_, fun hY ↦ ?_⟩
State after:
case h.refine_1
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I \ {x}
⊢ y ∈ I ∩ (J \ {x})

case h.refine_2
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I ∩ (J \ {x})
⊢ y ∈ I \ {x}

State before:
case h.refine_2
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I ∩ (J \ {x})
⊢ y ∈ I \ {x}
Tactic:
have hyB : y ∈ J \ {x} := Set.mem_of_mem_inter_right hY
State after:
case h.refine_2
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I ∩ (J \ {x})
hyB : y ∈ J \ {x}
⊢ y ∈ I \ {x}

State before:
case h.refine_2
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I ∩ (J \ {x})
hyB : y ∈ J \ {x}
⊢ y ∈ I \ {x}
Tactic:
have hynex : y ≠ x := by have := Set.not_mem_of_mem_diff hyB; exact this
State after:
case h.refine_2
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I ∩ (J \ {x})
hyB : y ∈ J \ {x}
hynex : y ≠ x
⊢ y ∈ I \ {x}

State before:
case h.refine_2
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I ∩ (J \ {x})
hyB : y ∈ J \ {x}
hynex : y ≠ x
⊢ y ∈ I \ {x}
Tactic:
exact ⟨Set.mem_of_mem_inter_left hY, hynex⟩
State after:
no goals

State before:
case h.refine_1
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I \ {x}
⊢ y ∈ I ∩ (J \ {x})
Tactic:
refine ⟨Set.mem_of_mem_diff hY, Set.mem_diff_singleton.mpr ?_⟩
State after:
case h.refine_1
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I \ {x}
⊢ y ∈ J ∧ y ≠ x

State before:
case h.refine_1
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I \ {x}
⊢ y ∈ J ∧ y ≠ x
Tactic:
refine ⟨rIJ (Set.mem_of_mem_diff hY), ?_⟩
State after:
case h.refine_1
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I \ {x}
⊢ y ≠ x

State before:
case h.refine_1
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I \ {x}
⊢ y ≠ x
Tactic:
have h := Set.not_mem_of_mem_diff hY
State after:
case h.refine_1
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I \ {x}
h : y ∉ {x}
⊢ y ≠ x

State before:
case h.refine_1
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I \ {x}
h : y ∉ {x}
⊢ y ≠ x
Tactic:
exact h
State after:
no goals

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I ∩ (J \ {x})
hyB : y ∈ J \ {x}
⊢ y ≠ x
Tactic:
have := Set.not_mem_of_mem_diff hyB
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I ∩ (J \ {x})
hyB : y ∈ J \ {x}
this : y ∉ {x}
⊢ y ≠ x

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I ∩ (J \ {x})
hyB : y ∈ J \ {x}
this : y ∉ {x}
⊢ y ≠ x
Tactic:
exact this
State after:
no goals