internlm/Lean-Github huggingface dataset:
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_2.intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
⊢ Nonempty (unifOn E ↑a ≂ unif a b)
Tactic:
obtain ⟨e⟩ := Fin.nonempty_equiv_iff_encard_eq.2 hE
Proof state after:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
⊢ Nonempty (unifOn E ↑a ≂ unif a b)
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
⊢ Nonempty (unifOn E ↑a ≂ unif a b)
Tactic:
refine ⟨e.trans (Equiv.Set.univ (Fin b)).symm, fun I ↦ ?_⟩
Proof state after:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ (unifOn E ↑a).Indep ↑I ↔ (unif a b).Indep ↑(⇑(e.trans (Equiv.Set.univ (Fin b)).symm) '' I)
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ (unifOn E ↑a).Indep ↑I ↔ (unif a b).Indep ↑(⇑(e.trans (Equiv.Set.univ (Fin b)).symm) '' I)
Tactic:
simp only [unifOn_indep_iff, Subtype.val_injective.encard_image, image_subset_iff, unif_ground_eq,
  Equiv.Set.univ, Equiv.trans_apply, Equiv.coe_fn_symm_mk, unif_indep_iff]
Proof state after:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ I.encard ≤ ↑a ∧ I ⊆ Subtype.val ⁻¹' E ↔ ((fun a_1 => ⟨e a_1, trivial⟩) '' I).encard ≤ ↑a
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ I.encard ≤ ↑a ∧ I ⊆ Subtype.val ⁻¹' E ↔ ((fun a_1 => ⟨e a_1, trivial⟩) '' I).encard ≤ ↑a
Tactic:
rw [Function.Injective.encard_image (fun _ _ ↦ by simp), and_iff_left_iff_imp]
Proof state after:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ I.encard ≤ ↑a → I ⊆ Subtype.val ⁻¹' E
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ I.encard ≤ ↑a → I ⊆ Subtype.val ⁻¹' E
Tactic:
exact fun _ ⟨_,hx⟩ _ ↦ hx
Proof state after:
no goals
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
⊢ M = unifOn M.E ↑a ∧ M.E.encard = ↑b
Tactic:
rw [eq_unifOn_iff, and_iff_right rfl, and_iff_left <| by simpa using e.toEquiv.encard_eq]
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
⊢ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
⊢ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
Tactic:
refine fun I ↦ ?_
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
Tactic:
obtain (hIE | hIE) := em' <| I ⊆ M.E
Proof state after:
case refine_1.inl
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : ¬I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E

case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
Tactic:
rw [and_iff_left hIE]
Proof state after:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a
Tactic:
have hwin := e.indep_image_iff (I := M.E ↓∩ I)
Proof state after:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
hwin : M.Indep ↑(M.E ↓∩ I) ↔ (unif a b).Indep ↑(⇑e '' M.E ↓∩ I)
⊢ M.Indep I ↔ I.encard ≤ ↑a
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
hwin : M.Indep ↑(M.E ↓∩ I) ↔ (unif a b).Indep ↑(⇑e '' M.E ↓∩ I)
⊢ M.Indep I ↔ I.encard ≤ ↑a
Tactic:
simp only [Subtype.image_preimage_coe, inter_eq_self_of_subset_right hIE, unif_ground_eq,
  unif_indep_iff] at hwin
Proof state after:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
hwin : M.Indep I ↔ ((fun a => ↑a) '' ((fun a_1 => e a_1) '' M.E ↓∩ I)).encard ≤ ↑a
⊢ M.Indep I ↔ I.encard ≤ ↑a
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
hwin : M.Indep I ↔ ((fun a => ↑a) '' ((fun a_1 => e a_1) '' M.E ↓∩ I)).encard ≤ ↑a
⊢ M.Indep I ↔ I.encard ≤ ↑a
Tactic:
rwa [Subtype.val_injective.encard_image, (EmbeddingLike.injective' _).encard_image,
  encard_preimage_of_injective_subset_range Subtype.val_injective (by simpa)] at hwin
Proof state after:
no goals
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
⊢ M.E.encard = ↑b
Tactic:
simpa using e.toEquiv.encard_eq
Proof state after:
no goals
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_1.inl
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : ¬I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
Tactic:
exact iff_of_false (fun h ↦ hIE h.subset_ground) (by simp [hIE])
Proof state after:
no goals
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : ¬I ⊆ M.E
⊢ ¬(I.encard ≤ ↑a ∧ I ⊆ M.E)
Tactic:
simp [hIE]
Proof state after:
no goals
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
hwin : M.Indep I ↔ (M.E ↓∩ I).encard ≤ ↑a
⊢ I ⊆ range Subtype.val
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
x✝¹ x✝ : ↑(unifOn E ↑a).E
⊢ ⟨e x✝¹, trivial⟩ = ⟨e x✝, trivial⟩ → x✝¹ = x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.nonempty_iso_unif_iff'
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ Nonempty (M ≂ unif a b) ↔ M = unifOn M.E ↑a ∧ M.E.encard = ↑b
Tactic:
rw [nonempty_iso_unif_iff]
Proof state after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (∃ E, M = unifOn E ↑a ∧ E.encard = ↑b) ↔ M = unifOn M.E ↑a ∧ M.E.encard = ↑b
Theorem: Matroid.nonempty_iso_unif_iff'
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (∃ E, M = unifOn E ↑a ∧ E.encard = ↑b) ↔ M = unifOn M.E ↑a ∧ M.E.encard = ↑b
Tactic:
exact ⟨by rintro ⟨E, rfl, h⟩; simp [h], fun h ↦ ⟨M.E, by simpa⟩⟩
Proof state after:
no goals
Theorem: Matroid.nonempty_iso_unif_iff'
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (∃ E, M = unifOn E ↑a ∧ E.encard = ↑b) → M = unifOn M.E ↑a ∧ M.E.encard = ↑b
Tactic:
rintro ⟨E, rfl, h⟩
Proof state after:
case intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
h : E.encard = ↑b
⊢ unifOn E ↑a = unifOn (unifOn E ↑a).E ↑a ∧ (unifOn E ↑a).E.encard = ↑b
Theorem: Matroid.nonempty_iso_unif_iff'
Proof state before:
case intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
h : E.encard = ↑b
⊢ unifOn E ↑a = unifOn (unifOn E ↑a).E ↑a ∧ (unifOn E ↑a).E.encard = ↑b
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Matroid.nonempty_iso_unif_iff'
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
h : M = unifOn M.E ↑a ∧ M.E.encard = ↑b
⊢ M = unifOn M.E ↑a ∧ M.E.encard = ↑b
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.nonempty_iso_line_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' n : ℕ
⊢ Nonempty (M ≂ unif 2 n) ↔ M.Simple ∧ M.erk ≤ 2 ∧ M.E.encard = ↑n
Tactic:
simp [nonempty_iso_unif_iff', ← and_assoc, and_congr_left_iff, eq_unifOn_two_iff, and_comm]
Proof state after:
no goals
Theorem: Matroid.unif_isoMinor_unif_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ d₂ : ℕ
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂)) ↔ a₁ ≤ a₂ ∧ d₁ ≤ d₂
Tactic:
refine ⟨fun ⟨e⟩ ↦ ⟨by simpa using e.rk_le, by simpa using IsoMinor.rk_le e.dual⟩, fun h ↦ ?_⟩
Proof state after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ d₂ : ℕ
h : a₁ ≤ a₂ ∧ d₁ ≤ d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂))
Theorem: Matroid.unif_isoMinor_unif_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ d₂ : ℕ
h : a₁ ≤ a₂ ∧ d₁ ≤ d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂))
Tactic:
obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le h.1
Proof state after:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ d₁ d₂ j : ℕ
h : a₁ ≤ a₁ + j ∧ d₁ ≤ d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif (a₁ + j) (a₁ + j + d₂))
Theorem: Matroid.unif_isoMinor_unif_iff
Proof state before:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ d₁ d₂ j : ℕ
h : a₁ ≤ a₁ + j ∧ d₁ ≤ d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif (a₁ + j) (a₁ + j + d₂))
Tactic:
exact ⟨(unif_isoMinor_contr a₁ (a₁ + d₁) j).trans (unif_isoRestr_unif _ (by linarith)).isoMinor⟩
Proof state after:
no goals
Theorem: Matroid.unif_isoMinor_unif_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ d₂ : ℕ
x✝ : Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂))
e : unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂)
⊢ a₁ ≤ a₂
Tactic:
simpa using e.rk_le
Proof state after:
no goals
Theorem: Matroid.unif_isoMinor_unif_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ d₂ : ℕ
x✝ : Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂))
e : unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂)
⊢ d₁ ≤ d₂
Tactic:
simpa using IsoMinor.rk_le e.dual
Proof state after:
no goals
Theorem: Matroid.unif_isoMinor_unif_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ d₁ d₂ j : ℕ
h : a₁ ≤ a₁ + j ∧ d₁ ≤ d₂
⊢ a₁ + d₁ + j ≤ a₁ + j + d₂
Tactic:
linarith
Proof state after:
no goals
Theorem: Matroid.unif_isoMinor_unif_iff'
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ b₁ b₂ : ℕ
h₁ : a₁ ≤ b₁
h₂ : a₂ ≤ b₂
⊢ Nonempty (unif a₁ b₁ ≤i unif a₂ b₂) ↔ a₁ ≤ a₂ ∧ b₁ - a₁ ≤ b₂ - a₂
Tactic:
obtain ⟨d₁, rfl⟩ := Nat.exists_eq_add_of_le h₁
Proof state after:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ b₂ : ℕ
h₂ : a₂ ≤ b₂
d₁ : ℕ
h₁ : a₁ ≤ a₁ + d₁
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ b₂) ↔ a₁ ≤ a₂ ∧ a₁ + d₁ - a₁ ≤ b₂ - a₂
Theorem: Matroid.unif_isoMinor_unif_iff'
Proof state before:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ b₂ : ℕ
h₂ : a₂ ≤ b₂
d₁ : ℕ
h₁ : a₁ ≤ a₁ + d₁
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ b₂) ↔ a₁ ≤ a₂ ∧ a₁ + d₁ - a₁ ≤ b₂ - a₂
Tactic:
obtain ⟨d₂, rfl⟩ := Nat.exists_eq_add_of_le h₂
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ : ℕ
h₁ : a₁ ≤ a₁ + d₁
d₂ : ℕ
h₂ : a₂ ≤ a₂ + d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂)) ↔ a₁ ≤ a₂ ∧ a₁ + d₁ - a₁ ≤ a₂ + d₂ - a₂
Theorem: Matroid.unif_isoMinor_unif_iff'
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ : ℕ
h₁ : a₁ ≤ a₁ + d₁
d₂ : ℕ
h₂ : a₂ ≤ a₂ + d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂)) ↔ a₁ ≤ a₂ ∧ a₁ + d₁ - a₁ ≤ a₂ + d₂ - a₂
Tactic:
rw [add_tsub_cancel_left, add_tsub_cancel_left, unif_isoMinor_unif_iff]
Proof state after:
no goals
Theorem: Matroid.ModularCut.inter
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ F ∩ F' ∈ C
Tactic:
rw [← sInter_pair]
Proof state after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ ⋂₀ {F, F'} ∈ C
Theorem: Matroid.ModularCut.inter
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ ⋂₀ {F, F'} ∈ C
Tactic:
apply C.sInter (pair_subset hF hF') _ (by simp)
Proof state after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ M.ModularFamily fun X => ↑X
Theorem: Matroid.ModularCut.inter
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ M.ModularFamily fun X => ↑X
Tactic:
let ⟨B, hB⟩ := hFF'
Proof state after:
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
⊢ M.ModularFamily fun X => ↑X
Theorem: Matroid.ModularCut.inter
Proof state before:
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
⊢ M.ModularFamily fun X => ↑X
Tactic:
refine' ⟨B, hB.1, fun i ↦ _⟩
Proof state after:
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
⊢ M.Basis ((fun X => ↑X) i ∩ B) ((fun X => ↑X) i)
Theorem: Matroid.ModularCut.inter
Proof state before:
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
⊢ M.Basis ((fun X => ↑X) i ∩ B) ((fun X => ↑X) i)
Tactic:
dsimp
Proof state after:
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
⊢ M.Basis (↑i ∩ B) ↑i
Theorem: Matroid.ModularCut.inter
Proof state before:
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
⊢ M.Basis (↑i ∩ B) ↑i
Tactic:
obtain (eq | ne) := mem_insert_iff.2 (Subtype.mem i)
Proof state after:
case inl
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
eq : ↑i = F
⊢ M.Basis (↑i ∩ B) ↑i

case inr
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
ne : ↑i ∈ {F'}
⊢ M.Basis (↑i ∩ B) ↑i
Theorem: Matroid.ModularCut.inter
Proof state before:
case inr
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
ne : ↑i ∈ {F'}
⊢ M.Basis (↑i ∩ B) ↑i
Tactic:
rw [mem_singleton_iff.1 ne]
Proof state after:
case inr
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
ne : ↑i ∈ {F'}
⊢ M.Basis (F' ∩ B) F'
Theorem: Matroid.ModularCut.inter
Proof state before:
case inr
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
ne : ↑i ∈ {F'}
⊢ M.Basis (F' ∩ B) F'
Tactic:
exact hB.2 false
Proof state after:
no goals
Theorem: Matroid.ModularCut.inter
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ {F, F'}.Nonempty
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.ModularCut.inter
Proof state before:
case inl
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
eq : ↑i = F
⊢ M.Basis (↑i ∩ B) ↑i
Tactic:
rw [eq]
Proof state after:
case inl
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
eq : ↑i = F
⊢ M.Basis (F ∩ B) F
Theorem: Matroid.ModularCut.inter
Proof state before:
case inl
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
eq : ↑i = F
⊢ M.Basis (F ∩ B) F
Tactic:
exact hB.2 true
Proof state after:
no goals
Theorem: Matroid.ModularCut.insert_cl
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.cl X ∈ C
Tactic:
rw [← (@inter_insert_eq _ X _ _ hne), Indep.cl_inter_eq_inter_cl]
Proof state after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.cl (insert a X) ∩ M.cl (insert b X) ∈ C

α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Indep (insert a X ∪ insert b X)
Theorem: Matroid.ModularCut.insert_cl
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Indep (insert a X ∪ insert b X)
Tactic:
rwa [union_insert_eq, insert_comm]
Proof state after:
no goals
Theorem: Matroid.ModularCut.insert_cl
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.cl (insert a X) ∩ M.cl (insert b X) ∈ C
Tactic:
apply C.inter ha hb (modularPair_iff.2 ⟨(insert a (insert b X)), hI, _⟩)
Proof state after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Basis (M.cl (insert a X) ∩ insert a (insert b X)) (M.cl (insert a X)) ∧
    M.Basis (M.cl (insert b X) ∩ insert a (insert b X)) (M.cl (insert b X))
Theorem: Matroid.ModularCut.insert_cl
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Basis (M.cl (insert a X) ∩ insert a (insert b X)) (M.cl (insert a X)) ∧
    M.Basis (M.cl (insert b X) ∩ insert a (insert b X)) (M.cl (insert b X))
Tactic:
rw [hI.cl_inter_eq_self_of_subset (subset_insert _ _), hI.cl_inter_eq_self_of_subset]
Proof state after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Basis (insert a X) (M.cl (insert a X)) ∧ M.Basis (insert b X) (M.cl (insert b X))

α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert a (insert b X)
Theorem: Matroid.ModularCut.insert_cl
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert a (insert b X)
Tactic:
rw [insert_comm]
Proof state after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert b (insert a X)
Theorem: Matroid.ModularCut.insert_cl
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert b (insert a X)
Tactic:
exact subset_insert _ _
Proof state after:
no goals
Theorem: Matroid.ModularCut.insert_cl
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Basis (insert a X) (M.cl (insert a X)) ∧ M.Basis (insert b X) (M.cl (insert b X))
Tactic:
refine' ⟨Indep.basis_cl (hI.subset _), Indep.basis_cl (hI.subset (subset_insert _ _))⟩
Proof state after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert a (insert b X)