Theorem: Matroid.CovBy.covBy_and_covBy_of_covBy_of_ssubset_of_ssubset (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀F' : F₀ ⋖[M] F'
hF'F₁ : F' ⋖[M] F₁
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
apply hF₀F'.flat_left.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two hF'F₁.flat_right
  ?_ hF h₀ h₁
State after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀F' : F₀ ⋖[M] F'
hF'F₁ : F' ⋖[M] F₁
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ M.relRank F₀ F₁ = 2

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀F' : F₀ ⋖[M] F'
hF'F₁ : F' ⋖[M] F₁
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ M.relRank F₀ F₁ = 2
Tactic:
rw [← M.relRank_add_of_subset_of_subset hF₀F'.subset hF'F₁.subset, hF'F₁.relRank_eq_one,
  hF₀F'.relRank_eq_one]
State after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀F' : F₀ ⋖[M] F'
hF'F₁ : F' ⋖[M] F₁
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ 1 + 1 = 2

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀F' : F₀ ⋖[M] F'
hF'F₁ : F' ⋖[M] F₁
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ 1 + 1 = 2
Tactic:
rfl
State after:
no goals