Theorem: Matroid.cocircuit_iff_mem_minimals (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ M.Cocircuit K ↔ K ∈ minimals (fun x x_1 => x ⊆ x_1) {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
Tactic:
revert K
State after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ ∀ {K : Set α}, M.Cocircuit K ↔ K ∈ minimals (fun x x_1 => x ⊆ x_1) {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}

State before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ ∀ {K : Set α}, M.Cocircuit K ↔ K ∈ minimals (fun x x_1 => x ⊆ x_1) {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
Tactic:
simp_rw [cocircuit_def, circuit_def, ← Set.ext_iff, dep_iff, ← coindep_def, dual_ground,
  coindep_iff_exists', not_and, imp_not_comm (b := (_ ⊆ _)), not_exists, not_and, subset_diff,
  not_and, not_disjoint_iff_nonempty_inter]
State after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ minimals (fun x x_1 => x ⊆ x_1) {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E} =
    minimals (fun x x_1 => x ⊆ x_1) {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}

State before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ minimals (fun x x_1 => x ⊆ x_1) {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E} =
    minimals (fun x x_1 => x ⊆ x_1) {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
Tactic:
apply (minimals_eq_minimals_of_subset_of_forall _ _).symm
State after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E} ⊆
    {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}

α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ ∀ x ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty},
    ∃ y ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}, y ⊆ x

State before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ ∀ x ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty},
    ∃ y ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}, y ⊆ x
Tactic:
refine' fun K hK ↦ ⟨K ∩ M.E, _, inter_subset_left⟩
State after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
⊢ K ∩ M.E ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}

State before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
⊢ K ∩ M.E ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}
Tactic:
simp only [mem_setOf_eq, inter_subset_right, forall_true_left, and_true]
State after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
⊢ ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ (K ∩ M.E)).Nonempty

State before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
⊢ ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ (K ∩ M.E)).Nonempty
Tactic:
rintro B hB hBE
State after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
B : Set α
hB : M.Base B
hBE : B ⊆ M.E
⊢ (B ∩ (K ∩ M.E)).Nonempty

State before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
B : Set α
hB : M.Base B
hBE : B ⊆ M.E
⊢ (B ∩ (K ∩ M.E)).Nonempty
Tactic:
rw [inter_comm, inter_assoc, inter_eq_self_of_subset_right hBE]
State after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
B : Set α
hB : M.Base B
hBE : B ⊆ M.E
⊢ (K ∩ B).Nonempty

State before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
B : Set α
hB : M.Base B
hBE : B ⊆ M.E
⊢ (K ∩ B).Nonempty
Tactic:
exact hK B hB
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E} ⊆
    {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
Tactic:
exact fun K ⟨hK1, hK2⟩ B hB ↦ by rw [inter_comm]; exact hK1 hK2 B hB hB.subset_ground
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
x✝ : K ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}
B : Set α
hB : M.Base B
hK1 : K ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ K).Nonempty
hK2 : K ⊆ M.E
⊢ (K ∩ B).Nonempty
Tactic:
rw [inter_comm]
State after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
x✝ : K ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}
B : Set α
hB : M.Base B
hK1 : K ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ K).Nonempty
hK2 : K ⊆ M.E
⊢ (B ∩ K).Nonempty

State before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
x✝ : K ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}
B : Set α
hB : M.Base B
hK1 : K ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ K).Nonempty
hK2 : K ⊆ M.E
⊢ (B ∩ K).Nonempty
Tactic:
exact hK1 hK2 B hB hB.subset_ground
State after:
no goals