Theorem: Matroid.Flat.wcovBy_iff_of_flat (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₀ : M.Flat F₀
hF₁ : M.Flat F₁
⊢ F₀ ⩿[M] F₁ ↔ F₀ ⊆ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
Tactic:
obtain (rfl | hne) := eq_or_ne F₀ F₁
State after:
case inl
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀ hF₁ : M.Flat F₀
⊢ F₀ ⩿[M] F₀ ↔ F₀ ⊆ F₀ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₀ → F = F₀ ∨ F = F₀

case inr
α : 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₀ : M.Flat F₀
hF₁ : M.Flat F₁
hne : F₀ ≠ F₁
⊢ F₀ ⩿[M] F₁ ↔ F₀ ⊆ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁

State before:
case inr
α : 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₀ : M.Flat F₀
hF₁ : M.Flat F₁
hne : F₀ ≠ F₁
⊢ F₀ ⩿[M] F₁ ↔ F₀ ⊆ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
Tactic:
rw [wCovby_iff_covBy_or_eq hF₀ hF₁, subset_iff_ssubset_or_eq, or_iff_left hne, or_iff_left hne,
  hF₀.covBy_iff_of_flat hF₁]
State after:
no goals

State before:
case inl
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀ hF₁ : M.Flat F₀
⊢ F₀ ⩿[M] F₀ ↔ F₀ ⊆ F₀ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₀ → F = F₀ ∨ F = F₀
Tactic:
simp only [hF₀, wCovBy_self, or_self, true_iff]
State after:
case inl
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀ hF₁ : M.Flat F₀
⊢ F₀ ⊆ F₀ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₀ → F = F₀

State before:
case inl
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀ hF₁ : M.Flat F₀
⊢ F₀ ⊆ F₀ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₀ → F = F₀
Tactic:
exact ⟨Subset.rfl, fun _ _  ↦ antisymm'⟩
State after:
no goals