internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Hyperplane.inter_covBy_comm
Proof state before:
case inr.refine_2
α : 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 : α
hH₁ : M.Hyperplane H₁
hH₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
h : H₁ ∩ H₂ ⋖[M] H₂
⊢ H₁ ∩ H₂ ⋖[M] H₁
Tactic:
exact And.left <| h.covBy_and_covBy_of_covBy_of_ssubset_of_ssubset hH₂.covBy hH₁.flat
  (hH₁.inter_ssubset_left_of_ne hH₂ hne) (hH₁.ssubset_ground)
Proof state after:
no goals
Theorem: Matroid.Hyperplane.inter_covBy_comm
Proof state before:
case inr.refine_1
α : 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 : α
hH₁ : M.Hyperplane H₁
hH₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
h : H₁ ∩ H₂ ⋖[M] H₁
⊢ H₁ ∩ H₂ ⋖[M] H₂
Tactic:
exact And.left <| h.covBy_and_covBy_of_covBy_of_ssubset_of_ssubset hH₁.covBy hH₂.flat
  (hH₁.inter_ssubset_right_of_ne hH₂ hne) hH₂.ssubset_ground
Proof state after:
no goals
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
⊢ (M ＼ (H \ I)).Hyperplane I
Tactic:
obtain ⟨e, he, heH⟩ := exists_of_ssubset hH.ssubset_ground
Proof state after:
case intro.intro
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ (M ＼ (H \ I)).Hyperplane I
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof state before:
case intro.intro
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ (M ＼ (H \ I)).Hyperplane I
Tactic:
convert Base.hyperplane_of_cl_diff_singleton (B := insert e I) (e := e) ?_ (.inl rfl)
Proof state after:
case h.e'_3
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I = (M ＼ (H \ I)).cl (insert e I \ {e})

case intro.intro.convert_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ (M ＼ (H \ I)).Base (insert e I)
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof state before:
case intro.intro.convert_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ (M ＼ (H \ I)).Base (insert e I)
Tactic:
simp only [delete_base_iff]
Proof state after:
case intro.intro.convert_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ M.Basis (insert e I) (M.E \ (H \ I))
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof state before:
case intro.intro.convert_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ M.Basis (insert e I) (M.E \ (H \ I))
Tactic:
refine hB.indep.basis_of_forall_insert ?_ fun x ⟨⟨hxE, _⟩, hx⟩ ↦ hB.insert_dep ⟨hxE, hx⟩
Proof state after:
case intro.intro.convert_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ insert e I ⊆ M.E \ (H \ I)
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof state before:
case intro.intro.convert_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ insert e I ⊆ M.E \ (H \ I)
Tactic:
suffices insert e I ∩ (H \ I) = ∅ by simpa [insert_subset_iff, he, heH, subset_diff,
  hI.indep.subset_ground, disjoint_iff_inter_eq_empty]
Proof state after:
case intro.intro.convert_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ insert e I ∩ (H \ I) = ∅
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof state before:
case intro.intro.convert_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ insert e I ∩ (H \ I) = ∅
Tactic:
rw [insert_inter_of_not_mem (by simp [heH])]
Proof state after:
case intro.intro.convert_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I ∩ (H \ I) = ∅
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof state before:
case intro.intro.convert_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I ∩ (H \ I) = ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Base (insert e I)
Tactic:
refine Indep.base_of_spanning ?_ ?_
Proof state after:
case refine_1
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Indep (insert e I)

case refine_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Spanning (insert e I)
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof state before:
case refine_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Spanning (insert e I)
Tactic:
rw [spanning_iff_cl, ← cl_insert_cl_eq_cl_insert, hI.cl_eq_cl, hH.flat.cl,
  hH.cl_eq_ground_of_ssuperset (ssubset_insert heH)]
Proof state after:
no goals
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof state before:
case refine_1
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Indep (insert e I)
Tactic:
rwa [hI.indep.insert_indep_iff_of_not_mem (not_mem_subset hI.subset heH), hI.cl_eq_cl,
  hH.flat.cl, mem_diff, and_iff_left heH]
Proof state after:
no goals
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof state before:
case h.e'_3
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I = (M ＼ (H \ I)).cl (insert e I \ {e})
Tactic:
simp only [mem_singleton_iff, insert_diff_of_mem, not_mem_subset hI.subset heH,
not_false_eq_true, diff_singleton_eq_self, delete_cl_eq]
Proof state after:
case h.e'_3
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I = M.cl (I \ (H \ I)) \ (H \ I)
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof state before:
case h.e'_3
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I = M.cl (I \ (H \ I)) \ (H \ I)
Tactic:
rw [disjoint_sdiff_right.sdiff_eq_left, hI.cl_eq_cl, hH.flat.cl, diff_diff_cancel_left]
Proof state after:
case h.e'_3
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I ⊆ H
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof state before:
case h.e'_3
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ I ⊆ H
Tactic:
exact hI.subset
Proof state after:
no goals
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
this : insert e I ∩ (H \ I) = ∅
⊢ insert e I ⊆ M.E \ (H \ I)
Tactic:
simpa [insert_subset_iff, he, heH, subset_diff,
hI.indep.subset_ground, disjoint_iff_inter_eq_empty]
Proof state after:
no goals
Theorem: Matroid.Hyperplane.basis_hyperplane_delete
Proof 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
⊢ e ∉ H \ I
Tactic:
simp [heH]
Proof state after:
no goals
Theorem: Matroid.Hyperplane.basis_hyperplane_restrict
Proof 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
⊢ (M ↾ (I ∪ M.E \ H)).Hyperplane I
Tactic:
convert hH.basis_hyperplane_delete hI using 1
Proof state after:
case h.e'_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
⊢ M ↾ (I ∪ M.E \ H) = M ＼ (H \ I)
Theorem: Matroid.Hyperplane.basis_hyperplane_restrict
Proof state before:
case h.e'_2
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
⊢ M ↾ (I ∪ M.E \ H) = M ＼ (H \ I)
Tactic:
rw [delete_eq_restrict, diff_diff_right, inter_eq_self_of_subset_right hI.indep.subset_ground,
  union_comm]
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_point
Proof 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 : α
he : M.Nonloop e
⊢ M.er (M.cl {e}) = 1
Tactic:
rw [er_cl_eq, he.indep.er, encard_singleton]
Proof state after:
no goals
Theorem: Matroid.loops_covBy_iff
Proof 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.cl ∅ ⋖[M] P ↔ M.Point P
Tactic:
simp only [covBy_iff_relRank_eq_one, cl_flat, relRank_cl_left, relRank_empty_left, true_and,
  and_congr_right_iff, and_iff_right_iff_imp]
Proof 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 P → M.er P = 1 → M.cl ∅ ⊆ P
Theorem: Matroid.loops_covBy_iff
Proof 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 P → M.er P = 1 → M.cl ∅ ⊆ P
Tactic:
exact fun h _ ↦ h.cl_subset_of_subset (empty_subset _)
Proof state after:
no goals
Theorem: Matroid.Point.exists_eq_cl_nonloop
Proof 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 : α
hP : M.Point P
⊢ ∃ e, M.Nonloop e ∧ P = M.cl {e}
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis P
Proof state after:
case intro
α : 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 : α
hP : M.Point P
I : Set α
hI : M.Basis I P
⊢ ∃ e, M.Nonloop e ∧ P = M.cl {e}
Theorem: Matroid.Point.exists_eq_cl_nonloop
Proof state before:
case intro
α : 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 : α
hP : M.Point P
I : Set α
hI : M.Basis I P
⊢ ∃ e, M.Nonloop e ∧ P = M.cl {e}
Tactic:
obtain ⟨e, rfl⟩ := encard_eq_one.1 <| hI.encard.trans hP.er
Proof state after:
case intro.intro
α : 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 : α
hP : M.Point P
e : α
hI : M.Basis {e} P
⊢ ∃ e, M.Nonloop e ∧ P = M.cl {e}
Theorem: Matroid.Point.exists_eq_cl_nonloop
Proof state before:
case intro.intro
α : 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 : α
hP : M.Point P
e : α
hI : M.Basis {e} P
⊢ ∃ e, M.Nonloop e ∧ P = M.cl {e}
Tactic:
obtain rfl := hP.flat.eq_cl_of_basis hI
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ L H H₁ H₂ H' B C K : Set α
e✝ f e : α
hP : M.Point (M.cl {e})
hI : M.Basis {e} (M.cl {e})
⊢ ∃ e_1, M.Nonloop e_1 ∧ M.cl {e} = M.cl {e_1}
Theorem: Matroid.Point.exists_eq_cl_nonloop
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ L H H₁ H₂ H' B C K : Set α
e✝ f e : α
hP : M.Point (M.cl {e})
hI : M.Basis {e} (M.cl {e})
⊢ ∃ e_1, M.Nonloop e_1 ∧ M.cl {e} = M.cl {e_1}
Tactic:
exact ⟨e, indep_singleton.1 hI.indep, rfl⟩
Proof state after:
no goals
Theorem: Matroid.Point.eq_cl_of_mem
Proof 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 : α
hP : M.Point P
he : M.Nonloop e
heP : e ∈ P
⊢ P = M.cl {e}
Tactic:
rw [← indep_singleton] at he
Proof 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 : α
hP : M.Point P
he : M.Indep {e}
heP : e ∈ P
⊢ P = M.cl {e}
Theorem: Matroid.Point.eq_cl_of_mem
Proof 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 : α
hP : M.Point P
he : M.Indep {e}
heP : e ∈ P
⊢ P = M.cl {e}
Tactic:
exact hP.flat.eq_cl_of_basis <| he.basis_of_subset_of_er_le_of_finite (singleton_subset_iff.2 heP)
  (by rw [hP.er, he.er, encard_singleton]) (finite_singleton e)
Proof state after:
no goals
Theorem: Matroid.Point.eq_cl_of_mem
Proof 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 : α
hP : M.Point P
he : M.Indep {e}
heP : e ∈ P
⊢ M.er P ≤ M.er {e}
Tactic:
rw [hP.er, he.er, encard_singleton]
Proof state after:
no goals
Theorem: Matroid.point_iff_exists_eq_cl_nonloop
Proof 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 : α
⊢ (∃ e, M.Nonloop e ∧ P = M.cl {e}) → M.Point P
Tactic:
rintro ⟨e, he, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ L H H₁ H₂ H' B C K : Set α
e✝ f e : α
he : M.Nonloop e
⊢ M.Point (M.cl {e})
Theorem: Matroid.point_iff_exists_eq_cl_nonloop
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ L H H₁ H₂ H' B C K : Set α
e✝ f e : α
he : M.Nonloop e
⊢ M.Point (M.cl {e})
Tactic:
exact he.cl_point
Proof state after:
no goals
Theorem: Matroid.point_contract_iff
Proof 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 : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ (M ／ C).Point P ↔ (M.cl C ⋖[M] (C ∪ P)) ∧ Disjoint P C
Tactic:
rw [Point, flat_contract_iff, covBy_iff_relRank_eq_one, relRank_cl_left,
  union_comm C, ← relRank_eq_relRank_union, and_iff_right (cl_flat _ _),
  ← relRank_eq_er_contract, and_assoc, and_assoc, and_congr_right_iff, and_comm,
  and_congr_left_iff, iff_and_self]
Proof 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 : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ M.Flat (P ∪ C) → Disjoint P C → M.relRank C P = 1 → M.cl C ⊆ P ∪ C
Theorem: Matroid.point_contract_iff
Proof 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 : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ M.Flat (P ∪ C) → Disjoint P C → M.relRank C P = 1 → M.cl C ⊆ P ∪ C
Tactic:
rintro h - -
Proof 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 : α
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Flat (P ∪ C)
⊢ M.cl C ⊆ P ∪ C
Theorem: Matroid.point_contract_iff
Proof 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 : α
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Flat (P ∪ C)
⊢ M.cl C ⊆ P ∪ C
Tactic:
rw [← h.cl]
Proof 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 : α
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Flat (P ∪ C)
⊢ M.cl C ⊆ M.cl (P ∪ C)
Theorem: Matroid.point_contract_iff
Proof 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 : α
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Flat (P ∪ C)
⊢ M.cl C ⊆ M.cl (P ∪ C)
Tactic:
exact M.cl_subset_cl subset_union_right
Proof state after:
no goals
Theorem: Matroid.Point.subset_or_inter_eq_loops_of_flat
Proof 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 : α
hP : M.Point P
hF : M.Flat F
⊢ P ⊆ F ∨ P ∩ F = M.cl ∅
Tactic:
obtain (h | h) := hP.eq_or_eq_of_flat_of_subset (hP.flat.inter hF) inter_subset_left
Proof state after:
case inl
α : 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 : α
hP : M.Point P
hF : M.Flat F
h : P ∩ F = M.cl ∅
⊢ P ⊆ F ∨ P ∩ F = M.cl ∅

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 : α
hP : M.Point P
hF : M.Flat F
h : P ∩ F = P
⊢ P ⊆ F ∨ P ∩ F = M.cl ∅
Theorem: Matroid.Point.subset_or_inter_eq_loops_of_flat
Proof 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 : α
hP : M.Point P
hF : M.Flat F
h : P ∩ F = P
⊢ P ⊆ F ∨ P ∩ F = M.cl ∅
Tactic:
exact Or.inl (inter_eq_left.1 h)
Proof state after:
no goals
Theorem: Matroid.Point.subset_or_inter_eq_loops_of_flat
Proof state before:
case inl
α : 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 : α
hP : M.Point P
hF : M.Flat F
h : P ∩ F = M.cl ∅
⊢ P ⊆ F ∨ P ∩ F = M.cl ∅
Tactic:
exact Or.inr h
Proof state after:
no goals
Theorem: Matroid.Line.mem_iff_covBy
Proof 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 : α
hL : M.Line L
he : M.Nonloop e
⊢ e ∈ L ↔ M.cl {e} ⋖[M] L
Tactic:
rw [(M.cl_flat {e}).covBy_iff_relRank_eq_one hL.flat, hL.flat.cl_subset_iff_subset,
  singleton_subset_iff, iff_self_and, relRank_cl_left]
Proof 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 : α
hL : M.Line L
he : M.Nonloop e
⊢ e ∈ L → M.relRank {e} L = 1
Theorem: Matroid.Line.mem_iff_covBy
Proof 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 : α
hL : M.Line L
he : M.Nonloop e
⊢ e ∈ L → M.relRank {e} L = 1
Tactic:
intro heL
Proof 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 : α
hL : M.Line L
he : M.Nonloop e
heL : e ∈ L
⊢ M.relRank {e} L = 1
Theorem: Matroid.Line.mem_iff_covBy
Proof 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 : α
hL : M.Line L
he : M.Nonloop e
heL : e ∈ L
⊢ M.relRank {e} L = 1
Tactic:
rw [(M.rFin_singleton e).relRank_eq_sub (by simpa), he.er_eq, hL.er]
Proof 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 : α
hL : M.Line L
he : M.Nonloop e
heL : e ∈ L
⊢ 2 - 1 = 1
Theorem: Matroid.Line.mem_iff_covBy
Proof 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 : α
hL : M.Line L
he : M.Nonloop e
heL : e ∈ L
⊢ 2 - 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.Line.mem_iff_covBy
Proof 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 : α
hL : M.Line L
he : M.Nonloop e
heL : e ∈ L
⊢ {e} ⊆ L
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_covBy_iff
Proof 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 : α
he : M.Nonloop e
⊢ M.cl {e} ⋖[M] L ↔ M.Line L ∧ e ∈ L
Tactic:
refine ⟨fun h ↦ ⟨⟨h.flat_right, ?_⟩,h.subset <| M.mem_cl_self e⟩,
  fun ⟨hL, heL⟩ ↦ by rwa [← hL.mem_iff_covBy he]⟩
Proof 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 : α
he : M.Nonloop e
h : M.cl {e} ⋖[M] L
⊢ M.er L = 2
Theorem: Matroid.Nonloop.cl_covBy_iff
Proof 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 : α
he : M.Nonloop e
h : M.cl {e} ⋖[M] L
⊢ M.er L = 2
Tactic:
rw [h.er_eq, er_cl_eq, he.er_eq]
Proof 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 : α
he : M.Nonloop e
h : M.cl {e} ⋖[M] L
⊢ 1 + 1 = 2
Theorem: Matroid.Nonloop.cl_covBy_iff
Proof 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 : α
he : M.Nonloop e
h : M.cl {e} ⋖[M] L
⊢ 1 + 1 = 2
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_covBy_iff
Proof 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 : α
he : M.Nonloop e
x✝ : M.Line L ∧ e ∈ L
hL : M.Line L
heL : e ∈ L
⊢ M.cl {e} ⋖[M] L
Tactic:
rwa [← hL.mem_iff_covBy he]
Proof state after:
no goals
Theorem: encard_le_one_iff_subsingleton
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ s.encard ≤ 1 ↔ s.Subsingleton
Tactic:
rw [encard_le_one_iff, Set.Subsingleton]
Proof state after:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
Theorem: encard_le_one_iff_subsingleton
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
Tactic:
tauto
Proof state after:
no goals
Theorem: Finite.encard_union_eq_add_encard_iff_disjoint
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : (s ∪ t).Finite
⊢ s.encard + t.encard = (s ∪ t).encard ↔ Disjoint s t
Tactic:
rw [← add_zero (encard (s ∪ t)), ← encard_union_add_encard_inter, WithTop.add_left_cancel_iff
  h.encard_lt_top.ne, encard_eq_zero, disjoint_iff_inter_eq_empty]
Proof state after:
no goals
Theorem: encard_pair_le
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e f : α
⊢ {e, f}.encard ≤ 2
Tactic:
obtain (rfl | hne) := eq_or_ne e f
Proof state after:
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α
⊢ {e, e}.encard ≤ 2

case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e f : α
hne : e ≠ f
⊢ {e, f}.encard ≤ 2
Theorem: encard_pair_le
Proof state before:
case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e f : α
hne : e ≠ f
⊢ {e, f}.encard ≤ 2
Tactic:
rw [encard_pair hne]
Proof state after:
no goals
Theorem: encard_pair_le
Proof state before:
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α
⊢ {e, e}.encard ≤ 2
Tactic:
simp only [mem_singleton_iff, insert_eq_of_mem, encard_singleton]
Proof state after:
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α
⊢ 1 ≤ 2
Theorem: encard_pair_le
Proof state before:
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α
⊢ 1 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Set.coe_le_encard_iff
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard
Tactic:
obtain (hfin | hinf) := s.finite_or_infinite
Proof state after:
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hfin : s.Finite
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard

case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hinf : s.Infinite
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard
Theorem: Set.coe_le_encard_iff
Proof state before:
case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hinf : s.Infinite
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard
Tactic:
rw [hinf.encard_eq, iff_true_intro le_top, true_iff, iff_false_intro hinf, false_imp_iff]
Proof state after:
case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hinf : s.Infinite
⊢ True
Theorem: Set.coe_le_encard_iff
Proof state before:
case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hinf : s.Infinite
⊢ True
Tactic:
trivial
Proof state after:
no goals
Theorem: Set.coe_le_encard_iff
Proof state before:
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hfin : s.Finite
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard
Tactic:
rw [← hfin.cast_ncard_eq, iff_true_intro hfin, Nat.cast_le, true_imp_iff]
Proof state after:
no goals
Theorem: Equiv.encard_univ_eq
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α ≃ β
⊢ univ.encard = univ.encard
Tactic:
rw [encard_univ, encard_univ, PartENat.card_congr e]
Proof state after:
no goals