mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listDecode.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3}
  (motive : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) → Sort u_4) (n₁ : ℕ)
  (t₁ : L.Term (α ⊕ Fin n₁)) (n₂ : ℕ) (t₂ : L.Term (α ⊕ Fin n₂))
  (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ))
  (h_1 :
    (n : ℕ) →
      (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
        motive (Sum.inr (Sum.inr n.succ.succ) :: l))
  (h_2 :
    (n₁ : ℕ) →
      (t₁ : L.Term (α ⊕ Fin n₁)) →
        (n₂ : ℕ) →
          (t₂ : L.Term (α ⊕ Fin n₂)) →
            (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
              motive (Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l))
  (h_3 :
    (n : ℕ) →
      (R : L.Relations n) →
        (k : ℕ) →
          (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
            motive (Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l))
  (h_4 : (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive (Sum.inr (Sum.inr 0) :: l))
  (h_5 : (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive (Sum.inr (Sum.inr 1) :: l))
  (h_6 : (x : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive x),
  (match Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l with
    | Sum.inr (Sum.inr n.succ.succ) :: l => h_1 n l
    | Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l => h_2 n₁ t₁ n₂ t₂ l
    | Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l => h_3 n R k l
    | Sum.inr (Sum.inr 0) :: l => h_4 l
    | Sum.inr (Sum.inr 1) :: l => h_5 l
    | x => h_6 x) =
    h_2 n₁ t₁ n₂ t₂ l
-- Mathlib.Data.FinEnum.Option
_private.Mathlib.Data.FinEnum.Option.0.FinEnum.recEmptyOption.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : n.succ = 0 → motive 0) (h_2 : (n_1 : ℕ) → n.succ = n_1.succ → motive n_1.succ),
  (match cardeq : n.succ with
    | 0 => h_1 cardeq
    | n_1.succ => h_2 n_1 cardeq) =
    h_2 n ⋯
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translate_zpow : ∀ (x : ℝ) (n : ℤ),
  CircleDeg1Lift.translate (Multiplicative.ofAdd x) ^ n = CircleDeg1Lift.translate (Multiplicative.ofAdd (↑n * x))
-- Mathlib.Order.Sublattice
Sublattice.instUniqueOfIsEmpty : {α : Type u_2} → [inst : Lattice α] → [IsEmpty α] → Unique (Sublattice α)
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Subtype.pseudoMetricSpace : {α : Type u_1} → [PseudoMetricSpace α] → {p : α → Prop} → PseudoMetricSpace (Subtype p)
-- Init.Data.List.Find
List.IsPrefix.find?_eq_some : ∀ {α : Type u_1} {b : α} {l₁ l₂ : List α} {p : α → Bool},
  l₁ <+: l₂ → List.find? p l₁ = some b → List.find? p l₂ = some b
-- Std.Sat.AIG.Basic
Std.Sat.AIG.CacheHit.idx : {α : Type} → {decls : Array (Std.Sat.AIG.Decl α)} → {decl : Std.Sat.AIG.Decl α} → Std.Sat.AIG.CacheHit decls decl → ℕ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.ordered_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → List.Pairwise (fun a b => cmp a b = Ordering.lt) t.keys
-- Mathlib.Data.Part
Part.append_get_eq : ∀ {α : Type u_1} [inst : Append α] (a b : Part α) (hab : (a ++ b).Dom), (a ++ b).get hab = a.get ⋯ ++ b.get ⋯
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- An `α`-indexed chain complex is a `HomologicalComplex`
in which `d i j ≠ 0` only if `j + 1 = i`.
 -/
ChainComplex : (V : Type u) →
  [inst : CategoryTheory.Category.{v, u} V] →
    [CategoryTheory.Limits.HasZeroMorphisms V] →
      (α : Type u_2) → [AddRightCancelSemigroup α] → [One α] → Type (max (max u_2 u) v)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_3.eq_3 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (l' : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l' : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l'))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  (match Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l' with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l' => h_3 l'
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) =
    h_3 l'
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- If `G` is a subgraph of `H` then `G.minDegree ≤ H.minDegree`.  -/
SimpleGraph.minDegree_le_minDegree : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype V] {H : SimpleGraph V} [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableRel H.Adj], G ≤ H → G.minDegree ≤ H.minDegree
-- Mathlib.Data.NNReal.Defs
NNReal.instDiv : Div NNReal
-- Mathlib.Algebra.Module.LocalizedModule.Int
/-- We can clear the denominators of a finite indexed family of fractions.  -/
IsLocalizedModule.exist_integer_multiples_of_finite : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {M' : Type u_3} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [IsLocalizedModule S f] {ι : Type u_4} [Finite ι] (g : ι → M'),
  ∃ b, ∀ (i : ι), IsLocalizedModule.IsInteger f (↑b • g i)
-- Mathlib.GroupTheory.Torsion
AddCommMonoid.primaryComponent.eq_1 : ∀ (G : Type u_1) [inst : AddCommMonoid G] (p : ℕ),
  AddCommMonoid.primaryComponent G p = { carrier := {g | ∃ k, p ^ k • g = 0}, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Logic.Embedding.Set
Function.Embedding.sumSet_preimage_inl : ∀ {α : Type u_1} {s t r : Set α} (h : Disjoint s t),
  Subtype.val '' Sum.inl ⁻¹' ⇑(Function.Embedding.sumSet h) ⁻¹' r = r ∩ s
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Functor C D) [inst_3 : CategoryTheory.MonObj A]
  (X : C), (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj A X).X = A.obj X
-- Mathlib.Order.Concept
lowerPolar_union : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t₁ t₂ : Set β),
  lowerPolar r (t₁ ∪ t₂) = lowerPolar r t₁ ∩ lowerPolar r t₂
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  k ∉ t₂ → (t₁ \ t₂).getD k fallback = t₁.getD k fallback
-- Aesop.Script.GoalWithMVars
Aesop.instBEqGoalWithMVars : BEq Aesop.GoalWithMVars
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_sInf : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (S : Set (ConvexCone R M)), ↑(sInf S) = ⋂ C ∈ S, ↑C
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.leftLim : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E}, BoundedVariationOn f Set.univ → BoundedVariationOn (Function.leftLim f) Set.univ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : β k → β k} {fallback : α},
      (Std.DTreeMap.Internal.Impl.modify k f t).minKeyD fallback = t.minKeyD fallback
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertMany_nil : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m.insertMany [] = m
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff.inj : ∀ {R : Type u_8} {M : Type u_9} {inst : Semiring R} {coeff coeff_1 : M →₀ R},
  AddMonoidAlgebra.ofCoeff coeff = AddMonoidAlgebra.ofCoeff coeff_1 → coeff = coeff_1
-- Std.Time.Internal.Bounded
_private.Std.Time.Internal.Bounded.0.Int.tdiv.match_1.eq_4 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.negSucc n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_4 m n
-- Mathlib.Algebra.Star.Unitary
Unitary.star_mul_self : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (U : ↥(unitary R)), star U * U = 1
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_left_lineMap : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  dist p₁ ((AffineMap.lineMap p₁ p₂) c) = ‖c‖ * dist p₁ p₂
-- Lean.Meta.Sym.SynthInstance
Lean.Meta.Sym.synthInstance : Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_sub`. -/
CuspForm.coe_sub : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Sub F] [inst_2 : Sub β]
  [IsSubApply F α β] (f g : F), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for an atomic 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.Mor₁.of : Mathlib.Tactic.BicategoryLike.Atom₁ → Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f)
        (CategoryTheory.Limits.pullback.map
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))
        (CategoryTheory.CategoryStruct.comp i₁
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f i) h))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f)
        (CategoryTheory.Limits.pullback.map
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
      h
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- A cyclotomic extension is integral.  -/
IsCyclotomicExtension.integral : ∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [IsCyclotomicExtension S A B], Algebra.IsIntegral A B
-- Lean.Meta.Closure
Lean.Meta.Closure.ToProcessElement.mk.sizeOf_spec : ∀ (fvarId newFVarId : Lean.FVarId),
  sizeOf { fvarId := fvarId, newFVarId := newFVarId } = 1 + sizeOf fvarId + sizeOf newFVarId
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.reflectsColimitsOfShape_of_final : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄}
  [inst_4 : CategoryTheory.Category.{v₄, u₄} B] (H : CategoryTheory.Functor E B)
  [CategoryTheory.Limits.ReflectsColimitsOfShape C H], CategoryTheory.Limits.ReflectsColimitsOfShape D H
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.decidableMemCentralizer.eq_1 : ∀ {M : Type u_1} {S : Set M} [inst : AddMonoid M] (a : M) [inst_1 : Decidable (∀ b ∈ S, b + a = a + b)],
  AddSubmonoid.decidableMemCentralizer a = decidable_of_iff' (∀ g ∈ S, g + a = a + g) ⋯
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- Naturality of the strong naturality constraint.  -/
CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (self : F.StrongTrans G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b))
      (self.naturality g).hom =
    CategoryTheory.CategoryStruct.comp (self.naturality f).hom
      (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_subset_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₂ < a₁ → b₁ ≤ b₂ → Set.Ico a₁ b₁ ⊆ Set.Ioo a₂ b₂
-- Mathlib.Algebra.Algebra.Pi
Pi.algebra : (ι : Type u_1) →
  {R : Type u_2} →
    (A : ι → Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (A i)] → [(i : ι) → Algebra R (A i)] → Algebra R ((i : ι) → A i)
-- Init.Data.Order.Ord
/-- Comparison is reflexive.  -/
Std.ReflCmp.compare_self : ∀ {α : Type u} {cmp : α → α → Ordering} [self : Std.ReflCmp cmp] {a : α}, cmp a a = Ordering.eq
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.complexMeasures : Array Lean.Elab.PreDefinition →
  Lean.Elab.FixedParamPerms →
    Array (Array Lean.Name) →
      Array Lean.Elab.WF.GuessLex.RecCallWithContext → Lean.MetaM (Array (Array Lean.Elab.WF.GuessLex.BasicMeasure))
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.coe_addRight : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableAdd G] (g : G),
  ⇑(MeasurableEquiv.addRight g) = fun x => x + g
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Purity.pure.sizeOf_spec : sizeOf Lean.Compiler.LCNF.Purity.pure = 1
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.fst_natCast : ∀ {q : ℕ} (n : ℕ), (↑n).1 = ↑n
-- Mathlib.Order.Filter.Map
Filter.principal_subtype : ∀ {α : Type u_6} (s : Set α) (t : Set ↑s),
  Filter.principal t = Filter.comap Subtype.val (Filter.principal (Subtype.val '' t))
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_whiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv)
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_of_nonneg : ∀ {r : ℝ} (hr : 0 ≤ r), r.toNNReal = NNReal.mk r hr
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The structure morphism associated to a coalgebra.  -/
CategoryTheory.Comonad.Coalgebra.a : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : CategoryTheory.Comonad C} → (self : G.Coalgebra) → self.A ⟶ G.obj self.A
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.FullyFaithful.homMulEquiv_symm_apply : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.MonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal] (hF : F.FullyFaithful) (f : F.obj X ⟶ F.obj M),
  (CategoryTheory.Functor.FullyFaithful.homMulEquiv F hF).symm f = hF.preimage f
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_fract : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  ⌊Int.fract a⌋ = 0
-- Init.Data.UInt.Lemmas
UInt8.ofNat_le_iff : ∀ {n : UInt8} {m : ℕ}, m < UInt8.size → (UInt8.ofNat m ≤ n ↔ m ≤ n.toNat)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_eq_some_get!_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], t.contains a = true → t.get? a = some (t.get! a)
-- Mathlib.Data.ENNReal.Inv
ENNReal.zero_zpow_def : ∀ (n : ℤ), 0 ^ n = if n = 0 then 1 else if 0 < n then 0 else ⊤
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.of_carrier : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] (Y : ContinuousGeneratedByCat X),
  { carrier := ↑Y, str := Y.str } = Y
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.mono_of_injective : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.SurjectiveOnStalks f],
  Function.Injective ⇑f → CategoryTheory.Mono f
-- Mathlib.Data.Subtype
Subtype.symm : ∀ {α : Sort u_1} {p : α → Prop} [inst : Setoid α] {s t : Subtype p}, s ≈ t → t ≈ s
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_toIcoDiv_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a b + toIcoDiv hp a b • p = b
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.instBEqPower.beq.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Power → Lean.Grind.CommRing.Power → Sort u_1) (x x_1 : Lean.Grind.CommRing.Power)
  (h_1 :
    (a : Lean.Grind.CommRing.Var) →
      (a_1 : ℕ) → (b : Lean.Grind.CommRing.Var) → (b_1 : ℕ) → motive { x := a, k := a_1 } { x := b, k := b_1 })
  (h_2 : (x x_2 : Lean.Grind.CommRing.Power) → motive x x_2),
  (∀ (a : Lean.Grind.CommRing.Var) (a_1 : ℕ) (b : Lean.Grind.CommRing.Var) (b_1 : ℕ),
      x = { x := a, k := a_1 } → x_1 = { x := b, k := b_1 } → False) →
    (match x, x_1 with
      | { x := a, k := a_1 }, { x := b, k := b_1 } => h_1 a a_1 b b_1
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Mathlib.Data.List.Flatten
/-- We can rebracket `x ++ (l₁ ++ x) ++ (l₂ ++ x) ++ ... ++ (lₙ ++ x)` to
`(x ++ l₁) ++ (x ++ l₂) ++ ... ++ (x ++ lₙ) ++ x` where `L = [l₁, l₂, ..., lₙ]`.  -/
List.append_flatten_map_append : ∀ {α : Type u_1} (L : List (List α)) (x : List α),
  x ++ (List.map (fun x_1 => x_1 ++ x) L).flatten = (List.map (fun x_1 => x ++ x_1) L).flatten ++ x
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.lipschitzWith_ofLp : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → PseudoEMetricSpace (β i)], LipschitzWith 1 WithLp.ofLp
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.apply_coe_mem_map : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) (x : ↥S),
  f ↑x ∈ AddSubmonoid.map f S
-- Mathlib.Algebra.Algebra.Hom
AlgHom.comp_assoc : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} {D : Type v₁} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Semiring D] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra R C] [inst_8 : Algebra R D] (φ₁ : C →ₐ[R] D) (φ₂ : B →ₐ[R] C) (φ₃ : A →ₐ[R] B),
  (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)
-- Batteries.Data.List.Basic
List.initsTR.eq_1 : ∀ {α : Type u_1} (l : List α),
  l.initsTR = (List.foldr (fun a arrs => (Array.map (fun t => a :: t) arrs).push []) #[[]] l).toListRev
-- Mathlib.AlgebraicTopology.MooreComplex
AlgebraicTopology.normalizedMooreComplex_objD : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  ((AlgebraicTopology.normalizedMooreComplex C).obj X).d (n + 1) n = AlgebraicTopology.NormalizedMooreComplex.objD X n
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Eta-expanded form of `CircleIntegrable.abs`

---

Analogue of `IntervalIntegrable.abs`: If a real-valued function `f` is circle integrable, then so is
`|f|`.
 -/
CircleIntegrable.fun_abs : ∀ {c : ℂ} {R : ℝ} {f : ℂ → ℝ}, CircleIntegrable f c R → CircleIntegrable (fun i => |f i|) c R
-- Mathlib.Algebra.CharP.Two
CharTwo.list_sum_sq : ∀ {R : Type u_1} [inst : CommSemiring R] [CharP R 2] (l : List R), l.sum ^ 2 = (List.map (fun x => x ^ 2) l).sum
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.toL1_zero : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (h : MeasureTheory.Integrable 0 μ), MeasureTheory.Integrable.toL1 0 h = 0
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKey! : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → [Inhabited α] → α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = false → t[a]? = none
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_sq : ∀ (x : ℝ), Real.cos x ^ 2 = 1 / 2 + Real.cos (2 * x) / 2
-- Lean.Elab.DeclUtil
/-- Sort the given list of `usedParams` using the following order:
- If it is an explicit level in `allUserParams`, then use user-given order.
- All other levels come in lexicographic order after these.

Remark: `scopeParams` are the universe params introduced using the `universe` command. `allUserParams` contains
the universe params introduced using the `universe` command *and* the `.{...}` notation.

Remark: this function return an exception if there is an `u` not in `usedParams`, that is in `allUserParams` but not in `scopeParams`.

Remark: `scopeParams` and `allUserParams` are in reverse declaration order. That is, the head is the last declared parameter.
 -/
Lean.Elab.sortDeclLevelParams : List Lean.Name → List Lean.Name → Array Lean.Name → Except String (List Lean.Name)
-- Init.Data.Array.OfFn
Array.ofFn_getElem : ∀ {α : Type u_1} {xs : Array α}, (Array.ofFn fun i => xs[↑i]) = xs
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The additive equivalence `Cochain K L n ≃+ Cochain (K⟦a⟧) L n'` when `n + a = n'` and
the category is `R`-linear.  -/
CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (R : Type u_1) →
        [inst_2 : Ring R] →
          [inst_3 : CategoryTheory.Linear R C] →
            (K L : CochainComplex C ℤ) →
              (n a n' : ℤ) →
                n + a = n' →
                  CochainComplex.HomComplex.Cochain K L n ≃ₗ[R]
                    CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.isInitial_natCast : ∀ (n : ℕ), (↑n).IsInitial