mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_nil_eq_iff_true : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x : ℕ} (h : [] ≠ []),
  List.maxIdxOn f [] h = x ↔ True
-- Mathlib.Order.Filter.NAry
/-- Symmetric statement to `Filter.map_map₂_distrib_left`.  -/
Filter.map₂_map_left_comm : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : Filter α} {g : Filter β}
  {m : α' → β → γ} {n : α → α'} {m' : α → β → δ} {n' : δ → γ},
  (∀ (a : α) (b : β), m (n a) b = n' (m' a b)) → Filter.map₂ m (Filter.map n f) g = Filter.map n' (Filter.map₂ m' f g)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.map_nil : ∀ {α : Type u} {β : Type v} (f : α → β), Stream'.WSeq.map f Stream'.WSeq.nil = Stream'.WSeq.nil
-- Mathlib.Data.Finmap
Finmap.mem_iff : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s : Finmap β}, a ∈ s ↔ ∃ b, Finmap.lookup a s = some b
-- Mathlib.GroupTheory.Commutator.Basic
map_commutatorElement : ∀ {G : Type u_1} {G' : Type u_2} {F : Type u_3} [inst : Group G] [inst_1 : Group G'] [inst_2 : FunLike F G G']
  [MonoidHomClass F G G'] (f : F) (g₁ g₂ : G), f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- The coloring of an empty graph.  -/
SimpleGraph.Coloring.ofIsEmpty : {V : Type u} → {G : SimpleGraph V} → {α : Type u_2} → [IsEmpty V] → G.Coloring α
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
/-- Eigenvalues of a diagonal linear operator with respect to standard basis
are the diagonal entries.  -/
hasEigenvalue_toLin'_diagonal_iff : ∀ {R : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R] [Nontrivial R]
  [IsDomain R] (d : n → R) {μ : R}, Module.End.HasEigenvalue (Matrix.toLin' (Matrix.diagonal d)) μ ↔ ∃ i, d i = μ
-- Mathlib.RingTheory.RingHom.Etale
RingHom.Etale.stableUnderComposition : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => RingHom.Etale
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
/-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `Set β`.  -/
Set.mulDistribMulActionSet : {α : Type u_1} →
  {β : Type u_2} → [inst : Monoid α] → [inst_1 : Monoid β] → [MulDistribMulAction α β] → MulDistribMulAction α (Set β)
-- Mathlib.NumberTheory.FunctionField
FunctionField.algebraMap_injective : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K]
  [inst_3 : Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K],
  Function.Injective ⇑(algebraMap (Polynomial F) K)
-- Mathlib.Topology.Constructions.SumProd
Continuous.uncurry_left : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y → Z} (x : X), Continuous (Function.uncurry f) → Continuous (f x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_eq_none : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  a ∉ t → t.getKey? a = none
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.equivalenceOfReindexing_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G),
  (CategoryTheory.Limits.Cone.equivalenceOfReindexing e α).unitIso =
    CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl s.pt) ⋯) ⋯ ≪≫
      CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Limits.Cone.whiskering e.functor).rightUnitor.symm
          ((CategoryTheory.Limits.Cone.whiskering e.inverse).comp
            (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom)) ≪≫
        CategoryTheory.Functor.isoWhiskerRight
            ((CategoryTheory.Limits.Cone.whiskering e.functor).isoWhiskerLeft
              (CategoryTheory.NatIso.ofComponents
                (fun s => CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl s.pt) ⋯) ⋯))
            ((CategoryTheory.Limits.Cone.whiskering e.inverse).comp
              (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom)) ≪≫
          CategoryTheory.Functor.isoWhiskerRight
              ((CategoryTheory.Limits.Cone.whiskering e.functor).associator
                  (CategoryTheory.Limits.Cone.postcompose α.hom) (CategoryTheory.Limits.Cone.postcompose α.inv)).symm
              ((CategoryTheory.Limits.Cone.whiskering e.inverse).comp
                (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom)) ≪≫
            ((CategoryTheory.Limits.Cone.whiskering e.functor).comp
                  (CategoryTheory.Limits.Cone.postcompose α.hom)).associator
              (CategoryTheory.Limits.Cone.postcompose α.inv)
              ((CategoryTheory.Limits.Cone.whiskering e.inverse).comp
                (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom))
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.testAgainstNN_lipschitz : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.ProbabilityMeasure Ω), LipschitzWith 1 fun f => μ.toFiniteMeasure.testAgainstNN f
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.comapSubgroup_symm_apply : ∀ {G : Type u_1} [inst : Group G] {H : Type u_5} [inst_1 : Group H] (f : G ≃* H) (H_1 : Subgroup G),
  (RelIso.symm f.comapSubgroup) H_1 = Subgroup.comap (↑f.symm) H_1
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.evalInduction : Lean.Elab.Tactic.Tactic
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_rio : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : Std.PRange.Least? α] [inst_3 : LT α] [inst_4 : DecidableLT α] [inst_5 : Std.PRange.UpwardEnumerable α]
  [inst_6 : Std.Rxo.IsAlwaysFinite α] [inst_7 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Rio α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur ⋯ b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn' xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- Consider a differentiable map `v : M → E₁` to a vector bundle, over a basemap `b₁ : M → B₁`, and
another basemap `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending
differentiably on `m`, one can apply `ϕ m` to `g m`, and the resulting map is differentiable.

Note that the differentiability of `ϕ` cannot be always be stated as differentiability of a map
into a manifold, as the pullback bundles `b₁ *ᵖ E₁` and `b₂ *ᵖ E₂` only make sense when `b₁`
and `b₂` are globally smooth, but we want to apply this lemma with only local information.
Therefore, we formulate it using differentiability of `ϕ` read in coordinates.

Version for `MDifferentiableWithinAt`. We also give a version for `MDifferentiableAt`, but no
version for `MDifferentiableOn` or `MDifferentiable` as our assumption, written in coordinates,
only makes sense around a point.
 -/
MDifferentiableWithinAt.clm_apply_of_inCoordinates : ∀ {𝕜 : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {B₁ : Type u_4} {B₂ : Type u_5} {M : Type u_6} {E₁ : B₁ → Type u_7}
  {E₂ : B₂ → Type u_8} [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B₁) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B₁) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B₁) → TopologicalSpace (E₁ x)]
  [inst_7 : (x : B₂) → AddCommGroup (E₂ x)] [inst_8 : (x : B₂) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B₂) → TopologicalSpace (E₂ x)] {EB₁ : Type u_9} [inst_13 : NormedAddCommGroup EB₁]
  [inst_14 : NormedSpace 𝕜 EB₁] {HB₁ : Type u_10} [inst_15 : TopologicalSpace HB₁] {IB₁ : ModelWithCorners 𝕜 EB₁ HB₁}
  [inst_16 : TopologicalSpace B₁] [inst_17 : ChartedSpace HB₁ B₁] {EB₂ : Type u_11} [inst_18 : NormedAddCommGroup EB₂]
  [inst_19 : NormedSpace 𝕜 EB₂] {HB₂ : Type u_12} [inst_20 : TopologicalSpace HB₂] {IB₂ : ModelWithCorners 𝕜 EB₂ HB₂}
  [inst_21 : TopologicalSpace B₂] [inst_22 : ChartedSpace HB₂ B₂] {EM : Type u_13} [inst_23 : NormedAddCommGroup EM]
  [inst_24 : NormedSpace 𝕜 EM] {HM : Type u_14} [inst_25 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  [inst_26 : TopologicalSpace M] [inst_27 : ChartedSpace HM M] [inst_28 : FiberBundle F₁ E₁]
  [inst_29 : VectorBundle 𝕜 F₁ E₁] [inst_30 : FiberBundle F₂ E₂] [inst_31 : VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁}
  {b₂ : M → B₂}, ⋯
-- Init.WF
emptyWf : {α : Sort u} → WellFoundedRelation α
-- Mathlib.Data.Set.Lattice
Set.biUnion_subset_biUnion_left : ∀ {α : Type u_1} {β : Type u_2} {s s' : Set α} {t : α → Set β}, s ⊆ s' → ⋃ x ∈ s, t x ⊆ ⋃ x ∈ s', t x
-- Mathlib.Topology.MetricSpace.Similarity
Similar.comp_isometry_left : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {f : P₁ → P₃},
  Isometry f → Similar v₁ v₂ → Similar (f ∘ v₁) v₂
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLastD.match_1.splitter : {α : Type u_1} →
  (motive : List α → α → Sort u_2) →
    (x : List α) →
      (x_1 : α) → ((a₀ : α) → motive [] a₀) → ((a : α) → (as : List α) → (x : α) → motive (a :: as) x) → motive x x_1
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- The trivial group-with-zero hom is absorbing for composition.  -/
MonoidWithZeroHom.comp_one : ∀ {M₀ : Type u_1} {N₀ : Type u_2} {G₀ : Type u_3} [inst : MulZeroOneClass M₀] [inst_1 : Nontrivial M₀]
  [inst_2 : NoZeroDivisors M₀] [inst_3 : MulZeroOneClass N₀] [inst_4 : MulZeroOneClass G₀]
  [inst_5 : DecidablePred fun x => x = 0] (f : N₀ →*₀ G₀), f.comp 1 = 1
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.BinaryBicone.ofColimitCocone_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)} (ht : CategoryTheory.Limits.IsColimit t),
  (CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).snd =
    CategoryTheory.Limits.BinaryCofan.IsColimit.desc ht 0 (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAt_iff_isLittleO : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  HasDerivAt f f' x ↔ (fun x' => f x' - f x - (x' - x) • f') =o[nhds x] fun x' => x' - x
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.implicitFunctionOfComplemented_apply_image : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E}
  (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented),
  HasStrictFDerivAt.implicitFunctionOfComplemented f f' hf hf' hker (f a) 0 = a
-- Init.Data.AC
Lean.Data.AC.removeNeutrals.eq_1 : ∀ {α : Sort u_1} [info : Lean.Data.AC.ContextInformation α] (ctx : α) (x_1 : ℕ) (xs : List ℕ),
  Lean.Data.AC.removeNeutrals ctx (x_1 :: xs) =
    match Lean.Data.AC.removeNeutrals.loop ctx (x_1 :: xs) with
    | [] => [x_1]
    | ys => ys
-- Mathlib.Logic.Equiv.Fin.Rotate
finRotate_zero : finRotate 0 = Equiv.refl (Fin 0)
-- Mathlib.Data.Set.Lattice
Set.sUnion_range : ∀ {β : Type u_2} {ι : Sort u_5} (f : ι → Set β), ⋃₀ Set.range f = ⋃ x, f x
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.instIsMulCommutative_iSup : ∀ {R : Type u} [inst : NonAssocSemiring R] {ι : Type u_1} [Nonempty ι] [inst_2 : Preorder ι] [IsDirectedOrder ι]
  {S : ι →o Subsemiring R} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.mul_add_right_left_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime (z * y + x) y ↔ IsRelPrime x y
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_1.splitter : {ρ : Type} →
  {σ : String.Slice → Type} →
    {pat : ρ} →
      [inst : String.Slice.Pattern.ToForwardSearcher pat σ] →
        {s : String.Slice} →
          (motive : Std.IterM Id s.Subslice → Std.IterStep (Std.IterM Id s.Subslice) s.Subslice → Sort u_1) →
            (x : Std.IterM Id s.Subslice) →
              (x_1 : Std.IterStep (Std.IterM Id s.Subslice) s.Subslice) →
                ((currPos : s.Pos) →
                    (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                      (currPos_1 : s.Pos) →
                        (s' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                          (out : s.Subslice) →
                            motive { internalState := String.Slice.SplitIterator.operating currPos s_1 }
                              (Std.IterStep.yield { internalState := String.Slice.SplitIterator.operating currPos_1 s' }
                                out)) →
                  ((currPos : s.Pos) →
                      (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                        (out : s.Subslice) →
                          motive { internalState := String.Slice.SplitIterator.operating currPos s_1 }
                            (Std.IterStep.yield { internalState := String.Slice.SplitIterator.atEnd } out)) →
                    ((currPos : s.Pos) →
                        (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                          (currPos_1 : s.Pos) →
                            (s' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                              motive { internalState := String.Slice.SplitIterator.operating currPos s_1 }
                                (Std.IterStep.skip
                                  { internalState := String.Slice.SplitIterator.operating currPos_1 s' })) →
                      ((currPos : s.Pos) →
                          (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                            motive { internalState := String.Slice.SplitIterator.operating currPos s_1 }
                              (Std.IterStep.skip { internalState := String.Slice.SplitIterator.atEnd })) →
                        ((currPos : s.Pos) →
                            (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                              motive { internalState := String.Slice.SplitIterator.operating currPos s_1 }
                                Std.IterStep.done) →
                          ((it : Std.IterM Id s.Subslice) →
                              (out : s.Subslice) →
                                motive { internalState := String.Slice.SplitIterator.atEnd }
                                  (Std.IterStep.yield it out)) →
                            ((it : Std.IterM Id s.Subslice) →
                                motive { internalState := String.Slice.SplitIterator.atEnd } (Std.IterStep.skip it)) →
                              (Unit → motive { internalState := String.Slice.SplitIterator.atEnd } Std.IterStep.done) →
                                motive x x_1
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorph.discreteTopology_range_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocalHomeomorph f → (DiscreteTopology ↑(Set.range f) ↔ DiscreteTopology X)
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
/-- The functor `SimplexCategory.rev : SimplexCategory ⥤ SimplexCategory`
as an equivalence of category.  -/
SimplexCategory.revEquivalence : SimplexCategory ≌ SimplexCategory
-- Mathlib.Tactic.DuplicateDecls
/-- Search for duplicate definitions that aren't instances or theorems,
Also indexes on the value, not just the type.  -/
Mathlib.Tactic.DuplicateDecls.Target.defs : Mathlib.Tactic.DuplicateDecls.Target
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.vcDim.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] (𝒜 𝒜_1 : Finset (Finset α)),
  𝒜 = 𝒜_1 → 𝒜.vcDim = 𝒜_1.vcDim
-- Init.Data.Slice.Array.Lemmas
Array.toList_mkSlice_roi : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ},
  Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = List.drop (lo + 1) xs.toList
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A function is `C^(n + 1)` on a domain iff locally, it has a derivative which is `C^n`.  -/
contDiffOn_succ_iff_hasFDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞},
  n ≠ ↑⊤ →
    (ContDiffOn 𝕜 (n + 1) f s ↔
      ∀ x ∈ s,
        ∃ u ∈ nhdsWithin x (insert x s),
          (n = ⊤ → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- the natural transformations between the right components  -/
CategoryTheory.Limits.CatCospanTransformMorphism.right : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {A' : Type u₄} →
        {B' : Type u₅} →
          {C' : Type u₆} →
            [inst : CategoryTheory.Category.{v₁, u₁} A] →
              [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                  {F : CategoryTheory.Functor A B} →
                    {G : CategoryTheory.Functor C B} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} →
                                  CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ' → (ψ.right ⟶ ψ'.right)
-- Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
CategoryTheory.Functor.preservesFiniteLimits_iff_forall_exact_map_and_mono : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  CategoryTheory.Limits.PreservesFiniteLimits F ↔
    ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Mono (F.map S.f)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.funMap_sumInr : ∀ {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} {S : Type u_3} [inst : L₁.Structure S] [inst_1 : L₂.Structure S]
  {n : ℕ} (f : L₂.Functions n),
  FirstOrder.Language.Structure.funMap (Sum.inr f) = FirstOrder.Language.Structure.funMap f
-- Lean.Meta.Hint
/-- No diff: Shows no deletion of the existing source, only an insertion of the suggestion.
 -/
Lean.Meta.Hint.DiffGranularity.none : Lean.Meta.Hint.DiffGranularity
-- Init.Data.BitVec.Lemmas
BitVec.srem_eq : ∀ {w : ℕ} (x y : BitVec w),
  x.srem y =
    match x.msb, y.msb with
    | false, false => x % y
    | false, true => x % -y
    | true, false => -(-x % y)
    | true, true => -(-x % -y)
-- Mathlib.Algebra.CharP.Lemmas
CharP.char_is_prime : ∀ (R : Type u_1) [inst : Ring R] [NoZeroDivisors R] [Nontrivial R] [Finite R] (p : ℕ) [CharP R p], Nat.Prime p
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_add_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} (c : F), deriv (fun y => f y + c) x = deriv f x
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.injective : ∀ {X : SSet} {n : ℕ} (self : X.StrictSegalCore n) {x y : X.obj (Opposite.op { len := n + 1 })},
  (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) x =
      (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) y →
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) y →
      x = y
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldr_eq_foldr_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {f : α → δ → δ}
  {init : δ}, Std.TreeMap.Raw.foldr (fun a x d => f a d) init t = Array.foldr f init t.keysArray
-- Mathlib.Data.Prod.Lex
Prod.Lex.instWellFoundedLTLex : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] [WellFoundedLT α] [WellFoundedLT β],
  WellFoundedLT (Lex (α × β))
-- Mathlib.Data.List.Sigma
_private.Mathlib.Data.List.Sigma.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- Use `IndObjectPresentation.coconeIsColimit` instead.  -/
CategoryTheory.Limits.IndObjectPresentation.isColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (self : CategoryTheory.Limits.IndObjectPresentation A) → CategoryTheory.Limits.IsColimit { pt := A, ι := self.ι }
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_eq_monomial_iff : ∀ {R : Type u} [inst : CommSemiring R] {α : Type u_2} (a₁ a₂ : α →₀ ℕ) (b₁ b₂ : R),
  (MvPolynomial.monomial a₁) b₁ = (MvPolynomial.monomial a₂) b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_strictMono : StrictMono Real.sigmoid
-- Mathlib.Data.Nat.Totient
Nat.dvd_two_of_totient_le_one : ∀ {a : ℕ}, 0 < a → a.totient ≤ 1 → a ∣ 2
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.IsDetpBalanced_comm : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] {A : Matrix n n R}
  {a b : R}, A.IsDetpBalanced a b ↔ A.IsDetpBalanced b a
-- Mathlib.Analysis.Asymptotics.LinearGrowth
Monotone.linearGrowthSup_comp : ∀ {u : ℕ → EReal} {v : ℕ → ℕ} {a : EReal},
  Monotone u →
    Filter.Tendsto (fun n => ↑(v n) / ↑n) Filter.atTop (nhds a) →
      a ≠ 0 → a ≠ ⊤ → LinearGrowth.linearGrowthSup (u ∘ v) = a * LinearGrowth.linearGrowthSup u
-- Aesop.Tree.AddRapp
Aesop.AddRapp : Type
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instDivisionCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivisionCommMonoid α],
  Lex.instDivisionCommMonoid = { toDivisionMonoid := Lex.instDivisionMonoid, mul_comm := ⋯ }