internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Parallel'.indep_substitute_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h_para : M.Parallel' e f
he : e ∈ I
hf : f ∉ I
hI : M.Indep (insert f (I \ {e}))
⊢ e ≠ f
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
he : e ∈ I
h_para : M.Parallel' e e
hf : e ∉ I
hI : M.Indep (insert e (I \ {e}))
⊢ False
Theorem: Matroid.Parallel'.indep_substitute_iff
Proof state before:
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
he : e ∈ I
h_para : M.Parallel' e e
hf : e ∉ I
hI : M.Indep (insert e (I \ {e}))
⊢ False
Tactic:
exact hf he
Proof state after:
no goals
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
⊢ M.mapEquiv (Equiv.swap e f) = M
Tactic:
have hrw := Equiv.swap_image_eq_self
    (show e ∈ M.E ↔ f ∈ M.E by simp [h.mem_ground_left, h.mem_ground_right])
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
⊢ M.mapEquiv (Equiv.swap e f) = M
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
⊢ M.mapEquiv (Equiv.swap e f) = M
Tactic:
simp only [eq_iff_indep_iff_indep_forall, mapEquiv_ground_eq, hrw, mapEquiv_indep_iff,
  Equiv.symm_swap, true_and]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
⊢ ∀ I ⊆ M.E, M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
⊢ ∀ I ⊆ M.E, M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
rintro I -
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
by_cases heI : e ∈ I
Proof state after:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I

case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
by_cases hfI : f ∈ I
Proof state after:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
hfI : f ∈ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I

case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
hfI : f ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
hfI : f ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
rw [Equiv.swap_image_eq_self (by simp [hfI, heI])]
Proof state after:
no goals
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
⊢ e ∈ M.E ↔ f ∈ M.E
Tactic:
simp [h.mem_ground_left, h.mem_ground_right]
Proof state after:
no goals
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
by_cases hfI : f ∈ I
Proof state after:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
hfI : f ∈ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I

case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
hfI : f ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
hfI : f ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
rw [Equiv.swap_image_eq_exchange heI hfI, ← h.indep_substitute_iff heI hfI]
Proof state after:
no goals
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
hfI : f ∈ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
rw [Equiv.swap_image_eq_self (by simp [heI, hfI])]
Proof state after:
no goals
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
hfI : f ∈ I
⊢ e ∈ I ↔ f ∈ I
Tactic:
simp [heI, hfI]
Proof state after:
no goals
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
hfI : f ∈ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
rw [Equiv.swap_comm, Equiv.swap_image_eq_exchange hfI heI,
  ← h.symm.indep_substitute_iff hfI heI]
Proof state after:
no goals
Theorem: Matroid.Parallel'.eq_mapEquiv_swap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
hfI : f ∉ I
⊢ e ∈ I ↔ f ∈ I
Tactic:
simp [hfI, heI]
Proof state after:
no goals
Theorem: Matroid.indep_iff_range_indep_of_paraMap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
⊢ M.Indep I ↔ M.Indep (range φ)
Tactic:
set ψ := Equiv.ofInjective _ hφ
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep I ↔ M.Indep (range φ)
Theorem: Matroid.indep_iff_range_indep_of_paraMap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep I ↔ M.Indep (range φ)
Tactic:
convert Iso.indep_image_iff (I := univ) <|
  (isoOfMapParallelRestr ψ (by simpa only [Equiv.ofInjective_apply, ψ] using h_para)) using 1
Proof state after:
case h.e'_1.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep I ↔ (M ↾ I).Indep ↑univ

case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ (M ↾ range φ).Indep ↑(⇑(isoOfMapParallelRestr ψ ⋯) '' univ)
Theorem: Matroid.indep_iff_range_indep_of_paraMap
Proof state before:
case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ (M ↾ range φ).Indep ↑(⇑(isoOfMapParallelRestr ψ ⋯) '' univ)
Tactic:
simp only [restrict_ground_eq, image_univ, restrict_indep_iff, image_subset_iff,
  Subtype.coe_preimage_self, subset_univ, and_true]
Proof state after:
case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ M.Indep ((fun a => ↑a) '' range fun a => (isoOfMapParallelRestr ψ ⋯) a)
Theorem: Matroid.indep_iff_range_indep_of_paraMap
Proof state before:
case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ M.Indep ((fun a => ↑a) '' range fun a => (isoOfMapParallelRestr ψ ⋯) a)
Tactic:
simp_rw [← image_univ, image_image, image_univ]
Proof state after:
case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ M.Indep (range fun x => ↑((isoOfMapParallelRestr ψ ⋯) x))
Theorem: Matroid.indep_iff_range_indep_of_paraMap
Proof state before:
case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ M.Indep (range fun x => ↑((isoOfMapParallelRestr ψ ⋯) x))
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.indep_iff_range_indep_of_paraMap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ ∀ (e : ↑I), ?m.371381.Parallel' ↑e ↑(ψ e)
Tactic:
simpa only [Equiv.ofInjective_apply, ψ] using h_para
Proof state after:
no goals
Theorem: Matroid.indep_iff_range_indep_of_paraMap
Proof state before:
case h.e'_1.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep I ↔ (M ↾ I).Indep ↑univ
Tactic:
simp [Subset.rfl]
Proof state after:
no goals
Theorem: Matroid.Indep.paraMap_injective
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
⊢ Function.Injective φ
Tactic:
intro x y hxy
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
x y : ↑I
hxy : φ x = φ y
⊢ x = y
Theorem: Matroid.Indep.paraMap_injective
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
x y : ↑I
hxy : φ x = φ y
⊢ x = y
Tactic:
have hx := h_para x
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
x y : ↑I
hxy : φ x = φ y
hx : M.Parallel' (↑x) (φ x)
⊢ x = y
Theorem: Matroid.Indep.paraMap_injective
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
x y : ↑I
hxy : φ x = φ y
hx : M.Parallel' (↑x) (φ x)
⊢ x = y
Tactic:
rw [hxy] at hx
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
x y : ↑I
hxy : φ x = φ y
hx : M.Parallel' (↑x) (φ y)
⊢ x = y
Theorem: Matroid.Indep.paraMap_injective
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
x y : ↑I
hxy : φ x = φ y
hx : M.Parallel' (↑x) (φ y)
⊢ x = y
Tactic:
exact Subtype.val_inj.1
  ((hx.trans (h_para y).symm).eq_of_indep (hI.subset (pair_subset x.2 y.2)))
Proof state after:
no goals
Theorem: Matroid.Indep.indep_range_paraMap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
⊢ M.Indep (range φ)
Tactic:
rwa [← indep_iff_range_indep_of_paraMap (hI.paraMap_injective φ h_para) h_para]
Proof state after:
no goals
Theorem: Matroid.Indep.image_paraMap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ M.Indep (φ '' I)
Tactic:
convert hI.indep_range_paraMap (fun e ↦ φ e) (by simpa)
Proof state after:
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ φ '' I = range fun e => φ ↑e
Theorem: Matroid.Indep.image_paraMap
Proof state before:
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ φ '' I = range fun e => φ ↑e
Tactic:
simp [Set.ext_iff]
Proof state after:
no goals
Theorem: Matroid.Indep.image_paraMap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ ∀ (e : ↑I), M.Parallel' (↑e) ((fun e => φ ↑e) e)
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Indep.of_image_paraMap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep (φ '' I)
hφ : InjOn φ I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ M.Indep I
Tactic:
rwa [indep_iff_range_indep_of_paraMap hφ.injective (by simpa), range_restrict]
Proof state after:
no goals
Theorem: Matroid.Indep.of_image_paraMap
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep (φ '' I)
hφ : InjOn φ I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ ∀ (e : ↑I), M.Parallel' (↑e) (I.restrict φ e)
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.mem_parallelClasses_iff_eq_cl_diff_loops
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ P ∈ M.parallelClasses ↔ ∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅
Tactic:
simp only [parallelClasses, Partition.mem_congr_iff, Flat.mem_covByPartition_iff,
  loops_covBy_iff, point_iff_exists_eq_cl_nonloop]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P) ↔ ∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅
Theorem: Matroid.mem_parallelClasses_iff_eq_cl_diff_loops
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P) ↔ ∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P) → ∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅

case mpr
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅) → ∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P
Theorem: Matroid.mem_parallelClasses_iff_eq_cl_diff_loops
Proof state before:
case mpr
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅) → ∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P
Tactic:
rintro ⟨e, he, rfl⟩
Proof state after:
case mpr.intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
e : α
he : M.Nonloop e
⊢ ∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = M.cl {e} \ M.cl ∅
Theorem: Matroid.mem_parallelClasses_iff_eq_cl_diff_loops
Proof state before:
case mpr.intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
e : α
he : M.Nonloop e
⊢ ∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = M.cl {e} \ M.cl ∅
Tactic:
exact ⟨_, ⟨e, he, rfl⟩,rfl⟩
Proof state after:
no goals
Theorem: Matroid.mem_parallelClasses_iff_eq_cl_diff_loops
Proof state before:
case mp
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P) → ∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅
Tactic:
rintro ⟨_, ⟨e, he, rfl⟩, rfl⟩
Proof state after:
case mp.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
e : α
he : M.Nonloop e
⊢ ∃ e_1, M.Nonloop e_1 ∧ M.cl {e} \ M.cl ∅ = M.cl {e_1} \ M.cl ∅
Theorem: Matroid.mem_parallelClasses_iff_eq_cl_diff_loops
Proof state before:
case mp.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
e : α
he : M.Nonloop e
⊢ ∃ e_1, M.Nonloop e_1 ∧ M.cl {e} \ M.cl ∅ = M.cl {e_1} \ M.cl ∅
Tactic:
exact ⟨e, he, rfl⟩
Proof state after:
no goals
Theorem: Matroid.mem_parallelClasses_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ P ∈ M.parallelClasses ↔ ∃ e, M.Nonloop e ∧ P = {f | M.Parallel e f}
Tactic:
simp_rw [mem_parallelClasses_iff_eq_cl_diff_loops, setOf_parallel_eq_cl_diff_loops]
Proof state after:
no goals
Theorem: Matroid.Paving.spanning_of_dep
Proof state before:
α : Type u_1
N M : Matroid α
C D : Set α
hM : M.Paving
hD : M.Dep D
⊢ M.Spanning D
Tactic:
obtain ⟨C, hCD, hC⟩ := hD.exists_circuit_subset
Proof state after:
case intro.intro
α : Type u_1
N M : Matroid α
C✝ D : Set α
hM : M.Paving
hD : M.Dep D
C : Set α
hCD : C ⊆ D
hC : M.Circuit C
⊢ M.Spanning D
Theorem: Matroid.Paving.spanning_of_dep
Proof state before:
case intro.intro
α : Type u_1
N M : Matroid α
C✝ D : Set α
hM : M.Paving
hD : M.Dep D
C : Set α
hCD : C ⊆ D
hC : M.Circuit C
⊢ M.Spanning D
Tactic:
exact (hM.spanning_of_circuit hC).superset hCD
Proof state after:
no goals
Theorem: Matroid.SparsePaving.dual
Proof state before:
α : Type u_1
N M : Matroid α
C D : Set α
h : M.SparsePaving
⊢ M✶.SparsePaving
Tactic:
rw [SparsePaving, dual_dual]
Proof state after:
α : Type u_1
N M : Matroid α
C D : Set α
h : M.SparsePaving
⊢ M✶.Paving ∧ M.Paving
Theorem: Matroid.SparsePaving.dual
Proof state before:
α : Type u_1
N M : Matroid α
C D : Set α
h : M.SparsePaving
⊢ M✶.Paving ∧ M.Paving
Tactic:
exact And.symm h
Proof state after:
no goals
Theorem: Matroid.circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Circuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C
Tactic:
simp [Circuit, mem_minimals_setOf_iff, and_congr_right_iff, eq_comm (b := C)]
Proof state after:
no goals
Theorem: Matroid.Circuit.ssubset_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hXC : X ⊂ C
⊢ M.Indep X
Tactic:
rw [← not_dep_iff (hXC.subset.trans hC.subset_ground)]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hXC : X ⊂ C
⊢ ¬M.Dep X
Theorem: Matroid.Circuit.ssubset_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hXC : X ⊂ C
⊢ ¬M.Dep X
Tactic:
exact fun h ↦ hXC.ne ((circuit_iff.1 hC).2 h hXC.subset)
Proof state after:
no goals
Theorem: Matroid.circuit_iff_forall_ssubset
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Circuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I
Tactic:
simp_rw [circuit_iff, dep_iff, and_congr_right_iff, ssubset_iff_subset_ne, and_imp]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ ¬M.Indep C →
    C ⊆ M.E → ((∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ M.E → I ⊆ C → I = C) ↔ ∀ ⦃I : Set α⦄, I ⊆ C → I ≠ C → M.Indep I)
Theorem: Matroid.circuit_iff_forall_ssubset
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ ¬M.Indep C →
    C ⊆ M.E → ((∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ M.E → I ⊆ C → I = C) ↔ ∀ ⦃I : Set α⦄, I ⊆ C → I ≠ C → M.Indep I)
Tactic:
exact fun _ hC ↦ ⟨fun h I hIC hne ↦ by_contra fun hi ↦ hne (h hi (hIC.trans hC) hIC),
  fun h I hi _ hIC ↦ by_contra fun hne ↦ hi (h hIC hne)⟩
Proof state after:
no goals
Theorem: Matroid.Circuit.diff_singleton_basis
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
he : e ∈ C
⊢ M.Basis (C \ {e}) C
Tactic:
nth_rw 2 [← insert_eq_of_mem he]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
he : e ∈ C
⊢ M.Basis (C \ {e}) (insert e C)
Theorem: Matroid.Circuit.diff_singleton_basis
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
he : e ∈ C
⊢ M.Basis (C \ {e}) (insert e C)
Tactic:
rw [← insert_diff_singleton, (hC.diff_singleton_indep he).basis_insert_iff,
  insert_diff_singleton, insert_eq_of_mem he]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
he : e ∈ C
⊢ M.Dep C ∨ e ∈ C \ {e}
Theorem: Matroid.Circuit.diff_singleton_basis
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
he : e ∈ C
⊢ M.Dep C ∨ e ∈ C \ {e}
Tactic:
exact Or.inl hC.dep
Proof state after:
no goals
Theorem: Matroid.Circuit.basis_iff_eq_diff_singleton
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
⊢ M.Basis I C ↔ ∃ e ∈ C, I = C \ {e}
Tactic:
refine' ⟨fun h ↦ _, _⟩
Proof state after:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
h : M.Basis I C
⊢ ∃ e ∈ C, I = C \ {e}

case refine'_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
⊢ (∃ e ∈ C, I = C \ {e}) → M.Basis I C
Theorem: Matroid.Circuit.basis_iff_eq_diff_singleton
Proof state before:
case refine'_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
⊢ (∃ e ∈ C, I = C \ {e}) → M.Basis I C
Tactic:
rintro ⟨e, he, rfl⟩
Proof state after:
case refine'_2.intro.intro
α : Type u_1
M : Matroid α
C C' X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ M.Basis (C \ {e}) C
Theorem: Matroid.Circuit.basis_iff_eq_diff_singleton
Proof state before:
case refine'_2.intro.intro
α : Type u_1
M : Matroid α
C C' X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ M.Basis (C \ {e}) C
Tactic:
exact hC.diff_singleton_basis he
Proof state after:
no goals
Theorem: Matroid.Circuit.basis_iff_eq_diff_singleton
Proof state before:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
h : M.Basis I C
⊢ ∃ e ∈ C, I = C \ {e}
Tactic:
obtain ⟨e, he⟩ := exists_of_ssubset
  (h.subset.ssubset_of_ne (by rintro rfl; exact hC.dep.not_indep h.indep))
Proof state after:
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
h : M.Basis I C
e : α
he : e ∈ C ∧ e ∉ I
⊢ ∃ e ∈ C, I = C \ {e}
Theorem: Matroid.Circuit.basis_iff_eq_diff_singleton
Proof state before:
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
h : M.Basis I C
e : α
he : e ∈ C ∧ e ∉ I
⊢ ∃ e ∈ C, I = C \ {e}
Tactic:
exact ⟨e, he.1, h.eq_of_subset_indep (hC.diff_singleton_indep he.1)
  (subset_diff_singleton h.subset he.2) diff_subset⟩
Proof state after:
no goals
Theorem: Matroid.Circuit.basis_iff_eq_diff_singleton
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
h : M.Basis I C
⊢ I ≠ C
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M : Matroid α
C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit I
h : M.Basis I I
⊢ False