awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ (i : ι), I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ e ∈ M.E

Tactic:
exact (hI i).subset_ground hes

Premises used: Matroid.IsBasis.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.IsBasis (⋃ (i : ι), (fun (x : ι) ↦ I) i) (⋃ (i : ι), X i)

Tactic:
IsBasis.iUnion_isBasis_iUnion X (fun _ ↦ I) (fun i ↦ hI i) _

Premises used: Matroid.IsBasis.iUnion_isBasis_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
h : I = ⋃ (i : ι), I
convert! : M.Indep (⋃ (i : ι), (fun (x : ι) ↦ I) i)
⊢ M.IsBasis I (⋃ (i : ι), X i)

Tactic:
convert! IsBasis.iUnion_isBasis_iUnion X (fun _ ↦ I) (fun i ↦ hI i) _

Premises used: Matroid.IsBasis.iUnion_isBasis_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
h h₁ : I = I
⊢ I = ⋃ (i : ι), I

Tactic:
rw [iUnion_const]

Premises used: Set.iUnion_const
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
rw : M.Indep I
⊢ M.Indep (⋃ (i : ι), (fun (x : ι) ↦ I) i)

Tactic:
rw [iUnion_const]

Premises used: Set.iUnion_const
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep I

Tactic:
(hI (Classical.arbitrary ι)).indep

Premises used: Classical.arbitrary, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep I

Tactic:
exact (hI (Classical.arbitrary ι)).indep

Premises used: Classical.arbitrary, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
rw : M.IsBasis I (⋃ (i : (↑Xs : Type u_1)), (↑i : Set α))
⊢ M.IsBasis I (⋃₀ Xs)

Tactic:
rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
⊢ Nonempty.{u_1 + 1} (↑Xs : Type u_1)

Tactic:
have := Iff.mpr nonempty_coe_sort hne
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
this : Nonempty.{u_1 + 1} (↑Xs : Type u_1)
⊢ M.IsBasis I (⋃ (i : (↑Xs : Type u_1)), (↑i : Set α))

Tactic:
IsBasis.isBasis_iUnion _ fun X ↦ h X X.prop

Premises used: Subtype.prop, Matroid.IsBasis.isBasis_iUnion, Subtype.val
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
this : Nonempty.{u_1 + 1} (↑Xs : Type u_1)
⊢ M.IsBasis I (⋃ (i : (↑Xs : Type u_1)), (↑i : Set α))

Tactic:
exact IsBasis.isBasis_iUnion _ fun X ↦ h X X.prop
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I {x : α | M.IsBasis I (insert x I)}

Tactic:
hI.isBasis_of_forall_insert (fun e he ↦ (?_ : M.IsBasis _ _))
    (fun e he ↦ ⟨fun hu ↦ he.2 ?_, he.1.subset_ground⟩)

Premises used: Matroid.Indep.isBasis_of_forall_insert, Matroid.IsBasis.subset_ground, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
refine_1 : ∀ (e : α) (he : e ∈ I), M.IsBasis I (insert e I)
refine_2 : ∀ (e : α) (he : e ∈ {x : α | M.IsBasis I (insert x I)} \ I) (hu : M.Indep (insert e I)), e ∈ I
⊢ M.IsBasis I {x : α | M.IsBasis I (insert x I)}

Tactic:
refine hI.isBasis_of_forall_insert (fun e he ↦ (?_ : M.IsBasis _ _))
    (fun e he ↦ ⟨fun hu ↦ he.2 ?_, he.1.subset_ground⟩)
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ I
refine_1 : M.IsBasis I I
⊢ M.IsBasis I (insert e I)

Tactic:
rw [insert_eq_of_mem he]

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ I
⊢ M.IsBasis I I

Tactic:
hI.isBasis_self

Premises used: Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ I
⊢ M.IsBasis I I

Tactic:
exact hI.isBasis_self

Premises used: Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ {x : α | M.IsBasis I (insert x I)} \ I
hu : M.Indep (insert e I)
⊢ e ∈ I

Tactic:
simpa using (hu.eq_of_isBasis he.1).symm

Premises used: And.left, Eq.symm, Matroid.Indep.eq_of_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
rw : M.IsBasis (⋃ (b : Bool), bif b then I else J) (⋃ (b : Bool), bif b then X else Y)
⊢ M.IsBasis (I ∪ J) (X ∪ Y)

Tactic:
rw [union_eq_iUnion, union_eq_iUnion]

Premises used: Set.union_eq_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis (⋃ (b : Bool), bif b then I else J) (⋃ (b : Bool), bif b then X else Y)

Tactic:
IsBasis.iUnion_isBasis_iUnion _ _ ?_ ?_

Premises used: Matroid.IsBasis.iUnion_isBasis_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
refine_1 : ∀ (i : Bool), M.IsBasis (bif i then I else J) (bif i then X else Y)
refine_2 : M.Indep (⋃ (i : Bool), bif i then I else J)
⊢ M.IsBasis (⋃ (b : Bool), bif b then I else J) (⋃ (b : Bool), bif b then X else Y)

Tactic:
refine IsBasis.iUnion_isBasis_iUnion _ _ ?_ ?_

Premises used: Matroid.IsBasis.iUnion_isBasis_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
refine_1 : M.IsBasis J Y ∧ M.IsBasis I X
⊢ ∀ (i : Bool), M.IsBasis (bif i then I else J) (bif i then X else Y)

Tactic:
simp only [Bool.forall_bool, cond_false, cond_true]

Premises used: Bool.forall_bool, cond_true, cond_false
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis J Y ∧ M.IsBasis I X

Tactic:
⟨hJY, hIX⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis J Y ∧ M.IsBasis I X

Tactic:
exact ⟨hJY, hIX⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h refine_2 refine_2₁ refine_2₂ refine_2₃ : M.Indep (I ∪ J)
⊢ M.Indep (⋃ (i : Bool), bif i then I else J)

Tactic:
rwa [← union_eq_iUnion]

Premises used: Set.union_eq_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.IsBasis (I ∪ I) (X ∪ Y)

Tactic:
hIX.union_isBasis_union hIY _

Premises used: Matroid.IsBasis.union_isBasis_union
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
h : I = I ∪ I
convert! : M.Indep (I ∪ I)
⊢ M.IsBasis I (X ∪ Y)

Tactic:
convert! hIX.union_isBasis_union hIY _

Premises used: Matroid.IsBasis.union_isBasis_union
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
h h₁ : I = I
⊢ I = I ∪ I

Tactic:
rw [union_self]

Premises used: Set.union_self
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
rw : M.Indep I
⊢ M.Indep (I ∪ I)

Tactic:
rw [union_self]

Premises used: Set.union_self
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.Indep I

Tactic:
hIX.indep

Premises used: Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.Indep I

Tactic:
exact hIX.indep

Premises used: Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.IsBasis (J ∪ I) (J ∪ X)

Tactic:
hJ.isBasis_self.union_isBasis_union hI _

Premises used: Matroid.IsBasis.union_isBasis_union, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
h : J = J ∪ I
convert! : M.Indep (J ∪ I)
⊢ M.IsBasis J (J ∪ X)

Tactic:
convert! hJ.isBasis_self.union_isBasis_union hI _

Premises used: Matroid.IsBasis.union_isBasis_union, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
h h₁ : J = J
⊢ J = J ∪ I

Tactic:
rw [union_eq_self_of_subset_right hIJ]

Premises used: Set.union_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
rw : M.Indep J
⊢ M.Indep (J ∪ I)

Tactic:
rw [union_eq_self_of_subset_right hIJ]

Premises used: Set.union_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.Indep J

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
h : M.Indep (insert e I)
simp_rw : ∀ (h : M.Indep (I ∪ {e})), M.IsBasis (I ∪ {e}) (X ∪ {e})
⊢ M.IsBasis (insert e I) (insert e X)

Tactic:
simp_rw [← union_singleton] at *

Premises used: Set.union_singleton
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
h : M.Indep (I ∪ {e})
⊢ M.IsBasis (I ∪ {e}) (X ∪ {e})

Tactic:
hI.union_isBasis_union (h.subset subset_union_right).isBasis_self h

Premises used: Set.subset_union_right, Matroid.Indep.subset, Matroid.IsBasis.union_isBasis_union, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
h : M.Indep (I ∪ {e})
⊢ M.IsBasis (I ∪ {e}) (X ∪ {e})

Tactic:
exact hI.union_isBasis_union (h.subset subset_union_right).isBasis_self h

Premises used: Set.subset_union_right, Matroid.Indep.subset, Matroid.IsBasis.union_isBasis_union, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I X : Set α
hB : M.IsBase B
hBX : B ⊆ X
hIX : M.IsBasis I X
by_contra : ∀ (h : ¬M.IsBase I), False
⊢ M.IsBase I

Tactic:
by_contra h
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I X : Set α
hB : M.IsBase B
hBX : B ⊆ X
hIX : M.IsBasis I X
h : ¬M.IsBase I
obtain : ∀ (e : α) (heBI : e ∈ B \ I) (he : M.Indep (insert e I)), False
⊢ False

Tactic:
obtain ⟨e, heBI, he⟩ := hIX.indep.exists_insert_of_not_isBase h hB

Premises used: Matroid.Indep.exists_insert_of_not_isBase, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I X : Set α
hB : M.IsBase B
hBX : B ⊆ X
hIX : M.IsBasis I X
h : ¬M.IsBase I
e : α
heBI : e ∈ B \ I
he : M.Indep (insert e I)
⊢ False

Tactic:
heBI.2 (hIX.mem_of_insert_indep (hBX heBI.1) he)

Premises used: And.right, And.left, Matroid.IsBasis.mem_of_insert_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I X : Set α
hB : M.IsBase B
hBX : B ⊆ X
hIX : M.IsBasis I X
h : ¬M.IsBase I
e : α
heBI : e ∈ B \ I
he : M.Indep (insert e I)
⊢ False

Tactic:
exact heBI.2 (hIX.mem_of_insert_indep (hBX heBI.1) he)

Premises used: And.right, And.left, Matroid.IsBasis.mem_of_insert_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hB : M.IsBase B
obtain : ∀ (B' : Set α) (hB' : M.IsBasis B' (I ∪ B)) (hIB' : I ⊆ B'), ∃ (B' : Set α), M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B
⊢ ∃ (B' : Set α), M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B

Tactic:
obtain ⟨B', hB', hIB'⟩ := hI.subset_isBasis_of_subset <| subset_union_left (t := B)

Premises used: Set.subset_union_left, Matroid.Indep.subset_isBasis_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hB : M.IsBase B
B' : Set α
hB' : M.IsBasis B' (I ∪ B)
hIB' : I ⊆ B'
⊢ ∃ (B' : Set α), M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B

Tactic:
⟨B', hB.isBase_of_isBasis_superset subset_union_right hB', hIB', hB'.subset⟩

Premises used: Set.subset_union_right, Matroid.IsBase.isBase_of_isBasis_superset, Matroid.IsBasis.subset, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hB : M.IsBase B
B' : Set α
hB' : M.IsBasis B' (I ∪ B)
hIB' : I ⊆ B'
⊢ ∃ (B' : Set α), M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B

Tactic:
exact ⟨B', hB.isBase_of_isBasis_superset subset_union_right hB', hIB', hB'.subset⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis I X
hIJ : I ⊆ J
hJ : M.Indep J
⊢ J ∩ X = I

Tactic:
(subset_inter hIJ hIX.subset).antisymm'
  (fun _ he ↦ hIX.mem_of_insert_indep he.2 (hJ.subset (insert_subset he.1 hIJ)))

Premises used: Matroid.Indep.subset, Matroid.IsBasis.subset, Set.subset_inter, And.right, And.left, Matroid.IsBasis.mem_of_insert_indep, HasSubset.Subset.antisymm', Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
hIJ : I ⊆ J
hJ : M.Indep J
rw : J ∩ X = J ∩ (X ∩ M.E)
rw₁ : J ∩ X = J ∩ (M.E ∩ X)
rw₂ : J ∩ X = J ∩ M.E ∩ X
rw₃ rw₄ : J ∩ X = J ∩ X
⊢ J ∩ X = I

Tactic:
rw [← hI.isBasis_inter_ground.inter_eq_of_subset_indep hIJ hJ, inter_comm X, ← inter_assoc,
    inter_eq_self_of_subset_left hJ.subset_ground]

Premises used: Matroid.IsBasis'.isBasis_inter_ground, Set.inter_comm, Matroid.Indep.subset_ground, Matroid.IsBasis.inter_eq_of_subset_indep, Set.inter_assoc, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hX : X ⊆ M.E
hB : M.IsBase B
hBX : B ⊆ X
rw : ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J
⊢ M.IsBasis B X

Tactic:
rw [isBasis_iff, and_iff_right hB.indep, and_iff_right hBX]

Premises used: Matroid.isBasis_iff, and_iff_right, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hX : X ⊆ M.E
hB : M.IsBase B
hBX : B ⊆ X
⊢ ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J

Tactic:
fun J hJ hBJ _ ↦ hB.eq_of_subset_indep hJ hBJ

Premises used: Matroid.IsBase.eq_of_subset_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hX : X ⊆ M.E
hB : M.IsBase B
hBX : B ⊆ X
⊢ ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J

Tactic:
exact fun J hJ hBJ _ ↦ hB.eq_of_subset_indep hJ hBJ

Premises used: Matroid.IsBase.eq_of_subset_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
obtain :
  ∀ (I I' : Set α) (hI : M.IsBasis I X) (hI' : M.IsBasis I' Y) (hII' : I ⊆ I'),
    ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J
⊢ ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J

Tactic:
obtain ⟨I, I', hI, hI', hII'⟩ := M.exists_isBasis_subset_isBasis hXY

Premises used: Matroid.exists_isBasis_subset_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
rwa : M.IsBasis (I ∪ I') Y
rwa₁ rwa₂ rwa₃ rwa₄ : M.IsBasis I' Y
⊢ M.IsBasis (I ∪ I' \ I) Y

Tactic:
rwa [union_diff_self, union_eq_self_of_subset_left hII']

Premises used: Set.union_eq_self_of_subset_left, Set.union_diff_self
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
refine : Disjoint X (I' \ I)
⊢ ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J

Tactic:
refine ⟨I, I' \ I, hI, by rwa [union_diff_self, union_eq_self_of_subset_left hII'], ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
rw : ∀ ⦃a : α⦄, a ∈ X → ∀ ⦃b : α⦄, b ∈ I' \ I → a ≠ b
⊢ Disjoint X (I' \ I)

Tactic:
rw [disjoint_iff_forall_ne]

Premises used: Set.disjoint_iff_forall_ne
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
e : α
heX : e ∈ X
heI' : e ∈ I'
heI : e ∉ I
⊢ False

Tactic:
heI <| hI.mem_of_insert_indep heX (hI'.indep.subset (insert_subset heI' hII'))

Premises used: Matroid.Indep.subset, Matroid.IsBasis.mem_of_insert_indep, Matroid.IsBasis.indep, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
e : α
heX : e ∈ X
heI' : e ∈ I'
heI : e ∉ I
⊢ False

Tactic:
exact heI <| hI.mem_of_insert_indep heX (hI'.indep.subset (insert_subset heI' hII'))

Premises used: Matroid.Indep.subset, Matroid.IsBasis.mem_of_insert_indep, Matroid.IsBasis.indep, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
⊢ Function.Injective f

Tactic:
fun M M' hMM' ↦ ?_

Premises used: Function.Injective
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
refine : ∀ (M M' : Matroid α) (hMM' : f M = f M'), M = M'
⊢ Function.Injective f

Tactic:
refine fun M M' hMM' ↦ ?_
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
M M' : Matroid α
hMM' : f M = f M'
⊢ M.E = M'.E ∧
    ∀ (x : Set α),
      Membership.mem (γ := Set (Set α)) {B : Set α | M.IsBase B} x ↔
        Membership.mem (γ := Set (Set α)) {B : Set α | M'.IsBase B} x

Tactic:
rw [Prod.mk.injEq, and_comm, Set.ext_iff, and_comm] at hMM'

Premises used: and_comm, Prod.mk.injEq, Set.ext_iff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
M M' : Matroid α
hMM' :
  M.E = M'.E ∧
    ∀ (x : Set α),
      Membership.mem (γ := Set (Set α)) {B : Set α | M.IsBase B} x ↔
        Membership.mem (γ := Set (Set α)) {B : Set α | M'.IsBase B} x
⊢ M = M'

Tactic:
ext_isBase hMM'.1 (fun B _ ↦ hMM'.2 B)

Premises used: Matroid.ext_isBase, And.right, And.left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
M M' : Matroid α
hMM' :
  M.E = M'.E ∧
    ∀ (x : Set α),
      Membership.mem (γ := Set (Set α)) {B : Set α | M.IsBase B} x ↔
        Membership.mem (γ := Set (Set α)) {B : Set α | M'.IsBase B} x
⊢ M = M'

Tactic:
exact ext_isBase hMM'.1 (fun B _ ↦ hMM'.2 B)

Premises used: Matroid.ext_isBase, And.right, And.left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
⊢ Function.Injective f

Tactic:
have hf : f.Injective := by
    refine fun M M' hMM' ↦ ?_
    rw [Prod.mk.injEq, and_comm, Set.ext_iff, and_comm] at hMM'
    exact ext_isBase hMM'.1 (fun B _ ↦ hMM'.2 B)
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
hf : Function.Injective f
rw : (f '' {M : Matroid α | M.E ⊆ E}).Finite
⊢ Set.Finite.{u_1} (α := Matroid α) {M : Matroid α | M.E ⊆ E}

Tactic:
rw [← Set.finite_image_iff hf.injOn]

Premises used: Function.Injective.injOn, Set.finite_image_iff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
hf : Function.Injective f
⊢ (f '' {M : Matroid α | M.E ⊆ E}).Finite

Tactic:
(hE.finite_subsets.prod hE.finite_subsets.finite_subsets).subset ?_

Premises used: Set.Finite.subset, Set.Finite.finite_subsets, Set.Finite.prod
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
hf : Function.Injective f
refine :
  f '' {M : Matroid α | M.E ⊆ E} ⊆
    SProd.sprod (α := Set (Set α)) (β := Set (Set (Set α))) {b : Set α | b ⊆ E}
      {b : Set (Set α) | b ⊆ {b : Set α | b ⊆ E}}
⊢ (f '' {M : Matroid α | M.E ⊆ E}).Finite

Tactic:
refine (hE.finite_subsets.prod hE.finite_subsets.finite_subsets).subset ?_

Premises used: Set.Finite.subset, Set.Finite.finite_subsets, Set.Finite.prod
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
E : Set α
hE_1 : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
hf : Function.Injective f
M : Matroid α
hE : M.E ⊆ E
⊢ (f M).1 ⊆ E ∧ (f M).2 ⊆ {b : Set α | b ⊆ E}

Tactic:
⟨hE, fun B hB ↦ hB.subset_ground.trans hE⟩

Premises used: HasSubset.Subset.trans, Matroid.IsBase.subset_ground, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
E : Set α
hE_1 : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
hf : Function.Injective f
M : Matroid α
hE : M.E ⊆ E
⊢ (f M).1 ⊆ E ∧ (f M).2 ⊆ {b : Set α | b ⊆ E}

Tactic:
exact ⟨hE, fun B hB ↦ hB.subset_ground.trans hE⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
hE : M.E.Finite
⊢ Membership.mem (γ := Set (Matroid α)) {M_1 : Matroid α | M_1.E ⊆ M.E} M

Tactic:
subset_refl M.E

Premises used: Set.Mem, Matroid.E, setOf, subset_refl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
hE : M.E.Finite
⊢ Membership.mem (γ := Set (Matroid α)) {M_1 : Matroid α | M_1.E ⊆ M.E} M

Tactic:
exact subset_refl M.E

Premises used: Matroid.E, subset_refl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ Minimal M.Dep C

Tactic:
Iff.rfl

Premises used: Iff.rfl, Matroid.IsCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ M.Dep C

Tactic:
hC.prop

Premises used: Minimal.prop
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ ¬M.Indep C

Tactic:
hC.dep.not_indep

Premises used: Matroid.Dep.not_indep, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ Minimal M.Dep C

Tactic:
hC

Premises used: Matroid.IsCircuit