awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ (i : ι), Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
refine : M.IsBasis J (Fs i ∪ X)
⊢ X ⊆ Fs i

Tactic:
refine subset_union_right.trans ((hFs i).1 (X := Fs i ∪ X) hIJ ?_)

Premises used: Set.subset_union_right, HasSubset.Subset.trans, Matroid.IsFlat.subset_of_isBasis_of_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ (i : ι), Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ M.IsBasis J (Fs i ∪ (J ∪ X))

Tactic:
hIJ.isBasis_union (hIX.isBasis_union_of_subset hIJ.indep hJ)

Premises used: Matroid.IsBasis.isBasis_union, Matroid.IsBasis.indep, Matroid.IsBasis.isBasis_union_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ (i : ι), Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
h : Fs i ∪ X = Fs i ∪ (J ∪ X)
⊢ M.IsBasis J (Fs i ∪ X)

Tactic:
convert! hIJ.isBasis_union (hIX.isBasis_union_of_subset hIJ.indep hJ) using 1

Premises used: Matroid.IsBasis.isBasis_union, Matroid.IsBasis.indep, Matroid.IsBasis.isBasis_union_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ (i : ι), Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
h : Fs i ∪ X = Fs i ∪ J ∪ X
h₁ h₂ : Fs i ∪ X = Fs i ∪ X
⊢ Fs i ∪ X = Fs i ∪ (J ∪ X)

Tactic:
rw [← union_assoc, union_eq_self_of_subset_right hIJ.subset]

Premises used: Set.union_eq_self_of_subset_right, Matroid.IsBasis.subset, Set.union_assoc
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M_1 : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set (↑(Iic M.E) : Type u_2)
hs : ∀ a ∈ s, (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a
inl :
  ∀
    (hs :
      ∀ (a : (↑(Iic M.E) : Type u_2)),
        Membership.mem (γ := Set (↑(Iic M.E) : Type u_2)) ∅ a →
          (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a),
    M.IsFlat (↑(sInf ∅) : Set α)
inr : ∀ (hne : s.Nonempty), M.IsFlat (↑(sInf s) : Set α)
⊢ M.IsFlat (↑(sInf s) : Set α)

Tactic:
obtain (rfl | hne) := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M_1 : Matroid α
F X Y : Set α
e f : α
M : Matroid α
hs :
  ∀ (a : (↑(Iic M.E) : Type u_2)),
    Membership.mem (γ := Set (↑(Iic M.E) : Type u_2)) ∅ a →
      (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a
⊢ M.IsFlat (↑(sInf ∅) : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M_1 : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set (↑(Iic M.E) : Type u_2)
hs : ∀ a ∈ s, (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a
hne : s.Nonempty
⊢ Nonempty.{u_2 + 1} (↑s : Type u_2)

Tactic:
have _ := hne.coe_sort
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M_1 : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set (↑(Iic M.E) : Type u_2)
hs : ∀ a ∈ s, (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a
hne : s.Nonempty
h : Nonempty.{u_2 + 1} (↑s : Type u_2)
⊢ M.IsFlat (⋂ (i : (↑s : Type u_2)), (fun (F : (↑s : Type u_2)) ↦ (↑(↑F : (↑(Iic M.E) : Type u_2)) : Set α)) i)

Tactic:
IsFlat.iInter (M := M) (Fs := fun (F : s) ↦ F.1.1) (fun F ↦ hs F.1 F.2)

Premises used: Matroid.IsFlat.iInter, Subtype.val, Subtype.property
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M_1 : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set (↑(Iic M.E) : Type u_2)
hs : ∀ a ∈ s, (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a
hne : s.Nonempty
h_1 : Nonempty.{u_2 + 1} (↑s : Type u_2)
h : (↑(sInf s) : Set α) = ⋂ (i : (↑s : Type u_2)), (↑(↑i : (↑(Iic M.E) : Type u_2)) : Set α)
⊢ M.IsFlat (↑(sInf s) : Set α)

Tactic:
convert! IsFlat.iInter (M := M) (Fs := fun (F : s) ↦ F.1.1) (fun F ↦ hs F.1 F.2)

Premises used: Matroid.IsFlat.iInter, Subtype.val, Subtype.property
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M_1 : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set (↑(Iic M.E) : Type u_2)
hs : ∀ a ∈ s, (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a
hne : s.Nonempty
h_1 : Nonempty.{u_2 + 1} (↑s : Type u_2)
h :
  ∀ (x : α),
    x ∈ (↑(sInf s) : Set α) ↔
      Membership.mem (γ := Set α) (⋂ (i : (↑s : Type u_2)), (↑(↑i : (↑(Iic M.E) : Type u_2)) : Set α)) x
⊢ (↑(sInf s) : Set α) = ⋂ (i : (↑s : Type u_2)), (↑(↑i : (↑(Iic M.E) : Type u_2)) : Set α)

Tactic:
ext
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M_1 : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set (↑(Iic M.E) : Type u_2)
hs : ∀ a ∈ s, (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a
hne : s.Nonempty
h : Nonempty.{u_2 + 1} (↑s : Type u_2)
x : α
⊢ x ∈ (↑(sInf s) : Set α) ↔
    Membership.mem (γ := Set α) (⋂ (i : (↑s : Type u_2)), (↑(↑i : (↑(Iic M.E) : Type u_2)) : Set α)) x

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
F : Set α
⊢ M.IsFlat F ↔ ∃ (h : F ⊆ M.E), M.subtypeClosure.IsClosed (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) F h)

Tactic:
simpa [subtypeClosure] using IsFlat.subset_ground

Premises used: Matroid.subtypeClosure, Matroid.IsFlat.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
F : (↑(Iic M.E) : Type u_2)
⊢ M.subtypeClosure.IsClosed F ↔ M.IsFlat (↑F : Set α)

Tactic:
simp [subtypeClosure]

Premises used: Matroid.subtypeClosure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.closure X = ⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F}

Tactic:
rfl

Premises used: Matroid.closure, rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
hX : X ⊆ M.E
rw : Eq.{u_2 + 1} (α := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F}) (⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F})
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F}) (⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F})
⊢ M.closure X = ⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F}

Tactic:
rw [closure, inter_eq_self_of_subset_left hX]

Premises used: Matroid.closure, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
F X Y : Set α
e f : α
⊢ Nonempty.{u_2 + 1} (↑{F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F} : Type u_2)

Tactic:
⟨M.E, M.ground_isFlat, inter_subset_right⟩

Premises used: Matroid.E, Matroid.ground_isFlat, Nonempty.intro, Subtype.mk, And.intro, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
this :
  ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔ x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a
⊢ M.closure X =
    (↑((M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
          (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) (X ∩ M.E) ⋯)) :
      Set α)

Tactic:
simpa [closure, subtypeClosure, Set.ext_iff]

Premises used: Matroid.subtypeClosure, Matroid.closure, Set.ext_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
suffices :
  ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔ x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a
⊢ M.closure X =
    (↑((M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
          (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) (X ∩ M.E) ⋯)) :
      Set α)

Tactic:
suffices ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔
    (x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a) by
    simpa [closure, subtypeClosure, Set.ext_iff]
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔ x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a

Tactic:
fun x ↦ ⟨fun h ↦ ⟨h _ M.ground_isFlat inter_subset_right, fun F _ hXF hF ↦ h F hF hXF⟩,
    fun ⟨_, h⟩ F hF hXF ↦ h F hF.subset_ground hXF hF⟩

Premises used: _private.0.Matroid.closure_eq_subtypeClosure.match_1, Matroid.E, Membership.mem, Matroid.ground_isFlat, And.intro, Iff.intro, Matroid.IsFlat.subset_ground, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔ x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a

Tactic:
exact fun x ↦ ⟨fun h ↦ ⟨h _ M.ground_isFlat inter_subset_right, fun F _ hXF hF ↦ h F hF hXF⟩,
    fun ⟨_, h⟩ F hF hXF ↦ h F hF.subset_ground hXF hF⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.closure X ⊆ M.E

Tactic:
sInter_subset_of_mem ⟨M.ground_isFlat, inter_subset_right⟩

Premises used: Matroid.ground_isFlat, Set.sInter_subset_of_mem, And.intro, Matroid.closure, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.E ⊆ M.closure X ↔ M.closure X = M.E

Tactic:
simp [M.closure_subset_ground X, subset_antisymm_iff]

Premises used: Matroid.closure_subset_ground, subset_antisymm_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
simp_rw :
  Eq.{u_2 + 1} (α := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ M.E ∩ M.E ⊆ F})
    (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F})
simp_rw₁ :
  Eq.{u_2 + 1} (α := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ (M.E ∩ M.E) ⊆ F})
    (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F})
⊢ M.closure (X ∩ M.E) = M.closure X

Tactic:
simp_rw [closure_def, inter_assoc, inter_self]

Premises used: Set.inter_self, Matroid.closure_def, Set.inter_assoc
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
simp_rw : ∀ (t' : Set α), Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F} t' → X ∩ M.E ⊆ t'
⊢ X ∩ M.E ⊆ M.closure X

Tactic:
simp_rw [closure_def, subset_sInter_iff]

Premises used: Matroid.closure_def, Set.subset_sInter_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ ∀ (t' : Set α), Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F} t' → X ∩ M.E ⊆ t'

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
X : Set α
hX : X ⊆ M.E
simp_rw :
  Membership.mem (γ := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F}) e ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
simp_rw₁ :
  (∀ (t : Set α), Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ X ⊆ F} t → e ∈ t) ↔
    ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
simp_rw₂ : (∀ (t : Set α), M.IsFlat t ∧ X ⊆ t → e ∈ t) ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
⊢ e ∈ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F

Tactic:
simp_rw [M.closure_def' X, mem_sInter, mem_setOf, and_imp]

Premises used: and_imp, Matroid.closure_def', Set.mem_setOf, Set.mem_sInter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
Y X : Set α
hX : X ⊆ M.E
simp_rw : Y ⊆ ⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F} ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
simp_rw₁ :
  (∀ (t' : Set α), Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ X ⊆ F} t' → Y ⊆ t') ↔
    ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
simp_rw₂ : (∀ (t' : Set α), M.IsFlat t' ∧ X ⊆ t' → Y ⊆ t') ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
⊢ Y ⊆ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F

Tactic:
simp_rw [M.closure_def' X, subset_sInter_iff, mem_setOf, and_imp]

Premises used: and_imp, Matroid.closure_def', Set.mem_setOf, Set.subset_sInter_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ X ⊆ M.closure X

Tactic:
simp [M.closure_def' X, subset_sInter_iff]

Premises used: Matroid.closure_def', Set.subset_sInter_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
F : Set α
hF : M.IsFlat F
⊢ Membership.mem (γ := Set (Set α)) {F_1 : Set α | M.IsFlat F_1 ∧ F ∩ M.E ⊆ F_1} F

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
rw : M.IsFlat (⋂ (i : (↑{F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F} : Type u_2)), (↑i : Set α))
⊢ M.IsFlat (M.closure X)

Tactic:
rw [closure, sInter_eq_iInter]

Premises used: Set.sInter_eq_iInter, Matroid.closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsFlat (⋂ (i : (↑{F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F} : Type u_2)), (↑i : Set α))

Tactic:
.iInter (·.2.1)

Premises used: And.left, Matroid.IsFlat.iInter, Subtype.property
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsFlat (⋂ (i : (↑{F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F} : Type u_2)), (↑i : Set α))

Tactic:
exact .iInter (·.2.1)
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
F : Set α
⊢ M.IsFlat F ↔ M.closure F = F

Tactic:
⟨(·.closure), (· ▸ isFlat_closure F)⟩

Premises used: Eq.rec, Matroid.isFlat_closure, Iff.intro, Matroid.IsFlat.closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
⊢ M.closure M.E = M.E

Tactic:
(M.closure_subset_ground M.E).antisymm (M.subset_closure M.E)

Premises used: Matroid.E, Matroid.closure_subset_ground, Matroid.subset_closure, HasSubset.Subset.antisymm
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
rw : M.closure (univ ∩ M.E) = M.E
rw₁ : M.closure M.E = M.E
rw₂ rw₃ : M.E = M.E
⊢ M.closure univ = M.E

Tactic:
rw [← closure_inter_ground, univ_inter, closure_ground]

Premises used: Set.univ_inter, Matroid.closure_ground, Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
X Y : Set α
M : Matroid α
h : X ⊆ Y
⊢ M.closure X ⊆ M.closure Y

Tactic:
subset_sInter (fun _ h' ↦ sInter_subset_of_mem
    ⟨h'.1, subset_trans (inter_subset_inter_left _ h) h'.2⟩)

Premises used: Matroid.E, subset_trans, Set.sInter_subset_of_mem, Set.inter_subset_inter_left, And.right, And.left, And.intro, Matroid.closure, Set.subset_sInter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
⊢ Monotone M.closure

Tactic:
fun _ _ ↦ M.closure_subset_closure

Premises used: Monotone, Matroid.closure_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.closure (M.closure X) = M.closure X

Tactic:
(M.subset_closure _).antisymm' (subset_sInter
    (fun F hF ↦ (closure_subset_closure _ (sInter_subset_of_mem hF)).trans hF.1.closure.subset))

Premises used: HasSubset.Subset.trans, Matroid.subset_closure, Set.sInter_subset_of_mem, Matroid.closure_subset_closure, Eq.subset, And.left, Set.subset_sInter, HasSubset.Subset.antisymm', Matroid.IsFlat.closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
hXY : X ⊆ M.closure Y
⊢ M.closure X ⊆ M.closure Y

Tactic:
(M.closure_subset_closure hXY).trans_eq (M.closure_closure Y)

Premises used: LE.le.trans_eq, Matroid.closure_closure, Matroid.closure_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
hX : X ⊆ M.E
⊢ M.closure X ⊆ M.closure Y ↔ X ⊆ M.closure Y

Tactic:
⟨(M.subset_closure X).trans, closure_subset_closure_of_subset_closure⟩

Premises used: HasSubset.Subset.trans, Matroid.subset_closure, Matroid.closure_subset_closure_of_subset_closure, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : Y ⊆ M.E
⊢ X ⊆ M.closure Y

Tactic:
hXY.trans (M.subset_closure Y)

Premises used: HasSubset.Subset.trans, Matroid.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : X ⊆ M.E
rw : X ⊆ M.closure (Y ∩ M.E)
⊢ X ⊆ M.closure Y

Tactic:
rw [← closure_inter_ground]

Premises used: Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : X ⊆ M.E
⊢ X ⊆ M.closure (Y ∩ M.E)

Tactic:
M.subset_closure_of_subset (subset_inter hXY hX)

Premises used: Matroid.subset_closure_of_subset, Set.subset_inter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : X ⊆ M.E
⊢ X ⊆ M.closure (Y ∩ M.E)

Tactic:
exact M.subset_closure_of_subset (subset_inter hXY hX)

Premises used: Matroid.subset_closure_of_subset, Set.subset_inter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
hXY : M.closure X ⊂ M.closure Y
by_contra! : ∀ (hcon : ∀ (e : α) (_ : e ∈ Y), e ∈ M.closure X), False
⊢ ∃ e ∈ Y, e ∉ M.closure X

Tactic:
by_contra! hcon
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
hXY : M.closure X ⊂ M.closure Y
hcon : ∀ (e : α) (_ : e ∈ Y), e ∈ M.closure X
⊢ False

Tactic:
hXY.not_subset (M.closure_subset_closure_of_subset_closure hcon)

Premises used: Matroid.closure_subset_closure_of_subset_closure, HasSSubset.SSubset.not_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
hXY : M.closure X ⊂ M.closure Y
hcon : ∀ (e : α) (_ : e ∈ Y), e ∈ M.closure X
⊢ False

Tactic:
exact hXY.not_subset (M.closure_subset_closure_of_subset_closure hcon)

Premises used: Matroid.closure_subset_closure_of_subset_closure, HasSSubset.SSubset.not_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
X : Set α
e : α
M : Matroid α
h : e ∈ X
hX : X ⊆ M.E
⊢ e ∈ M.closure X

Tactic:
(M.subset_closure X) h

Premises used: Matroid.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : e ∈ M.E
rw : e ∈ M.closure (X ∩ M.E)
⊢ e ∈ M.closure X

Tactic:
rw [← closure_inter_ground]

Premises used: Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : e ∈ M.E
⊢ e ∈ M.closure (X ∩ M.E)

Tactic:
M.mem_closure_of_mem ⟨heX, h⟩

Premises used: Matroid.mem_closure_of_mem, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : e ∈ M.E
⊢ e ∈ M.closure (X ∩ M.E)

Tactic:
exact M.mem_closure_of_mem ⟨heX, h⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ M.E \ M.closure X
⊢ e ∉ X

Tactic:
fun heX ↦ he.2 <| M.mem_closure_of_mem' heX he.1

Premises used: Matroid.mem_closure_of_mem', And.right, And.left, Not
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
⊢ e ∈ M.E

Tactic:
(M.closure_subset_ground _) he

Premises used: Matroid.closure_subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
simp_rw :
  Eq (α := { x : Set α // x ∈ Iic M.E })
    ((M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
        (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E)
          (⋃ (i : ι),
            (↑((M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
                    (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) (Xs i ∩ M.E) ⋯)) :
                Set α) ∩
              M.E)
          ⋯) :
      (↑(Iic M.E) : Type u_2))
    ((M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
        (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) (⋃ (i : ι), Xs i ∩ M.E) ⋯) :
      (↑(Iic M.E) : Type u_2))
⊢ M.closure (⋃ (i : ι), M.closure (Xs i)) = M.closure (⋃ (i : ι), Xs i)

Tactic:
simp_rw [closure_eq_subtypeClosure, iUnion_inter, Subtype.coe_inj]

Premises used: Subtype.coe_inj, Matroid.closure_eq_subtypeClosure, Set.iUnion_inter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ Eq (α := (↑(Iic M.E) : Type u_2))
    ((M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
      (⨆ (i : ι),
        (M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
          (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) (Xs i ∩ M.E) ⋯)))
    ((M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
      (⨆ (i : ι), Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) (Xs i ∩ M.E) ⋯))

Tactic:
M.subtypeClosure.closure_iSup_closure (fun i ↦ ⟨Xs i ∩ M.E, inter_subset_right⟩)

Premises used: Matroid.E, Matroid.subtypeClosure, Subtype.mk, Inter.inter, ClosureOperator.closure_iSup_closure, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ Eq.{u_2 + 1} (α := Set α)
    (⋃ (i : ι),
      (↑((M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
              (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) (Xs i ∩ M.E) ⋯)) :
          Set α) ∩
        M.E)
    (↑(⨆ (i : ι),
          (M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
            (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) (Xs i ∩ M.E) ⋯)) :
      Set α)

Tactic:
simp [← iUnion_inter, subtypeClosure]

Premises used: Matroid.subtypeClosure, Set.iUnion_inter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ Eq.{u_2 + 1} (α := Set α) (⋃ (i : ι), Xs i ∩ M.E)
    (↑(⨆ (i : ι), Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) (Xs i ∩ M.E) ⋯) : Set α)

Tactic:
simp [← iUnion_inter, subtypeClosure]

Premises used: Matroid.subtypeClosure, Set.iUnion_inter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs Ys : ι → Set α
h : ∀ (i : ι), M.closure (Xs i) = M.closure (Ys i)
⊢ M.closure (⋃ (i : ι), Xs i) = M.closure (⋃ (i : ι), Ys i)

Tactic:
simp [h, ← M.closure_iUnion_closure_eq_closure_iUnion]

Premises used: Matroid.closure_iUnion_closure_eq_closure_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
Xs : Set (Set α)
rw : M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃ (i : (↑Xs : Type u_2)), (↑i : Set α))
rw₁ : M.closure (⋃ (x : (↑Xs : Type u_2)), M.closure (↑x : Set α)) = M.closure (⋃ (i : (↑Xs : Type u_2)), (↑i : Set α))
rw₂ rw₃ : M.closure (⋃ (i : (↑Xs : Type u_2)), (↑i : Set α)) = M.closure (⋃ (i : (↑Xs : Type u_2)), (↑i : Set α))
⊢ M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)

Tactic:
rw [sUnion_eq_iUnion, biUnion_eq_iUnion, closure_iUnion_closure_eq_closure_iUnion]

Premises used: Matroid.closure_iUnion_closure_eq_closure_iUnion, Set.sUnion_eq_iUnion, Set.biUnion_eq_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
A : Set ι
rw : M.closure (⋃ (x : (↑A : Type u_1)), M.closure (Xs (↑x : ι))) = M.closure (⋃ i ∈ A, Xs i)
rw₁ : M.closure (⋃ (i : (↑A : Type u_1)), Xs (↑i : ι)) = M.closure (⋃ i ∈ A, Xs i)
rw₂ rw₃ : M.closure (⋃ (i : (↑A : Type u_1)), Xs (↑i : ι)) = M.closure (⋃ (x : (↑A : Type u_1)), Xs (↑x : ι))
⊢ M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)

Tactic:
rw [biUnion_eq_iUnion, M.closure_iUnion_closure_eq_closure_iUnion, biUnion_eq_iUnion]

Premises used: Matroid.closure_iUnion_closure_eq_closure_iUnion, Set.biUnion_eq_iUnion