internlm/Lean-Github huggingface dataset:
Theorem: RankMatroid.indep_subset
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset
Proof 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]
Proof 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
Theorem: RankMatroid.indep_subset
Proof 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)
Proof state after:
no goals
Theorem: RankMatroid.indep_subset
Proof 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
Proof 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})
Theorem: RankMatroid.indep_subset
Proof 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 ↦ ?_⟩
Proof 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}
Theorem: RankMatroid.indep_subset
Proof 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
Proof 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}
Theorem: RankMatroid.indep_subset
Proof 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
Proof 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}
Theorem: RankMatroid.indep_subset
Proof 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⟩
Proof state after:
no goals
Theorem: RankMatroid.indep_subset
Proof 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 ?_⟩
Proof 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
Theorem: RankMatroid.indep_subset
Proof 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), ?_⟩
Proof 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
Theorem: RankMatroid.indep_subset
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset
Proof 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
Proof state after:
no goals
Theorem: RankMatroid.indep_subset
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset
Proof 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
Proof state after:
no goals
Theorem: RankMatroid.relRank_mono_left
Proof state before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hBX : B ⊆ X
hAB : A ⊆ B
⊢ M.relRank B X ≤ M.relRank A X
Tactic:
rw [M.relRank_add_cancel hAB hBX]
Proof state after:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hBX : B ⊆ X
hAB : A ⊆ B
⊢ M.relRank B X ≤ M.relRank A B + M.relRank B X
Theorem: RankMatroid.relRank_mono_left
Proof state before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hBX : B ⊆ X
hAB : A ⊆ B
⊢ M.relRank B X ≤ M.relRank A B + M.relRank B X
Tactic:
simp only [self_le_add_left]
Proof state after:
no goals
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
⊢ M.Indep (Set.insert x I) ↔ M.relRank I (Set.insert x I) > 0
Tactic:
refine ⟨fun hIx_indep ↦ ?_, fun hr ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
⊢ M.relRank I (Set.insert x I) > 0

case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ M.Indep (Set.insert x I)
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ M.Indep (Set.insert x I)
Tactic:
refine M.indep_iff'.mpr ?_
Proof state after:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ Set.insert x I ⊆ M.E ∧ ∀ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) > 0
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ Set.insert x I ⊆ M.E ∧ ∀ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) > 0
Tactic:
refine ⟨Set.insert_subset (Set.mem_of_mem_diff hx) hI_indep.subset_ground, ?_⟩
Proof state after:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ ∀ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) > 0
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ ∀ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) > 0
Tactic:
contrapose! hr
Proof state after:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : ∃ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) ≤ 0
⊢ M.relRank I (Set.insert x I) ≤ 0
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : ∃ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) ≤ 0
⊢ M.relRank I (Set.insert x I) ≤ 0
Tactic:
rcases hr with ⟨y, hy, hr⟩
Proof state after:
case refine_2.intro.intro
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
⊢ M.relRank I (Set.insert x I) ≤ 0
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case refine_2.intro.intro
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
⊢ M.relRank I (Set.insert x I) ≤ 0
Tactic:
by_cases hxy : x = y
Proof state after:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
hxy : x = y
⊢ M.relRank I (Set.insert x I) ≤ 0

case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
hxy : ¬x = y
⊢ M.relRank I (Set.insert x I) ≤ 0
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
hxy : ¬x = y
h : M.relRank (I \ {y}) (Set.insert x I) ≤ 1
⊢ M.relRank I (Set.insert x I) ≤ 0
Tactic:
set C := (Set.insert x I)
Proof state after:
case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
h : M.relRank (I \ {y}) C ≤ 1
⊢ M.relRank I C ≤ 0
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
h : M.relRank (I \ {y}) C ≤ 1
⊢ M.relRank I C ≤ 0
Tactic:
set B := (I)
Proof state after:
case neg
α : Type u_1
A B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
h : M.relRank (B \ {y}) C ≤ 1
⊢ M.relRank B C ≤ 0
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case neg
α : Type u_1
A B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
h : M.relRank (B \ {y}) C ≤ 1
⊢ M.relRank B C ≤ 0
Tactic:
set A := (I \ {y})
Proof state after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
⊢ M.relRank B C ≤ 0
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
⊢ M.relRank B C ≤ 0
Tactic:
have h' : M.relRank A C = M.relRank A B + M.relRank B C := by
  have h₂ : B ⊆ C := Set.subset_insert x I
  have h₃ : A ⊆ B := Set.diff_subset
  exact M.relRank_add_cancel h₃ h₂
Proof state after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
⊢ M.relRank B C ≤ 0
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
⊢ M.relRank B C ≤ 0
Tactic:
contrapose! h
Proof state after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h : 0 < M.relRank B C
⊢ 1 < M.relRank A C
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h : 0 < M.relRank B C
⊢ 1 < M.relRank A C
Tactic:
rw [h']
Proof state after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h : 0 < M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h : 0 < M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Tactic:
have h := ENat.add_one_le_of_lt h
Proof state after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 0 + 1 ≤ M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 0 + 1 ≤ M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Tactic:
simp only [zero_add] at h
Proof state after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Tactic:
have := add_le_add h'' h
Proof state after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
this : 1 + 1 ≤ M.relRank A B + M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
this : 1 + 1 ≤ M.relRank A B + M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Tactic:
rw [one_add_one_eq_two] at this
Proof state after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
this : 2 ≤ M.relRank A B + M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
this : 2 ≤ M.relRank A B + M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Tactic:
refine (ENat.add_one_le_iff ?refine_2.intro.intro.hm).mp this
Proof state after:
case refine_2.intro.intro.hm
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
this : 2 ≤ M.relRank A B + M.relRank B C
⊢ 1 ≠ ⊤
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case refine_2.intro.intro.hm
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
this : 2 ≤ M.relRank A B + M.relRank B C
⊢ 1 ≠ ⊤
Tactic:
exact ENat.coe_toNat_eq_self.mp rfl
Proof state after:
no goals
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
⊢ M.relRank I (Set.insert x I) > 0
Tactic:
have h := hIx_indep.indep x (Set.mem_insert x I)
Proof state after:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
h : M.relRank (Set.insert x I \ {x}) (Set.insert x I) > 0
⊢ M.relRank I (Set.insert x I) > 0
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
h : M.relRank (Set.insert x I \ {x}) (Set.insert x I) > 0
⊢ M.relRank I (Set.insert x I) > 0
Tactic:
have : Set.insert x I \ {x} = I :=
  Set.insert_diff_self_of_not_mem (Set.not_mem_of_mem_diff hx)
Proof state after:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
h : M.relRank (Set.insert x I \ {x}) (Set.insert x I) > 0
this : Set.insert x I \ {x} = I
⊢ M.relRank I (Set.insert x I) > 0
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
h : M.relRank (Set.insert x I \ {x}) (Set.insert x I) > 0
this : Set.insert x I \ {x} = I
⊢ M.relRank I (Set.insert x I) > 0
Tactic:
rwa [this] at h
Proof state after:
no goals
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
hxy : x = y
⊢ M.relRank I (Set.insert x I) ≤ 0
Tactic:
rw [hxy] at hr hx ⊢
Proof state after:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
y : α
hx : y ∈ M.E \ I
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert y I \ {y}) (Set.insert y I) ≤ 0
hxy : x = y
⊢ M.relRank I (Set.insert y I) ≤ 0