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

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
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

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
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

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
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

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]
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

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
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

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
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

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
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

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
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

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
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

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]
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

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⟩
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

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⟩
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

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]
State after:
no goals

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
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

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'
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

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]
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)

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]
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)

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 ?_
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

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]
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

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
State after:
no goals

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]
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}

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
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}

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 ∈
    {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}
Tactic:
simp only [Set.mem_setOf_eq, and_imp]
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
⊢ (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I

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.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
Tactic:
exact ⟨⟨hI_indep, hI_subset⟩, hI_max⟩
State after:
no goals

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
hIA : M.relRank I A = 0
⊢ M.relRank J B = 0
Tactic:
rw [<-indep_subset_maximal_iff_relRank_zero hJ_subset hJ_indep]
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
hIA : M.relRank I A = 0
⊢ J ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ B}

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
hIA : M.relRank I A = 0
⊢ J ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ B}
Tactic:
unfold maximals
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
hIA : M.relRank I A = 0
⊢ J ∈
    {a |
      a ∈ {S | M.Indep S ∧ S ⊆ B} ∧
        ∀ ⦃b : Set α⦄, b ∈ {S | M.Indep S ∧ S ⊆ B} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}

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
hIA : M.relRank I A = 0
⊢ J ∈
    {a |
      a ∈ {S | M.Indep S ∧ S ⊆ B} ∧
        ∀ ⦃b : Set α⦄, b ∈ {S | M.Indep S ∧ S ⊆ B} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
Tactic:
simp only [Set.mem_setOf_eq, and_imp]
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
hIA : M.relRank I A = 0
⊢ (M.Indep J ∧ J ⊆ B) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J

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
hIA : M.relRank I A = 0
⊢ (M.Indep J ∧ J ⊆ B) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
Tactic:
exact ⟨⟨hJ_indep, hJ_subset⟩, hJ_max⟩
State after:
no goals

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
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank A B = M.relRank I A + M.relRank A B
Tactic:
rw [hIA]
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
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank A B = 0 + M.relRank A B

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
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank A B = 0 + M.relRank A B
Tactic:
simp only [zero_add]
State after:
no goals

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
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank I A + M.relRank A B = M.relRank I B
Tactic:
exact eq_comm.mp (M.relRank_add_cancel hI_subset hA)
State after:
no goals

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
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank I B = M.relRank I J + M.relRank J B
Tactic:
exact M.relRank_add_cancel hI hJ_subset
State after:
no goals

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
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank I J + M.relRank J B = M.relRank I J
Tactic:
rw [hJB]
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
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank I J + 0 = M.relRank I J

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
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank I J + 0 = M.relRank I J
Tactic:
simp only [add_zero]
State after:
no goals