awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ (M.mapSetEquiv (E := E) e).E = E

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
⊢ (M.mapEmbedding f).E = (⇑f : (a : α) → β) '' M.E

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
h_1 : M.Indep ((⇑f : (a : α) → β) ⁻¹' I) ∧ I ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
h : M.Indep ((⇑f : (a : α) → β) ⁻¹' I)
h' : I ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
rwa : image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' I) = I
rwa₁ rwa₂ rwa₃ rwa₄ : I ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ I = image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' I)

Tactic:
rwa [eq_comm, image_preimage_eq_iff]

Premises used: eq_comm, Set.image_preimage_eq_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
refine :
  (∃ (I₀ : Set α), M.Indep I₀ ∧ I = (⇑f : (a : α) → β) '' I₀) →
    M.Indep ((⇑f : (a : α) → β) ⁻¹' I) ∧ I ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ (∃ (I₀ : Set α), M.Indep I₀ ∧ I = (⇑f : (a : α) → β) '' I₀) ↔
    M.Indep ((⇑f : (a : α) → β) ⁻¹' I) ∧ I ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
refine ⟨?_, fun ⟨h,h'⟩ ↦ ⟨f ⁻¹' I, h, by rwa [eq_comm, image_preimage_eq_iff]⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set α
hI : M.Indep I
rw : M.Indep I ∧ Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
⊢ M.Indep (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' I)) ∧
    Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))

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 : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep I ∧ Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
⟨hI, image_subset_range _ _⟩

Premises used: Set.image_subset_range, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep I ∧ Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
exact ⟨hI, image_subset_range _ _⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
hI : M.Indep I
f : α ↪ β
⊢ (M.mapEmbedding f).Indep ((⇑f : (a : α) → β) '' I)

Tactic:
simpa [preimage_image_eq I 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 α
B : Set α
hB : M.IsBase B
f : α ↪ β
rw : ∃ (B₀ : Set α), M.IsBase B₀ ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' B) ((⇑f : (a : α) → β) '' B₀)
⊢ (M.mapEmbedding f).IsBase ((⇑f : (a : α) → β) '' B)

Tactic:
rw [Matroid.mapEmbedding, map_isBase_iff]

Premises used: Matroid.mapEmbedding, 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 : α ↪ β
⊢ ∃ (B₀ : Set α), M.IsBase B₀ ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' B) ((⇑f : (a : α) → β) '' 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 : α ↪ β
⊢ ∃ (B₀ : Set α), M.IsBase B₀ ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' B) ((⇑f : (a : α) → β) '' B₀)

Tactic:
exact ⟨B, hB, 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 : α ↪ β
⊢ (M.mapEmbedding f).IsBasis ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' X)

Tactic:
apply hIX.map

Premises used: Matroid.IsBasis.map
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
rw :
  (∃ (B₀ : Set α), M.IsBase B₀ ∧ B = (⇑f : (a : α) → β) '' B₀) ↔
    M.IsBase ((⇑f : (a : α) → β) ⁻¹' B) ∧ B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ (M.mapEmbedding f).IsBase B ↔
    M.IsBase ((⇑f : (a : α) → β) ⁻¹' B) ∧ B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
rw [mapEmbedding, map_isBase_iff]

Premises used: Matroid.mapEmbedding, Matroid.map_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
h_1 : M.IsBase ((⇑f : (a : α) → β) ⁻¹' B) ∧ B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
h : M.IsBase ((⇑f : (a : α) → β) ⁻¹' B)
h' : B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
rwa : image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' B) = B
rwa₁ rwa₂ rwa₃ rwa₄ : B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ B = image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' B)

Tactic:
rwa [eq_comm, image_preimage_eq_iff]

Premises used: eq_comm, Set.image_preimage_eq_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
refine :
  (∃ (B₀ : Set α), M.IsBase B₀ ∧ B = (⇑f : (a : α) → β) '' B₀) →
    M.IsBase ((⇑f : (a : α) → β) ⁻¹' B) ∧ B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ (∃ (B₀ : Set α), M.IsBase B₀ ∧ B = (⇑f : (a : α) → β) '' B₀) ↔
    M.IsBase ((⇑f : (a : α) → β) ⁻¹' B) ∧ B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
refine ⟨?_, fun ⟨h,h'⟩ ↦ ⟨f ⁻¹' B, h, by rwa [eq_comm, image_preimage_eq_iff]⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set α
hB : M.IsBase B
rw : M.IsBase B ∧ Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' B) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
⊢ M.IsBase (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' B)) ∧
    Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' B) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))

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 : α ↪ β
B : Set α
hB : M.IsBase B
⊢ M.IsBase B ∧ Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' B) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
⟨hB, image_subset_range _ _⟩

Premises used: Set.image_subset_range, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set α
hB : M.IsBase B
⊢ M.IsBase B ∧ Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' B) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
exact ⟨hB, image_subset_range _ _⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
rw :
  (∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀) ↔
    M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X) ∧
      I ⊆ X ∧ X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ (M.mapEmbedding f).IsBasis I X ↔
    M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X) ∧
      I ⊆ X ∧ X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
rw [mapEmbedding, map_isBasis_iff']

Premises used: Matroid.mapEmbedding, Matroid.map_isBasis_iff'
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
⊢ (∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀) ↔
    M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X) ∧
      I ⊆ X ∧ X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
⟨?_, fun ⟨hb, hIX, hX⟩ ↦ ?_⟩

Premises used: Exists, _private.0.Matroid.mapEmbedding_isBasis_iff.match_1, And, Iff.intro, Set.image, Matroid.IsBasis, Eq, DFunLike.coe
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
refine_1 :
  (∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀) →
    M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X) ∧
      I ⊆ X ∧ X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
refine_2 :
  M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X) ∧
      I ⊆ X ∧ X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) →
    ∀ (hb : M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X)) (hIX : I ⊆ X)
      (hX : X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)),
      ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀
⊢ (∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀) ↔
    M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X) ∧
      I ⊆ X ∧ X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
refine ⟨?_, fun ⟨hb, hIX, hX⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set α
hIX : M.IsBasis I X
⊢ M.IsBasis (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' I))
      (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)) ∧
    Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' X) ∧
      Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
simp [preimage_image_eq _ f.injective, image_mono hIX.subset, hIX]

Premises used: Set.image_mono, Matroid.IsBasis.subset, Function.Embedding.injective, Set.preimage_image_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
h :
  M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X) ∧
    I ⊆ X ∧ X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
hb : M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X)
hIX : I ⊆ X
hX : X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
refine_2 :
  ∀ (X : Set α),
    M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)) ∧
        I ⊆ (⇑f : (a : α) → β) '' X ∧
          Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) →
      ∀
        (hb :
          M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I)
            (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)))
        (hIX : I ⊆ (⇑f : (a : α) → β) '' X)
        (hX : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))),
        ∃ (I₀ : Set α) (X₀ : Set α),
          M.IsBasis I₀ X₀ ∧
            I = (⇑f : (a : α) → β) '' I₀ ∧
              Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' X) ((⇑f : (a : α) → β) '' X₀)
⊢ ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀

Tactic:
obtain ⟨X, rfl⟩ := subset_range_iff_exists_image_eq.1 hX

Premises used: Set.subset_range_iff_exists_image_eq, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
X : Set α
h :
  M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)) ∧
    I ⊆ (⇑f : (a : α) → β) '' X ∧
      Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
hb : M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X))
hIX : I ⊆ (⇑f : (a : α) → β) '' X
hX : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
refine_2 :
  ∀ (I : Set α),
    M.IsBasis (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' I))
          (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)) ∧
        Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' X) ∧
          Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) →
      ∀
        (hb :
          M.IsBasis (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' I))
            (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)))
        (hIX : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' X)),
        ∃ (I₀ : Set α) (X₀ : Set α),
          M.IsBasis I₀ X₀ ∧
            Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' I₀) ∧
              Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' X) ((⇑f : (a : α) → β) '' X₀)
⊢ ∃ (I₀ : Set α) (X₀ : Set α),
    M.IsBasis I₀ X₀ ∧
      I = (⇑f : (a : α) → β) '' I₀ ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' X) ((⇑f : (a : α) → β) '' X₀)

Tactic:
obtain ⟨I, -, rfl⟩ := subset_image_iff.1 hIX

Premises used: Set.subset_image_iff, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
X : Set α
hX : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
I : Set α
h :
  M.IsBasis (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' I))
      (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)) ∧
    Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' X) ∧
      Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
hb :
  M.IsBasis (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' I))
    (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X))
hIX : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' X)
⊢ M.IsBasis I X ∧
    Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' I) ∧
      Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' X) ((⇑f : (a : α) → β) '' X)

Tactic:
simpa [preimage_image_eq _ f.injective] using hb

Premises used: Function.Embedding.injective, Set.preimage_image_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
X : Set α
hX : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
I : Set α
h :
  M.IsBasis (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' I))
      (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)) ∧
    Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' X) ∧
      Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
hb :
  M.IsBasis (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' I))
    (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X))
hIX : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' X)
⊢ ∃ (I₀ : Set α) (X₀ : Set α),
    M.IsBasis I₀ X₀ ∧
      Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' I₀) ∧
        Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' X) ((⇑f : (a : α) → β) '' X₀)

Tactic:
exact ⟨I, X, by simpa [preimage_image_eq _ f.injective] using hb⟩
-- 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 : α ↪ β
⊢ (M.mapEmbedding f).Nonempty

Tactic:
inferInstanceAs (M.map f f.injective.injOn).Nonempty

Premises used: _private.0.Matroid.instNonemptyMapEmbedding._proof_1
-- 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 : α ↪ β
⊢ (M.mapEmbedding f).Finite

Tactic:
inferInstanceAs (M.map f f.injective.injOn).Finite

Premises used: _private.0.Matroid.instFiniteMapEmbedding._proof_1
-- 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 : α ↪ β
⊢ (M.mapEmbedding f).Finitary

Tactic:
inferInstanceAs (M.map f f.injective.injOn).Finitary

Premises used: _private.0.Matroid.instFinitaryMapEmbedding._proof_1
-- 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 : α ↪ β
⊢ (M.mapEmbedding f).RankFinite

Tactic:
inferInstanceAs (M.map f f.injective.injOn).RankFinite

Premises used: _private.0.Matroid.instRankFiniteMapEmbedding._proof_1
-- 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 : α ↪ β
⊢ (M.mapEmbedding f).RankPos

Tactic:
inferInstanceAs (M.map f f.injective.injOn).RankPos

Premises used: _private.0.Matroid.instRankPosMapEmbedding._proof_1
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
⊢ (M.mapEquiv f).E = (⇑f : (a : α) → β) '' M.E

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
⊢ M.mapEquiv f = M.map (⇑f : (a : α) → β) ⋯

Tactic:
rfl

Premises used: Matroid.mapEmbedding, Matroid.mapEquiv, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
rw : (∃ (I₀ : Set α), M.Indep I₀ ∧ I = (⇑f : (a : α) → β) '' I₀) ↔ M.Indep ((⇑f.symm : (a : β) → α) '' I)
⊢ (M.mapEquiv f).Indep I ↔ M.Indep ((⇑f.symm : (a : β) → α) '' I)

Tactic:
rw [mapEquiv_eq_map, map_indep_iff]

Premises used: Matroid.map_indep_iff, Matroid.mapEquiv_eq_map
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.Indep I
⊢ M.Indep (image.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) ((⇑f : (a : α) → β) '' I))

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
h : M.Indep ((⇑f.symm : (a : β) → α) '' I)
⊢ I = image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f.symm : (a : β) → α) '' I)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
⊢ (∃ (I₀ : Set α), M.Indep I₀ ∧ I = (⇑f : (a : α) → β) '' I₀) ↔ M.Indep ((⇑f.symm : (a : β) → α) '' I)

Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
rw : (∃ (D₀ : Set α), M.Dep D₀ ∧ D = (⇑f : (a : α) → β) '' D₀) ↔ M.Dep ((⇑f.symm : (a : β) → α) '' D)
⊢ (M.mapEquiv f).Dep D ↔ M.Dep ((⇑f.symm : (a : β) → α) '' D)

Tactic:
rw [mapEquiv_eq_map, map_dep_iff]

Premises used: Matroid.map_dep_iff, Matroid.mapEquiv_eq_map
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.Dep I
⊢ M.Dep (image.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) ((⇑f : (a : α) → β) '' I))

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
h : M.Dep ((⇑f.symm : (a : β) → α) '' D)
⊢ D = image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f.symm : (a : β) → α) '' D)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
⊢ (∃ (D₀ : Set α), M.Dep D₀ ∧ D = (⇑f : (a : α) → β) '' D₀) ↔ M.Dep ((⇑f.symm : (a : β) → α) '' D)

Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
rw : (∃ (B₀ : Set α), M.IsBase B₀ ∧ B = (⇑f : (a : α) → β) '' B₀) ↔ M.IsBase ((⇑f.symm : (a : β) → α) '' B)
⊢ (M.mapEquiv f).IsBase B ↔ M.IsBase ((⇑f.symm : (a : β) → α) '' B)

Tactic:
rw [mapEquiv_eq_map, map_isBase_iff]

Premises used: Matroid.map_isBase_iff, Matroid.mapEquiv_eq_map
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.IsBase I
⊢ M.IsBase (image.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) ((⇑f : (a : α) → β) '' I))

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
h : M.IsBase ((⇑f.symm : (a : β) → α) '' B)
⊢ B = image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f.symm : (a : β) → α) '' B)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
⊢ (∃ (B₀ : Set α), M.IsBase B₀ ∧ B = (⇑f : (a : α) → β) '' B₀) ↔ M.IsBase ((⇑f.symm : (a : β) → α) '' B)

Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
rw :
  (∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀) ↔
    M.IsBasis ((⇑f.symm : (a : β) → α) '' I) ((⇑f.symm : (a : β) → α) '' X)
⊢ (M.mapEquiv f).IsBasis I X ↔ M.IsBasis ((⇑f.symm : (a : β) → α) '' I) ((⇑f.symm : (a : β) → α) '' X)

Tactic:
rw [mapEquiv_eq_map, map_isBasis_iff']

Premises used: Matroid.map_isBasis_iff', Matroid.mapEquiv_eq_map
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
h : M.IsBasis ((⇑f.symm : (a : β) → α) '' I) ((⇑f.symm : (a : β) → α) '' X)
⊢ I = image.{u_3, u_4} (α := α) (⇑f : (a : α) → β) ((⇑f.symm : (a : β) → α) '' I)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
h : M.IsBasis ((⇑f.symm : (a : β) → α) '' I) ((⇑f.symm : (a : β) → α) '' X)
⊢ X = image.{u_3, u_4} (α := α) (⇑f : (a : α) → β) ((⇑f.symm : (a : β) → α) '' X)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
refine :
  ∀ (h : ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀),
    M.IsBasis ((⇑f.symm : (a : β) → α) '' I) ((⇑f.symm : (a : β) → α) '' X)
⊢ (∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀) ↔
    M.IsBasis ((⇑f.symm : (a : β) → α) '' I) ((⇑f.symm : (a : β) → α) '' X)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨_, _, h, by simp, by simp⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
h : ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀
obtain :
  ∀ (I X : Set α) (hIX : M.IsBasis I X),
    M.IsBasis (image.{u_4, u_3} (α := β) (⇑f.symm : (a : β) → α) ((⇑f : (a : α) → β) '' I))
      (image.{u_4, u_3} (α := β) (⇑f.symm : (a : β) → α) ((⇑f : (a : α) → β) '' X))
⊢ M.IsBasis ((⇑f.symm : (a : β) → α) '' I) ((⇑f.symm : (a : β) → α) '' X)

Tactic:
obtain ⟨I, X, hIX, rfl, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set α
hIX : M.IsBasis I X
⊢ M.IsBasis (image.{u_4, u_3} (α := β) (⇑f.symm : (a : β) → α) ((⇑f : (a : α) → β) '' I))
    (image.{u_4, u_3} (α := β) (⇑f.symm : (a : β) → α) ((⇑f : (a : α) → β) '' X))

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
f_2 : α ≃ β
inst : M.Nonempty
f : α ≃ β
⊢ (M.mapEquiv f).Nonempty

Tactic:
inferInstanceAs (M.map f f.injective.injOn).Nonempty

Premises used: _private.0.Matroid.instNonemptyMapEquiv._proof_1
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
f_2 : α ≃ β
inst : M.Finite
f : α ≃ β
⊢ (M.mapEquiv f).Finite

Tactic:
inferInstanceAs (M.map f f.injective.injOn).Finite

Premises used: _private.0.Matroid.instFiniteMapEquiv._proof_1