awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
e : α
hfe : f e ∉ f '' B
hi : N.Indep (f '' insert e B) ∧ f '' insert e B ⊆ range f
⊢ InjOn f B ∧ f e ∉ f '' B

Tactic:
⟨hBmax.1.2, hfe⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
e : α
hfe : f e ∉ f '' B
hi : N.Indep (f '' insert e B) ∧ f '' insert e B ⊆ range f
⊢ InjOn f B ∧ f e ∉ f '' B

Tactic:
exact ⟨hBmax.1.2, hfe⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
e : α
hfe : f e ∉ f '' B
hi : N.Indep (f '' insert e B) ∧ f '' insert e B ⊆ range f
⊢ InjOn f (insert e B)

Tactic:
have hinj : InjOn f (insert e B) := by
          rw [injOn_insert (fun heB ↦ hfe (mem_image_of_mem f heB))]
          exact ⟨hBmax.1.2, hfe⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
e : α
hfe : f e ∉ f '' B
hi : N.Indep (f '' insert e B) ∧ f '' insert e B ⊆ range f
hinj : InjOn f (insert e B)
⊢ False

Tactic:
hBmax.not_prop_of_ssuperset (t := insert e B) (ssubset_insert ?_) ⟨hi.1, hinj⟩

Premises used: Set.ssubset_insert, And.left, And.intro, Maximal.not_prop_of_ssuperset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
e : α
hfe : f e ∉ f '' B
hi : N.Indep (f '' insert e B) ∧ f '' insert e B ⊆ range f
hinj : InjOn f (insert e B)
refine : e ∉ B
⊢ False

Tactic:
refine hBmax.not_prop_of_ssuperset (t := insert e B) (ssubset_insert ?_) ⟨hi.1, hinj⟩

Premises used: Set.ssubset_insert, And.left, And.intro, Maximal.not_prop_of_ssuperset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
e : α
hfe : f e ∉ f '' B
hi : N.Indep (f '' insert e B) ∧ f '' insert e B ⊆ range f
hinj : InjOn f (insert e B)
⊢ e ∉ B

Tactic:
fun heB ↦ hfe <| mem_image_of_mem f heB

Premises used: Set.mem_image_of_mem, Not
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
e : α
hfe : f e ∉ f '' B
hi : N.Indep (f '' insert e B) ∧ f '' insert e B ⊆ range f
hinj : InjOn f (insert e B)
⊢ e ∉ B

Tactic:
exact fun heB ↦ hfe <| mem_image_of_mem f heB

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
⊢ (N ↾ range f).IsBase (f '' B)

Tactic:
have h₂ : (N ↾ range f).IsBase (f '' B) := by
        refine Indep.isBase_of_forall_insert (by simpa using hBmax.1.1) ?_
        rintro _ ⟨⟨e, heB, rfl⟩, hfe⟩ hi
        rw [restrict_indep_iff, ← image_insert_eq] at hi
        have hinj : InjOn f (insert e B) := by
          rw [injOn_insert (fun heB ↦ hfe (mem_image_of_mem f heB))]
          exact ⟨hBmax.1.2, hfe⟩
        refine hBmax.not_prop_of_ssuperset (t := insert e B) (ssubset_insert ?_) ⟨hi.1, hinj⟩
        exact fun heB ↦ hfe <| mem_image_of_mem f heB
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
⊢ (N ↾ range f).Indep (f '' I)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
obtain :
  ∀ (e : α) (he : e ∈ B) (hei : (N ↾ range f).Indep (insert (f e) (f '' I))) (he' : f e ∉ f '' I),
    ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)

Tactic:
obtain ⟨_, ⟨⟨e, he, rfl⟩, he'⟩, hei⟩ := Indep.exists_insert_of_not_isBase (by simpa) h₁ h₂

Premises used: Matroid.Indep.exists_insert_of_not_isBase, rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
e : α
he : e ∈ B
hei : (N ↾ range f).Indep (insert (f e) (f '' I))
he' : f e ∉ f '' I
⊢ e ∉ I

Tactic:
have heI : e ∉ I := fun heI ↦ he' (mem_image_of_mem f heI)
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
e : α
he : e ∈ B
hei : (N ↾ range f).Indep (insert (f e) (f '' I))
he' : f e ∉ f '' I
heI : e ∉ I
⊢ N.Indep (f '' insert e I) ∧ f '' insert e I ⊆ range f

Tactic:
rw [← image_insert_eq, restrict_indep_iff] at hei

Premises used: Matroid.restrict_indep_iff, Set.image_insert_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
e : α
he : e ∈ B
hei : (N ↾ range f).Indep (insert (f e) (f '' I))
he' : f e ∉ f '' I
heI : e ∉ I
hei₁ : N.Indep (f '' insert e I) ∧ f '' insert e I ⊆ range f
⊢ f e ∉ f '' I

Tactic:
rw [← image_insert_eq, restrict_indep_iff] at hei

Premises used: Matroid.restrict_indep_iff, Set.image_insert_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
e : α
he : e ∈ B
hei : (N ↾ range f).Indep (insert (f e) (f '' I))
he' : f e ∉ f '' I
heI : e ∉ I
hei₁ : N.Indep (f '' insert e I) ∧ f '' insert e I ⊆ range f
he'₁ : f e ∉ f '' I
⊢ e ∉ I

Tactic:
rw [← image_insert_eq, restrict_indep_iff] at hei

Premises used: Matroid.restrict_indep_iff, Set.image_insert_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
e : α
he : e ∈ B
hei : N.Indep (f '' insert e I) ∧ f '' insert e I ⊆ range f
he' : f e ∉ f '' I
heI : e ∉ I
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)

Tactic:
⟨e, ⟨he, heI⟩, hei.1, (injOn_insert heI).2 ⟨hIinj, he'⟩⟩

Premises used: Iff.mpr, Set.injOn_insert, And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
e : α
he : e ∈ B
hei : N.Indep (f '' insert e I) ∧ f '' insert e I ⊆ range f
he' : f e ∉ f '' I
heI : e ∉ I
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)

Tactic:
exact ⟨e, ⟨he, heI⟩, hei.1, (injOn_insert heI).2 ⟨hIinj, he'⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
⊢ f '' X ⊆ (N ↾ range f).E

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
⊢ (N ↾ range f).Indep (f '' I)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
obtain :
  ∀ (J : Set β) (hJ : f '' I ⊆ J ∧ Maximal (fun (K : Set β) ↦ (N ↾ range f).Indep K ∧ K ⊆ f '' X) J),
    ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) K ∧ K ⊆ X) J
⊢ ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) K ∧ K ⊆ X) J

Tactic:
obtain ⟨J, hJ⟩ := (N ↾ range f).existsMaximalSubsetProperty_indep (f '' X) (by simp)
        (f '' I) (by simpa) (image_mono hIX)

Premises used: Set.image_mono, Set.image, Set.range, Matroid.restrict, Matroid.existsMaximalSubsetProperty_indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hJ : f '' I ⊆ J ∧ Maximal (fun (K : Set β) ↦ (N ↾ range f).Indep K ∧ K ⊆ f '' X) J
simp :
  ∀
    (hJ :
      I ⊆ f ⁻¹' J ∧
        N.Indep J ∧ J ⊆ range f ∧ J ⊆ f '' X ∧ ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t),
    ∃ (J : Set α),
      I ⊆ J ∧ N.Indep (f '' J) ∧ InjOn f J ∧ J ⊆ X ∧ ∀ ⦃t : Set α⦄, N.Indep (f '' t) → InjOn f t → t ⊆ X → J ⊆ t → J = t
⊢ ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) K ∧ K ⊆ X) J

Tactic:
simp only [restrict_indep_iff, image_subset_iff, maximal_subset_iff, and_imp,
        and_assoc] at hJ ⊢

Premises used: and_imp, maximal_subset_iff, and_assoc, Matroid.restrict_indep_iff, Set.image_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hJ :
  I ⊆ f ⁻¹' J ∧
    N.Indep J ∧ J ⊆ range f ∧ J ⊆ f '' X ∧ ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
⊢ I ⊆ f ⁻¹' J

Tactic:
obtain ⟨hIJ, hJ, hJf, hJX, hJmax⟩ := hJ
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hJ :
  I ⊆ f ⁻¹' J ∧
    N.Indep J ∧ J ⊆ range f ∧ J ⊆ f '' X ∧ ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
hIJ : I ⊆ f ⁻¹' J
⊢ N.Indep J

Tactic:
obtain ⟨hIJ, hJ, hJf, hJX, hJmax⟩ := hJ
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hJ :
  I ⊆ f ⁻¹' J ∧
    N.Indep J ∧ J ⊆ range f ∧ J ⊆ f '' X ∧ ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
hIJ : I ⊆ f ⁻¹' J
hJ₁ : N.Indep J
⊢ J ⊆ range f

Tactic:
obtain ⟨hIJ, hJ, hJf, hJX, hJmax⟩ := hJ
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hJ :
  I ⊆ f ⁻¹' J ∧
    N.Indep J ∧ J ⊆ range f ∧ J ⊆ f '' X ∧ ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
hIJ : I ⊆ f ⁻¹' J
hJ₁ : N.Indep J
hJf : J ⊆ range f
⊢ J ⊆ f '' X

Tactic:
obtain ⟨hIJ, hJ, hJf, hJX, hJmax⟩ := hJ
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hJ :
  I ⊆ f ⁻¹' J ∧
    N.Indep J ∧ J ⊆ range f ∧ J ⊆ f '' X ∧ ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
hIJ : I ⊆ f ⁻¹' J
hJ₁ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
⊢ ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t

Tactic:
obtain ⟨hIJ, hJ, hJf, hJX, hJmax⟩ := hJ
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
obtain :
  ∀ (J₀ : Set α) (hIJ₀ : I ⊆ J₀) (hJ₀X : J₀ ⊆ X) (hbj : BijOn f J₀ (f '' f ⁻¹' J)),
    ∃ (J : Set α),
      I ⊆ J ∧ N.Indep (f '' J) ∧ InjOn f J ∧ J ⊆ X ∧ ∀ ⦃t : Set α⦄, N.Indep (f '' t) → InjOn f t → t ⊆ X → J ⊆ t → J = t
⊢ ∃ (J : Set α),
    I ⊆ J ∧ N.Indep (f '' J) ∧ InjOn f J ∧ J ⊆ X ∧ ∀ ⦃t : Set α⦄, N.Indep (f '' t) → InjOn f t → t ⊆ X → J ⊆ t → J = t

Tactic:
obtain ⟨J₀, hIJ₀, hJ₀X, hbj⟩ := hIinj.bijOn_image.exists_extend_of_subset hIX
        (image_mono hIJ) (image_subset_iff.2 <| preimage_mono hJX)

Premises used: Iff.mpr, Set.image_mono, Set.InjOn.bijOn_image, Set.preimage_mono, Set.BijOn.exists_extend_of_subset, Set.image_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hbj : BijOn f J₀ (f '' f ⁻¹' J)
rw : f '' J₀ = f '' f ⁻¹' J
rw₁ rw₂ : f '' f ⁻¹' J = f '' f ⁻¹' J
⊢ f '' J₀ = J

Tactic:
rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]

Premises used: Set.BijOn.image_eq, Set.image_preimage_eq_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hbj : BijOn f J₀ (f '' f ⁻¹' J)
⊢ I ⊆ f ⁻¹' f '' J₀

Tactic:
obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hbj : BijOn f J₀ (f '' f ⁻¹' J)
hIJ₁ : I ⊆ f ⁻¹' f '' J₀
⊢ N.Indep (f '' J₀)

Tactic:
obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hbj : BijOn f J₀ (f '' f ⁻¹' J)
hIJ₁ : I ⊆ f ⁻¹' f '' J₀
hJ₁ : N.Indep (f '' J₀)
⊢ f '' J₀ ⊆ range f

Tactic:
obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hbj : BijOn f J₀ (f '' f ⁻¹' J)
hIJ₁ : I ⊆ f ⁻¹' f '' J₀
hJ₁ : N.Indep (f '' J₀)
hJf₁ : f '' J₀ ⊆ range f
⊢ f '' J₀ ⊆ f '' X

Tactic:
obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hbj : BijOn f J₀ (f '' f ⁻¹' J)
hIJ₁ : I ⊆ f ⁻¹' f '' J₀
hJ₁ : N.Indep (f '' J₀)
hJf₁ : f '' J₀ ⊆ range f
hJX₁ : f '' J₀ ⊆ f '' X
⊢ ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → f '' J₀ ⊆ t → f '' J₀ = t

Tactic:
obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hbj : BijOn f J₀ (f '' f ⁻¹' J)
hIJ₁ : I ⊆ f ⁻¹' f '' J₀
hJ₁ : N.Indep (f '' J₀)
hJf₁ : f '' J₀ ⊆ range f
hJX₁ : f '' J₀ ⊆ f '' X
hJmax₁ : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → f '' J₀ ⊆ t → f '' J₀ = t
⊢ BijOn f J₀ (f '' f ⁻¹' f '' J₀)

Tactic:
obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hIJ : I ⊆ f ⁻¹' f '' J₀
hJ : N.Indep (f '' J₀)
hJf : f '' J₀ ⊆ range f
hJX : f '' J₀ ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → f '' J₀ ⊆ t → f '' J₀ = t
hbj : BijOn f J₀ (f '' f ⁻¹' f '' J₀)
⊢ ∃ (J : Set α),
    I ⊆ J ∧ N.Indep (f '' J) ∧ InjOn f J ∧ J ⊆ X ∧ ∀ ⦃t : Set α⦄, N.Indep (f '' t) → InjOn f t → t ⊆ X → J ⊆ t → J = t

Tactic:
⟨J₀, hIJ₀, hJ, hbj.injOn, hJ₀X, fun K hK hKinj hKX hJ₀K ↦ ?_⟩

Premises used: Set.BijOn.injOn, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hIJ : I ⊆ f ⁻¹' f '' J₀
hJ : N.Indep (f '' J₀)
hJf : f '' J₀ ⊆ range f
hJX : f '' J₀ ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → f '' J₀ ⊆ t → f '' J₀ = t
hbj : BijOn f J₀ (f '' f ⁻¹' f '' J₀)
refine : ∀ (K : Set α) (hK : N.Indep (f '' K)) (hKinj : InjOn f K) (hKX : K ⊆ X) (hJ₀K : J₀ ⊆ K), J₀ = K
⊢ ∃ (J : Set α),
    I ⊆ J ∧ N.Indep (f '' J) ∧ InjOn f J ∧ J ⊆ X ∧ ∀ ⦃t : Set α⦄, N.Indep (f '' t) → InjOn f t → t ⊆ X → J ⊆ t → J = t

Tactic:
refine ⟨J₀, hIJ₀, hJ, hbj.injOn, hJ₀X, fun K hK hKinj hKX hJ₀K ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hIJ : I ⊆ f ⁻¹' f '' J₀
hJ : N.Indep (f '' J₀)
hJf : f '' J₀ ⊆ range f
hJX : f '' J₀ ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → f '' J₀ ⊆ t → f '' J₀ = t
hbj : BijOn f J₀ (f '' f ⁻¹' f '' J₀)
K : Set α
hK : N.Indep (f '' K)
hKinj : InjOn f K
hKX : K ⊆ X
hJ₀K : J₀ ⊆ K
rw : f '' J₀ = f '' K
rw₁ rw₂ : f '' K = f '' K
⊢ J₀ = K

Tactic:
rw [← hKinj.image_eq_image_iff hJ₀K Subset.rfl, hJmax hK (image_subset_range _ _)
        (image_mono hKX) (image_mono hJ₀K)]

Premises used: Set.image_mono, Set.image_subset_range, Set.Subset.rfl, Set.InjOn.image_eq_image_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ (N.comap f).Indep I ↔ N.Indep (f '' I) ∧ InjOn f I

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
⊢ (N.comap f).E = f ⁻¹' N.E

Tactic:
rfl

Premises used: setOf, Set.preimage, rfl