internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Coloop.not_connected
Proof state before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K✝ : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
hconn : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.ConnectedTo e f
K : Set α
hK : M.Circuit K
heK : e ∈ K
⊢ False
Tactic:
exact he.not_mem_circuit hK heK
Proof state after:
no goals
Theorem: Matroid.Loop.not_connected
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
he : M.Loop e
hE : M.E.Nontrivial
⊢ ¬M.Connected
Tactic:
rw [← connected_dual_iff]
Proof state after:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
he : M.Loop e
hE : M.E.Nontrivial
⊢ ¬M✶.Connected
Theorem: Matroid.Loop.not_connected
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
he : M.Loop e
hE : M.E.Nontrivial
⊢ ¬M✶.Connected
Tactic:
exact he.dual_coloop.not_connected hE
Proof state after:
no goals
Theorem: Matroid.Connected.loopless
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.Connected
hE : M.E.Nontrivial
⊢ M.Loopless
Tactic:
rw [loopless_iff_forall_not_loop]
Proof state after:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.Connected
hE : M.E.Nontrivial
⊢ ∀ e ∈ M.E, ¬M.Loop e
Theorem: Matroid.Connected.loopless
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.Connected
hE : M.E.Nontrivial
⊢ ∀ e ∈ M.E, ¬M.Loop e
Tactic:
exact fun e _ hl ↦ hl.not_connected hE hM
Proof state after:
no goals
Theorem: Matroid.Connected.exists_circuit
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.Connected
hM : M.E.Nontrivial
he : e ∈ M.E
hf : f ∈ M.E
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ f ∈ C
Tactic:
obtain (rfl | hne) := eq_or_ne e f
Proof state after:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.Connected
hM : M.E.Nontrivial
he : e ∈ M.E
hf : f ∈ M.E
hne : e ≠ f
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ f ∈ C
Theorem: Matroid.Connected.exists_circuit
Proof state before:
case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.Connected
hM : M.E.Nontrivial
he : e ∈ M.E
hf : f ∈ M.E
hne : e ≠ f
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ f ∈ C
Tactic:
exact (h.2 he hf).exists_circuit_of_ne hne
Proof state after:
no goals
Theorem: Matroid.Connected.exists_circuit
Proof state before:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
Tactic:
obtain (he' | he') := em (M.Coloop e)
Proof state after:
case inl.inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : M.Coloop e
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C

case inl.inr
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : ¬M.Coloop e
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
Theorem: Matroid.Connected.exists_circuit
Proof state before:
case inl.inr
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : ¬M.Coloop e
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
Tactic:
obtain ⟨C, hC, heC⟩ := exists_mem_circuit_of_not_coloop he he'
Proof state after:
case inl.inr.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : ¬M.Coloop e
C : Set α
hC : M.Circuit C
heC : e ∈ C
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
Theorem: Matroid.Connected.exists_circuit
Proof state before:
case inl.inr.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : ¬M.Coloop e
C : Set α
hC : M.Circuit C
heC : e ∈ C
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
Tactic:
exact ⟨C, hC, heC, heC⟩
Proof state after:
no goals
Theorem: Matroid.Connected.exists_circuit
Proof state before:
case inl.inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : M.Coloop e
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
Tactic:
exact False.elim <| he'.not_connected hM h
Proof state after:
no goals
Theorem: Matroid.singleton_connected
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.E = {e}
⊢ M.E.Nonempty
Tactic:
simp [hM]
Proof state after:
no goals
Theorem: Matroid.singleton_connected
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.E = {e}
⊢ ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.ConnectedTo e f
Tactic:
simp [hM]
Proof state after:
no goals
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
α : Type u_1
M : Matroid α
B B' I I' J K X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
obtain ⟨K, hK, hIK⟩ := hI.subset_basis_of_subset (subset_union_left (s := I) (t := J))
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
have hsk := (hK.indep.subset_skew_diff hIK)
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew I (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew I (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
rw [skew_iff_cl_skew_left] at hsk
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
have' hdj := hsk.disjoint_of_indep_subset_right (hK.indep.diff _) Subset.rfl
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
have hb' : ∀ ⦃B⦄, M.Basis B (M.cl I) →
    (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard := by
  intro B hB
  rw [(hb hB).1.erk_dual_restrict, union_diff_left,
    ← encard_diff_add_encard_inter (J \ (K \ I)) B, add_comm, inter_comm _ B,
    inter_diff_distrib_left, (hdj.mono_left hB.subset).inter_eq, diff_empty]
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
have hind : ∀ Y, (M ↾ (Y ∪ J)).Indep (K \ I) := by
  intro Y
  rw [restrict_indep_iff, and_iff_right (hK.indep.diff I), diff_subset_iff, union_comm Y,
    ← union_assoc]
  exact hK.subset.trans subset_union_left
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
hind : ∀ (Y : Set α), (M ↾ (Y ∪ J)).Indep (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
hind : ∀ (Y : Set α), (M ↾ (Y ∪ J)).Indep (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
have hI'b := hII'.symm ▸ hI'.basis_cl
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
hind : ∀ (Y : Set α), (M ↾ (Y ∪ J)).Indep (K \ I)
hI'b : M.Basis I' (M.cl I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
hind : ∀ (Y : Set α), (M ↾ (Y ∪ J)).Indep (K \ I)
hI'b : M.Basis I' (M.cl I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
rw [← (hind I).contract_er_dual_eq,  ← (hind I').contract_er_dual_eq,
  restrict_contract_eq_contract_restrict _ (hb hI.basis_cl).2,
  restrict_contract_eq_contract_restrict _ (hb hI'b).2,
  union_diff_distrib, sdiff_eq_left.2 disjoint_sdiff_right,
  union_diff_distrib, sdiff_eq_left.2 (hdj.mono_left hI'b.subset), hb' hI.basis_cl, hb' hI'b]
Proof state after:
no goals
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
⊢ ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
Tactic:
refine fun B hB ↦ ⟨Indep.basis_of_subset_of_subset_cl ?_ ?_ ?_, ?_⟩
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ (M ／ (K \ I)).Indep B

case refine_2
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ⊆ B ∪ J \ (K \ I)

case refine_3
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ∪ J \ (K \ I) ⊆ (M ／ (K \ I)).cl B

case refine_4
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ K \ I ⊆ B ∪ J
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case refine_4
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ K \ I ⊆ B ∪ J
Tactic:
rw [diff_subset_iff, union_comm B, ← union_assoc]
Proof state after:
case refine_4
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ K ⊆ I ∪ J ∪ B
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case refine_4
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ K ⊆ I ∪ J ∪ B
Tactic:
exact hK.subset.trans <| subset_union_left
Proof state after:
no goals
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ (M ／ (K \ I)).Indep B
Tactic:
rw [(hK.indep.diff _).contract_indep_iff]
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ Disjoint B (K \ I) ∧ M.Indep (B ∪ K \ I)
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ Disjoint B (K \ I) ∧ M.Indep (B ∪ K \ I)
Tactic:
exact ⟨hdj.mono_left hB.subset,
  hsk.union_indep_of_indep_subsets hB.indep hB.subset (hK.indep.diff _) Subset.rfl⟩
Proof state after:
no goals
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ⊆ B ∪ J \ (K \ I)
Tactic:
exact subset_union_left
Proof state after:
no goals
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case refine_3
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ∪ J \ (K \ I) ⊆ (M ／ (K \ I)).cl B
Tactic:
rw [contract_cl_eq, subset_diff, disjoint_union_left, and_iff_left disjoint_sdiff_left,
  and_iff_left (hdj.mono_left hB.subset), ← cl_union_cl_left_eq, hB.cl_eq_cl, cl_cl,
  cl_union_cl_left_eq, union_diff_self, union_eq_self_of_subset_left hIK, hK.cl_eq_cl]
Proof state after:
case refine_3
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ∪ J \ (K \ I) ⊆ M.cl (I ∪ J)
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
case refine_3
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ∪ J \ (K \ I) ⊆ M.cl (I ∪ J)
Tactic:
exact union_subset (hB.subset.trans (M.cl_subset_cl subset_union_left))
  (M.subset_cl_of_subset (diff_subset.trans subset_union_right))
Proof state after:
no goals
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
⊢ ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Tactic:
intro B hB
Proof state after:
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
B : Set α
hB : M.Basis B (M.cl I)
⊢ (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
B : Set α
hB : M.Basis B (M.cl I)
⊢ (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Tactic:
rw [(hb hB).1.erk_dual_restrict, union_diff_left,
  ← encard_diff_add_encard_inter (J \ (K \ I)) B, add_comm, inter_comm _ B,
  inter_diff_distrib_left, (hdj.mono_left hB.subset).inter_eq, diff_empty]
Proof state after:
no goals
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
⊢ ∀ (Y : Set α), (M ↾ (Y ∪ J)).Indep (K \ I)
Tactic:
intro Y
Proof state after:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y✝ : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Y : Set α
⊢ (M ↾ (Y ∪ J)).Indep (K \ I)
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y✝ : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Y : Set α
⊢ (M ↾ (Y ∪ J)).Indep (K \ I)
Tactic:
rw [restrict_indep_iff, and_iff_right (hK.indep.diff I), diff_subset_iff, union_comm Y,
  ← union_assoc]
Proof state after:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y✝ : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Y : Set α
⊢ K ⊆ I ∪ J ∪ Y
Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl
Proof state before:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y✝ : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Y : Set α
⊢ K ⊆ I ∪ J ∪ Y
Tactic:
exact hK.subset.trans subset_union_left
Proof state after:
no goals
Theorem: Matroid.Basis'.encard_dual_switch_switch_eq
Proof state before:
α : Type u_1
M : Matroid α
B B' I✝ I'✝ J✝ K X✝ Y✝ I I' J J' X Y : Set α
hI : M.Basis' I X
hI' : M.Basis' I' X
hJ : M.Basis' J Y
hJ' : M.Basis' J' Y
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J').encard + (M ↾ (I' ∪ J'))✶.erk
Tactic:
rw [hI.indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl hI'.indep
    (by rw [hI.cl_eq_cl, hI'.cl_eq_cl]) hJ.indep,
  inter_comm, union_comm, hJ.indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl hJ'.indep
    (by rw [hJ.cl_eq_cl, hJ'.cl_eq_cl]) hI'.indep, inter_comm, union_comm]
Proof state after:
no goals