internlm/Lean-Github huggingface dataset:
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
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
Tactic:
have := Set.not_mem_of_mem_diff 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
this : y ∉ I
⊢ M.relRank I (Set.insert y I) ≤ 0
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
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
this : y ∉ I
⊢ M.relRank I (Set.insert y I) ≤ 0
Tactic:
have : Set.insert y I \ {y} = I := Set.insert_diff_self_of_not_mem this
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
this✝ : y ∉ I
this : Set.insert y I \ {y} = I
⊢ M.relRank I (Set.insert y I) ≤ 0
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
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
this✝ : y ∉ I
this : Set.insert y I \ {y} = I
⊢ M.relRank I (Set.insert y I) ≤ 0
Tactic:
rwa [this] at hr
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
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 \ {y}) (Set.insert x I) ≤ 1
Tactic:
set C := (Set.insert x I)
Proof state after:
α : 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
⊢ M.relRank (I \ {y}) C ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
⊢ M.relRank (I \ {y}) C ≤ 1
Tactic:
set B := (Set.insert x I \ {y})
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
⊢ M.relRank (I \ {y}) C ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
⊢ M.relRank (I \ {y}) C ≤ 1
Tactic:
set A := (I \ {y})
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
⊢ M.relRank A C ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
⊢ M.relRank A C ≤ 1
Tactic:
have h₂ : B ⊆ C := @Set.diff_subset α (insert x I) {y}
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ M.relRank A C ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ M.relRank A C ≤ 1
Tactic:
have h₃ : A ⊆ B := by
  refine Set.diff_singleton_subset_iff.mpr ?_
  rw [Set.insert_diff_singleton]
  exact (Set.subset_insert x I).trans (Set.subset_insert y (Set.insert x I))
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
⊢ M.relRank A C ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
hrAB : M.relRank A B ≤ 1
⊢ M.relRank A C ≤ 1
Tactic:
have h : M.relRank A B + M.relRank B C <= 1 := by
  exact add_le_add hrAB hr
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
hrAB : M.relRank A B ≤ 1
h : M.relRank A B + M.relRank B C ≤ 1
⊢ M.relRank A C ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
hrAB : M.relRank A B ≤ 1
h : M.relRank A B + M.relRank B C ≤ 1
⊢ M.relRank A C ≤ 1
Tactic:
have := M.relRank_add_cancel h₃ h₂
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
hrAB : M.relRank A B ≤ 1
h : M.relRank A B + M.relRank B C ≤ 1
this : M.relRank A C = M.relRank A B + M.relRank B C
⊢ M.relRank A C ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
hrAB : M.relRank A B ≤ 1
h : M.relRank A B + M.relRank B C ≤ 1
this : M.relRank A C = M.relRank A B + M.relRank B C
⊢ M.relRank A C ≤ 1
Tactic:
rwa [<-this] at h
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ A ⊆ B
Tactic:
refine Set.diff_singleton_subset_iff.mpr ?_
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ I ⊆ insert y B
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ I ⊆ insert y B
Tactic:
rw [Set.insert_diff_singleton]
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ I ⊆ insert y (Set.insert x I)
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ I ⊆ insert y (Set.insert x I)
Tactic:
exact (Set.subset_insert x I).trans (Set.subset_insert y (Set.insert x I))
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
⊢ M.relRank A B ≤ 1
Tactic:
have h := M.relRank_le_encard_diff A B
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h : M.relRank A B ≤ (B \ A).encard
⊢ M.relRank A B ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h : M.relRank A B ≤ (B \ A).encard
⊢ M.relRank A B ≤ 1
Tactic:
rw [Set.diff_diff_right] at h
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
⊢ M.relRank A B ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
⊢ M.relRank A B ≤ 1
Tactic:
have h := h.trans (Set.encard_union_le (B \ I) (B ∩ {y}))
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard + (B ∩ {y}).encard
⊢ M.relRank A B ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard + (B ∩ {y}).encard
⊢ M.relRank A B ≤ 1
Tactic:
rw [Set.encard_eq_zero.mpr Set.diff_inter_self] at h
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard + 0
⊢ M.relRank A B ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard + 0
⊢ M.relRank A B ≤ 1
Tactic:
simp only [add_zero] at h
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ M.relRank A B ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ M.relRank A B ≤ 1
Tactic:
have : B \ I ⊆ {x} := by refine Set.diff_subset_iff.mpr ?_; simp only [Set.union_singleton]; exact h₂
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
this : B \ I ⊆ {x}
⊢ M.relRank A B ≤ 1
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
this : B \ I ⊆ {x}
⊢ M.relRank A B ≤ 1
Tactic:
rcases Set.subset_singleton_iff_eq.mp this with h' | h'
Proof state after:
case inl
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
this : B \ I ⊆ {x}
h' : B \ I = ∅
⊢ M.relRank A B ≤ 1

case inr
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
this : B \ I ⊆ {x}
h' : B \ I = {x}
⊢ M.relRank A B ≤ 1
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case inr
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
this : B \ I ⊆ {x}
h' : B \ I = {x}
⊢ M.relRank A B ≤ 1
Tactic:
rw [h'] at h
Proof state after:
case inr
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ {x}.encard
this : B \ I ⊆ {x}
h' : B \ I = {x}
⊢ M.relRank A B ≤ 1
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case inr
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ {x}.encard
this : B \ I ⊆ {x}
h' : B \ I = {x}
⊢ M.relRank A B ≤ 1
Tactic:
rwa [Set.encard_singleton] at h
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ B \ I ⊆ {x}
Tactic:
refine Set.diff_subset_iff.mpr ?_
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ B ⊆ I ∪ {x}
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ B ⊆ I ∪ {x}
Tactic:
simp only [Set.union_singleton]
Proof state after:
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ B ⊆ insert x I
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ B ⊆ insert x I
Tactic:
exact h₂
Proof state after:
no goals
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case inl
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
this : B \ I ⊆ {x}
h' : B \ I = ∅
⊢ M.relRank A B ≤ 1
Tactic:
rw [h'] at h
Proof state after:
case inl
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ ∅.encard
this : B \ I ⊆ {x}
h' : B \ I = ∅
⊢ M.relRank A B ≤ 1
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case inl
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ ∅.encard
this : B \ I ⊆ {x}
h' : B \ I = ∅
⊢ M.relRank A B ≤ 1
Tactic:
rw [Set.encard_empty] at h
Proof state after:
case inl
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ 0
this : B \ I ⊆ {x}
h' : B \ I = ∅
⊢ M.relRank A B ≤ 1
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case inl
α : 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
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ 0
this : B \ I ⊆ {x}
h' : B \ I = ∅
⊢ M.relRank A B ≤ 1
Tactic:
exact h.trans zero_le_one
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
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
hrAB : M.relRank A B ≤ 1
⊢ M.relRank A B + M.relRank B C ≤ 1
Tactic:
exact add_le_add hrAB hr
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 α
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 A C = M.relRank A B + M.relRank B C
Tactic:
have h₂ : B ⊆ C := Set.subset_insert x I
Proof state after:
α : 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₂ : B ⊆ C
⊢ M.relRank A C = M.relRank A B + M.relRank B C
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
α : 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₂ : B ⊆ C
⊢ M.relRank A C = M.relRank A B + M.relRank B C
Tactic:
have h₃ : A ⊆ B := Set.diff_subset
Proof state after:
α : 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₂ : B ⊆ C
h₃ : A ⊆ B
⊢ M.relRank A C = M.relRank A B + M.relRank B C
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
α : 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₂ : B ⊆ C
h₃ : A ⊆ B
⊢ M.relRank A C = M.relRank A B + M.relRank B C
Tactic:
exact M.relRank_add_cancel h₃ h₂
Proof state after:
no goals