mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fintype.BigOperators
/-- The product over a product type equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Fintype.prod_prod_type'`.  -/
Fintype.prod_prod_type : ∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : CommMonoid γ]
  (f : α₁ × α₂ → γ), ∏ x, f x = ∏ x, ∏ y, f (x, y)
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.NatTrans.comp_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) (X : C) {F_1 : D → D → Type uF} {carrier : D → Type w}
  {instFunLike : (X Y : D) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory D F_1]
  (x : carrier (F.obj X)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.CategoryStruct.comp α β).app X)) x =
    (CategoryTheory.ConcreteCategory.hom (β.app X)) ((CategoryTheory.ConcreteCategory.hom (α.app X)) x)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_mk : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {f : A →+* B}
  (h : ∀ (r : R), (↑↑f).toFun ((algebraMap R A) r) = (algebraMap R B) r), ⇑{ toRingHom := f, commutes' := h } = ⇑f
-- Std.Time.Duration
Std.Time.Duration.instHAddOffset_2 : HAdd Std.Time.Duration Std.Time.Hour.Offset Std.Time.Duration
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) {Z : CategoryTheory.Functor C C}
  (h_1 : CategoryTheory.Functor.id C ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.truncLEIsoTruncLT a b h).hom
      (CategoryTheory.CategoryStruct.comp (t.truncLTι b) h_1) =
    CategoryTheory.CategoryStruct.comp (t.truncLEι a) h_1
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.blocksFun_le : ∀ {n : ℕ} (c : Composition n) (i : Fin c.length), c.blocksFun i ≤ n
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_update_same : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ) (a : R), (p.update n a).coeff n = a
-- Mathlib.Data.List.Cycle
List.nextOr_cons_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α) (y x d : α), x ≠ y → (y :: xs).nextOr x d = xs.nextOr x d
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.rpow_eq_exp_mul_log : ∀ (x : ENNReal) (y : ℝ), x ^ y = (↑y * x.log).exp
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Polynomial functor for the W-type of `P`. `A` is a data-less well-founded
tree whereas, for a given `a : A`, `B a` is a valid path in tree `a` so
that `Wp.obj α` is made of a tree and a function from its valid paths to
the values it contains  -/
MvPFunctor.wp : {n : ℕ} → MvPFunctor.{u} (n + 1) → MvPFunctor.{u} n
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.instNonAssocSemiring : {α : Type u_1} →
  [DecidableEq α] →
    [inst : NonAssocSemiring α] →
      [inst_1 : PartialOrder α] → [CanonicallyOrderedAdd α] → [Nontrivial α] → NonAssocSemiring (WithTop α)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_inter_add_sdiff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_inter_add_sdiff._auto_1 → μ.real (s ∩ t) + μ.real (s \ t) = μ.real s
-- Mathlib.LinearAlgebra.Matrix.IsDiag
/-- `Matrix.IsDiag.diagonal_diag` as an iff.  -/
Matrix.isDiag_iff_diagonal_diag : ∀ {α : Type u_1} {n : Type u_4} [inst : Zero α] [inst_1 : DecidableEq n] (A : Matrix n n α),
  A.IsDiag ↔ Matrix.diagonal A.diag = A
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasSum.hasSum_of_sum_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {a : α} {g : γ → α},
  (∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∑ x ∈ u', g x = ∑ b ∈ v', f b) →
    HasSum g a → HasSum f a
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- A 2-truncated quasicategory is a 2-truncated simplicial set with the properties:
* (2, 1)-filling: given two consecutive `Edge`s `e₀₁` and `e₁₂`, there exists a `CompStruct`
  with (0, 1)-edge `e₀₁` and (0, 2)-edge `e₁₂`.
* (3, 1)-filling: given three `CompStruct`s `f₃`, `f₀` and `f₂` which form a (3, 1)-horn,
  there exists a fourth `CompStruct` such that the four faces form the boundary
  ∂Δ[3] of a 3-simplex.
* (3, 2)-filling: given three `CompStruct`s `f₃`, `f₀` and `f₁` which form a (3, 2)-horn,
  there exists a fourth `CompStruct` such that the four faces form the boundary
  ∂Δ[3] of a 3-simplex.
 -/
SSet.Truncated.Quasicategory₂ : SSet.Truncated 2 → Prop
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.ediam_range : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [IsometryClass F α β] (f : F), Metric.ediam (Set.range ⇑f) = Metric.ediam Set.univ
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.instSMulCommClassTensorProduct : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing A] [inst_4 : Algebra R A], SMulCommClass S A (TensorProduct R S Ω[A⁄R])
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.lift_comp_of : ∀ {α : Type u_1} {M : Type u_4} [inst : AddMonoid M] (f : α → M), ⇑(FreeAddMonoid.lift f) ∘ FreeAddMonoid.of = f
-- Mathlib.Tactic.HaveI
/-- `haveI'` behaves like `have`, but inlines the value instead of producing a `have` term.

(This is the do-notation version of the term-mode `haveI`.)
 -/
Mathlib.Tactic.HaveI.doElemHaveI'_ : Lean.ParserDescr
-- Mathlib.Order.WellFounded
StrictMono.apply_le : ∀ {β : Type u_2} [inst : LinearOrder β] [WellFoundedGT β] {f : β → β}, StrictMono f → ∀ {x : β}, f x ≤ x
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
Monotone.le_csInf_image : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice β] [inst_1 : Preorder α] {f : α → β},
  Monotone f → ∀ {s : Set α}, s.Nonempty → ∀ {B : α}, B ∈ lowerBounds s → f B ≤ sInf (f '' s)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multispanShapeCoend_snd : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (f : CategoryTheory.Arrow J),
  (CategoryTheory.Limits.multispanShapeCoend J).snd f = f.right
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supported_eq_span_single : ∀ {α : Type u_1} (R : Type u_5) [inst : Semiring R] (s : Set α),
  Finsupp.supported R R s = Submodule.span R ((fun i => fun₀ | i => 1) '' s)
-- Std.Time.DateTime.PlainDateTime
/-- Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`.
 -/
Std.Time.PlainDate.atTime : Std.Time.PlainDate → Std.Time.PlainTime → Std.Time.PlainDateTime
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.continuousSMul : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E},
  ContinuousSMul 𝕜 (ContDiffMapSupportedIn E F n K)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → Option γ} {k : α},
  k ∈ Std.DTreeMap.filterMap f t ↔ ∃ (h : k ∈ t), (f (t.getKey k h) (Std.DTreeMap.Const.get t k h)).isSome = true
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂Congr.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') {F' : CategoryTheory.Functor C A} {G' : CategoryTheory.Functor D B} (e₁ : F ≅ F')
  (e₂ : G ≅ G') (α' : L' ⟶ G'.obj L) (β' : R.comp G' ⟶ F'.comp R')
  (hα : α = CategoryTheory.CategoryStruct.comp α' (e₂.inv.app L))
  (hβ :
    CategoryTheory.CategoryStruct.comp β (CategoryTheory.Functor.whiskerRight e₁.hom R') =
      CategoryTheory.CategoryStruct.comp (R.whiskerLeft e₂.hom) β'),
  CategoryTheory.StructuredArrow.map₂Congr α β e₁ e₂ α' β' hα hβ =
    CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.StructuredArrow.isoMk (e₁.app X.right) ⋯) ⋯
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_roc : ∀ {m n : ℤ} {i : ℕ}, (m<...=n).toList[i]! = if i < (n - m).toNat then m + 1 + ↑i else 0
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_subtype_val : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {U : TopologicalSpace.Opens M} (f : M → M') (x : ↥U),
      ChartedSpace.LiftPropAt P f ↑x ↔ ChartedSpace.LiftPropAt P (f ∘ Subtype.val) x
-- Mathlib.Order.RelIso.Basic
/-- Composition of two relation embeddings is a relation embedding.  -/
RelEmbedding.trans : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ↪r s → s ↪r t → r ↪r t
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Rat.isReal_infinitePlace : Rat.infinitePlace.IsReal
-- Mathlib.Data.Sym.Sym2
Sym2.toFinset_mk_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {x y : α}, s(x, y).toFinset = {x, y}
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A B : C)
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)] {Z : D}
  (h : F.obj A ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B))
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.SemiCartesianMonoidalCategory.fst A B)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst (F.obj A) (F.obj B)) h
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofDocElabInfo.sizeOf_spec : ∀ (i : Lean.Elab.DocElabInfo), sizeOf (Lean.Elab.Info.ofDocElabInfo i) = 1 + sizeOf i
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- Induction principle for the objects of the free category on a reflexive quiver.  -/
CategoryTheory.Cat.FreeRefl.induction : {V : Type u_1} →
  [inst : CategoryTheory.ReflQuiver V] →
    {motive : CategoryTheory.Cat.FreeRefl V → Sort u_2} →
      ((v : V) → motive (CategoryTheory.Cat.FreeRefl.mk v)) → (x : CategoryTheory.Cat.FreeRefl V) → motive x
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The property that describes how `homEquiv.symm` transforms compositions `X' ⟶ X ⟶ G Y`  -/
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : CategoryTheory.Adjunction.CoreHomEquiv F G)
  {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
  (self.homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (F.map f) ((self.homEquiv X Y).symm g)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_eq_singleton_append : ∀ {m n : ℕ}, m < n → (m...n).toArray = #[m] ++ ((m + 1)...n).toArray
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K]
  (φ ψ : K →+* ℂ), φ.comp (algebraMap k K) = ψ.comp (algebraMap k K) → ∃ σ, φ.comp ↑σ.symm = ψ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.toCocone_pt : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F),
  B.toCocone.pt = B.pt
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` reflects limits, then `F.rightOp : C ⥤ Dᵒᵖ` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimitsOfSize_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp
-- Mathlib.Topology.UniformSpace.Basic
instInfSetUniformSpace : {α : Type ua} → InfSet (UniformSpace α)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsClique.insert : ∀ {α : Type u_1} {G : SimpleGraph α} {s : Set α} {a : α},
  G.IsClique s → (∀ b ∈ s, a ≠ b → G.Adj a b) → G.IsClique (insert a s)
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.withBotCoe : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, Order.IsPredLimit x → Order.IsPredLimit ↑x
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.disjoint : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t : Set X}, Metric.AreSeparated s t → Disjoint s t
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.aevalAeval_Y : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (x y : A),
  (Polynomial.aevalAeval x y) Polynomial.X = y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_counitIso_inv_app_snd_app : ∀ {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) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (X_2 : X),
  ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).counitIso.inv.app X_1).snd.app X_2 =
    CategoryTheory.CategoryStruct.id (X_1.snd.obj X_2)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
mem_quasispectrum_iff : ∀ {R : Type u_3} {A : Type u_4} [inst : Semifield R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A} {x : R},
  x ∈ quasispectrum R a ↔ x = 0 ∨ x ∈ spectrum R a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toArray_toList : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.toList.toArray = t.toArray
-- Mathlib.AlgebraicGeometry.Restrict
/-- If `f : X ⟶ Y` is an open immersion, then for any `U : X.Opens`,
we have the isomorphism `U ≅ f ''ᵁ U`.  -/
AlgebraicGeometry.Scheme.Hom.isoImage : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      (U : X.Opens) → ↑U ≅ ↑((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_lt : ∀ {a b : UInt8}, a.toUInt64 < b.toUInt64 ↔ a < b
-- Init.Data.Nat.Gcd
Nat.gcd_dvd_gcd_of_dvd_left : ∀ {m k : ℕ} (n : ℕ), m ∣ k → m.gcd n ∣ k.gcd n
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.IsSubordinate.mono' : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} [inst : Fintype ι]
  {π : BoxIntegral.TaggedPrepartition I},
  π.IsSubordinate r₁ → (∀ J ∈ π, r₁ (π.tag J) ≤ r₂ (π.tag J)) → π.IsSubordinate r₂
-- Mathlib.Algebra.Group.Units.Opposite
isUnit_op : ∀ {M : Type u_2} [inst : Monoid M] {m : M}, IsUnit (MulOpposite.op m) ↔ IsUnit m
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.Semigrp.Hom.mk.inj : ∀ {A B : Semigrp} {hom' hom'_1 : ↑A →ₙ* ↑B}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- **Fermat's Theorem**: the derivative of a function at a local minimum equals zero.  -/
IsLocalMin.hasDerivAt_eq_zero : ∀ {f : ℝ → ℝ} {f' a : ℝ}, IsLocalMin f a → HasDerivAt f f' a → f' = 0
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.pow_zero_ne_zero : ∀ {α : Type u_1} [inst : Semiring α] [Nontrivial α] (a : α), a ^ 0 ≠ 0
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- The inclusion map (i.e., `coe`) from the sphere in `E` to `E` is analytic.  -/
contMDiff_coe_sphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {m : WithTop ℕ∞} {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)],
  ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ E) m Subtype.val
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- The **chain rule for manifolds**.  -/
HasMFDerivAt.comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {g : M' → M''} {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}
  {g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))},
  HasMFDerivAt% g (f x) g' → HasMFDerivAt% f x f' → HasMFDerivAt% (g ∘ f) x (g' ∘SL f')
-- Mathlib.Data.Nat.Factors
Nat.isChain_primeFactorsList : ∀ (n : ℕ), List.IsChain (fun x1 x2 => x1 ≤ x2) n.primeFactorsList
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensor_right_unitality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)).hom
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₁).hom
            (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₂).hom)
          h))
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_inv_app_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preregular C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPreregular A e).counitIso.inv.app X).hom.app X_1 =
    X.obj.map (e.counitIso.hom.app (Opposite.unop X_1)).op
-- Init.Conv
/-- Traverses into the right subterm of a binary operator.

In general, for an `n`-ary operator, it traverses into the last argument.
It is a synonym for `arg -1`.
 -/
Lean.Parser.Tactic.Conv.rhs : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.interSmaller.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ : Std.DHashMap.Internal.Raw₀ α β)
  (m₂ : Std.DHashMap.Raw α β),
  m₁.interSmaller m₂ =
    Std.DHashMap.Raw.fold (fun sofar k x => m₁.interSmallerFn sofar k) Std.DHashMap.Internal.Raw₀.emptyWithCapacity m₂
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- The object we're trying to show doesn't exist: A nontrivial quadratic Dirichlet character
whose L-function vanishes at `s = 1`.  -/
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar : (N : ℕ) → [NeZero N] → Type
-- Init.Data.Fin.Lemmas
Fin.le_castSucc_iff : ∀ {n : ℕ} {i : Fin (n + 1)} {j : Fin n}, i ≤ j.castSucc ↔ i < j.succ
-- Mathlib.RingTheory.IntegralDomain
/-- Every finite commutative domain is a field. More generally, commutativity is not required: this
can be found in `Mathlib/RingTheory/LittleWedderburn.lean`.  -/
Fintype.fieldOfDomain : (R : Type u_3) → [inst : CommRing R] → [IsDomain R] → [DecidableEq R] → [Fintype R] → Field R
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeAux_id : ∀ {B : Type u} [inst : Quiver B] {a : B} {b : CategoryTheory.FreeBicategory B} (p : Quiver.Path a b),
  CategoryTheory.FreeBicategory.normalizeAux p (CategoryTheory.CategoryStruct.id b) = p
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.hasIntValPattern : Lean.Meta.Match.Problem → Lean.MetaM Bool
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.LinearCnstr.toExpr : Lean.Meta.Simp.Arith.Nat.LinearCnstr → Lean.Expr
-- Std.Tactic.BVDecide.Syntax
Lean.Elab.Tactic.BVDecide.BVDecideConfig.mk : ℕ →
  Bool →
    Bool →
      Bool →
        Bool →
          Bool →
            Bool →
              Bool →
                Bool → Bool → ℕ → Bool → Lean.Elab.Tactic.BVDecide.SolverMode → Lean.Elab.Tactic.BVDecide.BVDecideConfig
-- Mathlib.CategoryTheory.HomCongr
/-- If `X` is isomorphic to `X₁` and `Y` is isomorphic to `Y₁`, then
there is a natural bijection between `X ⟶ Y` and `X₁ ⟶ Y₁`. See also `Equiv.arrowCongr`.  -/
CategoryTheory.Iso.homCongr : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y X₁ Y₁ : C} → (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁)
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.instNormedSpace : {𝕜 : Type u_1} →
  {V : Type u_3} →
    {W : Type u_4} →
      [inst : SeminormedAddCommGroup V] →
        [inst_1 : SeminormedAddCommGroup W] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : NormedSpace 𝕜 V] → [inst_4 : NormedSpace 𝕜 W] → NormedSpace 𝕜 (V →ᴬ[𝕜] W)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
/-- The functor `Karoubi (HomologicalComplex C c) ⥤ HomologicalComplex (Karoubi C) c`,
on objects.  -/
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c) →
            HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c