mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.Unitary
/-- The unitary subgroup of the units is equivalent to the unitary elements of the monoid.  -/
unitarySubgroupUnitsEquiv : {M : Type u_5} → [inst : Monoid M] → [inst_1 : StarMul M] → ↥(unitarySubgroup Mˣ) ≃* ↥(unitary M)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getKey! k' = k
-- Std.Http.Server.Handler
Std.Http.Server.StatelessHandler.mk : (Std.Http.Request Std.Http.Body.Stream → Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any)) →
  (IO.Error → Std.Async.Async Unit) → (Std.Http.Request.Head → Std.Async.Async Bool) → Std.Http.Server.StatelessHandler
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α}, k ∉ t₂ → Std.DTreeMap.Const.get! (t₁ ∪ t₂) k = Std.DTreeMap.Const.get! t₁ k
-- Lean.Parser.Term
Lean.Parser.Term.namedPattern.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Set.Defs
Set.instInsert : {α : Type u} → Insert α (Set α)
-- Mathlib.Topology.Algebra.Star.LinearMap
ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : ContinuousStar E]
  [inst_13 : ContinuousStar F] (f : WithConv (E →L[R] F)),
  IsSelfAdjoint f ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
IsLeast.csInf_mem : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α}, IsLeast s a → sInf s ∈ s
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.snd_expSeries_of_smul_comm : ∀ (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [inst : Field 𝕜] [CharZero 𝕜] [inst_2 : Ring R] [inst_3 : AddCommGroup M]
  [inst_4 : Algebra 𝕜 R] [inst_5 : Module 𝕜 M] [inst_6 : Module R M] [inst_7 : Module Rᵐᵒᵖ M]
  [inst_8 : SMulCommClass R Rᵐᵒᵖ M] [inst_9 : IsScalarTower 𝕜 R M] [inst_10 : IsScalarTower 𝕜 Rᵐᵒᵖ M]
  [inst_11 : TopologicalSpace R] [inst_12 : TopologicalSpace M] [inst_13 : IsTopologicalRing R]
  [inst_14 : IsTopologicalAddGroup M] [inst_15 : ContinuousSMul R M] [inst_16 : ContinuousSMul Rᵐᵒᵖ M]
  (x : TrivSqZeroExt R M),
  MulOpposite.op x.fst • x.snd = x.fst • x.snd →
    ∀ (n : ℕ),
      ((NormedSpace.expSeries 𝕜 (TrivSqZeroExt R M) (n + 1)) fun x_1 => x).snd =
        ((NormedSpace.expSeries 𝕜 R n) fun x_1 => x.fst) • x.snd
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.mk_eq_zero : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f : CauSeq β abv},
  CauSeq.Completion.mk f = 0 ↔ f.LimZero
-- Mathlib.RingTheory.Coalgebra.TensorProduct
_private.Mathlib.RingTheory.Coalgebra.TensorProduct.0.TensorProduct.coassoc : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid A] [inst_3 : AddCommMonoid B] [inst_4 : Algebra R S] [inst_5 : Module R A]
  [inst_6 : Module S A] [inst_7 : Module R B] [inst_8 : IsScalarTower R S A] [inst_9 : Coalgebra R B]
  [inst_10 : Coalgebra S A],
  ↑(TensorProduct.assoc S (TensorProduct R A B) (TensorProduct R A B) (TensorProduct R A B)) ∘ₗ
      LinearMap.rTensor (TensorProduct R A B) CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul =
    LinearMap.lTensor (TensorProduct R A B) CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
SSet.stdSimplex.toSSetObj_app_const_zero : (CategoryTheory.ConcreteCategory.hom (SSet.stdSimplex.toSSetObjI.app (Opposite.op { len := 0 })))
    (SSet.stdSimplex.const 1 0 (Opposite.op { len := 0 })) =
  TopCat.toSSetObj₀Equiv.symm 0
-- Mathlib.Data.Sign.Defs
SignType.instNeg : Neg SignType
-- Init.Data.Vector.Lemmas
Vector.getElem_take : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n} {j : ℕ} (hi : i < min j n), (xs.take j)[i] = xs[i]
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.quasiIso_map_iff_of_preservesLeftHomology : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_5 : S₁.HasHomology]
  [inst_6 : S₂.HasHomology] [inst_7 : (F.mapShortComplex.obj S₁).HasHomology]
  [inst_8 : (F.mapShortComplex.obj S₂).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂]
  [F.ReflectsIsomorphisms],
  CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) ↔ CategoryTheory.ShortComplex.QuasiIso φ
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The structure with all data necessary for rendering a rewrite suggestion  -/
Mathlib.Tactic.LibraryRewrite.RewriteInterface : Type
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the von Mangoldt function `Λ` converges at `s` when `re s > 1`.  -/
ArithmeticFunction.LSeriesSummable_vonMangoldt : ∀ {s : ℂ}, 1 < s.re → LSeriesSummable (fun n => ↑(ArithmeticFunction.vonMangoldt n)) s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.compare_getKey?_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  Option.all (fun x => decide (cmp x k = Ordering.eq)) (t.getKey? k) = true
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.splitAtPred_false : ∀ {α : Type u_1} (L : List α), Turing.PartrecToTM2.splitAtPred (fun x => false) L = (L, none, [])
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfcHom : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] (a : A)
  (f : C(↑(spectrum 𝕜 a), 𝕜)) (ha : autoParam (p a) nnnorm_cfcHom._auto_1), ‖(cfcHom ⋯) f‖₊ = ‖f‖₊
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.instInhabited : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → Inhabited (CategoryTheory.Monad C)
-- Batteries.Util.ProofWanted
def_wanted.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.List.Palindrome
List.Palindrome.singleton : ∀ {α : Type u_1} (x : α), [x].Palindrome
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.eval₂_const_uniqueAlgEquiv_symm : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Unique σ]
  {f : Polynomial R} {φ : R →+* S} {a : S},
  MvPolynomial.eval₂ φ (fun x => a) ((MvPolynomial.uniqueAlgEquiv R σ).symm f) = Polynomial.eval₂ φ a f
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnits_mono : ∀ {M : Type u_1} [inst : AddMonoid M], Monotone AddSubgroup.ofAddUnits
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.map_le_of_mem_box : ∀ {n d : ℕ} {x : Fin n → ℕ}, x ∈ Behrend.box n d → (Behrend.map (2 * d - 1)) x ≤ ∑ i, (d - 1) * (2 * d - 1) ^ ↑i
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.distinct_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) t.keys
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `α ◫ β`  -/
Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp.mkEvalHorizontalCompNilNil : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp m] →
    Mathlib.Tactic.BicategoryLike.Structural → Mathlib.Tactic.BicategoryLike.Structural → m Lean.Expr
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_single : ∀ {R : Type u_5} [inst : CommSemiring R] [inst_1 : StarRing R] {n : Type u_8} [inst_2 : DecidableEq n]
  {B : n → Type u_9} [inst_3 : (i : n) → AddCommMonoid (B i)] [inst_4 : (i : n) → Module R (B i)]
  [inst_5 : (i : n) → StarAddMonoid (B i)] [inst_6 : ∀ (i : n), StarModule R (B i)] (i : n),
  star (WithConv.toConv (LinearMap.single R B i)) = WithConv.toConv (LinearMap.single R B i)
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₂ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ)
  (h : a + b = n) (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).inv.app X).hom₂ =
    (CategoryTheory.shiftFunctorAdd' C a b n h).inv.app X.obj₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  k ∈ Std.ExtDTreeMap.Const.alter t k f ↔ (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode : Type u → Type u
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderivWithin_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [T2Space E],
  UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 id s x = ContinuousLinearMap.id 𝕜 E
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.lift₂NatTrans_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] (L₁ : CategoryTheory.Functor C₁ D₁)
  (L₂ : CategoryTheory.Functor C₂ D₂) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂]
  [inst_7 : W₁.ContainsIdentities] [inst_8 : W₂.ContainsIdentities]
  (F₁ F₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E))
  (F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E))
  [inst_9 : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁']
  [inst_10 : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'] (τ : F₁ ⟶ F₂) (X₁ : C₁) (X₂ : C₂),
  ((CategoryTheory.Localization.lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂) =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Localization.Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂)
      (CategoryTheory.CategoryStruct.comp ((τ.app X₁).app X₂)
        (((CategoryTheory.Localization.Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂))
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.ZeroAtFilter.mul_boundedAtFilter : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedRing β] {l : Filter α} {f g : α → β},
  l.ZeroAtFilter f → l.BoundedAtFilter g → l.ZeroAtFilter (f * g)
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.instInhabitedConfig.default : Mathlib.Tactic.AtomM.Recurse.Config
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic.0.IsCovariantDerivativeOn.differenceAux.congr_simp : ∀ {𝕜 : 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] {V : M → Type u_6} [inst_6 : (x : M) → AddCommGroup (V x)]
  [inst_7 : (x : M) → Module 𝕜 (V x)] [inst_8 : (x : M) → TopologicalSpace (V x)]
  [inst_9 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  (cov cov_1 : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x),
  cov = cov_1 →
    ∀ (cov' cov'_1 : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x),
      cov' = cov'_1 →
        ∀ (a a_1 : (x : M) → V x),
          a = a_1 →
            ∀ (x : M),
              IsCovariantDerivativeOn.differenceAux✝ cov cov' a x =
                IsCovariantDerivativeOn.differenceAux✝ cov_1 cov'_1 a_1 x
-- Mathlib.Data.Set.UnionLift
/-- `iUnionLift_const` is useful for proving that `iUnionLift` is a homomorphism
of algebraic structures when defined on the Union of algebraic subobjects.
For example, it could be used to prove that the lift of a collection
of group homomorphisms on a union of subgroups preserves `1`.  -/
Set.iUnionLift_const : ∀ {α : Type u_1} {ι : Sort u_3} {β : Sort u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β}
  {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {T : Set α}
  {hT : T ⊆ Set.iUnion S} (c : ↑T) (ci : (i : ι) → ↑(S i)),
  (∀ (i : ι), ↑(ci i) = ↑c) → ∀ (cβ : β), (∀ (i : ι), f i (ci i) = cβ) → Set.iUnionLift S f hf T hT c = cβ
-- Mathlib.Algebra.CharP.Lemmas
Commute.add_pow_prime_pow_eq' : ∀ {R : Type u_1} [inst : Semiring R] {p : ℕ},
  Nat.Prime p →
    ∀ {x y : R},
      Commute x y →
        ∀ (n : ℕ),
          (x + y) ^ p ^ n =
            x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)
-- Mathlib.CategoryTheory.Limits.Creates
/-- A helper to show a functor creates colimits. In particular, if we can show
that for any limit cocone `c` for `K ⋙ F`, there is a lift of it which is
a limit and `F` reflects isomorphisms, then `F` creates colimits.
Usually, `F` creating colimits says that _any_ lift of `c` is a colimit, but
here we only need to show that our particular lift of `c` is a colimit.
 -/
CategoryTheory.LiftsToColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor C D) →
                (c : CategoryTheory.Limits.Cocone (K.comp F)) →
                  CategoryTheory.Limits.IsColimit c → Type (max (max (max u₁ v₁) v₂) w)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_insertListConst_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      (k == k') = true →
        ∀ {v : β},
          List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert →
            (k, v) ∈ toInsert →
              ∀ {h : Std.Internal.List.containsKey k' (Std.Internal.List.insertListConst l toInsert) = true},
                Std.Internal.List.getValue k' (Std.Internal.List.insertListConst l toInsert) h = v
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Helper function for collecting all singleton patterns.  -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.collectSingletons : Lean.Expr → StateT (Array (Lean.Expr × List Lean.HeadIndex)) Lean.Meta.Grind.CollectorM✝ Unit
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_mul_infiniteNeg : ∀ {x y : ℝ*}, x.InfinitePos → y.InfiniteNeg → (x * y).InfiniteNeg
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Γ_obj : ∀ (X : AlgebraicGeometry.LocallyRingedSpaceᵒᵖ),
  AlgebraicGeometry.LocallyRingedSpace.Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op ⊤)
-- Lean.Language.Basic
/-- Transformation to be applied to the snapshot.  -/
Lean.Language.TransformedSnap.transform : {α : Type} → Lean.Language.TransformedSnap α → Lean.Language.SnapshotTreeTransform
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBySet_quotient_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  (s : Set R), Module.IsTorsionBySet R (M ⧸ N) s ↔ ∀ (x : M), ∀ r ∈ s, r • x ∈ N
-- Mathlib.Order.Defs.LinearOrder
/-- The minimum function is equivalent to the one you get from `minOfLe`.  -/
LinearOrder.min_def : ∀ {α : Type u_2} [self : LinearOrder α] (a b : α), min a b = if a ≤ b then a else b
-- Mathlib.Order.Interval.Set.Fin
Fin.image_natAdd_Ioi : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.natAdd m '' Set.Ioi i = Set.Ioi (Fin.natAdd m i)
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- Auxiliary definition for differentials for `CochainComplex.of`.  -/
CochainComplex.of.d : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [CategoryTheory.Limits.HasZeroMorphisms V] →
      {α : Type u_2} →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] → [DecidableEq α] → (X : α → V) → ((n : α) → X n ⟶ X (n + 1)) → (i j : α) → X i ⟶ X j
-- Std.Http.Data.Request
/-- Collection of HTTP headers for the request (Content-Type, Authorization, etc.).
 -/
Std.Http.Request.Head.headers : Std.Http.Request.Head → Std.Http.Headers
-- Mathlib.Control.Fold
Traversable.foldl : {α β : Type u} → {t : Type u → Type u} → [Traversable t] → (α → β → α) → α → t β → α
-- Aesop.Index.RulePattern
/-- Get all substitutions of the rule patterns that match a subexpression of
the given local declaration. Subexpressions containing bound variables are not
considered.  -/
Aesop.RulePatternIndex.getInLocalDeclCore : Aesop.RulePatternSubstMap → Lean.LocalDecl → Aesop.RulePatternIndex → Aesop.BaseM Aesop.RulePatternSubstMap
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.neg : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f : α → β} {a : α} {s : Set α}, IsLocalMaxOn f s a → IsLocalMinOn (fun x => -f x) s a
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- The homology data on a short complex equipped with a splitting.  -/
CategoryTheory.ShortComplex.Splitting.homologyData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} → [CategoryTheory.Limits.HasZeroObject C] → S.Splitting → S.HomologyData
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
/-- The functoriality map between divided power algebras associated with a linear map of the
underlying modules.
Given an `R`-algebra `S`, an `S`-module `N` and an `R`-linear map `f : M →ₗ[R] N`,
this is the map `DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra S N`
sending `dp R n m` to `dp S n (f m)`.  -/
DividedPowerAlgebra.map : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (S : Type u_4) →
            [inst_3 : CommSemiring S] →
              {N : Type u_5} →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module S N] →
                      (M →ₗ[R] N) →
                        [inst_7 : Algebra R S] →
                          [IsScalarTower R S N] → DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra S N
-- Mathlib.CategoryTheory.Comma.Basic
/-- Extract the isomorphism between the right objects from an isomorphism in the comma category.  -/
CategoryTheory.Comma.rightIso : {B : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} B] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {R₁ : CategoryTheory.Functor B T} →
              {L₁ : CategoryTheory.Functor A T} → {X Y : CategoryTheory.Comma L₁ R₁} → (X ≅ Y) → (X.right ≅ Y.right)
-- Mathlib.Tactic.Algebra.Basic
Mathlib.Tactic.Algebra.Cache.mk.inj : ∀ {u : Lean.Level} {A : Q(Type u)} {sA : Q(CommSemiring «$A»)} {toCache : Mathlib.Tactic.Ring.Common.Cache sA}
  {field : Option Q(Field «$A»)} {toCache_1 : Mathlib.Tactic.Ring.Common.Cache sA} {field_1 : Option Q(Field «$A»)},
  { toCache := toCache, field := field } = { toCache := toCache_1, field := field_1 } →
    toCache = toCache_1 ∧ field = field_1
-- Init.Data.List.Lemmas
List.head?_eq_head : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.head? = some (l.head h)
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.CasesTypes.isSplit : Lean.Meta.Grind.CasesTypes → Lean.Name → Bool
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_singleton : ∀ {ι : Type u_1} {π : ι → Sort u_2} (f g : (i : ι) → π i) [inst : DecidableEq ι] (i : ι),
  {i}.piecewise f g = Function.update g i (f i)
-- Std.Data.HashMap.Basic
/-- Compares two hash maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.HashMap.beq : {α : Type u} → {x : Hashable α} → {β : Type v} → [inst : BEq α] → [BEq β] → Std.HashMap α β → Std.HashMap α β → Bool
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
multipliable_one : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β},
  Multipliable (fun x => 1) L
-- Mathlib.Algebra.Polynomial.OfFn
Polynomial.ofFn_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] (n : ℕ), (Polynomial.ofFn n) 0 = 0
-- Mathlib.Algebra.Star.SelfAdjoint
/-- An element is self-adjoint if it is equal to its star.  -/
IsSelfAdjoint : {R : Type u_1} → [Star R] → R → Prop
-- Mathlib.Algebra.Lie.Extension
/-- The Lie algebra isomorphism from the kernel of an extension to the kernel of the projection.  -/
LieAlgebra.Extension.toKer : {R : Type u_1} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : LieRing M] → [inst_4 : LieAlgebra R M] → (E : LieAlgebra.Extension R M L) → M ≃ₗ⁅R⁆ ↥E.proj.ker
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.Bool.beq_congr : ∀ (lhs rhs lhs' rhs' : Bool), lhs' = lhs → rhs' = rhs → (lhs' == rhs') = (lhs == rhs)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- For additive subgroups generated by a single element, see the simpler
`zsmul_induction_left`.  -/
AddSubgroup.closure_induction_left : ∀ {G : Type u_2} [inst : AddGroup G] {s : Set G} {p : (x : G) → x ∈ AddSubgroup.closure s → Prop},
  p 0 ⋯ →
    (∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (x + y) ⋯) →
      (∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (-x + y) ⋯) →
        ∀ {x : G} (h : x ∈ AddSubgroup.closure s), p x h
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.mk.sizeOf_spec : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] [inst_4 : SizeOf C] [inst_5 : SizeOf D] [inst_6 : SizeOf A]
  (functor : A → CategoryTheory.Functor C D)
  (shiftIso : (n a a' : A) → n + a = a' → ((functor a').comp (CategoryTheory.shiftFunctor D n) ≅ functor a))
  (shiftIso_zero : ∀ (a : A), shiftIso 0 a a ⋯ = (functor a).isoWhiskerLeft (CategoryTheory.shiftFunctorZero D A))
  (shiftIso_add :
    ∀ (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a''),
      shiftIso (m + n) a a'' ⋯ =
        (functor a'').isoWhiskerLeft (CategoryTheory.shiftFunctorAdd D m n) ≪≫
          ((functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫
            CategoryTheory.Functor.isoWhiskerRight (shiftIso m a' a'' ha'') (CategoryTheory.shiftFunctor D n) ≪≫
              shiftIso n a a' ha'),
  sizeOf { functor := functor, shiftIso := shiftIso, shiftIso_zero := shiftIso_zero, shiftIso_add := shiftIso_add } = 1