mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Order.Ord
Std.TransOrd.isGE_trans : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α] {a b c : α},
  (compare a b).isGE = true → (compare b c).isGE = true → (compare a c).isGE = true
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom_continuous : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a),
  Continuous ⇑(cfcHom ha)
-- Mathlib.Algebra.Module.BigOperators
Fintype.sum_smul_sum : ∀ {α : Type u_3} {β : Type u_4} {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Fintype α] [inst_4 : Fintype β] (f : α → R) (g : β → M),
  (∑ i, f i) • ∑ j, g j = ∑ i, ∑ j, f i • g j
-- Mathlib.RingTheory.Artinian.Instances
IsArtinianRing.instDecompositionMonoid : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R] [IsReduced R], DecompositionMonoid R
-- Mathlib.Data.Finset.NAry
Finset.image_image₂_antidistrib : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq α']
  [inst_1 : DecidableEq β'] [inst_2 : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  [inst_3 : DecidableEq δ] {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'},
  (∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)) →
    Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' (Finset.image g₁ t) (Finset.image g₂ s)
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.map_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (X : LeftInvariantDerivation I G), X 0 = 0
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.isInducing : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsEmbedding f → Topology.IsInducing f
-- Mathlib.Analysis.Asymptotics.ExpGrowth
Frequently.le_expGrowthSup : ∀ {u : ℕ → ENNReal} {a : EReal}, (∃ᶠ (n : ℕ) in Filter.atTop, (a * ↑n).exp ≤ u n) → a ≤ ExpGrowth.expGrowthSup u
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.map_add_left : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] [inst_13 : AddCommMonoid Q]
  [inst_14 : Module R Q] (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q),
  TensorProduct.AlgebraTensorModule.map (f₁ + f₂) g =
    TensorProduct.AlgebraTensorModule.map f₁ g + TensorProduct.AlgebraTensorModule.map f₂ g
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.baseChange_dblU : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).dblU (⇑f ∘ P) = f ((W'.baseChange A).dblU P)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.lift₂_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  (f : M → M → α)
  (h :
    ∀ (a₁ b₁ a₂ b₂ : M),
      ArchimedeanClass.mk a₁ = ArchimedeanClass.mk b₁ →
        ArchimedeanClass.mk a₂ = ArchimedeanClass.mk b₂ → f a₁ a₂ = f b₁ b₂)
  (a b : M), ArchimedeanClass.lift₂ f h (ArchimedeanClass.mk a) (ArchimedeanClass.mk b) = f a b
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.matchGroundPattern : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.addCommMonoid.eq_1 : ∀ {M : Type u_4} [inst : AddCommMonoid M] (c : AddCon M),
  c.addCommMonoid = { toAddMonoid := c.addMonoid, add_comm := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- The (limiting) `PullbackCone f g` implicit in the statement
that we have an `IsPullback fst snd f g`.
 -/
CategoryTheory.IsPullback.cone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P X Y Z : C} →
      {fst : P ⟶ X} →
        {snd : P ⟶ Y} →
          {f : X ⟶ Z} → {g : Y ⟶ Z} → CategoryTheory.IsPullback fst snd f g → CategoryTheory.Limits.PullbackCone f g
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.rawAux : String.Pos.Raw → Bool → Lean.Parser.ParserFn
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.forIn_eq_forIn_keysArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.Internal.Impl.forIn (fun a x d => f a d) init t = forIn t.keysArray init f
-- Init.Data.Rat.Lemmas
Rat.div_lt_iff' : ∀ {a b c : ℚ}, 0 < b → (a / b < c ↔ a < b * c)
-- Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
/-- If `GenContFract.of v` terminated at step `n`, then the `n`th convergent is exactly `v`.  -/
GenContFract.of_correctness_of_terminatedAt : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] {v : K} {n : ℕ} [inst_2 : FloorRing K],
  (GenContFract.of v).TerminatedAt n → v = (GenContFract.of v).convs n
-- Batteries.Recycling.RBTree.Depth
/-- `depthLB c n` is the best upper bound on the depth of any balanced red-black tree
with root colored `c` and black-height `n`.
 -/
RBTree.RBNode.depthLB : RBTree.RBColor → ℕ → ℕ
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.skipPrefixWhile_prop_eq_skipPrefixWhile_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice},
  s.skipPrefixWhile p = s.skipPrefixWhile fun x => decide (p x)
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.Limits.constCone_pt : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : C), (CategoryTheory.Limits.constCone J X).pt = X
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.reflectsFiniteProducts_of_reflectsIsomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteProducts C]
  [CategoryTheory.Limits.PreservesFiniteProducts F], CategoryTheory.Limits.ReflectsFiniteProducts F
-- Init.Data.Int.Linear
Int.Internal.Linear.OrOver : ℕ → (ℕ → Prop) → Prop
-- Mathlib.Geometry.Convex.Cone.Dual
/-- **Alias** of `PointedCone.dual_hull`. -/
PointedCone.dual_span : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (s : Set M), PointedCone.dual p ↑(PointedCone.hull R s) = PointedCone.dual p s
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- Push the value in the local store to the given stack.  -/
Turing.PartrecToTM2.push' : Turing.PartrecToTM2.K' → Turing.PartrecToTM2.Stmt' → Turing.PartrecToTM2.Stmt'
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_insert_le : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (m.insert k v).size ≤ m.size + 1
-- Mathlib.Topology.Order.LeftRightLim
/-- An antitone function is continuous at a point if and only if its left and right limits
coincide.  -/
Antitone.continuousAt_iff_leftLim_eq_rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f →
    ∀ {x : α} [inst_4 : TopologicalSpace α] [OrderTopology α],
      ContinuousAt f x ↔ Function.leftLim f x = Function.rightLim f x
-- Lean.Data.NameMap.Basic
Lean.NameSet.instInter : Inter Lean.NameSet
-- Mathlib.Topology.Algebra.ConstMulAction
IsOpen.smul : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] {s : Set α}, IsOpen s → ∀ (c : G), IsOpen (c • s)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- One can reformulate smoothness on a set as continuity on this set, and smoothness in any
extended chart in the target.  -/
mdifferentiableOn_iff_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  [IsManifold I 1 M] [IsManifold I' 1 M'],
  MDiff[s] f ↔ ContinuousOn f s ∧ ∀ (y : M'), MDiff[s ∩ f ⁻¹' (extChartAt I' y).source] (↑(extChartAt I' y) ∘ f)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.coe_codRestrict_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂)
  (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p) (x : M₁), ↑((f.codRestrict p h) x) = f x
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Factors.piQuotientEquiv.congr_simp : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsDedekindDomain S] (p : Ideal R) (hp : Ideal.map (algebraMap R S) p ≠ ⊥),
  Ideal.Factors.piQuotientEquiv p hp = Ideal.Factors.piQuotientEquiv p hp
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the reverse direction of `hasMFDerivAt_iff_hasFDerivAt`. -/
HasFDerivAt.hasMFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {x : E} {f' : TangentSpace (modelWithCornersSelf 𝕜 E) x →L[𝕜] TangentSpace (modelWithCornersSelf 𝕜 E') (f x)},
  HasFDerivAt f f' x → HasMFDerivAt% f x f'
-- Lean.Attributes
Lean.throwAttrMustBeGlobal : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → {α : Type} → Lean.Name → Lean.AttributeKind → m α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instDecidableEqBVBit : DecidableEq Std.Tactic.BVDecide.BVBit
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Ici_iff : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ : α}, a₁ ≤ b₁ → (Set.Icc a₁ b₁ ⊆ Set.Ici a₂ ↔ a₂ ≤ a₁)
-- Init.Meta.Defs
Lean.Syntax.instCoeTSyntaxArrayTSepArray : {k : Lean.SyntaxNodeKinds} → {sep : String} → Coe (Lean.TSyntaxArray k) (Lean.Syntax.TSepArray k sep)
-- Mathlib.Util.AtomM
Mathlib.Tactic.AtomM.Context.mk.injEq : ∀ (red : Lean.Meta.TransparencyMode) (evalAtom : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result)
  (red_1 : Lean.Meta.TransparencyMode) (evalAtom_1 : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result),
  ({ red := red, evalAtom := evalAtom } = { red := red_1, evalAtom := evalAtom_1 }) =
    (red = red_1 ∧ evalAtom = evalAtom_1)
-- Init.Data.Vector.Range
/-- Variant of `mem_zipIdx` specialized at `k = 0`.  -/
Vector.mem_zipIdx' : ∀ {α : Type u_1} {n : ℕ} {x : α} {i : ℕ} {xs : Vector α n} (h : (x, i) ∈ xs.zipIdx), i < n ∧ x = xs[i]
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- The universal property that a derivation `d : M.Derivation φ` must
satisfy so that the presheaf of modules `M` can be considered as the presheaf of
(relative) differentials of a presheaf of commutative rings `φ : S ⟶ F.op ⋙ R`.  -/
PresheafOfModules.Derivation.Universal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
          {F : CategoryTheory.Functor C D} →
            {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
              {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
                {φ : S ⟶ F.op.comp R} → M.Derivation φ → Type (max (max (max u u₂) (v + 1)) v₂)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.trivializationAt_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (x : M),
  (trivializationAt E (TangentSpace I) x).target = (chartAt H x).source ×ˢ Set.univ
-- Mathlib.NumberTheory.NumberField.CMField
/-- The map `(𝓞 K)ˣ →* torsion K` defined by `u ↦ u * (conj u)⁻¹`.
 -/
NumberField.IsCMField.unitsMulComplexConjInv : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : CharZero K] →
      [NumberField.IsCMField K] → [NumberField K] → (NumberField.RingOfIntegers K)ˣ →* ↥(NumberField.Units.torsion K)
-- Mathlib.ModelTheory.LanguageMap
/-- Pulls an `L`-structure along a language map `ϕ : L →ᴸ L'`, and then expands it
to an `L'`-structure arbitrarily.  -/
FirstOrder.Language.LHom.defaultExpansion : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} →
    (ϕ : L →ᴸ L') →
      [(n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)] →
        [(n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)] →
          (M : Type u_1) → [Inhabited M] → [L.Structure M] → L'.Structure M
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.nil.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf Batteries.PairingHeapImp.Heap.nil = 1
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.forgetStalk_inv_comp_eval_assoc : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) {Z : Type u} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).inv
      (CategoryTheory.CategoryStruct.comp
        (TypeCat.ofHom ⇑(CommRingCat.Hom.hom (smoothSheafCommRing.evalHom IM I M R x))) h) =
    CategoryTheory.CategoryStruct.comp (smoothSheaf.evalHom IM I R x) h
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Ioc_of_strictAntiOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  a ≤ b → ContinuousOn f (Set.Icc a b) → StrictAntiOn f (Set.Icc a b) → f '' Set.Ioc a b = Set.Ico (f b) (f a)
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dHomologyData_right_ι : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆)
  (h₅₆ : CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_7),
  (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).right.ι =
    X.map f₂₃ f₄ f₅₆ f₃ f₄ f₅₆ (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅₆ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCallHierarchyIncomingCall : Lean.FromJson Lean.Lsp.CallHierarchyIncomingCall
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.isDiameter_iff_ofDiameter_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ ↔ EuclideanGeometry.Sphere.ofDiameter p₁ p₂ = s
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.Hom.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        {c : ℤ → ComplexShape κ} →
          {r₀ : ℤ} →
            {E E' : CategoryTheory.SpectralSequence C c r₀} →
              (hom :
                  (r : ℤ) →
                    (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_1) → E.page r ⋯ ⟶ E'.page r ⋯) →
                autoParam
                    (∀ (r r' : ℤ) (pq : κ) (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.Hom._auto_5)
                      (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_7),
                      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hom r ⋯) pq)
                          (E'.iso r r' pq ⋯ ⋯).hom =
                        CategoryTheory.CategoryStruct.comp (E.iso r r' pq ⋯ ⋯).hom ((hom r' ⋯).f pq))
                    CategoryTheory.SpectralSequence.Hom.comm._autoParam →
                  E.Hom E'
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.ofNat_ctorIdx : ∀ (x : Std.Tactic.BVDecide.BVBinOp), Std.Tactic.BVDecide.BVBinOp.ofNat x.ctorIdx = x
-- Mathlib.GroupTheory.PGroup
isPGroup_iff_exists_pow_pow_eq_one : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Finite G], IsPGroup p G ↔ ∃ k, ∀ (g : G), g ^ p ^ k = 1
-- Mathlib.NumberTheory.Dioph
Poly.instZero : {α : Type u_1} → Zero (Poly α)
-- Mathlib.Topology.Gluing
TopCat.GlueData.mk : (toGlueData : CategoryTheory.GlueData TopCat) →
  (∀ (i j : toGlueData.J), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (toGlueData.f i j))) →
    TopCat.GlueData
-- Mathlib.CategoryTheory.Bicategory.Product
/-- The cartesian product of two strict bicategories is strict.  -/
CategoryTheory.Bicategory.instStrictProd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory.Strict C], CategoryTheory.Bicategory.Strict (B × C)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.colimitRightOpIsoUnopLimit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasLimit F],
  CategoryTheory.Limits.colimitRightOpIsoUnopLimit F =
    CategoryTheory.Limits.colimit.isoColimitCocone
      { cocone := CategoryTheory.Limits.coconeRightOpOfCone (CategoryTheory.Limits.limit.cone F),
        isColimit := CategoryTheory.Limits.isColimitCoconeRightOpOfCone F (CategoryTheory.Limits.limit.isLimit F) }
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isNegNNRat.inj : ∀ {inst : Lean.Expr} {q : ℚ} {n d proof inst_1 : Lean.Expr} {q_1 : ℚ} {n_1 d_1 proof_1 : Lean.Expr},
  Mathlib.Meta.NormNum.Result'.isNegNNRat inst q n d proof =
      Mathlib.Meta.NormNum.Result'.isNegNNRat inst_1 q_1 n_1 d_1 proof_1 →
    inst = inst_1 ∧ q = q_1 ∧ n = n_1 ∧ d = d_1 ∧ proof = proof_1
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arcsin`.  -/
Orientation.oangle_add_left_eq_arcsin_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  o.oangle x y = ↑(Real.pi / 2) → o.oangle (x + y) y = ↑(Real.arcsin (‖x‖ / ‖x + y‖))
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.add : Nat.Primrec' fun v => v.head + v.tail.head
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_le_maxKey!_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β k}, (compare t.maxKey! (Std.DTreeMap.Internal.Impl.insert! k v t).maxKey!).isLE = true
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_bot : LinearGrowth.linearGrowthSup ⊥ = ⊥
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_X : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {f : σ → R} (n : σ),
  (MvPolynomial.eval f) (MvPolynomial.X n) = f n
-- Mathlib.LinearAlgebra.Ray
/-- The ray given by a nonzero vector.  -/
rayOfNeZero : (R : Type u_1) →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} → [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → (v : M) → v ≠ 0 → Module.Ray R M
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.colimitCocone_ι_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [inst_2 :
    ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
      CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))]
  [inst_3 : ∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] (j : J)
  (X : Cᵒᵖ),
  ((PresheafOfModules.colimitCocone F).ι.app j).app X =
    CategoryTheory.Limits.colimit.ι (F.comp (PresheafOfModules.evaluation R X)) j
-- Init.Tactics
/-- `focus tac` focuses on the main goal, suppressing all other goals, and runs `tac` on it.
Usually `· tac`, which enforces that the goal is closed by `tac`, should be preferred.
 -/
Lean.Parser.Tactic.focus : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono : ∀ (N : Type u_2) [inst : Mul N] [IsLeftCancelMul N] [inst_2 : PartialOrder N] [MulLeftMono N], MulLeftStrictMono N
-- Mathlib.Order.SymmDiff
symmDiff_eq_xor : ∀ (p q : Prop), symmDiff p q = Xor p q