awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
⊢ M.IsBasis B S ↔ M.IsBase B ∧ B ⊆ S

Tactic:
⟨fun h ↦ ⟨?_, h.subset⟩, fun h ↦ h.1.indep.isBasis_of_subset_of_subset_closure h.2 ?_⟩

Premises used: Matroid.IsBasis.subset, And.right, And.left, And.intro, Iff.intro, Matroid.IsBase.indep, Matroid.Indep.isBasis_of_subset_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
refine_1 : ∀ (h : M.IsBasis B S), M.IsBase B
refine_2 : ∀ (h : M.IsBase B ∧ B ⊆ S), S ⊆ M.closure B
⊢ M.IsBasis B S ↔ M.IsBase B ∧ B ⊆ S

Tactic:
refine ⟨fun h ↦ ⟨?_, h.subset⟩, fun h ↦ h.1.indep.isBasis_of_subset_of_subset_closure h.2 ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBasis B S
rwa rwa₁ rwa₂ rwa₃ : M.Spanning S
⊢ M.Spanning B

Tactic:
rwa [h.spanning_iff_spanning]

Premises used: Matroid.IsBasis.spanning_iff_spanning
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBasis B S
⊢ M.IsBase B

Tactic:
exact h.indep.isBase_of_spanning <| by rwa [h.spanning_iff_spanning]

Premises used: Matroid.Indep.isBase_of_spanning, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
refine_2 : S ⊆ M.E
⊢ S ⊆ M.closure B

Tactic:
rw [h.1.closure_eq]

Premises used: Matroid.IsBase.closure_eq, And.left
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
⊢ S ⊆ M.E

Tactic:
hS.subset_ground

Premises used: Matroid.Spanning.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
⊢ S ⊆ M.E

Tactic:
exact hS.subset_ground

Premises used: Matroid.Spanning.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS rwa rwa₁ rwa₂ rwa₃ : M.Spanning S
⊢ M.Coindep (M.E \ S)

Tactic:
rwa [← spanning_iff_compl_coindep]

Premises used: Matroid.spanning_iff_compl_coindep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
hX rwa rwa₁ rwa₂ rwa₃ : M.Spanning X
⊢ M.Spanning I

Tactic:
rwa [hIX.spanning_iff_spanning]

Premises used: Matroid.IsBasis.spanning_iff_spanning
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S I : Set α
hI : M.Indep I
hS : M.Spanning S
hIS : I ⊆ S
obtain : ∀ (B : Set α) (hB : M.IsBasis B S ∧ I ⊆ B), ∃ (B : Set α), M.IsBase B ∧ I ⊆ B ∧ B ⊆ S
⊢ ∃ (B : Set α), M.IsBase B ∧ I ⊆ B ∧ B ⊆ S

Tactic:
obtain ⟨B, hB⟩ := hI.subset_isBasis_of_subset hIS

Premises used: Matroid.Indep.subset_isBasis_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S I : Set α
hI : M.Indep I
hS : M.Spanning S
hIS : I ⊆ S
B : Set α
hB : M.IsBasis B S ∧ I ⊆ B
⊢ ∃ (B : Set α), M.IsBase B ∧ I ⊆ B ∧ B ⊆ S

Tactic:
⟨B, hB.1.isBase_of_spanning hS, hB.2, hB.1.subset⟩

Premises used: Matroid.IsBasis.isBase_of_spanning, Matroid.IsBasis.subset, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S I : Set α
hI : M.Indep I
hS : M.Spanning S
hIS : I ⊆ S
B : Set α
hB : M.IsBasis B S ∧ I ⊆ B
⊢ ∃ (B : Set α), M.IsBase B ∧ I ⊆ B ∧ B ⊆ S

Tactic:
exact ⟨B, hB.1.isBase_of_spanning hS, hB.2, hB.1.subset⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B : Set α
N : Matroid α
hR : N ≤r M
hN : M.Spanning N.E
obtain : ∀ (R : Set α) (hR : R ⊆ M.E) (hN : M.Spanning (M ↾ R).E), (M ↾ R).IsBase B ↔ M.IsBase B ∧ B ⊆ (M ↾ R).E
⊢ N.IsBase B ↔ M.IsBase B ∧ B ⊆ N.E

Tactic:
obtain ⟨R, hR : R ⊆ M.E, rfl⟩ := hR

Premises used: Matroid.E, rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B R : Set α
hR : R ⊆ M.E
hN : M.Spanning (M ↾ R).E
rw : M.IsBase B ∧ B ⊆ R ↔ M.IsBase B ∧ B ⊆ (M ↾ R).E
rw₁ rw₂ : M.IsBase B ∧ B ⊆ R ↔ M.IsBase B ∧ B ⊆ R
⊢ (M ↾ R).IsBase B ↔ M.IsBase B ∧ B ⊆ (M ↾ R).E

Tactic:
rw [Spanning.isBase_restrict_iff (show M.Spanning R from hN), restrict_ground_eq]

Premises used: Matroid.restrict_ground_eq, Matroid.Spanning.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
h₁ : ∀ (S : Set α), M.Spanning S ↔ M'.Spanning S
⊢ M.Spanning = M'.Spanning

Tactic:
ext S
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
hSE : S ⊆ M.E
rw rw₁ : M'.Spanning S ↔ M'.Spanning S
⊢ M.Spanning S ↔ M'.Spanning S

Tactic:
rw [hsp _ hSE]
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
⊢ M.Spanning S ↔ M'.Spanning S

Tactic:
refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE])
      (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
      (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))

Premises used: Matroid.E, em, HasSubset.Subset, iff_of_false, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
⊢ M.Spanning = M'.Spanning

Tactic:
have hsp' : M.Spanning = M'.Spanning := by
    ext S
    refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE])
      (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
      (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
rw : ∀ ⦃I : Set α⦄, I ⊆ M.E → (M✶.Indep I ↔ M'✶.Indep I)
⊢ M = M'

Tactic:
rw [← dual_inj, ext_iff_indep, dual_ground, dual_ground, and_iff_right h]

Premises used: and_iff_right, Matroid.dual_ground, Matroid.ext_iff_indep, Matroid.dual_inj
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
rw : M.Coindep I ↔ M'✶.Indep I
rw₁ : M.Coindep I ↔ M'.Coindep I
rw₂ : M.Spanning (M.E \ I) ↔ M'.Coindep I
rw₃ : M.Spanning (M.E \ I) ↔ M'.Spanning (M'.E \ I)
rw₄ : M'.Spanning (M.E \ I) ↔ M'.Spanning (M'.E \ I)
rw₅ rw₆ : M'.Spanning (M'.E \ I) ↔ M'.Spanning (M'.E \ I)
⊢ M✶.Indep I ↔ M'✶.Indep I

Tactic:
rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]

Premises used: Matroid.coindep_iff_compl_spanning, Matroid.coindep_def
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X B : Set α
hB : M.IsBase B
hX : M.Spanning X
hXB : X ⊆ B
B' : Set α
hB' : M.IsBase B'
hB'X rwa rwa₁ rwa₂ rwa₃ : B' ⊆ X
⊢ B ⊆ X

Tactic:
rwa [← hB'.eq_of_subset_isBase hB (hB'X.trans hXB)]

Premises used: HasSubset.Subset.trans, Matroid.IsBase.eq_of_subset_isBase
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B : Set α
rw : M.IsBase B ↔ M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
⊢ M.IsBase B ↔ Minimal M.Spanning B

Tactic:
rw [minimal_subset_iff]

Premises used: minimal_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t

Tactic:
⟨fun h ↦ ⟨h.spanning, fun _ ↦ h.eq_of_superset_spanning⟩, fun ⟨h, h'⟩ ↦ ?_⟩

Premises used: Matroid.IsBase.eq_of_superset_spanning, _private.0.Matroid.isBase_iff_minimal_spanning.match_1, Matroid.IsBase.spanning, Matroid.IsBase, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B : Set α
refine :
  (M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t) →
    ∀ (h : M.Spanning B) (h' : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t), M.IsBase B
⊢ M.IsBase B ↔ M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t

Tactic:
refine ⟨fun h ↦ ⟨h.spanning, fun _ ↦ h.eq_of_superset_spanning⟩, fun ⟨h, h'⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B : Set α
h_1 : M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
h : M.Spanning B
h' : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
obtain : ∀ (B' : Set α) (hB' : M.IsBase B') (hBB' : B' ⊆ B), M.IsBase B
⊢ M.IsBase B

Tactic:
obtain ⟨B', hB', hBB'⟩ := h.exists_isBase_subset

Premises used: Matroid.Spanning.exists_isBase_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B : Set α
h_1 : M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
h : M.Spanning B
h' : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
B' : Set α
hB' : M.IsBase B'
hBB' : B' ⊆ B
rwa rwa₁ rwa₂ rwa₃ : M.IsBase B'
⊢ M.IsBase B

Tactic:
rwa [h' hB'.spanning hBB']

Premises used: Matroid.IsBase.spanning
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
hX : M.Spanning X
h : ∀ ⦃Y : Set α⦄, M.Spanning Y → Y ⊆ X → X = Y
rwa : Minimal M.Spanning X
rwa₁ : M.Spanning X ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ X → X = t
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ X → X = t
⊢ M.IsBase X

Tactic:
rwa [isBase_iff_minimal_spanning, minimal_subset_iff, and_iff_right hX]

Premises used: and_iff_right, minimal_subset_iff, Matroid.isBase_iff_minimal_spanning
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X R : Set α
obtain : ∀ (I : Set α) (hI : (M ↾ R).IsBasis' I X), (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E
⊢ (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E

Tactic:
obtain ⟨I, hI⟩ := (M ↾ R).exists_isBasis' X

Premises used: Matroid.restrict, Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
⊢ M.IsBasis' I (X ∩ R)

Tactic:
obtain ⟨hI', hIR⟩ := isBasis'_restrict_iff.1 hI

Premises used: Matroid.isBasis'_restrict_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
⊢ I ⊆ R

Tactic:
obtain ⟨hI', hIR⟩ := isBasis'_restrict_iff.1 hI

Premises used: Matroid.isBasis'_restrict_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
h : ∀ (e : α), e ∈ (M ↾ R).closure X ↔ e ∈ M.closure (X ∩ R) ∩ R ∪ R \ M.E
⊢ (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E

Tactic:
ext e
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
h :
  e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
⊢ e ∈ (M ↾ R).closure X ↔ e ∈ M.closure (X ∩ R) ∩ R ∪ R \ M.E

Tactic:
rw [← hI.closure_eq_closure, ← hI'.closure_eq_closure, hI.indep.mem_closure_iff', mem_union,
    mem_inter_iff, hI'.indep.mem_closure_iff', restrict_ground_eq, restrict_indep_iff, mem_diff]

Premises used: Set.mem_union, Matroid.IsBasis'.closure_eq_closure, Matroid.Indep.mem_closure_iff', Set.mem_inter_iff, Matroid.restrict_ground_eq, Matroid.IsBasis'.indep, Set.mem_diff, Matroid.restrict_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
pos :
  ∀ (he : M.Indep (insert e I)),
    e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
      (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
neg :
  ∀ (he : ¬M.Indep (insert e I)),
    e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
      (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
⊢ e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

Tactic:
by_cases he : M.Indep (insert e I)

Premises used: Matroid.Indep, Insert.insert
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
he : M.Indep (insert e I)
⊢ e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

Tactic:
simp [he, and_comm, insert_subset_iff, hIR, (he.subset_ground (mem_insert ..)),
      imp_or_left_iff_true]

Premises used: and_comm, Set.insert_subset_iff, Matroid.Indep.subset_ground, Set.mem_insert, imp_or_left_iff_true
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
X R : Set α
M : Matroid α
hXR : X ⊆ R
hR : R ⊆ M.E
rw : M.closure (X ∩ R) ∩ R ∪ R \ M.E = M.closure X ∩ R
rw₁ : M.closure (X ∩ R) ∩ R ∪ ∅ = M.closure X ∩ R
rw₂ : M.closure (X ∩ R) ∩ R = M.closure X ∩ R
rw₃ rw₄ : M.closure X ∩ R = M.closure X ∩ R
⊢ (M ↾ R).closure X = M.closure X ∩ R

Tactic:
rw [restrict_closure_eq', diff_eq_empty.mpr hR, union_empty, inter_eq_self_of_subset_left hXR]

Premises used: Iff.mpr, Set.union_empty, Matroid.restrict_closure_eq', Set.diff_eq_empty, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
X : Set α
⊢ (emptyOn α).closure X = ∅

Tactic:
(closure_subset_ground ..).antisymm <| empty_subset _

Premises used: Matroid.closure_subset_ground, HasSubset.Subset.antisymm, Set.empty_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
E X : Set α
⊢ (loopyOn E).closure X = E

Tactic:
simp [loopyOn, restrict_closure_eq']

Premises used: Matroid.loopyOn, Matroid.restrict_closure_eq'
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
X E : Set α
rw : (loopyOn E).closure X = (loopyOn E).E ∧ X ⊆ (loopyOn E).E ↔ X ⊆ E
rw₁ : E = (loopyOn E).E ∧ X ⊆ (loopyOn E).E ↔ X ⊆ E
rw₂ : E = E ∧ X ⊆ E ↔ X ⊆ E
rw₃ rw₄ : X ⊆ E ↔ X ⊆ E
⊢ (loopyOn E).Spanning X ↔ X ⊆ E

Tactic:
rw [spanning_iff, loopyOn_closure_eq, loopyOn_ground, and_iff_right rfl]

Premises used: Matroid.spanning_iff, and_iff_right, Matroid.loopyOn_closure_eq, Matroid.loopyOn_ground, rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
E X : Set α
⊢ (freeOn E).closure X = X ∩ E

Tactic:
simp +contextual [← closure_inter_ground _ X, Set.ext_iff, and_comm,
    insert_subset_iff, freeOn_indep_iff, (freeOn_indep inter_subset_right).mem_closure_iff']

Premises used: Matroid.Indep.mem_closure_iff', Matroid.freeOn_indep, and_comm, Set.insert_subset_iff, Matroid.closure_inter_ground, Matroid.freeOn_indep_iff, Set.ext_iff, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
I E X : Set α
rw : (freeOn I ↾ E).closure X = X ∩ I ∩ E ∪ E \ I
rw₁ : (freeOn I).closure (X ∩ E) ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₂ : X ∩ E ∩ I ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₃ : X ∩ E ∩ E ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₄ : X ∩ (E ∩ E) ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₅ : X ∩ E ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₆ : X ∩ I ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₇ rw₈ : X ∩ I ∩ E ∪ E \ I = X ∩ I ∩ E ∪ E \ I
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I

Tactic:
rw [uniqueBaseOn, restrict_closure_eq', freeOn_closure_eq, inter_right_comm,
    inter_assoc (c := E), inter_self, inter_right_comm, freeOn_ground]

Premises used: Set.inter_self, Matroid.freeOn_ground, Matroid.uniqueBaseOn, Matroid.freeOn_closure_eq, Set.inter_right_comm, Matroid.restrict_closure_eq', Set.inter_assoc
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
h : M = loopyOn M.E
rw : (loopyOn M.E).closure ∅ = (loopyOn M.E).E
rw₁ : M.E = (loopyOn M.E).E
rw₂ rw₃ : M.E = M.E
⊢ M.closure ∅ = M.E

Tactic:
rw [h, loopyOn_closure_eq, loopyOn_ground]

Premises used: Matroid.loopyOn_closure_eq, Matroid.loopyOn_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
refine : ∀ (h : M.closure ∅ = M.E) (X : Set α), M.closure X = (loopyOn M.E).closure X
⊢ M.closure ∅ = M.E ↔ M = loopyOn M.E

Tactic:
refine ⟨fun h ↦ ext_closure ?_, fun h ↦ by rw [h, loopyOn_closure_eq, loopyOn_ground]⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ M.closure X ⊆ (loopyOn M.E).closure X

Tactic:
simp [closure_subset_ground]

Premises used: Matroid.closure_subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
refine : ∀ (X : Set α), (loopyOn M.E).closure X ⊆ M.closure X
⊢ ∀ (X : Set α), M.closure X = (loopyOn M.E).closure X

Tactic:
refine fun X ↦ subset_antisymm (by simp [closure_subset_ground]) ?_

Premises used: subset_antisymm
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
rw : M.closure ∅ ⊆ M.closure X
⊢ (loopyOn M.E).closure X ⊆ M.closure X

Tactic:
rw [loopyOn_closure_eq, ← h]

Premises used: Matroid.loopyOn_closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ M.closure ∅ ⊆ M.closure X

Tactic:
M.closure_mono (empty_subset _)

Premises used: Matroid.closure_mono, Set.empty_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ M.closure ∅ ⊆ M.closure X

Tactic:
exact M.closure_mono (empty_subset _)

Premises used: Matroid.closure_mono, Set.empty_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X : Set α
obtain : ∀ (I : Set α) (hI : (M.comap f).IsBasis' I X), (M.comap f).closure X = f ⁻¹' M.closure (f '' X)
⊢ (M.comap f).closure X = f ⁻¹' M.closure (f '' X)

Tactic:
obtain ⟨I, hI⟩ := (M.comap f).exists_isBasis' X

Premises used: Matroid.comap, Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
⊢ M.IsBasis' (f '' I) (f '' X)

Tactic:
obtain ⟨hI', hIinj, -⟩ := comap_isBasis'_iff.1 hI

Premises used: Matroid.comap_isBasis'_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
⊢ InjOn f I

Tactic:
obtain ⟨hI', hIinj, -⟩ := comap_isBasis'_iff.1 hI

Premises used: Matroid.comap_isBasis'_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
simp_rw :
  ∀ (x : α),
    f x ∈ M.E →
      (M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x)
⊢ (M.comap f).closure X = f ⁻¹' M.closure (f '' X)

Tactic:
simp_rw [← hI.closure_eq_closure, ← hI'.closure_eq_closure, Set.ext_iff,
    hI.indep.mem_closure_iff', comap_ground_eq, mem_preimage, hI'.indep.mem_closure_iff',
    comap_indep_iff, and_imp, mem_image, and_congr_right_iff, ← image_insert_eq]

Premises used: Matroid.IsBasis'.closure_eq_closure, Matroid.Indep.mem_closure_iff', and_imp, Set.mem_image, Matroid.comap_indep_iff, and_congr_right_iff, Matroid.IsBasis'.indep, Matroid.comap_ground_eq, Set.image_insert_eq, Set.ext_iff, Set.mem_preimage
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
pos :
  ∀ (hxI : x ∈ I),
    M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x
neg :
  ∀ (hxI : x ∉ I),
    M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x
⊢ M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x

Tactic:
by_cases hxI : x ∈ I
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∈ I
⊢ M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x

Tactic:
simp [hxI, show ∃ y ∈ I, f y = f x from ⟨x, hxI, rfl⟩]

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
⊢ M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x

Tactic:
simp [hxI, injOn_insert hxI, hIinj]

Premises used: Set.injOn_insert
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
obtain : ∀ (I : Set α) (hI : M.IsBasis I (f ⁻¹' X ∩ M.E)), (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis (f ⁻¹' X ∩ M.E)

Premises used: Matroid.E, Inter.inter, Set.preimage, Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
rw : (M.map f hf).closure (X ∩ (M.map f hf).E) = f '' M.closure (f ⁻¹' X)
rw₁ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X)
rw₂ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X ∩ M.E)
rw₃ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure I
rw₄ : (M.map f hf).closure (X ∩ f '' M.E) = (M.map f hf).closure (f '' I)
rw₅ : (M.map f hf).closure (f '' (f ⁻¹' X ∩ M.E)) = (M.map f hf).closure (f '' I)
rw₆ rw₇ : (M.map f hf).closure (f '' I) = (M.map f hf).closure (f '' I)
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Tactic:
rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]

Premises used: Matroid.map_ground, Set.image_preimage_inter, Matroid.closure_inter_ground, Matroid.IsBasis.map, Matroid.IsBasis.indep, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
suffices : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Tactic:
suffices aux : ∀ ⦃I⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' (M.closure I) by
    obtain ⟨I, hI⟩ := M.exists_isBasis (f ⁻¹' X ∩ M.E)
    rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
⊢ ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I

Tactic:
fun I hI ↦ Set.ext fun e ↦ ?_

Premises used: Set.ext
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
refine : ∀ (I : Set α) (hI : M.Indep I) (e : β), e ∈ (M.map f hf).closure (f '' I) ↔ e ∈ f '' M.closure I
⊢ ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I

Tactic:
refine fun I hI ↦ Set.ext fun e ↦ ?_

Premises used: Set.ext