internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Flat.iInter
Proof state before:
case h.e'_4
α : 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 : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
J : Set α
hIJ : M.Basis J (Fs i)
hJ : I ⊆ J
⊢ Fs i ∪ X = Fs i ∪ (J ∪ X)
Tactic:
rw [← union_assoc, union_eq_self_of_subset_right hIJ.subset]
Proof state after:
no goals
Theorem: Matroid.Flat.inter
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 : α
hF₁ : M.Flat F₁
hF₂ : M.Flat F₂
⊢ M.Flat (F₁ ∩ F₂)
Tactic:
rw [inter_eq_iInter]
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 : α
hF₁ : M.Flat F₁
hF₂ : M.Flat F₂
⊢ M.Flat (⋂ b, bif b then F₁ else F₂)
Theorem: Matroid.Flat.inter
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 : α
hF₁ : M.Flat F₁
hF₂ : M.Flat F₂
⊢ M.Flat (⋂ b, bif b then F₁ else F₂)
Tactic:
apply Flat.iInter
Proof state after:
case hFs
α : 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₂
⊢ ∀ (i : Bool), M.Flat (bif i then F₁ else F₂)
Theorem: Matroid.Flat.inter
Proof state before:
case hFs
α : 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₂
⊢ ∀ (i : Bool), M.Flat (bif i then F₁ else F₂)
Tactic:
simp [hF₁, hF₂]
Proof state after:
no goals
Theorem: Matroid.Flat.iInter_inter_ground
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 : α
ι : Type u_2
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
⊢ M.Flat ((⋂ i, Fs i) ∩ M.E)
Tactic:
obtain (hι | hι) := isEmpty_or_nonempty ι
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 : α
ι : Type u_2
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
hι : IsEmpty ι
⊢ M.Flat ((⋂ i, Fs i) ∩ M.E)

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 : α
ι : Type u_2
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
hι : Nonempty ι
⊢ M.Flat ((⋂ i, Fs i) ∩ M.E)
Theorem: Matroid.Flat.iInter_inter_ground
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 : α
ι : Type u_2
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
hι : Nonempty ι
⊢ M.Flat ((⋂ i, Fs i) ∩ M.E)
Tactic:
exact (Flat.iInter hFs).inter M.ground_flat
Proof state after:
no goals
Theorem: Matroid.Flat.iInter_inter_ground
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 : α
ι : Type u_2
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
hι : IsEmpty ι
⊢ M.Flat ((⋂ i, Fs i) ∩ M.E)
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Flat.biInter
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 : α
ι : Type u_2
Fs : ι → Set α
s : Set ι
hs : s.Nonempty
hFs : ∀ i ∈ s, M.Flat (Fs i)
⊢ M.Flat (⋂ i ∈ s, Fs i)
Tactic:
rw [biInter_eq_iInter]
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 : α
ι : Type u_2
Fs : ι → Set α
s : Set ι
hs : s.Nonempty
hFs : ∀ i ∈ s, M.Flat (Fs i)
⊢ M.Flat (⋂ x, Fs ↑x)
Theorem: Matroid.Flat.biInter
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 : α
ι : Type u_2
Fs : ι → Set α
s : Set ι
hs : s.Nonempty
hFs : ∀ i ∈ s, M.Flat (Fs i)
⊢ M.Flat (⋂ x, Fs ↑x)
Tactic:
have := hs.to_subtype
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 : α
ι : Type u_2
Fs : ι → Set α
s : Set ι
hs : s.Nonempty
hFs : ∀ i ∈ s, M.Flat (Fs i)
this : Nonempty ↑s
⊢ M.Flat (⋂ x, Fs ↑x)
Theorem: Matroid.Flat.biInter
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 : α
ι : Type u_2
Fs : ι → Set α
s : Set ι
hs : s.Nonempty
hFs : ∀ i ∈ s, M.Flat (Fs i)
this : Nonempty ↑s
⊢ M.Flat (⋂ x, Fs ↑x)
Tactic:
apply Flat.iInter (by simpa)
Proof state after:
no goals
Theorem: Matroid.Flat.biInter
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 : α
ι : Type u_2
Fs : ι → Set α
s : Set ι
hs : s.Nonempty
hFs : ∀ i ∈ s, M.Flat (Fs i)
this : Nonempty ↑s
⊢ ∀ (i : ↑s), M.Flat (Fs ↑i)
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Flat.biInter_inter_ground
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 : α
ι : Type u_2
Fs : ι → Set α
s : Set ι
hFs : ∀ i ∈ s, M.Flat (Fs i)
⊢ M.Flat ((⋂ i ∈ s, Fs i) ∩ M.E)
Tactic:
rw [biInter_eq_iInter]
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 : α
ι : Type u_2
Fs : ι → Set α
s : Set ι
hFs : ∀ i ∈ s, M.Flat (Fs i)
⊢ M.Flat ((⋂ x, Fs ↑x) ∩ M.E)
Theorem: Matroid.Flat.biInter_inter_ground
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 : α
ι : Type u_2
Fs : ι → Set α
s : Set ι
hFs : ∀ i ∈ s, M.Flat (Fs i)
⊢ M.Flat ((⋂ x, Fs ↑x) ∩ M.E)
Tactic:
exact Flat.iInter_inter_ground (by simpa)
Proof state after:
no goals
Theorem: Matroid.Flat.biInter_inter_ground
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 : α
ι : Type u_2
Fs : ι → Set α
s : Set ι
hFs : ∀ i ∈ s, M.Flat (Fs i)
⊢ ∀ (i : ↑s), M.Flat (Fs ↑i)
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Flat.sInter
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 : α
Fs : Set (Set α)
hF : Fs.Nonempty
h : ∀ F ∈ Fs, M.Flat F
⊢ M.Flat (⋂₀ Fs)
Tactic:
rw [sInter_eq_iInter]
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 : α
Fs : Set (Set α)
hF : Fs.Nonempty
h : ∀ F ∈ Fs, M.Flat F
⊢ M.Flat (⋂ i, ↑i)
Theorem: Matroid.Flat.sInter
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 : α
Fs : Set (Set α)
hF : Fs.Nonempty
h : ∀ F ∈ Fs, M.Flat F
⊢ M.Flat (⋂ i, ↑i)
Tactic:
have : Nonempty Fs := Iff.mpr nonempty_coe_sort hF
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 : α
Fs : Set (Set α)
hF : Fs.Nonempty
h : ∀ F ∈ Fs, M.Flat F
this : Nonempty ↑Fs
⊢ M.Flat (⋂ i, ↑i)
Theorem: Matroid.Flat.sInter
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 : α
Fs : Set (Set α)
hF : Fs.Nonempty
h : ∀ F ∈ Fs, M.Flat F
this : Nonempty ↑Fs
⊢ M.Flat (⋂ i, ↑i)
Tactic:
exact Flat.iInter (fun ⟨F, hF⟩ ↦ h _ hF)
Proof state after:
no goals
Theorem: Matroid.Flat.sInter_inter_ground
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 : α
Fs : Set (Set α)
h : ∀ F ∈ Fs, M.Flat F
⊢ M.Flat (⋂₀ Fs ∩ M.E)
Tactic:
rw [sInter_eq_iInter]
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 : α
Fs : Set (Set α)
h : ∀ F ∈ Fs, M.Flat F
⊢ M.Flat ((⋂ i, ↑i) ∩ M.E)
Theorem: Matroid.Flat.sInter_inter_ground
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 : α
Fs : Set (Set α)
h : ∀ F ∈ Fs, M.Flat F
⊢ M.Flat ((⋂ i, ↑i) ∩ M.E)
Tactic:
exact Flat.iInter_inter_ground (by simpa)
Proof state after:
no goals
Theorem: Matroid.Flat.sInter_inter_ground
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 : α
Fs : Set (Set α)
h : ∀ F ∈ Fs, M.Flat F
⊢ ∀ (i : ↑Fs), M.Flat ↑i
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.flat_iff_cl_self
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 : α
h : M.cl F = F
⊢ M.Flat F
Tactic:
rw [← 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 : α
h : M.cl F = F
⊢ M.Flat (M.cl F)
Theorem: Matroid.flat_iff_cl_self
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 : α
h : M.cl F = F
⊢ M.Flat (M.cl F)
Tactic:
exact cl_flat _ _
Proof state after:
no goals
Theorem: Matroid.flat_map_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✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set β
⊢ (M.map f hf).Flat F ↔ ∃ F₀, M.Flat F₀ ∧ F = f '' F₀
Tactic:
simp only [flat_iff_cl_self, map_cl_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✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set β
⊢ f '' M.cl (f ⁻¹' F) = F ↔ ∃ F₀, M.cl F₀ = F₀ ∧ F = f '' F₀
Theorem: Matroid.flat_map_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✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set β
⊢ f '' M.cl (f ⁻¹' F) = F ↔ ∃ F₀, M.cl F₀ = F₀ ∧ F = f '' F₀
Tactic:
refine ⟨fun h ↦ ⟨M.cl (f ⁻¹' F), by simp, h.symm⟩, ?_⟩
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✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set β
⊢ (∃ F₀, M.cl F₀ = F₀ ∧ F = f '' F₀) → f '' M.cl (f ⁻¹' F) = F
Theorem: Matroid.flat_map_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✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set β
⊢ (∃ F₀, M.cl F₀ = F₀ ∧ F = f '' F₀) → f '' M.cl (f ⁻¹' F) = F
Tactic:
rintro ⟨F, hF, rfl⟩
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✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set α
hF : M.cl F = F
⊢ f '' M.cl (f ⁻¹' (f '' F)) = f '' F
Theorem: Matroid.flat_map_iff
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✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set α
hF : M.cl F = F
⊢ f '' M.cl (f ⁻¹' (f '' F)) = f '' F
Tactic:
rw [← cl_inter_ground, hf.preimage_image_inter, hF]
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✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set α
hF : M.cl F = F
⊢ F ⊆ M.E
Theorem: Matroid.flat_map_iff
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✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set α
hF : M.cl F = F
⊢ F ⊆ M.E
Tactic:
exact hF.symm.subset.trans <| M.cl_subset_ground _
Proof state after:
no goals
Theorem: Matroid.flat_map_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✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set β
h : f '' M.cl (f ⁻¹' F) = F
⊢ M.cl (M.cl (f ⁻¹' F)) = M.cl (f ⁻¹' F)
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Flat.map
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✝ : α
β : Type u_2
f : α → β
hF : M.Flat F
hf : InjOn f M.E
⊢ (M.map f hf).Flat (f '' F)
Tactic:
rw [flat_iff_cl_self, map_cl_eq, ← cl_inter_ground, hf.preimage_image_inter hF.subset_ground,
  hF.cl]
Proof state after:
no goals
Theorem: Matroid.flat_iff_subset_cl_self
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
⊢ M.Flat F ↔ M.cl F ⊆ F
Tactic:
rw [flat_iff_cl_self, subset_antisymm_iff, and_iff_left_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 : α
hF : autoParam (F ⊆ M.E) _auto✝
⊢ M.cl F ⊆ F → F ⊆ M.cl F
Theorem: Matroid.flat_iff_subset_cl_self
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
⊢ M.cl F ⊆ F → F ⊆ M.cl F
Tactic:
exact fun _ ↦ M.subset_cl F
Proof state after:
no goals
Theorem: Matroid.exists_mem_cl_not_mem_of_not_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 : α
h : ¬M.Flat F
hF : autoParam (F ⊆ M.E) _auto✝
⊢ ∃ e, e ∈ M.cl F \ F
Tactic:
rw [flat_iff_cl_self, subset_antisymm_iff, and_iff_left (M.subset_cl F)] at 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 : α
h : ¬M.cl F ⊆ F
hF : autoParam (F ⊆ M.E) _auto✝
⊢ ∃ e, e ∈ M.cl F \ F
Theorem: Matroid.exists_mem_cl_not_mem_of_not_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 : α
h : ¬M.cl F ⊆ F
hF : autoParam (F ⊆ M.E) _auto✝
⊢ ∃ e, e ∈ M.cl F \ F
Tactic:
exact not_subset.1 h
Proof state after:
no goals
Theorem: Matroid.flat_iff_ssubset_cl_insert_forall
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
⊢ M.Flat F ↔ ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
Tactic:
refine' ⟨fun h e he ↦ (M.cl_subset_cl (subset_insert _ _)).ssubset_of_ne _, fun h ↦ _⟩
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.Flat F
e : α
he : e ∈ M.E \ F
⊢ M.cl F ≠ M.cl (insert e F)

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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
⊢ M.Flat F
Theorem: Matroid.flat_iff_ssubset_cl_insert_forall
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
⊢ M.Flat F
Tactic:
rw [flat_iff_cl_self]
Proof state after:
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
⊢ M.cl F = F
Theorem: Matroid.flat_iff_ssubset_cl_insert_forall
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
⊢ M.cl F = F
Tactic:
by_contra h'
Proof state after:
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
⊢ False
Theorem: Matroid.flat_iff_ssubset_cl_insert_forall
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
⊢ False
Tactic:
obtain ⟨e, he', heF⟩ := exists_of_ssubset (ssubset_of_ne_of_subset (Ne.symm h') (M.subset_cl F))
Proof state after:
case refine'_2.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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
e : α
he' : e ∈ M.cl F
heF : e ∉ F
⊢ False
Theorem: Matroid.flat_iff_ssubset_cl_insert_forall
Proof state before:
case refine'_2.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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
e : α
he' : e ∈ M.cl F
heF : e ∉ F
⊢ False
Tactic:
have h'' := h e ⟨(M.cl_subset_ground F) he', heF⟩
Proof state after:
case refine'_2.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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
e : α
he' : e ∈ M.cl F
heF : e ∉ F
h'' : M.cl F ⊂ M.cl (insert e F)
⊢ False
Theorem: Matroid.flat_iff_ssubset_cl_insert_forall
Proof state before:
case refine'_2.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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
e : α
he' : e ∈ M.cl F
heF : e ∉ F
h'' : M.cl F ⊂ M.cl (insert e F)
⊢ False
Tactic:
rw [← M.cl_insert_cl_eq_cl_insert e F, insert_eq_of_mem he', M.cl_cl] at h''
Proof state after:
case refine'_2.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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
e : α
he' : e ∈ M.cl F
heF : e ∉ F
h'' : M.cl F ⊂ M.cl F
⊢ False
Theorem: Matroid.flat_iff_ssubset_cl_insert_forall
Proof state before:
case refine'_2.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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
e : α
he' : e ∈ M.cl F
heF : e ∉ F
h'' : M.cl F ⊂ M.cl F
⊢ False
Tactic:
exact h''.ne rfl
Proof state after:
no goals
Theorem: Matroid.flat_iff_ssubset_cl_insert_forall
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.Flat F
e : α
he : e ∈ M.E \ F
⊢ M.cl F ≠ M.cl (insert e F)
Tactic:
rw [h.cl]
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.Flat F
e : α
he : e ∈ M.E \ F
⊢ F ≠ M.cl (insert e F)
Theorem: Matroid.flat_iff_ssubset_cl_insert_forall
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.Flat F
e : α
he : e ∈ M.E \ F
⊢ F ≠ M.cl (insert e F)
Tactic:
exact fun h' ↦ mt ((Set.ext_iff.mp h') e).mpr (not_mem_of_mem_diff he)
  ((M.subset_cl _ (insert_subset he.1 hF)) (mem_insert _ _))
Proof state after:
no goals
Theorem: Matroid.flat_iff_forall_circuit
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
⊢ M.Flat F ↔ ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
Tactic:
rw [flat_iff_cl_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 : α
hF : autoParam (F ⊆ M.E) _auto✝
⊢ M.cl F = F ↔ ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
Theorem: Matroid.flat_iff_forall_circuit
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
⊢ M.cl F = F ↔ ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
Tactic:
refine' ⟨fun h C e hC heC hCF ↦ _, fun h ↦ _⟩
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.cl F = F
C : Set α
e : α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ e ∈ F

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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
⊢ M.cl F = F
Theorem: Matroid.flat_iff_forall_circuit
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
⊢ M.cl F = F
Tactic:
refine' (M.subset_cl F hF).antisymm' (fun e heF ↦ by_contra fun he' ↦ _)
Proof state after:
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
e : α
heF : e ∈ M.cl F
he' : e ∉ F
⊢ False
Theorem: Matroid.flat_iff_forall_circuit
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
e : α
heF : e ∈ M.cl F
he' : e ∉ F
⊢ False
Tactic:
obtain ⟨C, hC, heC, hCF⟩ := (mem_cl_iff_exists_circuit_of_not_mem he').mp heF
Proof state after:
case refine'_2.intro.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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
e : α
heF : e ∈ M.cl F
he' : e ∉ F
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ False
Theorem: Matroid.flat_iff_forall_circuit
Proof state before:
case refine'_2.intro.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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
e : α
heF : e ∈ M.cl F
he' : e ∉ F
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ False
Tactic:
exact he' (h C e hC heC hCF)
Proof state after:
no goals
Theorem: Matroid.flat_iff_forall_circuit
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.cl F = F
C : Set α
e : α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ e ∈ F
Tactic:
rw [← h]
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.cl F = F
C : Set α
e : α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ e ∈ M.cl F
Theorem: Matroid.flat_iff_forall_circuit
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.cl F = F
C : Set α
e : α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ e ∈ M.cl F
Tactic:
refine' (M.cl_subset_cl _) (hC.subset_cl_diff_singleton e heC)
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.cl F = F
C : Set α
e : α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ C \ {e} ⊆ F
Theorem: Matroid.flat_iff_forall_circuit
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 : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.cl F = F
C : Set α
e : α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ C \ {e} ⊆ F
Tactic:
rwa [diff_subset_iff, singleton_union]
Proof state after:
no goals
Theorem: Matroid.flat_iff_forall_circuit'
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 F ↔ (∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F) ∧ F ⊆ M.E
Tactic:
refine' ⟨fun h ↦ ⟨(flat_iff_forall_circuit h.subset_ground).mp h, h.subset_ground⟩, fun h ↦
  (flat_iff_forall_circuit h.2).mpr h.1⟩
Proof state after:
no goals
Theorem: Matroid.Flat.cl_exchange
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 : α
hF : M.Flat F
he : e ∈ M.cl (insert f F) \ F
⊢ f ∈ M.cl (insert e F) \ F
Tactic:
nth_rw 2 [← hF.cl] at *
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 : α
hF : M.Flat F
he : e ∈ M.cl (insert f F) \ M.cl F
⊢ f ∈ M.cl (insert e F) \ M.cl F
Theorem: Matroid.Flat.cl_exchange
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 : α
hF : M.Flat F
he : e ∈ M.cl (insert f F) \ M.cl F
⊢ f ∈ M.cl (insert e F) \ M.cl F
Tactic:
exact Matroid.cl_exchange he
Proof state after:
no goals
Theorem: Matroid.Flat.cl_insert_eq_cl_insert_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 : α
hF : M.Flat F
he : e ∈ M.cl (insert f F) \ F
⊢ e ∈ M.cl (insert f F) \ M.cl F
Tactic:
rwa [hF.cl]
Proof state after:
no goals
Theorem: Matroid.Flat.cl_subset_of_subset
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 : α
hF : M.Flat F
h : X ⊆ F
⊢ M.cl X ⊆ F
Tactic:
have h' := M.cl_mono 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 : α
hF : M.Flat F
h : X ⊆ F
h' : M.cl X ≤ M.cl F
⊢ M.cl X ⊆ F