mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- `L₀.X₃` is the kernel of `v₁₂.τ₃ : L₁.X₃ ⟶ L₂.X₃`.  -/
CategoryTheory.ShortComplex.SnakeInput.h₀τ₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex.SnakeInput C) →
        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.v₀₁.τ₃ ⋯)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.norm_setToL1_le_mul_norm' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (f : ↥(MeasureTheory.Lp E 1 μ)), ‖(MeasureTheory.L1.setToL1 hT) f‖ ≤ max C 0 * ‖f‖
-- Mathlib.Combinatorics.Additive.FreimanHom
MulEquivClass.isMulFreimanIso : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β}
  {n : ℕ} [inst_2 : EquivLike F α β] [MulEquivClass F α β] (f : F), Set.BijOn (⇑f) A B → IsMulFreimanIso n A B ⇑f
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- If `g` has a chosen pullback, then `Over.ChosenPullbacksAlong.fst f g` has a chosen pullback.  -/
CategoryTheory.ChosenPullbacksAlong.chosenPullbacksAlongFst : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y Z X : C} →
      (f : Y ⟶ X) →
        (g : Z ⟶ X) →
          [inst_1 : CategoryTheory.ChosenPullbacksAlong g] →
            CategoryTheory.ChosenPullbacksAlong (CategoryTheory.ChosenPullbacksAlong.fst f g)
-- Init.Data.SInt.Bitwise
ISize.toUSize_or : ∀ (a b : ISize), (a ||| b).toUSize = a.toUSize ||| b.toUSize
-- Mathlib.GroupTheory.Sylow
Sylow.coe_equivProdPrimeFactors_apply : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (h : p ≠ 0) (H : Sylow p G), ↑((Sylow.equivProdPrimeFactors h) H) = ↑H
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The above data together form a topological additive group.  -/
ProfiniteAddGrp.topologicalAddGroup : ∀ (self : ProfiniteAddGrp.{u}), IsTopologicalAddGroup ↑self.toProfinite.toTop
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.whiskeringEquivalence.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J),
  CategoryTheory.Limits.Cone.whiskeringEquivalence e =
    { functor := CategoryTheory.Limits.Cone.whiskering e.functor,
      inverse :=
        (CategoryTheory.Limits.Cone.whiskering e.inverse).comp
          (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom),
      unitIso :=
        CategoryTheory.NatIso.ofComponents
          (fun s =>
            CategoryTheory.Limits.Cone.ext
              (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj s).pt) ⋯)
          ⋯,
      counitIso :=
        CategoryTheory.NatIso.ofComponents
          (fun s =>
            CategoryTheory.Limits.Cone.ext
              (CategoryTheory.Iso.refl
                ((((CategoryTheory.Limits.Cone.whiskering e.inverse).comp
                            (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom)).comp
                        (CategoryTheory.Limits.Cone.whiskering e.functor)).obj
                    s).pt)
              ⋯)
          ⋯,
      functor_unitIso_comp := ⋯ }
-- Mathlib.Algebra.Group.Defs
AddSemigroup.toAdd : {G : Type u} → [self : AddSemigroup G] → Add G
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.inl_desc_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W)
  (k : Y ⟶ W) (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Q Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj W Q ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight inl Q)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (hP.desc h k w) Q) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight h Q) h_1
-- Batteries.Data.BitVec.Lemmas
_private.Batteries.Data.BitVec.Lemmas.0.Fin.succ.match_1.splitter : {n : ℕ} → (motive : Fin n → Sort u_1) → (x : Fin n) → ((i : ℕ) → (h : i < n) → motive ⟨i, h⟩) → motive x
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.apply_lfpApprox_le_lfpApprox_of_lt : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a b : Ordinal.{u}},
  a < b → f (OrdinalApprox.lfpApprox f x a) ≤ OrdinalApprox.lfpApprox f x b
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- If an augmented simplicial object has an extradegeneracy, then
then augmentation is a split epimorphism.  -/
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.splitEpi : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject.Augmented C} → X.ExtraDegeneracy → CategoryTheory.SplitEpi X.hom
-- Aesop.Rule.Forward
Aesop.ForwardRule.mk.sizeOf_spec : ∀ (toForwardRuleInfo : Aesop.ForwardRuleInfo) (name : Aesop.RuleName) (term : Aesop.RuleTerm)
  (prio : Aesop.ForwardRulePriority),
  sizeOf { toForwardRuleInfo := toForwardRuleInfo, name := name, term := term, prio := prio } =
    1 + sizeOf toForwardRuleInfo + sizeOf name + sizeOf term + sizeOf prio
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insertMany_list_singleton : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.insertMany [⟨k, v⟩] = t.insert k v
-- Aesop.Forward.State
Aesop.PatSubstSource.hyp.inj : ∀ {fvarId fvarId_1 : Lean.FVarId},
  Aesop.PatSubstSource.hyp fvarId = Aesop.PatSubstSource.hyp fvarId_1 → fvarId = fvarId_1
-- Batteries.Util.ProofWanted
proof_wanted.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.PreDefinition.WF.Basic
Lean.Elab.WF.debug.rawDecreasingByGoal : Lean.Option Bool
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.tendsto_translation_number' : ∀ (f : CircleDeg1Lift) (x : ℝ),
  Filter.Tendsto (fun n => ((f ^ (n + 1)) x - x) / (↑n + 1)) Filter.atTop (nhds f.translationNumber)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for addition of `BitVec`s.  -/
BitVec.reduceAdd : Lean.Meta.Simp.DSimproc
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.takeEndWhile_eq_toSlice_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.takeEndWhile pat = s.toSlice ↔ s.revAll pat = true
-- Mathlib.Order.WithBot
WithTop.instBot.eq_1 : ∀ {α : Type u_1} [inst : Bot α], WithTop.instBot = { bot := ↑⊥ }
-- Mathlib.Data.Bool.Basic
Bool.or_eq_true_eq_eq_true_or_eq_true : ∀ (a b : Bool), ((a || b) = true) = (a = true ∨ b = true)
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.fold.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} (aig : Std.Sat.AIG α) (vec : aig.RefVec len)
  (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func],
  Std.Sat.AIG.RefVec.fold aig vec func = Std.Sat.AIG.RefVec.fold.go aig (aig.mkConstCached true) 0 len vec func
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.mono_L₂_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (self : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.Mono self.L₂.f
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Host.inst : Std.Http.Header Std.Http.Header.Host
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
inr_comp_cfcₙHom_eq_cfcₙAux : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] (a : A) [ha : IsStarNormal a],
  (Unitization.inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha) = cfcₙAux ⋯ a ha
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.userPreDSimprocs : Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.DSimproc
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Int.Icc_eq_insert_of_Icc_succ_eq : ∀ {m n : ℤ} {s : Finset ℤ}, m ≤ n → Finset.Icc (m + 1) n = s → Finset.Icc m n = insert m s
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- If `A` is a faithfully flat `R`-algebra, and `m` is a term of an `R`-module `M`,
then `1 ⊗ₜ[R] m = 0` if and only if `m = 0`.  -/
Module.FaithfullyFlat.one_tmul_eq_zero_iff : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : Ring A] [inst_4 : Algebra R A] [Module.FaithfullyFlat R A] (m : M), 1 ⊗ₜ[R] m = 0 ↔ m = 0
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
/-- If `B` is a (2,1)-category, then every lax functor `F` from a bicategory to `B` defines a
`CategoryTheory.LaxFunctor.PseudoCore` structure on `F` that can be used to promote `F` to a
pseudofunctor using `CategoryTheory.Pseudofunctor.mkOfLax`.  -/
CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {B' : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory B'] →
        [CategoryTheory.Bicategory.IsLocallyGroupoid B] → (F : CategoryTheory.LaxFunctor B' B) → F.PseudoCore
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSet_iff : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (s : ι → Set Ω),
  (∀ (i : ι), MeasurableSet (s i)) →
    ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
      ProbabilityTheory.iCondIndepSet m' hm' s μ ↔
        ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1 | m']
-- Mathlib.Analysis.Normed.Group.Real
enorm_enorm : ∀ {ε : Type u_9} [inst : ENorm ε] (x : ε), ‖‖x‖ₑ‖ₑ = ‖x‖ₑ
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.eval_separatingRight : ∀ {K : Type u_1} {V : Type u_2} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V],
  (Module.Dual.eval K V).SeparatingRight
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- The Bochner integral over simple functions in L1 space as a continuous linear map over ℝ.  -/
MeasureTheory.L1.SimpleFunc.integralCLM : (α : Type u_1) →
  (E : Type u_2) →
    [inst : NormedAddCommGroup E] →
      {m : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [inst_1 : NormedSpace ℝ E] → ↥(α →₁ₛ[μ] E) →L[ℝ] E
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.instIsModuleConvexSpaceProd : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid N]
  [inst_6 : Module R N] [inst_7 : Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M]
  [inst_9 : Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N], Convexity.IsModuleConvexSpace R (M × N)
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackIsoProdSubtype_inv_snd : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (TopCat.pullbackIsoProdSubtype f g).inv (CategoryTheory.Limits.pullback.snd f g) =
    TopCat.pullbackSnd f g
-- Init.Data.Vector.Lemmas
Vector.toArray_drop : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, (xs.drop i).toArray = xs.toArray.extract i n
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.between_comm : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V}, SimpleGraph.between s t G = SimpleGraph.between t s G
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The edge of the standard simplex with endpoints `a` and `b`.  -/
SSet.stdSimplex.edge : (n : ℕ) → (a b : Fin (n + 1)) → a ≤ b → (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := 1 })
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.FirstByte.done : ByteArray.utf8DecodeChar?.FirstByte
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.instInhabited : {X : Type u_1} → Inhabited (OnePoint X)
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `NonUnitalCommRing` instance along a surjective function.  -/
Function.Surjective.nonUnitalCommRing : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : Neg S] →
                [inst_4 : Sub S] →
                  [inst_5 : SMul ℕ S] →
                    [inst_6 : SMul ℤ S] →
                      [inst_7 : NonUnitalCommRing R] →
                        f 0 = 0 →
                          (∀ (x y : R), f (x + y) = f x + f y) →
                            (∀ (x y : R), f (x * y) = f x * f y) →
                              (∀ (x : R), f (-x) = -f x) →
                                (∀ (x y : R), f (x - y) = f x - f y) →
                                  (∀ (n : ℕ) (x : R), f (n • x) = n • f x) →
                                    (∀ (n : ℤ) (x : R), f (n • x) = n • f x) → NonUnitalCommRing S
-- Mathlib.Order.Filter.Partial
Filter.rcomap_compose : ∀ {α : Type u} {β : Type v} {γ : Type w} (r : SetRel α β) (s : SetRel β γ),
  Filter.rcomap r ∘ Filter.rcomap s = Filter.rcomap (r.comp s)
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.instStarSubtypeCliffordAlgebraMemSubmonoid : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → Star ↥(spinGroup Q)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.mk_point : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P : WeierstrassCurve.Projective.PointClass R}
  (h : W'.NonsingularLift P), { point := P, nonsingular := h }.point = P
-- Init.Data.SInt.Lemmas
Int64.toInt32_neg : ∀ (x : Int64), (-x).toInt32 = -x.toInt32
-- Mathlib.Data.Fintype.OfMap
Fintype.univ_ofSubsingleton : ∀ {α : Type u_1} (a : α) [inst : Subsingleton α], Finset.univ = {a}
-- Mathlib.Order.Grade
/-- Minimal elements have minimal grades.  -/
GradeMinOrder.isMin_grade : ∀ {𝕆 : Type u_5} {α : Type u_6} {inst : Preorder 𝕆} {inst_1 : Preorder α} [self : GradeMinOrder 𝕆 α] ⦃a : α⦄,
  IsMin a → IsMin (GradeOrder.grade a)
-- Mathlib.Topology.Order.DenselyOrdered
nhdsLT_neBot_of_exists_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {b : α},
  (∃ a, a < b) → (nhdsWithin b (Set.Iio b)).NeBot
-- Batteries.CodeAction.Attr
/-- An extension which collects all the tactic code actions.  -/
Batteries.CodeAction.tacticSeqCodeActionExt : Lean.PersistentEnvExtension Lean.Name (Lean.Name × Batteries.CodeAction.TacticSeqCodeAction)
  (Array Lean.Name × Array Batteries.CodeAction.TacticSeqCodeAction)
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.associator_eqToHom_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y z t : B} (e₁ : x = y) (e₂ : y = z) (e₃ : z = t),
  (CategoryTheory.Bicategory.associator (CategoryTheory.eqToHom e₁) (CategoryTheory.eqToHom e₂)
        (CategoryTheory.eqToHom e₃)).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.eqToHom e₁)
        (CategoryTheory.Bicategory.eqToHomTransIso e₂ e₃).inv)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.eqToHomTransIso e₁ ⋯).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.eqToHomTransIso ⋯ e₃).hom
          (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.eqToHomTransIso e₁ e₂).hom
            (CategoryTheory.eqToHom e₃))))
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_X : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), (PowerSeries.trunc (n + 2)) PowerSeries.X = Polynomial.X
-- Mathlib.RingTheory.Ideal.Maps
AlgHom.ker_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), RingHom.ker f = RingHom.ker ↑f
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.toMultilinearMap : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] → ContinuousMultilinearMap R M₁ M₂ → MultilinearMap R M₁ M₂
-- Mathlib.Analysis.InnerProductSpace.Orientation
Orientation.volumeForm_map : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : InnerProductSpace ℝ F] [inst_4 : Fact (Module.finrank ℝ F = n)] (φ : E ≃ₗᵢ[ℝ] F) (x : Fin n → F),
  ((Orientation.map (Fin n) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.basisCotangent_apply : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (r : σ),
  P.basisCotangent r = Algebra.Extension.Cotangent.mk ⟨P.relation r, ⋯⟩
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.take.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → List α → Sort u_2) →
    (x : ℕ) →
      (x_1 : List α) →
        ((x : List α) → motive 0 x) →
          ((n : ℕ) → motive n.succ []) → ((n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)) → motive x x_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insert k v).isEmpty = false
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂},
  (m₁ ∪ m₂)[k] = m₁[k]
-- Lean.Meta.Transform
/-- Removes all `inaccessible` annotations from `e`.  -/
Lean.Meta.eraseInaccessibleAnnotations : Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {i j : E.I₀}
  (k : E.I₁ i j),
  CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ k =
    CategoryTheory.Iso.refl (E.Y ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) k))
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- Functors out of the free groupoid biject with functors out of the original category.  -/
CategoryTheory.FreeGroupoid.functorEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Groupoid D] →
        CategoryTheory.Functor (CategoryTheory.FreeGroupoid C) D ≃ CategoryTheory.Functor C D
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.RotateRight
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastRotateRight : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.ShiftTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'}
  (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) {Z : C} (h : Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (data.mapZ φ) (CategoryTheory.CategoryStruct.comp (data.factorizationData g).p h) =
    CategoryTheory.CategoryStruct.comp (data.factorizationData f).p
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right φ) h)
-- Mathlib.Tactic.FunProp.Types
/-- Monad to run `fun_prop` tactic in.  -/
Mathlib.Meta.FunProp.FunPropM : Type → Type
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The norm, relative to `ℤ`, of `ζ - 1` in an `n`-th cyclotomic extension of `ℚ` where `n` is not a
power of a prime number is `1`.
 -/
IsPrimitiveRoot.norm_toInteger_sub_one_eq_one : ∀ {K : Type u} [inst : Field K] {ζ : K} [inst_1 : CharZero K] {n : ℕ} [IsCyclotomicExtension {n} ℚ K]
  (hζ : IsPrimitiveRoot ζ n) (h₁ : 2 < n),
  (∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n) →
    have this := ⋯;
    (Algebra.norm ℤ) (hζ.toInteger - 1) = 1
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_mono_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  f ≤ᵐ[μ] g → ⨍⁻ (a : α), f a ∂μ ≤ ⨍⁻ (a : α), g a ∂μ
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearEquiv.hasMFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E ≃L[𝕜] E') {x : E}, HasMFDerivAt% (⇑f) x ↑f
-- Mathlib.Order.Filter.CardinalInter
Filter.CardinalGenerateSets.below.univ : ∀ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {motive : (a : Set α) → Filter.CardinalGenerateSets g a → Prop},
  Filter.CardinalGenerateSets.below ⋯
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
/-- Given `F : C ⥤ H`, `W : MorphismProperty C` and `X : C`, we say that `F` has a
pointwise right derived functor at `X` if `F` has a left Kan extension
at `L.obj X` for any localization functor `L : C ⥤ D` for `W`. In the
definition, this is stated for `L := W.Q`, see `hasPointwiseRightDerivedFunctorAt_iff`
for the more general equivalence.  -/
CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAt : {C : Type u₁} →
  {H : Type u₃} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} H] →
        CategoryTheory.Functor C H → CategoryTheory.MorphismProperty C → C → Prop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true → t.maxKey? = none
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.obj.μ_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] (X : C) [inst_5 : CategoryTheory.MonObj X],
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X X) (F.map CategoryTheory.MonObj.mul)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Expressions of the form `f₁ ◁ ... ◁ fₙ ◁ η`.  -/
Mathlib.Tactic.BicategoryLike.WhiskerLeft : Type
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
/-- Right multiplication by a nonzero element in a `GroupWithZero` is a permutation of the
underlying type.  -/
Equiv.mulRight₀ : {G₀ : Type u_1} → [inst : GroupWithZero G₀] → (a : G₀) → a ≠ 0 → Equiv.Perm G₀
-- Mathlib.Analysis.Analytic.Binomial
Real.one_add_rpow_hasFPowerSeriesOnBall_zero : ∀ {a : ℝ}, HasFPowerSeriesOnBall (fun x => (1 + x) ^ a) (binomialSeries ℝ a) 0 1