awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
simp :
  ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) ↔
    ∃ (x : α), (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e
⊢ e ∈ (M.map f hf).closure (f '' I) ↔ e ∈ f '' M.closure I

Tactic:
simp only [(hI.map f hf).mem_closure_iff', map_ground, mem_image, map_indep_iff,
    forall_exists_index, and_imp, hI.mem_closure_iff']

Premises used: Matroid.Indep.mem_closure_iff', Matroid.map_ground, Matroid.Indep.map, and_imp, Set.mem_image, forall_exists_index, Matroid.map_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
mp :
  ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) →
    ∃ (x : α), (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e
mpr :
  (∃ (x : α), (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e) →
    (∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e
⊢ ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) ↔
    ∃ (x : α), (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
⊢ ∃ (x_1 : α), (x_1 ∈ M.E ∧ (M.Indep (insert x_1 I) → x_1 ∈ I)) ∧ f x_1 = f x

Tactic:
⟨x, ⟨hxE, fun hI' ↦ ?_⟩, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
mp : ∀ (hI' : M.Indep (insert x I)), x ∈ I
⊢ ∃ (x_1 : α), (x_1 ∈ M.E ∧ (M.Indep (insert x_1 I) → x_1 ∈ I)) ∧ f x_1 = f x

Tactic:
refine ⟨x, ⟨hxE, fun hI' ↦ ?_⟩, rfl⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hI' : M.Indep (insert x I)
mp : ∀ (y : α) (hyI : y ∈ I) (hfy : f y = f x), x ∈ I
⊢ x ∈ I

Tactic:
obtain ⟨y, hyI, hfy⟩ := h2 _ hI' image_insert_eq.symm

Premises used: Set.image_insert_eq, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hI' : M.Indep (insert x I)
y : α
hyI : y ∈ I
hfy : f y = f x
⊢ y = x

Tactic:
rw [hf.eq_iff (hI.subset_ground hyI) hxE] at hfy

Premises used: Set.InjOn.eq_iff, Matroid.Indep.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hI' : M.Indep (insert x I)
y : α
hyI : y ∈ I
hfy : y = x
mp mp₁ mp₂ mp₃ : y ∈ I
⊢ x ∈ I

Tactic:
rwa [← hfy]
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
⊢ (∃ x_1 ∈ M.E, f x_1 = f x) ∧ ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x

Tactic:
⟨⟨x, hxE, rfl⟩, fun J hJ hJI ↦ ⟨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 : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
mpr : ∀ (J : Set α) (hJ : M.Indep J) (hJI : insert (f x) (f '' I) = f '' J), M.Indep (insert x I)
⊢ (∃ x_1 ∈ M.E, f x_1 = f x) ∧ ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x

Tactic:
refine ⟨⟨x, hxE, rfl⟩, fun J hJ hJI ↦ ⟨x, hxi ?_, rfl⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJ : M.Indep J
hJI : insert (f x) (f '' I) = f '' J
⊢ (M.map f hf).Indep (f '' J)

Tactic:
replace hJ := hJ.map f hf
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : (M.map f hf).Indep (f '' J)
⊢ f '' insert x I = f '' J

Tactic:
have hrw := image_insert_eq ▸ hJI
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : (M.map f hf).Indep (f '' J)
hrw : f '' insert x I = f '' J
mpr : ∀ (hJ : (M.map f hf).Indep (f '' insert x I)) (hrw : f '' insert x I = f '' J), M.Indep (insert x I)
mpr₁ mpr₂ mpr₃ mpr₄ : ∀ (hJ : M.Indep (insert x I)) (hrw : f '' insert x I = f '' J), M.Indep (insert x I)
⊢ M.Indep (insert x I)

Tactic:
rwa [← hrw, map_image_indep_iff (insert_subset hxE hI.subset_ground)] at hJ

Premises used: Matroid.Indep.subset_ground, Matroid.map_image_indep_iff, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
rw : (M ↾ R).closure S = (M ↾ R).E ∧ S ⊆ (M ↾ R).E ↔ R ⊆ M.closure S
rw₁ : (M ↾ R).closure S = R ∧ S ⊆ R ↔ R ⊆ M.closure S
rw₂ : (M ↾ R).closure S = R ↔ R ⊆ M.closure S
rw₃ : M.closure S ∩ R = R ↔ R ⊆ M.closure S
rw₄ rw₅ : R ⊆ M.closure S ↔ R ⊆ M.closure S
⊢ (M ↾ R).Spanning S ↔ R ⊆ M.closure S

Tactic:
rw [spanning_iff, restrict_ground_eq, and_iff_left hSR, restrict_closure_eq _ hSR, inter_eq_right]

Premises used: and_iff_left, Matroid.restrict_closure_eq, Matroid.restrict_ground_eq, Matroid.spanning_iff, Set.inter_eq_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
R S : Set α
rw : S ⊆ R → (R ∩ M.E ⊆ M.closure (S ∩ R) ↔ R ∩ M.E ⊆ M.closure S)
⊢ (M ↾ R).Spanning S ↔ R ∩ M.E ⊆ M.closure S ∧ S ⊆ R

Tactic:
rw [spanning_iff, restrict_closure_eq', restrict_ground_eq, and_congr_left_iff,
    diff_eq_compl_inter, ← union_inter_distrib_right, inter_eq_right, union_comm,
    ← diff_subset_iff, diff_compl]

Premises used: Set.diff_subset_iff, Matroid.restrict_ground_eq, Set.diff_eq_compl_inter, Matroid.spanning_iff, Set.union_comm, Set.inter_eq_right, and_congr_left_iff, Matroid.restrict_closure_eq', Set.union_inter_distrib_right, Set.diff_compl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
rw rw₁ : R ∩ M.E ⊆ M.closure S ↔ R ∩ M.E ⊆ M.closure S
⊢ R ∩ M.E ⊆ M.closure (S ∩ R) ↔ R ∩ M.E ⊆ M.closure S

Tactic:
rw [inter_eq_self_of_subset_left hSR]

Premises used: Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α_1 : Type u_1
M : Matroid α_1
E B I X R J : Set α_1
α : Type u_2
⊢ ∀ ⦃I : Set α⦄, I = ∅ ↔ ∃ (B : Set α), B = ∅ ∧ I ⊆ B

Tactic:
simp [subset_empty_iff]

Premises used: Set.subset_empty_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α_1 : Type u_1
M : Matroid α_1
E B I X R J : Set α_1
α : Type u_2
Y : Set α
⊢ (fun (x : Set α) ↦ x = ∅) Y → ∀ a ∈ ∅ \ Y, ∃ b ∈ Y \ ∅, (fun (x : Set α) ↦ x = ∅) (insert b (∅ \ {a}))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α_1 : Type u_1
M : Matroid α_1
E B I X R J : Set α_1
α : Type u_2
X_1 : Set α
h : X_1 ⊆ ∅
⊢ Subset.{u_2} (α := Set α) ∅ ∅ ∧ Maximal (fun (K : Set α) ↦ (fun (x : Set α) ↦ x = ∅) K ∧ K ⊆ X_1) ∅

Tactic:
simp [Maximal]

Premises used: Maximal
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α_1 : Type u_1
M : Matroid α_1
E B I X R J : Set α_1
α : Type u_2
X_1 : Set α
h : X_1 ⊆ ∅
⊢ ∃ (J : Set α), ∅ ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (x : Set α) ↦ x = ∅) K ∧ K ⊆ X_1) J

Tactic:
exact ⟨∅, by simp [Maximal]⟩
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α_1 : Type u_1
M : Matroid α_1
E B I X R J : Set α_1
α : Type u_2
⊢ ∀ (B : Set α), B = ∅ → B ⊆ ∅

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
⊢ (emptyOn α).E = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
B : Set α
⊢ (emptyOn α).IsBase B ↔ B = ∅

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I : Set α
⊢ (emptyOn α).Indep I ↔ I = ∅

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
simp : M.E = ∅ → ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)
⊢ M.E = ∅ ↔ M = emptyOn α

Tactic:
simp only [emptyOn, ext_iff_indep, iff_self_and]

Premises used: iff_self_and, Matroid.emptyOn, Matroid.ext_iff_indep
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
h : M.E = ∅
⊢ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)

Tactic:
simp [h, subset_empty_iff]

Premises used: Set.subset_empty_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
⊢ M.E = ∅ → ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)

Tactic:
exact fun h ↦ by simp [h, subset_empty_iff]
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
rw : (emptyOn α)✶.E = ∅
⊢ (emptyOn α)✶ = emptyOn α

Tactic:
rw [← ground_eq_empty_iff]

Premises used: Matroid.ground_eq_empty_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
⊢ (emptyOn α)✶.E = ∅

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
⊢ M ↾ ∅ = emptyOn α

Tactic:
simp [← ground_eq_empty_iff]

Premises used: Matroid.ground_eq_empty_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
rw : M.E = ∅ ∨ M.Nonempty
⊢ M = emptyOn α ∨ M.Nonempty

Tactic:
rw [← ground_eq_empty_iff]

Premises used: Matroid.ground_eq_empty_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
⊢ M.E = ∅ ∨ M.Nonempty

Tactic:
M.E.eq_empty_or_nonempty.elim Or.inl (fun h ↦ Or.inr ⟨h⟩)

Premises used: Matroid.E, Set.eq_empty_or_nonempty, Or.inl, Or.elim, Matroid.Nonempty.mk, Or.inr
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
⊢ M.E = ∅ ∨ M.Nonempty

Tactic:
exact M.E.eq_empty_or_nonempty.elim Or.inl (fun h ↦ Or.inr ⟨h⟩)

Premises used: Matroid.E, Set.eq_empty_or_nonempty, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
inst : IsEmpty α
M : Matroid α
rw : M.E = ∅
⊢ M = emptyOn α

Tactic:
rw [← ground_eq_empty_iff]

Premises used: Matroid.ground_eq_empty_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
inst : IsEmpty α
M : Matroid α
⊢ M.E = ∅

Tactic:
M.E.eq_empty_of_isEmpty

Premises used: Matroid.E, Set.eq_empty_of_isEmpty
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
inst : IsEmpty α
M : Matroid α
⊢ M.E = ∅

Tactic:
exact M.E.eq_empty_of_isEmpty

Premises used: Matroid.E, Set.eq_empty_of_isEmpty
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α_1 : Type u_1
M : Matroid α_1
E B I X R J : Set α_1
α : Type u_2
⊢ (emptyOn α).Finite

Tactic:
⟨finite_empty⟩

Premises used: Set.finite_empty, Matroid.Finite.mk
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E : Set α
⊢ (loopyOn E).E = E

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_2
rw : Eq.{u_2 + 1} (α := Set α) (E (loopyOn ∅)) ∅
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set α) ∅ ∅
⊢ loopyOn ∅ = emptyOn α

Tactic:
rw [← ground_eq_empty_iff, loopyOn_ground]

Premises used: Matroid.ground_eq_empty_iff, Matroid.loopyOn_ground
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
simp : I = ∅ → I ⊆ E
⊢ (loopyOn E).Indep I ↔ I = ∅

Tactic:
simp only [loopyOn, restrict_indep_iff, emptyOn_indep_iff, and_iff_left_iff_imp]

Premises used: Matroid.loopyOn, Matroid.emptyOn_indep_iff, Matroid.restrict_indep_iff, and_iff_left_iff_imp
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E : Set α
⊢ ∅ ⊆ E

Tactic:
apply empty_subset

Premises used: Set.empty_subset
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E : Set α
simp : M.E = E → ((∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)) ↔ ∀ X ⊆ M.E, M.Indep X → X = ∅)
⊢ M = loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X → X = ∅

Tactic:
simp only [ext_iff_indep, loopyOn_ground, loopyOn_indep_iff, and_congr_right_iff]

Premises used: Matroid.loopyOn_indep_iff, and_congr_right_iff, Matroid.ext_iff_indep, Matroid.loopyOn_ground
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
h : ∀ X ⊆ M.E, M.Indep X → X = ∅
hIE : ∅ ⊆ M.E
⊢ M.Indep ∅

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
⊢ (∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)) ↔ ∀ X ⊆ M.E, M.Indep X → X = ∅

Tactic:
refine ⟨fun h I hI ↦ (h hI).1, fun h I hIE ↦ ⟨h I hIE, by rintro rfl; simp⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E B : Set α
⊢ (loopyOn E).IsBase B ↔ B = ∅

Tactic:
simp [Maximal, isBase_iff_maximal_indep]

Premises used: Maximal, Matroid.isBase_iff_maximal_indep
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E X : Set α
hX : X ⊆ E
rw : (loopyOn E).Indep ∅ ∧ ∅ ⊆ X ∧ ∀ (J : Set α), (loopyOn E).Indep J → ∅ ⊆ J → J ⊆ X → ∅ = J
⊢ (loopyOn E).IsBasis ∅ X

Tactic:
rw [isBasis_iff]

Premises used: Matroid.isBasis_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).Indep ∅ ∧ ∅ ⊆ X ∧ ∀ (J : Set α), (loopyOn E).Indep J → ∅ ⊆ J → J ⊆ X → ∅ = J

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E B I X R J : Set α
⊢ (loopyOn E).IsBase ∅ ∧ Set.Finite.{u_1} (α := α) ∅

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E : Set α
hE : E.Finite
⊢ (loopyOn E).Finite

Tactic:
⟨hE⟩

Premises used: Matroid.Finite.mk
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E R : Set α
⊢ loopyOn E ↾ R = loopyOn R

Tactic:
ext_indep rfl ?_

Premises used: Matroid.ext_indep, rfl
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E R : Set α
refine : ∀ ⦃I : Set α⦄, I ⊆ (loopyOn E ↾ R).E → ((loopyOn E ↾ R).Indep I ↔ (loopyOn R).Indep I)
⊢ loopyOn E ↾ R = loopyOn R

Tactic:
refine ext_indep rfl ?_

Premises used: Matroid.ext_indep, rfl
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E R : Set α
simp : ∀ ⦃I : Set α⦄, I ⊆ R → I = ∅ → I ⊆ R
⊢ ∀ ⦃I : Set α⦄, I ⊆ (loopyOn E ↾ R).E → ((loopyOn E ↾ R).Indep I ↔ (loopyOn R).Indep I)

Tactic:
simp only [restrict_ground_eq, restrict_indep_iff, loopyOn_indep_iff, and_iff_left_iff_imp]

Premises used: Matroid.loopyOn_indep_iff, Matroid.restrict_ground_eq, Matroid.restrict_indep_iff, and_iff_left_iff_imp
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E R : Set α
⊢ ∀ ⦃I : Set α⦄, I ⊆ R → I = ∅ → I ⊆ R

Tactic:
fun _ h _ ↦ h
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E R : Set α
⊢ ∀ ⦃I : Set α⦄, I ⊆ R → I = ∅ → I ⊆ R

Tactic:
exact fun _ h _ ↦ h
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
simp : (∀ ⦃y : Set α⦄, M.Indep y → y = ∅) ↔ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)
⊢ M.IsBase ∅ ↔ M = loopyOn M.E

Tactic:
simp only [isBase_iff_maximal_indep, Maximal, empty_indep, le_eq_subset, empty_subset,
    subset_empty_iff, true_implies, true_and, ext_iff_indep, loopyOn_ground,
    loopyOn_indep_iff]

Premises used: Set.le_eq_subset, Matroid.loopyOn_indep_iff, Matroid.empty_indep, true_implies, Set.empty_subset, Maximal, Set.subset_empty_iff, Matroid.isBase_iff_maximal_indep, Matroid.ext_iff_indep, Matroid.loopyOn_ground, true_and
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
h : ∀ ⦃y : Set α⦄, M.Indep y → y = ∅
I : Set α
h_1 : I ⊆ M.E
hI : I = ∅
⊢ M.Indep I

Tactic:
simp [hI]
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
⊢ (∀ ⦃y : Set α⦄, M.Indep y → y = ∅) ↔ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)

Tactic:
exact ⟨fun h I _ ↦ ⟨@h _, fun hI ↦ by simp [hI]⟩, fun h I hI ↦ (h hI.subset_ground).1 hI⟩
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
rw : M.IsBase ∅ ∨ ¬M.IsBase ∅
⊢ M = loopyOn M.E ∨ M.RankPos

Tactic:
rw [← empty_isBase_iff, rankPos_iff]

Premises used: Matroid.rankPos_iff, Matroid.empty_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
⊢ M.IsBase ∅ ∨ ¬M.IsBase ∅

Tactic:
apply em

Premises used: em
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
rw : ¬¬M.IsBase ∅ ↔ M = loopyOn M.E
rw₁ : ¬M = loopyOn M.E ↔ ¬M.IsBase ∅
rw₂ rw₃ : ¬M = loopyOn M.E ↔ ¬M = loopyOn M.E
⊢ ¬M.RankPos ↔ M = loopyOn M.E

Tactic:
rw [rankPos_iff, not_iff_comm, empty_isBase_iff]

Premises used: Matroid.rankPos_iff, Matroid.empty_isBase_iff, not_iff_comm
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E : Set α
⊢ (freeOn E).E = E

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E : Set α
rw : (loopyOn E)✶✶ = loopyOn E
rw₁ rw₂ : loopyOn E = loopyOn E
⊢ (freeOn E)✶ = loopyOn E

Tactic:
rw [freeOn, dual_dual]

Premises used: Matroid.dual_dual, Matroid.freeOn
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E : Set α
⊢ (loopyOn E)✶ = freeOn E

Tactic:
rfl

Premises used: rfl, Matroid.freeOn
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_2
⊢ freeOn ∅ = emptyOn α

Tactic:
simp [freeOn]

Premises used: Matroid.freeOn
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E B : Set α
⊢ (freeOn E).IsBase B ↔ B = E

Tactic:
simp only [freeOn, loopyOn_ground, dual_isBase_iff', loopyOn_isBase_iff, diff_eq_empty,
    ← subset_antisymm_iff, eq_comm (a := E)]

Premises used: Matroid.dual_isBase_iff', eq_comm, Matroid.loopyOn_isBase_iff, subset_antisymm_iff, Matroid.loopyOn_ground, Set.diff_eq_empty, Matroid.freeOn
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
⊢ (freeOn E).Indep I ↔ I ⊆ E

Tactic:
simp [indep_iff]

Premises used: Matroid.indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
hIE : I ⊆ E
⊢ (freeOn E).Indep I

Tactic:
freeOn_indep_iff.2 hIE

Premises used: Iff.mpr, Matroid.freeOn_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I X : Set α
mpr : I = X ∧ X ⊆ E → (freeOn E).IsBasis I X
⊢ (freeOn E).IsBasis I X ↔ I = X ∧ X ⊆ E

Tactic:
use fun h ↦ ⟨(freeOn_indep h.subset_ground).eq_of_isBasis h, h.subset_ground⟩
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
hIE : I ⊆ E
⊢ (freeOn E).IsBasis I I

Tactic:
(freeOn_indep hIE).isBasis_self

Premises used: Matroid.freeOn_indep, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
hIE : I ⊆ E
⊢ (freeOn E).IsBasis I I

Tactic:
exact (freeOn_indep hIE).isBasis_self

Premises used: Matroid.freeOn_indep, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I X : Set α
rw : (freeOn E).IsBasis I (X ∩ (freeOn E).E) ↔ I = X ∩ E
rw₁ : I = X ∩ (freeOn E).E ∧ X ∩ (freeOn E).E ⊆ E ↔ I = X ∩ E
rw₂ : I = X ∩ E ∧ X ∩ E ⊆ E ↔ I = X ∩ E
rw₃ rw₄ : I = X ∩ E ↔ I = X ∩ E
⊢ (freeOn E).IsBasis' I X ↔ I = X ∩ E

Tactic:
rw [isBasis'_iff_isBasis_inter_ground, freeOn_isBasis_iff, freeOn_ground,
    and_iff_left inter_subset_right]

Premises used: Matroid.freeOn_isBasis_iff, and_iff_left, Matroid.isBasis'_iff_isBasis_inter_ground, Matroid.freeOn_ground, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E : Set α
⊢ M = freeOn E ↔ M.E = E ∧ M.Indep E

Tactic:
⟨?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E : Set α
refine_1 : M = freeOn E → M.E = E ∧ M.Indep E
refine_2 : ∀ (h : M.E = E ∧ M.Indep E), M = freeOn E
⊢ M = freeOn E ↔ M.E = E ∧ M.Indep E

Tactic:
refine ⟨?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E : Set α
⊢ (freeOn E).E = E ∧ (freeOn E).Indep E

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M.E = E ∧ M.Indep E
refine_2 : ∀ ⦃I : Set α⦄, I ⊆ E → (M.Indep I ↔ I ⊆ E)
⊢ M = freeOn E

Tactic:
simp only [ext_iff_indep, freeOn_ground, freeOn_indep_iff, h.1, true_and]

Premises used: Matroid.freeOn_ground, And.left, Matroid.freeOn_indep_iff, Matroid.ext_iff_indep, true_and
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M.E = E ∧ M.Indep E
⊢ ∀ ⦃I : Set α⦄, I ⊆ E → (M.Indep I ↔ I ⊆ E)

Tactic:
fun I hIX ↦ iff_of_true (h.2.subset hIX) hIX

Premises used: Matroid.Indep.subset, iff_of_true, And.right
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M.E = E ∧ M.Indep E
⊢ ∀ ⦃I : Set α⦄, I ⊆ E → (M.Indep I ↔ I ⊆ E)

Tactic:
exact fun I hIX ↦ iff_of_true (h.2.subset hIX) hIX

Premises used: Matroid.Indep.subset, iff_of_true, And.right
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
⊢ M.Indep M.E ↔ M = freeOn M.E

Tactic:
simp [eq_freeOn_iff]

Premises used: Matroid.eq_freeOn_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E R : Set α
h : R ⊆ E
⊢ freeOn E ↾ R = freeOn R

Tactic:
simp [h, eq_freeOn_iff]

Premises used: Matroid.eq_freeOn_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
I : Set α
rw : (M ↾ I).E = I ∧ (M ↾ I).Indep I ↔ M.Indep I
rw₁ : (M ↾ I).Indep I ↔ M.Indep I
rw₂ : M.Indep I ∧ I ⊆ I ↔ M.Indep I
rw₃ rw₄ : M.Indep I ↔ M.Indep I
⊢ M ↾ I = freeOn I ↔ M.Indep I

Tactic:
rw [eq_freeOn_iff, and_iff_right M.restrict_ground_eq, restrict_indep_iff,
    and_iff_left Subset.rfl]

Premises used: and_iff_left, Matroid.restrict_ground_eq, and_iff_right, Set.Subset.rfl, Matroid.restrict_indep_iff, Matroid.eq_freeOn_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI rwa rwa₁ rwa₂ rwa₃ : M.Indep I
⊢ M ↾ I = freeOn I

Tactic:
rwa [restrict_eq_freeOn_iff]

Premises used: Matroid.restrict_eq_freeOn_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E B I X R J : Set α
simp : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → J ⊆ E) → I ⊆ E
⊢ (freeOn E).Finitary

Tactic:
simp only [finitary_iff, freeOn_indep_iff]

Premises used: Matroid.finitary_iff, Matroid.freeOn_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E B I_1 X R J I : Set α
h : ∀ J ⊆ I, J.Finite → J ⊆ E
e : α
heI : e ∈ I
⊢ {e} ⊆ I

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E B I_1 X R J I : Set α
h : ∀ J ⊆ I, J.Finite → J ⊆ E
e : α
heI : e ∈ I
⊢ e ∈ E

Tactic:
simpa using h {e} (by simpa)

Premises used: Singleton.singleton