internlm/Lean-Github huggingface dataset:
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
simp only [show ¬M.Circuit C from fun h ↦ hf <| h.subset_ground hfC, hfC, true_and, false_or]
Proof state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
by_cases heC : e ∈ C
Proof state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∉ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∉ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
rw [← (M.parallelExtend_parallel he f).parallel'.eq_mapEquiv_swap, mapEquiv_circuit_iff,
  Equiv.symm_swap, Equiv.swap_comm, Equiv.swap_image_eq_exchange hfC heC, aux (by simp [hef.symm])]
Proof state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∉ C
⊢ M.Circuit (insert e (C \ {f})) ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∉ C
⊢ M.Circuit (insert e (C \ {f})) ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
simp [heC, show C ≠ {e,f} by rintro rfl; simp at heC]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ e ≠ f
Tactic:
rintro rfl
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
hf : e ∉ M.E
⊢ False
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
hf : e ∉ M.E
⊢ False
Tactic:
exact hf he.mem_ground
Proof state after:
no goals
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
⊢ ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
Tactic:
intro C' hfC'
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
C' : Set α
hfC' : f ∉ C'
⊢ (M.parallelExtend e f).Circuit C' ↔ M.Circuit C'
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
C' : Set α
hfC' : f ∉ C'
⊢ (M.parallelExtend e f).Circuit C' ↔ M.Circuit C'
Tactic:
suffices h' : ((M.parallelExtend e f) ＼ f).Circuit C' ↔ M.Circuit C' by
  simpa [deleteElem, delete_circuit_iff, hfC'] using h'
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
C' : Set α
hfC' : f ∉ C'
⊢ (M.parallelExtend e f ＼ f).Circuit C' ↔ M.Circuit C'
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
C' : Set α
hfC' : f ∉ C'
⊢ (M.parallelExtend e f ＼ f).Circuit C' ↔ M.Circuit C'
Tactic:
rw [parallelExtend_delete_eq _ hf]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
C' : Set α
hfC' : f ∉ C'
h' : (M.parallelExtend e f ＼ f).Circuit C' ↔ M.Circuit C'
⊢ (M.parallelExtend e f).Circuit C' ↔ M.Circuit C'
Tactic:
simpa [deleteElem, delete_circuit_iff, hfC'] using h'
Proof state after:
no goals
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
simp [aux hfC, hfC, show C ≠ {e,f} by rintro rfl; simp at hfC]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ C
⊢ C ≠ {e, f}
Tactic:
rintro rfl
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ {e, f}
⊢ False
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ {e, f}
⊢ False
Tactic:
simp at hfC
Proof state after:
no goals
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
suffices (M.parallelExtend e f).Circuit C ↔ C = {e, f} by simpa [heC]
Proof state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f}
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f}
Tactic:
have hC := (M.parallelExtend_parallel he f).circuit_of_ne hef
Proof state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
hC : (M.parallelExtend e f).Circuit {e, f}
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f}
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
hC : (M.parallelExtend e f).Circuit {e, f}
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f}
Tactic:
exact ⟨fun h ↦ Eq.symm <| hC.eq_of_subset_circuit h (by simp [pair_subset_iff, heC, hfC]),
  by rintro rfl; assumption⟩
Proof state after:
no goals
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
this : (M.parallelExtend e f).Circuit C ↔ C = {e, f}
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
simpa [heC]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
hC : (M.parallelExtend e f).Circuit {e, f}
h : (M.parallelExtend e f).Circuit C
⊢ {e, f} ⊆ C
Tactic:
simp [pair_subset_iff, heC, hfC]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
hC : (M.parallelExtend e f).Circuit {e, f}
⊢ C = {e, f} → (M.parallelExtend e f).Circuit C
Tactic:
rintro rfl
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hC : (M.parallelExtend e f).Circuit {e, f}
hfC : f ∈ {e, f}
heC : e ∈ {e, f}
⊢ (M.parallelExtend e f).Circuit {e, f}
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hC : (M.parallelExtend e f).Circuit {e, f}
hfC : f ∈ {e, f}
heC : e ∈ {e, f}
⊢ (M.parallelExtend e f).Circuit {e, f}
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∉ C
⊢ f ∉ insert e (C \ {f})
Tactic:
simp [hef.symm]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∉ C
⊢ C ≠ {e, f}
Tactic:
rintro rfl
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ {e, f}
heC : e ∉ {e, f}
⊢ False
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ {e, f}
heC : e ∉ {e, f}
⊢ False
Tactic:
simp at heC
Proof state after:
no goals
Theorem: Matroid.seriesExtend_dual
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
⊢ (M.seriesExtend e f)✶ = M✶.parallelExtend e f
Tactic:
rw [seriesExtend, dual_dual]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_dual
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
⊢ (M.parallelExtend e f)✶ = M✶.seriesExtend e f
Tactic:
rw [seriesExtend, dual_dual]
Proof state after:
no goals
Theorem: Matroid.seriesExtend_self
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f : α
M : Matroid α
e : α
⊢ M.seriesExtend e e = M.addColoop e
Tactic:
rw [seriesExtend, parallelExtend_self, addColoop]
Proof state after:
no goals
Theorem: Matroid.seriesExtend_coloop
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
he : M.Coloop e
f : α
⊢ M.seriesExtend e f = (M ／ f).addColoop f
Tactic:
rw [seriesExtend, parallelExtend_not_nonloop, addColoop, deleteElem, contract_elem,
  contract_dual_eq_dual_delete]
Proof state after:
case he
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
he : M.Coloop e
f : α
⊢ ¬M✶.Nonloop e
Theorem: Matroid.seriesExtend_coloop
Proof state before:
case he
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
he : M.Coloop e
f : α
⊢ ¬M✶.Nonloop e
Tactic:
simp [Nonloop, dual_loop_iff_coloop, he]
Proof state after:
no goals
Theorem: Matroid.seriesExtend_not_mem_ground
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
he : e ∉ M.E
f : α
⊢ M.seriesExtend e f = (M ／ f).addColoop f
Tactic:
rw [seriesExtend, parallelExtend_not_nonloop, addColoop, contract_elem, deleteElem,
  contract_dual_eq_dual_delete]
Proof state after:
case he
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
he : e ∉ M.E
f : α
⊢ ¬M✶.Nonloop e
Theorem: Matroid.seriesExtend_not_mem_ground
Proof state before:
case he
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
he : e ∉ M.E
f : α
⊢ ¬M✶.Nonloop e
Tactic:
simp [Nonloop, he]
Proof state after:
no goals
Theorem: Matroid.seriesExtend_eq_seriesExtend_contract
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
hef : e ≠ f
⊢ M.seriesExtend e f = (M ／ f).seriesExtend e f
Tactic:
rw [seriesExtend, parallelExtend_eq_parallelExtend_delete _ hef, seriesExtend]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
hef : e ≠ f
⊢ ((M✶ ＼ f).parallelExtend e f)✶ = ((M ／ f)✶.parallelExtend e f)✶
Theorem: Matroid.seriesExtend_eq_seriesExtend_contract
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
hef : e ≠ f
⊢ ((M✶ ＼ f).parallelExtend e f)✶ = ((M ／ f)✶.parallelExtend e f)✶
Tactic:
simp only [deleteElem, contract_elem, contract_dual_eq_dual_delete]
Proof state after:
no goals
Theorem: Matroid.seriesExtend_contract_eq'
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
⊢ M.seriesExtend e f ／ f = M ／ f
Tactic:
rw [seriesExtend, contract_elem, ← delete_dual_eq_dual_contract, ← deleteElem,
  parallelExtend_delete_eq']
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
⊢ (M✶ ＼ f)✶ = M ／ f
Theorem: Matroid.seriesExtend_contract_eq'
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
⊢ (M✶ ＼ f)✶ = M ／ f
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.seriesExtend_contract_eq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e✝ f e : α
hf : f ∉ M.E
⊢ M.seriesExtend e f ／ f = M
Tactic:
rw [seriesExtend, contract_elem, ← delete_dual_eq_dual_contract, ← deleteElem,
  parallelExtend_delete_eq _ (show f ∉ M✶.E from hf), dual_dual]
Proof state after:
no goals
Theorem: Matroid.seriesExtend_series
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
heE : e ∈ M.E
he : ¬M.Coloop e
f : α
⊢ (M.seriesExtend e f).Series e f
Tactic:
rw [Series, seriesExtend, dual_dual]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
heE : e ∈ M.E
he : ¬M.Coloop e
f : α
⊢ (M✶.parallelExtend e f).Parallel e f
Theorem: Matroid.seriesExtend_series
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
heE : e ∈ M.E
he : ¬M.Coloop e
f : α
⊢ (M✶.parallelExtend e f).Parallel e f
Tactic:
apply parallelExtend_parallel
Proof state after:
case he
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
heE : e ∈ M.E
he : ¬M.Coloop e
f : α
⊢ M✶.Nonloop e
Theorem: Matroid.seriesExtend_series
Proof state before:
case he
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
heE : e ∈ M.E
he : ¬M.Coloop e
f : α
⊢ M✶.Nonloop e
Tactic:
rwa [Nonloop, dual_ground, and_iff_left heE, dual_loop_iff_coloop]
Proof state after:
no goals
Theorem: Matroid.eq_seriesExtend_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f : α
heE : e ∈ M.E
he : ¬M.Coloop e
hf : f ∉ M.E
⊢ M' = M.seriesExtend e f ↔ M'.Series e f ∧ M' ／ f = M
Tactic:
rw [seriesExtend, eq_dual_comm, eq_comm, eq_parallelExtend_iff _ (show f ∉ M✶.E from hf),
  deleteElem, ← contract_dual_eq_dual_delete, ← contract_elem, dual_inj, Series]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f : α
heE : e ∈ M.E
he : ¬M.Coloop e
hf : f ∉ M.E
⊢ M✶.Nonloop e
Theorem: Matroid.eq_seriesExtend_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f : α
heE : e ∈ M.E
he : ¬M.Coloop e
hf : f ∉ M.E
⊢ M✶.Nonloop e
Tactic:
rwa [Nonloop, and_iff_left (show e ∈ M✶.E from heE), dual_loop_iff_coloop]
Proof state after:
no goals
Theorem: Matroid.erk_eq_er_ground
Proof state before:
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
⊢ M.erk = M.er M.E
Tactic:
rw [er, restrict_ground_eq_self]
Proof state after:
no goals
Theorem: Matroid.Basis'.encard
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : M.Basis' I X
⊢ I.encard = M.er X
Tactic:
rw [er,erk]
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : M.Basis' I X
⊢ I.encard = ⨅ B, (↑B).encard
Theorem: Matroid.Basis'.encard
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : M.Basis' I X
⊢ I.encard = ⨅ B, (↑B).encard
Tactic:
rw [← base_restrict_iff'] at hI
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : (M ↾ X).Base I
⊢ I.encard = ⨅ B, (↑B).encard
Theorem: Matroid.Basis'.encard
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : (M ↾ X).Base I
⊢ I.encard = ⨅ B, (↑B).encard
Tactic:
have : _root_.Nonempty ↑{B | (M ↾ X).Base B} := ⟨I, hI⟩
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : (M ↾ X).Base I
this : Nonempty ↑{B | (M ↾ X).Base B}
⊢ I.encard = ⨅ B, (↑B).encard
Theorem: Matroid.Basis'.encard
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : (M ↾ X).Base I
this : Nonempty ↑{B | (M ↾ X).Base B}
⊢ I.encard = ⨅ B, (↑B).encard
Tactic:
rw [iInf_congr (_ : ∀ B : ↑{B | (M ↾ X).Base B}, (B : Set α).encard = I.encard), iInf_const]
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : (M ↾ X).Base I
this : Nonempty ↑{B | (M ↾ X).Base B}
⊢ ∀ (B : ↑{B | (M ↾ X).Base B}), (↑B).encard = I.encard
Theorem: Matroid.Basis'.encard
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : (M ↾ X).Base I
this : Nonempty ↑{B | (M ↾ X).Base B}
⊢ ∀ (B : ↑{B | (M ↾ X).Base B}), (↑B).encard = I.encard
Tactic:
simp only [mem_setOf_eq, Subtype.forall]
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : (M ↾ X).Base I
this : Nonempty ↑{B | (M ↾ X).Base B}
⊢ ∀ (a : Set α), (M ↾ X).Base a → a.encard = I.encard
Theorem: Matroid.Basis'.encard
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : (M ↾ X).Base I
this : Nonempty ↑{B | (M ↾ X).Base B}
⊢ ∀ (a : Set α), (M ↾ X).Base a → a.encard = I.encard
Tactic:
exact fun B' hB' ↦ hB'.card_eq_card_of_base hI
Proof state after:
no goals
Theorem: Matroid.eq_er_iff
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : autoParam (X ⊆ M.E) _auto✝
h : M.er X = n
I : Set α
hI : M.Basis I X
⊢ I.encard = n
Tactic:
rw [hI.encard, ← h]
Proof state after:
no goals
Theorem: Matroid.eq_er_iff
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ I, M.Basis I X ∧ I.encard = n
I : Set α
hI : M.Basis I X
hIc : I.encard = n
⊢ M.er X = n
Tactic:
rw [← hI.encard, hIc]
Proof state after:
no goals
Theorem: Matroid.Basis'.er
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIX : M.Basis' I X
⊢ M.er I = M.er X
Tactic:
rw [← hIX.encard, hIX.indep.er]
Proof state after:
no goals
Theorem: Matroid.Basis.er
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIX : M.Basis I X
⊢ M.er I = M.er X
Tactic:
rw [← hIX.encard, hIX.indep.er]
Proof state after:
no goals
Theorem: Matroid.Basis'.er_eq_encard
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIX : M.Basis' I X
⊢ M.er X = I.encard
Tactic:
rw [← hIX.er, hIX.indep.er]
Proof state after:
no goals
Theorem: Matroid.Basis.er_eq_encard
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIX : M.Basis I X
⊢ M.er X = I.encard
Tactic:
rw [← hIX.er, hIX.indep.er]
Proof state after:
no goals
Theorem: Matroid.Base.er
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hB : M.Base B
⊢ M.er B = M.erk
Tactic:
rw [hB.indep.er, erk_eq_er_ground, hB.basis_ground.encard]
Proof state after:
no goals
Theorem: Matroid.Base.encard
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hB : M.Base B
⊢ B.encard = M.erk
Tactic:
rw [hB.basis_ground.encard, erk_eq_er_ground]
Proof state after:
no goals
Theorem: Matroid.erk_map
Proof state before:
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f✝ : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).erk = M.erk
Tactic:
obtain ⟨B, hB⟩ := M.exists_base
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f✝ : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.Base B
⊢ (M.map f hf).erk = M.erk
Theorem: Matroid.erk_map
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f✝ : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.Base B
⊢ (M.map f hf).erk = M.erk
Tactic:
rw [← (hB.map hf).encard, ← hB.encard, (hf.mono hB.subset_ground).encard_image]
Proof state after:
no goals
Theorem: Matroid.erk_loopyOn
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
E : Set α
⊢ (loopyOn E).erk = 0
Tactic:
simp [← (show (loopyOn E).Base ∅ by simp).encard]
Proof state after:
no goals
Theorem: Matroid.erk_loopyOn
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
E : Set α
⊢ (loopyOn E).Base ∅
Tactic:
simp
Proof state after:
no goals