awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
X R : Set α
M : Matroid α
hXR : X ⊆ R
hR : R ⊆ M.E
rw : M.closure (X ∩ R) ∩ R ∪ R \ M.E = M.closure X ∩ R
rw₁ : M.closure (X ∩ R) ∩ R ∪ ∅ = M.closure X ∩ R
⊢ (M ↾ R).closure X = M.closure X ∩ R
have rw₂ : M.closure (X ∩ R) ∩ R = M.closure X ∩ R
Tactic: rw [restrict_closure_eq', diff_eq_empty.mpr hR, union_empty, inter_eq_self_of_subset_left hXR]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
X R : Set α
M : Matroid α
hXR : X ⊆ R
hR : R ⊆ M.E
rw : M.closure (X ∩ R) ∩ R ∪ R \ M.E = M.closure X ∩ R
rw₁ : M.closure (X ∩ R) ∩ R ∪ ∅ = M.closure X ∩ R
rw₂ : M.closure (X ∩ R) ∩ R = M.closure X ∩ R
⊢ (M ↾ R).closure X = M.closure X ∩ R
have rw₃ : M.closure X ∩ R = M.closure X ∩ R
Tactic: rw [restrict_closure_eq', diff_eq_empty.mpr hR, union_empty, inter_eq_self_of_subset_left hXR]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
X E : Set α
⊢ (loopyOn E).Spanning X ↔ X ⊆ E
have rw : (loopyOn E).closure X = (loopyOn E).E ∧ X ⊆ (loopyOn E).E ↔ X ⊆ E
Tactic: rw [spanning_iff, loopyOn_closure_eq, loopyOn_ground, and_iff_right rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
X E : Set α
rw : (loopyOn E).closure X = (loopyOn E).E ∧ X ⊆ (loopyOn E).E ↔ X ⊆ E
⊢ (loopyOn E).Spanning X ↔ X ⊆ E
have rw₁ : E = (loopyOn E).E ∧ X ⊆ (loopyOn E).E ↔ X ⊆ E
Tactic: rw [spanning_iff, loopyOn_closure_eq, loopyOn_ground, and_iff_right rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
X E : Set α
rw : (loopyOn E).closure X = (loopyOn E).E ∧ X ⊆ (loopyOn E).E ↔ X ⊆ E
rw₁ : E = (loopyOn E).E ∧ X ⊆ (loopyOn E).E ↔ X ⊆ E
⊢ (loopyOn E).Spanning X ↔ X ⊆ E
have rw₂ : E = E ∧ X ⊆ E ↔ X ⊆ E
Tactic: rw [spanning_iff, loopyOn_closure_eq, loopyOn_ground, and_iff_right rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
X E : Set α
rw : (loopyOn E).closure X = (loopyOn E).E ∧ X ⊆ (loopyOn E).E ↔ X ⊆ E
rw₁ : E = (loopyOn E).E ∧ X ⊆ (loopyOn E).E ↔ X ⊆ E
rw₂ : E = E ∧ X ⊆ E ↔ X ⊆ E
⊢ (loopyOn E).Spanning X ↔ X ⊆ E
have rw₃ : X ⊆ E ↔ X ⊆ E
Tactic: rw [spanning_iff, loopyOn_closure_eq, loopyOn_ground, and_iff_right rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
I E X : Set α
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I
have rw : (freeOn I ↾ E).closure X = X ∩ I ∩ E ∪ E \ I
Tactic: rw [uniqueBaseOn, restrict_closure_eq', freeOn_closure_eq, inter_right_comm,
    inter_assoc (c := E), inter_self, inter_right_comm, freeOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
I E X : Set α
rw : (freeOn I ↾ E).closure X = X ∩ I ∩ E ∪ E \ I
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I
have rw₁ : (freeOn I).closure (X ∩ E) ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
Tactic: rw [uniqueBaseOn, restrict_closure_eq', freeOn_closure_eq, inter_right_comm,
    inter_assoc (c := E), inter_self, inter_right_comm, freeOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
I E X : Set α
rw : (freeOn I ↾ E).closure X = X ∩ I ∩ E ∪ E \ I
rw₁ : (freeOn I).closure (X ∩ E) ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I
have rw₂ : X ∩ E ∩ I ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
Tactic: rw [uniqueBaseOn, restrict_closure_eq', freeOn_closure_eq, inter_right_comm,
    inter_assoc (c := E), inter_self, inter_right_comm, freeOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
I E X : Set α
rw : (freeOn I ↾ E).closure X = X ∩ I ∩ E ∪ E \ I
rw₁ : (freeOn I).closure (X ∩ E) ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₂ : X ∩ E ∩ I ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I
have rw₃ : X ∩ E ∩ E ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
Tactic: rw [uniqueBaseOn, restrict_closure_eq', freeOn_closure_eq, inter_right_comm,
    inter_assoc (c := E), inter_self, inter_right_comm, freeOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
I E X : Set α
rw : (freeOn I ↾ E).closure X = X ∩ I ∩ E ∪ E \ I
rw₁ : (freeOn I).closure (X ∩ E) ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₂ : X ∩ E ∩ I ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₃ : X ∩ E ∩ E ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I
have rw₄ : X ∩ (E ∩ E) ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
Tactic: rw [uniqueBaseOn, restrict_closure_eq', freeOn_closure_eq, inter_right_comm,
    inter_assoc (c := E), inter_self, inter_right_comm, freeOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
I E X : Set α
rw : (freeOn I ↾ E).closure X = X ∩ I ∩ E ∪ E \ I
rw₁ : (freeOn I).closure (X ∩ E) ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₂ : X ∩ E ∩ I ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₃ : X ∩ E ∩ E ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₄ : X ∩ (E ∩ E) ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I
have rw₅ : X ∩ E ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
Tactic: rw [uniqueBaseOn, restrict_closure_eq', freeOn_closure_eq, inter_right_comm,
    inter_assoc (c := E), inter_self, inter_right_comm, freeOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
I E X : Set α
rw : (freeOn I ↾ E).closure X = X ∩ I ∩ E ∪ E \ I
rw₁ : (freeOn I).closure (X ∩ E) ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₂ : X ∩ E ∩ I ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₃ : X ∩ E ∩ E ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₄ : X ∩ (E ∩ E) ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₅ : X ∩ E ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I
have rw₆ : X ∩ I ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
Tactic: rw [uniqueBaseOn, restrict_closure_eq', freeOn_closure_eq, inter_right_comm,
    inter_assoc (c := E), inter_self, inter_right_comm, freeOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
I E X : Set α
rw : (freeOn I ↾ E).closure X = X ∩ I ∩ E ∪ E \ I
rw₁ : (freeOn I).closure (X ∩ E) ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₂ : X ∩ E ∩ I ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₃ : X ∩ E ∩ E ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₄ : X ∩ (E ∩ E) ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₅ : X ∩ E ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
rw₆ : X ∩ I ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I
have rw₇ : X ∩ I ∩ E ∪ E \ I = X ∩ I ∩ E ∪ E \ I
Tactic: rw [uniqueBaseOn, restrict_closure_eq', freeOn_closure_eq, inter_right_comm,
    inter_assoc (c := E), inter_self, inter_right_comm, freeOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
h : M = loopyOn M.E
⊢ M.closure ∅ = M.E
have rw : (loopyOn M.E).closure ∅ = (loopyOn M.E).E
Tactic: rw [h, loopyOn_closure_eq, loopyOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
h : M = loopyOn M.E
rw : (loopyOn M.E).closure ∅ = (loopyOn M.E).E
⊢ M.closure ∅ = M.E
have rw₁ : M.E = (loopyOn M.E).E
Tactic: rw [h, loopyOn_closure_eq, loopyOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
h : M = loopyOn M.E
rw : (loopyOn M.E).closure ∅ = (loopyOn M.E).E
rw₁ : M.E = (loopyOn M.E).E
⊢ M.closure ∅ = M.E
have rw₂ : M.E = M.E
Tactic: rw [h, loopyOn_closure_eq, loopyOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
⊢ M.closure ∅ = M.E ↔ M = loopyOn M.E
have refine : ∀ (h : M.closure ∅ = M.E) (X : Set α), M.closure X = (loopyOn M.E).closure X
Tactic: refine ⟨fun h ↦ ext_closure ?_, fun h ↦ by rw [h, loopyOn_closure_eq, loopyOn_ground]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
⊢ ∀ (X : Set α), M.closure X = (loopyOn M.E).closure X
have refine : ∀ (X : Set α), (loopyOn M.E).closure X ⊆ M.closure X
Tactic: refine fun X ↦ subset_antisymm (by simp [closure_subset_ground]) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ (loopyOn M.E).closure X ⊆ M.closure X
have rw : M.closure ∅ ⊆ M.closure X
Tactic: rw [loopyOn_closure_eq, ← h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X : Set α
⊢ (M.comap f).closure X = f ⁻¹' M.closure (f '' X)
have obtain : ∀ (I : Set α) (hI : (M.comap f).IsBasis' I X), (M.comap f).closure X = f ⁻¹' M.closure (f '' X)
Tactic: obtain ⟨I, hI⟩ := (M.comap f).exists_isBasis' X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
⊢ (M.comap f).closure X = f ⁻¹' M.closure (f '' X)
have hI' : M.IsBasis' (f '' I) (f '' X)
Tactic: obtain ⟨hI', hIinj, -⟩ := comap_isBasis'_iff.1 hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
⊢ (M.comap f).closure X = f ⁻¹' M.closure (f '' X)
have hIinj : InjOn f I
Tactic: obtain ⟨hI', hIinj, -⟩ := comap_isBasis'_iff.1 hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ (M.comap f).closure X = f ⁻¹' M.closure (f '' X)
have simp_rw : ∀ (x : α),
  f x ∈ M.E →
    (M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x)
Tactic: simp_rw [← hI.closure_eq_closure, ← hI'.closure_eq_closure, Set.ext_iff,
    hI.indep.mem_closure_iff', comap_ground_eq, mem_preimage, hI'.indep.mem_closure_iff',
    comap_indep_iff, and_imp, mem_image, and_congr_right_iff, ← image_insert_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
⊢ M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x
have pos : ∀ (hxI : x ∈ I),
  M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x
Tactic: by_cases hxI : x ∈ I
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
pos :
  ∀ (hxI : x ∈ I),
    M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x
⊢ M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x
have neg : ∀ (hxI : x ∉ I),
  M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x
Tactic: by_cases hxI : x ∈ I
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
have obtain : ∀ (I : Set α) (hI : M.IsBasis I (f ⁻¹' X ∩ M.E)), (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis (f ⁻¹' X ∩ M.E)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
have rw : (M.map f hf).closure (X ∩ (M.map f hf).E) = f '' M.closure (f ⁻¹' X)
Tactic: rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
rw : (M.map f hf).closure (X ∩ (M.map f hf).E) = f '' M.closure (f ⁻¹' X)
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
have rw₁ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X)
Tactic: rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
rw : (M.map f hf).closure (X ∩ (M.map f hf).E) = f '' M.closure (f ⁻¹' X)
rw₁ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X)
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
have rw₂ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X ∩ M.E)
Tactic: rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
rw : (M.map f hf).closure (X ∩ (M.map f hf).E) = f '' M.closure (f ⁻¹' X)
rw₁ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X)
rw₂ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X ∩ M.E)
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
have rw₃ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure I
Tactic: rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
rw : (M.map f hf).closure (X ∩ (M.map f hf).E) = f '' M.closure (f ⁻¹' X)
rw₁ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X)
rw₂ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X ∩ M.E)
rw₃ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure I
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
have rw₄ : (M.map f hf).closure (X ∩ f '' M.E) = (M.map f hf).closure (f '' I)
Tactic: rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
rw : (M.map f hf).closure (X ∩ (M.map f hf).E) = f '' M.closure (f ⁻¹' X)
rw₁ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X)
rw₂ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X ∩ M.E)
rw₃ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure I
rw₄ : (M.map f hf).closure (X ∩ f '' M.E) = (M.map f hf).closure (f '' I)
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
have rw₅ : (M.map f hf).closure (f '' (f ⁻¹' X ∩ M.E)) = (M.map f hf).closure (f '' I)
Tactic: rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
rw : (M.map f hf).closure (X ∩ (M.map f hf).E) = f '' M.closure (f ⁻¹' X)
rw₁ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X)
rw₂ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure (f ⁻¹' X ∩ M.E)
rw₃ : (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure I
rw₄ : (M.map f hf).closure (X ∩ f '' M.E) = (M.map f hf).closure (f '' I)
rw₅ : (M.map f hf).closure (f '' (f ⁻¹' X ∩ M.E)) = (M.map f hf).closure (f '' I)
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
have rw₆ : (M.map f hf).closure (f '' I) = (M.map f hf).closure (f '' I)
Tactic: rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
have suffices : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
Tactic: suffices aux : ∀ ⦃I⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' (M.closure I) by
    obtain ⟨I, hI⟩ := M.exists_isBasis (f ⁻¹' X ∩ M.E)
    rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
⊢ ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
have refine : ∀ (I : Set α) (hI : M.Indep I) (e : β), e ∈ (M.map f hf).closure (f '' I) ↔ e ∈ f '' M.closure I
Tactic: refine fun I hI ↦ Set.ext fun e ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ e ∈ (M.map f hf).closure (f '' I) ↔ e ∈ f '' M.closure I
have simp : ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) ↔
  ∃ (x : α), (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e
Tactic: simp only [(hI.map f hf).mem_closure_iff', map_ground, mem_image, map_indep_iff,
    forall_exists_index, and_imp, hI.mem_closure_iff']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) ↔
    ∃ (x : α), (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e
have mp : ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) →
  ∃ (x : α), (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
mp :
  ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) →
    ∃ (x : α), (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e
⊢ ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) ↔
    ∃ (x : α), (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e
have mpr : (∃ (x : α), (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e) →
  (∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
⊢ ∃ (x_1 : α), (x_1 ∈ M.E ∧ (M.Indep (insert x_1 I) → x_1 ∈ I)) ∧ f x_1 = f x
have mp : ∀ (hI' : M.Indep (insert x I)), x ∈ I
Tactic: refine ⟨x, ⟨hxE, fun hI' ↦ ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hI' : M.Indep (insert x I)
⊢ x ∈ I
have mp : ∀ (y : α) (hyI : y ∈ I) (hfy : f y = f x), x ∈ I
Tactic: obtain ⟨y, hyI, hfy⟩ := h2 _ hI' image_insert_eq.symm
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hI' : M.Indep (insert x I)
y : α
hyI : y ∈ I
hfy : f y = f x
⊢ x ∈ I
have hfy₁ : y = x
Tactic: rw [hf.eq_iff (hI.subset_ground hyI) hxE] at hfy
Cleared hypotheses: hfy
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
⊢ (∃ x_1 ∈ M.E, f x_1 = f x) ∧ ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
have mpr : ∀ (J : Set α) (hJ : M.Indep J) (hJI : insert (f x) (f '' I) = f '' J), M.Indep (insert x I)
Tactic: refine ⟨⟨x, hxE, rfl⟩, fun J hJ hJI ↦ ⟨x, hxi ?_, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJ : M.Indep J
hJI : insert (f x) (f '' I) = f '' J
⊢ M.Indep (insert x I)
have hJ₁ : (M.map f hf).Indep (f '' J)
Tactic: replace hJ := hJ.map f hf
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : (M.map f hf).Indep (f '' J)
⊢ M.Indep (insert x I)
have hrw : f '' insert x I = f '' J
Tactic: have hrw := image_insert_eq ▸ hJI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : (M.map f hf).Indep (f '' J)
hrw : f '' insert x I = f '' J
⊢ M.Indep (insert x I)
have mpr : ∀ (hJ : (M.map f hf).Indep (f '' insert x I)) (hrw : f '' insert x I = f '' J), M.Indep (insert x I)
Tactic: rwa [← hrw, map_image_indep_iff (insert_subset hxE hI.subset_ground)] at hJ
Cleared hypotheses: hJ, hrw