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 : α → β
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
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)
have obtain : ∀ (I' : Set α) (hII' : I ⊂ I') (hI' : N.Indep (f '' I')) (hI'inj : InjOn f I'),
  ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)
Tactic: obtain ⟨I', hII', hI', hI'inj⟩ := (not_maximal_subset_iff ⟨hI, hIinj⟩).1 hImax
-- 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 : α → β
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'
⊢ ¬(N ↾ range f).IsBase (f '' I)
have refine : ∀ (hB : (N ↾ range f).IsBase (f '' I)), I = I'
Tactic: refine fun hB ↦ hII'.ne ?_
-- 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_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'
hB : (N ↾ range f).IsBase (f '' I)
⊢ I = I'
have h_im : f '' I = f '' I'
Tactic: have h_im := hB.eq_of_subset_indep (by simpa) (image_mono hII'.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 β
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'
hB : (N ↾ range f).IsBase (f '' I)
h_im : f '' I = f '' I'
⊢ I = I'
have rwa : ∀ (h_im : I = I'), I = I'
Tactic: rwa [hI'inj.image_eq_image_iff hII'.subset Subset.rfl] at h_im
Cleared hypotheses: h_im
-- 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_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'
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)
have h₁ : ¬(N ↾ range f).IsBase (f '' I)
Tactic: have h₁ : ¬(N ↾ range f).IsBase (f '' I) := by
        refine fun hB ↦ hII'.ne ?_
        have h_im := hB.eq_of_subset_indep (by simpa) (image_mono hII'.subset)
        rwa [hI'inj.image_eq_image_iff hII'.subset Subset.rfl] at h_im
-- 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 : α → β
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)
have refine : ∀ e ∈ (N ↾ range f).E \ f '' B, ¬(N ↾ range f).Indep (insert e (f '' B))
Tactic: refine Indep.isBase_of_forall_insert (by simpa using hBmax.1.1) ?_
-- 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_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 ↾ range f).Indep (insert (f e) (f '' B))
⊢ False
have hi₁ : N.Indep (f '' insert e B) ∧ f '' insert e B ⊆ range f
Tactic: rw [restrict_indep_iff, ← image_insert_eq] at hi
Cleared hypotheses: 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 β
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)
have rw : InjOn f B ∧ f e ∉ f '' B
Tactic: rw [injOn_insert (fun heB ↦ hfe (mem_image_of_mem f heB))]
-- 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_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
⊢ False
have hinj : 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⟩
-- 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 : α → β
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
have refine : e ∉ B
Tactic: refine hBmax.not_prop_of_ssuperset (t := insert e B) (ssubset_insert ?_) ⟨hi.1, hinj⟩
-- 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_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)
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)
have h₂ : (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
-- 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 : α → β
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)
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)
have 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)
Tactic: obtain ⟨_, ⟨⟨e, he, rfl⟩, he'⟩, hei⟩ := Indep.exists_insert_of_not_isBase (by simpa) h₁ h₂
-- 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_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
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)
have heI : e ∉ I
Tactic: have heI : e ∉ I := fun heI ↦ he' (mem_image_of_mem f heI)
-- 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_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
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)
have hei₁ : N.Indep (f '' insert e I) ∧ f '' insert e I ⊆ range f
Tactic: rw [← image_insert_eq, restrict_indep_iff] at hei
Cleared hypotheses: hei, he', heI
-- 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 α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) K ∧ K ⊆ X) J
have 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
Tactic: obtain ⟨J, hJ⟩ := (N ↾ range f).existsMaximalSubsetProperty_indep (f '' X) (by simp)
        (f '' I) (by simpa) (image_mono hIX)
-- 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 β
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
have 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
Tactic: simp only [restrict_indep_iff, image_subset_iff, maximal_subset_iff, and_imp,
        and_assoc] at hJ ⊢
Cleared hypotheses: hJ
-- 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_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
⊢ ∃ (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
have hIJ : I ⊆ f ⁻¹' J
Tactic: obtain ⟨hIJ, hJ, hJf, hJX, hJmax⟩ := hJ
Cleared hypotheses: hJ
-- 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_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
⊢ ∃ (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
have hJ₁ : N.Indep J
Tactic: obtain ⟨hIJ, hJ, hJf, hJX, hJmax⟩ := hJ
Cleared hypotheses: hJ
-- 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_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 : 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
have hJf : J ⊆ range f
Tactic: obtain ⟨hIJ, hJ, hJf, hJX, hJmax⟩ := hJ
Cleared hypotheses: hJ
-- 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_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 : 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
have hJX : J ⊆ f '' X
Tactic: obtain ⟨hIJ, hJ, hJf, hJX, hJmax⟩ := hJ
Cleared hypotheses: hJ
-- 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_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
⊢ ∃ (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
have hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
Tactic: obtain ⟨hIJ, hJ, hJf, hJX, hJmax⟩ := hJ
Cleared hypotheses: hJ
-- 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 ⊆ 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 α),
    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
have 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
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)
-- 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 ⊆ 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)
⊢ f '' J₀ = J
have rw : f '' J₀ = f '' f ⁻¹' J
Tactic: rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]
-- 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 ⊆ 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
⊢ f '' J₀ = J
have rw₁ : f '' f ⁻¹' J = f '' f ⁻¹' J
Tactic: rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]
-- 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_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)
⊢ ∃ (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
have hIJ₁ : I ⊆ f ⁻¹' f '' J₀
Tactic: obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]
Cleared hypotheses: J, hIJ, hJ, hJf, hJX, hJmax, hbj
-- 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_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₀
⊢ ∃ (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
have hJ₁ : N.Indep (f '' J₀)
Tactic: obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]
Cleared hypotheses: J, hIJ, hJ, hJf, hJX, hJmax, hbj
-- 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_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₀)
⊢ ∃ (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
have hJf₁ : f '' J₀ ⊆ range f
Tactic: obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]
Cleared hypotheses: J, hIJ, hJ, hJf, hJX, hJmax, hbj
-- 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_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
⊢ ∃ (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
have hJX₁ : f '' J₀ ⊆ f '' X
Tactic: obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]
Cleared hypotheses: J, hIJ, hJ, hJf, hJX, hJmax, hbj
-- 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_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
⊢ ∃ (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
have hJmax₁ : ∀ ⦃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]
Cleared hypotheses: J, hIJ, hJ, hJf, hJX, hJmax, hbj
-- 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_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
⊢ ∃ (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
have hbj₁ : BijOn f J₀ (f '' f ⁻¹' f '' J₀)
Tactic: obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]
Cleared hypotheses: J, hIJ, hJ, hJf, hJX, hJmax, hbj
-- 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₀)
⊢ ∃ (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
have refine : ∀ (K : Set α) (hK : N.Indep (f '' K)) (hKinj : InjOn f K) (hKX : K ⊆ X) (hJ₀K : J₀ ⊆ K), J₀ = K
Tactic: refine ⟨J₀, hIJ₀, hJ, hbj.injOn, hJ₀X, fun K hK hKinj hKX hJ₀K ↦ ?_⟩
-- 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
⊢ J₀ = K
have rw : f '' J₀ = 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)]