awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
rw : (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E ↔ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I
⊢ (N.comap f).Dep I ↔ N.Dep (f '' I) ∨ N.Indep (f '' I) ∧ ¬InjOn f I

Tactic:
rw [Dep, comap_indep_iff, not_and, comap_ground_eq, Dep, image_subset_iff]

Premises used: Matroid.Dep, Matroid.comap_indep_iff, Matroid.comap_ground_eq, Set.image_subset_iff, not_and
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E → ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I

Tactic:
grind
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
refine :
  ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I → (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E ↔ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I

Tactic:
refine ⟨by grind, ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : ¬N.Indep (f '' I)
hIE : I ⊆ f ⁻¹' N.E
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

Tactic:
⟨fun h ↦ (hI h).elim, hIE⟩

Premises used: False.elim, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : ¬N.Indep (f '' I)
hIE : I ⊆ f ⁻¹' N.E
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

Tactic:
exact ⟨fun h ↦ (hI h).elim, hIE⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
inr : I ⊆ f ⁻¹' N.E
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

Tactic:
rw [iff_true_intro hI.1, iff_true_intro hI.2, implies_true, true_and]

Premises used: And.right, And.left, iff_true_intro, implies_true, true_and
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ I ⊆ f ⁻¹' N.E

Tactic:
simpa using hI.1.subset_ground

Premises used: Matroid.Indep.subset_ground, And.left
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
β : Type u_2
N : Matroid β
⊢ ∀ ⦃I : Set β⦄, I ⊆ (N.comap id).E → ((N.comap id).Indep I ↔ N.Indep I)

Tactic:
simp [injective_id.injOn]

Premises used: Function.Injective.injOn, Function.injective_id
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
rw : N.Indep (f '' I) → InjOn f I
⊢ (N.comap f).Indep I ↔ N.Indep (f '' I)

Tactic:
rw [comap_indep_iff, and_iff_left_iff_imp]

Premises used: Matroid.comap_indep_iff, and_iff_left_iff_imp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ N.Indep (f '' I) → InjOn f I

Tactic:
fun hi ↦ hf.mono <| subset_trans ?_ (preimage_mono hi.subset_ground)

Premises used: subset_trans, Matroid.Indep.subset_ground, Set.preimage_mono, Set.InjOn.mono
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
refine : ∀ (hi : N.Indep (f '' I)), I ⊆ f ⁻¹' f '' I
⊢ N.Indep (f '' I) → InjOn f I

Tactic:
refine fun hi ↦ hf.mono <| subset_trans ?_ (preimage_mono hi.subset_ground)

Premises used: subset_trans, Set.preimage_mono, Set.InjOn.mono
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
hi : N.Indep (f '' I)
⊢ I ⊆ f ⁻¹' f '' I

Tactic:
apply subset_preimage_image

Premises used: Set.subset_preimage_image
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ (emptyOn β).comap 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
f : α → β
E : Set β
rw : ((loopyOn E).comap f).E = f ⁻¹' E ∧ ∀ X ⊆ ((loopyOn E).comap f).E, ((loopyOn E).comap f).Indep X → X = ∅
⊢ (loopyOn E).comap f = loopyOn (f ⁻¹' E)

Tactic:
rw [eq_loopyOn_iff]

Premises used: Matroid.eq_loopyOn_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E : Set β
⊢ ((loopyOn E).comap f).E = f ⁻¹' E ∧ ∀ X ⊆ ((loopyOn E).comap f).E, ((loopyOn E).comap f).Indep X → X = ∅

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
⊢ (N.comap f).IsBasis I X ↔ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X

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

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
refine_1 : ∀ (h : (N.comap f).IsBasis I X), N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
refine_2 : ∀ (h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X), (N.comap f).IsBasis I X
⊢ (N.comap f).IsBasis I X ↔ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
⊢ N.Indep (f '' I)

Tactic:
obtain ⟨hI, hinj⟩ := comap_indep_iff.1 h.indep

Premises used: Matroid.comap_indep_iff, Iff.mp, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
hI : N.Indep (f '' I)
⊢ InjOn f I

Tactic:
obtain ⟨hI, hinj⟩ := comap_indep_iff.1 h.indep

Premises used: Matroid.comap_indep_iff, Iff.mp, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
⊢ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X

Tactic:
⟨hI.isBasis_of_forall_insert (image_mono h.subset) fun e he ↦ ?_, hinj, h.subset⟩

Premises used: Matroid.Indep.isBasis_of_forall_insert, Set.image_mono, Matroid.IsBasis.subset, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
refine_1 : ∀ (e : β) (he : e ∈ f '' X \ f '' I), N.Dep (insert e (f '' I))
⊢ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X

Tactic:
refine ⟨hI.isBasis_of_forall_insert (image_mono h.subset) fun e he ↦ ?_, hinj, h.subset⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : β
he : e ∈ f '' X \ f '' I
⊢ (∃ x ∈ X, f x = e) ∧ ∀ x ∈ I, ¬f x = e

Tactic:
simp only [mem_diff, mem_image, not_exists, not_and] at he

Premises used: Set.mem_image, not_exists, Set.mem_diff, not_and
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : β
he : (∃ x ∈ X, f x = e) ∧ ∀ x ∈ I, ¬f x = e
refine_1 : ∀ (e : α) (heX : e ∈ X) (he : ∀ x ∈ I, ¬f x = f e), N.Dep (insert (f e) (f '' I))
⊢ N.Dep (insert e (f '' I))

Tactic:
obtain ⟨⟨e, heX, rfl⟩, he⟩ := he

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
⊢ e ∉ I

Tactic:
have heI : e ∉ I := fun heI ↦ (he e heI rfl)
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
⊢ (N.comap f).Dep (insert e I)

Tactic:
replace h := h.insert_dep ⟨heX, heI⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
h : (N.comap f).Dep (insert e I)
⊢ (N.Indep (insert (f e) (f '' I)) → ∀ x ∈ I, ¬f x = f e) → N.Dep (insert (f e) (f '' I))

Tactic:
simp only [comap_dep_iff, image_insert_eq, or_iff_not_imp_right, injOn_insert heI,
      hinj, mem_image, not_exists, not_and, true_and, not_forall, not_not] at h

Premises used: Classical.or_iff_not_imp_right, Classical.not_not, Set.mem_image, not_exists, Matroid.comap_dep_iff, Set.injOn_insert, Set.image_insert_eq, not_and, Classical.not_forall, true_and
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
h : (N.Indep (insert (f e) (f '' I)) → ∀ x ∈ I, ¬f x = f e) → N.Dep (insert (f e) (f '' I))
⊢ N.Dep (insert (f e) (f '' I))

Tactic:
h (fun _ ↦ he)
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
h : (N.Indep (insert (f e) (f '' I)) → ∀ x ∈ I, ¬f x = f e) → N.Dep (insert (f e) (f '' I))
⊢ N.Dep (insert (f e) (f '' I))

Tactic:
exact h (fun _ ↦ he)
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
⊢ (N.comap f).IsBasis I X

Tactic:
Indep.isBasis_of_forall_insert ?_ h.2.2 fun e ⟨heX, heI⟩ ↦ ?_

Premises used: Matroid.Indep.isBasis_of_forall_insert, Matroid.Dep, Insert.insert, _private.0.Matroid.comap_isBasis_iff.match_7, And.right, Matroid.comap
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
refine_2 : (N.comap f).Indep I
refine_2₁ : ∀ e ∈ X \ I, ∀ (heX : e ∈ X) (heI : e ∉ I), (N.comap f).Dep (insert e I)
⊢ (N.comap f).IsBasis I X

Tactic:
refine Indep.isBasis_of_forall_insert ?_ h.2.2 fun e ⟨heX, heI⟩ ↦ ?_

Premises used: Matroid.Indep.isBasis_of_forall_insert, Matroid.Dep, Insert.insert, _private.0.Matroid.comap_isBasis_iff.match_7, And.right
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
⊢ (N.comap f).Indep I

Tactic:
simp [comap_indep_iff, h.1.indep, h.2]

Premises used: Matroid.comap_indep_iff, And.right, And.left, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
h_1 : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
simp_rw : f '' insert e I ⊆ N.E
⊢ insert e I ⊆ (N.comap f).E

Tactic:
simp_rw [comap_ground_eq, ← image_subset_iff]

Premises used: Matroid.comap_ground_eq, Set.image_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
h_1 : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ f '' insert e I ⊆ N.E

Tactic:
(image_mono (insert_subset heX h.2.2)).trans h.1.subset_ground

Premises used: Matroid.IsBasis.subset_ground, Set.image_mono, HasSubset.Subset.trans, And.right, And.left, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
h_1 : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ f '' insert e I ⊆ N.E

Tactic:
exact (image_mono (insert_subset heX h.2.2)).trans h.1.subset_ground

Premises used: Matroid.IsBasis.subset_ground, Set.image_mono, HasSubset.Subset.trans, And.right, And.left, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
h_1 : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ insert e I ⊆ (N.comap f).E

Tactic:
have hIE : insert e I ⊆ (N.comap f).E := by
      simp_rw [comap_ground_eq, ← image_subset_iff]
      exact (image_mono (insert_subset heX h.2.2)).trans h.1.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
h_1 : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
this : N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
⊢ (N.comap f).Dep (insert e I)

Tactic:
simpa [← not_indep_iff hIE, injOn_insert heI, h.2.1, image_insert_eq]

Premises used: Set.injOn_insert, And.right, And.left, Set.image_insert_eq, Matroid.not_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
h_1 : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
refine_2 : N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
⊢ (N.comap f).Dep (insert e I)

Tactic:
suffices N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
    by simpa [← not_indep_iff hIE, injOn_insert heI, h.2.1, image_insert_eq]
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
h_1 : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
⊢ N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e

Tactic:
h.1.mem_of_insert_indep (mem_image_of_mem f heX)

Premises used: Set.Mem, setOf, And.left, Set.mem_image_of_mem, Matroid.IsBasis.mem_of_insert_indep, Set.image
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
h_1 : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
⊢ N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e

Tactic:
exact h.1.mem_of_insert_indep (mem_image_of_mem f heX)

Premises used: And.left, Set.mem_image_of_mem, Matroid.IsBasis.mem_of_insert_indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
rw :
  N.IsBasis (f '' B) (f '' (N.comap f).E) ∧ InjOn f B ∧ B ⊆ (N.comap f).E ↔
    N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
⊢ (N.comap f).IsBase B ↔ N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E

Tactic:
rw [← isBasis_ground_iff, comap_isBasis_iff]

Premises used: Matroid.isBasis_ground_iff, Matroid.comap_isBasis_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ N.IsBasis (f '' B) (f '' (N.comap f).E) ∧ InjOn f B ∧ B ⊆ (N.comap f).E ↔
    N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
simp : N.IsBasis (f '' I) (f '' X ∩ N.E) → InjOn f I → I ⊆ X → I ⊆ f ⁻¹' N.E
⊢ (N.comap f).IsBasis' I X ↔ N.IsBasis' (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X

Tactic:
simp only [isBasis'_iff_isBasis_inter_ground, comap_ground_eq, comap_isBasis_iff,
    image_inter_preimage, subset_inter_iff, ← and_assoc, and_iff_left_iff_imp,
    and_imp]

Premises used: Set.image_inter_preimage, and_imp, Set.subset_inter_iff, Matroid.isBasis'_iff_isBasis_inter_ground, Matroid.comap_isBasis_iff, Matroid.comap_ground_eq, and_assoc, and_iff_left_iff_imp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
⊢ N.IsBasis (f '' I) (f '' X ∩ N.E) → InjOn f I → I ⊆ X → I ⊆ f ⁻¹' N.E

Tactic:
fun h _ _ ↦ (image_subset_iff.1 h.indep.subset_ground)

Premises used: Matroid.Indep.subset_ground, Iff.mp, Set.image_subset_iff, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
⊢ N.IsBasis (f '' I) (f '' X ∩ N.E) → InjOn f I → I ⊆ X → I ⊆ f ⁻¹' N.E

Tactic:
exact fun h _ _ ↦ (image_subset_iff.1 h.indep.subset_ground)

Premises used: Iff.mp, Set.image_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N_1 N : Matroid β
inst : N.Finitary
f : α → β
⊢ (N.comap f).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_1 N : Matroid β
inst : N.Finitary
f : α → β
refine : ∀ (I : Set α) (hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J), (N.comap f).Indep I
⊢ (N.comap f).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_1 N : Matroid β
inst : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
rw : (∀ J ⊆ f '' I, J.Finite → N.Indep J) ∧ InjOn f I
⊢ (N.comap f).Indep I

Tactic:
rw [comap_indep_iff, indep_iff_forall_finite_subset_indep]

Premises used: Matroid.comap_indep_iff, Matroid.indep_iff_forall_finite_subset_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 β
inst : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
simp : (∀ t ⊆ I, (f '' t).Finite → N.Indep (f '' t)) ∧ InjOn f I
⊢ (∀ J ⊆ f '' I, J.Finite → N.Indep J) ∧ InjOn f I

Tactic:
simp only [forall_subset_image_iff]

Premises used: Set.forall_subset_image_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 β
inst : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
x : α
hx : x ∈ I
y : α
hy : y ∈ I
⊢ Set.Finite (α := α) {x, y}

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 β
inst : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
x : α
hx : x ∈ I
y : α
hy : y ∈ I
⊢ Membership.mem (γ := Set α) {x, y} x

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 β
inst : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
x : α
hx : x ∈ I
y : α
hy : y ∈ I
⊢ Membership.mem (γ := Set α) {x, y} y

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 β
inst : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
refine : ∀ (J : Set α) (hJ : J ⊆ I) (hfin : (f '' J).Finite), N.Indep (f '' J)
⊢ (∀ t ⊆ I, (f '' t).Finite → N.Indep (f '' t)) ∧ InjOn f I

Tactic:
refine ⟨fun J hJ hfin ↦ ?_,
    fun x hx y hy ↦ (hI _ (pair_subset hx hy) (by simp)).2 (by simp) (by 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 β
inst : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
J : Set α
hJ : J ⊆ I
hfin : (f '' J).Finite
obtain : ∀ (J' : Set α) (hJ'J : J' ⊆ J) (hJ' : BijOn f J' (f '' J)), N.Indep (f '' J)
⊢ N.Indep (f '' J)

Tactic:
obtain ⟨J', hJ'J, hJ'⟩ := (surjOn_image f J).exists_bijOn_subset

Premises used: Set.surjOn_image, Set.SurjOn.exists_bijOn_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 β
inst : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
J : Set α
hJ : J ⊆ I
hfin : (f '' J).Finite
J' : Set α
hJ'J : J' ⊆ J
hJ' : BijOn f J' (f '' J)
rw : ∀ (hfin : (f '' J').Finite) (hJ'J : J' ⊆ J) (hJ' : BijOn f J' (f '' J)), N.Indep (f '' J')
⊢ N.Indep (f '' J)

Tactic:
rw [← hJ'.image_eq] at hfin ⊢

Premises used: Set.BijOn.image_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 β
inst : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
J : Set α
hJ : J ⊆ I
J' : Set α
hfin : (f '' J').Finite
hJ'J : J' ⊆ J
hJ' : BijOn f J' (f '' J)
⊢ N.Indep (f '' J')

Tactic:
(hI J' (hJ'J.trans hJ) (hfin.of_finite_image hJ'.injOn)).1

Premises used: HasSubset.Subset.trans, Set.BijOn.injOn, And.left, Set.Finite.of_finite_image
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
inst : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
J : Set α
hJ : J ⊆ I
J' : Set α
hfin : (f '' J').Finite
hJ'J : J' ⊆ J
hJ' : BijOn f J' (f '' J)
⊢ N.Indep (f '' J')

Tactic:
exact (hI J' (hJ'J.trans hJ) (hfin.of_finite_image hJ'.injOn)).1

Premises used: HasSubset.Subset.trans, Set.BijOn.injOn, And.left, Set.Finite.of_finite_image
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N_1 N : Matroid β
inst : N.RankFinite
f : α → β
obtain : ∀ (B : Set α) (hB : (N.comap f).IsBase B), (N.comap f).RankFinite
⊢ (N.comap f).RankFinite

Tactic:
obtain ⟨B, hB⟩ := (N.comap f).exists_isBase

Premises used: Matroid.exists_isBase, Matroid.comap
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N_1 N : Matroid β
inst : N.RankFinite
f : α → β
B : Set α
hB : (N.comap f).IsBase B
⊢ (N.comap f).RankFinite

Tactic:
hB.rankFinite_of_finite ?_

Premises used: Matroid.IsBase.rankFinite_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N_1 N : Matroid β
inst : N.RankFinite
f : α → β
B : Set α
hB : (N.comap f).IsBase B
refine : B.Finite
⊢ (N.comap f).RankFinite

Tactic:
refine hB.rankFinite_of_finite ?_

Premises used: Matroid.IsBase.rankFinite_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N_1 N : Matroid β
inst : N.RankFinite
f : α → β
B : Set α
hB : (N.comap f).IsBase B
⊢ N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E

Tactic:
simp only [comap_isBase_iff] at hB

Premises used: Matroid.comap_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N_1 N : Matroid β
inst : N.RankFinite
f : α → β
B : Set α
hB : N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
⊢ B.Finite

Tactic:
(hB.1.indep.finite.of_finite_image hB.2.1)

Premises used: Matroid.Indep.finite, And.right, And.left, Set.Finite.of_finite_image, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N_1 N : Matroid β
inst : N.RankFinite
f : α → β
B : Set α
hB : N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
⊢ B.Finite

Tactic:
exact (hB.1.indep.finite.of_finite_image hB.2.1)

Premises used: Matroid.Indep.finite, And.right, And.left, Set.Finite.of_finite_image, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
rw : f ⁻¹' N.E = (N.comap f).E
⊢ N.comapOn (f ⁻¹' N.E) f = N.comap f

Tactic:
rw [comapOn, restrict_eq_self_iff]

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

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E I : Set α
⊢ (N.comapOn E f).Indep I ↔ N.Indep (f '' I) ∧ InjOn f I ∧ I ⊆ E

Tactic:
simp [comapOn, and_assoc]

Premises used: Matroid.comapOn, and_assoc
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
⊢ (N.comapOn E f).E = E

Tactic:
rfl

Premises used: rfl