internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ground_circuit_iff
Proof state before:
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
Tactic:
rw [h]
Proof state after:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M = circuitOn M.E
⊢ (circuitOn M.E).Circuit (circuitOn M.E).E
Theorem: Matroid.ground_circuit_iff
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M = circuitOn M.E
⊢ (circuitOn M.E).Circuit (circuitOn M.E).E
Tactic:
exact circuitOn_ground_circuit M.ground_nonempty
Proof state after:
no goals
Theorem: Matroid.ground_circuit_iff
Proof state before:
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
Tactic:
refine eq_of_circuit_iff_circuit_forall rfl <| fun C hC ↦ ?_
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
C : Set α
hC : C ⊆ M.E
⊢ M.Circuit C ↔ (circuitOn M.E).Circuit C
Theorem: Matroid.ground_circuit_iff
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C✝ : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
C : Set α
hC : C ⊆ M.E
⊢ M.Circuit C ↔ (circuitOn M.E).Circuit C
Tactic:
rw [circuitOn_circuit_iff h.nonempty]
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
C : Set α
hC : C ⊆ M.E
⊢ M.Circuit C ↔ C = M.E
Theorem: Matroid.ground_circuit_iff
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C✝ : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
C : Set α
hC : C ⊆ M.E
⊢ M.Circuit C ↔ C = M.E
Tactic:
exact ⟨fun h' ↦ h'.eq_of_subset_circuit h hC, by rintro rfl; assumption⟩
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
h : M.Circuit M.E
C : Set α
hC : C ⊆ M.E
⊢ C = M.E → M.Circuit C
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
hC : M.E ⊆ M.E
⊢ M.Circuit M.E
Theorem: Matroid.ground_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
hC : M.E ⊆ M.E
⊢ M.Circuit M.E
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.circuit_iff_restr_eq_circuitOn
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
⊢ M.Circuit C ↔ M ↾ C = circuitOn C
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
⊢ M ↾ C = circuitOn C

case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M ↾ C = circuitOn C
⊢ M.Circuit C
Theorem: Matroid.circuit_iff_restr_eq_circuitOn
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M ↾ C = circuitOn C
⊢ M.Circuit C
Tactic:
have h' := restrict_circuit_iff hC (C := C)
Proof state after:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M ↾ C = circuitOn C
h' : (M ↾ C).Circuit C ↔ M.Circuit C ∧ C ⊆ C
⊢ M.Circuit C
Theorem: Matroid.circuit_iff_restr_eq_circuitOn
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M ↾ C = circuitOn C
h' : (M ↾ C).Circuit C ↔ M.Circuit C ∧ C ⊆ C
⊢ M.Circuit C
Tactic:
rwa [and_iff_left Subset.rfl, h, iff_true_intro (circuitOn_ground_circuit hCne), true_iff] at h'
Proof state after:
no goals
Theorem: Matroid.circuit_iff_restr_eq_circuitOn
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
⊢ M ↾ C = circuitOn C
Tactic:
refine eq_of_circuit_iff_circuit_forall rfl fun C' hC' ↦ ?_
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
C' : Set α
hC' : C' ⊆ (M ↾ C).E
⊢ (M ↾ C).Circuit C' ↔ (circuitOn C).Circuit C'
Theorem: Matroid.circuit_iff_restr_eq_circuitOn
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
C' : Set α
hC' : C' ⊆ (M ↾ C).E
⊢ (M ↾ C).Circuit C' ↔ (circuitOn C).Circuit C'
Tactic:
rw [restrict_circuit_iff h.subset_ground, circuitOn_circuit_iff h.nonempty,
  and_iff_left (show C' ⊆ C from hC')]
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
C' : Set α
hC' : C' ⊆ (M ↾ C).E
⊢ M.Circuit C' ↔ C' = C
Theorem: Matroid.circuit_iff_restr_eq_circuitOn
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
C' : Set α
hC' : C' ⊆ (M ↾ C).E
⊢ M.Circuit C' ↔ C' = C
Tactic:
exact ⟨fun h' ↦ h'.eq_of_subset_circuit h hC', fun h' ↦ by rwa [h']⟩
Proof state after:
no goals
Theorem: Matroid.circuit_iff_restr_eq_circuitOn
Proof state before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
C' : Set α
hC' : C' ⊆ (M ↾ C).E
h' : C' = C
⊢ M.Circuit C'
Tactic:
rwa [h']
Proof state after:
no goals
Theorem: Set.inter_distrib_biInter
Proof state before:
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
⊢ t ∩ ⋂ i ∈ u, s i = ⋂ i ∈ u, t ∩ s i
Tactic:
have := hu.coe_sort
Proof state after:
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
this : Nonempty ↑u
⊢ t ∩ ⋂ i ∈ u, s i = ⋂ i ∈ u, t ∩ s i
Theorem: Set.inter_distrib_biInter
Proof state before:
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
this : Nonempty ↑u
⊢ t ∩ ⋂ i ∈ u, s i = ⋂ i ∈ u, t ∩ s i
Tactic:
rw [biInter_eq_iInter, inter_iInter, biInter_eq_iInter]
Proof state after:
no goals
Theorem: Set.biInter_distrib_inter
Proof state before:
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
⊢ (⋂ i ∈ u, s i) ∩ t = ⋂ i ∈ u, s i ∩ t
Tactic:
simp_rw [inter_comm, inter_distrib_biInter _ hu]
Proof state after:
no goals
Theorem: Set.union_distrib_biUnion
Proof state before:
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
⊢ t ∪ ⋃ i ∈ u, s i = ⋃ i ∈ u, t ∪ s i
Tactic:
have := hu.coe_sort
Proof state after:
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
this : Nonempty ↑u
⊢ t ∪ ⋃ i ∈ u, s i = ⋃ i ∈ u, t ∪ s i
Theorem: Set.union_distrib_biUnion
Proof state before:
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
this : Nonempty ↑u
⊢ t ∪ ⋃ i ∈ u, s i = ⋃ i ∈ u, t ∪ s i
Tactic:
rw [biUnion_eq_iUnion, union_iUnion, biUnion_eq_iUnion]
Proof state after:
no goals
Theorem: Set.biUnion_distrib_union
Proof state before:
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
⊢ (⋃ i ∈ u, s i) ∪ t = ⋃ i ∈ u, s i ∪ t
Tactic:
simp_rw [union_comm, union_distrib_biUnion _ hu]
Proof state after:
no goals
Theorem: Set.inter_distrib_sInter
Proof state before:
α : Type u_1
ι : Type u_2
s : Set (Set α)
hs : s.Nonempty
t : Set α
⊢ t ∩ ⋂₀ s = ⋂ x ∈ s, t ∩ x
Tactic:
rw [sInter_eq_biInter, inter_distrib_biInter _ hs]
Proof state after:
no goals
Theorem: Set.sInter_distrib_inter
Proof state before:
α : Type u_1
ι : Type u_2
s : Set (Set α)
hs : s.Nonempty
t : Set α
⊢ ⋂₀ s ∩ t = ⋂ x ∈ s, x ∩ t
Tactic:
simp_rw [inter_comm _ t, inter_distrib_sInter hs]
Proof state after:
no goals
Theorem: Set.union_distrib_sUnion
Proof state before:
α : Type u_1
ι : Type u_2
s : Set (Set α)
hs : s.Nonempty
t : Set α
⊢ t ∪ ⋃₀ s = ⋃ x ∈ s, t ∪ x
Tactic:
rw [sUnion_eq_biUnion, union_distrib_biUnion _ hs]
Proof state after:
no goals
Theorem: Set.sUnion_distrib_union
Proof state before:
α : Type u_1
ι : Type u_2
s : Set (Set α)
hs : s.Nonempty
t : Set α
⊢ ⋃₀ s ∪ t = ⋃ x ∈ s, x ∪ t
Tactic:
rw [sUnion_eq_biUnion, biUnion_distrib_union _ hs]
Proof state after:
no goals
Theorem: Set.diff_eq_diff_inter_of_subset
Proof state before:
α : Type u_1
ι : Type u_2
s t : Set α
h : s ⊆ t
r : Set α
⊢ s \ r = s \ (r ∩ t)
Tactic:
rw [diff_inter, diff_eq_empty.2 h, union_empty]
Proof state after:
no goals
Theorem: Set.diff_union_eq_union_of_subset
Proof state before:
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ⊆ r
⊢ s \ t ∪ r = s ∪ r
Tactic:
ext x
Proof state after:
case h
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ⊆ r
x : α
⊢ x ∈ s \ t ∪ r ↔ x ∈ s ∪ r
Theorem: Set.diff_union_eq_union_of_subset
Proof state before:
case h
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ⊆ r
x : α
⊢ x ∈ s \ t ∪ r ↔ x ∈ s ∪ r
Tactic:
simp only [mem_union, mem_diff]
Proof state after:
case h
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ⊆ r
x : α
⊢ x ∈ s ∧ x ∉ t ∨ x ∈ r ↔ x ∈ s ∨ x ∈ r
Theorem: Set.diff_union_eq_union_of_subset
Proof state before:
case h
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ⊆ r
x : α
⊢ x ∈ s ∧ x ∉ t ∨ x ∈ r ↔ x ∈ s ∨ x ∈ r
Tactic:
tauto
Proof state after:
no goals
Theorem: Set.diff_eq_diff_iff_inter_eq_inter
Proof state before:
α : Type u_1
ι : Type u_2
s t r : Set α
⊢ s \ t = s \ r ↔ t ∩ s = r ∩ s
Tactic:
rw [← diff_inter_self_eq_diff, ← diff_inter_self_eq_diff (t := r)]
Proof state after:
α : Type u_1
ι : Type u_2
s t r : Set α
⊢ s \ (t ∩ s) = s \ (r ∩ s) ↔ t ∩ s = r ∩ s
Theorem: Set.diff_eq_diff_iff_inter_eq_inter
Proof state before:
α : Type u_1
ι : Type u_2
s t r : Set α
⊢ s \ (t ∩ s) = s \ (r ∩ s) ↔ t ∩ s = r ∩ s
Tactic:
refine' ⟨fun h ↦ _, fun h ↦ by rw [h]⟩
Proof state after:
α : Type u_1
ι : Type u_2
s t r : Set α
h : s \ (t ∩ s) = s \ (r ∩ s)
⊢ t ∩ s = r ∩ s
Theorem: Set.diff_eq_diff_iff_inter_eq_inter
Proof state before:
α : Type u_1
ι : Type u_2
s t r : Set α
h : s \ (t ∩ s) = s \ (r ∩ s)
⊢ t ∩ s = r ∩ s
Tactic:
rw [← diff_diff_cancel_left inter_subset_right, h, diff_diff_cancel_left inter_subset_right]
Proof state after:
no goals
Theorem: Set.diff_eq_diff_iff_inter_eq_inter
Proof state before:
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ∩ s = r ∩ s
⊢ s \ (t ∩ s) = s \ (r ∩ s)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Set.diff_inter_diff_right
Proof state before:
α : Type u_1
ι : Type u_2
s t r : Set α
⊢ t \ s ∩ (r \ s) = (t ∩ r) \ s
Tactic:
simp only [diff_eq, inter_assoc, inter_comm sᶜ, inter_self]
Proof state after:
no goals
Theorem: Set.inter_diff_right_comm
Proof state before:
α : Type u_1
ι : Type u_2
s t r : Set α
⊢ (s ∩ t) \ r = s \ r ∩ t
Tactic:
simp_rw [diff_eq, inter_right_comm]
Proof state after:
no goals
Theorem: Set.inter_insert_eq
Proof state before:
α : Type u_1
ι : Type u_2
A : Set α
b c : α
hne : b ≠ c
⊢ insert b A ∩ insert c A = A
Tactic:
rw [insert_eq, insert_eq, ← inter_union_distrib_right, Disjoint.inter_eq _, empty_union]
Proof state after:
α : Type u_1
ι : Type u_2
A : Set α
b c : α
hne : b ≠ c
⊢ Disjoint {b} {c}
Theorem: Set.inter_insert_eq
Proof state before:
α : Type u_1
ι : Type u_2
A : Set α
b c : α
hne : b ≠ c
⊢ Disjoint {b} {c}
Tactic:
rwa [disjoint_singleton]
Proof state after:
no goals
Theorem: Set.union_insert_eq
Proof state before:
α : Type u_1
ι : Type u_2
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: Set.not_mem_or_exists_eq_insert_not_mem
Proof state before:
α : Type u_1
ι : Type u_2
s : Set α
x : α
h : x ∈ s
⊢ x ∉ s \ {x}
Tactic:
simp
Proof state after:
no goals
Theorem: Set.not_mem_or_exists_eq_insert_not_mem
Proof state before:
α : Type u_1
ι : Type u_2
s : Set α
x : α
h : x ∈ s
⊢ s = insert x (s \ {x})
Tactic:
simp [insert_eq_of_mem h]
Proof state after:
no goals
Theorem: Set.biInter_diff_singleton_eq_diff
Proof state before:
α : Type u_1
ι : Type u_2
s t : Set α
ht : t.Nonempty
⊢ ⋂ i ∈ t, s \ {i} = s \ t
Tactic:
simp only [ext_iff, mem_iInter, mem_diff, mem_singleton_iff]
Proof state after:
α : Type u_1
ι : Type u_2
s t : Set α
ht : t.Nonempty
⊢ ∀ (x : α), (∀ i ∈ t, x ∈ s ∧ ¬x = i) ↔ x ∈ s ∧ x ∉ t
Theorem: Set.biInter_diff_singleton_eq_diff
Proof state before:
α : Type u_1
ι : Type u_2
s t : Set α
ht : t.Nonempty
⊢ ∀ (x : α), (∀ i ∈ t, x ∈ s ∧ ¬x = i) ↔ x ∈ s ∧ x ∉ t
Tactic:
exact fun x ↦ ⟨fun h ↦ ⟨(h _ ht.some_mem).1, fun hxt ↦ (h x hxt).2 rfl⟩,
  fun h y hyt ↦ ⟨h.1, fun hxy ↦ h.2 <| hxy.symm ▸ hyt⟩⟩
Proof state after:
no goals
Theorem: Set.subset_diff_singleton_iff
Proof state before:
α : Type u_1
ι : Type u_2
s t : Set α
x : α
⊢ s ⊆ t \ {x} ↔ s ⊆ t ∧ x ∉ s
Tactic:
rw [subset_diff, disjoint_singleton_right]
Proof state after:
no goals
Theorem: Set.diff_ssubset
Proof state before:
α : Type u_1
ι : Type u_2
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
⊢ t \ s ⊂ t
Tactic:
refine diff_subset.ssubset_of_ne fun h_eq ↦ ?_
Proof state after:
α : Type u_1
ι : Type u_2
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
h_eq : t \ s = t
⊢ False
Theorem: Set.diff_ssubset
Proof state before:
α : Type u_1
ι : Type u_2
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
h_eq : t \ s = t
⊢ False
Tactic:
rw [sdiff_eq_left, disjoint_iff_inter_eq_empty, inter_eq_self_of_subset_right hst] at h_eq
Proof state after:
α : Type u_1
ι : Type u_2
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
h_eq : s = ∅
⊢ False
Theorem: Set.diff_ssubset
Proof state before:
α : Type u_1
ι : Type u_2
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
h_eq : s = ∅
⊢ False
Tactic:
simp [h_eq] at hs
Proof state after:
no goals
Theorem: Matroid.delete_er_eq'
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
D X : Set α
⊢ (M ＼ D).er X = M.er (X \ D)
Tactic:
rw [← restrict_compl, restrict_er_eq', diff_eq, inter_comm M.E, ← inter_assoc, ← diff_eq,
  er_inter_ground_eq]
Proof state after:
no goals
Theorem: Matroid.delete_er_eq
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
h : Disjoint X D
⊢ (M ＼ D).er X = M.er X
Tactic:
rwa [delete_er_eq', sdiff_eq_left.2]
Proof state after:
no goals
Theorem: Matroid.delete_er_eq_delete_er_diff
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
D X : Set α
⊢ (M ＼ D).er X = (M ＼ D).er (X \ D)
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.delete_rFin_iff
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
⊢ (M ＼ D).rFin X ↔ M.rFin (X \ D)
Tactic:
rw [← er_lt_top_iff, delete_er_eq', er_lt_top_iff]
Proof state after:
no goals
Theorem: Matroid.Coindep.delete_erk_eq
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : M.Coindep X
⊢ (M ＼ X).erk = M.erk
Tactic:
rw [coindep_iff_cl_compl_eq_ground] at hX
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : M.cl (M.E \ X) = M.E
⊢ (M ＼ X).erk = M.erk
Theorem: Matroid.Coindep.delete_erk_eq
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : M.cl (M.E \ X) = M.E
⊢ (M ＼ X).erk = M.erk
Tactic:
rw [erk_eq_er_ground, delete_ground, delete_er_eq', diff_diff, union_self, ← er_cl_eq, hX,
  erk_eq_er_ground]
Proof state after:
no goals
Theorem: Matroid.Indep.delete_erk_dual_eq
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
⊢ (M ／ I)✶.erk = M✶.erk
Tactic:
rw [← hI.coindep.delete_erk_eq, contract_dual_eq_dual_delete]
Proof state after:
no goals
Theorem: Matroid.Indep.erk_dual_restrict_eq
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
⊢ (M ↾ I)✶.erk = 0
Tactic:
simp [hI.restrict_eq_freeOn]
Proof state after:
no goals
Theorem: Matroid.Basis.erk_dual_restrict_of_disjoint
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hB : M.Basis I (I ∪ X)
hdj : Disjoint I X
⊢ (M ↾ (I ∪ X))✶.erk = X.encard
Tactic:
rw [← Base.encard_compl_eq hB.restrict_base]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hB : M.Basis I (I ∪ X)
hdj : Disjoint I X
⊢ ((M ↾ (I ∪ X)).E \ I).encard = X.encard
Theorem: Matroid.Basis.erk_dual_restrict_of_disjoint
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hB : M.Basis I (I ∪ X)
hdj : Disjoint I X
⊢ ((M ↾ (I ∪ X)).E \ I).encard = X.encard
Tactic:
simp [hdj.sdiff_eq_right]
Proof state after:
no goals
Theorem: Matroid.Basis.erk_dual_restrict
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hB : M.Basis I X
⊢ (M ↾ X)✶.erk = (X \ I).encard
Tactic:
rw [← Base.encard_compl_eq hB.restrict_base, restrict_ground_eq]
Proof state after:
no goals
Theorem: Matroid.erk_dual_restrict_eq_zero_iff
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
⊢ (M ↾ I)✶.erk = 0 ↔ M.Indep I
Tactic:
rw [← restrict_eq_freeOn_iff, erk_eq_zero_iff, dual_ground, restrict_ground_eq,
  eq_comm, eq_dual_comm, loopyOn_dual_eq]
Proof state after:
no goals
Theorem: Matroid.Indep.contract_er_dual_eq
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
⊢ (M ／ I)✶.erk = M✶.erk
Tactic:
rw [contract_dual_eq_dual_delete, hI.coindep.delete_erk_eq]
Proof state after:
no goals
Theorem: Matroid.relRank_le_er
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X Y ≤ M.er Y
Tactic:
obtain ⟨I, hI⟩ := (M ／ X).exists_basis (Y ∩ (M ／ X).E)
Proof state after:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y I : Set α
hI : (M ／ X).Basis I (Y ∩ (M ／ X).E)
⊢ M.relRank X Y ≤ M.er Y
Theorem: Matroid.relRank_le_er
Proof state before:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y I : Set α
hI : (M ／ X).Basis I (Y ∩ (M ／ X).E)
⊢ M.relRank X Y ≤ M.er Y
Tactic:
rw [relRank, ← er_inter_ground_eq, ← hI.encard, ← hI.indep.of_contract.er]
Proof state after:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y I : Set α
hI : (M ／ X).Basis I (Y ∩ (M ／ X).E)
⊢ M.er I ≤ M.er Y
Theorem: Matroid.relRank_le_er
Proof state before:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y I : Set α
hI : (M ／ X).Basis I (Y ∩ (M ／ X).E)
⊢ M.er I ≤ M.er Y
Tactic:
exact M.er_mono (hI.subset.trans inter_subset_left)
Proof state after:
no goals
Theorem: Matroid.relRank_eq_er_diff_contract
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X Y = (M ／ X).er (Y \ X)
Tactic:
rw [relRank_eq_er_contract, ← er_cl_eq, contract_cl_eq, eq_comm, ← er_cl_eq, contract_cl_eq,
  diff_union_self]
Proof state after:
no goals
Theorem: Matroid.relRank_eq_union_right
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X Y = M.relRank X (Y ∪ X)
Tactic:
rw [eq_comm, relRank_eq_diff_right, union_diff_right, ← relRank_eq_diff_right]
Proof state after:
no goals
Theorem: Matroid.relRank_mono_left
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X X' Y : Set α
h : X ⊆ X'
⊢ M.relRank X' Y ≤ M.relRank X Y
Tactic:
rw [relRank, relRank, ← union_diff_cancel h, ← contract_contract]
Proof state after:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X X' Y : Set α
h : X ⊆ X'
⊢ (M ／ X ／ (X' \ X)).er Y ≤ (M ／ X).er Y
Theorem: Matroid.relRank_mono_left
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X X' Y : Set α
h : X ⊆ X'
⊢ (M ／ X ／ (X' \ X)).er Y ≤ (M ／ X).er Y
Tactic:
apply relRank_le_er
Proof state after:
no goals
Theorem: Matroid.relRank_empty_right
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
M : Matroid α
X : Set α
⊢ M.relRank X ∅ = 0
Tactic:
rw [relRank_eq_er_contract, er_empty]
Proof state after:
no goals
Theorem: Matroid.relRank_empty_left
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
M : Matroid α
X : Set α
⊢ M.relRank ∅ X = M.er X
Tactic:
rw [relRank_eq_er_contract, contract_empty]
Proof state after:
no goals
Theorem: Matroid.relRank_eq_zero_of_subset
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
h : Y ⊆ X
⊢ M.relRank X Y = 0
Tactic:
rw [relRank_eq_diff_right, diff_eq_empty.2 h, relRank_empty_right]
Proof state after:
no goals
Theorem: Matroid.relRank_cl_left
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank (M.cl X) Y = M.relRank X Y
Tactic:
rw [relRank, relRank, contract_cl_eq_contract_delete, delete_er_eq', LoopEquiv.er_eq_er]
Proof state after:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).LoopEquiv (Y \ (M.cl X \ X)) Y
Theorem: Matroid.relRank_cl_left
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).LoopEquiv (Y \ (M.cl X \ X)) Y
Tactic:
rw [loopEquiv_iff_union_eq_union, contract_loops_eq, diff_union_self]
Proof state after:
no goals
Theorem: Matroid.relRank_cl_right
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X (M.cl Y) = M.relRank X Y
Tactic:
refine le_antisymm ?_ ?_
Proof state after:
case refine_1
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X (M.cl Y) ≤ M.relRank X Y

case refine_2
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X Y ≤ M.relRank X (M.cl Y)
Theorem: Matroid.relRank_cl_right
Proof state before:
case refine_2
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X Y ≤ M.relRank X (M.cl Y)
Tactic:
rw [relRank, ← er_inter_ground_eq, contract_ground, ← inter_diff_assoc]
Proof state after:
case refine_2
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).er ((Y ∩ M.E) \ X) ≤ M.relRank X (M.cl Y)
Theorem: Matroid.relRank_cl_right
Proof state before:
case refine_2
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).er ((Y ∩ M.E) \ X) ≤ M.relRank X (M.cl Y)
Tactic:
exact er_mono _ <| diff_subset.trans
  ((M.subset_cl _).trans (M.cl_subset_cl inter_subset_left))
Proof state after:
no goals
Theorem: Matroid.relRank_cl_right
Proof state before:
case refine_1
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X (M.cl Y) ≤ M.relRank X Y
Tactic:
rw [relRank_eq_er_diff_contract,  relRank, ← (M ／ X).er_cl_eq Y, contract_cl_eq]
Proof state after:
case refine_1
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).er (M.cl Y \ X) ≤ (M ／ X).er (M.cl (Y ∪ X) \ X)
Theorem: Matroid.relRank_cl_right
Proof state before:
case refine_1
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).er (M.cl Y \ X) ≤ (M ／ X).er (M.cl (Y ∪ X) \ X)
Tactic:
exact (M ／ X).er_mono (diff_subset_diff_left (M.cl_subset_cl subset_union_left))
Proof state after:
no goals
Theorem: Matroid.relRank_inter_ground_left
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank (X ∩ M.E) Y = M.relRank X Y
Tactic:
rw [←relRank_cl_left, cl_inter_ground, relRank_cl_left]
Proof state after:
no goals
Theorem: Matroid.relRank_inter_ground_right
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X (Y ∩ M.E) = M.relRank X Y
Tactic:
rw [← relRank_cl_right, eq_comm, ← relRank_cl_right, cl_inter_ground]
Proof state after:
no goals