awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
⊢ (M.map f hf).IsBasis (f '' I) (f '' X) ↔ M.IsBasis I X

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.map hf⟩

Premises used: Matroid.IsBasis.map, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
refine : ∀ (h : (M.map f hf).IsBasis (f '' I) (f '' X)), M.IsBasis I X
⊢ (M.map f hf).IsBasis (f '' I) (f '' X) ↔ M.IsBasis I X

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.map hf⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
obtain : ∀ (I' : Set α) (hI' : M.Indep I') (hII' : f '' I = f '' I'), M.IsBasis I X
⊢ M.IsBasis I X

Tactic:
obtain ⟨I', hI', hII'⟩ := map_indep_iff.1 h.indep

Premises used: Matroid.map_indep_iff, Iff.mp, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : f '' I = f '' I'
⊢ I = I'

Tactic:
rw [hf.image_eq_image_iff hI hI'.subset_ground] at hII'

Premises used: Matroid.Indep.subset_ground, Set.InjOn.image_eq_image_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : I = I'
⊢ M.Indep I

Tactic:
obtain rfl := hII'

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

Tactic:
have hss := (hf.image_subset_image_iff hI hX).1 h.subset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
⊢ M.IsBasis I X

Tactic:
hI'.isBasis_of_maximal_subset hss (fun J hJ hIJ hJX ↦ ?_)

Premises used: Matroid.Indep.isBasis_of_maximal_subset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
refine : ∀ (J : Set α) (hJ : M.Indep J) (hIJ : I ⊆ J) (hJX : J ⊆ X), J ⊆ I
⊢ M.IsBasis I X

Tactic:
refine hI'.isBasis_of_maximal_subset hss (fun J hJ hIJ hJX ↦ ?_)

Premises used: Matroid.Indep.isBasis_of_maximal_subset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ f '' I = f '' J

Tactic:
have hIJ' := h.eq_of_subset_indep (hJ.map f hf) (image_mono hIJ) (image_mono hJX)
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
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
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
hIJ' : I = J
⊢ J ⊆ I

Tactic:
hIJ'.symm.subset

Premises used: Eq.subset, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
hIJ' : I = J
⊢ J ⊆ I

Tactic:
exact hIJ'.symm.subset

Premises used: Eq.subset, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
⊢ (M.map f hf).IsBasis I X ↔ ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀

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

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

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

Tactic:
obtain ⟨I, hI, rfl⟩ := subset_image_iff.1 h.indep.subset_ground

Premises used: Set.subset_image_iff, Matroid.Indep.subset_ground, Iff.mp, Matroid.IsBasis.indep, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
X : Set β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) X
refine_1 :
  ∀ (X : Set α) (hX : X ⊆ M.E) (h : (M.map f hf).IsBasis (f '' I) (f '' X)),
    ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ f '' X = f '' X₀
⊢ ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ X = f '' X₀

Tactic:
obtain ⟨X, hX, rfl⟩ := subset_image_iff.1 h.subset_ground

Premises used: Matroid.IsBasis.subset_ground, Set.subset_image_iff, Iff.mp, 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
X : Set α
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ M.IsBasis I X

Tactic:
rw [map_isBasis_iff _ _ hI hX] at h

Premises used: Matroid.map_isBasis_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
X : Set α
hX : X ⊆ M.E
h : M.IsBasis I X
⊢ ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ f '' X = f '' X₀

Tactic:
⟨I, X, h, rfl, 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
I : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : M.IsBasis I X
⊢ ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ f '' X = f '' X₀

Tactic:
exact ⟨I, X, h, rfl, rfl⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
⊢ (M.map f hf).IsBasis (f '' I) (f '' X)

Tactic:
hIX.map hf

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

Tactic:
exact hIX.map hf

Premises used: Matroid.IsBasis.map
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ (M.map f hf)✶.E = (M✶.map f hf).E

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
apply : ∀ ⦃B : Set β⦄, B ⊆ (M.map f hf)✶.E → ((M.map f hf)✶.IsBase B ↔ (M✶.map f hf).IsBase B)
⊢ (M.map f hf)✶ = M✶.map f hf

Tactic:
apply ext_isBase (by simp)

Premises used: Matroid.ext_isBase
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
simp : ∀ a ⊆ M.E, ((M.map f hf).IsBase (f '' M.E \ f '' a) ∧ ∃ u ⊆ M.E, f '' u = f '' a) ↔ (M✶.map f hf).IsBase (f '' a)
⊢ ∀ ⦃B : Set β⦄, B ⊆ (M.map f hf)✶.E → ((M.map f hf)✶.IsBase B ↔ (M✶.map f hf).IsBase B)

Tactic:
simp only [dual_ground, map_ground, subset_image_iff, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, dual_isBase_iff']

Premises used: Matroid.dual_isBase_iff', Matroid.map_ground, and_imp, forall_exists_index, Set.subset_image_iff, Matroid.dual_ground, forall_apply_eq_imp_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
simp_rw : M.IsBase (M.E \ B) → ∃ u ⊆ M.E, f '' u = f '' B
⊢ ((M.map f hf).IsBase (f '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).IsBase (f '' B)

Tactic:
simp_rw [← hf.image_diff_subset hB, map_image_isBase_iff diff_subset,
    map_image_isBase_iff (show B ⊆ M✶.E from hB), dual_isBase_iff hB, and_iff_left_iff_imp]

Premises used: Set.diff_subset, Matroid.map_image_isBase_iff, Matroid.dual_isBase_iff, Set.InjOn.image_diff_subset, and_iff_left_iff_imp
-- 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
⊢ M.IsBase (M.E \ B) → ∃ u ⊆ M.E, f '' u = f '' B

Tactic:
fun _ ↦ ⟨B, hB, 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
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) → ∃ u ⊆ M.E, f '' u = f '' B

Tactic:
exact fun _ ↦ ⟨B, hB, rfl⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
f : α → β
⊢ InjOn f (emptyOn α).E

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ (emptyOn α).map f ⋯ = emptyOn β

Tactic:
simp [← ground_eq_empty_iff]

Premises used: Matroid.ground_eq_empty_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (loopyOn E).E
⊢ (loopyOn E).map f hf = loopyOn (f '' E)

Tactic:
simp [eq_loopyOn_iff]

Premises used: Matroid.eq_loopyOn_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (freeOn E).E
rw : ((freeOn E).map f hf)✶ = (freeOn (f '' E))✶
⊢ (freeOn E).map f hf = freeOn (f '' E)

Tactic:
rw [← dual_inj]

Premises used: Matroid.dual_inj
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (freeOn E).E
⊢ ((freeOn E).map f hf)✶ = (freeOn (f '' E))✶

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
⊢ M.map id ⋯ = M

Tactic:
simp [ext_iff_indep]

Premises used: Matroid.ext_iff_indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ ((N.comap f).map f hf).E = N.E

Tactic:
simpa [image_preimage_eq_iff]

Premises used: Set.image_preimage_eq_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
refine : ∀ ⦃I : Set β⦄, I ⊆ ((N.comap f).map f hf).E → (((N.comap f).map f hf).Indep I ↔ N.Indep I)
⊢ (N.comap f).map f hf = N

Tactic:
refine ext_indep (by simpa [image_preimage_eq_iff]) ?_

Premises used: Matroid.ext_indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
simp : ∀ t ⊆ f ⁻¹' N.E, (∃ (I₀ : Set α), (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' t = f '' I₀) ↔ N.Indep (f '' t)
⊢ ∀ ⦃I : Set β⦄, I ⊆ ((N.comap f).map f hf).E → (((N.comap f).map f hf).Indep I ↔ N.Indep I)

Tactic:
simp only [map_ground, comap_ground_eq, map_indep_iff, comap_indep_iff, forall_subset_image_iff]

Premises used: Matroid.map_ground, Matroid.comap_indep_iff, Set.forall_subset_image_iff, Matroid.map_indep_iff, Matroid.comap_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
I : Set α
hI : I ⊆ f ⁻¹' N.E
⊢ (∃ (I₀ : Set α), (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' I = f '' I₀) → N.Indep (f '' I)

Tactic:
grind
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ ∀ t ⊆ f ⁻¹' N.E, (∃ (I₀ : Set α), (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' t = f '' I₀) ↔ N.Indep (f '' t)

Tactic:
exact fun I hI ↦ ⟨by grind, fun h ↦ ⟨_, ⟨h, hf.mono hI⟩, rfl⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : Injective f
⊢ (M.map f ⋯).comap f = M

Tactic:
simp [ext_iff_indep, preimage_image_eq _ hf, and_iff_left hf.injOn,
    image_eq_image hf]

Premises used: Function.Injective.injOn, and_iff_left, Set.image_eq_image, Set.preimage_image_eq, Matroid.ext_iff_indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst : M.Nonempty
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).E.Nonempty

Tactic:
simp [M.ground_nonempty]

Premises used: Matroid.ground_nonempty
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst : M.Finite
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Finite

Tactic:
⟨M.ground_finite.image f⟩

Premises used: Set.Finite.image, Matroid.Finite.mk, Matroid.ground_finite
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Finitary

Tactic:
⟨fun I hI ↦ ?_⟩

Premises used: Matroid.Finitary.mk
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
refine : ∀ (I : Set β) (hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J), (M.map f hf).Indep I
⊢ (M.map f hf).Finitary

Tactic:
refine ⟨fun I hI ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
e : β
he : e ∈ I
⊢ {e} ⊆ I

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
e : β
he : e ∈ I
⊢ Set.Finite (α := β) {e}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
e : β
he : e ∈ I
obtain : ∀ (I₀ : Set α) (hI₀ : M.Indep I₀) (h_eq : {e} = f '' I₀), e ∈ f '' M.E
⊢ e ∈ f '' M.E

Tactic:
obtain ⟨I₀, hI₀, h_eq⟩ := hI {e} (by simpa) (by simp)

Premises used: Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
e : β
he : e ∈ I
I₀ : Set α
hI₀ : M.Indep I₀
h_eq : {e} = f '' I₀
⊢ e ∈ f '' M.E

Tactic:
image_mono hI₀.subset_ground <| h_eq.subset rfl

Premises used: Set.image_mono, Eq.subset, Matroid.Indep.subset_ground, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
e : β
he : e ∈ I
I₀ : Set α
hI₀ : M.Indep I₀
h_eq : {e} = f '' I₀
⊢ e ∈ f '' M.E

Tactic:
exact image_mono hI₀.subset_ground <| h_eq.subset rfl

Premises used: Set.image_mono, Eq.subset, Matroid.Indep.subset_ground, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
⊢ I ⊆ f '' M.E

Tactic:
have h' : I ⊆ f '' M.E := by
    intro e he
    obtain ⟨I₀, hI₀, h_eq⟩ := hI {e} (by simpa) (by simp)
    exact image_mono hI₀.subset_ground <| h_eq.subset rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
h' : I ⊆ f '' M.E
obtain :
  ∀ (I₀ : Set α) (hI₀E : I₀ ⊆ M.E) (hI : ∀ J ⊆ f '' I₀, J.Finite → (M.map f hf).Indep J) (h' : f '' I₀ ⊆ f '' M.E),
    ∃ (I₀_1 : Set α), M.Indep I₀_1 ∧ f '' I₀ = f '' I₀_1
⊢ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀

Tactic:
obtain ⟨I₀, hI₀E, rfl⟩ := subset_image_iff.1 h'

Premises used: Set.subset_image_iff, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I₀ : Set α
hI₀E : I₀ ⊆ M.E
hI : ∀ J ⊆ f '' I₀, J.Finite → (M.map f hf).Indep J
h' : f '' I₀ ⊆ f '' M.E
⊢ ∃ (I₀_1 : Set α), M.Indep I₀_1 ∧ f '' I₀ = f '' I₀_1

Tactic:
⟨I₀, indep_of_forall_finite_subset_indep _ fun J₀ hJ₀I₀ hJ₀ ↦ ?_, rfl⟩

Premises used: Matroid.indep_of_forall_finite_subset_indep, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I₀ : Set α
hI₀E : I₀ ⊆ M.E
hI : ∀ J ⊆ f '' I₀, J.Finite → (M.map f hf).Indep J
h' : f '' I₀ ⊆ f '' M.E
refine : ∀ (J₀ : Set α) (hJ₀I₀ : J₀ ⊆ I₀) (hJ₀ : J₀.Finite), M.Indep J₀
⊢ ∃ (I₀_1 : Set α), M.Indep I₀_1 ∧ f '' I₀ = f '' I₀_1

Tactic:
refine ⟨I₀, indep_of_forall_finite_subset_indep _ fun J₀ hJ₀I₀ hJ₀ ↦ ?_, rfl⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I₀ : Set α
hI₀E : I₀ ⊆ M.E
hI : ∀ J ⊆ f '' I₀, J.Finite → (M.map f hf).Indep J
h' : f '' I₀ ⊆ f '' M.E
J₀ : Set α
hJ₀I₀ : J₀ ⊆ I₀
hJ₀ : J₀.Finite
⊢ (M.map f hf).Indep (f '' J₀)

Tactic:
specialize hI (f '' J₀) (image_mono hJ₀I₀) (hJ₀.image _)

Premises used: Set.image_mono, Set.Finite.image, Set.image
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I₀ : Set α
hI₀E : I₀ ⊆ M.E
h' : f '' I₀ ⊆ f '' M.E
J₀ : Set α
hJ₀I₀ : J₀ ⊆ I₀
hJ₀ : J₀.Finite
hI : (M.map f hf).Indep (f '' J₀)
rwa rwa₁ rwa₂ rwa₃ : ∀ (hI : M.Indep J₀), M.Indep J₀
⊢ M.Indep J₀

Tactic:
rwa [map_image_indep_iff (hJ₀I₀.trans hI₀E)] at hI

Premises used: HasSubset.Subset.trans, Matroid.map_image_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst : M.RankFinite
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).RankFinite

Tactic:
let ⟨_, hB⟩ := M.exists_isBase
  (hB.map hf).rankFinite_of_finite (hB.finite.image _)

Premises used: Matroid.IsBase.map, Matroid.IsBase.rankFinite_of_finite, Set.Finite.image, Matroid.exists_isBase, _private.0.Matroid.instRankFiniteMap.match_1, Matroid.RankFinite, Matroid.map, Matroid.IsBase.finite
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst : M.RankPos
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).RankPos

Tactic:
let ⟨_, hB⟩ := M.exists_isBase
  (hB.map hf).rankPos_of_nonempty (hB.nonempty.image _)

Premises used: Matroid.IsBase.rankPos_of_nonempty, Matroid.IsBase.map, Matroid.IsBase.nonempty, Matroid.RankPos, Set.Nonempty.image, Matroid.exists_isBase, _private.0.Matroid.instRankFiniteMap.match_1, Matroid.map
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
E : Set β
e : Equiv.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) (↑E : Type u_2)
I : Set β
h :
  ∀ (x : (↑M.E : Type u_1)),
    Membership.mem (γ := Set (↑M.E : Type u_1))
        (comp (β := { x : β // x ∈ E }) (Subtype.val (p := fun (x : β) ↦ x ∈ E))
            (⇑e : (a : (↑M.E : Type u_1)) → (↑E : Type u_2)) ⁻¹'
          I)
        x ↔
      Membership.mem (γ := Set (↑M.E : Type u_1))
        (image (α := (↑E : Type u_2)) (⇑e.symm : (a : (↑E : Type u_2)) → (↑M.E : Type u_1)) (E ↓∩ I)) x
⊢ Eq.{u_1 + 1} (α := Set (↑M.E : Type u_1))
    (comp (β := { x : β // x ∈ E }) (Subtype.val (p := fun (x : β) ↦ x ∈ E))
        (⇑e : (a : (↑M.E : Type u_1)) → (↑E : Type u_2)) ⁻¹'
      I)
    (image (α := (↑E : Type u_2)) (⇑e.symm : (a : (↑E : Type u_2)) → (↑M.E : Type u_1)) (E ↓∩ I))

Tactic:
ext
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
E : Set β
e : Equiv.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) (↑E : Type u_2)
I : Set β
x : (↑M.E : Type u_1)
⊢ Membership.mem (γ := Set (↑M.E : Type u_1))
      (comp (β := { x : β // x ∈ E }) (Subtype.val (p := fun (x : β) ↦ x ∈ E))
          (⇑e : (a : (↑M.E : Type u_1)) → (↑E : Type u_2)) ⁻¹'
        I)
      x ↔
    Membership.mem (γ := Set (↑M.E : Type u_1))
      (image (α := (↑E : Type u_2)) (⇑e.symm : (a : (↑E : Type u_2)) → (↑M.E : Type u_1)) (E ↓∩ I)) x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
E : Set β
e : Equiv.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) (↑E : Type u_2)
⊢ ∀ (I : Set β),
    Eq.{u_1 + 1} (α := Set (↑M.E : Type u_1))
      (comp (β := { x : β // x ∈ E }) (Subtype.val (p := fun (x : β) ↦ x ∈ E))
          (⇑e : (a : (↑M.E : Type u_1)) → (↑E : Type u_2)) ⁻¹'
        I)
      (image (α := (↑E : Type u_2)) (⇑e.symm : (a : (↑E : Type u_2)) → (↑M.E : Type u_1)) (E ↓∩ I))

Tactic:
have hrw : ∀ I : Set β, Subtype.val ∘ ⇑e ⁻¹' I = ⇑e.symm '' E ↓∩ I := fun I ↦ by ext; simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
E : Set β
e : Equiv.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) (↑E : Type u_2)
hrw :
  ∀ (I : Set β),
    Eq.{u_1 + 1} (α := Set (↑M.E : Type u_1))
      (comp (β := { x : β // x ∈ E }) (Subtype.val (p := fun (x : β) ↦ x ∈ E))
          (⇑e : (a : (↑M.E : Type u_1)) → (↑E : Type u_2)) ⁻¹'
        I)
      (image (α := (↑E : Type u_2)) (⇑e.symm : (a : (↑E : Type u_2)) → (↑M.E : Type u_1)) (E ↓∩ I))
⊢ E = (M.mapSetEmbedding (e.toEmbedding.trans (Embedding.subtype fun (x : β) ↦ x ∈ E))).E ∧
    ∀ (I : Set β),
      (M.mapSetEmbedding (e.toEmbedding.trans (Embedding.subtype fun (x : β) ↦ x ∈ E))).Indep I ↔
        (fun (I : Set β) ↦
            M.Indep
                (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                  (image (α := (↑E : Type u_2)) (⇑e.symm : (a : (↑E : Type u_2)) → (↑M.E : Type u_1)) (E ↓∩ I))) ∧
              I ⊆ E)
          I

Tactic:
simp [Equiv.toEmbedding, Embedding.subtype, Embedding.trans, hrw]

Premises used: Equiv.toEmbedding, Function.Embedding.trans, Function.Embedding.subtype
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
E : Set β
e : Equiv.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) (↑E : Type u_2)
I : Set β
⊢ (M.mapSetEquiv (E := E) e).Indep I ↔
    M.Indep
        (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
          (image (α := (↑E : Type u_2)) (⇑e.symm : (a : (↑E : Type u_2)) → (↑M.E : Type u_1)) (E ↓∩ I))) ∧
      I ⊆ E

Tactic:
Iff.rfl

Premises used: Iff.rfl