Theorem: Matroid.hyperplane_iff_maximal_proper_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 : α
⊢ M.Hyperplane H ↔ M.Flat H ∧ H ⊂ M.E ∧ ∀ (F : Set α), H ⊂ F → M.Flat F → F = M.E
Tactic:
rw [hyperplane_iff_covBy, covBy_iff, and_iff_right M.ground_flat, and_congr_right_iff,
  and_congr_right_iff]
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 : α
⊢ M.Flat H →
    H ⊂ M.E →
      ((∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → F = H ∨ F = M.E) ↔ ∀ (F : Set α), H ⊂ F → M.Flat F → F = M.E)

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 : α
⊢ M.Flat H →
    H ⊂ M.E →
      ((∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → F = H ∨ F = M.E) ↔ ∀ (F : Set α), H ⊂ F → M.Flat F → F = M.E)
Tactic:
simp_rw [or_iff_not_imp_left, ssubset_iff_subset_ne, and_imp]
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 : α
⊢ M.Flat H →
    H ⊆ M.E →
      H ≠ M.E →
        ((∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → ¬F = H → F = M.E) ↔
          ∀ (F : Set α), H ⊆ F → H ≠ F → M.Flat F → F = M.E)

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 : α
⊢ M.Flat H →
    H ⊆ M.E →
      H ≠ M.E →
        ((∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → ¬F = H → F = M.E) ↔
          ∀ (F : Set α), H ⊆ F → H ≠ F → M.Flat F → F = M.E)
Tactic:
exact fun _ _ _  ↦
  ⟨fun h F hHF hne' hF ↦ h F hF hHF hF.subset_ground hne'.symm, fun h F hF hHF _ hne' ↦
    h F hHF (Ne.symm hne') hF⟩
State after:
no goals