awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ J₀ = K
have rw₁ : f '' K = f '' K
Tactic: rw [← hKinj.image_eq_image_iff hJ₀K Subset.rfl, hJmax hK (image_subset_range _ _)
        (image_mono hKX) (image_mono hJ₀K)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ (N.comap f).Dep I ↔ N.Dep (f '' I) ∨ N.Indep (f '' I) ∧ ¬InjOn f I
have 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
Tactic: rw [Dep, comap_indep_iff, not_and, comap_ground_eq, Dep, image_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
have 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
Tactic: refine ⟨by grind, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
have inr : I ⊆ f ⁻¹' N.E
Tactic: rw [iff_true_intro hI.1, iff_true_intro hI.2, implies_true, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ (N.comap f).Indep I ↔ N.Indep (f '' I)
have rw : N.Indep (f '' I) → InjOn f I
Tactic: rw [comap_indep_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
have refine : ∀ (hi : N.Indep (f '' I)), I ⊆ f ⁻¹' f '' I
Tactic: refine fun hi ↦ hf.mono <| subset_trans ?_ (preimage_mono hi.subset_ground)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
E : Set β
⊢ (loopyOn E).comap f = loopyOn (f ⁻¹' E)
have rw : ((loopyOn E).comap f).E = f ⁻¹' E ∧ ∀ X ⊆ ((loopyOn E).comap f).E, ((loopyOn E).comap f).Indep X → X = ∅
Tactic: rw [eq_loopyOn_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
have refine_1 : ∀ (h : (N.comap f).IsBasis I X), N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ (N.comap f).IsBasis I X ↔ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
have refine_2 : ∀ (h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X), (N.comap f).IsBasis I X
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
⊢ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
have hI : N.Indep (f '' I)
Tactic: obtain ⟨hI, hinj⟩ := comap_indep_iff.1 h.indep
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
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)
⊢ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
have hinj : InjOn f I
Tactic: obtain ⟨hI, hinj⟩ := comap_indep_iff.1 h.indep
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
have refine_1 : ∀ (e : β) (he : e ∈ f '' X \ f '' I), N.Dep (insert e (f '' I))
Tactic: refine ⟨hI.isBasis_of_forall_insert (image_mono h.subset) fun e he ↦ ?_, hinj, h.subset⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
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
⊢ N.Dep (insert e (f '' I))
have he₁ : (∃ x ∈ X, f x = e) ∧ ∀ x ∈ I, ¬f x = e
Tactic: simp only [mem_diff, mem_image, not_exists, not_and] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ N.Dep (insert e (f '' I))
have refine_1 : ∀ (e : α) (heX : e ∈ X) (he : ∀ x ∈ I, ¬f x = f e), N.Dep (insert (f e) (f '' I))
Tactic: obtain ⟨⟨e, heX, rfl⟩, he⟩ := he
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
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
⊢ N.Dep (insert (f e) (f '' I))
have heI : e ∉ I
Tactic: have heI : e ∉ I := fun heI ↦ (he e heI rfl)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
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.Dep (insert (f e) (f '' I))
have h₁ : (N.comap f).Dep (insert e I)
Tactic: replace h := h.insert_dep ⟨heX, heI⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
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.Dep (insert (f e) (f '' I))
have h₁ : (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
have refine_2 : (N.comap f).Indep I
Tactic: refine Indep.isBasis_of_forall_insert ?_ h.2.2 fun e ⟨heX, heI⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ (N.comap f).IsBasis I X
have refine_2₁ : ∀ e ∈ X \ I, ∀ (heX : e ∈ X) (heI : e ∉ I), (N.comap f).Dep (insert e I)
Tactic: refine Indep.isBasis_of_forall_insert ?_ h.2.2 fun e ⟨heX, heI⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
have simp_rw : f '' insert e I ⊆ N.E
Tactic: simp_rw [comap_ground_eq, ← image_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
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
⊢ (N.comap f).Dep (insert e I)
have hIE : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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.comap f).Dep (insert e I)
have refine_2 : N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ (N.comap f).IsBase B ↔ N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
have 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
Tactic: rw [← isBasis_ground_iff, comap_isBasis_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
have simp : N.IsBasis (f '' I) (f '' X ∩ N.E) → InjOn f I → I ⊆ X → I ⊆ f ⁻¹' N.E
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
have refine : ∀ (I : Set α) (hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J), (N.comap f).Indep I
Tactic: refine ⟨fun I hI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ (N.comap f).Indep I
have rw : (∀ J ⊆ f '' I, J.Finite → N.Indep J) ∧ InjOn f I
Tactic: rw [comap_indep_iff, indep_iff_forall_finite_subset_indep]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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 ⊆ f '' I, J.Finite → N.Indep J) ∧ InjOn f I
have simp : (∀ t ⊆ I, (f '' t).Finite → N.Indep (f '' t)) ∧ InjOn f I
Tactic: simp only [forall_subset_image_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ (∀ t ⊆ I, (f '' t).Finite → N.Indep (f '' t)) ∧ InjOn f I
have refine : ∀ (J : Set α) (hJ : J ⊆ I) (hfin : (f '' J).Finite), N.Indep (f '' J)
Tactic: refine ⟨fun J hJ hfin ↦ ?_,
    fun x hx y hy ↦ (hI _ (pair_subset hx hy) (by simp)).2 (by simp) (by simp)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ N.Indep (f '' J)
have obtain : ∀ (J' : Set α) (hJ'J : J' ⊆ J) (hJ' : BijOn f J' (f '' J)), N.Indep (f '' J)
Tactic: obtain ⟨J', hJ'J, hJ'⟩ := (surjOn_image f J).exists_bijOn_subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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)
⊢ N.Indep (f '' J)
have rw : ∀ (hfin : (f '' J').Finite) (hJ'J : J' ⊆ J) (hJ' : BijOn f J' (f '' J)), N.Indep (f '' J')
Tactic: rw [← hJ'.image_eq] at hfin ⊢
Cleared hypotheses: hfin, hJ'J, hJ'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N_1 N : Matroid β
inst : N.RankFinite
f : α → β
⊢ (N.comap f).RankFinite
have obtain : ∀ (B : Set α) (hB : (N.comap f).IsBase B), (N.comap f).RankFinite
Tactic: obtain ⟨B, hB⟩ := (N.comap f).exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
have refine : B.Finite
Tactic: refine hB.rankFinite_of_finite ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
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
⊢ B.Finite
have hB₁ : N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
Tactic: simp only [comap_isBase_iff] at hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
⊢ N.comapOn (f ⁻¹' N.E) f = N.comap f
have rw : f ⁻¹' N.E = (N.comap f).E
Tactic: rw [comapOn, restrict_eq_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
⊢ (N.comapOn E f).IsBase B ↔ N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E
have rw : (N.comap f ↾ E).IsBase B ↔ N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E
Tactic: rw [comapOn, isBase_restrict_iff', comap_isBasis'_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ (N.comapOn E f).IsBase B ↔ N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E
have rw₁ : (N.comap f).IsBasis' B E ↔ N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E
Tactic: rw [comapOn, isBase_restrict_iff', comap_isBasis'_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ (N.comapOn E f).IsBase B ↔ N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E
have rw₂ : N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E ↔ N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E
Tactic: rw [comapOn, isBase_restrict_iff', comap_isBasis'_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E
have simp_rw : N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E
have simp_rw₁ : InjOn f B ∧ B ⊆ E → (N.IsBasis' (f '' B) (f '' E) ↔ N.IsBase (f '' B))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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))
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E
have simp_rw₂ : InjOn f B → B ⊆ E → (N.IsBasis' (f '' B) (f '' E) ↔ N.IsBase (f '' B))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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))
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E
have simp_rw₃ : InjOn f B → B ⊆ E → (N.IsBasis (f '' B) (f '' E ∩ N.E) ↔ N.IsBase (f '' B))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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))
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E
have simp_rw₄ : InjOn f B → B ⊆ E → (N.IsBasis (f '' B) N.E ↔ N.IsBase (f '' B))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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))
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E
have simp_rw₅ : InjOn f B → B ⊆ E → True
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ B ⊆ E
have rw : B ⊆ E → ((N.comapOn E f).IsBase B ↔ N.IsBase (f '' B))
Tactic: rw [← and_iff_left_of_imp (IsBase.subset_ground (M := N.comapOn E f) (B := B)),
    comapOn_ground_eq, and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ B ⊆ E → ((N.comapOn E f).IsBase B ↔ N.IsBase (f '' B))
have suffices : B ⊆ E → InjOn f B
Tactic: suffices h' : B ⊆ E → InjOn f B from fun hB ↦
    by simp [hB, comapOn_isBase_iff_of_surjOn h.surjOn, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f)✶ = N✶.comapOn E f
have refine : ∀ (B : Set α) (hB : B ⊆ (N.comapOn E f)✶.E), (N.comapOn E f)✶.IsBase B ↔ (N✶.comapOn E f).IsBase B
Tactic: refine ext_isBase (by simp) (fun B hB ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ (N.comapOn E f)✶.IsBase B ↔ (N✶.comapOn E f).IsBase B
have rw : f '' B ⊆ N.E
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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) β
⊢ ∃ (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
have 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
Tactic: obtain (rfl | ⟨⟨e, he⟩⟩) := eq_emptyOn_or_nonempty M
Cleared hypotheses: M, f
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain (rfl | ⟨⟨e, he⟩⟩) := eq_emptyOn_or_nonempty M