internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
⊢ False
Tactic:
have hCss : M.fundCct e B₂ \ {e} ⊆ B₂ := by
  rw [diff_subset_iff, singleton_union]; exact fundCct_subset_insert _ _
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
⊢ False
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
⊢ False
Tactic:
have hcl : M.fundCct e B₂ ⊆ M.cl (B₁ \ {e}) := by
  refine' (hC.subset_cl_diff_singleton e).trans (cl_subset_cl_of_subset_cl (fun f hf ↦ _))
  have hef : f ≠ e := by rintro rfl; exact hf.2 rfl
  rw [(hB₁.indep.diff {e}).mem_cl_iff, dep_iff, insert_subset_iff,
    and_iff_left (diff_subset.trans hB₁.subset_ground), or_iff_not_imp_right, mem_diff,
    and_iff_left (hC.subset_ground hf.1), mem_singleton_iff,
    and_iff_left hef, insert_diff_singleton_comm hef]
  exact fun hfB₁ ↦ h _ ⟨hCss hf,hfB₁⟩ (diff_subset hf)
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
hcl : M.fundCct e B₂ ⊆ M.cl (B₁ \ {e})
⊢ False
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
hcl : M.fundCct e B₂ ⊆ M.cl (B₁ \ {e})
⊢ False
Tactic:
exact hB₁.indep.not_mem_cl_diff_of_mem he.1 (hcl (mem_fundCct _ _ _))
Proof state after:
no goals
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
h1 : ∃ f ∈ B₂ \ B₁, M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})
⊢ ∃ f ∈ B₂ \ B₁, M.Base (insert e B₂ \ {f}) ∧ M.Base (insert f B₁ \ {e})
Tactic:
obtain ⟨f, hf, h₁, h₂⟩ := h1
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
f : α
hf : f ∈ B₂ \ B₁
h₁ : M.Indep (insert e B₂ \ {f})
h₂ : M.Indep (insert f B₁ \ {e})
⊢ ∃ f ∈ B₂ \ B₁, M.Base (insert e B₂ \ {f}) ∧ M.Base (insert f B₁ \ {e})
Theorem: Matroid.Base.strong_exchange
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
f : α
hf : f ∈ B₂ \ B₁
h₁ : M.Indep (insert e B₂ \ {f})
h₂ : M.Indep (insert f B₁ \ {e})
⊢ ∃ f ∈ B₂ \ B₁, M.Base (insert e B₂ \ {f}) ∧ M.Base (insert f B₁ \ {e})
Tactic:
exact ⟨f, hf, hB₂.exchange_base_of_indep' hf.1 he.2 h₁,
  hB₁.exchange_base_of_indep' he.1 hf.2 h₂⟩
Proof state after:
no goals
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
⊢ e ∈ M.cl B₂ \ B₂
Tactic:
rw [hB₂.cl_eq]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
⊢ e ∈ M.E \ B₂
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
⊢ e ∈ M.E \ B₂
Tactic:
exact ⟨hB₁.subset_ground he.1, he.2⟩
Proof state after:
no goals
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
⊢ M.fundCct e B₂ \ {e} ⊆ B₂
Tactic:
rw [diff_subset_iff, singleton_union]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
⊢ M.fundCct e B₂ ⊆ insert e B₂
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
⊢ M.fundCct e B₂ ⊆ insert e B₂
Tactic:
exact fundCct_subset_insert _ _
Proof state after:
no goals
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
⊢ M.fundCct e B₂ ⊆ M.cl (B₁ \ {e})
Tactic:
refine' (hC.subset_cl_diff_singleton e).trans (cl_subset_cl_of_subset_cl (fun f hf ↦ _))
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
⊢ f ∈ M.cl (B₁ \ {e})
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
⊢ f ∈ M.cl (B₁ \ {e})
Tactic:
have hef : f ≠ e := by rintro rfl; exact hf.2 rfl
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
hef : f ≠ e
⊢ f ∈ M.cl (B₁ \ {e})
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
hef : f ≠ e
⊢ f ∈ M.cl (B₁ \ {e})
Tactic:
rw [(hB₁.indep.diff {e}).mem_cl_iff, dep_iff, insert_subset_iff,
  and_iff_left (diff_subset.trans hB₁.subset_ground), or_iff_not_imp_right, mem_diff,
  and_iff_left (hC.subset_ground hf.1), mem_singleton_iff,
  and_iff_left hef, insert_diff_singleton_comm hef]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
hef : f ≠ e
⊢ f ∉ B₁ → ¬M.Indep (insert f B₁ \ {e})
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
hef : f ≠ e
⊢ f ∉ B₁ → ¬M.Indep (insert f B₁ \ {e})
Tactic:
exact fun hfB₁ ↦ h _ ⟨hCss hf,hfB₁⟩ (diff_subset hf)
Proof state after:
no goals
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
⊢ f ≠ e
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
f : α
he : f ∈ B₁ \ B₂
he₁ : f ∈ M.cl B₂ \ B₂
h : ∀ f_1 ∈ B₂ \ B₁, f_1 ∈ M.fundCct f B₂ → ¬M.Indep (insert f_1 B₁ \ {f})
hC : M.Circuit (M.fundCct f B₂)
hCss : M.fundCct f B₂ \ {f} ⊆ B₂
hf : f ∈ M.fundCct f B₂ \ {f}
⊢ False
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
f : α
he : f ∈ B₁ \ B₂
he₁ : f ∈ M.cl B₂ \ B₂
h : ∀ f_1 ∈ B₂ \ B₁, f_1 ∈ M.fundCct f B₂ → ¬M.Indep (insert f_1 B₁ \ {f})
hC : M.Circuit (M.fundCct f B₂)
hCss : M.fundCct f B₂ \ {f} ⊆ B₂
hf : f ∈ M.fundCct f B₂ \ {f}
⊢ False
Tactic:
exact hf.2 rfl
Proof state after:
no goals
Theorem: Matroid.Basis.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
⊢ ∃ f ∈ I₂ \ I₁, M.Basis (insert e I₂ \ {f}) X ∧ M.Basis (insert f I₁ \ {e}) X
Tactic:
obtain ⟨f, hf, h₁, h₂⟩ := hI₁.base_restrict.strong_exchange hI₂.base_restrict he
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
f : α
hf : f ∈ I₂ \ I₁
h₁ : (M ↾ X).Base (insert e I₂ \ {f})
h₂ : (M ↾ X).Base (insert f I₁ \ {e})
⊢ ∃ f ∈ I₂ \ I₁, M.Basis (insert e I₂ \ {f}) X ∧ M.Basis (insert f I₁ \ {e}) X
Theorem: Matroid.Basis.strong_exchange
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
f : α
hf : f ∈ I₂ \ I₁
h₁ : (M ↾ X).Base (insert e I₂ \ {f})
h₂ : (M ↾ X).Base (insert f I₁ \ {e})
⊢ ∃ f ∈ I₂ \ I₁, M.Basis (insert e I₂ \ {f}) X ∧ M.Basis (insert f I₁ \ {e}) X
Tactic:
rw [base_restrict_iff] at h₁ h₂
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
f : α
hf : f ∈ I₂ \ I₁
h₁ : M.Basis (insert e I₂ \ {f}) X
h₂ : M.Basis (insert f I₁ \ {e}) X
⊢ ∃ f ∈ I₂ \ I₁, M.Basis (insert e I₂ \ {f}) X ∧ M.Basis (insert f I₁ \ {e}) X
Theorem: Matroid.Basis.strong_exchange
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
f : α
hf : f ∈ I₂ \ I₁
h₁ : M.Basis (insert e I₂ \ {f}) X
h₂ : M.Basis (insert f I₁ \ {e}) X
⊢ ∃ f ∈ I₂ \ I₁, M.Basis (insert e I₂ \ {f}) X ∧ M.Basis (insert f I₁ \ {e}) X
Tactic:
exact ⟨f, hf, h₁, h₂⟩
Proof state after:
no goals
Theorem: Matroid.Basis.rev_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
⊢ ∀ (a : α),
    a ∈ I₂ \ I₁ ∧ M.Basis (insert e I₂ \ {a}) X ∧ M.Basis (insert a I₁ \ {e}) X →
      a ∈ I₂ \ I₁ ∧ M.Basis (insert e I₂ \ {a}) X
Tactic:
simp only [mem_diff, mem_insert_iff, mem_singleton_iff]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
⊢ ∀ (a : α),
    (a ∈ I₂ ∧ a ∉ I₁) ∧ M.Basis (insert e I₂ \ {a}) X ∧ M.Basis (insert a I₁ \ {e}) X →
      (a ∈ I₂ ∧ a ∉ I₁) ∧ M.Basis (insert e I₂ \ {a}) X
Theorem: Matroid.Basis.rev_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
⊢ ∀ (a : α),
    (a ∈ I₂ ∧ a ∉ I₁) ∧ M.Basis (insert e I₂ \ {a}) X ∧ M.Basis (insert a I₁ \ {e}) X →
      (a ∈ I₂ ∧ a ∉ I₁) ∧ M.Basis (insert e I₂ \ {a}) X
Tactic:
tauto
Proof state after:
no goals
Theorem: Matroid.Iso.circuit_image
Proof state before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
⊢ N.Circuit ↑(⇑e '' C)
Tactic:
simp_rw [circuit_iff, ← e.dep_image_iff, and_iff_right hC.dep]
Proof state after:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
⊢ ∀ ⦃I : Set β⦄, N.Dep I → I ⊆ ↑(⇑e '' C) → I = ↑(⇑e '' C)
Theorem: Matroid.Iso.circuit_image
Proof state before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
⊢ ∀ ⦃I : Set β⦄, N.Dep I → I ⊆ ↑(⇑e '' C) → I = ↑(⇑e '' C)
Tactic:
intro I hI hIC
Proof state after:
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
I : Set β
hI : N.Dep I
hIC : I ⊆ ↑(⇑e '' C)
⊢ I = ↑(⇑e '' C)
Theorem: Matroid.Iso.circuit_image
Proof state before:
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
I : Set β
hI : N.Dep I
hIC : I ⊆ ↑(⇑e '' C)
⊢ I = ↑(⇑e '' C)
Tactic:
obtain ⟨I,rfl⟩ := Subset.eq_image_val hI.subset_ground
Proof state after:
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
I : Set ↑N.E
hI : N.Dep ↑I
hIC : ↑I ⊆ ↑(⇑e '' C)
⊢ ↑I = ↑(⇑e '' C)
Theorem: Matroid.Iso.circuit_image
Proof state before:
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
I : Set ↑N.E
hI : N.Dep ↑I
hIC : ↑I ⊆ ↑(⇑e '' C)
⊢ ↑I = ↑(⇑e '' C)
Tactic:
replace hC := hC.eq_of_dep_subset (e.symm.image_dep hI)
Proof state after:
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
I : Set ↑N.E
hI : N.Dep ↑I
hIC : ↑I ⊆ ↑(⇑e '' C)
hC : ↑(⇑e.symm '' I) ⊆ ↑C → ↑(⇑e.symm '' I) = ↑C
⊢ ↑I = ↑(⇑e '' C)
Theorem: Matroid.Iso.circuit_image
Proof state before:
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
I : Set ↑N.E
hI : N.Dep ↑I
hIC : ↑I ⊆ ↑(⇑e '' C)
hC : ↑(⇑e.symm '' I) ⊆ ↑C → ↑(⇑e.symm '' I) = ↑C
⊢ ↑I = ↑(⇑e '' C)
Tactic:
simp only [image_subset_iff, preimage_val_image_val_eq_self, image_symm_eq_preimage,
  preimage_subset_iff, image_val_inj] at hIC hC
Proof state after:
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
I : Set ↑N.E
hI : N.Dep ↑I
hIC : I ⊆ ⇑e '' C
hC : I ⊆ ⇑e '' C → ⇑e ⁻¹' I = C
⊢ ↑I = ↑(⇑e '' C)
Theorem: Matroid.Iso.circuit_image
Proof state before:
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
I : Set ↑N.E
hI : N.Dep ↑I
hIC : I ⊆ ⇑e '' C
hC : I ⊆ ⇑e '' C → ⇑e ⁻¹' I = C
⊢ ↑I = ↑(⇑e '' C)
Tactic:
simp [← hC hIC]
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_dep_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E
Tactic:
by_cases hD : D ⊆ E
Proof state after:
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hD : D ⊆ E
⊢ (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E

case neg
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hD : ¬D ⊆ E
⊢ (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E
Theorem: Matroid.uniqueBaseOn_dep_iff
Proof state before:
case neg
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hD : ¬D ⊆ E
⊢ (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E
Tactic:
exact iff_of_false (fun h ↦ hD h.subset_ground) (by simp [hD])
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_dep_iff
Proof state before:
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hD : D ⊆ E
⊢ (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E
Tactic:
simp (config := {contextual := true}) [← not_indep_iff (M := uniqueBaseOn I E) hD, hD,
  nonempty_iff_ne_empty, not_imp_not]
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_dep_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hD : ¬D ⊆ E
⊢ ¬(D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E)
Tactic:
simp [hD]
Proof state after:
no goals
Theorem: Matroid.loopyOn_dep_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ (loopyOn E).Dep D ↔ D.Nonempty ∧ D ⊆ E
Tactic:
simp [Dep, nonempty_iff_ne_empty]
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ (uniqueBaseOn I E).Circuit C ↔ ∃ e ∈ E \ I, C = {e}
Tactic:
simp only [circuit_iff_dep_forall_diff_singleton_indep, uniqueBaseOn_dep_iff,
  uniqueBaseOn_indep_iff', subset_inter_iff, diff_singleton_subset_iff, mem_diff]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ ((C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E) ↔ ∃ e, (e ∈ E ∧ e ∉ I) ∧ C = {e}
Theorem: Matroid.uniqueBaseOn_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ ((C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E) ↔ ∃ e, (e ∈ E ∧ e ∉ I) ∧ C = {e}
Tactic:
refine ⟨fun ⟨⟨⟨e,he⟩, hCI, hCE⟩, h2⟩ ↦ ⟨e, ⟨hCE he, fun heI ↦ hCI ?_⟩, ?_⟩, ?_⟩
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
heI : e ∈ I
⊢ C ⊆ I

case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
⊢ C = {e}

case refine_3
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ (∃ e, (e ∈ E ∧ e ∉ I) ∧ C = {e}) → (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
Theorem: Matroid.uniqueBaseOn_circuit_iff
Proof state before:
case refine_3
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ (∃ e, (e ∈ E ∧ e ∉ I) ∧ C = {e}) → (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
Tactic:
rintro ⟨e, ⟨heI,heC⟩, rfl⟩
Proof state after:
case refine_3.intro.intro.intro
α : Type u_1
M : Matroid α
C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
e : α
heI : e ∈ E
heC : e ∉ I
⊢ ({e}.Nonempty ∧ ¬{e} ⊆ I ∧ {e} ⊆ E) ∧ ∀ e_1 ∈ {e}, {e} ⊆ insert e_1 I ∧ {e} ⊆ insert e_1 E
Theorem: Matroid.uniqueBaseOn_circuit_iff
Proof state before:
case refine_3.intro.intro.intro
α : Type u_1
M : Matroid α
C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
e : α
heI : e ∈ E
heC : e ∉ I
⊢ ({e}.Nonempty ∧ ¬{e} ⊆ I ∧ {e} ⊆ E) ∧ ∀ e_1 ∈ {e}, {e} ⊆ insert e_1 I ∧ {e} ⊆ insert e_1 E
Tactic:
simp [heI, heC]
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_circuit_iff
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
heI : e ∈ I
⊢ C ⊆ I
Tactic:
exact (h2 e he).1.trans (insert_subset heI Subset.rfl)
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_circuit_iff
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
⊢ C = {e}
Tactic:
suffices hsub : C.Subsingleton from hsub.eq_singleton_of_mem he
Proof state after:
case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
⊢ C.Subsingleton
Theorem: Matroid.uniqueBaseOn_circuit_iff
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
⊢ C.Subsingleton
Tactic:
refine fun f hf f' hf' ↦ by_contra fun hne ↦ hCI ?_
Proof state after:
case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f✝ x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
f : α
hf : f ∈ C
f' : α
hf' : f' ∈ C
hne : ¬f = f'
⊢ C ⊆ I
Theorem: Matroid.uniqueBaseOn_circuit_iff
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f✝ x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
f : α
hf : f ∈ C
f' : α
hf' : f' ∈ C
hne : ¬f = f'
⊢ C ⊆ I
Tactic:
simpa [inter_insert_eq hne] using subset_inter (h2 f hf).1 (h2 f' hf').1
Proof state after:
no goals
Theorem: Matroid.loopyOn_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E✝ D E : Set α
⊢ (loopyOn E).Circuit C ↔ ∃ e ∈ E, C = {e}
Tactic:
simp [← uniqueBaseOn_empty]
Proof state after:
no goals
Theorem: Matroid.freeOn_not_circuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E✝ D E : Set α
⊢ ¬(freeOn E).Circuit C
Tactic:
simp [← uniqueBaseOn_self]
Proof state after:
no goals
Theorem: Matroid.emptyOn_not_circuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ ¬(emptyOn α).Circuit C
Tactic:
simp [← freeOn_empty]
Proof state after:
no goals
Theorem: Matroid.girth_emptyOn
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ (emptyOn α).girth = ⊤
Tactic:
simp [girth]
Proof state after:
no goals
Theorem: Matroid.girth_freeOn
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ (freeOn E).girth = ⊤
Tactic:
simp [Subset.rfl]
Proof state after:
no goals