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 : Set α
M : Matroid α
N : Matroid β
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
have inl : range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1)) (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) = (emptyOn β).E ∧
  ∀ (I : Set β),
    (emptyOn β).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: refine ⟨emptyOn β, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
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) β
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
have x : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
Tactic: have _ : Nonempty M.E := ⟨⟨e,he⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
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) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 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 x : Nonempty α
Tactic: have _ : Nonempty α := ⟨e⟩
-- 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) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
h_1 : Nonempty α
⊢ ∃ (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 : ∀ (I : Set β),
  Indep
      (M.comapOn (range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β)) fun (x : β) ↦
        (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α))
      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: refine ⟨M.comapOn (range f) (fun x ↦ ↑(invFunOn f univ x)), rfl, ?_⟩
-- 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) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
h_1 : Nonempty α
⊢ ∀ (I : Set β),
    Indep
        (M.comapOn (range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β)) fun (x : β) ↦
          (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α))
        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 : ∀ (I : Set β),
  (∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I) →
    (M.Indep ((fun (x : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α)) '' I) ∧
        InjOn.{u_2, u_1} (β := α) (fun (x : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α)) I ↔
      M.Indep
        (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
          ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)))
Tactic: simp_rw [comapOn_indep_iff, ← and_assoc, and_congr_left_iff, subset_range_iff_exists_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_1 : Matroid α
N : Matroid β
M : Matroid α
f : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
h_1 : Nonempty α
I : Set (↑M.E : Type u_1)
⊢ M.Indep
        ((fun (x : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α)) ''
          (⇑f : (a : (↑M.E : Type u_1)) → β) '' I) ∧
      InjOn.{u_2, u_1} (β := α) (fun (x : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α))
        ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) ↔
    M.Indep
      (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
        (preimage.{u_1, u_2} (β := β) (⇑f : (a : (↑M.E : Type u_1)) → β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I)))
have inr : M.Indep ↑I →
  InjOn.{u_2, u_1} (β := α) (fun (x : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α))
    ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I)
Tactic: rw [← image_image, InjOn.invFunOn_image f.injective.injOn (subset_univ _),
      preimage_image_eq _ f.injective, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
f : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
e : α
he : e ∈ M.E
h : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
h_1 : Nonempty α
I : Set (↑M.E : Type u_1)
x : β
hx : Membership.mem (γ := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) x
y : β
hy : Membership.mem (γ := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) y
⊢ Eq.{u_1 + 1} (α := α) ((fun (x : β) ↦ ((↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α) : α)) x)
      ((fun (x : β) ↦ ((↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x) : α) : α)) y) →
    x = y
have inr : Eq.{max 1 (u_1 + 1)} (α := { x : α // x ∈ M.E }) (invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x)
    (invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ y) →
  x = y
Tactic: simp only [Subtype.val_inj]
-- 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: classical
    obtain (rfl | ⟨⟨e, he⟩⟩) := eq_emptyOn_or_nonempty M
    · refine ⟨emptyOn β, ?_⟩
      simp only [emptyOn_ground] at f
      simp [range_eq_empty f, subset_empty_iff]
    have _ : Nonempty M.E := ⟨⟨e,he⟩⟩
    have _ : Nonempty α := ⟨e⟩
    refine ⟨M.comapOn (range f) (fun x ↦ ↑(invFunOn f univ x)), rfl, ?_⟩
    simp_rw [comapOn_indep_iff, ← and_assoc, and_congr_left_iff, subset_range_iff_exists_image_eq]
    rintro _ ⟨I, rfl⟩
    rw [← image_image, InjOn.invFunOn_image f.injective.injOn (subset_univ _),
      preimage_image_eq _ f.injective, and_iff_left_iff_imp]
    rintro - x hx y hy
    simp only [Subtype.val_inj]
    exact (invFunOn_injOn_image f univ) (image_mono (subset_univ I) hx)
      (image_mono (subset_univ I) hy)
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: classical
    obtain (rfl | ⟨⟨e, he⟩⟩) := eq_emptyOn_or_nonempty M
    · refine ⟨emptyOn β, ?_⟩
      simp only [emptyOn_ground] at f
      simp [range_eq_empty f, subset_empty_iff]
    have _ : Nonempty M.E := ⟨⟨e,he⟩⟩
    have _ : Nonempty α := ⟨e⟩
    refine ⟨M.comapOn (range f) (fun x ↦ ↑(invFunOn f univ x)), rfl, ?_⟩
    simp_rw [comapOn_indep_iff, ← and_assoc, and_congr_left_iff, subset_range_iff_exists_image_eq]
    rintro _ ⟨I, rfl⟩
    rw [← image_image, InjOn.invFunOn_image f.injective.injOn (subset_univ _),
      preimage_image_eq _ f.injective, and_iff_left_iff_imp]
    rintro - x hx y hy
    simp only [Subtype.val_inj]
    exact (invFunOn_injOn_image f univ) (image_mono (subset_univ I) hx)
      (image_mono (subset_univ I) hy)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
I : Set β
⊢ (M.mapSetEmbedding f).Indep I ↔
    ∃ (I₀ : Set (↑M.E : Type u_1)),
      M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀
have simp : (M.Indep
      (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
        ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
    ∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I) ↔
  ∃ (I₀ : Set (↑M.E : Type u_1)),
    M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀
Tactic: simp only [mapSetEmbedding_indep_iff, subset_range_iff_exists_image_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
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)) ∧
      ∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I) ↔
    ∃ (I₀ : Set (↑M.E : Type u_1)),
      M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀
have mp : (M.Indep
      (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
        ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
    ∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I) →
  ∃ (I₀ : Set (↑M.E : Type u_1)),
    M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
I : Set β
mp :
  (M.Indep
        (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
          ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
      ∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I) →
    ∃ (I₀ : Set (↑M.E : Type u_1)),
      M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀
⊢ (M.Indep
        (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
          ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
      ∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I) ↔
    ∃ (I₀ : Set (↑M.E : Type u_1)),
      M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀
have mpr : (∃ (I₀ : Set (↑M.E : Type u_1)),
    M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I₀) ∧ I = (⇑f : (a : (↑M.E : Type u_1)) → β) '' I₀) →
  M.Indep
      (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
        ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
    ∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
I : Set (↑M.E : Type u_1)
hI :
  M.Indep
    (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
      (preimage.{u_1, u_2} (β := β) (⇑f : (a : (↑M.E : Type u_1)) → β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I)))
⊢ M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I)
have rwa : ∀ (hI : M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I)),
  M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I)
Tactic: rwa [preimage_image_eq _ f.injective] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
I : Set (↑M.E : Type u_1)
hI : M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I)
⊢ M.Indep
      (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
        (preimage.{u_1, u_2} (β := β) (⇑f : (a : (↑M.E : Type u_1)) → β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I))) ∧
    ∃ (t : Set (↑M.E : Type u_1)),
      Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' t) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I)
have mpr : M.Indep (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) ∧
  ∃ (t : Set (↑M.E : Type u_1)),
    Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' t) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I)
Tactic: rw [preimage_image_eq _ f.injective]
-- 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 : α → β
hf : InjOn f M.E
⊢ ∃ (M_2 : Matroid β),
    f '' M.E = M_2.E ∧ ∀ (I : Set β), M_2.Indep I ↔ (fun (I : Set β) ↦ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀) I
have refine : ∀ (I : Set β),
  (M.mapSetEmbedding
          { toFun := M.E.restrict (π := fun (a : α) ↦ β) f, inj' := sorry :
            Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β }).Indep
      I ↔
    (fun (I : Set β) ↦ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀) I
Tactic: refine ⟨M.mapSetEmbedding ⟨_, hf.injective⟩, by simp, fun I ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (M.mapSetEmbedding
          { toFun := M.E.restrict (π := fun (a : α) ↦ β) f, inj' := ⋯ :
            Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β }).Indep
      I ↔
    (fun (I : Set β) ↦ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀) I
have simp_rw : (∃ s ⊆ M.E, M.Indep s ∧ I = f '' s) ↔ ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀
Tactic: simp_rw [mapSetEmbedding_indep_iff', Embedding.coeFn_mk, restrict_apply,
      ← image_image f Subtype.val, Subtype.exists_set_subtype (p := fun J ↦ M.Indep J ∧ I = f '' J)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I : Set β
hf : InjOn f M.E
hI : (M.map f hf).Indep I
⊢ ∃ (I₀ : Set α), M.Indep I₀ ∧ BijOn f I₀ I
have obtain : ∀ (I₀ : Set α) (hI₀ : M.Indep I₀), ∃ (I₀_1 : Set α), M.Indep I₀_1 ∧ BijOn f I₀_1 (f '' I₀)
Tactic: obtain ⟨I₀, hI₀, rfl⟩ := hI
Cleared hypotheses: I, hI
-- 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
I : Set α
hI : I ⊆ M.E
⊢ (∃ (I₀ : Set α), M.Indep I₀ ∧ f '' I = f '' I₀) ↔ M.Indep I
have refine : (∃ (I₀ : Set α), M.Indep I₀ ∧ f '' I = f '' I₀) → ∀ (J : Set α) (hJ : M.Indep J) (hIJ : f '' I = f '' J), M.Indep I
Tactic: refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨I, 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
I : Set α
hI : I ⊆ M.E
h : ∃ (I₀ : Set α), M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : f '' I = f '' J
⊢ M.Indep 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
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ Maximal (M.map f hf).Indep B ↔ ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀
have refine_1 : ∀ (h : Maximal (M.map f hf).Indep B), ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
refine_1 : ∀ (h : Maximal (M.map f hf).Indep B), ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀
⊢ Maximal (M.map f hf).Indep B ↔ ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀
have refine_2 : (∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀) → Maximal (M.map f hf).Indep B
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
⊢ ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀
have refine_1 : ∀ (B₀ : Set α) (hB₀ : M.Indep B₀) (hbij : BijOn f B₀ B), ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀
Tactic: obtain ⟨B₀, hB₀, hbij⟩ := h.prop.exists_bijOn_of_map
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
⊢ ∃ (B₀ : Set α), M.IsBase B₀ ∧ B = f '' B₀
have refine_1 : ∀ (J : Set α) (hJ : M.Indep J) (hB₀J : B₀ ⊆ J), B₀ = J
Tactic: refine ⟨B₀, hB₀.isBase_of_maximal fun J hJ hB₀J ↦ ?_, hbij.image_eq.symm⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ B₀ = J
have refine_1 : B = f '' J
Tactic: rw [← hf.image_eq_image_iff hB₀.subset_ground hJ.subset_ground, hbij.image_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
⊢ Maximal (M.map f hf).Indep (f '' B)
have refine_2 : (M.map f hf).Indep (f '' B) ∧ ∀ ⦃t : Set β⦄, (M.map f hf).Indep t → f '' B ⊆ t → f '' B = t
Tactic: rw [maximal_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
⊢ (M.map f hf).Indep (f '' B) ∧ ∀ ⦃t : Set β⦄, (M.map f hf).Indep t → f '' B ⊆ t → f '' B = t
have refine_2 : ∀ (I : Set β) (hI : (M.map f hf).Indep I) (hBI : f '' B ⊆ I), f '' B = I
Tactic: refine ⟨hB.indep.map f hf, fun I hI hBI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
hBI : f '' B ⊆ I
⊢ f '' B = I
have refine_2 : ∀ (I₀ : Set α) (hI₀ : M.Indep I₀) (hbij : BijOn f I₀ I), f '' B = I
Tactic: obtain ⟨I₀, hI₀, hbij⟩ := hI.exists_bijOn_of_map
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
hBI : f '' B ⊆ I
I₀ : Set α
hI₀ : M.Indep I₀
hbij : BijOn f I₀ I
⊢ f '' B = I
have hBI₁ : B ⊆ I₀
Tactic: rw [← hbij.image_eq, hf.image_subset_image_iff hB.subset_ground hI₀.subset_ground] at hBI
Cleared hypotheses: hBI, hI₀, hbij
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
I₀ : Set α
hBI : B ⊆ I₀
hI₀ : M.Indep I₀
hbij : BijOn f I₀ I
⊢ f '' B = I
have refine_2 : f '' I₀ = I
Tactic: rw [hB.eq_of_subset_indep hI₀ hBI, hbij.image_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
I₀ : Set α
hBI : B ⊆ I₀
hI₀ : M.Indep I₀
hbij : BijOn f I₀ I
refine_2 : f '' I₀ = I
⊢ f '' B = I
have refine_2₁ : I = I
Tactic: rw [hB.eq_of_subset_indep hI₀ hBI, hbij.image_eq]