internlm/Lean-Github huggingface dataset:
Theorem: Matroid.girth_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
⊢ (loopyOn E).girth = 1
Tactic:
have _ : RkPos (loopyOn E)✶ := by rw [loopyOn_dual_eq]; exact freeOn_rkPos hE
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ (loopyOn E).girth = 1
Theorem: Matroid.girth_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ (loopyOn E).girth = 1
Tactic:
refine le_antisymm ?_ (one_le_girth _)
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ (loopyOn E).girth ≤ 1
Theorem: Matroid.girth_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ (loopyOn E).girth ≤ 1
Tactic:
simp only [girth_le_iff, loopyOn_circuit_iff]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ ∃ C, (∃ e ∈ E, C = {e}) ∧ C.encard ≤ 1
Theorem: Matroid.girth_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ ∃ C, (∃ e ∈ E, C = {e}) ∧ C.encard ≤ 1
Tactic:
exact ⟨{hE.some}, ⟨_, hE.some_mem, rfl⟩, by simp⟩
Proof state after:
no goals
Theorem: Matroid.girth_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
⊢ (loopyOn E)✶.RkPos
Tactic:
rw [loopyOn_dual_eq]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
⊢ (freeOn E).RkPos
Theorem: Matroid.girth_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
⊢ (freeOn E).RkPos
Tactic:
exact freeOn_rkPos hE
Proof state after:
no goals
Theorem: Matroid.girth_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ {hE.some}.encard ≤ 1
Tactic:
simp
Proof state after:
no goals
Theorem: setIndependent_singleton
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s : α
⊢ CompleteLattice.SetIndependent {s}
Tactic:
simp [CompleteLattice.SetIndependent]
Proof state after:
no goals
Theorem: Matroid.Nonloop.point_count_contract_eq
Proof state before:
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ sorryAx ℕ∞ true = {L | M.Line L ∧ e ∈ L}.encard
Tactic:
rw [point_count_eq_num_points]
Proof state after:
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ {P | ?m.6317.Point P}.encard = {L | M.Line L ∧ e ∈ L}.encard

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Matroid ?m.6315

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Type ?u.6314
Theorem: Matroid.Nonloop.point_count_contract_eq
Proof state before:
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ {P | ?m.6317.Point P}.encard = {L | M.Line L ∧ e ∈ L}.encard

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Matroid ?m.6315

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Type ?u.6314
Tactic:
apply encard_congr
Proof state after:
case e
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ ↑{P | ?m.6317.Point P} ≃ ↑{L | M.Line L ∧ e ∈ L}

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Matroid ?m.6315

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Type ?u.6314
Theorem: Matroid.Nonloop.point_count_contract_eq
Proof state before:
case e
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ ↑{P | ?m.6317.Point P} ≃ ↑{L | M.Line L ∧ e ∈ L}

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Matroid ?m.6315

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Type ?u.6314
Tactic:
simp only [coe_setOf]
Proof state after:
case e
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ { P // ?m.6317.Point P } ≃ { L // M.Line L ∧ e ∈ L }

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Matroid ?m.6315

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Type ?u.6314
Theorem: Matroid.Nonloop.point_count_contract_eq
Proof state before:
case e
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ { P // ?m.6317.Point P } ≃ { L // M.Line L ∧ e ∈ L }

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Matroid ?m.6315

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Type ?u.6314
Tactic:
convert he.contract_flat_equiv 1 using 2
Proof state after:
case h.e'_2.h.e'_2
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ (fun L => M.Line L ∧ e ∈ L) = fun F => M.Flat F ∧ M.er F = ↑1 + 1 ∧ e ∈ F
Theorem: Matroid.Nonloop.point_count_contract_eq
Proof state before:
case h.e'_2.h.e'_2
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ (fun L => M.Line L ∧ e ∈ L) = fun F => M.Flat F ∧ M.er F = ↑1 + 1 ∧ e ∈ F
Tactic:
ext L
Proof state after:
case h.e'_2.h.e'_2.h.a
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
L : Set α
⊢ M.Line L ∧ e ∈ L ↔ M.Flat L ∧ M.er L = ↑1 + 1 ∧ e ∈ L
Theorem: Matroid.Nonloop.point_count_contract_eq
Proof state before:
case h.e'_2.h.e'_2.h.a
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
L : Set α
⊢ M.Line L ∧ e ∈ L ↔ M.Flat L ∧ M.er L = ↑1 + 1 ∧ e ∈ L
Tactic:
simp [Line, and_assoc, one_add_one_eq_two]
Proof state after:
no goals
Theorem: Matroid.modular_finite_intersection
Proof state before:
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
⊢ ⋂₀ X ∈ C
Tactic:
obtain (⟨x, rfl⟩ | X_nt) := X_none.exists_eq_singleton_or_nontrivial
Proof state after:
case inl.intro
α : Type u_1
α✝ : Type u_2
C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
x : Set α✝
X_fin : {x}.Finite
X_sub : {x} ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : {x}.Nonempty
⊢ ⋂₀ {x} ∈ C

case inr
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
⊢ ⋂₀ X ∈ C
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
⊢ ⋂₀ X ∈ C
Tactic:
obtain ⟨x, y, xy_ne, xy_sub⟩ := nontrivial_iff_pair_subset.1 X_nt
Proof state after:
case inr.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ ⋂₀ X ∈ C
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ ⋂₀ X ∈ C
Tactic:
have x_eq_insert : X = insert x (X \ {x})
Proof state after:
case x_eq_insert
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ X = insert x (X \ {x})

case inr.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
⊢ ⋂₀ X ∈ C
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
⊢ ⋂₀ X ∈ C
Tactic:
rw [x_eq_insert, sInter_insert]
Proof state after:
case inr.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
⊢ x ∩ ⋂₀ (X \ {x}) ∈ C
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
⊢ x ∩ ⋂₀ (X \ {x}) ∈ C
Tactic:
obtain ⟨B, B_mod⟩ := X_mod
Proof state after:
case inr.intro.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : ?m.1084 C_mod X_fin X_sub
B_mod : sorryAx Prop true
⊢ x ∩ ⋂₀ (X \ {x}) ∈ C
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inl.intro
α : Type u_1
α✝ : Type u_2
C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
x : Set α✝
X_fin : {x}.Finite
X_sub : {x} ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : {x}.Nonempty
⊢ ⋂₀ {x} ∈ C
Tactic:
rwa [sInter_singleton, ← singleton_subset_iff]
Proof state after:
no goals
Theorem: Matroid.modular_finite_intersection
Proof state before:
case x_eq_insert
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ X = insert x (X \ {x})
Tactic:
simp [pair_subset_iff.1 xy_sub]
Proof state after:
no goals
Theorem: Matroid.modular_cut_iff_modular_cut'_finite
Proof state before:
α : Type u_1
C : Set (Set α)
M : Matroid α
inst✝ : M.Finite
⊢ M.Modular_cut C ↔ sorryAx Prop true
Tactic:
unfold Modular_cut Modular_cut'
Proof state after:
α : Type u_1
C : Set (Set α)
M : Matroid α
inst✝ : M.Finite
⊢ sorryAx ({α : Type u_1} → Matroid α → Set (Set α) → Prop) true M C ↔ sorryAx Prop true
Theorem: Matroid.union_insert_eq
Proof state before:
α : Type u_1
A : Set α
b c : α
⊢ insert b A ∪ insert c A = insert c (insert b A)
Tactic:
rw [insert_eq, insert_eq, ← union_union_distrib_right, @union_comm _ {b} _,
  union_assoc, ← insert_eq, ← insert_eq]
Proof state after:
no goals
Theorem: Matroid.inter_insert_eq
Proof state before:
α : Type u_1
A : Set α
b c : α
hne : b ≠ c
⊢ insert b A ∩ insert c A = A
Tactic:
rw [insert_eq, insert_eq, ← union_distrib_right, Disjoint.inter_eq _, empty_union]
Proof state after:
α : Type u_1
A : Set α
b c : α
hne : b ≠ c
⊢ Disjoint {b} {c}
Theorem: Matroid.inter_insert_eq
Proof state before:
α : Type u_1
A : Set α
b c : α
hne : b ≠ c
⊢ Disjoint {b} {c}
Tactic:
rwa [disjoint_singleton]
Proof state after:
no goals
Theorem: Matroid.Basis.exchange_base_of_indep
Proof state before:
α : Type u_1
B X : Set α
f e : α
M : Matroid α
hB : M.Basis B X
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
⊢ M.Basis (insert f (B \ {e})) X
Tactic:
have X_sub := hB.subset_ground
Proof state after:
α : Type u_1
B X : Set α
f e : α
M : Matroid α
hB : M.Basis B X
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ M.Basis (insert f (B \ {e})) X
Theorem: Matroid.Basis.exchange_base_of_indep
Proof state before:
α : Type u_1
B X : Set α
f e : α
M : Matroid α
hB : M.Basis B X
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ M.Basis (insert f (B \ {e})) X
Tactic:
rw [← base_restrict_iff] at hB ⊢
Proof state after:
α : Type u_1
B X : Set α
f e : α
M : Matroid α
hB : (M ↾ X).Base B
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ (M ↾ X).Base (insert f (B \ {e}))
Theorem: Matroid.Basis.exchange_base_of_indep
Proof state before:
α : Type u_1
B X : Set α
f e : α
M : Matroid α
hB : (M ↾ X).Base B
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ (M ↾ X).Base (insert f (B \ {e}))
Tactic:
apply hB.exchange_base_of_indep hf.2 (hI.indep_restrict_of_subset (insert_subset hf.1
(diff_subset.trans hB.subset_ground)))
Proof state after:
no goals
Theorem: Matroid.Modular_pair_comm
Proof state before:
α✝ : Type u_1
M : Matroid α✝
X Y : Set α✝
h : M.Modular_pair X Y
⊢ M.Modular_pair Y X
Tactic:
obtain ⟨B, B_Base, B_modular⟩ := h
Proof state after:
no goals
Theorem: Matroid.Modular_cut_pair
Proof state before:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert a (insert b X))
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
⊢ M.cl X ∈ C
Tactic:
rw [← union_insert_eq] at h_ind
Proof state after:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
⊢ M.cl X ∈ C
Theorem: Matroid.Modular_cut_pair
Proof state before:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
⊢ M.cl X ∈ C
Tactic:
have ab_cl_inter_eq : sInter {M.cl (insert b X), M.cl (insert a X)} = M.cl X
Proof state after:
case ab_cl_inter_eq
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
⊢ ⋂₀ {M.cl (insert b X), M.cl (insert a X)} = M.cl X

α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
ab_cl_inter_eq : ⋂₀ {M.cl (insert b X), M.cl (insert a X)} = M.cl X
⊢ M.cl X ∈ C
Theorem: Matroid.Modular_cut_pair
Proof state before:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
ab_cl_inter_eq : ⋂₀ {M.cl (insert b X), M.cl (insert a X)} = M.cl X
⊢ M.cl X ∈ C
Tactic:
rw [← ab_cl_inter_eq]
Proof state after:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
ab_cl_inter_eq : ⋂₀ {M.cl (insert b X), M.cl (insert a X)} = M.cl X
⊢ ⋂₀ {M.cl (insert b X), M.cl (insert a X)} ∈ C
Theorem: Matroid.Modular_cut_pair
Proof state before:
case ab_cl_inter_eq
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
⊢ ⋂₀ {M.cl (insert b X), M.cl (insert a X)} = M.cl X
Tactic:
rw [sInter_pair, ← h_ind.cl_inter_eq_inter_cl, inter_insert_eq hne.symm]
Proof state after:
no goals
Theorem: Matroid.flat_of_deleteElem_flat
Proof state before:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ (M ＼ e).Flat F
Tactic:
rw [flat_iff_cl_self, deleteElem, delete_cl_eq, diff_singleton_eq_self e_nF]
Proof state after:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F \ {e} = F
Theorem: Matroid.flat_of_deleteElem_flat
Proof state before:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F \ {e} = F
Tactic:
apply subset_antisymm _ (subset_diff_singleton (M.subset_cl _ ((subset_insert _ _).trans
 hF.subset_ground)) e_nF)
Proof state after:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F \ {e} ⊆ F
Theorem: Matroid.flat_of_deleteElem_flat
Proof state before:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F \ {e} ⊆ F
Tactic:
rw [diff_singleton_subset_iff]
Proof state after:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F ⊆ insert e F
Theorem: Matroid.flat_of_deleteElem_flat
Proof state before:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F ⊆ insert e F
Tactic:
apply (hF.cl_subset_of_subset (subset_insert _ _))
Proof state after:
no goals
Theorem: Matroid.sInter_insert_each
Proof state before:
α : Type u_1
X : Set (Set α)
a : α
⊢ insert a (⋂₀ X) = ⋂₀ {x | ∃ x_1 ∈ X, insert a x_1 = x}
Tactic:
ext x
Proof state after:
case h
α : Type u_1
X : Set (Set α)
a x : α
⊢ x ∈ insert a (⋂₀ X) ↔ x ∈ ⋂₀ {x | ∃ x_1 ∈ X, insert a x_1 = x}
Theorem: Matroid.sInter_insert_each
Proof state before:
case h
α : Type u_1
X : Set (Set α)
a x : α
⊢ x ∈ insert a (⋂₀ X) ↔ x ∈ ⋂₀ {x | ∃ x_1 ∈ X, insert a x_1 = x}
Tactic:
simp
Proof state after:
case h
α : Type u_1
X : Set (Set α)
a x : α
⊢ (x = a ∨ ∀ t ∈ X, x ∈ t) ↔ ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
Theorem: Matroid.sInter_insert_each
Proof state before:
case h
α : Type u_1
X : Set (Set α)
a x : α
⊢ (x = a ∨ ∀ t ∈ X, x ∈ t) ↔ ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
Tactic:
refine' ⟨fun h y y_mem ↦ _, fun h ↦ _⟩
Proof state after:
case h.refine'_1
α : Type u_1
X : Set (Set α)
a x : α
h : x = a ∨ ∀ t ∈ X, x ∈ t
y : Set α
y_mem : y ∈ X
⊢ x = a ∨ x ∈ y

case h.refine'_2
α : Type u_1
X : Set (Set α)
a x : α
h : ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
⊢ x = a ∨ ∀ t ∈ X, x ∈ t
Theorem: Matroid.sInter_insert_each
Proof state before:
case h.refine'_2
α : Type u_1
X : Set (Set α)
a x : α
h : ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
⊢ x = a ∨ ∀ t ∈ X, x ∈ t
Tactic:
obtain (rfl | ne) := eq_or_ne x a
Proof state after:
case h.refine'_2.inl
α : Type u_1
X : Set (Set α)
x : α
h : ∀ a ∈ X, x = x ∨ x ∈ a
⊢ x = x ∨ ∀ t ∈ X, x ∈ t

case h.refine'_2.inr
α : Type u_1
X : Set (Set α)
a x : α
h : ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
ne : x ≠ a
⊢ x = a ∨ ∀ t ∈ X, x ∈ t
Theorem: Matroid.sInter_insert_each
Proof state before:
case h.refine'_2.inr
α : Type u_1
X : Set (Set α)
a x : α
h : ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
ne : x ≠ a
⊢ x = a ∨ ∀ t ∈ X, x ∈ t
Tactic:
exact Or.inr (fun t t_mem ↦ (or_iff_right ne).1 (h t t_mem))
Proof state after:
no goals
Theorem: Matroid.sInter_insert_each
Proof state before:
case h.refine'_1
α : Type u_1
X : Set (Set α)
a x : α
h : x = a ∨ ∀ t ∈ X, x ∈ t
y : Set α
y_mem : y ∈ X
⊢ x = a ∨ x ∈ y
Tactic:
obtain (rfl | h) := h
Proof state after:
case h.refine'_1.inl
α : Type u_1
X : Set (Set α)
x : α
y : Set α
y_mem : y ∈ X
⊢ x = x ∨ x ∈ y

case h.refine'_1.inr
α : Type u_1
X : Set (Set α)
a x : α
y : Set α
y_mem : y ∈ X
h : ∀ t ∈ X, x ∈ t
⊢ x = a ∨ x ∈ y
Theorem: Matroid.sInter_insert_each
Proof state before:
case h.refine'_1.inr
α : Type u_1
X : Set (Set α)
a x : α
y : Set α
y_mem : y ∈ X
h : ∀ t ∈ X, x ∈ t
⊢ x = a ∨ x ∈ y
Tactic:
exact Or.inr (h y y_mem)
Proof state after:
no goals
Theorem: Matroid.sInter_insert_each
Proof state before:
case h.refine'_1.inl
α : Type u_1
X : Set (Set α)
x : α
y : Set α
y_mem : y ∈ X
⊢ x = x ∨ x ∈ y
Tactic:
exact Or.inl rfl
Proof state after:
no goals
Theorem: Matroid.sInter_insert_each
Proof state before:
case h.refine'_2.inl
α : Type u_1
X : Set (Set α)
x : α
h : ∀ a ∈ X, x = x ∨ x ∈ a
⊢ x = x ∨ ∀ t ∈ X, x ∈ t
Tactic:
exact Or.inl rfl
Proof state after:
no goals
Theorem: Matroid.modular_of_modular_restrict
Proof state before:
α : Type u_1
M : Matroid α
X : Set (Set α)
hX : ⋃₀ X ⊆ M.E
R : Set α
hR : ∃ B, sorryAx Prop true
⊢ ∃ B, sorryAx Prop true
Tactic:
obtain ⟨B, ⟨B_base, B_mod⟩⟩ := hR
Proof state after:
no goals
Theorem: Matroid.modular_cut_of_flats_remove
Proof state before:
α : Type u_1
e : α
M : Matroid α
⊢ (M ＼ e).Modular_cut {F | e ∉ F ∧ M.Flat (insert e F) ∧ e ∈ M.cl F}
Tactic:
refine' ⟨fun F F_flat ↦ flat_of_deleteElem_flat F_flat.1 F_flat.2.1,
 fun F F' F_Flat F_sub_F' F'_Flat ↦ _, fun X X_sub X_none X_modular ↦ _⟩
Proof state after:
no goals
Theorem: Matroid.matroid_of_cut_indep_iff
Proof state before:
α : Type u_1
I : Set α
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
e : α
e_nE : e ∉ M.E
⊢ (M.matroid_of_cut hC e_nE).Indep I ↔ if e ∈ I then M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ C else M.Indep I
Tactic:
simp [matroid_of_cut]
Proof state after:
α : Type u_1
I : Set α
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
e : α
e_nE : e ∉ M.E
⊢ (M.indepmatroid_of_cut C hC e_nE).Indep I ↔ if e ∈ I then M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ C else M.Indep I
Theorem: Matroid.matroid_of_cut_ground_eq
Proof state before:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
e : α
e_nE : e ∉ M.E
⊢ (M.matroid_of_cut hC e_nE).E = insert e M.E
Tactic:
simp [matroid_of_cut]
Proof state after:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
e : α
e_nE : e ∉ M.E
⊢ (M.indepmatroid_of_cut C hC e_nE).E = insert e M.E
Theorem: RankMatroid.relRank_self_eq_zero
Proof state before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
⊢ M.relRank A A = 0
Tactic:
obtain h := M.relRank_le_encard_diff A A
Proof state after:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
h : M.relRank A A ≤ (A \ A).encard
⊢ M.relRank A A = 0
Theorem: RankMatroid.relRank_self_eq_zero
Proof state before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
h : M.relRank A A ≤ (A \ A).encard
⊢ M.relRank A A = 0
Tactic:
simpa only [sdiff_self, Set.bot_eq_empty, Set.encard_empty, nonpos_iff_eq_zero] using h
Proof state after:
no goals
Theorem: RankMatroid.relRank_inter_ground
Proof state before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
⊢ M.relRank (A ∩ M.E) (B ∩ M.E) = M.relRank A B
Tactic:
rw [M.relRank_inter_ground_left, M.relRank_inter_ground_right]
Proof state after:
no goals
Theorem: RankMatroid.indep_subset
Proof state before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hJ : M.Indep J
rIJ : I ⊆ J
⊢ M.Indep I
Tactic:
refine M.indep_iff'.mpr ⟨rIJ.trans hJ.subset_ground, fun x hx ↦ ?_⟩
Proof state after:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hJ : M.Indep J
rIJ : I ⊆ J
x : α
hx : x ∈ I
⊢ M.relRank (I \ {x}) I > 0
Theorem: RankMatroid.indep_subset
Proof state before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hJ : M.Indep J
rIJ : I ⊆ J
x : α
hx : x ∈ I
⊢ M.relRank (I \ {x}) I > 0
Tactic:
have hJ := hJ.relRank_pos_of_sub_mem (rIJ hx)
Proof state after:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
rIJ : I ⊆ J
x : α
hx : x ∈ I
hJ : M.relRank (J \ {x}) J > 0
⊢ M.relRank (I \ {x}) I > 0
Theorem: RankMatroid.indep_subset
Proof state before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
rIJ : I ⊆ J
x : α
hx : x ∈ I
hJ : M.relRank (J \ {x}) J > 0
⊢ M.relRank (I \ {x}) I > 0
Tactic:
set A := I
Proof state after:
α : Type u_1
A✝ B I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
hJ : M.relRank (J \ {x}) J > 0
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
⊢ M.relRank (A \ {x}) A > 0
Theorem: RankMatroid.indep_subset
Proof state before:
α : Type u_1
A✝ B I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
hJ : M.relRank (J \ {x}) J > 0
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
⊢ M.relRank (A \ {x}) A > 0
Tactic:
set B := J \ {x}
Proof state after:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
⊢ M.relRank (A \ {x}) A > 0
Theorem: RankMatroid.indep_subset
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
⊢ M.relRank (A \ {x}) A > 0
Tactic:
have hAUB : J = I ∪ (J \ {x}) :=
  (Set.union_diff_cancel' (Set.singleton_subset_iff.mpr hx) rIJ).symm
Proof state after:
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
⊢ M.relRank (A \ {x}) A > 0