internlm/Lean-Github huggingface dataset:
Theorem: Matroid.parallel_iff_circuit
Proof state before:
case refine'_1.inr
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
x : α
hef : e ≠ x
h : M.Parallel e x
⊢ M.Indep ({e, x} \ {x})
Tactic:
rw [pair_diff_right hef]
Proof state after:
case refine'_1.inr
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
x : α
hef : e ≠ x
h : M.Parallel e x
⊢ M.Indep {e}
Theorem: Matroid.parallel_iff_circuit
Proof state before:
case refine'_1.inr
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
x : α
hef : e ≠ x
h : M.Parallel e x
⊢ M.Indep {e}
Tactic:
exact h.nonloop_left.indep
Proof state after:
no goals
Theorem: Matroid.parallel_iff_circuit
Proof state before:
case refine'_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ e ∈ M.cl {f}
Tactic:
convert h.mem_cl_diff_singleton_of_mem (mem_insert _ _)
Proof state after:
case h.e'_5.h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ {f} = {e, f} \ {e}
Theorem: Matroid.parallel_iff_circuit
Proof state before:
case h.e'_5.h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ {f} = {e, f} \ {e}
Tactic:
rw [pair_diff_left hef]
Proof state after:
no goals
Theorem: Matroid.Parallel.circuit_of_ne
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : M.Parallel e f
hne : e ≠ f
⊢ M.Circuit {e, f}
Tactic:
rwa [parallel_iff_circuit hne] at hef
Proof state after:
no goals
Theorem: Matroid.Nonloop.parallel_iff_dep
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
hf : M.Nonloop f
hef : e ≠ f
⊢ M.Parallel e f ↔ M.Dep {e, f}
Tactic:
rw [← hf.indep.mem_cl_iff_of_not_mem hef, he.parallel_iff_mem_cl]
Proof state after:
no goals
Theorem: Matroid.Parallel.eq_of_indep
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
hi : M.Indep {e, f}
⊢ e = f
Tactic:
by_contra hef
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
hi : M.Indep {e, f}
hef : ¬e = f
⊢ False
Theorem: Matroid.Parallel.eq_of_indep
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
hi : M.Indep {e, f}
hef : ¬e = f
⊢ False
Tactic:
exact ((h.nonloop_left.parallel_iff_dep h.nonloop_right hef).1 h).not_indep hi
Proof state after:
no goals
Theorem: Matroid.parallel_iff_nonloop_nonloop_indep_imp_eq
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Parallel e f ↔ M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
Tactic:
refine ⟨fun h ↦ ⟨h.nonloop_left, h.nonloop_right, fun hi ↦ h.eq_of_indep hi⟩, fun h ↦ ?_⟩
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
⊢ M.Parallel e f
Theorem: Matroid.parallel_iff_nonloop_nonloop_indep_imp_eq
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
⊢ M.Parallel e f
Tactic:
obtain (rfl | hne) := eq_or_ne e f
Proof state after:
case inl
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop e ∧ (M.Indep {e, e} → e = e)
⊢ M.Parallel e e

case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
hne : e ≠ f
⊢ M.Parallel e f
Theorem: Matroid.parallel_iff_nonloop_nonloop_indep_imp_eq
Proof state before:
case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
hne : e ≠ f
⊢ M.Parallel e f
Tactic:
rw [h.1.parallel_iff_dep h.2.1 hne, Dep, pair_subset_iff, and_iff_left h.2.1.mem_ground,
  and_iff_left h.1.mem_ground]
Proof state after:
case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
hne : e ≠ f
⊢ ¬M.Indep {e, f}
Theorem: Matroid.parallel_iff_nonloop_nonloop_indep_imp_eq
Proof state before:
case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
hne : e ≠ f
⊢ ¬M.Indep {e, f}
Tactic:
exact fun hi ↦ hne (h.2.2 hi)
Proof state after:
no goals
Theorem: Matroid.parallel_iff_nonloop_nonloop_indep_imp_eq
Proof state before:
case inl
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop e ∧ (M.Indep {e, e} → e = e)
⊢ M.Parallel e e
Tactic:
exact h.1.parallel_self
Proof state after:
no goals
Theorem: Matroid.Parallel.mem_cl_iff_mem_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
h : M.Parallel e f
X : Set α
⊢ e ∈ M.cl X ↔ f ∈ M.cl X
Tactic:
refine ⟨fun h' ↦ ?_, fun h' ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
h : M.Parallel e f
X : Set α
h' : e ∈ M.cl X
⊢ f ∈ M.cl X

case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
h : M.Parallel e f
X : Set α
h' : f ∈ M.cl X
⊢ e ∈ M.cl X
Theorem: Matroid.Parallel.mem_cl_iff_mem_cl
Proof state before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
h : M.Parallel e f
X : Set α
h' : f ∈ M.cl X
⊢ e ∈ M.cl X
Tactic:
exact mem_of_mem_of_subset h.mem_cl (M.cl_subset_cl_of_subset_cl (by simpa))
Proof state after:
no goals
Theorem: Matroid.Parallel.mem_cl_iff_mem_cl
Proof state before:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
h : M.Parallel e f
X : Set α
h' : e ∈ M.cl X
⊢ f ∈ M.cl X
Tactic:
exact mem_of_mem_of_subset h.symm.mem_cl (M.cl_subset_cl_of_subset_cl (by simpa))
Proof state after:
no goals
Theorem: Matroid.Parallel.mem_cl_iff_mem_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
h : M.Parallel e f
X : Set α
h' : e ∈ M.cl X
⊢ {e} ⊆ M.cl X
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Parallel.mem_cl_iff_mem_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
h : M.Parallel e f
X : Set α
h' : f ∈ M.cl X
⊢ {f} ⊆ M.cl X
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Parallel.loop_of_contract
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : M.Parallel e f
hne : e ≠ f
⊢ (M ／ e).Loop f
Tactic:
rw [loop_iff_mem_cl_empty, contract_elem, contract_loops_eq, mem_diff]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : M.Parallel e f
hne : e ≠ f
⊢ f ∈ M.cl {e} ∧ f ∉ {e}
Theorem: Matroid.Parallel.loop_of_contract
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : M.Parallel e f
hne : e ≠ f
⊢ f ∈ M.cl {e} ∧ f ∉ {e}
Tactic:
exact ⟨hef.symm.mem_cl, hne.symm⟩
Proof state after:
no goals
Theorem: Matroid.restrict_parallel_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D R : Set α
⊢ (M ↾ R).Parallel e f ↔ M.Parallel e f ∧ e ∈ R ∧ f ∈ R
Tactic:
simp only [parallel_iff_nonloop_nonloop_indep_imp_eq, restrict_nonloop_iff, restrict_indep_iff,
  pair_subset_iff, and_imp]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D R : Set α
⊢ (M.Nonloop e ∧ e ∈ R) ∧ (M.Nonloop f ∧ f ∈ R) ∧ (M.Indep {e, f} → e ∈ R → f ∈ R → e = f) ↔
    (M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)) ∧ e ∈ R ∧ f ∈ R
Theorem: Matroid.restrict_parallel_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D R : Set α
⊢ (M.Nonloop e ∧ e ∈ R) ∧ (M.Nonloop f ∧ f ∈ R) ∧ (M.Indep {e, f} → e ∈ R → f ∈ R → e = f) ↔
    (M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)) ∧ e ∈ R ∧ f ∈ R
Tactic:
aesop
Proof state after:
no goals
Theorem: Matroid.removeLoops_parallel_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.removeLoops.Parallel e f ↔ M.Parallel e f
Tactic:
rw [removeLoops_eq_restr, restrict_parallel_iff,
  and_iff_left_of_imp (fun h ↦ ⟨h.nonloop_left, h.nonloop_right⟩)]
Proof state after:
no goals
Theorem: Matroid.Parallel.mem_cocircuit_of_mem
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
⊢ f ∈ K
Tactic:
by_contra hf
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
⊢ False
Theorem: Matroid.Parallel.mem_cocircuit_of_mem
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
⊢ False
Tactic:
have hK' := (hK.compl_hyperplane).flat.cl
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
⊢ False
Theorem: Matroid.Parallel.mem_cocircuit_of_mem
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
⊢ False
Tactic:
have hfK := hK'.symm.subset ⟨hef.mem_ground_right, hf⟩
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
hfK : f ∈ M.cl (M.E \ K)
⊢ False
Theorem: Matroid.Parallel.mem_cocircuit_of_mem
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
hfK : f ∈ M.cl (M.E \ K)
⊢ False
Tactic:
rw [← hef.mem_cl_iff_mem_cl, hK'] at hfK
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
hfK : e ∈ M.E \ K
⊢ False
Theorem: Matroid.Parallel.mem_cocircuit_of_mem
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
hfK : e ∈ M.E \ K
⊢ False
Tactic:
exact hfK.2 he
Proof state after:
no goals
Theorem: Matroid.Parallel'.parallel_of_nonloop
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Nonloop e
⊢ M.Parallel e f
Tactic:
rwa [Nonloop.parallel_iff_cl_eq_cl, h.cl_eq_cl]
Proof state after:
no goals
Theorem: Matroid.Parallel'.loop_of_loop
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
⊢ M.Loop f
Tactic:
have h' := h.cl_eq_cl
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
h' : M.cl {e} = M.cl {f}
⊢ M.Loop f
Theorem: Matroid.Parallel'.loop_of_loop
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
h' : M.cl {e} = M.cl {f}
⊢ M.Loop f
Tactic:
rw [he.cl, eq_comm] at h'
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
h' : M.cl {f} = M.cl ∅
⊢ M.Loop f
Theorem: Matroid.Parallel'.loop_of_loop
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
h' : M.cl {f} = M.cl ∅
⊢ M.Loop f
Tactic:
rwa [loop_iff_cl_eq_cl_empty h.mem_ground_right]
Proof state after:
no goals
Theorem: Matroid.Parallel'.loop_or_parallel
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
⊢ M.Loop e ∧ M.Loop f ∨ M.Parallel e f
Tactic:
obtain (he | he) := M.loop_or_nonloop e
Proof state after:
case inl
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
⊢ M.Loop e ∧ M.Loop f ∨ M.Parallel e f

case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Nonloop e
⊢ M.Loop e ∧ M.Loop f ∨ M.Parallel e f
Theorem: Matroid.Parallel'.loop_or_parallel
Proof state before:
case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Nonloop e
⊢ M.Loop e ∧ M.Loop f ∨ M.Parallel e f
Tactic:
exact .inr <| h.parallel_of_nonloop he
Proof state after:
no goals
Theorem: Matroid.Parallel'.loop_or_parallel
Proof state before:
case inl
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
⊢ M.Loop e ∧ M.Loop f ∨ M.Parallel e f
Tactic:
exact .inl ⟨he, h.loop_of_loop he⟩
Proof state after:
no goals
Theorem: Matroid.parallel'_iff_loops_or_parallel
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Parallel' e f ↔ M.Loop e ∧ M.Loop f ∨ M.Parallel e f
Tactic:
refine ⟨Parallel'.loop_or_parallel, ?_⟩
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Loop e ∧ M.Loop f ∨ M.Parallel e f → M.Parallel' e f
Theorem: Matroid.parallel'_iff_loops_or_parallel
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Loop e ∧ M.Loop f ∨ M.Parallel e f → M.Parallel' e f
Tactic:
rintro (⟨he, hf⟩ | hef)
Proof state after:
case inl.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Loop e
hf : M.Loop f
⊢ M.Parallel' e f

case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : M.Parallel e f
⊢ M.Parallel' e f
Theorem: Matroid.parallel'_iff_loops_or_parallel
Proof state before:
case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : M.Parallel e f
⊢ M.Parallel' e f
Tactic:
exact hef.parallel'
Proof state after:
no goals
Theorem: Matroid.parallel'_iff_loops_or_parallel
Proof state before:
case inl.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Loop e
hf : M.Loop f
⊢ M.Parallel' e f
Tactic:
rw [Matroid.Parallel', he.cl, hf.cl]
Proof state after:
case inl.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Loop e
hf : M.Loop f
⊢ e ∈ M.E ∧ f ∈ M.E ∧ M.cl ∅ = M.cl ∅
Theorem: Matroid.parallel'_iff_loops_or_parallel
Proof state before:
case inl.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Loop e
hf : M.Loop f
⊢ e ∈ M.E ∧ f ∈ M.E ∧ M.cl ∅ = M.cl ∅
Tactic:
simp [he.mem_ground, hf.mem_ground]
Proof state after:
no goals
Theorem: Matroid.parallel'_iff_cl_eq_cl
Proof state before:
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
e f : α
he : autoParam (e ∈ M.E) _auto✝
hf : autoParam (f ∈ M.E) _auto✝
⊢ M.Parallel' e f ↔ M.cl {e} = M.cl {f}
Tactic:
rw [Matroid.Parallel', and_iff_right he, and_iff_right hf]
Proof state after:
no goals
Theorem: Matroid.Parallel'.mem_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
⊢ e ∈ M.cl {f}
Tactic:
rw [← h.cl_eq_cl]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
⊢ e ∈ M.cl {e}
Theorem: Matroid.Parallel'.mem_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
⊢ e ∈ M.cl {e}
Tactic:
apply mem_cl_self _ _ h.mem_ground_left
Proof state after:
no goals
Theorem: Matroid.parallel'_iff_parallel
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Parallel' e f ↔ M.Parallel e f
Tactic:
rw [parallel'_iff_loops_or_parallel, or_iff_right (fun h ↦ M.not_loop e h.1)]
Proof state after:
no goals
Theorem: Matroid.Parallel'.mem_cl_iff_mem_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
h : M.Parallel' e f
X : Set α
⊢ e ∈ M.cl X ↔ f ∈ M.cl X
Tactic:
obtain (⟨he, hf⟩ | h) := h.loop_or_parallel
Proof state after:
case inl.intro
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
h : M.Parallel' e f
X : Set α
he : M.Loop e
hf : M.Loop f
⊢ e ∈ M.cl X ↔ f ∈ M.cl X

case inr
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
h✝ : M.Parallel' e f
X : Set α
h : M.Parallel e f
⊢ e ∈ M.cl X ↔ f ∈ M.cl X
Theorem: Matroid.Parallel'.mem_cl_iff_mem_cl
Proof state before:
case inr
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
h✝ : M.Parallel' e f
X : Set α
h : M.Parallel e f
⊢ e ∈ M.cl X ↔ f ∈ M.cl X
Tactic:
exact h.mem_cl_iff_mem_cl
Proof state after:
no goals
Theorem: Matroid.Parallel'.mem_cl_iff_mem_cl
Proof state before:
case inl.intro
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
h : M.Parallel' e f
X : Set α
he : M.Loop e
hf : M.Loop f
⊢ e ∈ M.cl X ↔ f ∈ M.cl X
Tactic:
simp [he.mem_cl, hf.mem_cl]
Proof state after:
no goals
Theorem: Matroid.cl_range_of_forall_parallel'_subtype
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D X : Set α
φ : ↑X → α
h_para : ∀ (e : ↑X), M.Parallel' (↑e) (φ e)
⊢ M.cl (range φ) = M.cl X
Tactic:
simpa using M.cl_iUnion_congr (fun e ↦ {φ e}) (fun e ↦ {e.1}) (fun e ↦ (h_para e).cl_eq_cl.symm)
Proof state after:
no goals
Theorem: Matroid.cl_image_of_forall_parallel'_subtype
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D X : Set α
φ : ↑X → α
h_para : ∀ (e : ↑X), M.Parallel' (↑e) (φ e)
Y : Set ↑X
⊢ M.cl (φ '' Y) = M.cl ↑Y
Tactic:
convert M.cl_biUnion_congr (fun e : X ↦ {φ e}) (fun e ↦ {e.1}) Y
  (fun e _ ↦ (h_para e).cl_eq_cl.symm) <;> aesop
Proof state after:
no goals
Theorem: Matroid.cl_image_of_forall_parallel'
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
h_para : ∀ (e : α), M.Parallel' e (φ e)
X : Set α
⊢ M.cl (φ '' X) = M.cl X
Tactic:
rw [← cl_range_of_forall_parallel'_subtype (fun x : X ↦ φ x) (fun x ↦ h_para x), image_eq_range]
Proof state after:
no goals
Theorem: Matroid.isoOfMapParallelBijOn_apply_image
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
hφ : BijOn φ M.E M.E
h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)
X : Set ↑M.E
⊢ ↑(⇑(isoOfMapParallelBijOn hφ h_para) '' X) = φ '' ↑X
Tactic:
suffices ∀ (x y : α) (h : y ∈ M.E), ⟨y, h⟩ ∈ X → φ y = x → x ∈ M.E by simpa [Set.ext_iff]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
hφ : BijOn φ M.E M.E
h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)
X : Set ↑M.E
⊢ ∀ (x y : α) (h : y ∈ M.E), ⟨y, h⟩ ∈ X → φ y = x → x ∈ M.E
Theorem: Matroid.isoOfMapParallelBijOn_apply_image
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
hφ : BijOn φ M.E M.E
h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)
X : Set ↑M.E
⊢ ∀ (x y : α) (h : y ∈ M.E), ⟨y, h⟩ ∈ X → φ y = x → x ∈ M.E
Tactic:
rintro x y h - rfl
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
hφ : BijOn φ M.E M.E
h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)
X : Set ↑M.E
y : α
h : y ∈ M.E
⊢ φ y ∈ M.E
Theorem: Matroid.isoOfMapParallelBijOn_apply_image
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
hφ : BijOn φ M.E M.E
h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)
X : Set ↑M.E
y : α
h : y ∈ M.E
⊢ φ y ∈ M.E
Tactic:
exact (h_para y h).mem_ground_right
Proof state after:
no goals
Theorem: Matroid.isoOfMapParallelBijOn_apply_image
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
hφ : BijOn φ M.E M.E
h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)
X : Set ↑M.E
this : ∀ (x y : α) (h : y ∈ M.E), ⟨y, h⟩ ∈ X → φ y = x → x ∈ M.E
⊢ ↑(⇑(isoOfMapParallelBijOn hφ h_para) '' X) = φ '' ↑X
Tactic:
simpa [Set.ext_iff]
Proof state after:
no goals
Theorem: Matroid.isoOfSwapParallel_apply_image
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
inst✝ : DecidableEq α
h_para : M.Parallel' e f
X : Set ↑M.E
⊢ ↑(⇑(isoOfSwapParallel h_para) '' X) = ⇑(Equiv.swap e f) '' ↑X
Tactic:
rw [isoOfSwapParallel, isoOfMapParallelBijOn_apply_image]
Proof state after:
no goals
Theorem: Matroid.Indep.parallel'_substitute
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
⊢ M.Indep (insert f (I \ {e}))
Tactic:
convert (isoOfSwapParallel h_para).image_indep (I := M.E ↓∩ I)
  (by rwa [Subset.image_val_preimage_val_eq hI.subset_ground])
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 : M.Parallel' e f
heI : e ∈ I
⊢ insert f (I \ {e}) = ↑(⇑(isoOfSwapParallel h_para) '' M.E ↓∩ I)
Theorem: Matroid.Indep.parallel'_substitute
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 : M.Parallel' e f
heI : e ∈ I
⊢ insert f (I \ {e}) = ↑(⇑(isoOfSwapParallel h_para) '' M.E ↓∩ I)
Tactic:
simp only [isoOfSwapParallel_apply_image, Subtype.image_preimage_coe,
  inter_eq_self_of_subset_right hI.subset_ground]
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 : M.Parallel' e f
heI : e ∈ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' I
Theorem: Matroid.Indep.parallel'_substitute
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 : M.Parallel' e f
heI : e ∈ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' 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 α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
hfI : f ∈ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' I

case neg
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
hfI : f ∉ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' I
Theorem: Matroid.Indep.parallel'_substitute
Proof state before:
case neg
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
hfI : f ∉ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' I
Tactic:
rw [(Equiv.swap_bijOn_exchange heI hfI).image_eq]
Proof state after:
no goals
Theorem: Matroid.Indep.parallel'_substitute
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
⊢ M.Indep ↑(M.E ↓∩ I)
Tactic:
rwa [Subset.image_val_preimage_val_eq hI.subset_ground]
Proof state after:
no goals
Theorem: Matroid.Indep.parallel'_substitute
Proof state before:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
hfI : f ∈ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' I
Tactic:
obtain (rfl : e = f) := h_para.eq_of_indep (hI.subset (pair_subset heI hfI))
Proof state after:
case pos
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
hI : M.Indep I
heI : e ∈ I
h_para : M.Parallel' e e
hfI : e ∈ I
⊢ insert e (I \ {e}) = ⇑(Equiv.swap e e) '' I
Theorem: Matroid.Indep.parallel'_substitute
Proof state before:
case pos
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
hI : M.Indep I
heI : e ∈ I
h_para : M.Parallel' e e
hfI : e ∈ I
⊢ insert e (I \ {e}) = ⇑(Equiv.swap e e) '' I
Tactic:
simpa
Proof state after:
no goals
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
⊢ M.Indep I ↔ M.Indep (insert f (I \ {e}))
Tactic:
refine ⟨fun hI ↦ hI.parallel'_substitute h_para he, fun hI ↦ ?_⟩
Proof state after:
α : 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}))
⊢ M.Indep I
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}))
⊢ M.Indep I
Tactic:
convert hI.parallel'_substitute h_para.symm (mem_insert _ _)
Proof state after:
case h.e'_3
α : 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}))
⊢ I = insert e (insert f (I \ {e}) \ {f})
Theorem: Matroid.Parallel'.indep_substitute_iff
Proof state before:
case h.e'_3
α : 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}))
⊢ I = insert e (insert f (I \ {e}) \ {f})
Tactic:
have hef : e ≠ f := by rintro rfl; exact hf he
Proof state after:
case h.e'_3
α : 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}))
hef : e ≠ f
⊢ I = insert e (insert f (I \ {e}) \ {f})
Theorem: Matroid.Parallel'.indep_substitute_iff
Proof state before:
case h.e'_3
α : 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}))
hef : e ≠ f
⊢ I = insert e (insert f (I \ {e}) \ {f})
Tactic:
simp [insert_diff_singleton_comm hef, insert_eq_of_mem he, diff_singleton_eq_self hf]
Proof state after:
no goals