awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
I : Set (↑M.E : Type u_1)
hI : M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I)
mpr :
  M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) ∧
    ∃ (t : Set (↑M.E : Type u_1)),
      Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' t) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I)
⊢ M.Indep
      (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
        (preimage.{u_1, u_2} (β := β) (⇑f : (a : (↑M.E : Type u_1)) → β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I))) ∧
    ∃ (t : Set (↑M.E : Type u_1)),
      Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' t) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I)

Tactic:
rw [preimage_image_eq _ f.injective]

Premises used: Function.Embedding.injective, Set.preimage_image_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
I : Set (↑M.E : Type u_1)
hI : M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I)
⊢ M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) ∧
    ∃ (t : Set (↑M.E : Type u_1)),
      Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' t) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I)

Tactic:
⟨hI, _, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
I : Set (↑M.E : Type u_1)
hI : M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I)
⊢ M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) ∧
    ∃ (t : Set (↑M.E : Type u_1)),
      Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' t) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I)

Tactic:
exact ⟨hI, _, rfl⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
⊢ f '' M.E = (M.mapSetEmbedding { toFun := M.E.restrict (π := fun (a : α) ↦ β) f, inj' := ⋯ }).E

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
refine :
  ∀ (I : Set β),
    (M.mapSetEmbedding
            { toFun := M.E.restrict (π := fun (a : α) ↦ β) f, inj' := ⋯ :
              Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β }).Indep
        I ↔
      (fun (I : Set β) ↦ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀) I
⊢ ∃ (M_2 : Matroid β),
    f '' M.E = M_2.E ∧ ∀ (I : Set β), M_2.Indep I ↔ (fun (I : Set β) ↦ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀) I

Tactic:
refine ⟨M.mapSetEmbedding ⟨_, hf.injective⟩, by simp, fun I ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
simp_rw : (∃ s ⊆ M.E, M.Indep s ∧ I = f '' s) ↔ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀
⊢ (M.mapSetEmbedding
          { toFun := M.E.restrict (π := fun (a : α) ↦ β) f, inj' := ⋯ :
            Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β }).Indep
      I ↔
    (fun (I : Set β) ↦ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀) I

Tactic:
simp_rw [mapSetEmbedding_indep_iff', Embedding.coeFn_mk, restrict_apply,
      ← image_image f Subtype.val, Subtype.exists_set_subtype (p := fun J ↦ M.Indep J ∧ I = f '' J)]

Premises used: Set.image_image, Set.restrict_apply, Matroid.Indep, Matroid.mapSetEmbedding_indep_iff', Subtype.exists_set_subtype, And, Function.Embedding.coeFn_mk, Set.image, Subtype.val, Eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (∃ s ⊆ M.E, M.Indep s ∧ I = f '' s) ↔ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀

Tactic:
⟨fun ⟨I₀, _, hI₀⟩ ↦ ⟨I₀, hI₀⟩, fun ⟨I₀, hI₀⟩ ↦ ⟨I₀, hI₀.1.subset_ground, hI₀⟩⟩

Premises used: Matroid.E, Exists, Matroid.Indep, HasSubset.Subset, Matroid.Indep.subset_ground, And, And.left, And.intro, Iff.intro, _private.0.Matroid.map.match_2, Exists.intro, Set.image, Eq, _private.0.Matroid.map.match_1
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (∃ s ⊆ M.E, M.Indep s ∧ I = f '' s) ↔ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀

Tactic:
exact ⟨fun ⟨I₀, _, hI₀⟩ ↦ ⟨I₀, hI₀⟩, fun ⟨I₀, hI₀⟩ ↦ ⟨I₀, hI₀.1.subset_ground, hI₀⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).E = f '' M.E

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set β
⊢ (M.map f hf).Indep I ↔ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
hI : M.Indep I
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Indep (f '' I)

Tactic:
map_indep_iff.2 ⟨I, hI, rfl⟩

Premises used: Iff.mpr, Matroid.map_indep_iff, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I : Set β
hf : InjOn f M.E
hI : (M.map f hf).Indep I
obtain : ∀ (I₀ : Set α) (hI₀ : M.Indep I₀), ∃ (I₀_1 : Set α), M.Indep I₀_1 ∧ BijOn f I₀_1 (f '' I₀)
⊢ ∃ (I₀ : Set α), M.Indep I₀ ∧ BijOn f I₀ I

Tactic:
obtain ⟨I₀, hI₀, rfl⟩ := hI

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I₀ : Set α
hI₀ : M.Indep I₀
⊢ ∃ (I₀_1 : Set α), M.Indep I₀_1 ∧ BijOn f I₀_1 (f '' I₀)

Tactic:
⟨I₀, hI₀, (hf.mono hI₀.subset_ground).bijOn_image⟩

Premises used: Set.InjOn.bijOn_image, Matroid.Indep.subset_ground, And.intro, Exists.intro, Set.InjOn.mono
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I₀ : Set α
hI₀ : M.Indep I₀
⊢ ∃ (I₀_1 : Set α), M.Indep I₀_1 ∧ BijOn f I₀_1 (f '' I₀)

Tactic:
exact ⟨I₀, hI₀, (hf.mono hI₀.subset_ground).bijOn_image⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
⊢ (∃ (I₀ : Set α), M.Indep I₀ ∧ f '' I = f '' I₀) ↔ M.Indep I

Tactic:
⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨I, h, rfl⟩⟩

Premises used: Matroid.Indep, _private.0.Matroid.map_image_indep_iff.match_1, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
refine :
  (∃ (I₀ : Set α), M.Indep I₀ ∧ f '' I = f '' I₀) → ∀ (J : Set α) (hJ : M.Indep J) (hIJ : f '' I = f '' J), M.Indep I
⊢ (∃ (I₀ : Set α), M.Indep I₀ ∧ f '' I = f '' I₀) ↔ M.Indep I

Tactic:
refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨I, h, rfl⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
h : ∃ (I₀ : Set α), M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : f '' I = f '' J
⊢ I = J

Tactic:
rw [hf.image_eq_image_iff hI hJ.subset_ground] at hIJ

Premises used: Matroid.Indep.subset_ground, Set.InjOn.image_eq_image_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
h : ∃ (I₀ : Set α), M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : I = J
rwa rwa₁ rwa₂ rwa₃ : M.Indep J
⊢ M.Indep I

Tactic:
rwa [hIJ]
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ Maximal (M.map f hf).Indep B ↔ ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀

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

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
refine_1 : ∀ (h : Maximal (M.map f hf).Indep B), ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀
refine_2 : (∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀) → Maximal (M.map f hf).Indep B
⊢ Maximal (M.map f hf).Indep B ↔ ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
refine_1 : ∀ (B₀ : Set α) (hB₀ : M.Indep B₀) (hbij : BijOn f B₀ B), ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀
⊢ ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀

Tactic:
obtain ⟨B₀, hB₀, hbij⟩ := h.prop.exists_bijOn_of_map

Premises used: Matroid.Indep.exists_bijOn_of_map, Maximal.prop
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
⊢ ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀

Tactic:
⟨B₀, hB₀.isBase_of_maximal fun J hJ hB₀J ↦ ?_, hbij.image_eq.symm⟩

Premises used: Matroid.Indep.isBase_of_maximal, Set.BijOn.image_eq, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
refine_1 : ∀ (J : Set α) (hJ : M.Indep J) (hB₀J : B₀ ⊆ J), B₀ = J
⊢ ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀

Tactic:
refine ⟨B₀, hB₀.isBase_of_maximal fun J hJ hB₀J ↦ ?_, hbij.image_eq.symm⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
refine_1 : B = f '' J
⊢ B₀ = J

Tactic:
rw [← hf.image_eq_image_iff hB₀.subset_ground hJ.subset_ground, hbij.image_eq]

Premises used: Set.BijOn.image_eq, Matroid.Indep.subset_ground, Set.InjOn.image_eq_image_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ B = f '' J

Tactic:
h.eq_of_subset (hJ.map f hf) (hbij.image_eq ▸ image_mono hB₀J)

Premises used: Matroid.Indep.map, Set.image_mono, Eq.rec, Set.BijOn.image_eq, Maximal.eq_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ B = f '' J

Tactic:
exact h.eq_of_subset (hJ.map f hf) (hbij.image_eq ▸ image_mono hB₀J)

Premises used: Matroid.Indep.map, Set.image_mono, Eq.rec, Set.BijOn.image_eq, Maximal.eq_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
refine_2 : (M.map f hf).Indep (f '' B) ∧ ∀ ⦃t : Set β⦄, (M.map f hf).Indep t → f '' B ⊆ t → f '' B = t
⊢ Maximal (M.map f hf).Indep (f '' B)

Tactic:
rw [maximal_subset_iff]

Premises used: maximal_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
⊢ (M.map f hf).Indep (f '' B) ∧ ∀ ⦃t : Set β⦄, (M.map f hf).Indep t → f '' B ⊆ t → f '' B = t

Tactic:
⟨hB.indep.map f hf, fun I hI hBI ↦ ?_⟩

Premises used: Matroid.Indep.map, And.intro, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
refine_2 : ∀ (I : Set β) (hI : (M.map f hf).Indep I) (hBI : f '' B ⊆ I), f '' B = I
⊢ (M.map f hf).Indep (f '' B) ∧ ∀ ⦃t : Set β⦄, (M.map f hf).Indep t → f '' B ⊆ t → f '' B = t

Tactic:
refine ⟨hB.indep.map f hf, fun I hI hBI ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
hBI : f '' B ⊆ I
refine_2 : ∀ (I₀ : Set α) (hI₀ : M.Indep I₀) (hbij : BijOn f I₀ I), f '' B = I
⊢ f '' B = I

Tactic:
obtain ⟨I₀, hI₀, hbij⟩ := hI.exists_bijOn_of_map

Premises used: Matroid.Indep.exists_bijOn_of_map
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
hBI : f '' B ⊆ I
I₀ : Set α
hI₀ : M.Indep I₀
hbij : BijOn f I₀ I
⊢ B ⊆ I₀

Tactic:
rw [← hbij.image_eq, hf.image_subset_image_iff hB.subset_ground hI₀.subset_ground] at hBI

Premises used: Matroid.IsBase.subset_ground, Set.BijOn.image_eq, Matroid.Indep.subset_ground, Set.InjOn.image_subset_image_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
hBI : f '' B ⊆ I
I₀ : Set α
hI₀ : M.Indep I₀
hbij : BijOn f I₀ I
hBI₁ : B ⊆ I₀
⊢ M.Indep I₀

Tactic:
rw [← hbij.image_eq, hf.image_subset_image_iff hB.subset_ground hI₀.subset_ground] at hBI

Premises used: Matroid.IsBase.subset_ground, Set.BijOn.image_eq, Matroid.Indep.subset_ground, Set.InjOn.image_subset_image_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
hBI : f '' B ⊆ I
I₀ : Set α
hI₀ : M.Indep I₀
hbij : BijOn f I₀ I
hBI₁ : B ⊆ I₀
hI₁ : M.Indep I₀
⊢ BijOn f I₀ I

Tactic:
rw [← hbij.image_eq, hf.image_subset_image_iff hB.subset_ground hI₀.subset_ground] at hBI

Premises used: Matroid.IsBase.subset_ground, Set.BijOn.image_eq, Matroid.Indep.subset_ground, Set.InjOn.image_subset_image_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
I₀ : Set α
hBI : B ⊆ I₀
hI₀ : M.Indep I₀
hbij : BijOn f I₀ I
refine_2 : f '' I₀ = I
refine_2₁ refine_2₂ : I = I
⊢ f '' B = I

Tactic:
rw [hB.eq_of_subset_indep hI₀ hBI, hbij.image_eq]

Premises used: Matroid.IsBase.eq_of_subset_indep, Set.BijOn.image_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α → β
hf : InjOn f M.E
rw : ∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀
⊢ (M.map f hf).IsBase (f '' B)

Tactic:
rw [map_isBase_iff]

Premises used: Matroid.map_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α → β
hf : InjOn f M.E
⊢ ∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀

Tactic:
⟨B, hB, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α → β
hf : InjOn f M.E
⊢ ∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀

Tactic:
exact ⟨B, hB, rfl⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D : Set β
simp :
  ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) ↔
    ∃ (D₀ : Set α), (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀
⊢ (M.map f hf).Dep D ↔ ∃ (D₀ : Set α), M.Dep D₀ ∧ D = f '' D₀

Tactic:
simp only [Dep, map_indep_iff, not_exists, not_and, map_ground, subset_image_iff]

Premises used: Matroid.Dep, Matroid.map_ground, not_exists, Set.subset_image_iff, Matroid.map_indep_iff, not_and
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D : Set β
mp :
  ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) →
    ∃ (D₀ : Set α), (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀
mpr :
  (∃ (D₀ : Set α), (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀) →
    (∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D
⊢ ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) ↔
    ∃ (D₀ : Set α), (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀E : D₀ ⊆ M.E
h : ∀ (x : Set α), M.Indep x → ¬f '' D₀ = f '' x
⊢ ∃ (D₀_1 : Set α), (¬M.Indep D₀_1 ∧ D₀_1 ⊆ M.E) ∧ f '' D₀ = f '' D₀_1

Tactic:
⟨D₀, ⟨fun hd ↦ h _ hd rfl, hD₀E⟩, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀E : D₀ ⊆ M.E
h : ∀ (x : Set α), M.Indep x → ¬f '' D₀ = f '' x
⊢ ∃ (D₀_1 : Set α), (¬M.Indep D₀_1 ∧ D₀_1 ⊆ M.E) ∧ f '' D₀ = f '' D₀_1

Tactic:
exact ⟨D₀, ⟨fun hd ↦ h _ hd rfl, hD₀E⟩, rfl⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
⊢ (∀ (x : Set α), M.Indep x → ¬f '' D₀ = f '' x) ∧ ∃ u ⊆ M.E, f '' u = f '' D₀

Tactic:
⟨fun I hI h_eq ↦ ?_, ⟨_, hD₀E, rfl⟩⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
mpr : ∀ (I : Set α) (hI : M.Indep I) (h_eq : f '' D₀ = f '' I), False
⊢ (∀ (x : Set α), M.Indep x → ¬f '' D₀ = f '' x) ∧ ∃ u ⊆ M.E, f '' u = f '' D₀

Tactic:
refine ⟨fun I hI h_eq ↦ ?_, ⟨_, hD₀E, rfl⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : f '' D₀ = f '' I
⊢ D₀ = I

Tactic:
rw [hf.image_eq_image_iff hD₀E hI.subset_ground] at h_eq

Premises used: Matroid.Indep.subset_ground, Set.InjOn.image_eq_image_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : D₀ = I
⊢ M.Indep D₀

Tactic:
subst h_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
hI : M.Indep D₀
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
rw : (∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀) ↔ M.IsBase B
⊢ (M.map f hf).IsBase (f '' B) ↔ M.IsBase B

Tactic:
rw [map_isBase_iff]

Premises used: Matroid.map_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀) ↔ M.IsBase B

Tactic:
⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨B, h, rfl⟩⟩

Premises used: Matroid.IsBase, _private.0.Matroid.map_image_isBase_iff.match_1, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
refine :
  (∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀) → ∀ (J : Set α) (hJ : M.IsBase J) (hIJ : f '' B = f '' J), M.IsBase B
⊢ (∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀) ↔ M.IsBase B

Tactic:
refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨B, h, rfl⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
h : ∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.IsBase J
hIJ : f '' B = f '' J
⊢ B = J

Tactic:
rw [hf.image_eq_image_iff hB hJ.subset_ground] at hIJ

Premises used: Matroid.IsBase.subset_ground, Set.InjOn.image_eq_image_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
h : ∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.IsBase J
hIJ : B = J
rwa rwa₁ rwa₂ rwa₃ : M.IsBase J
⊢ M.IsBase B

Tactic:
rwa [hIJ]
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).IsBasis (f '' I) (f '' X)

Tactic:
(hIX.indep.map f hf).isBasis_of_forall_insert (image_mono hIX.subset) ?_

Premises used: Matroid.Indep.isBasis_of_forall_insert, Matroid.Indep.map, Set.image_mono, Matroid.IsBasis.subset, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
refine : ∀ e ∈ f '' X \ f '' I, (M.map f hf).Dep (insert e (f '' I))
⊢ (M.map f hf).IsBasis (f '' I) (f '' X)

Tactic:
refine (hIX.indep.map f hf).isBasis_of_forall_insert (image_mono hIX.subset) ?_

Premises used: Matroid.Indep.isBasis_of_forall_insert, Matroid.Indep.map, Set.image_mono, Matroid.IsBasis.subset, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
⊢ insert e I ⊆ M.E

Tactic:
have hss := insert_subset (hIX.subset_ground he) hIX.indep.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ insert (f e) (f '' I) ⊆ (M.map f hf).E

Tactic:
simpa [← image_insert_eq] using image_mono hss

Premises used: Set.image_mono, Set.image_insert_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
rw : ¬(M.map f hf).Indep (insert (f e) (f '' I))
⊢ (M.map f hf).Dep (insert (f e) (f '' I))

Tactic:
rw [← not_indep_iff (by simpa [← image_insert_eq] using image_mono hss)]

Premises used: Matroid.not_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
simp : ∀ (x : Set α), M.Indep x → ¬insert (f e) (f '' I) = f '' x
⊢ ¬(M.map f hf).Indep (insert (f e) (f '' I))

Tactic:
simp only [map_indep_iff, not_exists, not_and]

Premises used: not_exists, Matroid.map_indep_iff, not_and
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert (f e) (f '' I) = f '' J
⊢ insert e I = J

Tactic:
rw [← image_insert_eq, hf.image_eq_image_iff hss hJ.subset_ground] at hins

Premises used: Matroid.Indep.subset_ground, Set.InjOn.image_eq_image_iff, Set.image_insert_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert e I = J
⊢ M.Indep (insert e I)

Tactic:
obtain rfl := hins

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
hJ : M.Indep (insert e I)
⊢ False

Tactic:
he' (mem_image_of_mem f (hIX.mem_of_insert_indep he hJ))

Premises used: Set.mem_image_of_mem, Matroid.IsBasis.mem_of_insert_indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
hJ : M.Indep (insert e I)
⊢ False

Tactic:
exact he' (mem_image_of_mem f (hIX.mem_of_insert_indep he hJ))

Premises used: Set.mem_image_of_mem, Matroid.IsBasis.mem_of_insert_indep