internlm/Lean-Github huggingface dataset:
Theorem: LinearMap.domRestrict_injective
Proof state before:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ ↑x = ↑y
Tactic:
apply_fun f using hf
Proof state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ f ↑x = f ↑y
Theorem: LinearMap.domRestrict_injective
Proof state before:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ f ↑x = f ↑y
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LinearMap.finrank_map_of_inj
Proof state before:
K : Type u_1
V : Type u_2
V₂ : Type u_3
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
hf : Function.Injective ⇑f
U : Submodule K V
⊢ FiniteDimensional.finrank K ↥(Submodule.map f U) = FiniteDimensional.finrank K ↥U
Tactic:
rw [← LinearMap.finrank_range_of_inj (LinearMap.domRestrict_injective hf _),
  LinearMap.range_domRestrict]
Proof state after:
no goals
Theorem: Set.mem_subtypeOrderEmbedding_iff
Proof state before:
α : Type u_1
β : Type u_2
s✝ t r✝ s : Set α
x : α
r : Set ↑s
⊢ x ∈ s.subtypeOrderEmbedding r ↔ ∃ (hx : x ∈ s), ⟨x, hx⟩ ∈ r
Tactic:
simp [Set.subtypeOrderEmbedding]
Proof state after:
no goals
Theorem: Set.mem_subtypeOrderIso_iff
Proof state before:
α : Type u_1
β : Type u_2
s✝ t r✝ s : Set α
x : α
r : Set ↑s
⊢ x ∈ ↑(s.subtypeOrderIso r) ↔ ∃ (hx : x ∈ s), ⟨x, hx⟩ ∈ r
Tactic:
simp [Set.subtypeOrderIso]
Proof state after:
no goals
Theorem: Matroid.modularBase_pair_iff
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
B X Y : Set α
⊢ (M.ModularBase B fun i => ↑i) ↔ M.Base B ∧ M.Basis (X ∩ B) X ∧ M.Basis (Y ∩ B) Y
Tactic:
simp [ModularBase]
Proof state after:
no goals
Theorem: Matroid.ModularBase.basis_iUnion
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularBase B Xs
⊢ M.Basis ((⋃ i, Xs i) ∩ B) (⋃ i, Xs i)
Tactic:
simp_rw [h.1.indep.inter_basis_cl_iff_subset_cl_inter, iUnion_subset_iff]
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularBase B Xs
⊢ ∀ (i : ι), Xs i ⊆ M.cl ((⋃ i, Xs i) ∩ B)
Theorem: Matroid.ModularBase.basis_iUnion
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularBase B Xs
⊢ ∀ (i : ι), Xs i ⊆ M.cl ((⋃ i, Xs i) ∩ B)
Tactic:
exact fun i ↦ (h.subset_cl_inter i).trans
  (M.cl_subset_cl (inter_subset_inter_left _ (subset_iUnion _ i)))
Proof state after:
no goals
Theorem: Matroid.ModularBase.basis_biUnion
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularBase B Xs
A : Set ι
⊢ M.Basis ((⋃ i ∈ A, Xs i) ∩ B) (⋃ i ∈ A, Xs i)
Tactic:
convert (h.subtype A).basis_iUnion <;> simp
Proof state after:
no goals
Theorem: Matroid.exists_modularBase_of_iUnion_indep
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.Indep (⋃ i, Xs i)
⊢ ∃ B, M.ModularBase B Xs
Tactic:
obtain ⟨B, hB, hIB⟩ := h.exists_base_superset
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.Indep (⋃ i, Xs i)
B : Set α
hB : M.Base B
hIB : ⋃ i, Xs i ⊆ B
⊢ ∃ B, M.ModularBase B Xs
Theorem: Matroid.exists_modularBase_of_iUnion_indep
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.Indep (⋃ i, Xs i)
B : Set α
hB : M.Base B
hIB : ⋃ i, Xs i ⊆ B
⊢ ∃ B, M.ModularBase B Xs
Tactic:
refine ⟨B, hB, fun i ↦ ?_⟩
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
h : M.Indep (⋃ i, Xs i)
B : Set α
hB : M.Base B
hIB : ⋃ i, Xs i ⊆ B
i : ι
⊢ M.Basis (Xs i ∩ B) (Xs i)
Theorem: Matroid.exists_modularBase_of_iUnion_indep
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
h : M.Indep (⋃ i, Xs i)
B : Set α
hB : M.Base B
hIB : ⋃ i, Xs i ⊆ B
i : ι
⊢ M.Basis (Xs i ∩ B) (Xs i)
Tactic:
rw [inter_eq_self_of_subset_left <| iUnion_subset_iff.1 hIB i]
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
h : M.Indep (⋃ i, Xs i)
B : Set α
hB : M.Base B
hIB : ⋃ i, Xs i ⊆ B
i : ι
⊢ M.Basis (Xs i) (Xs i)
Theorem: Matroid.exists_modularBase_of_iUnion_indep
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
h : M.Indep (⋃ i, Xs i)
B : Set α
hB : M.Base B
hIB : ⋃ i, Xs i ⊆ B
i : ι
⊢ M.Basis (Xs i) (Xs i)
Tactic:
exact (h.subset (subset_iUnion _ i)).basis_self
Proof state after:
no goals
Theorem: Matroid.Base.modularBase_of_forall_subset_cl
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hB : M.Base B
h : ∀ (i : ι), Xs i ⊆ M.cl (Xs i ∩ B)
⊢ M.ModularBase B Xs
Tactic:
exact ⟨hB, fun i ↦ hB.indep.inter_basis_cl_iff_subset_cl_inter.2 (h i)⟩
Proof state after:
no goals
Theorem: Matroid.ModularBase.modularBase_of_forall_subset_subset_cl
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hB : M.ModularBase B Xs
hXY : ∀ (i : ι), Xs i ⊆ Ys i
hYX : ∀ (i : ι), Ys i ⊆ M.cl (Xs i)
⊢ M.ModularBase B Ys
Tactic:
refine ⟨hB.base, fun i ↦ hB.indep.inter_basis_cl_iff_subset_cl_inter.2 ?_⟩
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
hB : M.ModularBase B Xs
hXY : ∀ (i : ι), Xs i ⊆ Ys i
hYX : ∀ (i : ι), Ys i ⊆ M.cl (Xs i)
i : ι
⊢ Ys i ⊆ M.cl (Ys i ∩ B)
Theorem: Matroid.ModularBase.modularBase_of_forall_subset_subset_cl
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
hB : M.ModularBase B Xs
hXY : ∀ (i : ι), Xs i ⊆ Ys i
hYX : ∀ (i : ι), Ys i ⊆ M.cl (Xs i)
i : ι
⊢ Ys i ⊆ M.cl (Ys i ∩ B)
Tactic:
refine (hYX i).trans (M.cl_subset_cl_of_subset_cl ?_)
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
hB : M.ModularBase B Xs
hXY : ∀ (i : ι), Xs i ⊆ Ys i
hYX : ∀ (i : ι), Ys i ⊆ M.cl (Xs i)
i : ι
⊢ Xs i ⊆ M.cl (Ys i ∩ B)
Theorem: Matroid.ModularBase.modularBase_of_forall_subset_subset_cl
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
hB : M.ModularBase B Xs
hXY : ∀ (i : ι), Xs i ⊆ Ys i
hYX : ∀ (i : ι), Ys i ⊆ M.cl (Xs i)
i : ι
⊢ Xs i ⊆ M.cl (Ys i ∩ B)
Tactic:
exact (hB.2 i).subset_cl.trans (M.cl_subset_cl (inter_subset_inter_left B (hXY i)))
Proof state after:
no goals
Theorem: Matroid.ModularBase.iInter_cl_eq_cl_iInter
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Nonempty ι
hB : M.ModularBase B Xs
⊢ ⋂ i, M.cl (Xs i) = M.cl (⋂ i, Xs i)
Tactic:
simp_rw [subset_antisymm_iff, subset_iInter_iff, ← hB.cl_inter_eq]
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Nonempty ι
hB : M.ModularBase B Xs
⊢ ⋂ i, M.cl (Xs i ∩ B) ⊆ M.cl (⋂ i, Xs i) ∧ ∀ (i : ι), M.cl (⋂ i, Xs i) ⊆ M.cl (Xs i ∩ B)
Theorem: Matroid.ModularBase.iInter_cl_eq_cl_iInter
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Nonempty ι
hB : M.ModularBase B Xs
⊢ ⋂ i, M.cl (Xs i ∩ B) ⊆ M.cl (⋂ i, Xs i) ∧ ∀ (i : ι), M.cl (⋂ i, Xs i) ⊆ M.cl (Xs i ∩ B)
Tactic:
rw [← cl_iInter_eq_iInter_cl_of_iUnion_indep, ← iInter_inter B Xs]
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Nonempty ι
hB : M.ModularBase B Xs
⊢ M.cl ((⋂ i, Xs i) ∩ B) ⊆ M.cl (⋂ i, Xs i) ∧ ∀ (i : ι), M.cl (⋂ i, Xs i) ⊆ M.cl (Xs i ∩ B)

case h
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Nonempty ι
hB : M.ModularBase B Xs
⊢ M.Indep (⋃ i, Xs i ∩ B)
Theorem: Matroid.ModularBase.iInter_cl_eq_cl_iInter
Proof state before:
case h
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Nonempty ι
hB : M.ModularBase B Xs
⊢ M.Indep (⋃ i, Xs i ∩ B)
Tactic:
exact hB.base.indep.subset (iUnion_subset (fun _ ↦ inter_subset_right))
Proof state after:
no goals
Theorem: Matroid.ModularBase.iInter_cl_eq_cl_iInter
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Nonempty ι
hB : M.ModularBase B Xs
⊢ M.cl ((⋂ i, Xs i) ∩ B) ⊆ M.cl (⋂ i, Xs i) ∧ ∀ (i : ι), M.cl (⋂ i, Xs i) ⊆ M.cl (Xs i ∩ B)
Tactic:
refine ⟨M.cl_subset_cl inter_subset_left, fun i ↦ ?_⟩
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Nonempty ι
hB : M.ModularBase B Xs
i : ι
⊢ M.cl (⋂ i, Xs i) ⊆ M.cl (Xs i ∩ B)
Theorem: Matroid.ModularBase.iInter_cl_eq_cl_iInter
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Nonempty ι
hB : M.ModularBase B Xs
i : ι
⊢ M.cl (⋂ i, Xs i) ⊆ M.cl (Xs i ∩ B)
Tactic:
rw [hB.cl_inter_eq]
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Nonempty ι
hB : M.ModularBase B Xs
i : ι
⊢ M.cl (⋂ i, Xs i) ⊆ M.cl (Xs i)
Theorem: Matroid.ModularBase.iInter_cl_eq_cl_iInter
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Nonempty ι
hB : M.ModularBase B Xs
i : ι
⊢ M.cl (⋂ i, Xs i) ⊆ M.cl (Xs i)
Tactic:
exact M.cl_subset_cl (iInter_subset _ i)
Proof state after:
no goals
Theorem: Matroid.Indep.modularFamily
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hI : M.Indep I
hXs : ∀ (i : ι), M.Basis (Xs i ∩ I) (Xs i)
⊢ M.ModularFamily Xs
Tactic:
simp_rw [hI.inter_basis_cl_iff_subset_cl_inter] at hXs
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hI : M.Indep I
hXs : ∀ (i : ι), Xs i ⊆ M.cl (Xs i ∩ I)
⊢ M.ModularFamily Xs
Theorem: Matroid.Indep.modularFamily
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hI : M.Indep I
hXs : ∀ (i : ι), Xs i ⊆ M.cl (Xs i ∩ I)
⊢ M.ModularFamily Xs
Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_base_superset
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hI : M.Indep I
hXs : ∀ (i : ι), Xs i ⊆ M.cl (Xs i ∩ I)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ M.ModularFamily Xs
Theorem: Matroid.Indep.modularFamily
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hI : M.Indep I
hXs : ∀ (i : ι), Xs i ⊆ M.cl (Xs i ∩ I)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ M.ModularFamily Xs
Tactic:
refine ⟨B, hB, ?_⟩
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hI : M.Indep I
hXs : ∀ (i : ι), Xs i ⊆ M.cl (Xs i ∩ I)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
Theorem: Matroid.Indep.modularFamily
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hI : M.Indep I
hXs : ∀ (i : ι), Xs i ⊆ M.cl (Xs i ∩ I)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
Tactic:
simp_rw [hB.indep.inter_basis_cl_iff_subset_cl_inter]
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hI : M.Indep I
hXs : ∀ (i : ι), Xs i ⊆ M.cl (Xs i ∩ I)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ ∀ (i : ι), Xs i ⊆ M.cl (Xs i ∩ B)
Theorem: Matroid.Indep.modularFamily
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hI : M.Indep I
hXs : ∀ (i : ι), Xs i ⊆ M.cl (Xs i ∩ I)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ ∀ (i : ι), Xs i ⊆ M.cl (Xs i ∩ B)
Tactic:
exact fun i ↦ (hXs i).trans (M.cl_subset_cl (inter_subset_inter_right _ hIB))
Proof state after:
no goals
Theorem: Matroid.Indep.modularFamily_of_subsets
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
⊢ M.ModularFamily Js
Tactic:
refine hI.modularFamily (fun i ↦ ?_)
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
i : ι
⊢ M.Basis (Js i ∩ I) (Js i)
Theorem: Matroid.Indep.modularFamily_of_subsets
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
i : ι
⊢ M.Basis (Js i ∩ I) (Js i)
Tactic:
have hJI : Js i ⊆ I := (subset_iUnion _ i).trans hJs
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
i : ι
hJI : Js i ⊆ I
⊢ M.Basis (Js i ∩ I) (Js i)
Theorem: Matroid.Indep.modularFamily_of_subsets
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
i : ι
hJI : Js i ⊆ I
⊢ M.Basis (Js i ∩ I) (Js i)
Tactic:
rw [inter_eq_self_of_subset_left hJI]
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
i : ι
hJI : Js i ⊆ I
⊢ M.Basis (Js i) (Js i)
Theorem: Matroid.Indep.modularFamily_of_subsets
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
i : ι
hJI : Js i ⊆ I
⊢ M.Basis (Js i) (Js i)
Tactic:
exact (hI.subset hJI).basis_self
Proof state after:
no goals
Theorem: Matroid.modularFamily_of_isEmpty
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : IsEmpty ι
⊢ ⋃ i, Xs i ⊆ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.modularFamily_iff_of_subsingleton
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Subsingleton ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E
Tactic:
obtain (h | ⟨⟨i⟩⟩) := isEmpty_or_nonempty ι
Proof state after:
case inl
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Subsingleton ι
h : IsEmpty ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E

case inr.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E
Theorem: Matroid.modularFamily_iff_of_subsingleton
Proof state before:
case inl
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Subsingleton ι
h : IsEmpty ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E

case inr.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E
Tactic:
simp
Proof state after:
case inr.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E
Theorem: Matroid.modularFamily_iff_of_subsingleton
Proof state before:
case inr.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E
Tactic:
refine ⟨fun h ↦ h.subset_ground_of_mem, fun h ↦ ?_⟩
Proof state after:
case inr.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
⊢ M.ModularFamily Xs
Theorem: Matroid.modularFamily_iff_of_subsingleton
Proof state before:
case inr.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
⊢ M.ModularFamily Xs
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (Xs i)
Proof state after:
case inr.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
I : Set α
hI : M.Basis I (Xs i)
⊢ M.ModularFamily Xs
Theorem: Matroid.modularFamily_iff_of_subsingleton
Proof state before:
case inr.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
I : Set α
hI : M.Basis I (Xs i)
⊢ M.ModularFamily Xs
Tactic:
obtain ⟨B, hB, hIB⟩ := hI.indep.exists_base_superset
Proof state after:
case inr.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
I : Set α
hI : M.Basis I (Xs i)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ M.ModularFamily Xs
Theorem: Matroid.modularFamily_iff_of_subsingleton
Proof state before:
case inr.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
I : Set α
hI : M.Basis I (Xs i)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ M.ModularFamily Xs
Tactic:
refine ⟨B, hB, fun j ↦ ?_⟩
Proof state after:
case inr.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j✝ : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
I : Set α
hI : M.Basis I (Xs i)
B : Set α
hB : M.Base B
hIB : I ⊆ B
j : ι
⊢ M.Basis (Xs j ∩ B) (Xs j)
Theorem: Matroid.modularFamily_iff_of_subsingleton
Proof state before:
case inr.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j✝ : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
I : Set α
hI : M.Basis I (Xs i)
B : Set α
hB : M.Base B
hIB : I ⊆ B
j : ι
⊢ M.Basis (Xs j ∩ B) (Xs j)
Tactic:
rwa [Subsingleton.elim j i, inter_comm, hI.inter_eq_of_subset_indep hIB hB.indep]
Proof state after:
no goals
Theorem: Matroid.ModularFamily_of_loopEquiv
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularFamily Xs
he : ∀ (i : ι), M.LoopEquiv (Xs i) (Ys i)
⊢ M.ModularFamily Ys
Tactic:
obtain ⟨B, hB⟩ := h
Proof state after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : ∀ (i : ι), M.LoopEquiv (Xs i) (Ys i)
B : Set α
hB : M.ModularBase B Xs
⊢ M.ModularFamily Ys
Theorem: Matroid.ModularFamily_of_loopEquiv
Proof state before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : ∀ (i : ι), M.LoopEquiv (Xs i) (Ys i)
B : Set α
hB : M.ModularBase B Xs
⊢ M.ModularFamily Ys
Tactic:
refine ⟨B, hB.base, fun i ↦ ?_⟩
Proof state after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
he : ∀ (i : ι), M.LoopEquiv (Xs i) (Ys i)
B : Set α
hB : M.ModularBase B Xs
i : ι
⊢ M.Basis (Ys i ∩ B) (Ys i)
Theorem: Matroid.ModularFamily_of_loopEquiv
Proof state before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
he : ∀ (i : ι), M.LoopEquiv (Xs i) (Ys i)
B : Set α
hB : M.ModularBase B Xs
i : ι
⊢ M.Basis (Ys i ∩ B) (Ys i)
Tactic:
rw [← (he i).basis_iff, ← (he i).inter_eq_of_indep hB.indep]
Proof state after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
he : ∀ (i : ι), M.LoopEquiv (Xs i) (Ys i)
B : Set α
hB : M.ModularBase B Xs
i : ι
⊢ M.Basis (Xs i ∩ B) (Xs i)
Theorem: Matroid.ModularFamily_of_loopEquiv
Proof state before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
he : ∀ (i : ι), M.LoopEquiv (Xs i) (Ys i)
B : Set α
hB : M.ModularBase B Xs
i : ι
⊢ M.Basis (Xs i ∩ B) (Xs i)
Tactic:
exact hB.basis_inter i
Proof state after:
no goals
Theorem: Matroid.ModularFamily.ofRestrict'
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
R : Set α
h : (M ↾ R).ModularFamily Xs
⊢ M.ModularFamily fun i => Xs i ∩ M.E
Tactic:
obtain ⟨B, hBb, hB⟩ := h
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
⊢ M.ModularFamily fun i => Xs i ∩ M.E
Theorem: Matroid.ModularFamily.ofRestrict'
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
⊢ M.ModularFamily fun i => Xs i ∩ M.E
Tactic:
obtain ⟨B', hB'⟩ := hBb.indep.of_restrict.exists_base_superset
Proof state after:
case intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
⊢ M.ModularFamily fun i => Xs i ∩ M.E
Theorem: Matroid.ModularFamily.ofRestrict'
Proof state before:
case intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
⊢ M.ModularFamily fun i => Xs i ∩ M.E
Tactic:
refine' ⟨B', hB'.1, fun i ↦ _⟩
Proof state after:
case intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
R B : Set α
hBb : (M ↾ R).Base B
hB : ∀ (i : ι), (M ↾ R).Basis (Xs i ∩ B) (Xs i)
B' : Set α
hB' : M.Base B' ∧ B ⊆ B'
i : ι
⊢ M.Basis ((fun i => Xs i ∩ M.E) i ∩ B') ((fun i => Xs i ∩ M.E) i)