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 α
f : α ↪ β
I X : Set β
⊢ (∃ (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 : α) → β)
have refine_1 : (∃ (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: refine ⟨?_, fun ⟨hb, hIX, hX⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
refine_1 :
  (∃ (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 : α) → β)
⊢ (∃ (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 : α) → β)
have refine_2 : M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X) ∧
    I ⊆ X ∧ X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) →
  ∀ (hb : M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X)) (hIX : I ⊆ X)
    (hX : X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)),
    ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀
Tactic: refine ⟨?_, fun ⟨hb, hIX, hX⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
h :
  M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X) ∧
    I ⊆ X ∧ X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
hb : M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) ((⇑f : (a : α) → β) ⁻¹' X)
hIX : I ⊆ X
hX : X ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀
have refine_2 : ∀ (X : Set α),
  M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)) ∧
      I ⊆ (⇑f : (a : α) → β) '' X ∧
        Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) →
    ∀
      (hb :
        M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I)
          (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)))
      (hIX : I ⊆ (⇑f : (a : α) → β) '' X)
      (hX : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))),
      ∃ (I₀ : Set α) (X₀ : Set α),
        M.IsBasis I₀ X₀ ∧
          I = (⇑f : (a : α) → β) '' I₀ ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' X) ((⇑f : (a : α) → β) '' X₀)
Tactic: obtain ⟨X, rfl⟩ := subset_range_iff_exists_image_eq.1 hX
Cleared hypotheses: X, h, hb, hIX, hX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
X : Set α
h :
  M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)) ∧
    I ⊆ (⇑f : (a : α) → β) '' X ∧
      Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
hb : M.IsBasis ((⇑f : (a : α) → β) ⁻¹' I) (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X))
hIX : I ⊆ (⇑f : (a : α) → β) '' X
hX : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
⊢ ∃ (I₀ : Set α) (X₀ : Set α),
    M.IsBasis I₀ X₀ ∧
      I = (⇑f : (a : α) → β) '' I₀ ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' X) ((⇑f : (a : α) → β) '' X₀)
have refine_2 : ∀ (I : Set α),
  M.IsBasis (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' I))
        (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)) ∧
      Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' X) ∧
        Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' X) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) →
    ∀
      (hb :
        M.IsBasis (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' I))
          (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' X)))
      (hIX : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' X)),
      ∃ (I₀ : Set α) (X₀ : Set α),
        M.IsBasis I₀ X₀ ∧
          Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' I) ((⇑f : (a : α) → β) '' I₀) ∧
            Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' X) ((⇑f : (a : α) → β) '' X₀)
Tactic: obtain ⟨I, -, rfl⟩ := subset_image_iff.1 hIX
Cleared hypotheses: I, h, hb, hIX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
⊢ (M.mapEquiv f).Indep I ↔ M.Indep ((⇑f.symm : (a : β) → α) '' I)
have rw : (∃ (I₀ : Set α), M.Indep I₀ ∧ I = (⇑f : (a : α) → β) '' I₀) ↔ M.Indep ((⇑f.symm : (a : β) → α) '' I)
Tactic: rw [mapEquiv_eq_map, map_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
⊢ (M.mapEquiv f).Dep D ↔ M.Dep ((⇑f.symm : (a : β) → α) '' D)
have rw : (∃ (D₀ : Set α), M.Dep D₀ ∧ D = (⇑f : (a : α) → β) '' D₀) ↔ M.Dep ((⇑f.symm : (a : β) → α) '' D)
Tactic: rw [mapEquiv_eq_map, map_dep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
⊢ (M.mapEquiv f).IsBase B ↔ M.IsBase ((⇑f.symm : (a : β) → α) '' B)
have rw : (∃ (B₀ : Set α), M.IsBase B₀ ∧ B = (⇑f : (a : α) → β) '' B₀) ↔ M.IsBase ((⇑f.symm : (a : β) → α) '' B)
Tactic: rw [mapEquiv_eq_map, map_isBase_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
⊢ (M.mapEquiv f).IsBasis I X ↔ M.IsBasis ((⇑f.symm : (a : β) → α) '' I) ((⇑f.symm : (a : β) → α) '' X)
have rw : (∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀) ↔
  M.IsBasis ((⇑f.symm : (a : β) → α) '' I) ((⇑f.symm : (a : β) → α) '' X)
Tactic: rw [mapEquiv_eq_map, map_isBasis_iff']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
⊢ (∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀) ↔
    M.IsBasis ((⇑f.symm : (a : β) → α) '' I) ((⇑f.symm : (a : β) → α) '' X)
have refine : ∀ (h : ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀),
  M.IsBasis ((⇑f.symm : (a : β) → α) '' I) ((⇑f.symm : (a : β) → α) '' X)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨_, _, h, by simp, by simp⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
h : ∃ (I₀ : Set α) (X₀ : Set α), M.IsBasis I₀ X₀ ∧ I = (⇑f : (a : α) → β) '' I₀ ∧ X = (⇑f : (a : α) → β) '' X₀
⊢ M.IsBasis ((⇑f.symm : (a : β) → α) '' I) ((⇑f.symm : (a : β) → α) '' X)
have obtain : ∀ (I X : Set α) (hIX : M.IsBasis I X),
  M.IsBasis (image.{u_4, u_3} (α := β) (⇑f.symm : (a : β) → α) ((⇑f : (a : α) → β) '' I))
    (image.{u_4, u_3} (α := β) (⇑f.symm : (a : β) → α) ((⇑f : (a : α) → β) '' X))
Tactic: obtain ⟨I, X, hIX, rfl, rfl⟩ := h
Cleared hypotheses: I, X, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
X I : Set α
M : Matroid α
hIX : I ⊆ X
⊢ (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep I
have rw : I ⊆ range (ι := (↑X : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ X))
Tactic: rw [restrictSubtype_indep_iff, image_preimage_eq_iff.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set (↑Y : Type u_1)
⊢ (M.restrictSubtype Y).IsBasis I X ↔
    M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' X)
have rw : M.IsBasis (↑I) (↑X ∩ M.E) ∧ ↑X ⊆ Y ↔
  M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' X ∩ M.E)
Tactic: rw [restrictSubtype, comap_isBasis_iff, and_iff_right Subtype.val_injective.injOn,
    and_iff_left_of_imp, isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set (↑Y : Type u_1)
rw :
  M.IsBasis (↑I) (↑X ∩ M.E) ∧ ↑X ⊆ Y ↔
    M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' X ∩ M.E)
⊢ (M.restrictSubtype Y).IsBasis I X ↔
    M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' X)
have rw₁ : (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X
Tactic: rw [restrictSubtype, comap_isBasis_iff, and_iff_right Subtype.val_injective.injOn,
    and_iff_left_of_imp, isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
X : Set α
M : Matroid α
B : Set (↑X : Type u_1)
⊢ (M.restrictSubtype X).IsBase B ↔ M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ X) '' B) X
have rw : (M ↾ X).IsBasis ↑B ↑(X ↓∩ (M ↾ X).E) ∧ InjOn (Subtype.val (p := fun (x : α) ↦ x ∈ X)) B ∧ B ⊆ X ↓∩ (M ↾ X).E ↔
  M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ X) '' B) X
Tactic: rw [restrictSubtype, comap_isBase_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set (↑M.E : Type u_1)
⊢ IsBase (M.restrictSubtype M.E) B ↔ M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
have rw : M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B) M.E ↔
  M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
Tactic: rw [restrictSubtype_isBase_iff, isBasis'_iff_isBasis, isBasis_ground_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set (↑M.E : Type u_1)
rw :
  M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B) M.E ↔
    M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
⊢ IsBase (M.restrictSubtype M.E) B ↔ M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
have rw₁ : M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B) M.E ↔ M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
Tactic: rw [restrictSubtype_isBase_iff, isBasis'_iff_isBasis, isBasis_ground_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set (↑M.E : Type u_1)
rw :
  M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B) M.E ↔
    M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
rw₁ :
  M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B) M.E ↔
    M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
⊢ IsBase (M.restrictSubtype M.E) B ↔ M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
have rw₂ : M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B) ↔ M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
Tactic: rw [restrictSubtype_isBase_iff, isBasis'_iff_isBasis, isBasis_ground_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set (↑M.E : Type u_1)
⊢ IsBasis (M.restrictSubtype M.E) I X ↔
    M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X)
have rw : M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X) ↔
  M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X)
Tactic: rw [restrictSubtype_isBasis_iff, isBasis'_iff_isBasis]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set (↑M.E : Type u_1)
rw :
  M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X) ↔
    M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X)
⊢ IsBasis (M.restrictSubtype M.E) I X ↔
    M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X)
have rw₁ : M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X) ↔
  M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X)
Tactic: rw [restrictSubtype_isBasis_iff, isBasis'_iff_isBasis]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
E : Set α
M N : Matroid α
hM : M.E = E
hN : N.E = E
h : M.restrictSubtype E = N.restrictSubtype E
⊢ M = N
have hN₁ : N.E = M.E
Tactic: subst hM
Cleared hypotheses: E, hM, hN, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
E : Set α
M N : Matroid α
hM : M.E = E
hN : N.E = E
h : M.restrictSubtype E = N.restrictSubtype E
hN₁ : N.E = M.E
⊢ M = N
have h₁ : Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E) (N.restrictSubtype M.E)
Tactic: subst hM
Cleared hypotheses: E, hM, hN, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E) (N.restrictSubtype M.E)
⊢ M.E = N.E
have rw : M.E = M.E
Tactic: rw [hN]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E) (N.restrictSubtype M.E)
⊢ M = N
have refine : ∀ (I : Set α) (hI : I ⊆ M.E), M.Indep I ↔ N.Indep I
Tactic: refine ext_indep (by rw [hN]) (fun I hI ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E) (N.restrictSubtype M.E)
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ N.Indep I
have rwa : Indep (α := (↑M.E : Type u_1)) (M.restrictSubtype M.E) (M.E ↓∩ I) ↔ N.Indep I
Tactic: rwa [← restrictSubtype_indep_iff_of_subset hI, h, restrictSubtype_indep_iff_of_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E) (N.restrictSubtype M.E)
I : Set α
hI : I ⊆ M.E
rwa : Indep (α := (↑M.E : Type u_1)) (M.restrictSubtype M.E) (M.E ↓∩ I) ↔ N.Indep I
⊢ M.Indep I ↔ N.Indep I
have rwa₁ : Indep (α := (↑M.E : Type u_1)) (N.restrictSubtype M.E) (M.E ↓∩ I) ↔ N.Indep I
Tactic: rwa [← restrictSubtype_indep_iff_of_subset hI, h, restrictSubtype_indep_iff_of_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E) (N.restrictSubtype M.E)
I : Set α
hI : I ⊆ M.E
rwa : Indep (α := (↑M.E : Type u_1)) (M.restrictSubtype M.E) (M.E ↓∩ I) ↔ N.Indep I
rwa₁ : Indep (α := (↑M.E : Type u_1)) (N.restrictSubtype M.E) (M.E ↓∩ I) ↔ N.Indep I
⊢ M.Indep I ↔ N.Indep I
have rwa₂ : N.Indep I ↔ N.Indep I
Tactic: rwa [← restrictSubtype_indep_iff_of_subset hI, h, restrictSubtype_indep_iff_of_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E)✶ (M✶.restrictSubtype M.E)
have rw : BijOn (α := (↑M.E : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E)) (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E
Tactic: rw [restrictSubtype, ← comapOn_preimage_eq, comapOn_dual_eq_of_bijOn, restrict_ground_eq_self,
    ← dual_ground, comapOn_preimage_eq, restrictSubtype, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
E : Set α
M : Matroid α
hM : M.E = E
⊢ (M.restrictSubtype E)✶ = M✶.restrictSubtype E
have rw : Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E)✶ (M✶.restrictSubtype M.E)
Tactic: rw [← hM, restrictSubtype_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
Goal:
α : Type u_1
E : Set α
M : Matroid α
hM : M.E = E
rw : Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E)✶ (M✶.restrictSubtype M.E)
⊢ (M.restrictSubtype E)✶ = M✶.restrictSubtype E
have rw₁ : Eq (α := Matroid (↑M.E : Type u_1)) (M✶.restrictSubtype M.E) (M✶.restrictSubtype M.E)
Tactic: rw [← hM, restrictSubtype_dual]
-- 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 β
E X I : Set α
M : Matroid α
inst : M.RankPos
⊢ RankPos (α := (↑M.E : Type u_1)) (M.restrictSubtype M.E)
have obtain : ∀ (B : Set (↑M.E : Type u_1)) (hB : IsBase (M.restrictSubtype M.E) B),
  RankPos (α := (↑M.E : Type u_1)) (M.restrictSubtype M.E)
Tactic: obtain ⟨B, hB⟩ := (M.restrictSubtype M.E).exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
E X I : Set α
M : Matroid α
inst : M.RankPos
B : Set (↑M.E : Type u_1)
hB : IsBase (M.restrictSubtype M.E) B
⊢ RankPos (α := (↑M.E : Type u_1)) (M.restrictSubtype M.E)
have hB' : M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
Tactic: have hB' : M.IsBase ↑B := by simpa using hB.map Subtype.val_injective.injOn
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ (M ＼ X)✶ = M✶ ／ X
have rw : (M✶✶ ＼ X)✶ = M✶✶✶ ／ X
Tactic: rw [← dual_dual M, dual_delete_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : (M✶✶ ＼ X)✶ = M✶✶✶ ／ X
⊢ (M ＼ X)✶ = M✶ ／ X
have rw₁ : M✶ ／ X = M✶✶✶ ／ X
Tactic: rw [← dual_dual M, dual_delete_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : (M✶✶ ＼ X)✶ = M✶✶✶ ／ X
rw₁ : M✶ ／ X = M✶✶✶ ／ X
⊢ (M ＼ X)✶ = M✶ ／ X
have rw₂ : M✶ ／ X = M✶ ／ X
Tactic: rw [← dual_dual M, dual_delete_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ (M ／ X)✶ = M✶ ＼ X
have rw : (M✶ ＼ X)✶✶ = M✶ ＼ X
Tactic: rw [← dual_delete_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : (M✶ ＼ X)✶✶ = M✶ ＼ X
⊢ (M ／ X)✶ = M✶ ＼ X
have rw₁ : M✶ ＼ X = M✶ ＼ X
Tactic: rw [← dual_delete_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ M ／ C = M ↔ Disjoint C M.E
have rw : (M✶ ＼ C)✶ = M ↔ Disjoint C M.E
Tactic: rw [← dual_delete_dual, ← dual_inj, dual_dual, delete_eq_self_iff, dual_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ C)✶ = M ↔ Disjoint C M.E
⊢ M ／ C = M ↔ Disjoint C M.E
have rw₁ : (M✶ ＼ C)✶✶ = M✶ ↔ Disjoint C M.E
Tactic: rw [← dual_delete_dual, ← dual_inj, dual_dual, delete_eq_self_iff, dual_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ C)✶ = M ↔ Disjoint C M.E
rw₁ : (M✶ ＼ C)✶✶ = M✶ ↔ Disjoint C M.E
⊢ M ／ C = M ↔ Disjoint C M.E
have rw₂ : M✶ ＼ C = M✶ ↔ Disjoint C M.E
Tactic: rw [← dual_delete_dual, ← dual_inj, dual_dual, delete_eq_self_iff, dual_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ C)✶ = M ↔ Disjoint C M.E
rw₁ : (M✶ ＼ C)✶✶ = M✶ ↔ Disjoint C M.E
rw₂ : M✶ ＼ C = M✶ ↔ Disjoint C M.E
⊢ M ／ C = M ↔ Disjoint C M.E
have rw₃ : Disjoint C M✶.E ↔ Disjoint C M.E
Tactic: rw [← dual_delete_dual, ← dual_inj, dual_dual, delete_eq_self_iff, dual_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ C)✶ = M ↔ Disjoint C M.E
rw₁ : (M✶ ＼ C)✶✶ = M✶ ↔ Disjoint C M.E
rw₂ : M✶ ＼ C = M✶ ↔ Disjoint C M.E
rw₃ : Disjoint C M✶.E ↔ Disjoint C M.E
⊢ M ／ C = M ↔ Disjoint C M.E
have rw₄ : Disjoint C M.E ↔ Disjoint C M.E
Tactic: rw [← dual_delete_dual, ← dual_inj, dual_dual, delete_eq_self_iff, dual_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ M ／ {e} = M
have rw : (M✶ ＼ {e})✶ = M
Tactic: rw [← dual_delete_dual, deleteElem_eq_self (by simpa), dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
rw : (M✶ ＼ {e})✶ = M
⊢ M ／ {e} = M
have rw₁ : M✶✶ = M
Tactic: rw [← dual_delete_dual, deleteElem_eq_self (by simpa), dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
rw : (M✶ ＼ {e})✶ = M
rw₁ : M✶✶ = M
⊢ M ／ {e} = M
have rw₂ : M = M
Tactic: rw [← dual_delete_dual, deleteElem_eq_self (by simpa), dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M ／ ∅ = M
have rw : (M✶ ＼ ∅)✶ = M
Tactic: rw [← dual_delete_dual, delete_empty, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
rw : (M✶ ＼ ∅)✶ = M
⊢ M ／ ∅ = M
have rw₁ : M✶✶ = M
Tactic: rw [← dual_delete_dual, delete_empty, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
rw : (M✶ ＼ ∅)✶ = M
rw₁ : M✶✶ = M
⊢ M ／ ∅ = M
have rw₂ : M = M
Tactic: rw [← dual_delete_dual, delete_empty, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ M ／ C₁ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
have rw : (M✶ ＼ C₁)✶ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
Tactic: rw [← dual_delete_dual, ← dual_delete_dual, dual_inj, delete_eq_delete_iff, dual_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
rw : (M✶ ＼ C₁)✶ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
⊢ M ／ C₁ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
have rw₁ : (M✶ ＼ C₁)✶ = (M✶ ＼ C₂)✶ ↔ C₁ ∩ M.E = C₂ ∩ M.E
Tactic: rw [← dual_delete_dual, ← dual_delete_dual, dual_inj, delete_eq_delete_iff, dual_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
rw : (M✶ ＼ C₁)✶ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
rw₁ : (M✶ ＼ C₁)✶ = (M✶ ＼ C₂)✶ ↔ C₁ ∩ M.E = C₂ ∩ M.E
⊢ M ／ C₁ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
have rw₂ : M✶ ＼ C₁ = M✶ ＼ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
Tactic: rw [← dual_delete_dual, ← dual_delete_dual, dual_inj, delete_eq_delete_iff, dual_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
rw : (M✶ ＼ C₁)✶ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
rw₁ : (M✶ ＼ C₁)✶ = (M✶ ＼ C₂)✶ ↔ C₁ ∩ M.E = C₂ ∩ M.E
rw₂ : M✶ ＼ C₁ = M✶ ＼ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
⊢ M ／ C₁ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
have rw₃ : C₁ ∩ M✶.E = C₂ ∩ M✶.E ↔ C₁ ∩ M.E = C₂ ∩ M.E
Tactic: rw [← dual_delete_dual, ← dual_delete_dual, dual_inj, delete_eq_delete_iff, dual_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
rw : (M✶ ＼ C₁)✶ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
rw₁ : (M✶ ＼ C₁)✶ = (M✶ ＼ C₂)✶ ↔ C₁ ∩ M.E = C₂ ∩ M.E
rw₂ : M✶ ＼ C₁ = M✶ ＼ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
rw₃ : C₁ ∩ M✶.E = C₂ ∩ M✶.E ↔ C₁ ∩ M.E = C₂ ∩ M.E
⊢ M ／ C₁ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
have rw₄ : C₁ ∩ M.E = C₂ ∩ M.E ↔ C₁ ∩ M.E = C₂ ∩ M.E
Tactic: rw [← dual_delete_dual, ← dual_delete_dual, dual_inj, delete_eq_delete_iff, dual_ground]