internlm/Lean-Github huggingface dataset:
Theorem: Matroid.simplification_isSimplification
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f g : α
I X P D : Set α
M : Matroid α
⊢ M.simplification.IsSimplification M
Tactic:
let f := M.removeLoops.parallelClasses.nonempty_repFun.some
Proof state after:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.simplification.IsSimplification M
Theorem: Matroid.simplification_isSimplification
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.simplification.IsSimplification M
Tactic:
refine ⟨Partition.RepFun.mk f (fun a ha ↦ f.apply_of_not_mem (by simpa))
  (fun a ha ↦ by simpa [mem_setOf_eq, parallelClasses_rel_eq] using f.rel_apply (by simpa))
  (fun a b hab ↦ f.apply_eq_apply (by simpa)), ?_⟩
Proof state after:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.simplification =
    M ↾
      ⇑{ toFun := ⇑f, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯, apply_eq_of_rel := ⋯ } '' {e | M.Nonloop e}
Theorem: Matroid.simplification_isSimplification
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.simplification =
    M ↾
      ⇑{ toFun := ⇑f, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯, apply_eq_of_rel := ⋯ } '' {e | M.Nonloop e}
Tactic:
simp only [simplification, removeLoops_nonloop_iff, Partition.RepFun.mk_apply]
Proof state after:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.removeLoops ↾ ⇑⋯.some '' {e | M.Nonloop e} = M ↾ (fun a => f a) '' {e | M.Nonloop e}
Theorem: Matroid.simplification_isSimplification
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.removeLoops ↾ ⇑⋯.some '' {e | M.Nonloop e} = M ↾ (fun a => f a) '' {e | M.Nonloop e}
Tactic:
rw [removeLoops_restr_eq_restr]
Proof state after:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ ⇑⋯.some '' {e | M.Nonloop e} ⊆ {e | M.Nonloop e}
Theorem: Matroid.simplification_isSimplification
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ ⇑⋯.some '' {e | M.Nonloop e} ⊆ {e | M.Nonloop e}
Tactic:
simpa only [M.removeLoops_nonloop_iff] using f.image_subset_self
Proof state after:
no goals
Theorem: Matroid.simplification_isSimplification
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
a : α
ha : a ∉ {e | M.Nonloop e}
⊢ a ∉ {e | M.removeLoops.Nonloop e}
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.simplification_isSimplification
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
a : α
ha : a ∈ {e | M.Nonloop e}
⊢ M.parallelClasses.Rel a (f a)
Tactic:
simpa [mem_setOf_eq, parallelClasses_rel_eq] using f.rel_apply (by simpa)
Proof state after:
no goals
Theorem: Matroid.simplification_isSimplification
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
a : α
ha : a ∈ {e | M.Nonloop e}
⊢ a ∈ {e | M.removeLoops.Nonloop e}
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.simplification_isSimplification
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
a b : α
hab : M.parallelClasses.Rel a b
⊢ M.removeLoops.parallelClasses.Rel a b
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.simplification_eq_self
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
⊢ M.simplification = M
Tactic:
rwa [IsSimplification.eq_self_iff M.simplification_isSimplification]
Proof state after:
no goals
Theorem: Matroid.simplification_eq_self_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.simplification = M
⊢ M.Simple
Tactic:
rw [← h]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.simplification = M
⊢ M.simplification.Simple
Theorem: Matroid.simplification_eq_self_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.simplification = M
⊢ M.simplification.Simple
Tactic:
exact M.simplification_simple
Proof state after:
no goals
Theorem: Matroid.simplification_factorsThrough_removeLoops
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝¹ x✝ : Matroid α
h : x✝¹.removeLoops = x✝.removeLoops
⊢ x✝¹.simplification = x✝.simplification
Tactic:
rw [simplification, h, simplification]
Proof state after:
no goals
Theorem: Matroid.simplification_removeLoops_eq
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f g : α
I X P D : Set α
M : Matroid α
⊢ M.removeLoops.simplification = M.simplification
Tactic:
rw [removeLoops_eq_delete, simplification_delete_eq_of_subset_loops M Subset.rfl]
Proof state after:
no goals
Theorem: Matroid.simplification_idem
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f g : α
I X P D : Set α
M : Matroid α
⊢ M.simplification.simplification = M.simplification
Tactic:
rw [simplification_eq_self_iff]
Proof state after:
α : Type u_1
M✝ N : Matroid α
e f g : α
I X P D : Set α
M : Matroid α
⊢ M.simplification.Simple
Theorem: Matroid.simplification_idem
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f g : α
I X P D : Set α
M : Matroid α
⊢ M.simplification.Simple
Tactic:
exact M.simplification_simple
Proof state after:
no goals
Theorem: Matroid.Minor.exists_minor_isSimplification
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hNM : N ≤m M
hN : N.Simple
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Tactic:
obtain ⟨I, hI, hr, -⟩ := hNM.exists_contract_spanning_restrict
Proof state after:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Theorem: Matroid.Minor.exists_minor_isSimplification
Proof state before:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Tactic:
have hN' := hr.eq_restrict ▸
  M.contract_restrict_eq_restrict_contract _ _ (subset_diff.1 hr.subset).2.symm
Proof state after:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Theorem: Matroid.Minor.exists_minor_isSimplification
Proof state before:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Tactic:
have h : (M ↾ (N.E ∪ I)).Simple := by
  apply Indep.simple_of_contract_simple (I := I) _ (by rwa [← hN'])
  refine restrict_indep_iff.2 ⟨hI, subset_union_right⟩
Proof state after:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h : (M ↾ (N.E ∪ I)).Simple
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Theorem: Matroid.Minor.exists_minor_isSimplification
Proof state before:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h : (M ↾ (N.E ∪ I)).Simple
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Tactic:
obtain ⟨M₀, hM₀, h⟩ := h.exists_restriction_isSimplification_of_restriction (M := M)
  (restrict_restriction _ _ (union_subset hNM.subset hI.subset_ground))
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Theorem: Matroid.Minor.exists_minor_isSimplification
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Tactic:
refine ⟨M₀, Minor.trans ?_ h.minor, hM₀⟩
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ N ≤m M ↾ (N.E ∪ I)
Theorem: Matroid.Minor.exists_minor_isSimplification
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ N ≤m M ↾ (N.E ∪ I)
Tactic:
rw [hN']
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ (M ↾ (N.E ∪ I)) ／ I ≤m M ↾ (((M ↾ (N.E ∪ I)) ／ I).E ∪ I)
Theorem: Matroid.Minor.exists_minor_isSimplification
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ (M ↾ (N.E ∪ I)) ／ I ≤m M ↾ (((M ↾ (N.E ∪ I)) ／ I).E ∪ I)
Tactic:
simpa using contract_minor _ _
Proof state after:
no goals
Theorem: Matroid.Minor.exists_minor_isSimplification
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ (M ↾ (N.E ∪ I)).Simple
Tactic:
apply Indep.simple_of_contract_simple (I := I) _ (by rwa [← hN'])
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ (M ↾ (N.E ∪ I)).Indep I
Theorem: Matroid.Minor.exists_minor_isSimplification
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ (M ↾ (N.E ∪ I)).Indep I
Tactic:
refine restrict_indep_iff.2 ⟨hI, subset_union_right⟩
Proof state after:
no goals
Theorem: Matroid.Minor.exists_minor_isSimplification
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ ((M ↾ (N.E ∪ I)) ／ I).Simple
Tactic:
rwa [← hN']
Proof state after:
no goals
Theorem: Matroid.Simple.minor_iff_minor_simplification
Proof state before:
α : Type u_1
M✝ N : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
⊢ Nonempty (N ≤i M) ↔ Nonempty (N ≤i M.simplification)
Tactic:
refine ⟨fun ⟨e⟩ ↦ ?_, fun ⟨e⟩ ↦ ⟨e.trans M.simplification_restriction.minor.isoMinor⟩⟩
Proof state after:
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
⊢ Nonempty (N ≤i M.simplification)
Theorem: Matroid.Simple.minor_iff_minor_simplification
Proof state before:
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
⊢ Nonempty (N ≤i M.simplification)
Tactic:
obtain ⟨M₀, hM₀, ⟨i, -⟩⟩ := e.exists_iso
Proof state after:
case intro.intro.intro
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
M₀ : Matroid β
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ Nonempty (N ≤i M.simplification)
Theorem: Matroid.Simple.minor_iff_minor_simplification
Proof state before:
case intro.intro.intro
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
M₀ : Matroid β
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ Nonempty (N ≤i M.simplification)
Tactic:
obtain ⟨M', hM₀M', hM'⟩ := hM₀.exists_minor_isSimplification (hN.of_iso i)
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
M₀ : Matroid β
hM₀ : M₀ ≤m M
i : N ≂ M₀
M' : Matroid β
hM₀M' : M₀ ≤m M'
hM' : M'.IsSimplification M
⊢ Nonempty (N ≤i M.simplification)
Theorem: Matroid.Simple.minor_iff_minor_simplification
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
M₀ : Matroid β
hM₀ : M₀ ≤m M
i : N ≂ M₀
M' : Matroid β
hM₀M' : M₀ ≤m M'
hM' : M'.IsSimplification M
⊢ Nonempty (N ≤i M.simplification)
Tactic:
exact ⟨i.isoMinor.trans
  (hM₀M'.isoMinor.trans (hM'.iso (M.simplification_isSimplification)).isoMinor)⟩
Proof state after:
no goals
Theorem: Matroid.insert_base_of_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
⊢ M.Base (insert f I)
Tactic:
obtain (rfl | hef) := eq_or_ne e f
Proof state after:
case inl
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∉ I
heI : M.Base (insert e I)
hf : e ∉ I
hfI : M.Indep (insert e I)
⊢ M.Base (insert e I)

case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.Base (insert f I)
Theorem: Matroid.insert_base_of_insert_indep
Proof state before:
case inl
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∉ I
heI : M.Base (insert e I)
hf : e ∉ I
hfI : M.Indep (insert e I)
⊢ M.Base (insert e I)

case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.Base (insert f I)
Tactic:
assumption
Proof state after:
case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.Base (insert f I)
Theorem: Matroid.insert_base_of_insert_indep
Proof state before:
case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.Base (insert f I)
Tactic:
simpa [diff_singleton_eq_self he, hfI]
  using heI.exchange_base_of_indep (e := e) (f := f) (by simp [hef.symm, hf])
Proof state after:
no goals
Theorem: Matroid.insert_base_of_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ f ∉ insert e I
Tactic:
simp [hef.symm, hf]
Proof state after:
no goals
Theorem: Matroid.Indep.base_of_forall_insert
Proof state before:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
⊢ M.Base B
Tactic:
refine by_contra fun hnb ↦ ?_
Proof state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.Base B
⊢ False
Theorem: Matroid.Indep.base_of_forall_insert
Proof state before:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.Base B
⊢ False
Tactic:
obtain ⟨B', hB'⟩ := M.exists_base
Proof state after:
case intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.Base B
B' : Set α
hB' : M.Base B'
⊢ False
Theorem: Matroid.Indep.base_of_forall_insert
Proof state before:
case intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.Base B
B' : Set α
hB' : M.Base B'
⊢ False
Tactic:
obtain ⟨e, he, h⟩ := hB.exists_insert_of_not_base hnb hB'
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.Base B
B' : Set α
hB' : M.Base B'
e : α
he : e ∈ B' \ B
h : M.Indep (insert e B)
⊢ False
Theorem: Matroid.Indep.base_of_forall_insert
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.Base B
B' : Set α
hB' : M.Base B'
e : α
he : e ∈ B' \ B
h : M.Indep (insert e B)
⊢ False
Tactic:
exact hBmax e ⟨hB'.subset_ground he.1, he.2⟩ h
Proof state after:
no goals
Theorem: cl_iInter_eq_iInter_cl'
Proof state before:
α : Type u_1
M : Matroid α
Xs : Ordinal.{u} → Set α
h : ∀ ⦃i j : Ordinal.{u}⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
b : Ordinal.{u}
⊢ M.cl (⋂ i ∈ Iic b, Xs i) = ⋂ i ∈ Iic b, M.cl (Xs i)
Tactic:
sorry
Proof state after:
no goals
Theorem: foo
Proof state before:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
⊢ P univ
Tactic:
set r : ι → ι → Prop := WellOrderingRel
Proof state after:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
⊢ P univ
Theorem: foo
Proof state before:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
⊢ P univ
Tactic:
suffices hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r),
    P (range (fun p : Iio o ↦ Ordinal.enum r p.1 (lt_of_lt_of_le p.2 ho))) by
  convert hwin (Ordinal.type r) rfl.le
  rw [eq_comm, eq_univ_iff_forall]
  refine fun i ↦ ⟨⟨Ordinal.typein r i, Ordinal.typein_lt_type r i⟩, Ordinal.enum_typein _ _⟩
Proof state after:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
Theorem: foo
Proof state before:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
Tactic:
intro o
Proof state after:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
o : Ordinal.{u}
⊢ ∀ (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
Theorem: foo
Proof state before:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
o : Ordinal.{u}
⊢ ∀ (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
Tactic:
induction' o using Ordinal.induction with p hp
Proof state after:
case h
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
p : Ordinal.{u}
hp : ∀ k < p, ∀ (ho : k ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ ∀ (ho : p ≤ Ordinal.type r), P (range fun p_1 => Ordinal.enum r ↑p_1 ⋯)
Theorem: foo
Proof state before:
case h
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
p : Ordinal.{u}
hp : ∀ k < p, ∀ (ho : k ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ ∀ (ho : p ≤ Ordinal.type r), P (range fun p_1 => Ordinal.enum r ↑p_1 ⋯)
Tactic:
intro hpr
Proof state after:
case h
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
p : Ordinal.{u}
hp : ∀ k < p, ∀ (ho : k ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
hpr : p ≤ Ordinal.type r
⊢ P (range fun p_1 => Ordinal.enum r ↑p_1 ⋯)
Theorem: foo
Proof state before:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ P univ
Tactic:
convert hwin (Ordinal.type r) rfl.le
Proof state after:
case h.e'_1
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ univ = range fun p => Ordinal.enum r ↑p ⋯
Theorem: foo
Proof state before:
case h.e'_1
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ univ = range fun p => Ordinal.enum r ↑p ⋯
Tactic:
rw [eq_comm, eq_univ_iff_forall]
Proof state after:
case h.e'_1
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ ∀ (x : ι), x ∈ range fun p => Ordinal.enum r ↑p ⋯
Theorem: foo
Proof state before:
case h.e'_1
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ ∀ (x : ι), x ∈ range fun p => Ordinal.enum r ↑p ⋯
Tactic:
refine fun i ↦ ⟨⟨Ordinal.typein r i, Ordinal.typein_lt_type r i⟩, Ordinal.enum_typein _ _⟩
Proof state after:
no goals
Theorem: cl_iInter_eq_iInter_cl
Proof state before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
⊢ M.cl (⋂ i, Xs i) = {k}
Tactic:
set r : ι → ι → Prop := WellOrderingRel
Proof state after:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
⊢ M.cl (⋂ i, Xs i) = {k}
Theorem: cl_iInter_eq_iInter_cl
Proof state before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
⊢ M.cl (⋂ i, Xs i) = {k}
Tactic:
set P : Set ι → Prop := fun I ↦ M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
Proof state after:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
⊢ M.cl (⋂ i, Xs i) = {k}
Theorem: cl_iInter_eq_iInter_cl
Proof state before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
⊢ M.cl (⋂ i, Xs i) = {k}
Tactic:
suffices hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r),
    P (range (fun p : Iio o ↦ Ordinal.enum r p.1 (lt_of_lt_of_le p.2 ho))) by
  convert hwin (Ordinal.type r) rfl.le
Proof state after:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
Theorem: cl_iInter_eq_iInter_cl
Proof state before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
Tactic:
set r : ι → ι → Prop := WellOrderingRel
Proof state after:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r✝), P (range fun p => Ordinal.enum r✝ ↑p ⋯)