Bump mathlib

Author: YaelDillies

LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -104,7 +104,7 @@ protected lemma IsIndContained.isContained : G₁ ⊴ G₂ → G₁ ⊑ G₂ :=
 protected lemma Iso.isIndContained (e : G ≃g H) : G ⊴ H := ⟨e⟩
 protected lemma Iso.isIndContained' (e : G ≃g H) : H ⊴ G := e.symm.isIndContained
 
-protected lemma Subgraph.IsInduced'.isIndContained {G' : G.Subgraph} (hG' : G'.IsInduced') :
+protected lemma Subgraph.IsInduced.isIndContained {G' : G.Subgraph} (hG' : G'.IsInduced) :
     G'.coe ⊴ G :=
   ⟨{  toFun := (↑)
       inj' := Subtype.coe_injective
@@ -120,12 +120,12 @@ lemma isIndContained_of_isEmpty [IsEmpty α] : G ⊴ H :=
       map_rel_iff' := fun {a} ↦ isEmptyElim a }⟩
 
 lemma isIndContained_iff_exists_iso_subgraph :
-    G ⊴ H ↔ ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced' := by
+    G ⊴ H ↔ ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced := by
   constructor
   · rintro ⟨f⟩
     refine ⟨Subgraph.map f.toHom ⊤,
       (Subgraph.Copy.map ⟨f.toHom, f.injective⟩ _).comp Subgraph.topIso.symm, ?_⟩
-    rintro _ _ ⟨a, -, rfl⟩ ⟨b, -, rfl⟩
+    rintro _ ⟨a, -, rfl⟩ _ ⟨b, -, rfl⟩
     simp [Relation.map_apply_apply, f.injective]
   · rintro ⟨H', e, hH'⟩
     exact e.isIndContained.trans hH'.isIndContained

LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

@@ -27,16 +27,5 @@ def ofLE (h : H ≤ G) : G.Subgraph where
   edge_vert _ := Set.mem_univ _
   symm := H.symm
 
-open scoped Classical
-
-/-- A subgraph is called an *induced subgraph* if vertices of `G'` are adjacent if they are adjacent
-in `G`. -/
-def IsInduced' (G' : Subgraph G) : Prop :=
-  ∀ ⦃v w⦄, v ∈ G'.verts → w ∈ G'.verts → G.Adj v w → G'.Adj v w
-
-@[simp] protected lemma IsInduced'.adj {G' : G.Subgraph} (hG' : G'.IsInduced') {a b : G'.verts} :
-    G'.Adj a b ↔ G.Adj a b :=
-  ⟨coe_adj_sub _ _ _, hG' a.2 b.2⟩
-
 end Subgraph
 end SimpleGraph

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3543cd86729039b24e8ac9551a954830f1b28053",
+   "rev": "eab98761167237d45662033394ebd5ee28613aac",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,