awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
rw : (N.comap f ↾ E).IsBase B ↔ N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E
rw₁ : (N.comap f).IsBasis' B E ↔ N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E
rw₂ rw₃ : N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E ↔ N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E
⊢ (N.comapOn E f).IsBase B ↔ N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E

Tactic:
rw [comapOn, isBase_restrict_iff', comap_isBasis'_iff]

Premises used: Matroid.comap_isBasis'_iff, Matroid.isBase_restrict_iff', Matroid.comapOn
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
simp_rw : N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E
simp_rw₁ : InjOn f B ∧ B ⊆ E → (N.IsBasis' (f '' B) (f '' E) ↔ N.IsBase (f '' B))
simp_rw₂ : InjOn f B → B ⊆ E → (N.IsBasis' (f '' B) (f '' E) ↔ N.IsBase (f '' B))
simp_rw₃ : InjOn f B → B ⊆ E → (N.IsBasis (f '' B) (f '' E ∩ N.E) ↔ N.IsBase (f '' B))
simp_rw₄ : InjOn f B → B ⊆ E → (N.IsBasis (f '' B) N.E ↔ N.IsBase (f '' B))
simp_rw₅ : InjOn f B → B ⊆ E → True
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E

Tactic:
simp_rw [comapOn_isBase_iff, and_congr_left_iff, and_imp, isBasis'_iff_isBasis_inter_ground,
    inter_eq_self_of_subset_right h, isBasis_ground_iff, implies_true]

Premises used: and_imp, Matroid.isBasis_ground_iff, Matroid.comapOn_isBase_iff, Matroid.isBasis'_iff_isBasis_inter_ground, and_congr_left_iff, Set.inter_eq_self_of_subset_right, implies_true
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
rw : B ⊆ E → ((N.comapOn E f).IsBase B ↔ N.IsBase (f '' B))
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ B ⊆ E

Tactic:
rw [← and_iff_left_of_imp (IsBase.subset_ground (M := N.comapOn E f) (B := B)),
    comapOn_ground_eq, and_congr_left_iff]

Premises used: and_iff_left_of_imp, Matroid.comapOn_ground_eq, Matroid.IsBase.subset_ground, and_congr_left_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
h' : B ⊆ E → InjOn f B
hB : B ⊆ E
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B)

Tactic:
simp [hB, comapOn_isBase_iff_of_surjOn h.surjOn, h']

Premises used: Matroid.comapOn_isBase_iff_of_surjOn, Set.BijOn.surjOn
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
suffices : B ⊆ E → InjOn f B
⊢ B ⊆ E → ((N.comapOn E f).IsBase B ↔ N.IsBase (f '' B))

Tactic:
suffices h' : B ⊆ E → InjOn f B from fun hB ↦
    by simp [hB, comapOn_isBase_iff_of_surjOn h.surjOn, h']
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ B ⊆ E → InjOn f B

Tactic:
fun hBE ↦ h.injOn.mono hBE

Premises used: Set.BijOn.injOn, Set.InjOn.mono
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ B ⊆ E → InjOn f B

Tactic:
exact fun hBE ↦ h.injOn.mono hBE

Premises used: Set.BijOn.injOn, Set.InjOn.mono
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f)✶.E = (N✶.comapOn E f).E

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
refine : ∀ (B : Set α) (hB : B ⊆ (N.comapOn E f)✶.E), (N.comapOn E f)✶.IsBase B ↔ (N✶.comapOn E f).IsBase B
⊢ (N.comapOn E f)✶ = N✶.comapOn E f

Tactic:
refine ext_isBase (by simp) (fun B hB ↦ ?_)

Premises used: Matroid.ext_isBase
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ BijOn f E N✶.E

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ B ⊆ E

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
rw : f '' B ⊆ N.E
⊢ (N.comapOn E f)✶.IsBase B ↔ (N✶.comapOn E f).IsBase B

Tactic:
rw [comapOn_isBase_iff_of_bijOn (by simpa), dual_isBase_iff, comapOn_isBase_iff_of_bijOn h,
    dual_isBase_iff _, comapOn_ground_eq, and_iff_left diff_subset, and_iff_left (by simpa),
    h.injOn.image_diff_subset (by simpa), h.image_eq]

Premises used: Set.diff_subset, and_iff_left, Matroid.comapOn_ground_eq, Matroid.dual_isBase_iff, Matroid.comapOn_isBase_iff_of_bijOn, Set.BijOn.image_eq, Set.BijOn.injOn, Set.InjOn.image_diff_subset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ f '' B ⊆ N.E

Tactic:
exact (h.mapsTo.mono_left (show B ⊆ E by simpa)).image_subset

Premises used: Set.MapsTo.mono_left, Set.BijOn.mapsTo, Set.MapsTo.image_subset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M : Matroid α
N : Matroid β
E B I : Set α
inst : N.Finitary
⊢ (N.comap f ↾ E).Finitary

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M : Matroid α
N : Matroid β
E B I : Set α
inst : N.RankFinite
⊢ (N.comap f ↾ E).RankFinite

Tactic:
infer_instance
-- 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 : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
inl :
  ∀ (f : Embedding.{u_1 + 1, u_2 + 1} (↑(emptyOn α).E : Type u_1) β),
    ∃ (M : Matroid β),
      range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1)) (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) = M.E ∧
        ∀ (I : Set β),
          M.Indep I ↔
            (fun (I : Set β) ↦
                (emptyOn α).Indep
                    (image (α := { x : α // x ∈ (emptyOn α).E }) (Subtype.val (p := fun (x : α) ↦ x ∈ (emptyOn α).E))
                      ((⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) ⁻¹' I)) ∧
                  I ⊆
                    range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1))
                      (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β))
              I
inr :
  ∀ (e : α) (he : e ∈ M.E),
    ∃ (M_2 : Matroid β),
      range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β) = M_2.E ∧
        ∀ (I : Set β),
          M_2.Indep I ↔
            (fun (I : Set β) ↦
                M.Indep
                    (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                      ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
                  I ⊆ range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β))
              I
⊢ ∃ (M_2 : Matroid β),
    range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β) = M_2.E ∧
      ∀ (I : Set β),
        M_2.Indep I ↔
          (fun (I : Set β) ↦
              M.Indep
                  (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                    ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
                I ⊆ range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β))
            I

Tactic:
obtain (rfl | ⟨⟨e, he⟩⟩) := eq_emptyOn_or_nonempty M

Premises used: Matroid.eq_emptyOn_or_nonempty, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
f : Embedding.{u_1 + 1, u_2 + 1} (↑(emptyOn α).E : Type u_1) β
⊢ ∃ (M : Matroid β),
    range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1)) (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) = M.E ∧
      ∀ (I : Set β),
        M.Indep I ↔
          (fun (I : Set β) ↦
              (emptyOn α).Indep
                  (image (α := { x : α // x ∈ (emptyOn α).E }) (Subtype.val (p := fun (x : α) ↦ x ∈ (emptyOn α).E))
                    ((⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) ⁻¹' I)) ∧
                I ⊆
                  range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1)) (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β))
            I

Tactic:
⟨emptyOn β, ?_⟩

Premises used: Matroid.emptyOn, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
f : Embedding.{u_1 + 1, u_2 + 1} (↑(emptyOn α).E : Type u_1) β
inl :
  range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1)) (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) = (emptyOn β).E ∧
    ∀ (I : Set β),
      (emptyOn β).Indep I ↔
        (fun (I : Set β) ↦
            (emptyOn α).Indep
                (image (α := { x : α // x ∈ (emptyOn α).E }) (Subtype.val (p := fun (x : α) ↦ x ∈ (emptyOn α).E))
                  ((⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) ⁻¹' I)) ∧
              I ⊆ range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1)) (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β))
          I
⊢ ∃ (M : Matroid β),
    range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1)) (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) = M.E ∧
      ∀ (I : Set β),
        M.Indep I ↔
          (fun (I : Set β) ↦
              (emptyOn α).Indep
                  (image (α := { x : α // x ∈ (emptyOn α).E }) (Subtype.val (p := fun (x : α) ↦ x ∈ (emptyOn α).E))
                    ((⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) ⁻¹' I)) ∧
                I ⊆
                  range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1)) (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β))
            I

Tactic:
refine ⟨emptyOn β, ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
f : Embedding.{u_1 + 1, u_2 + 1} (↑∅ : Type u_1) β
⊢ range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1)) (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) = (emptyOn β).E ∧
    ∀ (I : Set β),
      (emptyOn β).Indep I ↔
        (fun (I : Set β) ↦
            (emptyOn α).Indep
                (image (α := { x : α // x ∈ (emptyOn α).E }) (Subtype.val (p := fun (x : α) ↦ x ∈ (emptyOn α).E))
                  ((⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) ⁻¹' I)) ∧
              I ⊆ range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1)) (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β))
          I

Tactic:
simp [range_eq_empty f, subset_empty_iff]

Premises used: Set.subset_empty_iff, Set.range_eq_empty, DFunLike.coe
-- 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 : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
e : α
he : e ∈ M.E
⊢ Nonempty.{u_1 + 1} (↑M.E : Type u_1)

Tactic:
have _ : Nonempty M.E := ⟨⟨e,he⟩⟩
-- 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 : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
⊢ Nonempty α

Tactic:
have _ : Nonempty α := ⟨e⟩
-- 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 : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
h_1 : Nonempty α
⊢ ∃ (M_2 : Matroid β),
    range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β) = M_2.E ∧
      ∀ (I : Set β),
        M_2.Indep I ↔
          (fun (I : Set β) ↦
              M.Indep
                  (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                    ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
                I ⊆ range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β))
            I

Tactic:
⟨M.comapOn (range f) (fun x ↦ ↑(invFunOn f univ x)), rfl, ?_⟩

Premises used: Function.invFunOn, Matroid.comapOn, Set.univ, And.intro, Exists.intro, Set.range, Subtype.val, DFunLike.coe, 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 : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
h_1 : Nonempty α
inr :
  ∀ (I : Set β),
    Indep
        (M.comapOn (range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β)) fun (x : β) ↦
          (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α))
        I ↔
      (fun (I : Set β) ↦
          M.Indep
              (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
            I ⊆ range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β))
        I
⊢ ∃ (M_2 : Matroid β),
    range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β) = M_2.E ∧
      ∀ (I : Set β),
        M_2.Indep I ↔
          (fun (I : Set β) ↦
              M.Indep
                  (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                    ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
                I ⊆ range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β))
            I

Tactic:
refine ⟨M.comapOn (range f) (fun x ↦ ↑(invFunOn f univ x)), 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 : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
h_1 : Nonempty α
inr :
  ∀ (I : Set β),
    (∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I) →
      (M.Indep ((fun (x : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α)) '' I) ∧
          InjOn.{u_2, u_1} (β := α) (fun (x : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α)) I ↔
        M.Indep
          (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
            ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)))
⊢ ∀ (I : Set β),
    Indep
        (M.comapOn (range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β)) fun (x : β) ↦
          (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α))
        I ↔
      (fun (I : Set β) ↦
          M.Indep
              (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
            I ⊆ range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β))
        I

Tactic:
simp_rw [comapOn_indep_iff, ← and_assoc, and_congr_left_iff, subset_range_iff_exists_image_eq]

Premises used: Matroid.comapOn_indep_iff, Set.subset_range_iff_exists_image_eq, and_congr_left_iff, and_assoc
-- 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 : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
h_1 : Nonempty α
I : Set (↑M.E : Type u_1)
inr :
  M.Indep ↑I →
    InjOn.{u_2, u_1} (β := α) (fun (x : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α))
      ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I)
⊢ M.Indep
        ((fun (x : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α)) ''
          (⇑f : (a : (↑M.E : Type u_1)) → β) '' I) ∧
      InjOn.{u_2, u_1} (β := α) (fun (x : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α))
        ((⇑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)))

Tactic:
rw [← image_image, InjOn.invFunOn_image f.injective.injOn (subset_univ _),
      preimage_image_eq _ f.injective, and_iff_left_iff_imp]

Premises used: Set.image_image, Function.Injective.injOn, Set.subset_univ, Set.InjOn.invFunOn_image, Function.Embedding.injective, Set.preimage_image_eq, and_iff_left_iff_imp
-- 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 : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
h_1 : Nonempty α
I : Set (↑M.E : Type u_1)
x : β
hx : Membership.mem (γ := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) x
y : β
hy : Membership.mem (γ := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) y
inr :
  Eq.{max 1 (u_1 + 1)} (α := { x : α // x ∈ M.E }) (invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x)
      (invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ y) →
    x = y
⊢ Eq.{u_1 + 1} (α := α) ((fun (x : β) ↦ ((↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α) : α)) x)
      ((fun (x : β) ↦ ((↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α) : α)) y) →
    x = y

Tactic:
simp only [Subtype.val_inj]

Premises used: Subtype.val_inj
-- 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 : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
h_1 : Nonempty α
I : Set (↑M.E : Type u_1)
x : β
hx : Membership.mem (γ := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) x
y : β
hy : Membership.mem (γ := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) y
⊢ Eq.{max 1 (u_1 + 1)} (α := { x : α // x ∈ M.E }) (invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x)
      (invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ y) →
    x = y

Tactic:
(invFunOn_injOn_image f univ) (image_mono (subset_univ I) hx)
      (image_mono (subset_univ I) hy)

Premises used: Set.subset_univ, Set.univ, Set.image_mono, Function.invFunOn_injOn_image, DFunLike.coe
-- 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 : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
h_1 : Nonempty α
I : Set (↑M.E : Type u_1)
x : β
hx : Membership.mem (γ := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) x
y : β
hy : Membership.mem (γ := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) y
⊢ Eq.{max 1 (u_1 + 1)} (α := { x : α // x ∈ M.E }) (invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x)
      (invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ y) →
    x = y

Tactic:
exact (invFunOn_injOn_image f univ) (image_mono (subset_univ I) hx)
      (image_mono (subset_univ I) hy)

Premises used: Set.subset_univ, Set.univ, Set.image_mono, Function.invFunOn_injOn_image, DFunLike.coe
-- 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) β
⊢ (M.mapSetEmbedding f).E = range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β)

Tactic:
rfl

Premises used: setOf, Set.range, 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.mapSetEmbedding f).Indep I ↔
    M.Indep
        (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
          ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
      I ⊆ range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β)

Tactic:
Iff.rfl

Premises used: Iff.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 β
hI : (M.mapSetEmbedding f).Indep I
⊢ ∃ (I₀ : Set (↑M.E : Type u_1)),
    M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀

Tactic:
⟨f ⁻¹' I, hI.1, Eq.symm <| image_preimage_eq_of_subset hI.2⟩

Premises used: And.right, Set.preimage, And.left, Set.image_preimage_eq_of_subset, And.intro, Exists.intro, Eq.symm, DFunLike.coe
-- 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 β
simp :
  (M.Indep
        (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
          ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
      ∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I) ↔
    ∃ (I₀ : Set (↑M.E : Type u_1)),
      M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀
⊢ (M.mapSetEmbedding f).Indep I ↔
    ∃ (I₀ : Set (↑M.E : Type u_1)),
      M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀

Tactic:
simp only [mapSetEmbedding_indep_iff, subset_range_iff_exists_image_eq]

Premises used: Set.subset_range_iff_exists_image_eq, Matroid.mapSetEmbedding_indep_iff
-- 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 β
mp :
  (M.Indep
        (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
          ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
      ∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I) →
    ∃ (I₀ : Set (↑M.E : Type u_1)),
      M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀
mpr :
  (∃ (I₀ : Set (↑M.E : Type u_1)),
      M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀) →
    M.Indep
        (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
          ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
      ∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I
⊢ (M.Indep
        (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
          ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
      ∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I) ↔
    ∃ (I₀ : Set (↑M.E : Type u_1)),
      M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀

Tactic:
constructor
-- 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
    (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)))
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hI : M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I)),
    M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I)
⊢ M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I)

Tactic:
rwa [preimage_image_eq _ f.injective] at hI

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
    (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)))
⊢ ∃ (I₀ : Set (↑M.E : Type u_1)),
    M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧
      Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀)

Tactic:
exact ⟨I, by rwa [preimage_image_eq _ f.injective] at hI, rfl⟩