internlm/Lean-Github huggingface dataset:
Theorem: Matroid.simple_uniqueBaseOn_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D E : Set α
⊢ E ⊆ I → ∀ ⦃e f : α⦄, e ∈ E → f ∈ E → (e ∈ I ∧ f ∈ I) ∧ e ∈ E ∧ f ∈ E
Tactic:
tauto
Proof state after:
no goals
Theorem: Matroid.Simple.map
Proof state before:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Simple
Tactic:
simp only [simple_iff_forall_pair_indep, map_ground, mem_image, map_indep_iff,
  forall_exists_index, and_imp]
Proof state after:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
⊢ ∀ ⦃e f_1 : β⦄, ∀ x ∈ M.E, f x = e → ∀ x ∈ M.E, f x = f_1 → ∃ I₀, M.Indep I₀ ∧ {e, f_1} = f '' I₀
Theorem: Matroid.Simple.map
Proof state before:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
⊢ ∀ ⦃e f_1 : β⦄, ∀ x ∈ M.E, f x = e → ∀ x ∈ M.E, f x = f_1 → ∃ I₀, M.Indep I₀ ∧ {e, f_1} = f '' I₀
Tactic:
rintro _ _ x hx rfl y hy rfl
Proof state after:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
x : α
hx : x ∈ M.E
y : α
hy : y ∈ M.E
⊢ ∃ I₀, M.Indep I₀ ∧ {f x, f y} = f '' I₀
Theorem: Matroid.Simple.map
Proof state before:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
x : α
hx : x ∈ M.E
y : α
hy : y ∈ M.E
⊢ ∃ I₀, M.Indep I₀ ∧ {f x, f y} = f '' I₀
Tactic:
exact ⟨_, pair_indep hx hy, by simp [image_insert_eq]⟩
Proof state after:
no goals
Theorem: Matroid.Simple.map
Proof state before:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
x : α
hx : x ∈ M.E
y : α
hy : y ∈ M.E
⊢ {f x, f y} = f '' {x, y}
Tactic:
simp [image_insert_eq]
Proof state after:
no goals
Theorem: Matroid.Simple.of_iso
Proof state before:
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
⊢ N.Simple
Tactic:
obtain (h | h) := isEmpty_or_nonempty β
Proof state after:
case inl
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : IsEmpty β
⊢ N.Simple

case inr
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : Nonempty β
⊢ N.Simple
Theorem: Matroid.Simple.of_iso
Proof state before:
case inr
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : Nonempty β
⊢ N.Simple
Tactic:
obtain ⟨f, hf, rfl⟩ := i.exists_eq_map
Proof state after:
case inr.intro.intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
h : Nonempty β
f : α → β
hf : InjOn f M.E
i : M ≂ M.map f hf
⊢ (M.map f hf).Simple
Theorem: Matroid.Simple.of_iso
Proof state before:
case inr.intro.intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
h : Nonempty β
f : α → β
hf : InjOn f M.E
i : M ≂ M.map f hf
⊢ (M.map f hf).Simple
Tactic:
exact hM.map hf
Proof state after:
no goals
Theorem: Matroid.Simple.of_iso
Proof state before:
case inl
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : IsEmpty β
⊢ N.Simple
Tactic:
rw [eq_emptyOn N]
Proof state after:
case inl
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : IsEmpty β
⊢ (emptyOn β).Simple
Theorem: Matroid.Simple.of_iso
Proof state before:
case inl
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : IsEmpty β
⊢ (emptyOn β).Simple
Tactic:
infer_instance
Proof state after:
no goals
Theorem: Matroid.simple_iff_forall_parallel_class
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple ↔ ∀ P ∈ M.parallelClasses, P.encard = 1
Tactic:
simp only [mem_parallelClasses_iff, forall_exists_index, and_imp, encard_eq_one]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple ↔ ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
Theorem: Matroid.simple_iff_forall_parallel_class
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple ↔ ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
Tactic:
refine ⟨?_, fun h ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple → ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}

case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
⊢ M.Simple
Theorem: Matroid.simple_iff_forall_parallel_class
Proof state before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
⊢ M.Simple
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall, and_iff_right (by assumption)]
Proof state after:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
⊢ ∀ (e f : α), M.Parallel e f → e = f
Theorem: Matroid.simple_iff_forall_parallel_class
Proof state before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
⊢ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
refine fun e f hef ↦ ?_
Proof state after:
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
e f : α
hef : M.Parallel e f
⊢ e = f
Theorem: Matroid.simple_iff_forall_parallel_class
Proof state before:
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
e f : α
hef : M.Parallel e f
⊢ e = f
Tactic:
obtain ⟨x, hx⟩ := h _ e hef.nonloop_left rfl
Proof state after:
case refine_2.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
e f : α
hef : M.Parallel e f
x : α
hx : {f | M.Parallel e f} = {x}
⊢ e = f
Theorem: Matroid.simple_iff_forall_parallel_class
Proof state before:
case refine_2.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
e f : α
hef : M.Parallel e f
x : α
hx : {f | M.Parallel e f} = {x}
⊢ e = f
Tactic:
rw [(show f = x from hx.subset hef), show e = x from hx.subset (hef.nonloop_left.parallel_self)]
Proof state after:
no goals
Theorem: Matroid.simple_iff_forall_parallel_class
Proof state before:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple → ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
Tactic:
rintro h P x hx rfl
Proof state after:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : M.Simple
x : α
hx : M.Nonloop x
⊢ ∃ x_1, {f | M.Parallel x f} = {x_1}
Theorem: Matroid.simple_iff_forall_parallel_class
Proof state before:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : M.Simple
x : α
hx : M.Nonloop x
⊢ ∃ x_1, {f | M.Parallel x f} = {x_1}
Tactic:
exact ⟨x, by simp [Set.ext_iff, parallel_iff_eq hx.mem_ground]⟩
Proof state after:
no goals
Theorem: Matroid.simple_iff_forall_parallel_class
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : M.Simple
x : α
hx : M.Nonloop x
⊢ {f | M.Parallel x f} = {x}
Tactic:
simp [Set.ext_iff, parallel_iff_eq hx.mem_ground]
Proof state after:
no goals
Theorem: Matroid.simple_iff_forall_parallel_class
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
⊢ M.Loopless
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.simple_iff_parallelClasses_eq_discrete'
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
Tactic:
refine ⟨fun h ↦ ⟨by infer_instance, Partition.eq_of_rel_iff_rel ?_⟩, fun ⟨_,h⟩ ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ ∀ (x y : α), M.parallelClasses.Rel x y ↔ (Partition.discrete {e | M.Nonloop e}).Rel x y

case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
left✝ : M.Loopless
h : M.parallelClasses = Partition.discrete {e | M.Nonloop e}
⊢ M.Simple
Theorem: Matroid.simple_iff_parallelClasses_eq_discrete'
Proof state before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
left✝ : M.Loopless
h : M.parallelClasses = Partition.discrete {e | M.Nonloop e}
⊢ M.Simple
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall, and_iff_right (by assumption)]
Proof state after:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
left✝ : M.Loopless
h : M.parallelClasses = Partition.discrete {e | M.Nonloop e}
⊢ ∀ (e f : α), M.Parallel e f → e = f
Theorem: Matroid.simple_iff_parallelClasses_eq_discrete'
Proof state before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
left✝ : M.Loopless
h : M.parallelClasses = Partition.discrete {e | M.Nonloop e}
⊢ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
simp [Parallel, h]
Proof state after:
no goals
Theorem: Matroid.simple_iff_parallelClasses_eq_discrete'
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ M.Loopless
Tactic:
infer_instance
Proof state after:
no goals
Theorem: Matroid.simple_iff_parallelClasses_eq_discrete'
Proof state before:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ ∀ (x y : α), M.parallelClasses.Rel x y ↔ (Partition.discrete {e | M.Nonloop e}).Rel x y
Tactic:
simp only [Partition.discrete.rel_iff_eq, mem_setOf_eq,
  show M.parallelClasses.Rel = M.Parallel from rfl]
Proof state after:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ ∀ (x y : α), M.Parallel x y ↔ x = y ∧ M.Nonloop x
Theorem: Matroid.simple_iff_parallelClasses_eq_discrete'
Proof state before:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ ∀ (x y : α), M.Parallel x y ↔ x = y ∧ M.Nonloop x
Tactic:
exact fun x y ↦ ⟨fun h ↦ ⟨h.eq, h.nonloop_left⟩, by rintro ⟨rfl, h⟩; exact h.parallel_self⟩
Proof state after:
no goals
Theorem: Matroid.simple_iff_parallelClasses_eq_discrete'
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
x y : α
⊢ x = y ∧ M.Nonloop x → M.Parallel x y
Tactic:
rintro ⟨rfl, h⟩
Proof state after:
case intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h✝ : M.Simple
x : α
h : M.Nonloop x
⊢ M.Parallel x x
Theorem: Matroid.simple_iff_parallelClasses_eq_discrete'
Proof state before:
case intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h✝ : M.Simple
x : α
h : M.Nonloop x
⊢ M.Parallel x x
Tactic:
exact h.parallel_self
Proof state after:
no goals
Theorem: Matroid.simple_iff_parallelClasses_eq_discrete'
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
left✝ : M.Loopless
h : M.parallelClasses = Partition.discrete {e | M.Nonloop e}
⊢ M.Loopless
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.simple_iff_parallelClasses_eq_discrete
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple ↔ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
Tactic:
rw [simple_iff_parallelClasses_eq_discrete', and_iff_right (by assumption)]
Proof state after:
no goals
Theorem: Matroid.simple_iff_parallelClasses_eq_discrete
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Loopless
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.parallelClasses_eq_discrete
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
⊢ M.Simple
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.Simple.eq_of_parallel_of_mem
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : (M ↾ X).Simple
he : e ∈ X
hf : f ∈ X
hef : M.Parallel e f
⊢ ↑⟨e, he⟩ ∈ (M ↾ X).E
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Simple.eq_of_parallel_of_mem
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : (M ↾ X).Simple
he : e ∈ X
hf : f ∈ X
hef : M.Parallel e f
⊢ (M ↾ X).Parallel ↑⟨e, he⟩ ↑⟨f, hf⟩
Tactic:
simp [restrict_parallel_iff, hef, he, hf]
Proof state after:
no goals
Theorem: Matroid.exists_loop_or_para_of_not_simple
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬M.Simple
⊢ (∃ e, M.Loop e) ∨ ∃ e f, M.Parallel e f ∧ e ≠ f
Tactic:
by_contra! h
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬M.Simple
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
⊢ False
Theorem: Matroid.exists_loop_or_para_of_not_simple
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬M.Simple
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
⊢ False
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall, loopless_iff_forall_not_loop] at hM
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬((∀ e ∈ M.E, ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f)
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
⊢ False
Theorem: Matroid.exists_loop_or_para_of_not_simple
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬((∀ e ∈ M.E, ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f)
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
⊢ False
Tactic:
push_neg at hM
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
hM : (∀ e ∈ M.E, ¬M.Loop e) → ∃ e f, M.Parallel e f ∧ e ≠ f
⊢ False
Theorem: Matroid.exists_loop_or_para_of_not_simple
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
hM : (∀ e ∈ M.E, ¬M.Loop e) → ∃ e f, M.Parallel e f ∧ e ≠ f
⊢ False
Tactic:
obtain ⟨e, f, hef, hne⟩ := hM (fun e _ ↦ h.1 e)
Proof state after:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
hM : (∀ e ∈ M.E, ¬M.Loop e) → ∃ e f, M.Parallel e f ∧ e ≠ f
e f : α
hef : M.Parallel e f
hne : e ≠ f
⊢ False
Theorem: Matroid.exists_loop_or_para_of_not_simple
Proof state before:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
hM : (∀ e ∈ M.E, ¬M.Loop e) → ∃ e f, M.Parallel e f ∧ e ≠ f
e f : α
hef : M.Parallel e f
hne : e ≠ f
⊢ False
Tactic:
exact hne <| h.2 e f hef
Proof state after:
no goals
Theorem: Matroid.Indep.restr_simple
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
⊢ (M ↾ I).Simple
Tactic:
simp only [simple_iff_forall_pair_indep, restrict_ground_eq, mem_singleton_iff,
  restrict_indep_iff, pair_subset_iff]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
⊢ ∀ ⦃e f : α⦄, e ∈ I → f ∈ I → M.Indep {e, f} ∧ e ∈ I ∧ f ∈ I
Theorem: Matroid.Indep.restr_simple
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
⊢ ∀ ⦃e f : α⦄, e ∈ I → f ∈ I → M.Indep {e, f} ∧ e ∈ I ∧ f ∈ I
Tactic:
rintro e f he hf
Proof state after:
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
hI : M.Indep I
e f : α
he : e ∈ I
hf : f ∈ I
⊢ M.Indep {e, f} ∧ e ∈ I ∧ f ∈ I
Theorem: Matroid.Indep.restr_simple
Proof state before:
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
hI : M.Indep I
e f : α
he : e ∈ I
hf : f ∈ I
⊢ M.Indep {e, f} ∧ e ∈ I ∧ f ∈ I
Tactic:
exact ⟨hI.subset (pair_subset he hf), he, hf⟩
Proof state after:
no goals
Theorem: Matroid.Simple.subset
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D X Y : Set α
hY : (M ↾ Y).Simple
hXY : X ⊆ Y
⊢ (M ↾ X).Simple
Tactic:
simp only [simple_iff_forall_pair_indep, restrict_ground_eq, mem_singleton_iff,
  restrict_indep_iff, pair_subset_iff] at *
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D X Y : Set α
hXY : X ⊆ Y
hY : ∀ ⦃e f : α⦄, e ∈ Y → f ∈ Y → M.Indep {e, f} ∧ e ∈ Y ∧ f ∈ Y
⊢ ∀ ⦃e f : α⦄, e ∈ X → f ∈ X → M.Indep {e, f} ∧ e ∈ X ∧ f ∈ X
Theorem: Matroid.Simple.subset
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D X Y : Set α
hXY : X ⊆ Y
hY : ∀ ⦃e f : α⦄, e ∈ Y → f ∈ Y → M.Indep {e, f} ∧ e ∈ Y ∧ f ∈ Y
⊢ ∀ ⦃e f : α⦄, e ∈ X → f ∈ X → M.Indep {e, f} ∧ e ∈ X ∧ f ∈ X
Tactic:
aesop
Proof state after:
no goals
Theorem: Matroid.Loopless.of_restrict_contract
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless
h : (M ／ C).Loopless
⊢ M.Loopless
Tactic:
rw [loopless_iff_cl_empty] at *
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).cl ∅ = ∅
h : (M ／ C).cl ∅ = ∅
⊢ M.cl ∅ = ∅
Theorem: Matroid.Loopless.of_restrict_contract
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).cl ∅ = ∅
h : (M ／ C).cl ∅ = ∅
⊢ M.cl ∅ = ∅
Tactic:
rw [contract_loops_eq, diff_eq_empty] at h
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).cl ∅ = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ = ∅
Theorem: Matroid.Loopless.of_restrict_contract
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).cl ∅ = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ = ∅
Tactic:
rw [restrict_cl_eq', empty_inter, union_empty_iff] at hC
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : M.cl ∅ ∩ C = ∅ ∧ C \ M.E = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ = ∅
Theorem: Matroid.Loopless.of_restrict_contract
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : M.cl ∅ ∩ C = ∅ ∧ C \ M.E = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ = ∅
Tactic:
rw [← inter_union_diff (s := M.cl ∅) (t := C), hC.1, empty_union, diff_eq_empty]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : M.cl ∅ ∩ C = ∅ ∧ C \ M.E = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ ⊆ C
Theorem: Matroid.Loopless.of_restrict_contract
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : M.cl ∅ ∩ C = ∅ ∧ C \ M.E = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ ⊆ C
Tactic:
exact (M.cl_subset_cl <| empty_subset C).trans h
Proof state after:
no goals
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Simple
h : (M ／ C).Simple
⊢ M.Simple
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall] at h hC ⊢
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless ∧ ∀ (e f : α), (M ↾ C).Parallel e f → e = f
h : (M ／ C).Loopless ∧ ∀ (e f : α), (M ／ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless ∧ ∀ (e f : α), (M ↾ C).Parallel e f → e = f
h : (M ／ C).Loopless ∧ ∀ (e f : α), (M ／ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
obtain ⟨hl, h⟩ := h
Proof state after:
case intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless ∧ ∀ (e f : α), (M ↾ C).Parallel e f → e = f
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless ∧ ∀ (e f : α), (M ↾ C).Parallel e f → e = f
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
obtain ⟨hCl, hC⟩ := hC
Proof state after:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), (M ↾ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), (M ↾ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
simp only [restrict_parallel_iff, and_imp] at hC
Proof state after:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
refine ⟨(hCl.of_restrict_contract hl), fun e f hef ↦ ?_⟩
Proof state after:
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
⊢ e = f
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
⊢ e = f
Tactic:
by_cases heC : e ∈ C
Proof state after:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
⊢ e = f

case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
⊢ e = f
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
⊢ e = f
Tactic:
by_cases hfC : f ∈ C
Proof state after:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∈ C
⊢ e = f

case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∉ C
⊢ e = f