mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionOntoL_apply_eq_zero_iff : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q) {x : M},
  (p.projectionOntoL q h) x = 0 ↔ x ∈ q
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
SimpleGraph.ConnectedComponent.Represents.exists_inter_eq_singleton : ∀ {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} {c : G.ConnectedComponent},
  SimpleGraph.ConnectedComponent.Represents s C → c ∈ C → ∃ x, s ∩ c.supp = {x}
-- Init.Data.Array.Sort.Lemmas
/-- If the input array is already sorted, then `mergeSort` does not change the array.
 -/
Array.mergeSort_of_pairwise : ∀ {α : Type u_1} {le : α → α → Bool} {xs : Array α},
  List.Pairwise (fun x1 x2 => le x1 x2 = true) xs.toList → xs.mergeSort le = xs
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The inclusion `Δ[1] ⟶ Λ[2, 0]` which avoids `1`.  -/
SSet.horn₂₀.ι₀₂ : SSet.stdSimplex.obj { len := 1 } ⟶ (SSet.horn 2 0).toSSet
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_update : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommGroup (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (x : (i : ι) → M₁ i) (i : ι) (v : M₁ i),
  f (Function.update x i v) = f x - f (Function.update x i (x i - v))
-- Init.Data.Nat.Basic
Nat.pow_succ : ∀ (n m : ℕ), n ^ m.succ = n ^ m * n
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Entry.global.injEq : ∀ {α : Type} (a a_1 : α),
  (Lean.ScopedEnvExtension.Entry.global a = Lean.ScopedEnvExtension.Entry.global a_1) = (a = a_1)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.sinh_ne_zero : ∀ {x : ℝ}, Real.sinh x ≠ 0 ↔ x ≠ 0
-- Mathlib.Data.Nat.Find
Nat.findGreatest_eq_iff : ∀ {m k : ℕ} {P : ℕ → Prop} [inst : DecidablePred P],
  Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} {mid : C} {ι : X ⟶ mid} {π : mid ⟶ Y}
  {ι_π : autoParam (CategoryTheory.CategoryStruct.comp ι π = f) CategoryTheory.Factorisation.ι_π._autoParam} {mid_1 : C}
  {ι_1 : X ⟶ mid_1} {π_1 : mid_1 ⟶ Y}
  {ι_π_1 : autoParam (CategoryTheory.CategoryStruct.comp ι_1 π_1 = f) CategoryTheory.Factorisation.ι_π._autoParam},
  { mid := mid, ι := ι, π := π, ι_π := ι_π } = { mid := mid_1, ι := ι_1, π := π_1, ι_π := ι_π_1 } →
    mid = mid_1 ∧ ι ≍ ι_1 ∧ π ≍ π_1
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The trivial subgroup `{0}` is normal.  -/
AddSubgroup.normal_bot : ∀ {G : Type u_1} [inst : AddGroup G], ⊥.Normal
-- Mathlib.Algebra.Group.Fin.Basic
Fin.add_lt_left_iff : ∀ {n : ℕ} {a b : Fin n}, a + b < a ↔ b.rev < a
-- Mathlib.Algebra.Module.LocalizedModule.Basic
isLocalizedModule_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (S : Submonoid R) (f : M →ₗ[R] M'),
  IsLocalizedModule S f ↔
    (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M')) ↑x)) ∧
      (∀ (y : M'), ∃ x, x.2 • y = f x.1) ∧ ∀ {x₁ x₂ : M}, f x₁ = f x₂ → ∃ c, c • x₁ = c • x₂
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.posFittingCompOf.eq_1 : ∀ (R : Type u_2) {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (x : L),
  LieModule.posFittingCompOf R M x = { toSubmodule := ⨅ k, ((LieModule.toEnd R L M) x ^ k).range, lie_mem := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C]
  {X Y : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C} (α : X ⟶ Y),
  (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C).map α =
    ((CategoryTheory.Functor.mapCommMonFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C).map α).app
      (CategoryTheory.CommMon.trivial (CategoryTheory.Discrete PUnit.{u + 1}))
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- The canonical factor `CanonicalFactor R w` has no zeros inside the ball of radius `R`.
 -/
Complex.canonicalFactor_ne_zero : ∀ {R : ℝ} {w z : ℂ}, w ∈ Metric.ball 0 R → z ∈ Metric.closedBall 0 R → z ≠ w → Complex.canonicalFactor R w z ≠ 0
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.exists_le_of_le_expect : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : Module ℚ≥0 α] [PosSMulStrictMono ℚ≥0 α] {a : α} {s : Finset ι} {f : ι → α},
  s.Nonempty → (a ≤ s.expect fun i => f i) → ∃ x ∈ s, a ≤ f x
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_subset_compl_of_subset : ∀ {α : Type u_1} {s t : Set α}, t ⊆ s → sᶜ ⊆ tᶜ
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.lieSpan_lieSpan_coe_preimage : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {s : Set L},
  LieSubalgebra.lieSpan R (↥(LieSubalgebra.lieSpan R L s)) (Subtype.val ⁻¹' s) = ⊤
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sOppSide_comm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SOppSide x y ↔ s.SOppSide y x
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.coe_prod : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (s : NonUnitalSubsemiring R) (t : NonUnitalSubsemiring S), ↑(s.prod t) = ↑s ×ˢ ↑t
-- Mathlib.Combinatorics.SimpleGraph.Prod
/-- Turn a walk on `H` into a walk on `G □ H`.  -/
SimpleGraph.Walk.boxProdRight : {α : Type u_1} →
  {β : Type u_2} →
    (G : SimpleGraph α) → {H : SimpleGraph β} → {b₁ b₂ : β} → (a : α) → H.Walk b₁ b₂ → (G □ H).Walk (a, b₁) (a, b₂)
-- Lean.Meta.RecursorInfo
_private.Lean.Meta.RecursorInfo.0.Lean.Meta.getMotiveLevel : Lean.Name → Lean.Expr → Lean.MetaM Lean.Level
-- Mathlib.Analysis.Convex.Between
/-- The closed interior of a 1-simplex is a segment between its vertices.  -/
Affine.Simplex.closedInterior_eq_affineSegment : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] (s : Affine.Simplex R P 1),
  s.closedInterior = affineSegment R (s.points 0) (s.points 1)
-- Init.Data.Int.Linear
Int.Internal.Linear.le_coeff : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.le_coeff_cert p₁ p₂ k = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0
-- Init.Data.List.Sort.Lemmas
/-- Another statement of stability of merge sort.
If `c` is a sorted sublist of `l`,
then `c` is still a sublist of `mergeSort le l`.
 -/
List.sublist_mergeSort : ∀ {α : Type u_1} {le : α → α → Bool} {xs : List α},
  (∀ (a b c : α), le a b = true → le b c = true → le a c = true) →
    (∀ (a b : α), (le a b || le b a) = true) →
      ∀ {ys : List α}, List.Pairwise (fun a b => le a b = true) ys → ys.Sublist xs → ys.Sublist (xs.mergeSort le)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k k' : α}
  {v : β},
  Array.find? (fun x => cmp x.1 k == Ordering.eq) (Std.DTreeMap.Const.toArray t) = some (k', v) ↔
    t.getKey? k = some k' ∧ Std.DTreeMap.Const.get? t k = some v
-- Mathlib.CategoryTheory.Products.Basic
/-- `fst` is the functor `(X, Y) ↦ X`.  -/
CategoryTheory.Prod.fst : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor (C × D) C
-- Mathlib.Data.List.Cycle
Cycle.reverse_coe : ∀ {α : Type u_1} (l : List α), (↑l).reverse = ↑l.reverse
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The eigenspaces of a linear operator form an independent family of subspaces of `M`.  That is,
any eigenspace has trivial intersection with the span of all the other eigenspaces.  -/
Module.End.eigenspaces_iSupIndep : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] (f : Module.End R M), iSupIndep f.eigenspace
-- Mathlib.Topology.Category.CompHaus.Frm
topCatOpToFrm_map : ∀ {X Y : TopCatᵒᵖ} (f : X ⟶ Y), topCatOpToFrm.map f = Frm.ofHom (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.unop))
-- Mathlib.Analysis.Seminorm
Seminorm.ball_mono : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] {x : E}
  {p : Seminorm 𝕜 E} {r₁ r₂ : ℝ}, r₁ ≤ r₂ → p.ball x r₁ ⊆ p.ball x r₂
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.mk_le_mk : ∀ {M : Type u_1} [inst : Add M] {s t : Set M} (h_add : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s)
  (h_add' : ∀ {a b : M}, a ∈ t → b ∈ t → a + b ∈ t),
  { carrier := s, add_mem' := h_add } ≤ { carrier := t, add_mem' := h_add' } ↔ s ⊆ t
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.types : CategoryTheory.Category.{u, u + 1} (Type u)
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.get!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] (m : Std.DHashMap.Raw α β)
  (a : α) [inst_3 : Inhabited (β a)],
  m.get! a = if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.get! ⟨m, h⟩ a else default
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Algebra.Field.Defs
DivisionRing.toRing : {K : Type u_2} → [self : DivisionRing K] → Ring K
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceOfIntLE : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- Linear isometric equivalence between the space of continuous multilinear maps with variables
indexed by `ι ⊕ ι'` and the space of continuous multilinear maps with variables indexed by `ι`
taking values in the space of continuous multilinear maps with variables indexed by `ι'`.

The forward and inverse functions are `ContinuousMultilinearMap.currySum`
and `ContinuousMultilinearMap.uncurrySum`. Use this definition only if you need
some properties of `LinearIsometryEquiv`.  -/
ContinuousMultilinearMap.currySumEquiv : (𝕜 : Type u) →
  (ι : Type v) →
    (ι' : Type v') →
      (G : Type wG) →
        (G' : Type wG') →
          [inst : Fintype ι] →
            [inst_1 : Fintype ι'] →
              [inst_2 : NontriviallyNormedField 𝕜] →
                [inst_3 : NormedAddCommGroup G] →
                  [inst_4 : NormedSpace 𝕜 G] →
                    [inst_5 : NormedAddCommGroup G'] →
                      [inst_6 : NormedSpace 𝕜 G'] →
                        ContinuousMultilinearMap 𝕜 (fun x => G) G' ≃ₗᵢ[𝕜]
                          ContinuousMultilinearMap 𝕜 (fun x => G) (ContinuousMultilinearMap 𝕜 (fun x => G) G')
-- Init.Data.Array.Lemmas
Array.toList_filter' : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} {stop : ℕ},
  stop = xs.size → (Array.filter p xs 0 stop).toList = List.filter p xs.toList
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) {Z : C} (h : S₂.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂)
      (CategoryTheory.CategoryStruct.comp h₂.homologyIso.inv h)
-- Init.Data.Array.Lex.Lemmas
_private.Init.Data.Array.Lex.Lemmas.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_of_lt_of_neg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b c : α},
  b < c → a < 0 → b + a < c
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.allLTTR.loop.match_1.splitter : (n : ℕ) →
  (motive : (x : ℕ) → x ≤ n → Sort u_1) →
    (x : ℕ) → (x_1 : x ≤ n) → ((x : 0 ≤ n) → motive 0 x) → ((i : ℕ) → (h : i + 1 ≤ n) → motive i.succ h) → motive x x_1
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
SubMulAction.instMonoid : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Monoid R] →
      [inst_1 : MulAction R M] →
        [inst_2 : Monoid M] → [IsScalarTower R M M] → [SMulCommClass R M M] → Monoid (SubMulAction R M)
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.join_map_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β},
  Measurable f →
    ∀ (μ : MeasureTheory.Measure (MeasureTheory.Measure α)),
      (MeasureTheory.Measure.map (MeasureTheory.Measure.map f) μ).join = MeasureTheory.Measure.map f μ.join
-- Lean.Structure
_private.Lean.Structure.0.Lean.mergeStructureResolutionOrders.selectParent : {m : Type → Type} → [Monad m] → Array (Array Lean.Name) → m (Bool × Lean.Name)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `k` is an epimorphism, then `k.right` is an epimorphism. In other words, `Under.forget X`
preserves epimorphisms.
The converse of `CategoryTheory.under.epi_of_epi_right`.
 -/
CategoryTheory.Under.epi_right_of_epi : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (k : f ⟶ g)
  [CategoryTheory.Epi k], CategoryTheory.Epi (CategoryTheory.Under.Hom.right k)
-- Mathlib.Topology.Constructions
Continuous.quotient_map' : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Setoid X} {t : Setoid Y}
  {f : X → Y}, Continuous f → ∀ (H : Relator.LiftFun (⇑s) (⇑t) f f), Continuous (Quotient.map' f H)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_eq_oneMore_iff_toBitVec : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.oneMore ↔
    BitVec.extractLsb' 5 3 b.toBitVec = 6#3
-- Mathlib.GroupTheory.GroupAction.Hom
/-- If additive actions of `M` and `N` on `α` commute,
then for `c : M`, `(c • · : α → α)` is an `N`-additive action homomorphism.  -/
VAddCommClass.toAddActionHom : {M : Type u_11} →
  (N : Type u_9) → (α : Type u_10) → [inst : VAdd M α] → [inst_1 : VAdd N α] → [VAddCommClass M N α] → M → α →ₑ[id] α
-- Mathlib.CategoryTheory.ObjectProperty.SiteLocal
CategoryTheory.ObjectProperty.IsLocal.mk_of_zeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsClosedUnderIsomorphisms],
  (∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)) → P.IsLocal K
-- Mathlib.Algebra.GroupWithZero.Basic
zero_pow_eq_one₀ : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {n : ℕ} [Nontrivial M₀], 0 ^ n = 1 ↔ n = 0
-- Init.System.IO
IO.FS.Metadata.mk : IO.FS.SystemTime → IO.FS.SystemTime → UInt64 → IO.FS.FileType → UInt64 → IO.FS.Metadata
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.mul_dvd_of_left_isPrimal : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsRelPrime x y → x ∣ z → y ∣ z → IsPrimal x → x * y ∣ z
-- Mathlib.Computability.ContextFreeGrammar
/-- Rewrite rules.  -/
ContextFreeGrammar.rules : {T : Type u_1} → (self : ContextFreeGrammar T) → Finset (ContextFreeRule T self.NT)
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsLocalExtr.hasLineDerivAt_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {f : E → ℝ} {a b : E} {f' : ℝ}, IsLocalExtr f a → HasLineDerivAt ℝ f f' a b → f' = 0
-- Batteries.Recycling.RBTree.Basic
/-- An empty tree.  -/
RBTree.RBNode.nil : {α : Type u} → RBTree.RBNode α
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.isAddUnit_iff_addRight_bijective : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M}, IsAddUnit a ↔ Function.Bijective fun x => x + a
-- Mathlib.SetTheory.Cardinal.SchroederBernstein
/-- **The Schröder-Bernstein Theorem**:
Given injections `α → β` and `β → α` that satisfy a pointwise property `R`, we can get a bijection
`α → β` that satisfies that same pointwise property.  -/
Function.Embedding.schroeder_bernstein_of_rel : ∀ {α : Type u} {β : Type v} {f : α → β} {g : β → α},
  Function.Injective f →
    Function.Injective g →
      ∀ (R : α → β → Prop),
        (∀ (a : α), R a (f a)) → (∀ (b : β), R (g b) b) → ∃ h, Function.Bijective h ∧ ∀ (a : α), R a (h a)
-- Init.Data.String.Lemmas.Order
String.Pos.slice_le_slice_iff : ∀ {s : String} {p₀ p₁ q r : s.Pos} {h₁ : p₀ ≤ q} {h₁' : p₀ ≤ r} {h₂ : q ≤ p₁} {h₂' : r ≤ p₁},
  q.slice p₀ p₁ h₁ h₂ ≤ r.slice p₀ p₁ h₁' h₂' ↔ q ≤ r
-- Mathlib.Order.RelIso.Basic
/-- Transport a `RelHom` across a pair of `RelIso`s, by pre- and post-composition.

This is `Equiv.arrowCongr` for `RelHom`.  -/
RelIso.relHomCongr : {α₁ : Type u_5} →
  {β₁ : Type u_6} →
    {α₂ : Type u_7} →
      {β₂ : Type u_8} →
        {r₁ : α₁ → α₁ → Prop} →
          {s₁ : β₁ → β₁ → Prop} →
            {r₂ : α₂ → α₂ → Prop} → {s₂ : β₂ → β₂ → Prop} → r₁ ≃r r₂ → s₁ ≃r s₂ → r₁ →r s₁ ≃ (r₂ →r s₂)
-- Mathlib.Analysis.Analytic.Composition
/-- The norm of `f.compAlongComposition p c` is controlled by the product of
the norms of the relevant bits of `f` and `p`.  -/
FormalMultilinearSeries.compAlongComposition_bound : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} (p : FormalMultilinearSeries 𝕜 E F)
  (c : Composition n) (f : F [×c.length]→L[𝕜] G) (v : Fin n → E),
  ‖(ContinuousMultilinearMap.compAlongComposition p c f) v‖ ≤ (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) * ∏ i, ‖v i‖
-- Mathlib.Algebra.Ring.Action.Pointwise.Set
Set.smul_set_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroup β] [inst_1 : DistribSMul α β] (a : α) (t : Set β), a • -t = -(a • t)
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.ofGradedObject_X_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂)
  (X : CategoryTheory.GradedObject (I₁ × I₂) C) (d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂))
  (d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂'))
  (shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0)
  (shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0)
  (d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₁ i₁' i₁'' i₂) = 0)
  (d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₂ i₁ i₂' i₂'') = 0)
  (comm :
    ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂),
      CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₂ i₁' i₂ i₂') =
        CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₁ i₁ i₁' i₂'))
  (i₁ : I₁) (i₂ : I₂),
  ((HomologicalComplex₂.ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).X i₁).X i₂ = X (i₁, i₂)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_eq_iSup : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] (s : Finset α) (f : α → β), s.sup f = ⨆ a ∈ s, f a
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₃.X₂ =
    CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Adjunction.toComonad_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R),
  h.toComonad.δ = CategoryTheory.Functor.whiskerRight (R.whiskerLeft h.unit) L
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, FiniteMultiplicity a b → ∀ {m : ℕ}, multiplicity a b < m → ¬a ^ m ∣ b
-- Init.Data.List.Attach
List.pmap_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} {q : β → Prop} {g : (a : α) → p a → β}
  {f : (b : β) → q b → γ} {l : List α} (H₁ : ∀ a ∈ l, p a) (H₂ : ∀ a ∈ List.pmap g l H₁, q a),
  List.pmap f (List.pmap g l H₁) H₂ = List.pmap (fun a h => f (g (↑a) h) ⋯) l.attach ⋯
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.as_sum_support_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p = ∑ i ∈ p.support, Polynomial.C (p.coeff i) * Polynomial.X ^ i
-- Mathlib.Order.Hom.Bounded
/-- Copy of a `TopHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
TopHom.copy : {α : Type u_2} →
  {β : Type u_3} → [inst : Top α] → [inst_1 : Top β] → (f : TopHom α β) → (f' : α → β) → f' = ⇑f → TopHom α β
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The determinant of `rotation` (as a linear equiv) is equal to `1`.  -/
Orientation.linearEquiv_det_rotation : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle), LinearEquiv.det (o.rotation θ).toLinearEquiv = 1
-- Lean.Parser.Command
/-- This is an auxiliary command to generate constructor injectivity theorems for
inductive types defined at `Prelude.lean`.
Temporarily also controls the generation of the `ctorIdx` definition.
It is meant for bootstrapping purposes only.  -/
Lean.Parser.Command.genInjectiveTheorems : Lean.Parser.Parser
-- Mathlib.Data.List.Rotate
List.rotate_eq_drop_append_take_mod : ∀ {α : Type u} {l : List α} {n : ℕ}, l.rotate n = List.drop (n % l.length) l ++ List.take (n % l.length) l
-- Mathlib.Topology.IsClosedRestrict
/-- Homeomorphism between the set of functions that coincide with a given set of functions away
from a given set `S`, and dependent functions away from `S` times any value on `S`.  -/
Homeomorph.preimageImageRestrict : {ι : Type u_1} →
  (α : ι → Type u_3) →
    [inst : (i : ι) → TopologicalSpace (α i)] →
      (S : Set ι) →
        (s : Set ((j : ι) → α j)) →
          ↑(Sᶜ.domRestrict ⁻¹' Sᶜ.domRestrict '' s) ≃ₜ ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)