mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.rank.eq_def : ∀ {α : Type u_1} (x : Batteries.BinomialHeap.Imp.HeapNode α),
  x.rank =
    match x with
    | Batteries.BinomialHeap.Imp.HeapNode.nil => 0
    | Batteries.BinomialHeap.Imp.HeapNode.node a child s => s.rank + 1
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  {Z : AlgebraicGeometry.LocallyRingedSpace} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict f).hom
      (CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Analysis.Convex.Intrinsic
mem_intrinsicClosure : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P} {x : P},
  x ∈ intrinsicClosure 𝕜 s ↔ ∃ y ∈ closure (Subtype.val ⁻¹' s), ↑y = x
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHomClass.mk : ∀ {F : Type u_1} {A : outParam (Type u_2)} {B : outParam (Type u_3)} [inst : NonUnitalNonAssocSemiring A]
  [inst_1 : Star A] [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] [inst_4 : FunLike F A B]
  [inst_5 : NonUnitalRingHomClass F A B] [toStarHomClass : StarHomClass F A B], NonUnitalStarRingHomClass F A B
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.restoreM_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α ρ : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m α),
  ⦃fun s => (Std.Do.wp x).apply (fun a => Q.1 a s, Q.2)⦄ MonadControl.restoreM x ⦃Q⦄
-- Mathlib.Analysis.Calculus.Taylor
taylor_within_apply : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ x : ℝ),
  taylorWithinEval f n s x₀ x =
    ∑ k ∈ Finset.range (n + 1), ((↑k.factorial)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  (CategoryTheory.ShortComplex.SnakeInput.Hom.id S).f₃ = CategoryTheory.CategoryStruct.id S.L₃
-- Lean.Meta.Sym.Apply
Lean.Meta.Sym.ApplyResult.failed.sizeOf_spec : sizeOf Lean.Meta.Sym.ApplyResult.failed = 1
-- Init.Data.Range.Polymorphic.PRange
/-- Every element of the intersection is an element of both original ranges.
   -/
Std.Ric.LawfulRcoIntersection.mem_intersection_iff : ∀ {α : Type w} {inst : LT α} {inst_1 : LE α} {inst_2 : Std.Ric.HasRcoIntersection α}
  [self : Std.Ric.LawfulRcoIntersection α] {a : α} {r : Std.Ric α} {s : Std.Rco α},
  a ∈ Std.Ric.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.addLetToUnfold : Lean.FVarId → Lean.Elab.Tactic.ElabSimpArgResult
-- Mathlib.Data.Seq.Computation
Computation.corec_eq : ∀ {α : Type u} {β : Type v} (f : β → α ⊕ β) (b : β),
  (Computation.corec f b).destruct = Computation.rmap (Computation.corec f) (f b)
-- Init.Data.List.Pairwise
List.pairwise_reverse : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.Pairwise R l.reverse ↔ List.Pairwise (fun a b => R b a) l
-- Mathlib.Data.Matrix.Mul
Matrix.ext_of_mulVec_single : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  {M N : Matrix m n α}, (∀ (i : n), M.mulVec (Pi.single i 1) = N.mulVec (Pi.single i 1)) → M = N
-- Init.Data.UInt.Bitwise
USize.and_le_right : ∀ {a b : USize}, a &&& b ≤ b
-- Init.Data.Iterators.Lemmas.Combinators.Append
Std.Iter.Intermediate.appendSnd_eq_toIter_appendSnd_toIterM : ∀ {α₁ α₂ β : Type w} [Std.Iterator α₁ Id β] [inst : Std.Iterator α₂ Id β] {it₂ : Std.Iter β},
  Std.Iter.Intermediate.appendSnd α₁ it₂ = (Std.IterM.Intermediate.appendSnd α₁ it₂.toIterM).toIter
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- For types in the signature, we want to be sure pi binder types are pretty printed.
 -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabForallParamsWithSignature.delabTy : Lean.PrettyPrinter.Delaborator.DelabM Lean.Term
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.subsingleton_subalgebra : ∀ (α : Type u_1) [inst : TopologicalSpace α] (R : Type u_2) [inst_1 : CommSemiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] [Subsingleton α], Subsingleton (Subalgebra R C(α, R))
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J]
  [W.IsStableUnderTransfiniteCompositionOfShape J], W.transfiniteCompositionsOfShape J ≤ W
-- Mathlib.NumberTheory.FermatPsp
/-- This is a proof that the number produced using `psp_from_prime` is actually pseudoprime to base `b`.
The primary purpose of this lemma is to help prove `exists_infinite_pseudoprimes`.

We use <https://primes.utm.edu/notes/proofs/a_pseudoprimes.html> as a rough outline of the proof.
 -/
_private.Mathlib.NumberTheory.FermatPsp.0.Nat.psp_from_prime_psp : ∀ {b : ℕ}, 2 ≤ b → ∀ {p : ℕ}, Nat.Prime p → 2 < p → ¬p ∣ b * (b ^ 2 - 1) → (Nat.psp_from_prime✝ b p).FermatPsp b
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem : ∀ {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} {x : ↥X} {U : ↑X.affineOpens},
  x ∈ ↑U → (x ∈ I.support ↔ x ∈ X.zeroLocus ↑(I.ideal U))
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalIntros : Lean.Elab.Tactic.Tactic
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.one_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (f : M ⟶ N)
  [CategoryTheory.IsMonHom f] {Z : C} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp 1 (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp 1 h
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instNeg : {m : Type u_1} → {n : Type u_2} → {α : m → n → Type v} → [(i : m) → (j : n) → Neg (α i j)] → Neg (DMatrix m n α)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.diseq_int_module : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx p ≠ 0 → Lean.Grind.CommRing.Poly.denoteAsIntModule ctx p ≠ 0
-- Mathlib.Analysis.Calculus.ContDiff.Basic
ftaylorSeries.eq_1 : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (x : E) (n : ℕ), ftaylorSeries 𝕜 f x n = iteratedFDeriv 𝕜 n f x
-- Mathlib.Topology.WithTopology
WithTopology.instNonempty : ∀ {X : Type u_1} (t : TopologicalSpace X) [Nonempty X], Nonempty (WithTopology X t)
-- Init.Data.Order.PackageFactories
Std.FactoryInstances.instOrdOfDecidableLE : {α : Type u} → [inst : LE α] → [DecidableLE α] → Ord α
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_convexOn_of_integrand_ae : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
  [ClosedIciTopology E] {β : Type u_6} [inst_6 : AddCommMonoid β] [inst_7 : Module ℝ β] {f : α → β → E} {s : Set β},
  Convex ℝ s →
    (∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)) →
      (∀ a ∈ s, MeasureTheory.Integrable (fun x => f x a) μ) → ConvexOn ℝ s fun b => ∫ (x : α), f x b ∂μ
-- Init.Data.Int.Order
Int.ne_iff_lt_or_gt : ∀ {a b : ℤ}, a ≠ b ↔ a < b ∨ b < a
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addCommGroup.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddCommGroup (f i)],
  Pi.addCommGroup = { toAddGroup := Pi.addGroup, add_comm := ⋯ }
-- Mathlib.Lean.Expr.Basic
/-- Update the name of a `ConstantInfo`.  -/
Lean.ConstantInfo.updateName : Lean.ConstantInfo → Lean.Name → Lean.ConstantInfo
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.instBornology : {X : Type u_1} → {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → [Bornology X] → Bornology (Metric.Snowflaking X α hα₀ hα₁)
-- Init.Data.Array.Subarray
/-- A subarray with the provided upper bound, starting at the index 0.  -/
Array.«term__[:_]» : Lean.TrailingParserDescr
-- Mathlib.Topology.MetricSpace.Completion
/-- The new distance is continuous.  -/
UniformSpace.Completion.continuous_dist : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β]
  {f g : β → UniformSpace.Completion α}, Continuous f → Continuous g → Continuous fun x => dist (f x) (g x)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prodMk_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} {a : C} (x : F.obj a)
  (y : G.obj a),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.fst.app a))
      (CategoryTheory.FunctorToTypes.prodMk x y) =
    x
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.le_join_of_refl`. -/
Relation.join_of_single : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r], r ≤ Relation.Join r
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.mk.sizeOf_spec : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toFun : α → MeasureTheory.Measure β) (measurable' : Measurable toFun),
  sizeOf { toFun := toFun, measurable' := measurable' } = 1
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.toRingEquiv_restrictScalars : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A ≃ₐ[S] B), (AlgEquiv.restrictScalars R f).toRingEquiv = f.toRingEquiv
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.bilinearCombination_apply : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] {v : α → M} [inst_4 : Module S M] [inst_5 : SMulCommClass R S M],
  (Finsupp.bilinearCombination R S) v = Finsupp.linearCombination R v
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.commRingCat_hasStrictTerminalObjects : CategoryTheory.Limits.HasStrictTerminalObjects CommRingCat
-- Lean.Parser.Module
Lean.Parser.instInhabitedModuleParserState : Inhabited Lean.Parser.ModuleParserState
-- Std.Data.DHashMap.Lemmas
/-- Variant of `getD_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.DHashMap.Const.getD_map' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α} {fallback : γ},
  Std.DHashMap.Const.getD (Std.DHashMap.map f m) k fallback =
    (Option.pmap (fun v h => f (m.getKey k h) v) (Std.DHashMap.Const.get? m k) ⋯).getD fallback
-- Init.Core
/-- `pure (a : α) s` means that the block exited normally with return value `a`  -/
DoResultPRBC.pure : {α β σ : Type u} → α → σ → DoResultPRBC α β σ
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  {B : Type u_3} {J : Type u_4} [inst_1 : CategoryTheory.Category.{v_2, u_2} A]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} B] [inst_3 : CategoryTheory.Category.{v_4, u_4} J]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  [CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Comma L R)]
  [(CategoryTheory.MorphismProperty.commaObj L R P).IsClosedUnderColimitsOfShape J],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.MorphismProperty.Comma L R P ⊤ ⊤)
-- Mathlib.Algebra.Group.End
Equiv.pow_mulLeft : ∀ {α : Type u_4} [inst : Group α] (a : α) (n : ℕ), Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)
-- Mathlib.Computability.Primrec.Basic
PrimrecRel.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {R : β → γ → Prop} {f : α → β} {g : α → γ}, PrimrecRel R → Primrec f → Primrec g → PrimrecPred fun a => R (f a) (g a)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.leftOp_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor C Dᵒᵖ} (α : F ⟶ G) (β : G ⟶ H),
  CategoryTheory.NatTrans.leftOp (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftOp β) (CategoryTheory.NatTrans.leftOp α)
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFunDual_map_const_add : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure E} [BorelSpace E] (r : E) (L : StrongDual ℝ E),
  MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun x => r + x) μ) L =
    MeasureTheory.charFunDual μ L * Complex.exp (↑(L r) * Complex.I)
-- Mathlib.Combinatorics.SimpleGraph.Tutte
SimpleGraph.IsTutteViolator.empty : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V], Odd (Nat.card V) → G.IsTutteViolator ∅
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
/-- **Alias** of `CategoryTheory.Sheaf.functorH`.

---

`H` as a functor.  -/
CategoryTheory.Sheaf.cohomologyFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
        [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] →
          ℕ → CategoryTheory.Functor (CategoryTheory.Sheaf J AddCommGrpCat) AddCommGrpCat
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V : (x : M) → TangentSpace I x}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  (MDiffAt[s] fun x => ⟨x, V x⟩) x →
    DifferentiableWithinAt 𝕜
      (VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) V (Set.range ↑I))
      (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_neg_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.covariance X (fun ω => -Y ω) μ = -ProbabilityTheory.covariance X Y μ
-- Mathlib.Data.Set.Lattice.Image
Set.image_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, GaloisConnection (Set.image f) (Set.preimage f)
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
CategoryTheory.Groupoid.vertexGroup_one : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (c : C), 1 = CategoryTheory.CategoryStruct.id c
-- Mathlib.Topology.UniformSpace.CompareReals
CompareReals.compare_uc_symm : UniformContinuous ⇑CompareReals.compareEquiv.symm
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.range_snd : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S],
  NonUnitalRingHom.srange (NonUnitalRingHom.snd R S) = ⊤
-- Mathlib.Algebra.Lie.OfAssociative
LinearEquiv.lieConj_symm : ∀ {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₂] (e : M₁ ≃ₗ[R] M₂), e.lieConj.symm = e.symm.lieConj
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModuleHierarchyImportedByParams.module : Lean.Lsp.LeanModuleHierarchyImportedByParams → Lean.Lsp.LeanModule
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.pullback_target : ∀ {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : TopologicalSpace F] [inst_3 : TopologicalSpace B]
  [inst_4 : ∀ (_b : B), Nonempty (E _b)] {K : Type U} [inst_5 : FunLike K B' B] [inst_6 : ContinuousMapClass K B' B]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (f : K), (e.pullback f).target = (⇑f ⁻¹' e.baseSet) ×ˢ Set.univ
-- Mathlib.Logic.Relation
Relation.transGen_minimal : ∀ {α : Type u_1} {r r' : α → α → Prop} [IsTrans α r'], r ≤ r' → Relation.TransGen r ≤ r'
-- Mathlib.Tactic.NormNum.PowMod
Nat.modCore.eq_1 : ∀ (x y : ℕ), x.modCore y = if hy : 0 < y then Nat.modCore.go y hy x.succ x ⋯ else x
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.parseHeader : Std.Internal.Parsec.ByteArray.Parser Std.Time.TimeZone.TZif.Header
-- Mathlib.Data.Num.Prime
PosNum.minFacAux_to_nat : ∀ {fuel : ℕ} {n k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.bot_adj : ∀ {V : Type u_2} (v w : V), ⊥.Adj v w ↔ False
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- Given a continuous representation `π` of `G` on `V`,
this defines a Continuous representation `π.coind₁` of `G` on the function space `C(G,V)`.
The action of an element `g : G` is defined by `f ↦ (x ↦ π g (f (g⁻¹ * x)))`.
This new representation of `G` is isomorphic to the continuous coinduction
of the trivial representation of the trivial subgroup of `G`, but the action has been
twisted so that the map `const : V → C(G,V)` is an intertwining map.  -/
ContRepresentation.coind₁ : {R : Type u_1} →
  {V : Type u_3} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : TopologicalSpace V] →
          [inst_3 : IsTopologicalAddGroup V] →
            [inst_4 : Module R V] →
              {G : Type u_7} →
                [inst_5 : Group G] →
                  [inst_6 : TopologicalSpace G] →
                    [inst_7 : TopologicalSpace R] →
                      [inst_8 : ContinuousSMul R V] →
                        [IsTopologicalGroup G] → ContRepresentation R G V → ContRepresentation R G C(G, V)
-- Mathlib.Logic.Basic
Iff.not_left : ∀ {a b : Prop}, (a ↔ ¬b) → (¬a ↔ b)
-- Mathlib.Tactic.GRewrite.Core
/-- The monad used for `grw`.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.GRewriteM : Type → Type
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_Ioi : ∀ {α : Type u_1} [inst : Preorder α] [LocallyFiniteOrderTop α] (a : α), (Set.Ioi a).Finite
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The ring of integers of an `n`-th cyclotomic extension of `ℚ` is a cyclotomic extension.  -/
IsCyclotomicExtension.ringOfIntegers : ∀ {n : ℕ} {K : Type u} [inst : Field K] [NeZero n] [inst_2 : CharZero K] [IsCyclotomicExtension {n} ℚ K],
  IsCyclotomicExtension {n} ℤ (NumberField.RingOfIntegers K)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.not_nonneg_iff_neg_of_sum_mem_range_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [CharZero R] (f : ι → ℤ),
  ∑ j ∈ b.support, f j • P.root j ∈ Set.range ⇑P.root → Function.support f ⊆ ↑b.support → (¬0 ≤ f ↔ f < 0)
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.instFunLike : {N : Type u_1} →
  {X : Type u_2} → [inst : TopologicalSpace X] → {x : X} → FunLike (↑(GenLoop N X x)) (N → ↑unitInterval) X
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of `AffineSubspace.isConnected_setOfPred_sSameSide`. -/
AffineSubspace.isConnected_setOf_sSameSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {x : P},
  x ∉ s → (↑s).Nonempty → IsConnected {y | s.SSameSide x y}
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.Paths.of_map : ∀ (V : Type u₁) [inst : Quiver V] {X Y : V} (f : X ⟶ Y), (CategoryTheory.Paths.of V).map f = f.toPath
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticOnNhd.log : ∀ {f : ℝ → ℝ} {s : Set ℝ}, AnalyticOnNhd ℝ f s → (∀ x ∈ s, 0 < f x) → AnalyticOnNhd ℝ (fun z => Real.log (f z)) s
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- A functor `StructuredArrow S toLightProfinite ⥤ FintypeCat` whose limit in `LightProfinite` is
isomorphic to `S`.
 -/
LightProfinite.fintypeDiagram' : (S : LightProfinite) → CategoryTheory.Functor (CategoryTheory.StructuredArrow S FintypeCat.toLightProfinite) FintypeCat
-- Mathlib.Data.Finite.Perm
Nat.card_perm : ∀ {α : Type u_1} [Finite α], Nat.card (Equiv.Perm α) = (Nat.card α).factorial
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.ofStabilizer.snoc.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {a : α} {n : ℕ}
  (x : Fin n ↪ ↥(SubAddAction.ofStabilizer G a)),
  SubAddAction.ofStabilizer.snoc x =
    Fin.Embedding.snoc (x.trans (Function.Embedding.subtype fun x => x ∈ SubAddAction.ofStabilizer G a)) ⋯
-- Lean.Elab.PreDefinition.Structural.BRecOn
/-- Calculates the `.brecOn` motive corresponding to one structural recursive function.
The `value` is the function with (only) the fixed parameters moved into the context.
The `type` is the corresponding function type with (only) the fixed parameters instantiated.
 -/
Lean.Elab.Structural.mkBRecOnMotive : Lean.Elab.Structural.RecArgInfo → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.Ideal.Maps
/-- `I.map f` is the span of the image of the ideal `I` under `f`, which may be bigger than
the image itself.  -/
Ideal.map : {R : Type u} →
  {S : Type v} → {F : Type u_1} → [inst : Semiring R] → [inst_1 : Semiring S] → [FunLike F R S] → F → Ideal R → Ideal S
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.pow_mulRight : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (a : A) (n : ℕ), LinearMap.mulRight R a ^ n = LinearMap.mulRight R (a ^ n)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₁_map_one : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : ↥(groupCohomology.cocycles₁ A)),
  f 1 = 0
-- Mathlib.FieldTheory.SeparableDegree
/-- The separable degree of `F⟮α⟯ / F` is equal to the separable degree of the
minimal polynomial of `α` over `F`.  -/
IntermediateField.finSepDegree_adjoin_simple_eq_natSepDegree : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {α : E},
  IsAlgebraic F α → Field.finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree
-- Mathlib.Data.Set.Lattice
Set.iInter_dite : ∀ {α : Type u_1} {ι : Sort u_5} (p : ι → Prop) [inst : DecidablePred p] (f : (i : ι) → p i → Set α)
  (g : (i : ι) → ¬p i → Set α),
  (⋂ i, if h : p i then f i h else g i h) = (⋂ i, ⋂ (h : p i), f i h) ∩ ⋂ i, ⋂ (h : ¬p i), g i h
-- Init.Data.Array.OfFn
Array.ofFn_succ' : ∀ {n : ℕ} {α : Type u_1} {f : Fin (n + 1) → α}, Array.ofFn f = #[f 0] ++ Array.ofFn fun i => f i.succ