internlm/Lean-Github huggingface dataset:
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof state before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this : M.relRank I (Set.insert x I) > 0
hx : x ∈ M.E
⊢ M.relRank I X > 0
Tactic:
rw [M.relRank_add_cancel (Set.subset_insert x I) (Set.insert_subset (hI' hxI') hI)]
Proof state after:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this : M.relRank I (Set.insert x I) > 0
hx : x ∈ M.E
⊢ M.relRank I (insert x I) + M.relRank (insert x I) X > 0
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof state before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this : M.relRank I (Set.insert x I) > 0
hx : x ∈ M.E
⊢ M.relRank I (insert x I) + M.relRank (insert x I) X > 0
Tactic:
exact Left.add_pos_of_pos_of_nonneg this (zero_le (M.relRank (Set.insert x I) X))
Proof state after:
no goals
Theorem: Matroid.basis_of_maximal_extension
Proof state before:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h : J ∈ maximals (fun x x_1 => x ⊆ x_1) {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X}
⊢ M.Basis J X
Tactic:
unfold Basis
Proof state after:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h : J ∈ maximals (fun x x_1 => x ⊆ x_1) {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X}
⊢ J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ X} ∧ X ⊆ M.E
Theorem: Matroid.basis_of_maximal_extension
Proof state before:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h : J ∈ maximals (fun x x_1 => x ⊆ x_1) {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X}
⊢ J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ X} ∧ X ⊆ M.E
Tactic:
unfold maximals at h ⊢
Proof state after:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h :
  J ∈
    {a |
      a ∈ {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X} ∧
        ∀ ⦃b : Set α⦄,
          b ∈ {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
⊢ J ∈
      {a |
        a ∈ {A | M.Indep A ∧ A ⊆ X} ∧
          ∀ ⦃b : Set α⦄, b ∈ {A | M.Indep A ∧ A ⊆ X} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a} ∧
    X ⊆ M.E
Theorem: Matroid.basis_of_maximal_extension
Proof state before:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h :
  J ∈
    {a |
      a ∈ {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X} ∧
        ∀ ⦃b : Set α⦄,
          b ∈ {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
⊢ J ∈
      {a |
        a ∈ {A | M.Indep A ∧ A ⊆ X} ∧
          ∀ ⦃b : Set α⦄, b ∈ {A | M.Indep A ∧ A ⊆ X} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a} ∧
    X ⊆ M.E
Tactic:
simp only [Set.mem_setOf_eq, and_imp] at h ⊢
Proof state after:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h : (M.Indep J ∧ I ⊆ J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
⊢ ((M.Indep J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J) ∧ X ⊆ M.E
Theorem: Matroid.basis_of_maximal_extension
Proof state before:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h : (M.Indep J ∧ I ⊆ J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
⊢ ((M.Indep J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J) ∧ X ⊆ M.E
Tactic:
obtain ⟨⟨hJ_indep, hIJ, hJX⟩, hJ_max⟩ := h
Proof state after:
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ ((M.Indep J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J) ∧ X ⊆ M.E
Theorem: Matroid.basis_of_maximal_extension
Proof state before:
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ ((M.Indep J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J) ∧ X ⊆ M.E
Tactic:
refine ⟨⟨⟨hJ_indep, hJX⟩, ?_⟩, hX⟩
Proof state after:
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J
Theorem: Matroid.basis_of_maximal_extension
Proof state before:
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J
Tactic:
intro J' hJ'_indep hJ'X hJJ'
Proof state after:
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
J' : Set α
hJ'_indep : M.Indep J'
hJ'X : J' ⊆ X
hJJ' : J ⊆ J'
⊢ J' ⊆ J
Theorem: Matroid.basis_of_maximal_extension
Proof state before:
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
J' : Set α
hJ'_indep : M.Indep J'
hJ'X : J' ⊆ X
hJJ' : J ⊆ J'
⊢ J' ⊆ J
Tactic:
exact hJ_max hJ'_indep (hIJ.trans hJJ') hJ'X hJJ'
Proof state after:
no goals
Theorem: Matroid.relRank_intro
Proof state before:
α : Type u_1
I : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Tactic:
obtain ⟨I, hI⟩ := M.maximality A (hA.trans hB) ∅ M.empty_indep (Set.empty_subset A)
Proof state after:
case intro
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : I ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ ∅ ⊆ Y ∧ Y ⊆ A}
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Theorem: Matroid.relRank_intro
Proof state before:
case intro
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : I ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ ∅ ⊆ Y ∧ Y ⊆ A}
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Tactic:
unfold maximals at hI
Proof state after:
case intro
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI :
  I ∈
    {a |
      a ∈ {Y | M.Indep Y ∧ ∅ ⊆ Y ∧ Y ⊆ A} ∧
        ∀ ⦃b : Set α⦄, b ∈ {Y | M.Indep Y ∧ ∅ ⊆ Y ∧ Y ⊆ A} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Theorem: Matroid.relRank_intro
Proof state before:
case intro
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI :
  I ∈
    {a |
      a ∈ {Y | M.Indep Y ∧ ∅ ⊆ Y ∧ Y ⊆ A} ∧
        ∀ ⦃b : Set α⦄, b ∈ {Y | M.Indep Y ∧ ∅ ⊆ Y ∧ Y ⊆ A} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Tactic:
simp only [Set.empty_subset, true_and, Set.mem_setOf_eq, and_imp] at hI
Proof state after:
case intro
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Theorem: Matroid.relRank_intro
Proof state before:
case intro
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Tactic:
have ⟨⟨hI_indep, hI_subset_A⟩, _⟩ := hI
Proof state after:
case intro
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Theorem: Matroid.relRank_intro
Proof state before:
case intro
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Tactic:
obtain ⟨J, hJ⟩ := M.maximality B hB I hI_indep (hI_subset_A.trans hA)
Proof state after:
case intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Theorem: Matroid.relRank_intro
Proof state before:
case intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Tactic:
use I
Proof state after:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
⊢ ∃ J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Theorem: Matroid.relRank_intro
Proof state before:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
⊢ ∃ J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Tactic:
use J
Proof state after:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
⊢ I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Theorem: Matroid.relRank_intro
Proof state before:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
⊢ I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
Tactic:
unfold Basis
Proof state after:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
⊢ I ⊆ J ∧
    (I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.Indep A_1 ∧ A_1 ⊆ A} ∧ A ⊆ M.E) ∧
      (J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ B} ∧ B ⊆ M.E) ∧ M.relRank A B = (J \ I).encard
Theorem: Matroid.relRank_intro
Proof state before:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
⊢ I ⊆ J ∧
    (I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.Indep A_1 ∧ A_1 ⊆ A} ∧ A ⊆ M.E) ∧
      (J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ B} ∧ B ⊆ M.E) ∧ M.relRank A B = (J \ I).encard
Tactic:
have hIJ : I ⊆ J := hJ.1.2.1
Proof state after:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
⊢ I ⊆ J ∧
    (I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.Indep A_1 ∧ A_1 ⊆ A} ∧ A ⊆ M.E) ∧
      (J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ B} ∧ B ⊆ M.E) ∧ M.relRank A B = (J \ I).encard
Theorem: Matroid.relRank_intro
Proof state before:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
⊢ I ⊆ J ∧
    (I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.Indep A_1 ∧ A_1 ⊆ A} ∧ A ⊆ M.E) ∧
      (J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ B} ∧ B ⊆ M.E) ∧ M.relRank A B = (J \ I).encard
Tactic:
have hI_basis : M.Basis I A := by
  refine @basis_of_maximal_extension α M ∅ A I (hA.trans hB) ?_
  unfold maximals; simp only [Set.empty_subset, true_and, Set.mem_setOf_eq, and_imp]
  assumption
Proof state after:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
hI_basis : M.Basis I A
⊢ I ⊆ J ∧
    (I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.Indep A_1 ∧ A_1 ⊆ A} ∧ A ⊆ M.E) ∧
      (J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ B} ∧ B ⊆ M.E) ∧ M.relRank A B = (J \ I).encard
Theorem: Matroid.relRank_intro
Proof state before:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
hI_basis : M.Basis I A
⊢ I ⊆ J ∧
    (I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.Indep A_1 ∧ A_1 ⊆ A} ∧ A ⊆ M.E) ∧
      (J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ B} ∧ B ⊆ M.E) ∧ M.relRank A B = (J \ I).encard
Tactic:
have hJ_basis : M.Basis J B := by
  refine M.basis_of_maximal_extension hB hJ
Proof state after:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
hI_basis : M.Basis I A
hJ_basis : M.Basis J B
⊢ I ⊆ J ∧
    (I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.Indep A_1 ∧ A_1 ⊆ A} ∧ A ⊆ M.E) ∧
      (J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ B} ∧ B ⊆ M.E) ∧ M.relRank A B = (J \ I).encard
Theorem: Matroid.relRank_intro
Proof state before:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
hI_basis : M.Basis I A
hJ_basis : M.Basis J B
⊢ I ⊆ J ∧
    (I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.Indep A_1 ∧ A_1 ⊆ A} ∧ A ⊆ M.E) ∧
      (J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ B} ∧ B ⊆ M.E) ∧ M.relRank A B = (J \ I).encard
Tactic:
refine ⟨hIJ, hI_basis, hJ_basis, ?_⟩
Proof state after:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
hI_basis : M.Basis I A
hJ_basis : M.Basis J B
⊢ M.relRank A B = (J \ I).encard
Theorem: Matroid.relRank_intro
Proof state before:
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
hI_basis : M.Basis I A
hJ_basis : M.Basis J B
⊢ M.relRank A B = (J \ I).encard
Tactic:
exact Basis.relRank_eq_encard_diff_of_subset_basis hI_basis hJ_basis hIJ
Proof state after:
no goals
Theorem: Matroid.relRank_intro
Proof state before:
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
⊢ M.Basis I A
Tactic:
refine @basis_of_maximal_extension α M ∅ A I (hA.trans hB) ?_
Proof state after:
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {I' | M.Indep I' ∧ ∅ ⊆ I' ∧ I' ⊆ A}
Theorem: Matroid.relRank_intro
Proof state before:
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {I' | M.Indep I' ∧ ∅ ⊆ I' ∧ I' ⊆ A}
Tactic:
unfold maximals
Proof state after:
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
⊢ I ∈
    {a |
      a ∈ {I' | M.Indep I' ∧ ∅ ⊆ I' ∧ I' ⊆ A} ∧
        ∀ ⦃b : Set α⦄,
          b ∈ {I' | M.Indep I' ∧ ∅ ⊆ I' ∧ I' ⊆ A} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
Theorem: Matroid.relRank_intro
Proof state before:
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
⊢ I ∈
    {a |
      a ∈ {I' | M.Indep I' ∧ ∅ ⊆ I' ∧ I' ⊆ A} ∧
        ∀ ⦃b : Set α⦄,
          b ∈ {I' | M.Indep I' ∧ ∅ ⊆ I' ∧ I' ⊆ A} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
Tactic:
simp only [Set.empty_subset, true_and, Set.mem_setOf_eq, and_imp]
Proof state after:
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
⊢ (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
Theorem: Matroid.relRank_intro
Proof state before:
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
⊢ (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.relRank_intro
Proof state before:
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
hI_basis : M.Basis I A
⊢ M.Basis J B
Tactic:
refine M.basis_of_maximal_extension hB hJ
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
hA : A ⊆ B
hB : M.Indep B
⊢ M.relRank A B = (B \ A).encard
Tactic:
set P := fun n ↦ ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
Proof state after:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
hA : A ⊆ B
hB : M.Indep B
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
⊢ M.relRank A B = (B \ A).encard
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
hA : A ⊆ B
hB : M.Indep B
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
h_induc : ∀ (n : ℕ∞), P n
⊢ M.relRank A B = (B \ A).encard
Tactic:
exact h_induc (B \ A).encard A B hA hB rfl
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
hA : A ⊆ B
hB : M.Indep B
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
⊢ ∀ (n : ℕ∞), P n
Tactic:
intro n
Proof state after:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
hA : A ⊆ B
hB : M.Indep B
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
⊢ P n