chore(Data/Matroid): refactoring ext lemmas (#19664)

Co-authored-by: madvorak <dvorakmartinbridge@seznam.cz>

Author: madvorak

Mathlib/Data/Matroid/Basic.lean

@@ -189,7 +189,7 @@ def Matroid.ExistsMaximalSubsetProperty {α : Type _} (P : Set α → Prop) (X :
   use `Matroid.ofBase` or a variant. If just the independent sets are known,
   define an `IndepMatroid`, and then use `IndepMatroid.matroid`.
   -/
-@[ext] structure Matroid (α : Type _) where
+structure Matroid (α : Type _) where
   /-- `M` has a ground set `E`. -/
   (E : Set α)
   /-- `M` has a predicate `Base` defining its bases. -/
@@ -209,6 +209,8 @@ def Matroid.ExistsMaximalSubsetProperty {α : Type _} (P : Set α → Prop) (X :
   /-- Every base is contained in the ground set. -/
   (subset_ground : ∀ B, Base B → B ⊆ E)
 
+attribute [local ext] Matroid
+
 namespace Matroid
 
 variable {α : Type*} {M : Matroid α}
@@ -460,13 +462,19 @@ theorem Base.diff_infinite_comm (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) :
     (B₁ \ B₂).Infinite ↔ (B₂ \ B₁).Infinite :=
   infinite_iff_infinite_of_encard_eq_encard (hB₁.encard_diff_comm hB₂)
 
-theorem eq_of_base_iff_base_forall {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E)
+theorem ext_base {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E)
     (h : ∀ ⦃B⦄, B ⊆ M₁.E → (M₁.Base B ↔ M₂.Base B)) : M₁ = M₂ := by
   have h' : ∀ B, M₁.Base B ↔ M₂.Base B :=
     fun B ↦ ⟨fun hB ↦ (h hB.subset_ground).1 hB,
       fun hB ↦ (h <| hB.subset_ground.trans_eq hE.symm).2 hB⟩
   ext <;> simp [hE, M₁.indep_iff', M₂.indep_iff', h']
 
+@[deprecated (since := "2024-12-25")] alias eq_of_base_iff_base_forall := ext_base
+
+theorem ext_iff_base {M₁ M₂ : Matroid α} :
+    M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ ⦃B⦄, B ⊆ M₁.E → (M₁.Base B ↔ M₂.Base B) :=
+  ⟨fun h ↦ by simp [h], fun ⟨hE, h⟩ ↦ ext_base hE h⟩
+
 theorem base_compl_iff_maximal_disjoint_base (hB : B ⊆ M.E := by aesop_mat) :
     M.Base (M.E \ B) ↔ Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) B := by
   simp_rw [maximal_iff, and_iff_right hB, and_imp, forall_exists_index]
@@ -663,22 +671,35 @@ theorem ground_indep_iff_base : M.Indep M.E ↔ M.Base M.E :=
 
 theorem Base.exists_insert_of_ssubset (hB : M.Base B) (hIB : I ⊂ B) (hB' : M.Base B') :
     ∃ e ∈ B' \ I, M.Indep (insert e I) :=
-(hB.indep.subset hIB.subset).exists_insert_of_not_base
+  (hB.indep.subset hIB.subset).exists_insert_of_not_base
     (fun hI ↦ hIB.ne (hI.eq_of_subset_base hB hIB.subset)) hB'
 
-theorem eq_of_indep_iff_indep_forall {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E)
-    (h : ∀ I, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)) : M₁ = M₂ :=
+@[ext] theorem ext_indep {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E)
+    (h : ∀ ⦃I⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)) : M₁ = M₂ :=
   have h' : M₁.Indep = M₂.Indep := by
     ext I
     by_cases hI : I ⊆ M₁.E
     · rwa [h]
     exact iff_of_false (fun hi ↦ hI hi.subset_ground)
       (fun hi ↦ hI (hi.subset_ground.trans_eq hE.symm))
-  eq_of_base_iff_base_forall hE (fun B _ ↦ by simp_rw [base_iff_maximal_indep, h'])
+  ext_base hE (fun B _ ↦ by simp_rw [base_iff_maximal_indep, h'])
+
+@[deprecated (since := "2024-12-25")] alias eq_of_indep_iff_indep_forall := ext_indep
 
-theorem eq_iff_indep_iff_indep_forall {M₁ M₂ : Matroid α} :
-    M₁ = M₂ ↔ (M₁.E = M₂.E) ∧ ∀ I, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I) :=
-⟨fun h ↦ by (subst h; simp), fun h ↦ eq_of_indep_iff_indep_forall h.1 h.2⟩
+theorem ext_iff_indep {M₁ M₂ : Matroid α} :
+    M₁ = M₂ ↔ (M₁.E = M₂.E) ∧ ∀ ⦃I⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I) :=
+⟨fun h ↦ by (subst h; simp), fun h ↦ ext_indep h.1 h.2⟩
+
+@[deprecated (since := "2024-12-25")] alias eq_iff_indep_iff_indep_forall := ext_iff_indep
+
+/-- If every base of `M₁` is independent in `M₂` and vice versa, then `M₁ = M₂`. -/
+lemma ext_base_indep {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (hM₁ : ∀ ⦃B⦄, M₁.Base B → M₂.Indep B)
+    (hM₂ : ∀ ⦃B⦄, M₂.Base B → M₁.Indep B) : M₁ = M₂ := by
+  refine ext_indep hE fun I hIE ↦ ⟨fun hI ↦ ?_, fun hI ↦ ?_⟩
+  · obtain ⟨B, hB, hIB⟩ := hI.exists_base_superset
+    exact (hM₁ hB).subset hIB
+  obtain ⟨B, hB, hIB⟩ := hI.exists_base_superset
+  exact (hM₂ hB).subset hIB
 
 /-- A `Finitary` matroid is one where a set is independent if and only if it all
   its finite subsets are independent, or equivalently a matroid whose circuits are finite. -/
@@ -1003,7 +1024,7 @@ theorem finite_setOf_matroid {E : Set α} (hE : E.Finite) : {M : Matroid α | M.
   have hf : f.Injective := by
     refine fun M M' hMM' ↦ ?_
     rw [Prod.mk.injEq, and_comm, Set.ext_iff, and_comm] at hMM'
-    exact eq_of_base_iff_base_forall hMM'.1 (fun B _ ↦ hMM'.2 B)
+    exact ext_base hMM'.1 (fun B _ ↦ hMM'.2 B)
   rw [← Set.finite_image_iff hf.injOn]
   refine (hE.finite_subsets.prod hE.finite_subsets.finite_subsets).subset ?_
   rintro _ ⟨M, hE : M.E ⊆ E, rfl⟩

Mathlib/Data/Matroid/Closure.lean

@@ -637,7 +637,7 @@ lemma mem_closure_diff_singleton_iff_closure (he : e ∈ X) (heE : e ∈ M.E :=
 end insert
 
 lemma ext_closure {M₁ M₂ : Matroid α} (h : ∀ X, M₁.closure X = M₂.closure X) : M₁ = M₂ :=
-  eq_of_indep_iff_indep_forall (by simpa using h univ)
+  ext_indep (by simpa using h univ)
     (fun _ _ ↦ by simp_rw [indep_iff_forall_closure_diff_ne, h])
 
 
@@ -745,7 +745,7 @@ lemma ext_spanning {M M' : Matroid α} (h : M.E = M'.E)
     refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE] )
       (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
       (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))
-  rw [← dual_inj, eq_iff_indep_iff_indep_forall, dual_ground, dual_ground, and_iff_right h]
+  rw [← dual_inj, ext_iff_indep, dual_ground, dual_ground, and_iff_right h]
   intro I hIE
   rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]
 

Mathlib/Data/Matroid/Constructions.lean

@@ -55,7 +55,7 @@ def emptyOn (α : Type*) : Matroid α where
 @[simp] theorem emptyOn_indep_iff : (emptyOn α).Indep I ↔ I = ∅ := Iff.rfl
 
 theorem ground_eq_empty_iff : (M.E = ∅) ↔ M = emptyOn α := by
-  simp only [emptyOn, eq_iff_indep_iff_indep_forall, iff_self_and]
+  simp only [emptyOn, ext_iff_indep, iff_self_and]
   exact fun h ↦ by simp [h, subset_empty_iff]
 
 @[simp] theorem emptyOn_dual_eq : (emptyOn α)✶ = emptyOn α := by
@@ -92,9 +92,9 @@ def loopyOn (E : Set α) : Matroid α := emptyOn α ↾ E
   rintro rfl; apply empty_subset
 
 theorem eq_loopyOn_iff : M = loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X → X = ∅ := by
-  simp only [eq_iff_indep_iff_indep_forall, loopyOn_ground, loopyOn_indep_iff, and_congr_right_iff]
+  simp only [ext_iff_indep, loopyOn_ground, loopyOn_indep_iff, and_congr_right_iff]
   rintro rfl
-  refine ⟨fun h I hI ↦ (h I hI).1, fun h I hIE ↦ ⟨h I hIE, by rintro rfl; simp⟩⟩
+  refine ⟨fun h I hI ↦ (h hI).1, fun h I hIE ↦ ⟨h I hIE, by rintro rfl; simp⟩⟩
 
 @[simp] theorem loopyOn_base_iff : (loopyOn E).Base B ↔ B = ∅ := by
   simp [Maximal, base_iff_maximal_indep]
@@ -110,15 +110,15 @@ theorem Finite.loopyOn_finite (hE : E.Finite) : Matroid.Finite (loopyOn E) :=
   ⟨hE⟩
 
 @[simp] theorem loopyOn_restrict (E R : Set α) : (loopyOn E) ↾ R = loopyOn R := by
-  refine eq_of_indep_iff_indep_forall rfl ?_
+  refine ext_indep rfl ?_
   simp only [restrict_ground_eq, restrict_indep_iff, loopyOn_indep_iff, and_iff_left_iff_imp]
   exact fun _ h _ ↦ h
 
 theorem empty_base_iff : M.Base ∅ ↔ M = loopyOn M.E := by
   simp only [base_iff_maximal_indep, Maximal, empty_indep, le_eq_subset, empty_subset,
-    subset_empty_iff, true_implies, true_and, eq_iff_indep_iff_indep_forall, loopyOn_ground,
+    subset_empty_iff, true_implies, true_and, ext_iff_indep, loopyOn_ground,
     loopyOn_indep_iff]
-  exact ⟨fun h I _ ↦ ⟨@h _, fun hI ↦ by simp [hI]⟩, fun h I hI ↦ (h I hI.subset_ground).1 hI⟩
+  exact ⟨fun h I _ ↦ ⟨@h _, fun hI ↦ by simp [hI]⟩, fun h I hI ↦ (h hI.subset_ground).1 hI⟩
 
 theorem eq_loopyOn_or_rkPos (M : Matroid α) : M = loopyOn M.E ∨ RkPos M := by
   rw [← empty_base_iff, rkPos_iff_empty_not_base]; apply em
@@ -165,7 +165,7 @@ theorem freeOn_indep (hIE : I ⊆ E) : (freeOn E).Indep I :=
 theorem eq_freeOn_iff : M = freeOn E ↔ M.E = E ∧ M.Indep E := by
   refine ⟨?_, fun h ↦ ?_⟩
   · rintro rfl; simp [Subset.rfl]
-  simp only [eq_iff_indep_iff_indep_forall, freeOn_ground, freeOn_indep_iff, h.1, true_and]
+  simp only [ext_iff_indep, freeOn_ground, freeOn_indep_iff, h.1, true_and]
   exact fun I hIX ↦ iff_of_true (h.2.subset hIX) hIX
 
 theorem ground_indep_iff_eq_freeOn : M.Indep M.E ↔ M = freeOn M.E := by
@@ -219,7 +219,7 @@ theorem uniqueBaseOn_inter_basis (hX : X ⊆ E) : (uniqueBaseOn I E).Basis (X 
 @[simp] theorem uniqueBaseOn_dual_eq (I E : Set α) :
     (uniqueBaseOn I E)✶ = uniqueBaseOn (E \ I) E := by
   rw [← uniqueBaseOn_inter_ground_eq]
-  refine eq_of_base_iff_base_forall rfl (fun B (hB : B ⊆ E) ↦ ?_)
+  refine ext_base rfl (fun B (hB : B ⊆ E) ↦ ?_)
   rw [dual_base_iff, uniqueBaseOn_base_iff inter_subset_right, uniqueBaseOn_base_iff diff_subset,
     uniqueBaseOn_ground]
   exact ⟨fun h ↦ by rw [← diff_diff_cancel_left hB, h, diff_inter_self_eq_diff],
@@ -233,7 +233,7 @@ theorem uniqueBaseOn_inter_basis (hX : X ⊆ E) : (uniqueBaseOn I E).Basis (X 
 
 theorem uniqueBaseOn_restrict' (I E R : Set α) :
     (uniqueBaseOn I E) ↾ R = uniqueBaseOn (I ∩ R ∩ E) R := by
-  simp_rw [eq_iff_indep_iff_indep_forall, restrict_ground_eq, uniqueBaseOn_ground, true_and,
+  simp_rw [ext_iff_indep, restrict_ground_eq, uniqueBaseOn_ground, true_and,
     restrict_indep_iff, uniqueBaseOn_indep_iff', subset_inter_iff]
   tauto
 

Mathlib/Data/Matroid/Dual.lean

@@ -149,7 +149,7 @@ theorem setOf_dual_base_eq : {B | M✶.Base B} = (fun X ↦ M.E \ X) '' {B | M.B
   rwa [← h, diff_diff_cancel_left hB'.subset_ground]
 
 @[simp] theorem dual_dual (M : Matroid α) : M✶✶ = M :=
-  eq_of_base_iff_base_forall rfl (fun B (h : B ⊆ M.E) ↦
+  ext_base rfl (fun B (h : B ⊆ M.E) ↦
     by rw [dual_base_iff, dual_base_iff, dual_ground, diff_diff_cancel_left h])
 
 theorem dual_involutive : Function.Involutive (dual : Matroid α → Matroid α) := dual_dual

Mathlib/Data/Matroid/Map.lean

@@ -174,7 +174,7 @@ def comap (N : Matroid β) (f : α → β) : Matroid α :=
   simpa using hI.1.subset_ground
 
 @[simp] lemma comap_id (N : Matroid β) : N.comap id = N :=
-  eq_of_indep_iff_indep_forall rfl <| by simp [injective_id.injOn]
+  ext_indep rfl <| by simp [injective_id.injOn]
 
 lemma comap_indep_iff_of_injOn (hf : InjOn f (f ⁻¹' N.E)) :
     (N.comap f).Indep I ↔ N.Indep (f '' I) := by
@@ -276,7 +276,7 @@ lemma comapOn_base_iff_of_bijOn (h : BijOn f E N.E) :
 
 lemma comapOn_dual_eq_of_bijOn (h : BijOn f E N.E) :
     (N.comapOn E f)✶ = N✶.comapOn E f := by
-  refine eq_of_base_iff_base_forall (by simp) (fun B hB ↦ ?_)
+  refine ext_base (by simp) (fun B hB ↦ ?_)
   rw [comapOn_base_iff_of_bijOn (by simpa), dual_base_iff, comapOn_base_iff_of_bijOn h,
     dual_base_iff _, comapOn_ground_eq, and_iff_left diff_subset, and_iff_left (by simpa),
     h.injOn.image_diff_subset (by simpa), h.image_eq]
@@ -438,7 +438,7 @@ lemma map_basis_iff' {I X : Set β} {hf} :
   exact hIX.map hf
 
 @[simp] lemma map_dual {hf} : (M.map f hf)✶ = M✶.map f hf := by
-  apply eq_of_base_iff_base_forall (by simp)
+  apply ext_base (by simp)
   simp only [dual_ground, map_ground, subset_image_iff, forall_exists_index, and_imp,
     forall_apply_eq_imp_iff₂, dual_base_iff']
   intro B hB
@@ -456,18 +456,18 @@ lemma map_basis_iff' {I X : Set β} {hf} :
   rw [← dual_inj]; simp
 
 @[simp] lemma map_id : M.map id (injOn_id M.E) = M := by
-  simp [eq_iff_indep_iff_indep_forall]
+  simp [ext_iff_indep]
 
 lemma map_comap {f : α → β} (h_range : N.E ⊆ range f) (hf : InjOn f (f ⁻¹' N.E)) :
     (N.comap f).map f hf = N := by
-  refine eq_of_indep_iff_indep_forall (by simpa [image_preimage_eq_iff]) ?_
+  refine ext_indep (by simpa [image_preimage_eq_iff]) ?_
   simp only [map_ground, comap_ground_eq, map_indep_iff, comap_indep_iff, forall_subset_image_iff]
   refine fun I hI ↦ ⟨fun ⟨I₀, ⟨hI₀, _⟩, hII₀⟩ ↦ ?_, fun h ↦ ⟨_, ⟨h, hf.mono hI⟩, rfl⟩⟩
   suffices h : I₀ ⊆ f ⁻¹' N.E by rw [InjOn.image_eq_image_iff hf hI h] at hII₀; rwa [hII₀]
   exact (subset_preimage_image f I₀).trans <| preimage_mono (f := f) hI₀.subset_ground
 
 lemma comap_map {f : α → β} (hf : f.Injective) : (M.map f hf.injOn).comap f = M := by
-  simp [eq_iff_indep_iff_indep_forall, preimage_image_eq _ hf, and_iff_left hf.injOn,
+  simp [ext_iff_indep, preimage_image_eq _ hf, and_iff_left hf.injOn,
     image_eq_image hf]
 
 instance [M.Nonempty] {f : α → β} (hf) : (M.map f hf).Nonempty :=
@@ -672,7 +672,7 @@ lemma restrictSubtype_base_iff {B : Set X} : (M.restrictSubtype X).Base B ↔ M.
 lemma eq_of_restrictSubtype_eq {N : Matroid α} (hM : M.E = E) (hN : N.E = E)
     (h : M.restrictSubtype E = N.restrictSubtype E) : M = N := by
   subst hM
-  refine eq_of_indep_iff_indep_forall (by rw [hN]) (fun I hI ↦ ?_)
+  refine ext_indep (by rw [hN]) (fun I hI ↦ ?_)
   rwa [← restrictSubtype_indep_iff_of_subset hI, h, restrictSubtype_indep_iff_of_subset]
 
 @[simp] lemma restrictSubtype_dual : (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E := by

Mathlib/Data/Matroid/Restrict.lean

@@ -138,11 +138,11 @@ theorem restrict_finite {R : Set α} (hR : R.Finite) : (M ↾ R).Finite :=
   rw [Dep, restrict_indep_iff, restrict_ground_eq]; tauto
 
 @[simp] theorem restrict_ground_eq_self (M : Matroid α) : (M ↾ M.E) = M := by
-  refine eq_of_indep_iff_indep_forall rfl ?_; aesop
+  refine ext_indep rfl ?_; aesop
 
 theorem restrict_restrict_eq {R₁ R₂ : Set α} (M : Matroid α) (hR : R₂ ⊆ R₁) :
     (M ↾ R₁) ↾ R₂ = M ↾ R₂ := by
-  refine eq_of_indep_iff_indep_forall rfl ?_
+  refine ext_indep rfl ?_
   simp only [restrict_ground_eq, restrict_indep_iff, and_congr_left_iff, and_iff_left_iff_imp]
   exact fun _ h _ _ ↦ h.trans hR
 
@@ -195,7 +195,7 @@ theorem basis_restrict_iff (hR : R ⊆ M.E := by aesop_mat) :
 
 theorem restrict_eq_restrict_iff (M M' : Matroid α) (X : Set α) :
     M ↾ X = M' ↾ X ↔ ∀ I, I ⊆ X → (M.Indep I ↔ M'.Indep I) := by
-  refine ⟨fun h I hIX ↦ ?_, fun h ↦ eq_of_indep_iff_indep_forall rfl fun I (hI : I ⊆ X) ↦ ?_⟩
+  refine ⟨fun h I hIX ↦ ?_, fun h ↦ ext_indep rfl fun I (hI : I ⊆ X) ↦ ?_⟩
   · rw [← and_iff_left (a := (M.Indep I)) hIX, ← and_iff_left (a := (M'.Indep I)) hIX,
       ← restrict_indep_iff, h, restrict_indep_iff]
   rw [restrict_indep_iff, and_iff_left hI, restrict_indep_iff, and_iff_left hI, h _ hI]