internlm/Lean-Github huggingface dataset:
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 : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
⊢ M.relRank A A' = c + 1
Tactic:
rw [hP (ENat.toNat c + 1) A A' (Set.subset_union_left) hA'_indep hA'A, hcc]
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 : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
hrAA' : M.relRank A A' = c + 1
⊢ M.relRank A B ≥ c + 1
Tactic:
rw [M.relRank_add_cancel Set.subset_union_left hA'_subset_B, hrAA']
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 : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
hrAA' : M.relRank A A' = c + 1
⊢ c + 1 + M.relRank (A ∪ D) B ≥ c + 1
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 : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
hrAA' : M.relRank A A' = c + 1
⊢ c + 1 + M.relRank (A ∪ D) B ≥ c + 1
Tactic:
simp only [ge_iff_le, self_le_add_right]
Proof state after:
no goals
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
⊢ M.relRank A B = M.matroid.relRank A B
Tactic:
suffices h : ∀ {A B}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B by
  set A' := A ∩ M.E
  set B' := (B ∩ M.E) ∪ A'
  rw [<-relRank_inter_ground, relRank_eq_union_right, <-M.matroid.relRank_inter_ground_left,
      <-M.matroid.relRank_inter_ground_right, M.matroid.relRank_eq_union_right]
  simp only [matroid_E]
  refine h Set.subset_union_right ?_
  rw [<-Set.union_inter_distrib_right]
  exact Set.inter_subset_right
Proof state after:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
⊢ ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
⊢ ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
Tactic:
intro A B hA hB
Proof state after:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
⊢ M.relRank A B = M.matroid.relRank A B
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
⊢ M.relRank A B = M.matroid.relRank A B
Tactic:
obtain ⟨I, J, hI, ⟨hI_basis_A, _⟩, ⟨hJ_basis_B, _⟩, h⟩ := M.matroid.relRank_intro hA hB
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
hI_basis_A : I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A}
right✝¹ : A ⊆ M.matroid.E
h : M.matroid.relRank A B = (J \ I).encard
hJ_basis_B : J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.matroid.Indep A ∧ A ⊆ B}
right✝ : B ⊆ M.matroid.E
⊢ M.relRank A B = M.matroid.relRank A B
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
hI_basis_A : I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A}
right✝¹ : A ⊆ M.matroid.E
h : M.matroid.relRank A B = (J \ I).encard
hJ_basis_B : J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.matroid.Indep A ∧ A ⊆ B}
right✝ : B ⊆ M.matroid.E
⊢ M.relRank A B = M.matroid.relRank A B
Tactic:
rw [h]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
hI_basis_A : I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A}
right✝¹ : A ⊆ M.matroid.E
h : M.matroid.relRank A B = (J \ I).encard
hJ_basis_B : J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.matroid.Indep A ∧ A ⊆ B}
right✝ : B ⊆ M.matroid.E
⊢ M.relRank A B = (J \ I).encard
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
hI_basis_A : I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A}
right✝¹ : A ⊆ M.matroid.E
h : M.matroid.relRank A B = (J \ I).encard
hJ_basis_B : J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.matroid.Indep A ∧ A ⊆ B}
right✝ : B ⊆ M.matroid.E
⊢ M.relRank A B = (J \ I).encard
Tactic:
clear h
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
hI_basis_A : I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A}
right✝¹ : A ⊆ M.matroid.E
hJ_basis_B : J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.matroid.Indep A ∧ A ⊆ B}
right✝ : B ⊆ M.matroid.E
⊢ M.relRank A B = (J \ I).encard
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
hI_basis_A : I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A}
right✝¹ : A ⊆ M.matroid.E
hJ_basis_B : J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.matroid.Indep A ∧ A ⊆ B}
right✝ : B ⊆ M.matroid.E
⊢ M.relRank A B = (J \ I).encard
Tactic:
unfold maximals at hI_basis_A hJ_basis_B
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
hI_basis_A :
  I ∈
    {a |
      a ∈ {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A} ∧
        ∀ ⦃b : Set α⦄,
          b ∈ {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
right✝¹ : A ⊆ M.matroid.E
hJ_basis_B :
  J ∈
    {a |
      a ∈ {A | M.matroid.Indep A ∧ A ⊆ B} ∧
        ∀ ⦃b : Set α⦄, b ∈ {A | M.matroid.Indep A ∧ A ⊆ B} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
right✝ : B ⊆ M.matroid.E
⊢ M.relRank A B = (J \ I).encard
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
hI_basis_A :
  I ∈
    {a |
      a ∈ {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A} ∧
        ∀ ⦃b : Set α⦄,
          b ∈ {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
right✝¹ : A ⊆ M.matroid.E
hJ_basis_B :
  J ∈
    {a |
      a ∈ {A | M.matroid.Indep A ∧ A ⊆ B} ∧
        ∀ ⦃b : Set α⦄, b ∈ {A | M.matroid.Indep A ∧ A ⊆ B} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
right✝ : B ⊆ M.matroid.E
⊢ M.relRank A B = (J \ I).encard
Tactic:
simp only [matroid_Indep, Set.mem_setOf_eq, and_imp] at hI_basis_A hJ_basis_B
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_basis_A : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hJ_basis_B : (M.Indep J ∧ J ⊆ B) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
⊢ M.relRank A B = (J \ I).encard
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_basis_A : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hJ_basis_B : (M.Indep J ∧ J ⊆ B) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
⊢ M.relRank A B = (J \ I).encard
Tactic:
obtain ⟨⟨hI_indep, hI_subset⟩, hI_max⟩ := hI_basis_A
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hJ_basis_B : (M.Indep J ∧ J ⊆ B) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
⊢ M.relRank A B = (J \ I).encard
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hJ_basis_B : (M.Indep J ∧ J ⊆ B) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
⊢ M.relRank A B = (J \ I).encard
Tactic:
obtain ⟨⟨hJ_indep, hJ_subset⟩, hJ_max⟩ := hJ_basis_B
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
⊢ M.relRank A B = (J \ I).encard
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
⊢ M.relRank A B = (J \ I).encard
Tactic:
rw [<-M.relRank_indeps_eq_encard_diff hI hJ_indep]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
⊢ M.relRank A B = M.relRank I J
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
⊢ M.relRank A B = M.relRank I J
Tactic:
have hIA : M.relRank I A = 0 := by
  rw [<-indep_subset_maximal_iff_relRank_zero hI_subset hI_indep]
  unfold maximals; simp only [Set.mem_setOf_eq, and_imp]
  exact ⟨⟨hI_indep, hI_subset⟩, hI_max⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
⊢ M.relRank A B = M.relRank I J
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
⊢ M.relRank A B = M.relRank I J
Tactic:
have hJB : M.relRank J B = 0 := by
  rw [<-indep_subset_maximal_iff_relRank_zero hJ_subset hJ_indep]
  unfold maximals; simp only [Set.mem_setOf_eq, and_imp]
  exact ⟨⟨hJ_indep, hJ_subset⟩, hJ_max⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank A B = M.relRank I J
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank A B = M.relRank I J
Tactic:
calc
  M.relRank A B = M.relRank I A + M.relRank A B := by
    rw [hIA]; simp only [zero_add]
  _ = M.relRank I B := by
    exact eq_comm.mp (M.relRank_add_cancel hI_subset hA)
  _ = M.relRank I J + M.relRank J B := by
    exact M.relRank_add_cancel hI hJ_subset
  _ = M.relRank I J := by
    rw [hJB]; simp only [add_zero]
Proof state after:
no goals
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
⊢ M.relRank A B = M.matroid.relRank A B
Tactic:
set A' := A ∩ M.E
Proof state after:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
⊢ M.relRank A B = M.matroid.relRank A B
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
⊢ M.relRank A B = M.matroid.relRank A B
Tactic:
set B' := (B ∩ M.E) ∪ A'
Proof state after:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ M.relRank A B = M.matroid.relRank A B
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ M.relRank A B = M.matroid.relRank A B
Tactic:
rw [<-relRank_inter_ground, relRank_eq_union_right, <-M.matroid.relRank_inter_ground_left,
    <-M.matroid.relRank_inter_ground_right, M.matroid.relRank_eq_union_right]
Proof state after:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ M.relRank (A ∩ M.E) (B ∩ M.E ∪ A ∩ M.E) = M.matroid.relRank (A ∩ M.matroid.E) (B ∩ M.matroid.E ∪ A ∩ M.matroid.E)
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ M.relRank (A ∩ M.E) (B ∩ M.E ∪ A ∩ M.E) = M.matroid.relRank (A ∩ M.matroid.E) (B ∩ M.matroid.E ∪ A ∩ M.matroid.E)
Tactic:
simp only [matroid_E]
Proof state after:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ M.relRank (A ∩ M.E) (B ∩ M.E ∪ A ∩ M.E) = M.matroid.relRank (A ∩ M.E) (B ∩ M.E ∪ A ∩ M.E)
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ M.relRank (A ∩ M.E) (B ∩ M.E ∪ A ∩ M.E) = M.matroid.relRank (A ∩ M.E) (B ∩ M.E ∪ A ∩ M.E)
Tactic:
refine h Set.subset_union_right ?_
Proof state after:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ B ∩ M.E ∪ A ∩ M.E ⊆ M.E
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ B ∩ M.E ∪ A ∩ M.E ⊆ M.E
Tactic:
rw [<-Set.union_inter_distrib_right]
Proof state after:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ (B ∪ A) ∩ M.E ⊆ M.E
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ (B ∪ A) ∩ M.E ⊆ M.E
Tactic:
exact Set.inter_subset_right
Proof state after:
no goals
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
⊢ M.relRank I A = 0
Tactic:
rw [<-indep_subset_maximal_iff_relRank_zero hI_subset hI_indep]
Proof state after:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ A}
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ A}
Tactic:
unfold maximals
Proof state after:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
⊢ I ∈
    {a |
      a ∈ {S | M.Indep S ∧ S ⊆ A} ∧
        ∀ ⦃b : Set α⦄, b ∈ {S | M.Indep S ∧ S ⊆ A} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}