mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.MonCat.Limits
CategoryTheory.Limits.Types.isLimitEquivSections.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.Limits.Types.isLimitEquivSections t =
    { toFun := CategoryTheory.Limits.Types.sectionOfCone c,
      invFun := fun s =>
        (CategoryTheory.ConcreteCategory.hom (t.lift (CategoryTheory.Limits.Types.coneOfSection ⋯))) PUnit.unit,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- The `PowerBasis` given by a primitive root `η`.  -/
IsPrimitiveRoot.powerBasis : {n : ℕ} →
  [NeZero n] →
    (K : Type u) →
      {L : Type v} →
        [inst : Field K] →
          [inst_1 : CommRing L] →
            [IsDomain L] →
              [inst_3 : Algebra K L] → [IsCyclotomicExtension {n} K L] → {ζ : L} → IsPrimitiveRoot ζ n → PowerBasis K L
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.out_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizationMonoid α] (a b : Associates α),
  (a * b).out = a.out * b.out
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
/-- Delaborator for `Functor.obj`  -/
CategoryTheory.CartesianClosed.delabFunctorObjExp : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.EMetricSpace.Defs
/-- The extended metric induced by an injective function taking values in an emetric space.
See Note [reducible non-instances].  -/
EMetricSpace.induced : {γ : Type u_2} → {β : Type u_3} → (f : γ → β) → Function.Injective f → EMetricSpace β → EMetricSpace γ
-- Mathlib.Data.Set.NAry
Set.image2_image_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} (f : α → γ → δ) (g : β → γ),
  Set.image2 f s (g '' t) = Set.image2 (fun a b => f a (g b)) s t
-- Lean.Compiler.LCNF.Basic
/-- We set this flag to true during LCNF conversion. When we receive
a block of functions to be compiled, we set this flag to `true`
if there is an application to the function in the block containing
it. This is an approximation, but it should be good enough because
in the frontend, we invoke the compiler with blocks of strongly connected
components only.
We use this information to control inlining.
 -/
Lean.Compiler.LCNF.Decl.recursive : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → Bool
-- Mathlib.Data.Nat.Factorial.Basic
Nat.zero_descFactorial_succ : ∀ (k : ℕ), Nat.descFactorial 0 (k + 1) = 0
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₁₂Obj_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : 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} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
  ((CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂).obj X₃ = (G.obj ((F₁₂.obj X₁).obj X₂)).obj X₃
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
hasSum_op : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {f : β → α} {a : α}, HasSum (fun a => MulOpposite.op (f a)) (MulOpposite.op a) L ↔ HasSum f a L
-- Mathlib.LinearAlgebra.InvariantBasisNumber
le_of_fin_injective : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R),
  Function.Injective ⇑f → n ≤ m
-- Init.Data.Vector.Basic
Vector.unzip : {α : Type u_1} → {β : Type u_2} → {n : ℕ} → Vector (α × β) n → Vector α n × Vector β n
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.mono_of_kernel_ι_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  CategoryTheory.Limits.kernel.ι f = 0 → CategoryTheory.Mono f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_nonpos_of_pi_div_two_le_of_le : ∀ {x : ℝ}, Real.pi / 2 ≤ x → x ≤ Real.pi + Real.pi / 2 → Real.cos x ≤ 0
-- Init.Data.UInt.Lemmas
UInt16.toNat_lt_size : ∀ (a : UInt16), a.toNat < UInt16.size
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.erase.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a a_1 : α) (b : β a_1) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.erase a (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    bif a_1 == a then es else Std.DHashMap.Internal.AssocList.cons a_1 b (Std.DHashMap.Internal.AssocList.erase a es)
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsLocallyArtinian.discreteTopology : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyArtinian X], DiscreteTopology ↥X
-- Lean.Elab.Binders
Lean.Elab.Term.LetIdDeclView.value : Lean.Elab.Term.LetIdDeclView → Lean.Syntax
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.iSup_eq_closure : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {ι : Sort u_3} (S : ι → L.Substructure M),
  ⨆ i, S i = (FirstOrder.Language.Substructure.closure L).toFun (⋃ i, ↑(S i))
-- Mathlib.Algebra.Order.Module.Defs
/-- Constructor for `IsOrderedModule` when the semimodule is in fact a module.  -/
IsOrderedModule.of_smul_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β]
  [inst_3 : PartialOrder α] [inst_4 : PartialOrder β] [IsOrderedAddMonoid α] [IsOrderedAddMonoid β],
  (∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b) → IsOrderedModule α β
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.complex_d_succ_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (P.complex.d n (n + 1)) (P.complex.d (n + 1) (n + 2)) = 0
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- Multilinear maps on `N : (ι ⊕ ι') → Type*` identify to multilinear maps
from `(fun (i : ι) ↦ N (.inl i))` taking values in the space of
linear maps on `(fun (i : ι') ↦ N (.inr i))`.  -/
MultilinearMap.currySumEquiv : {R : Type uR} →
  {ι : Type uι} →
    {ι' : Type uι'} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₂] →
            [inst_2 : Module R M₂] →
              {N : ι ⊕ ι' → Type u_1} →
                [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)] →
                  [inst_4 : (i : ι ⊕ ι') → Module R (N i)] →
                    MultilinearMap R N M₂ ≃ₗ[R]
                      MultilinearMap R (fun i => N (Sum.inl i)) (MultilinearMap R (fun i => N (Sum.inr i)) M₂)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialRightAdjointHomEquiv_symm_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} {Y Y' : F.PartialRightAdjointSource} (f : F.obj X ⟶ Y.obj) (g : Y ⟶ Y')
  {Z : C} (h : F.partialRightAdjointObj Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.partialRightAdjointHomEquiv.symm f)
      (CategoryTheory.CategoryStruct.comp (F.partialRightAdjointMap g) h) =
    CategoryTheory.CategoryStruct.comp (F.partialRightAdjointHomEquiv.symm (CategoryTheory.CategoryStruct.comp f g.hom))
      h
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.pow_zero : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.npow a 0 = Lean.Grind.Ring.OfSemiring.natCast 1
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
DirectedOn.csSup_le_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {s t : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s →
    DirectedOn (fun x1 x2 => x1 ≤ x2) t → BddAbove t → s.Nonempty → s ⊆ t → sSup s ≤ sSup t
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.rightUnitorHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : C) →
        [inst_2 : Mathlib.Tactic.Coherence.LiftObj X] →
          Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
-- Std.Data.DHashMap.AdditionalOperations
/-- Updates the values of the hash map by applying the given function to all mappings.  -/
Std.DHashMap.map : {α : Type u} →
  {β : α → Type v} →
    {δ : α → Type w} →
      [inst : BEq α] → [inst_1 : Hashable α] → ((a : α) → β a → δ a) → Std.DHashMap α β → Std.DHashMap α δ
-- Mathlib.RingTheory.Artinian.Module
instIsDedekindFiniteMonoidOfIsArtinianRing : ∀ (R : Type u_1) [inst : Semiring R] [IsArtinianRing R], IsDedekindFiniteMonoid R
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
WeakDual.CharacterSpace.coe_toNonUnitalAlgHom : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : TopologicalSpace A]
  [inst_6 : Module 𝕜 A] (φ : ↑(WeakDual.characterSpace 𝕜 A)), ⇑(WeakDual.CharacterSpace.toNonUnitalAlgHom φ) = ⇑φ
-- Mathlib.Order.BooleanAlgebra.Defs
/-- A Boolean algebra is a bounded distributive lattice with a complement operator `ᶜ` such that
`x ⊓ xᶜ = ⊥` and `x ⊔ xᶜ = ⊤`. For convenience, it must also provide a set difference operation `\`
and a Heyting implication `⇨` satisfying `x \ y = x ⊓ yᶜ` and `x ⇨ y = y ⊔ xᶜ`.

This is a generalization of (classical) logic of propositions, or the powerset lattice.

Since `BoundedOrder`, `OrderBot`, and `OrderTop` are mixins that require `LE`
to be present at define-time, the `extends` mechanism does not work with them.
Instead, we extend using the underlying `Bot` and `Top` data typeclasses, and replicate the
order axioms of those classes here. A "forgetful" instance back to `BoundedOrder` is provided.
 -/
BooleanAlgebra : Type u → Type u
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.instIsIsoToRangeOfMono : ∀ {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.IsIso (SSet.Subcomplex.toRange f)
-- Mathlib.Computability.Language
Language.reverse_one : ∀ {α : Type u_1}, Language.reverse 1 = 1
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
Order.cof_ordinal : Order.cof Ordinal.{u} = Cardinal.univ.{u, u + 1}
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defn.inj : ∀ {e : Lean.Expr} {p : Int.Internal.Linear.Poly} {e_1 : Lean.Expr} {p_1 : Int.Internal.Linear.Poly},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defn e p = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defn e_1 p_1 →
    e = e_1 ∧ p = p_1
-- Std.Sync.Channel
/-- Closes the channel, returns `Except.ok` when called the first time, otherwise `Except.error`.
When a channel is closed:
- no new values can be sent successfully anymore
- all blocked consumers are resolved to `none` (as no new messages can be sent they will never
  resolve)
- if there are already values waiting to be received they can still be received by subsequent `recv`
  calls
 -/
Std.CloseableChannel.close : {α : Type} → Std.CloseableChannel α → EIO Std.CloseableChannel.Error Unit
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.binaryProductIso F G).inv
      CategoryTheory.Limits.prod.snd =
    CategoryTheory.FunctorToTypes.prod.snd
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.map_id : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal]
  (h : optParam (N ≤ AddSubgroup.comap (AddMonoidHom.id G) N) ⋯),
  QuotientAddGroup.map N N (AddMonoidHom.id G) h = AddMonoidHom.id (G ⧸ N)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_add_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.T R (n + 2) = 2 * Polynomial.X * Polynomial.Chebyshev.T R (n + 1) - Polynomial.Chebyshev.T R n
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : AddZeroClass α] [inst_4 : AddZeroClass β] [inst_5 : AddZeroClass γ] {g : β →+o γ} {f₁ f₂ : α →+o β},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_X_add_C_pow : ∀ {R : Type u} [inst : CommSemiring R] (c : R) (m : ℕ),
  Polynomial.derivative ((Polynomial.X + Polynomial.C c) ^ m) =
    Polynomial.C ↑m * (Polynomial.X + Polynomial.C c) ^ (m - 1)
-- Mathlib.RingTheory.MvPowerSeries.Derivative
/-- The partial derivative of `g^n` equals `n * g^(n-1) * g'`.  -/
MvPowerSeries.pderiv_pow : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ} (g : MvPowerSeries σ R) (n : ℕ),
  (MvPowerSeries.pderiv R i) (g ^ n) = ↑n * g ^ (n - 1) * (MvPowerSeries.pderiv R i) g
-- Mathlib.Algebra.Lie.OfAssociative
/-- A linear equivalence of two modules induces a Lie algebra equivalence of their endomorphisms.  -/
LinearEquiv.lieConj : {R : Type u} →
  {M₁ : Type v} →
    {M₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module R M₁] →
            [inst_3 : AddCommGroup M₂] → [inst_4 : Module R M₂] → (M₁ ≃ₗ[R] M₂) → Module.End R M₁ ≃ₗ⁅R⁆ Module.End R M₂
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.isTotallyComplex_iff : ∀ (K : Type u_1) [inst : Field K], NumberField.IsTotallyComplex K ↔ ∀ (v : NumberField.InfinitePlace K), v.IsComplex
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The type copy of `E →SL[σ] F` endowed with the weak operator topology, denoted as
`E →SWOT[σ] F`. Likewise, when `σ := RingHom.id 𝕜`, the notation `E →WOT[𝕜] F` is available.  -/
ContinuousLinearMapWOT : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : Semiring 𝕜₁] →
      [inst_1 : Semiring 𝕜₂] →
        (𝕜₁ →+* 𝕜₂) →
          (E : Type u_3) →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [TopologicalSpace E] →
                  [Module 𝕜₁ E] → [inst : AddCommGroup F] → [TopologicalSpace F] → [Module 𝕜₂ F] → Type (max u_3 u_4)
-- Mathlib.Data.Set.Function
Set.injOn_union : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f : α → β},
  Disjoint s₁ s₂ → (Set.InjOn f (s₁ ∪ s₂) ↔ Set.InjOn f s₁ ∧ Set.InjOn f s₂ ∧ ∀ x ∈ s₁, ∀ y ∈ s₂, f x ≠ f y)
-- Std.Data.DTreeMap.Internal.Zipper
Std.Slice.iter.eq_1 : ∀ {γ : Type u_1} {α β : Type u_2} [inst : Std.ToIterator (Std.Slice γ) Id α β] (s : Std.Slice γ),
  s.iter = Std.Slice.Internal.iter s
-- Lean.Meta.Basic
Lean.Meta.instTypeNameFunInfo : TypeName Lean.Meta.FunInfo
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.minimalPeriod_eq_prime_pow : ∀ {α : Type u_1} {f : α → α} {x : α} {p k : ℕ} [hp : Fact (Nat.Prime p)],
  ¬Function.IsPeriodicPt f (p ^ k) x →
    Function.IsPeriodicPt f (p ^ (k + 1)) x → Function.minimalPeriod f x = p ^ (k + 1)
-- Lean.Declaration
Lean.TheoremVal.value : Lean.TheoremVal → Lean.Expr
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
DFinsupp.linearIndependent_single : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] {φ : ι → Type u_4} (f : (i : ι) → φ i → M i),
  (∀ (i : ι), LinearIndependent R (f i)) → LinearIndependent R fun ix => fun₀ | ix.fst => f ix.fst ix.snd
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.apply_symm_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂) (p : P₂), e (e.symm p) = p
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.norm_lt_one : ∀ (z : Complex.UnitDisc), ‖↑z‖ < 1
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow.fst : ∀ {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}}, (e.oadd n a).NFBelow b → e.NF
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkPushforward_germ_apply : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C X) (U : TopologicalSpace.Opens ↑Y) (x : ↑X)
  (hx : (CategoryTheory.ConcreteCategory.hom f) x ∈ U) {F_1 : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory C F_1]
  (x_1 : carrier (((TopCat.Presheaf.pushforward C f).obj F).obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.stalkPushforward C f F x))
      ((CategoryTheory.ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward C f).obj F).germ U ((CategoryTheory.ConcreteCategory.hom f) x) hx))
        x_1) =
    (CategoryTheory.ConcreteCategory.hom (F.germ ((TopologicalSpace.Opens.map f).obj U) x hx)) x_1
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.Std.Iter.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Algebra.Homology.HomotopyFiber
/-- The homotopy fiber of a morphism between homological complexes.  -/
HomologicalComplex.homotopyFiber : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {α : Type u_2} →
        {c : ComplexShape α} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) → [DecidableRel c.Rel] → [HomologicalComplex.HasHomotopyFiber φ] → HomologicalComplex C c
-- Mathlib.Topology.Connected.PathConnected
pathConnectedSpace_iff_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X], PathConnectedSpace X ↔ ∃ x, pathComponent x = Set.univ
-- Mathlib.Data.List.AList
/-- Look up the value associated to a key in an association list.  -/
AList.lookup : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → AList β → Option (β a)
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.Q.mk.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (p : α × α),
  Lean.Grind.IntModule.OfNatModule.Q.mk p = Quot.mk (Lean.Grind.IntModule.OfNatModule.r α) p
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.hasColimitsOfShape_discrete : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ] (X Y : C)
  (p : X ⟶ Y),
  CategoryTheory.Limits.HasColimitsOfShape
    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex I.homFamily p)) C
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.faceι_ι_assoc : ∀ {n : ℕ} (i : Fin (n + 2)) {Z : SSet} (h : SSet.stdSimplex.obj { len := n + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.boundary.faceι i)
      (CategoryTheory.CategoryStruct.comp (SSet.boundary (n + 1)).ι h) =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.face {i}ᶜ).ι h
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.extensionHom_coe : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α] [inst_3 : IsUniformAddGroup α]
  {β : Type u} [inst_4 : UniformSpace β] [inst_5 : Ring β] [inst_6 : IsUniformAddGroup β] [inst_7 : IsTopologicalRing β]
  (f : α →+* β) (hf : Continuous ⇑f) [inst_8 : CompleteSpace β] [inst_9 : T0Space β] (a : α),
  (UniformSpace.Completion.extensionHom f hf) ↑a = f a
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.toLinearMap_trans : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ),
  (↑(φ.trans ψ)).toLinearMap = (↑ψ).toLinearMap ∘ₗ (↑φ).toLinearMap
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_ofReal_of_pos : ∀ {x : ℝ}, 0 < x → (ENNReal.ofReal x).log = ↑(Real.log x)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.OpenCover.restrict_I₀ : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens), (𝒰.restrict U).I₀ = 𝒰.I₀
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
dense_addSubmonoidClosure_iff_addSubgroupClosure : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G]
  {s : Set G}, Dense ↑(AddSubmonoid.closure s) ↔ Dense ↑(AddSubgroup.closure s)
-- Lean.Elab.Command
Lean.Elab.Command.State.nextMacroScope : Lean.Elab.Command.State → ℕ
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.unitOfArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {a : Array α}, (Std.HashMap.Raw.unitOfArray a).WF
-- Lean.Meta.Tactic.Grind.Internalize
/-- Inserts `e` into the list of case-split candidates if applicable.  -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.checkAndAddSplitCandidate : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Init.Data.String.Basic
String.Slice.Pos.sliceTo.congr_simp : ∀ {s : String.Slice} (p₀ pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : pos ≤ p₀), p₀.sliceTo pos h = p₀.sliceTo pos_1 ⋯
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.IterM.step_intermediateZip.match_1.splitter : {α₁ β₁ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α₁ m β₁] →
      {it₁ : Std.IterM m β₁} →
        (motive : it₁.Step → Sort u_3) →
          (x : it₁.Step) →
            ((it₁' : Std.IterM m β₁) →
                (out : β₁) →
                  (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩) →
              ((it₁' : Std.IterM m β₁) →
                  (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩) →
                ((hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩) → motive x
-- Lean.MetavarContext
Lean.LocalInstance.className : Lean.LocalInstance → Lean.Name
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_sum'`.

---

Variant where the image of `g` is a `SkewMonoidAlgebra`.  -/
SkewMonoidAlgebra.toFinsupp_sum' : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [inst_1 : AddCommMonoid k']
  (f : SkewMonoidAlgebra k G) (g : G → k → SkewMonoidAlgebra k' G'),
  (f.sum g).coeff = f.coeff.sum fun x1 x2 => (g x1 x2).coeff
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mem_top : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M}, x ∈ ⊤
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_eq_iff_forall : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {p : α → Prop} {f g : α →₀ M},
  Finsupp.subtypeDomain p f = Finsupp.subtypeDomain p g ↔ ∀ (x : α), p x → f x = g x