awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X I : Set α
h : M.IsRkFinite X
hI : M.IsBasis' I X
⊢ I.Finite

Tactic:
have := h.rankFinite
  (isBase_restrict_iff'.2 hI).finite

Premises used: Iff.mpr, Matroid.isBase_restrict_iff', Matroid.IsRkFinite.rankFinite, Matroid.IsBase.finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X I : Set α
h : M.IsRkFinite X
hI : M.IsBasis I X
⊢ I.Finite

Tactic:
h.finite_of_isBasis' hI.isBasis'

Premises used: Matroid.IsBasis.isBasis', Matroid.IsRkFinite.finite_of_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite X
⊢ ∃ (I : Set α), M.IsBasis' I X ∧ I.Finite

Tactic:
h.exists_finite_isBase

Premises used: Matroid.IsBasis', Matroid.RankFinite.exists_finite_isBase, Maximal
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite X
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
⊢ M.IsBasis' (↑(hIfin.toFinset (s := I)) : Set α) X

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.IsRkFinite X ↔ ∃ (I : Set α), M.IsBasis' I X ∧ I.Finite

Tactic:
⟨IsRkFinite.exists_finite_isBasis', fun ⟨_, hIX, hI⟩ ↦ hIX.isRkFinite_of_finite hI⟩

Premises used: _private.0.Matroid.isRkFinite_iff_exists_isBasis'.match_1, Matroid.IsRkFinite.exists_finite_isBasis', Matroid.IsBasis'.isRkFinite_of_finite, Iff.intro, Matroid.IsRkFinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
obtain : ∀ (I : Set α) (hI : M.IsBasis' I Y), M.IsRkFinite Y
⊢ M.IsRkFinite Y

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' Y

Premises used: Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
I : Set α
hI : M.IsBasis' I Y
obtain : ∀ (J : Set α) (hJ : M.IsBasis' J X) (hIJ : I ⊆ J), M.IsRkFinite Y
⊢ M.IsRkFinite Y

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis'_of_subset (hI.subset.trans hXY)

Premises used: HasSubset.Subset.trans, Matroid.IsBasis'.indep, Matroid.Indep.subset_isBasis'_of_subset, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
I : Set α
hI : M.IsBasis' I Y
J : Set α
hJ : M.IsBasis' J X
hIJ : I ⊆ J
⊢ M.IsRkFinite Y

Tactic:
hI.isRkFinite_of_finite <| (hJ.finite_of_isRkFinite h).subset hIJ

Premises used: Matroid.IsBasis'.finite_of_isRkFinite, Set.Finite.subset, Matroid.IsBasis'.isRkFinite_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
I : Set α
hI : M.IsBasis' I Y
J : Set α
hJ : M.IsBasis' J X
hIJ : I ⊆ J
⊢ M.IsRkFinite Y

Tactic:
exact hI.isRkFinite_of_finite <| (hJ.finite_of_isRkFinite h).subset hIJ

Premises used: Matroid.IsBasis'.finite_of_isRkFinite, Set.Finite.subset, Matroid.IsBasis'.isRkFinite_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.IsRkFinite (X ∩ M.E) ↔ M.IsRkFinite X

Tactic:
let ⟨_I, hI⟩ := M.exists_isBasis' X
  ⟨fun h ↦ hI.isRkFinite_of_finite (hI.isBasis_inter_ground.finite_of_isRkFinite h),
    fun h ↦ h.subset inter_subset_left⟩

Premises used: Matroid.IsBasis.finite_of_isRkFinite, Matroid.E, Matroid.IsRkFinite.subset, Set.inter_subset_left, Matroid.IsBasis'.isBasis_inter_ground, Inter.inter, Iff, Matroid.IsBasis'.isRkFinite_of_finite, Iff.intro, Matroid.exists_isBasis', _private.0.Matroid.isRkFinite_inter_ground_iff.match_1, Matroid.IsRkFinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite X
⊢ M.IsRkFinite (X ∩ M.E)

Tactic:
isRkFinite_inter_ground_iff.2 h

Premises used: Iff.mpr, Matroid.isRkFinite_inter_ground_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
simp_rw : (∃ (I : Set α), M.IsBasis' I X ∧ I.Finite) ↔ ∃ (I : Set α), M.IsBasis I X ∧ I.Finite
⊢ M.IsRkFinite X ↔ ∃ (I : Set α), M.IsBasis I X ∧ I.Finite

Tactic:
simp_rw [isRkFinite_iff_exists_isBasis', M.isBasis'_iff_isBasis hX]

Premises used: Matroid.isRkFinite_iff_exists_isBasis', Matroid.isBasis'_iff_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsRkFinite I ↔ I.Finite

Tactic:
hI.isBasis_self.finite_iff_isRkFinite.symm

Premises used: Matroid.IsBasis.finite_iff_isRkFinite, Iff.symm, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
X : Set α
M : Matroid α
hX : X.Finite
⊢ M.IsRkFinite X

Tactic:
let ⟨_, hI⟩ := M.exists_isBasis' X
  hI.isRkFinite_of_finite (hX.subset hI.subset)

Premises used: Set.Finite.subset, Matroid.IsBasis'.isRkFinite_of_finite, Matroid.IsBasis'.subset, Matroid.exists_isBasis', Matroid.IsRkFinite, _private.0.Matroid.isRkFinite_of_finite.match_1
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.Indep I
hIX : I ⊆ X
hX : M.IsRkFinite X
⊢ ∃ (J : Set α), M.IsBasis' J X ∧ I ⊆ J ∧ J.Finite

Tactic:
(hI.subset_isBasis'_of_subset hIX).imp fun _ hJ => ⟨hJ.1, hJ.2, hJ.1.finite_of_isRkFinite hX⟩

Premises used: Exists.imp, Matroid.Indep.subset_isBasis'_of_subset, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.Indep I
hIX : I ⊆ X
hX : M.IsRkFinite X
hXE : X ⊆ M.E
⊢ ∃ (J : Set α), M.IsBasis J X ∧ I ⊆ J ∧ J.Finite

Tactic:
(hI.subset_isBasis_of_subset hIX).imp fun _ hJ => ⟨hJ.1, hJ.2, hJ.1.finite_of_isRkFinite hX⟩

Premises used: Exists.imp, And.intro, Matroid.Indep.subset_isBasis_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsRkFinite {e}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
⊢ M.IsRkFinite ∅

Tactic:
isRkFinite_of_finite M finite_empty

Premises used: Set.finite_empty, Matroid.isRkFinite_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hX : M.IsRkFinite X
hI : M.Indep I
hIX : I ⊆ X
⊢ I.Finite

Tactic:
hI.finite_of_isRkFinite <| hX.subset hIX

Premises used: Matroid.IsRkFinite.subset, Matroid.Indep.finite_of_isRkFinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
rw : (M ↾ M.E).RankFinite ↔ M.RankFinite
rw₁ rw₂ : M.RankFinite ↔ M.RankFinite
⊢ M.IsRkFinite M.E ↔ M.RankFinite

Tactic:
rw [IsRkFinite, restrict_ground_eq_self]

Premises used: Matroid.restrict_ground_eq_self, Matroid.IsRkFinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
inst rwa rwa₁ rwa₂ rwa₃ : M.RankFinite
⊢ M.IsRkFinite M.E

Tactic:
rwa [isRkFinite_ground_iff_rankFinite]

Premises used: Matroid.isRkFinite_ground_iff_rankFinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.Indep I
hIX : I ⊆ X
hX : M.IsRkFinite X
⊢ I.Finite

Tactic:
hX.finite_of_indep_subset hI hIX

Premises used: Matroid.IsRkFinite.finite_of_indep_subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite X
⊢ M.IsRkFinite (M.closure X)

Tactic:
let ⟨_, hI⟩ := M.exists_isBasis' X
  hI.isBasis_closure_right.isRkFinite_of_finite <| hI.finite_of_isRkFinite h

Premises used: Matroid.IsBasis'.finite_of_isRkFinite, Matroid.IsBasis.isRkFinite_of_finite, Matroid.closure, Matroid.exists_isBasis', _private.0.Matroid.isRkFinite_inter_ground_iff.match_1, Matroid.IsRkFinite, Matroid.IsBasis'.isBasis_closure_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.IsRkFinite (M.closure X) ↔ M.IsRkFinite (X ∩ M.E)
⊢ M.IsRkFinite (M.closure X) ↔ M.IsRkFinite X

Tactic:
rw [← isRkFinite_inter_ground_iff (X := X)]

Premises used: Matroid.isRkFinite_inter_ground_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite (X ∩ M.E)
⊢ M.IsRkFinite (M.closure X)

Tactic:
simpa using h.closure

Premises used: Matroid.IsRkFinite.closure
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.IsRkFinite (M.closure X) ↔ M.IsRkFinite (X ∩ M.E)

Tactic:
exact ⟨fun h ↦ h.subset <| M.inter_ground_subset_closure X, fun h ↦ by simpa using h.closure⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
obtain : ∀ (I : Set α) (hI : M.IsBasis' I X) (hIfin : I.Finite), M.IsRkFinite (X ∪ Y)
⊢ M.IsRkFinite (X ∪ Y)

Tactic:
obtain ⟨I, hI, hIfin⟩ := hX.exists_finite_isBasis'

Premises used: Matroid.IsRkFinite.exists_finite_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
obtain : ∀ (J : Set α) (hJ : M.IsBasis' J Y) (hJfin : J.Finite), M.IsRkFinite (X ∪ Y)
⊢ M.IsRkFinite (X ∪ Y)

Tactic:
obtain ⟨J, hJ, hJfin⟩ := hY.exists_finite_isBasis'

Premises used: Matroid.IsRkFinite.exists_finite_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
rw : M.IsRkFinite ((X ∪ Y) ∩ M.E)
⊢ M.IsRkFinite (X ∪ Y)

Tactic:
rw [← isRkFinite_inter_ground_iff]

Premises used: Matroid.isRkFinite_inter_ground_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ M.IsRkFinite ((X ∪ Y) ∩ M.E)

Tactic:
(M.isRkFinite_of_finite (hIfin.union hJfin)).closure.subset ?_

Premises used: Set.Finite.union, Matroid.IsRkFinite.subset, Matroid.IsRkFinite.closure, Matroid.isRkFinite_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
refine : (X ∪ Y) ∩ M.E ⊆ M.closure (I ∪ J)
⊢ M.IsRkFinite ((X ∪ Y) ∩ M.E)

Tactic:
refine (M.isRkFinite_of_finite (hIfin.union hJfin)).closure.subset ?_

Premises used: Set.Finite.union, Matroid.IsRkFinite.subset, Matroid.IsRkFinite.closure, Matroid.isRkFinite_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
rw : (X ∪ Y) ∩ M.E ⊆ M.closure (X ∪ Y)
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (I ∪ J)

Tactic:
rw [closure_union_congr_left hI.closure_eq_closure,
    closure_union_congr_right hJ.closure_eq_closure]

Premises used: Matroid.closure_union_congr_right, Matroid.IsBasis'.closure_eq_closure, Matroid.closure_union_congr_left
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (X ∪ Y)

Tactic:
inter_ground_subset_closure M (X ∪ Y)

Premises used: Matroid.inter_ground_subset_closure, Union.union
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (X ∪ Y)

Tactic:
exact inter_ground_subset_closure M (X ∪ Y)

Premises used: Matroid.inter_ground_subset_closure, Union.union
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
⊢ M.IsRkFinite (X ∪ Y) ↔ M.IsRkFinite Y

Tactic:
⟨fun h ↦ h.subset subset_union_right, fun h ↦ hX.union h⟩

Premises used: Set.subset_union_right, Matroid.IsRkFinite.subset, Matroid.IsRkFinite.union, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
rw : M.IsRkFinite (X ∪ Y \ X) ↔ M.IsRkFinite Y
rw₁ : M.IsRkFinite (X ∪ Y) ↔ M.IsRkFinite Y
rw₂ rw₃ : M.IsRkFinite Y ↔ M.IsRkFinite Y
⊢ M.IsRkFinite (Y \ X) ↔ M.IsRkFinite Y

Tactic:
rw [← hX.isRkFinite_union_iff, union_diff_self, hX.isRkFinite_union_iff]

Premises used: Matroid.IsRkFinite.isRkFinite_union_iff, Set.union_diff_self
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
⊢ M.IsRkFinite (X ∩ Y)

Tactic:
hX.subset inter_subset_left

Premises used: Matroid.IsRkFinite.subset, Set.inter_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
⊢ M.IsRkFinite (Y ∩ X)

Tactic:
hX.subset inter_subset_right

Premises used: Matroid.IsRkFinite.subset, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
⊢ M.IsRkFinite (X \ Y)

Tactic:
hX.subset diff_subset

Premises used: Set.diff_subset, Matroid.IsRkFinite.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.IsRkFinite X
e : α
rw : M.IsRkFinite (X ∪ {e})
⊢ M.IsRkFinite (Insert.insert e X)

Tactic:
rw [← union_singleton]

Premises used: Set.union_singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.IsRkFinite X
e : α
⊢ M.IsRkFinite (X ∪ {e})

Tactic:
hX.union M.isRkFinite_singleton

Premises used: Matroid.IsRkFinite.union, Matroid.isRkFinite_singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.IsRkFinite X
e : α
⊢ M.IsRkFinite (X ∪ {e})

Tactic:
exact hX.union M.isRkFinite_singleton

Premises used: Matroid.IsRkFinite.union, Matroid.isRkFinite_singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
rw : M.IsRkFinite ({e} ∪ X) ↔ M.IsRkFinite X
rw₁ rw₂ : M.IsRkFinite X ↔ M.IsRkFinite X
⊢ M.IsRkFinite (insert e X) ↔ M.IsRkFinite X

Tactic:
rw [← singleton_union, isRkFinite_singleton.isRkFinite_union_iff]

Premises used: Matroid.IsRkFinite.isRkFinite_union_iff, Set.singleton_union, Matroid.isRkFinite_singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
rw rw₁ : M.IsRkFinite X ↔ M.IsRkFinite X
⊢ M.IsRkFinite (X \ {e}) ↔ M.IsRkFinite X

Tactic:
rw [isRkFinite_singleton.isRkFinite_diff_iff]

Premises used: Matroid.IsRkFinite.isRkFinite_diff_iff, Matroid.isRkFinite_singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
inst : M.RankFinite
X : Set α
⊢ M.IsRkFinite X

Tactic:
let ⟨_, hI⟩ := M.exists_isBasis' X
  hI.isRkFinite_of_finite hI.indep.finite

Premises used: Matroid.Indep.finite, Matroid.IsBasis'.indep, Matroid.IsBasis'.isRkFinite_of_finite, Matroid.exists_isBasis', _private.0.Matroid.isRkFinite_inter_ground_iff.match_1, Matroid.IsRkFinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
inst : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
choose : ∀ (Is : (i : ι) → Set α) (hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)), M.IsRkFinite (⋃ (i : ι), Xs i)
⊢ M.IsRkFinite (⋃ (i : ι), Xs i)

Tactic:
choose Is hIs using fun i ↦ M.exists_isBasis' (Xs i)

Premises used: Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
inst : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : (i : ι) → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
⊢ Set.Finite.{u_1} (α := α) (⋃ (i : ι), Is i)

Tactic:
have hfin : (⋃ i, Is i).Finite := finite_iUnion <| fun i ↦ (h i).finite_of_isBasis' (hIs i)
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
inst : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : (i : ι) → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : Set.Finite.{u_1} (α := α) (⋃ (i : ι), Is i)
⊢ M.IsRkFinite (⋃ (i : ι), Xs i)

Tactic:
isRkFinite_inter_ground_iff.1 <| (M.isRkFinite_of_finite hfin).closure.subset ?_

Premises used: Matroid.IsRkFinite.subset, Matroid.IsRkFinite.closure, Iff.mp, Matroid.isRkFinite_of_finite, Matroid.isRkFinite_inter_ground_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
inst : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : (i : ι) → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : Set.Finite.{u_1} (α := α) (⋃ (i : ι), Is i)
refine : (⋃ (i : ι), Xs i) ∩ M.E ⊆ M.closure (⋃ (i : ι), Is i)
⊢ M.IsRkFinite (⋃ (i : ι), Xs i)

Tactic:
refine isRkFinite_inter_ground_iff.1 <| (M.isRkFinite_of_finite hfin).closure.subset ?_

Premises used: Matroid.IsRkFinite.subset, Matroid.IsRkFinite.closure, Iff.mp, Matroid.isRkFinite_of_finite, Matroid.isRkFinite_inter_ground_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
inst : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : (i : ι) → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : Set.Finite.{u_1} (α := α) (⋃ (i : ι), Is i)
rw : ∀ (i : ι), Xs i ∩ M.E ⊆ M.closure (⋃ (i : ι), Is i)
⊢ (⋃ (i : ι), Xs i) ∩ M.E ⊆ M.closure (⋃ (i : ι), Is i)

Tactic:
rw [iUnion_inter, iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff, Set.iUnion_inter
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
inst : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : (i : ι) → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : Set.Finite.{u_1} (α := α) (⋃ (i : ι), Is i)
⊢ ∀ (i : ι), Xs i ∩ M.E ⊆ M.closure (⋃ (i : ι), Is i)

Tactic:
fun i ↦ (hIs i).isBasis_inter_ground.subset_closure.trans <| M.closure_subset_closure <|
    subset_iUnion ..

Premises used: HasSubset.Subset.trans, Matroid.closure_subset_closure, Matroid.IsBasis'.isBasis_inter_ground, Set.subset_iUnion, Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
inst : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : (i : ι) → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : Set.Finite.{u_1} (α := α) (⋃ (i : ι), Is i)
⊢ ∀ (i : ι), Xs i ∩ M.E ⊆ M.closure (⋃ (i : ι), Is i)

Tactic:
exact fun i ↦ (hIs i).isBasis_inter_ground.subset_closure.trans <| M.closure_subset_closure <|
    subset_iUnion ..

Premises used: HasSubset.Subset.trans, Matroid.closure_subset_closure, Matroid.IsBasis'.isBasis_inter_ground, Set.subset_iUnion, Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
⊢ (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) ↔
    ∃ (B : Set ((i : ι) × α i)), (∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) ∧ I ⊆ B

Tactic:
⟨fun h ↦ ?_, fun ⟨B, hB, hIB⟩ i ↦ (hB i).indep.subset (preimage_mono hIB)⟩

Premises used: Matroid.Indep, Matroid.Indep.subset, Set.preimage_mono, Set.preimage, Iff.intro, Sigma.mk, Matroid.IsBase.indep, _private.0.Matroid.sigma.match_1
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
refine :
  ∀ (h : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)),
    ∃ (B : Set ((i : ι) × α i)), (∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) ∧ I ⊆ B
⊢ (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) ↔
    ∃ (B : Set ((i : ι) × α i)), (∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) ∧ I ⊆ B

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨B, hB, hIB⟩ i ↦ (hB i).indep.subset (preimage_mono hIB)⟩
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
choose :
  ∀ (Bs : (i : ι) → Set (α i)) (hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Bs i),
    ∃ (B : Set ((i : ι) × α i)), (∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) ∧ I ⊆ B
⊢ ∃ (B : Set ((i : ι) × α i)), (∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) ∧ I ⊆ B

Tactic:
choose Bs hBs using fun i ↦ (h i).exists_isBase_superset

Premises used: Matroid.Indep.exists_isBase_superset
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Bs i
i : ι
⊢ (M i).IsBase (Sigma.mk (β := α) i ⁻¹' Set.sigma (α := α) univ Bs)

Tactic:
simpa using (hBs i).1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Bs i
refine : I ⊆ Set.sigma (α := α) univ Bs
⊢ ∃ (B : Set ((i : ι) × α i)), (∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) ∧ I ⊆ B

Tactic:
refine ⟨univ.sigma Bs, fun i ↦ by simpa using (hBs i).1, ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Bs i
rw :
  (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' I) ⊆
    Set.sigma (α := α) univ Bs
⊢ I ⊆ Set.sigma (α := α) univ Bs

Tactic:
rw [← univ_sigma_preimage_mk I]

Premises used: Set.univ_sigma_preimage_mk
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Bs i
⊢ (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' I) ⊆
    Set.sigma (α := α) univ Bs

Tactic:
sigma_mono rfl.subset fun i ↦ (hBs i).2

Premises used: Eq.subset, And.right, Set.sigma_mono, rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Bs i
⊢ (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' I) ⊆
    Set.sigma (α := α) univ Bs

Tactic:
refine sigma_mono rfl.subset fun i ↦ (hBs i).2

Premises used: Eq.subset, And.right, Set.sigma_mono, rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
choose :
  ∀ (B : (i : ι) → Set (α i)) (hB : ∀ (i : ι), (M i).IsBase (B i)),
    ∃ (B : Set ((i : ι) × α i)), ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)
⊢ ∃ (B : Set ((i : ι) × α i)), ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)

Tactic:
choose B hB using fun i ↦ (M i).exists_isBase

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B : (i : ι) → Set (α i)
hB : ∀ (i : ι), (M i).IsBase (B i)
⊢ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' Set.sigma (α := α) univ B)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B : (i : ι) → Set (α i)
hB : ∀ (i : ι), (M i).IsBase (B i)
⊢ ∃ (B : Set ((i : ι) × α i)), ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)

Tactic:
exact ⟨univ.sigma B, by simpa⟩