awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).IsBase (f '' B)
have rw : ∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀
Tactic: rw [map_isBase_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D : Set β
⊢ (M.map f hf).Dep D ↔ ∃ (D₀ : Set α), M.Dep D₀ ∧ D = f '' D₀
have simp : ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) ↔
  ∃ (D₀ : Set α), (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀
Tactic: simp only [Dep, map_indep_iff, not_exists, not_and, map_ground, subset_image_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D : Set β
⊢ ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) ↔
    ∃ (D₀ : Set α), (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀
have mp : ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) →
  ∃ (D₀ : Set α), (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D : Set β
mp :
  ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) →
    ∃ (D₀ : Set α), (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀
⊢ ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) ↔
    ∃ (D₀ : Set α), (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀
have mpr : (∃ (D₀ : Set α), (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀) →
  (∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
⊢ (∀ (x : Set α), M.Indep x → ¬f '' D₀ = f '' x) ∧ ∃ u ⊆ M.E, f '' u = f '' D₀
have mpr : ∀ (I : Set α) (hI : M.Indep I) (h_eq : f '' D₀ = f '' I), False
Tactic: refine ⟨fun I hI h_eq ↦ ?_, ⟨_, hD₀E, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : f '' D₀ = f '' I
⊢ False
have h_eq₁ : D₀ = I
Tactic: rw [hf.image_eq_image_iff hD₀E hI.subset_ground] at h_eq
Cleared hypotheses: h_eq
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : D₀ = I
⊢ False
have hI₁ : M.Indep D₀
Tactic: subst h_eq
Cleared hypotheses: I, hI, h_eq
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (M.map f hf).IsBase (f '' B) ↔ M.IsBase B
have rw : (∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀) ↔ M.IsBase B
Tactic: rw [map_isBase_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀) ↔ M.IsBase B
have refine : (∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀) → ∀ (J : Set α) (hJ : M.IsBase J) (hIJ : f '' B = f '' J), M.IsBase B
Tactic: refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨B, h, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
h : ∃ (B₀ : Set α), M.IsBase B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.IsBase J
hIJ : f '' B = f '' J
⊢ M.IsBase B
have hIJ₁ : B = J
Tactic: rw [hf.image_eq_image_iff hB hJ.subset_ground] at hIJ
Cleared hypotheses: hIJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).IsBasis (f '' I) (f '' X)
have refine : ∀ e ∈ f '' X \ f '' I, (M.map f hf).Dep (insert e (f '' I))
Tactic: refine (hIX.indep.map f hf).isBasis_of_forall_insert (image_mono hIX.subset) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
⊢ (M.map f hf).Dep (insert (f e) (f '' I))
have hss : insert e I ⊆ M.E
Tactic: have hss := insert_subset (hIX.subset_ground he) hIX.indep.subset_ground
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ (M.map f hf).Dep (insert (f e) (f '' I))
have rw : ¬(M.map f hf).Indep (insert (f e) (f '' I))
Tactic: rw [← not_indep_iff (by simpa [← image_insert_eq] using image_mono hss)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ ¬(M.map f hf).Indep (insert (f e) (f '' I))
have simp : ∀ (x : Set α), M.Indep x → ¬insert (f e) (f '' I) = f '' x
Tactic: simp only [map_indep_iff, not_exists, not_and]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert (f e) (f '' I) = f '' J
⊢ False
have hins₁ : insert e I = J
Tactic: rw [← image_insert_eq, hf.image_eq_image_iff hss hJ.subset_ground] at hins
Cleared hypotheses: hins
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert e I = J
⊢ False
have hJ₁ : M.Indep (insert e I)
Tactic: obtain rfl := hins
Cleared hypotheses: J, hJ, hins
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
⊢ (M.map f hf).IsBasis (f '' I) (f '' X) ↔ M.IsBasis I X
have refine : ∀ (h : (M.map f hf).IsBasis (f '' I) (f '' X)), M.IsBasis I X
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.map hf⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ M.IsBasis I X
have obtain : ∀ (I' : Set α) (hI' : M.Indep I') (hII' : f '' I = f '' I'), M.IsBasis I X
Tactic: obtain ⟨I', hI', hII'⟩ := map_indep_iff.1 h.indep
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : f '' I = f '' I'
⊢ M.IsBasis I X
have hII'₁ : I = I'
Tactic: rw [hf.image_eq_image_iff hI hI'.subset_ground] at hII'
Cleared hypotheses: hII'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : I = I'
⊢ M.IsBasis I X
have hI'₁ : M.Indep I
Tactic: obtain rfl := hII'
Cleared hypotheses: I', hI', hII'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
⊢ M.IsBasis I X
have hss : I ⊆ X
Tactic: have hss := (hf.image_subset_image_iff hI hX).1 h.subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
⊢ M.IsBasis I X
have refine : ∀ (J : Set α) (hJ : M.Indep J) (hIJ : I ⊆ J) (hJX : J ⊆ X), J ⊆ I
Tactic: refine hI'.isBasis_of_maximal_subset hss (fun J hJ hIJ hJX ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ J ⊆ I
have hIJ' : f '' I = f '' J
Tactic: have hIJ' := h.eq_of_subset_indep (hJ.map f hf) (image_mono hIJ) (image_mono hJX)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
hIJ' : f '' I = f '' J
⊢ J ⊆ I
have hIJ'₁ : I = J
Tactic: rw [hf.image_eq_image_iff hI hJ.subset_ground] at hIJ'
Cleared hypotheses: hIJ'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
⊢ (M.map f hf).IsBasis I X ↔ ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀
have refine_1 : ∀ (h : (M.map f hf).IsBasis I X), ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
refine_1 : ∀ (h : (M.map f hf).IsBasis I X), ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀
⊢ (M.map f hf).IsBasis I X ↔ ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀
have refine_2 : (∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀) → (M.map f hf).IsBasis I X
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
h : (M.map f hf).IsBasis I X
⊢ ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀
have refine_1 : ∀ (I : Set α) (hI : I ⊆ M.E) (h : (M.map f hf).IsBasis (f '' I) X),
  ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ X = f '' X₀
Tactic: obtain ⟨I, hI, rfl⟩ := subset_image_iff.1 h.indep.subset_ground
Cleared hypotheses: I, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
X : Set β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) X
⊢ ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ X = f '' X₀
have refine_1 : ∀ (X : Set α) (hX : X ⊆ M.E) (h : (M.map f hf).IsBasis (f '' I) (f '' X)),
  ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ f '' X = f '' X₀
Tactic: obtain ⟨X, hX, rfl⟩ := subset_image_iff.1 h.subset_ground
Cleared hypotheses: X, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ f '' X = f '' X₀
have h₁ : M.IsBasis I X
Tactic: rw [map_isBasis_iff _ _ hI hX] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ (M.map f hf)✶ = M✶.map f hf
have apply : ∀ ⦃B : Set β⦄, B ⊆ (M.map f hf)✶.E → ((M.map f hf)✶.IsBase B ↔ (M✶.map f hf).IsBase B)
Tactic: apply ext_isBase (by simp)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ ∀ ⦃B : Set β⦄, B ⊆ (M.map f hf)✶.E → ((M.map f hf)✶.IsBase B ↔ (M✶.map f hf).IsBase B)
have simp : ∀ a ⊆ M.E, ((M.map f hf).IsBase (f '' M.E \ f '' a) ∧ ∃ u ⊆ M.E, f '' u = f '' a) ↔ (M✶.map f hf).IsBase (f '' a)
Tactic: simp only [dual_ground, map_ground, subset_image_iff, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, dual_isBase_iff']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ ((M.map f hf).IsBase (f '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).IsBase (f '' B)
have simp_rw : M.IsBase (M.E \ B) → ∃ u ⊆ M.E, f '' u = f '' B
Tactic: simp_rw [← hf.image_diff_subset hB, map_image_isBase_iff diff_subset,
    map_image_isBase_iff (show B ⊆ M✶.E from hB), dual_isBase_iff hB, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (freeOn E).E
⊢ (freeOn E).map f hf = freeOn (f '' E)
have rw : ((freeOn E).map f hf)✶ = (freeOn (f '' E))✶
Tactic: rw [← dual_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ (N.comap f).map f hf = N
have refine : ∀ ⦃I : Set β⦄, I ⊆ ((N.comap f).map f hf).E → (((N.comap f).map f hf).Indep I ↔ N.Indep I)
Tactic: refine ext_indep (by simpa [image_preimage_eq_iff]) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ ∀ ⦃I : Set β⦄, I ⊆ ((N.comap f).map f hf).E → (((N.comap f).map f hf).Indep I ↔ N.Indep I)
have simp : ∀ t ⊆ f ⁻¹' N.E, (∃ (I₀ : Set α), (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' t = f '' I₀) ↔ N.Indep (f '' t)
Tactic: simp only [map_ground, comap_ground_eq, map_indep_iff, comap_indep_iff, 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 : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Finitary
have refine : ∀ (I : Set β) (hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J), (M.map f hf).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 : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
e : β
he : e ∈ I
⊢ e ∈ f '' M.E
have obtain : ∀ (I₀ : Set α) (hI₀ : M.Indep I₀) (h_eq : {e} = f '' I₀), e ∈ f '' M.E
Tactic: obtain ⟨I₀, hI₀, h_eq⟩ := hI {e} (by simpa) (by simp)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
⊢ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀
have h' : I ⊆ f '' M.E
Tactic: have h' : I ⊆ f '' M.E := by
    intro e he
    obtain ⟨I₀, hI₀, h_eq⟩ := hI {e} (by simpa) (by simp)
    exact image_mono hI₀.subset_ground <| h_eq.subset rfl
-- 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 : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
h' : I ⊆ f '' M.E
⊢ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀
have obtain : ∀ (I₀ : Set α) (hI₀E : I₀ ⊆ M.E) (hI : ∀ J ⊆ f '' I₀, J.Finite → (M.map f hf).Indep J) (h' : f '' I₀ ⊆ f '' M.E),
  ∃ (I₀_1 : Set α), M.Indep I₀_1 ∧ f '' I₀ = f '' I₀_1
Tactic: obtain ⟨I₀, hI₀E, rfl⟩ := subset_image_iff.1 h'
Cleared hypotheses: I, hI, h'
-- 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 : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I₀ : Set α
hI₀E : I₀ ⊆ M.E
hI : ∀ J ⊆ f '' I₀, J.Finite → (M.map f hf).Indep J
h' : f '' I₀ ⊆ f '' M.E
⊢ ∃ (I₀_1 : Set α), M.Indep I₀_1 ∧ f '' I₀ = f '' I₀_1
have refine : ∀ (J₀ : Set α) (hJ₀I₀ : J₀ ⊆ I₀) (hJ₀ : J₀.Finite), M.Indep J₀
Tactic: refine ⟨I₀, indep_of_forall_finite_subset_indep _ fun J₀ hJ₀I₀ hJ₀ ↦ ?_, rfl⟩
-- 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 : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I₀ : Set α
hI₀E : I₀ ⊆ M.E
hI : ∀ J ⊆ f '' I₀, J.Finite → (M.map f hf).Indep J
h' : f '' I₀ ⊆ f '' M.E
J₀ : Set α
hJ₀I₀ : J₀ ⊆ I₀
hJ₀ : J₀.Finite
⊢ M.Indep J₀
have hI₁ : (M.map f hf).Indep (f '' J₀)
Tactic: specialize hI (f '' J₀) (image_mono hJ₀I₀) (hJ₀.image _)
Cleared hypotheses: hI
-- 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 : Matroid β
inst : M.Finitary
f : α → β
hf : InjOn f M.E
I₀ : Set α
hI₀E : I₀ ⊆ M.E
h' : f '' I₀ ⊆ f '' M.E
J₀ : Set α
hJ₀I₀ : J₀ ⊆ I₀
hJ₀ : J₀.Finite
hI : (M.map f hf).Indep (f '' J₀)
⊢ M.Indep J₀
have rwa : ∀ (hI : M.Indep J₀), M.Indep J₀
Tactic: rwa [map_image_indep_iff (hJ₀I₀.trans hI₀E)] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
E : Set β
e : Equiv.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) (↑E : Type u_2)
I : Set β
⊢ Eq.{u_1 + 1} (α := Set (↑M.E : Type u_1))
    (comp (β := { x : β // x ∈ E }) (Subtype.val (p := fun (x : β) ↦ x ∈ E))
        (⇑e : (a : (↑M.E : Type u_1)) → (↑E : Type u_2)) ⁻¹'
      I)
    (image (α := (↑E : Type u_2)) (⇑e.symm : (a : (↑E : Type u_2)) → (↑M.E : Type u_1)) (E ↓∩ I))
have h : ∀ (x : (↑M.E : Type u_1)),
  Membership.mem (γ := Set (↑M.E : Type u_1))
      (comp (β := { x : β // x ∈ E }) (Subtype.val (p := fun (x : β) ↦ x ∈ E))
          (⇑e : (a : (↑M.E : Type u_1)) → (↑E : Type u_2)) ⁻¹'
        I)
      x ↔
    Membership.mem (γ := Set (↑M.E : Type u_1))
      (image (α := (↑E : Type u_2)) (⇑e.symm : (a : (↑E : Type u_2)) → (↑M.E : Type u_1)) (E ↓∩ I)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
E : Set β
e : Equiv.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) (↑E : Type u_2)
⊢ E = (M.mapSetEmbedding (e.toEmbedding.trans (Embedding.subtype fun (x : β) ↦ x ∈ E))).E ∧
    ∀ (I : Set β),
      (M.mapSetEmbedding (e.toEmbedding.trans (Embedding.subtype fun (x : β) ↦ x ∈ E))).Indep I ↔
        (fun (I : Set β) ↦
            M.Indep
                (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                  (image (α := (↑E : Type u_2)) (⇑e.symm : (a : (↑E : Type u_2)) → (↑M.E : Type u_1)) (E ↓∩ I))) ∧
              I ⊆ E)
          I
have hrw : ∀ (I : Set β),
  Eq.{u_1 + 1} (α := Set (↑M.E : Type u_1))
    (comp (β := { x : β // x ∈ E }) (Subtype.val (p := fun (x : β) ↦ x ∈ E))
        (⇑e : (a : (↑M.E : Type u_1)) → (↑E : Type u_2)) ⁻¹'
      I)
    (image (α := (↑E : Type u_2)) (⇑e.symm : (a : (↑E : Type u_2)) → (↑M.E : Type u_1)) (E ↓∩ I))
Tactic: have hrw : ∀ I : Set β, Subtype.val ∘ ⇑e ⁻¹' I = ⇑e.symm '' E ↓∩ I := fun I ↦ by ext; simp
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
h_1 : M.Indep ((⇑f : (a : α) → β) ⁻¹' I) ∧ I ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
h : M.Indep ((⇑f : (a : α) → β) ⁻¹' I)
h' : I ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ I = image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' I)
have rwa : image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' I) = I
Tactic: rwa [eq_comm, image_preimage_eq_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
⊢ (∃ (I₀ : Set α), M.Indep I₀ ∧ I = (⇑f : (a : α) → β) '' I₀) ↔
    M.Indep ((⇑f : (a : α) → β) ⁻¹' I) ∧ I ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
have refine : (∃ (I₀ : Set α), M.Indep I₀ ∧ I = (⇑f : (a : α) → β) '' I₀) →
  M.Indep ((⇑f : (a : α) → β) ⁻¹' I) ∧ I ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
Tactic: refine ⟨?_, fun ⟨h,h'⟩ ↦ ⟨f ⁻¹' I, h, by rwa [eq_comm, image_preimage_eq_iff]⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' I)) ∧
    Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
have rw : M.Indep I ∧ Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
Tactic: rw [preimage_image_eq _ f.injective]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α ↪ β
⊢ (M.mapEmbedding f).IsBase ((⇑f : (a : α) → β) '' B)
have rw : ∃ (B₀ : Set α), M.IsBase B₀ ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' B) ((⇑f : (a : α) → β) '' B₀)
Tactic: rw [Matroid.mapEmbedding, map_isBase_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
⊢ (M.mapEmbedding f).IsBase B ↔
    M.IsBase ((⇑f : (a : α) → β) ⁻¹' B) ∧ B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
have rw : (∃ (B₀ : Set α), M.IsBase B₀ ∧ B = (⇑f : (a : α) → β) '' B₀) ↔
  M.IsBase ((⇑f : (a : α) → β) ⁻¹' B) ∧ B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
Tactic: rw [mapEmbedding, map_isBase_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
h_1 : M.IsBase ((⇑f : (a : α) → β) ⁻¹' B) ∧ B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
h : M.IsBase ((⇑f : (a : α) → β) ⁻¹' B)
h' : B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ B = image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' B)
have rwa : image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' B) = B
Tactic: rwa [eq_comm, image_preimage_eq_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
⊢ (∃ (B₀ : Set α), M.IsBase B₀ ∧ B = (⇑f : (a : α) → β) '' B₀) ↔
    M.IsBase ((⇑f : (a : α) → β) ⁻¹' B) ∧ B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
have refine : (∃ (B₀ : Set α), M.IsBase B₀ ∧ B = (⇑f : (a : α) → β) '' B₀) →
  M.IsBase ((⇑f : (a : α) → β) ⁻¹' B) ∧ B ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
Tactic: refine ⟨?_, fun ⟨h,h'⟩ ↦ ⟨f ⁻¹' B, h, by rwa [eq_comm, image_preimage_eq_iff]⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set α
hB : M.IsBase B
⊢ M.IsBase (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' B)) ∧
    Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' B) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
have rw : M.IsBase B ∧ Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' B) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
Tactic: rw [preimage_image_eq _ f.injective]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
⊢ (M.mapEmbedding f).IsBasis I X ↔
    M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X) ∧
      I ⊆ X ∧ X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
have rw : (∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀) ↔
  M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X) ∧
    I ⊆ X ∧ X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
Tactic: rw [mapEmbedding, map_isBasis_iff']