mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.FLT.Three
/-- `Solution'` is a tuple given by a solution to `a ^ 3 + b ^ 3 = u * c ^ 3`,
where `a`, `b`, `c` and `u` are as in `FermatLastTheoremForThreeGen`.
See `Solution` for the actual structure on which we will do the descent.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution' : {K : Type u_1} → [inst : Field K] → {ζ : K} → IsPrimitiveRoot ζ 3 → Type u_1
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.ae_le_set_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {I : Set ι}
  {s t : (i : ι) → Set (α i)}, (∀ i ∈ I, s i ≤ᵐ[μ i] t i) → I.pi s ≤ᵐ[MeasureTheory.Measure.pi μ] I.pi t
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- Append `Fin m ↪ ofFixingSubgroup M s` at the end of an enumeration of `s`.  -/
SubAddAction.ofFixingAddSubgroup.append : {M : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        {s : Set α} → {n : ℕ} → [Finite ↑s] → (Fin n ↪ ↥(SubAddAction.ofFixingAddSubgroup M s)) → Fin (s.ncard + n) ↪ α
-- Mathlib.Control.Random
/-- Generate a random `Fin`.  -/
Random.randFin : {m : Type → Type u_1} → [Monad m] → {g : Type} → {n : ℕ} → [NeZero n] → [RandomGen g] → RandGT g m (Fin n)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.FormatterM.orElse : {α : Type} →
  Lean.PrettyPrinter.FormatterM α → (Unit → Lean.PrettyPrinter.FormatterM α) → Lean.PrettyPrinter.FormatterM α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} {fallback : Unit},
  Std.DTreeMap.Const.getD (Std.DTreeMap.Const.unitOfList l cmp) k fallback = ()
-- Mathlib.Order.Hom.WithTopBot
WithBot.toDualTopEquiv_coe : ∀ {α : Type u_1} [inst : LE α] (a : α), WithBot.toDualTopEquiv ↑(OrderDual.toDual a) = OrderDual.toDual ↑a
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOnFilter.congr : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {p' : Filter α} {F' : ι → α → β},
  TendstoUniformlyOnFilter F f p p' →
    (∀ᶠ (n : ι × α) in p ×ˢ p', F n.1 n.2 = F' n.1 n.2) → TendstoUniformlyOnFilter F' f p p'
-- Mathlib.Analysis.Normed.Module.Dual
NormedSpace.eq_zero_of_forall_dual_eq_zero : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E},
  (∀ (f : StrongDual 𝕜 E), f x = 0) → x = 0
-- Lean.Linter.Init
Lean.Linter.instInhabitedLinterSetsState.default : Lean.Linter.LinterSetsState
-- Mathlib.Tactic.FunProp.Theorems
/-- priority  -/
Mathlib.Meta.FunProp.FunctionTheorem.priority : Mathlib.Meta.FunProp.FunctionTheorem → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The multispan associated to `I : MultispanIndex`.  -/
CategoryTheory.Limits.MultispanIndex.multispan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      CategoryTheory.Limits.MultispanIndex J C → CategoryTheory.Functor (CategoryTheory.Limits.WalkingMultispan J) C
-- Mathlib.Algebra.Group.Conj
ConjClasses.one_eq_mk_one : ∀ {α : Type u} [inst : Monoid α], 1 = ConjClasses.mk 1
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.instIsTriangulatedHomologicalKernel : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological], F.homologicalKernel.IsTriangulated
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsShortComplex_X₃ : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{w, u, v} k G) (S : Subgroup G)
  [inst_2 : S.Normal], (A.coinvariantsShortComplex S).X₃ = A.toCoinvariants S
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_subset_support : ∀ {V : Type u} (G : SimpleGraph V) (v : V), G.neighborSet v ⊆ G.support
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoOpsRef : Type
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_eq_getKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α} {h : a ∈ t}, t.getKey a h = t.getKeyD a fallback
-- Mathlib.Data.ENat.Lattice
/-- **Alias** of `ENat.iInf_natCast_lt_top`. -/
ENat.iInf_coe_lt_top : ∀ {ι : Sort u_1} {f : ι → ℕ}, ⨅ i, ↑(f i) < ⊤ ↔ Nonempty ι
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_comp_nonneg : ∀ {u : ℕ → EReal} {v : ℕ → ℕ},
  Monotone u → u ≠ ⊥ → Filter.Tendsto v Filter.atTop Filter.atTop → 0 ≤ LinearGrowth.linearGrowthInf (u ∘ v)
-- Mathlib.Data.Set.Image
Set.range_subset_singleton : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {x : α}, Set.range f ⊆ {x} ↔ f = Function.const ι x
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} → {Φ₁ Φ₂ : J.Point} → (Φ₂.fiber ⟶ Φ₁.fiber) → Φ₁.Hom Φ₂
-- Mathlib.Topology.Order.LeftRightLim
Antitone.tendsto_rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f →
    ∀ [inst_4 : TopologicalSpace α] [OrderTopology α] (x : α),
      Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (Function.rightLim f x))
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.linMulLinSelfPosDef : ∀ {M : Type u_4} {A : Type u_7} [inst : AddCommMonoid M] {R : Type u_9} [inst_1 : CommSemiring R] [inst_2 : Module R M]
  [inst_3 : Semiring A] [inst_4 : LinearOrder A] [IsStrictOrderedRing A] [ExistsAddOfLE A] [inst_7 : Module R A]
  [inst_8 : SMulCommClass R A A] [inst_9 : IsScalarTower R A A] (f : M →ₗ[R] A),
  f.ker = ⊥ → (QuadraticMap.linMulLin f f).PosDef
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.mk : Lean.VisibilityMap✝ Lean.Kernel.Environment →
  Array Lean.EnvExtensionState →
    Task Lean.Kernel.Environment →
      Lean.VisibilityMap✝ Lean.AsyncConsts✝ →
        Option Lean.AsyncContext✝ →
          Option Lean.RealizationContext✝ →
            Lean.NameMap Lean.RealizationContext✝ → Task (Lean.NameMap Lean.AsyncConst✝) → Bool → Lean.Environment
-- Mathlib.Data.PNat.Defs
PNat.coe_injective : Function.Injective PNat.val
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.continuous_map : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Filter.Tendsto f (Filter.coclosedCompact X) (Filter.coclosedCompact Y) → Continuous (OnePoint.map f)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instFromJsonErrorCode : Lean.FromJson Lean.JsonRpc.ErrorCode
-- Mathlib.CategoryTheory.Subobject.Comma
CategoryTheory.StructuredArrow.liftSubobject.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {A : CategoryTheory.StructuredArrow S T}
  (P : CategoryTheory.Subobject A.right) {q : S ⟶ T.obj (CategoryTheory.Subobject.underlying.obj P)}
  (hq : CategoryTheory.CategoryStruct.comp q (T.map P.arrow) = A.hom),
  CategoryTheory.StructuredArrow.liftSubobject P hq =
    CategoryTheory.Subobject.mk (CategoryTheory.StructuredArrow.homMk P.arrow hq)
-- Mathlib.CategoryTheory.FinCategory.AsType
CategoryTheory.FinCategory.asTypeToObjAsType_map : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : CategoryTheory.SmallCategory α] [inst_2 : CategoryTheory.FinCategory α]
  {x x_1 : CategoryTheory.FinCategory.AsType α} (a : Fin (Fintype.card (x ⟶ x_1))),
  (CategoryTheory.FinCategory.asTypeToObjAsType α).map a = (Fintype.equivFin (x ⟶ x_1)).symm a
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.llp_ofHoms_iff_hasLiftingProperty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (ι : Type u_1) [Nonempty ι] {A B X Y : C} (i : A ⟶ B)
  (p : X ⟶ Y), (CategoryTheory.MorphismProperty.ofHoms fun x => p).llp i ↔ CategoryTheory.HasLiftingProperty i p
-- Mathlib.Algebra.Lie.OfAssociative
Module.End.lie_apply : ∀ {R : Type u} [inst : CommRing R] {M : Type w} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (m : M), ⁅f, m⁆ = f m
-- Init.Data.Array.BinSearch
_private.Init.Data.Array.BinSearch.0.Array.binInsertAux.match_1.eq_1 : ∀ {α : Type u_1} (lt : α → α → Bool) (as : Array α) (k : α)
  (motive : (x x_1 : Fin as.size) → ↑x ≤ ↑x_1 → lt as[x] k = true → Sort u_2) (lo hi : Fin as.size) (h : ↑lo ≤ ↑hi)
  (w : lt as[lo] k = true)
  (h_1 : (lo hi : Fin as.size) → (h : ↑lo ≤ ↑hi) → (w : lt as[lo] k = true) → motive lo hi h w),
  (match lo, hi, h, w with
    | lo, hi, h, w => h_1 lo hi h w) =
    h_1 lo hi h w
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.isIso_toSucc_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C]
  [inst_4 : CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)],
  CategoryTheory.IsIso (CategoryTheory.OrthogonalReflection.toSucc W Z) ↔ W.isLocal Z
-- Std.Http.Data.Chunk
/-- Checks if the trailer has no headers.
 -/
Std.Http.Trailer.isEmpty : Std.Http.Trailer → Bool
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.Ref.mk.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} (gate gate_1 : ℕ)
  (e_gate : gate = gate_1) (invert invert_1 : Bool),
  invert = invert_1 →
    ∀ (hgate : gate < aig.decls.size),
      { gate := gate, invert := invert, hgate := hgate } = { gate := gate_1, invert := invert_1, hgate := ⋯ }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).getKey? k = if (f (t.get? k)).isSome = true then some k else none
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.mapToEqualizer_eq_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)) {X B : C}
  (π : X ⟶ B) [inst_1 : CategoryTheory.Limits.HasPullback π π],
  CategoryTheory.regularTopology.mapToEqualizer P π (CategoryTheory.Limits.pullback.fst π π)
      (CategoryTheory.Limits.pullback.snd π π) ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.lift (P.map π.op) ⋯)
      (CategoryTheory.Limits.Types.equalizerIso (P.map (CategoryTheory.Limits.pullback.fst π π).op)
          (P.map (CategoryTheory.Limits.pullback.snd π π).op)).hom
-- Lean.Elab.PreDefinition.Structural.IndPred
/-- Return the `i`th projection of the type `e` where `e` has `n` Ands.  -/
_private.Lean.Elab.PreDefinition.Structural.IndPred.0.Lean.Elab.Structural.andProj : ℕ → ℕ → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)],
  P.isoClosure.limitsClosure J = P.limitsClosure J
-- Mathlib.Data.Nat.Prime.Defs
/-- **Alias** of the forward direction of `Nat.Prime.dvd_mul`. -/
Nat.Prime.dvd_or_dvd : ∀ {p m n : ℕ}, Nat.Prime p → p ∣ m * n → p ∣ m ∨ p ∣ n
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_zero : Ordinal.cof 0 = 0
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.notMem_uIoc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ∉ Set.uIoc b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.DefaultConsumers.forIn'.eq_1 : ∀ {m : Type w → Type w'} {α β : Type w} [inst : Std.Iterator α m β] {n : Type x → Type x'} [inst_1 : Monad n]
  (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x)
  (PlausibleForInStep : β → γ → ForInStep γ → Prop) (it : Std.IterM m β) (init : γ) (P : β → Prop)
  (hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b)
  (f : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))),
  Std.IterM.DefaultConsumers.forIn' lift γ PlausibleForInStep it init P hP f =
    WellFounded.extrinsicFix₃ (InvImage (Std.IteratorLoop.rel α m PlausibleForInStep) fun x => (x.fst, x.snd.fst))
      (fun it acc hP recur =>
        (fun x => lift (Std.Shrink it.Step) γ x it.step) fun s =>
          match s.inflate with
          | ⟨Std.IterStep.yield it' out, h⟩ => do
            let __do_lift ← f out ⋯ acc
            match __do_lift with
              | ⟨ForInStep.yield c, h'⟩ => recur it' c ⋯ ⋯
              | ⟨ForInStep.done c, h⟩ => pure c
          | ⟨Std.IterStep.skip it', h⟩ => recur it' acc ⋯ ⋯
          | ⟨Std.IterStep.done, property⟩ => pure acc)
      it init hP
-- Lean.Language.Lean.Types
/-- Header processing task.  -/
Lean.Language.Lean.HeaderParsedState.processedSnap : Lean.Language.Lean.HeaderParsedState → Lean.Language.SnapshotTask Lean.Language.Lean.HeaderProcessedSnapshot
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNorm.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : SeminormedCommRing R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S]
  [inst_3 : SizeOf R] [inst_4 : SizeOf S] (toRingNorm : RingNorm S)
  (smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x),
  sizeOf { toRingNorm := toRingNorm, smul' := smul' } = 1 + sizeOf toRingNorm
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.preimage_Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (a b : β),
  ⇑e ⁻¹' Set.Ioo a b = Set.Ioo (e.symm a) (e.symm b)
-- Mathlib.Data.Nat.Choose.Basic
Nat.multichoose_zero_right : ∀ (n : ℕ), n.multichoose 0 = 1
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.any_mapM : ∀ {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : MonadLiftT m n] [inst_3 : Std.IteratorLoop α m m] [inst_4 : Monad m]
  [LawfulMonad m] [inst_6 : Monad n] [inst_7 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [LawfulMonadLiftT m n] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → n β'} {p : β' → Bool},
  Std.IterM.any p (Std.IterM.mapM f it) =
    Std.IterM.anyM (fun x => (fun x => { down := p x }) <$> f x) (Std.IterM.mapM pure it)
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.sub_apply : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ) (f g : AdicCompletion.AdicCauchySequence I M), ↑(f - g) n = ↑f n - ↑g n
-- Mathlib.Data.Finset.Lattice.Basic
Finset.coe_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), ↑(s₁ ∩ s₂) = ↑s₁ ∩ ↑s₂
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.ShiftSequence.leftComp_shiftIso : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  {F : CategoryTheory.Functor C A} {π : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D A} (e : π.comp H ≅ F)
  (M : Type u_4) [inst_3 : AddMonoid M] [inst_4 : CategoryTheory.HasShift C M] [inst_5 : CategoryTheory.HasShift D M]
  [inst_6 : π.CommShift M] [inst_7 : H.ShiftSequence M] (n a a' : M) (ha' : n + a = a'),
  CategoryTheory.Functor.ShiftSequence.shiftIso n a a' ha' =
    ((CategoryTheory.shiftFunctor C n).associator π (H.shift a)).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.commShiftIso π n) (H.shift a) ≪≫
        π.associator (CategoryTheory.shiftFunctor D n) (H.shift a) ≪≫ π.isoWhiskerLeft (H.shiftIso n a a' ha')
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `G` is fully faithful, whiskering the natural
transformation `H ⟶ F` with `G` yields the composition of the counit of the second adjunction with
the unit of the first adjunction.  -/
CategoryTheory.Adjunction.Triple.whiskerRight_rightToLeft_assoc : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful]
  {Z : CategoryTheory.Functor C C} (h : F.comp G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight t.rightToLeft G) h =
    CategoryTheory.CategoryStruct.comp t.adj₂.counit (CategoryTheory.CategoryStruct.comp t.adj₁.unit h)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₃₂_apply_mem_cycles₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x : G × G × G →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.d₃₂ A)) x ∈ groupHomology.cycles₂ A
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MonotoneOn.integrableOn_isCompact : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  IsCompact s → MonotoneOn f s → MeasureTheory.IntegrableOn f s μ
-- Mathlib.Order.FixedPoints
OrderHom.le_map_sSup_subset_fixedPoints : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), ∀ A ⊆ Function.fixedPoints ⇑f, sSup A ≤ f (sSup A)
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- The trivial additive group is the normal closure of a finite set of relations.  -/
AddSubgroup.IsFinitelyNormallyGenerated.bot : ∀ {G : Type u_1} [inst : AddGroup G], ⊥.IsFinitelyNormallyGenerated
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.supSpanSingleton_apply_mk : ∀ {E : Type u_4} [inst : AddCommGroup E] {F : Type u_5} [inst_1 : AddCommGroup F] {K : Type u_7} {L : Type u_8}
  [inst_2 : DivisionRing K] [inst_3 : DivisionRing L] {σ : K →+* L} [inst_4 : Module K E] [inst_5 : Module L F]
  (f : E →ₛₗ.[σ] F) (x : E) (y : F) (hx : x ∉ f.domain) (x' : E) (hx' : x' ∈ f.domain) (c : K),
  ↑(f.supSpanSingleton x y hx) ⟨x' + c • x, ⋯⟩ = ↑f ⟨x', hx'⟩ + σ c • y
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_range : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] {f : α → ZFSet.{u}} {x : ZFSet.{u}}, x ∈ ZFSet.range f ↔ ∃ i, f i = x
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.relabel_relabel : ∀ {α : Type u_1} {α_1 : Type u_2} {r1 : α → α_1} {α_2 : Type u_3} {r2 : α_2 → α} {f : Std.Sat.CNF α_2},
  Std.Sat.CNF.relabel r1 (Std.Sat.CNF.relabel r2 f) = Std.Sat.CNF.relabel (r1 ∘ r2) f
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_of_smul_tendsto_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] {ε : ι → 𝕜} {l : Filter ι} [l.NeBot],
  (∀ᶠ (n : ι) in l, ε n ≠ 0) →
    ∀ {S : Set E},
      (∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Filter.Tendsto (ε • x) l (nhds 0)) → Bornology.IsVonNBounded 𝕜 S
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k k' : α} {fallback : γ},
  m.WF →
    m.getKey? k = some k' →
      Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.filterMap f m) k fallback =
        ((Std.DHashMap.Raw.Const.get? m k).bind fun x => f k' x).getD fallback
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmopFunctor_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᴹᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.unmopFunctor C).map f = f.unmop
-- Init.Omega.IntList
/-- Returns the leading coefficient, i.e. the first non-zero entry.  -/
Lean.Omega.IntList.leading : Lean.Omega.IntList → ℤ
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_sum_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {ι : Type u_7} {s : Finset ι} {f : ι → AddMonoidAlgebra R A},
  AddMonoidAlgebra.supDegree D (∑ i ∈ s, f i) ≤ s.sup fun i => AddMonoidAlgebra.supDegree D (f i)
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.snd_comp_prod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : M →+ N) (g : M →+ P), (AddMonoidHom.snd N P).comp (f.prod g) = g
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.instIsIntegralFiberOfGeometricallyIntegral : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (s : ↥S) [AlgebraicGeometry.GeometricallyIntegral f],
  AlgebraicGeometry.IsIntegral (AlgebraicGeometry.Scheme.Hom.fiber f s)
-- Mathlib.Analysis.Analytic.Composition
Composition.blocks.hcongr_2 : ∀ (n n' : ℕ), n = n' → ∀ (self : Composition n) (self' : Composition n'), self ≍ self' → self.blocks ≍ self'.blocks
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.eLpNorm.eq_1 : ∀ {α : Type u_1} {ε : Type u_2} [inst : ENorm ε] {x : MeasurableSpace α} (f : α → ε) (p : ENNReal)
  (μ : MeasureTheory.Measure α),
  MeasureTheory.eLpNorm f p μ =
    if p = 0 then 0 else if p = ⊤ then MeasureTheory.eLpNormEssSup f μ else MeasureTheory.eLpNorm' f p.toReal μ
-- Mathlib.Analysis.Calculus.DSlope
/-- `dslope f a b` is defined as `slope f a b = (b - a)⁻¹ • (f b - f a)` for `a ≠ b` and
`deriv f a` for `a = b`.  -/
dslope : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → 𝕜 → 𝕜 → E
-- Mathlib.Algebra.Divisibility.Basic
/-- Transitivity of `RightDvd` for use in `calc` blocks.  -/
instIsTransRightDvd : ∀ {α : Type u_1} [inst : Semigroup α], IsTrans α RightDvd
-- Mathlib.Analysis.Analytic.Linear
/-- Reinterpret a bilinear map `f : E →L[𝕜] F →L[𝕜] G` as a multilinear map
`(E × F) [×2]→L[𝕜] G`. This multilinear map is the second term in the formal
multilinear series expansion of `uncurry f`. It is given by
`f.uncurryBilinear ![(x, y), (x', y')] = f x y'`.  -/
ContinuousLinearMap.uncurryBilinear : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {G : Type u_4} →
                  [inst_5 : NormedAddCommGroup G] → [inst_6 : NormedSpace 𝕜 G] → (E →L[𝕜] F →L[𝕜] G) → E × F [×2]→L[𝕜] G
-- Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
Finset.sum_inv_index : ∀ {α : Type u_1} {ι : Type u_2} [inst : AddCommMonoid α] [inst_1 : DecidableEq ι] [inst_2 : InvolutiveInv ι]
  (s : Finset ι) (f : ι → α), ∑ i ∈ s⁻¹, f i = ∑ i ∈ s, f i⁻¹
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_mul_apply_right : ∀ {R : Type u_1} {G : Type u_3} [inst : Semiring R] [inst_1 : AddGroup G] (x y : AddMonoidAlgebra R G) (g : G),
  (x * y).coeff g = y.coeff.sum fun h r => x.coeff (g + -h) * r