internlm/Lean-Github huggingface dataset:
Theorem: Matroid.truncate_eq_self_of_rk_le
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
⊢ M.truncateTo k = M
Tactic:
refine eq_of_indep_iff_indep_forall truncateTo_ground_eq (fun I _ ↦ ?_)
Proof state after:
α : Type u_1
M : Matroid α
E I✝ B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
I : Set α
x✝ : I ⊆ (M.truncateTo k).E
⊢ (M.truncateTo k).Indep I ↔ M.Indep I
Theorem: Matroid.truncate_eq_self_of_rk_le
Proof state before:
α : Type u_1
M : Matroid α
E I✝ B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
I : Set α
x✝ : I ⊆ (M.truncateTo k).E
⊢ (M.truncateTo k).Indep I ↔ M.Indep I
Tactic:
rw [truncateTo_indep_iff, and_iff_left_iff_imp]
Proof state after:
α : Type u_1
M : Matroid α
E I✝ B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
I : Set α
x✝ : I ⊆ (M.truncateTo k).E
⊢ M.Indep I → I.encard ≤ k
Theorem: Matroid.truncate_eq_self_of_rk_le
Proof state before:
α : Type u_1
M : Matroid α
E I✝ B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
I : Set α
x✝ : I ⊆ (M.truncateTo k).E
⊢ M.Indep I → I.encard ≤ k
Tactic:
exact fun hi ↦ hi.encard_le_erk.trans h_rk
Proof state after:
no goals
Theorem: Matroid.truncateTo_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ (M.truncateTo ↑k).Base B ↔ M.Indep B ∧ B.encard = ↑k
Tactic:
simp_rw [base_iff_maximal_indep, truncateTo_indep_iff, and_imp]
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ ((M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I) ↔ M.Indep B ∧ B.encard = ↑k
Theorem: Matroid.truncateTo_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ ((M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I) ↔ M.Indep B ∧ B.encard = ↑k
Tactic:
refine ⟨fun ⟨⟨hB, hBk⟩, h⟩ ↦ ⟨hB, hBk.antisymm (le_of_not_lt fun hlt ↦ ?_)⟩,
  fun ⟨hB, hBk⟩ ↦ ⟨⟨ hB, hBk.le⟩,
    fun I _ hIk hBI ↦ ?_⟩ ⟩
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
⊢ False

case refine_2
α : Type u_1
M : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝¹ : M.Indep B ∧ B.encard = ↑k
hB : M.Indep B
hBk : B.encard = ↑k
I : Set α
x✝ : M.Indep I
hIk : I.encard ≤ ↑k
hBI : B ⊆ I
⊢ B = I
Theorem: Matroid.truncateTo_base_iff
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝¹ : M.Indep B ∧ B.encard = ↑k
hB : M.Indep B
hBk : B.encard = ↑k
I : Set α
x✝ : M.Indep I
hIk : I.encard ≤ ↑k
hBI : B ⊆ I
⊢ B = I
Tactic:
exact (finite_of_encard_eq_coe hBk).eq_of_subset_of_encard_le' hBI (hIk.trans_eq hBk.symm)
Proof state after:
no goals
Theorem: Matroid.truncateTo_base_iff
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
⊢ False
Tactic:
obtain ⟨B', hB', hJB'⟩ := hB.exists_base_superset
Proof state after:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
B' : Set α
hB' : M.Base B'
hJB' : B ⊆ B'
⊢ False
Theorem: Matroid.truncateTo_base_iff
Proof state before:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
B' : Set α
hB' : M.Base B'
hJB' : B ⊆ B'
⊢ False
Tactic:
obtain ⟨J, hBJ, hJB', h'⟩ :=
  exists_superset_subset_encard_eq hJB' hBk (h_rk.trans_eq hB'.encard.symm)
Proof state after:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
B' : Set α
hB' : M.Base B'
hJB'✝ : B ⊆ B'
J : Set α
hBJ : B ⊆ J
hJB' : J ⊆ B'
h' : J.encard = ↑k
⊢ False
Theorem: Matroid.truncateTo_base_iff
Proof state before:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
B' : Set α
hB' : M.Base B'
hJB'✝ : B ⊆ B'
J : Set α
hBJ : B ⊆ J
hJB' : J ⊆ B'
h' : J.encard = ↑k
⊢ False
Tactic:
rw [h _ (hB'.indep.subset hJB') h'.le hBJ] at hlt
Proof state after:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
B' : Set α
hB' : M.Base B'
hJB'✝ : B ⊆ B'
J : Set α
hlt : J.encard < ↑k
hBJ : B ⊆ J
hJB' : J ⊆ B'
h' : J.encard = ↑k
⊢ False
Theorem: Matroid.truncateTo_base_iff
Proof state before:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
B' : Set α
hB' : M.Base B'
hJB'✝ : B ⊆ B'
J : Set α
hlt : J.encard < ↑k
hBJ : B ⊆ J
hJB' : J ⊆ B'
h' : J.encard = ↑k
⊢ False
Tactic:
exact hlt.ne h'
Proof state after:
no goals
Theorem: Matroid.truncate_base_iff_of_finiteRk
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.FiniteRk
h_rk : k ≤ M.erk
⊢ (M.truncateTo k).Base B ↔ M.Indep B ∧ B.encard = k
Tactic:
lift k to ℕ using (h_rk.trans_lt M.erk_lt_top).ne
Proof state after:
case intro
α : Type u_1
M : Matroid α
E I B : Set α
inst✝ : M.FiniteRk
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ (M.truncateTo ↑k).Base B ↔ M.Indep B ∧ B.encard = ↑k
Theorem: Matroid.truncate_base_iff_of_finiteRk
Proof state before:
case intro
α : Type u_1
M : Matroid α
E I B : Set α
inst✝ : M.FiniteRk
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ (M.truncateTo ↑k).Base B ↔ M.Indep B ∧ B.encard = ↑k
Tactic:
rwa [truncateTo_base_iff]
Proof state after:
no goals
Theorem: Matroid.Indep.of_truncateTo
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
h : (M.truncateTo k).Indep I
⊢ M.Indep I
Tactic:
rw [truncateTo_indep_iff] at h
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
h : M.Indep I ∧ I.encard ≤ k
⊢ M.Indep I
Theorem: Matroid.Indep.of_truncateTo
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
h : M.Indep I ∧ I.encard ≤ k
⊢ M.Indep I
Tactic:
exact h.1
Proof state after:
no goals
Theorem: Matroid.truncateTo_er_eq
Proof state before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X : Set α
⊢ (M.truncateTo k).er X = min (M.er X) k
Tactic:
simp_rw [le_antisymm_iff, le_er_iff, er_le_iff, truncateTo_indep_iff]
Proof state after:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X : Set α
⊢ (∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k) ∧
    ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
Theorem: Matroid.truncateTo_er_eq
Proof state before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X : Set α
⊢ (∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k) ∧
    ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
Proof state after:
case intro
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ (∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k) ∧
    ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
Theorem: Matroid.truncateTo_er_eq
Proof state before:
case intro
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ (∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k) ∧
    ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
Tactic:
refine ⟨?_, ?_⟩
Proof state after:
case intro.refine_1
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ ∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k

case intro.refine_2
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
Theorem: Matroid.truncateTo_er_eq
Proof state before:
case intro.refine_2
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
Tactic:
obtain ⟨I₀, hI₀, hI₀ss⟩ := exists_subset_encard_eq (min_le_of_left_le (b := k) hI.encard.symm.le)
Proof state after:
case intro.refine_2.intro.intro
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
I₀ : Set α
hI₀ : I₀ ⊆ I
hI₀ss : I₀.encard = min (M.er X) k
⊢ ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
Theorem: Matroid.truncateTo_er_eq
Proof state before:
case intro.refine_2.intro.intro
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
I₀ : Set α
hI₀ : I₀ ⊆ I
hI₀ss : I₀.encard = min (M.er X) k
⊢ ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
Tactic:
exact ⟨_, hI₀.trans hI.subset, ⟨hI.indep.subset hI₀, hI₀ss.trans_le (min_le_right _ _)⟩, hI₀ss⟩
Proof state after:
no goals
Theorem: Matroid.truncateTo_er_eq
Proof state before:
case intro.refine_1
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ ∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k
Tactic:
intro J hJX hJi
Proof state after:
case intro.refine_1
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
J : Set α
hJX : J ⊆ X
hJi : M.Indep J ∧ J.encard ≤ k
⊢ J.encard ≤ min (M.er X) k
Theorem: Matroid.truncateTo_er_eq
Proof state before:
case intro.refine_1
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
J : Set α
hJX : J ⊆ X
hJi : M.Indep J ∧ J.encard ≤ k
⊢ J.encard ≤ min (M.er X) k
Tactic:
exact le_min (hJi.1.encard_le_er_of_subset hJX) hJi.2
Proof state after:
no goals
Theorem: Matroid.truncate_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
⊢ M.truncate.Indep I ↔ M.Indep I ∧ ¬M.Base I
Tactic:
simp only [truncate_indep_iff', and_congr_right_iff]
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
⊢ M.Indep I → (M.Base I → I = ∅ ↔ ¬M.Base I)
Theorem: Matroid.truncate_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
⊢ M.Indep I → (M.Base I → I = ∅ ↔ ¬M.Base I)
Tactic:
exact fun _ ↦ ⟨fun h hB ↦ hB.nonempty.ne_empty (h hB), fun h hB ↦ by contradiction⟩
Proof state after:
no goals
Theorem: Matroid.truncate_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : M.Indep I
h : ¬M.Base I
hB : M.Base I
⊢ I = ∅
Tactic:
contradiction
Proof state after:
no goals
Theorem: Matroid.truncate_loopyOn_eq
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k : ℕ∞
E : Set α
⊢ (loopyOn E).truncate = loopyOn E
Tactic:
simp (config := {contextual := true}) [truncate, ModularCut.principal, eq_loopyOn_iff]
Proof state after:
no goals
Theorem: Matroid.truncate_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
⊢ M.truncate.Base B ↔ ∃ e ∉ B, M.Base (insert e B)
Tactic:
refine ⟨fun h ↦ ?_, fun ⟨e, he, hBe⟩ ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
⊢ ∃ e ∉ B, M.Base (insert e B)

case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.truncate.Base B
Theorem: Matroid.truncate_base_iff
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.truncate.Base B
Tactic:
refine Indep.base_of_forall_insert ?_ ?_
Proof state after:
case refine_2.refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.truncate.Indep B

case refine_2.refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ ∀ e ∈ M.truncate.E \ B, ¬M.truncate.Indep (insert e B)
Theorem: Matroid.truncate_base_iff
Proof state before:
case refine_2.refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ ∀ e ∈ M.truncate.E \ B, ¬M.truncate.Indep (insert e B)
Tactic:
simp only [truncate_ground_eq, mem_diff, truncate_indep_iff, not_and, not_not, and_imp]
Proof state after:
case refine_2.refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ ∀ e ∈ M.E, e ∉ B → M.Indep (insert e B) → M.Base (insert e B)
Theorem: Matroid.truncate_base_iff
Proof state before:
case refine_2.refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ ∀ e ∈ M.E, e ∉ B → M.Indep (insert e B) → M.Base (insert e B)
Tactic:
exact fun f _ hfB hfBi ↦ insert_base_of_insert_indep he hfB hBe hfBi
Proof state after:
no goals
Theorem: Matroid.truncate_base_iff
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
⊢ ∃ e ∉ B, M.Base (insert e B)
Tactic:
obtain ⟨hB, hBb⟩ := truncate_indep_iff.1 h.indep
Proof state after:
case refine_1.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
⊢ ∃ e ∉ B, M.Base (insert e B)
Theorem: Matroid.truncate_base_iff
Proof state before:
case refine_1.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
⊢ ∃ e ∉ B, M.Base (insert e B)
Tactic:
obtain ⟨B', hB', hBB'⟩ := hB.exists_base_superset
Proof state after:
case refine_1.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
⊢ ∃ e ∉ B, M.Base (insert e B)
Theorem: Matroid.truncate_base_iff
Proof state before:
case refine_1.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
⊢ ∃ e ∉ B, M.Base (insert e B)
Tactic:
obtain ⟨e, heB', heB⟩ := exists_of_ssubset (hBB'.ssubset_of_ne (by rintro rfl; contradiction))
Proof state after:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ ∃ e ∉ B, M.Base (insert e B)
Theorem: Matroid.truncate_base_iff
Proof state before:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ ∃ e ∉ B, M.Base (insert e B)
Tactic:
refine ⟨e, heB, ?_⟩
Proof state after:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.Base (insert e B)
Theorem: Matroid.truncate_base_iff
Proof state before:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.Base (insert e B)
Tactic:
rwa [h.eq_of_subset_indep ?_ (subset_diff_singleton hBB' heB), insert_diff_singleton,
  insert_eq_of_mem heB']
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.truncate.Indep (B' \ {e})
Theorem: Matroid.truncate_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.truncate.Indep (B' \ {e})
Tactic:
rw [truncate_indep_iff]
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.Indep (B' \ {e}) ∧ ¬M.Base (B' \ {e})
Theorem: Matroid.truncate_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.Indep (B' \ {e}) ∧ ¬M.Base (B' \ {e})
Tactic:
exact ⟨hB'.indep.subset diff_subset, hB'.not_base_of_ssubset <| diff_singleton_sSubset.mpr heB'⟩
Proof state after:
no goals
Theorem: Matroid.truncate_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
⊢ B ≠ B'
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
hB' : M.Base B
hBB' : B ⊆ B
⊢ False
Theorem: Matroid.truncate_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
hB' : M.Base B
hBB' : B ⊆ B
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Matroid.truncate_base_iff
Proof state before:
case refine_2.refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.truncate.Indep B
Tactic:
rw [truncate_indep_iff]
Proof state after:
case refine_2.refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.Indep B ∧ ¬M.Base B
Theorem: Matroid.truncate_base_iff
Proof state before:
case refine_2.refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.Indep B ∧ ¬M.Base B
Tactic:
exact ⟨hBe.indep.subset (subset_insert _ _), hBe.not_base_of_ssubset (ssubset_insert he)⟩
Proof state after:
no goals
Theorem: Matroid.circuitOn_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
⊢ (circuitOn C).Indep I ↔ I ⊂ C
Tactic:
have := freeOn_rkPos hC
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
this : (freeOn C).RkPos
⊢ (circuitOn C).Indep I ↔ I ⊂ C
Theorem: Matroid.circuitOn_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
this : (freeOn C).RkPos
⊢ (circuitOn C).Indep I ↔ I ⊂ C
Tactic:
simp [circuitOn, truncate_indep_iff, ssubset_iff_subset_ne]
Proof state after:
no goals
Theorem: Matroid.circuitOn_dep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
D : Set α
⊢ (circuitOn C).Dep D ↔ D = C
Tactic:
simp only [Dep, circuitOn_indep_iff hC, ssubset_iff_subset_ne, ne_eq, not_and, not_not,
  circuitOn_ground]
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
D : Set α
⊢ (D ⊆ C → D = C) ∧ D ⊆ C ↔ D = C
Theorem: Matroid.circuitOn_dep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
D : Set α
⊢ (D ⊆ C → D = C) ∧ D ⊆ C ↔ D = C
Tactic:
exact ⟨fun h ↦ h.1 h.2, by rintro rfl; simp [Subset.rfl]⟩
Proof state after:
no goals
Theorem: Matroid.circuitOn_dep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
D : Set α
⊢ D = C → (D ⊆ C → D = C) ∧ D ⊆ C
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
D : Set α
hC : D.Nonempty
⊢ (D ⊆ D → D = D) ∧ D ⊆ D
Theorem: Matroid.circuitOn_dep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
D : Set α
hC : D.Nonempty
⊢ (D ⊆ D → D = D) ∧ D ⊆ D
Tactic:
simp [Subset.rfl]
Proof state after:
no goals
Theorem: Matroid.circuitOn_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
⊢ (circuitOn C).Base B ↔ ∃ e ∉ B, insert e B = C
Tactic:
have _ := freeOn_rkPos hC
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
x✝ : (freeOn C).RkPos
⊢ (circuitOn C).Base B ↔ ∃ e ∉ B, insert e B = C
Theorem: Matroid.circuitOn_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
x✝ : (freeOn C).RkPos
⊢ (circuitOn C).Base B ↔ ∃ e ∉ B, insert e B = C
Tactic:
simp [circuitOn, truncate_base_iff]
Proof state after:
no goals
Theorem: Matroid.circuitOn_ground_circuit
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
⊢ (circuitOn C).Circuit C
Tactic:
simp [circuit_iff_forall_ssubset, circuitOn_dep_iff hC, circuitOn_indep_iff hC]
Proof state after:
no goals
Theorem: Matroid.circuitOn_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
C' : Set α
⊢ (circuitOn C).Circuit C' ↔ C' = C
Tactic:
refine ⟨fun h ↦ h.eq_of_subset_circuit (circuitOn_ground_circuit hC) h.subset_ground, ?_⟩
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
C' : Set α
⊢ C' = C → (circuitOn C).Circuit C'
Theorem: Matroid.circuitOn_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
C' : Set α
⊢ C' = C → (circuitOn C).Circuit C'
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C' : Set α
hC : C'.Nonempty
⊢ (circuitOn C').Circuit C'
Theorem: Matroid.circuitOn_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C' : Set α
hC : C'.Nonempty
⊢ (circuitOn C').Circuit C'
Tactic:
exact circuitOn_ground_circuit hC
Proof state after:
no goals
Theorem: Matroid.ground_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
⊢ M.Circuit M.E ↔ M = circuitOn M.E
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
⊢ M = circuitOn M.E

case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M = circuitOn M.E
⊢ M.Circuit M.E