mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {f : α → Bool}
  {k : α}, k ∈ Std.DTreeMap.filter (fun a x => f a) t ↔ ∃ (h : k ∈ t), f (t.getKey k h) = true
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- Any chosen pullback functor of the identity morphism is naturally isomorphic to the identity
functor.  -/
CategoryTheory.ChosenPullbacksAlong.pullbackId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : C) →
      [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id X)] →
        CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.id X) ≅
          CategoryTheory.Functor.id (CategoryTheory.Over X)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.dropUntil.eq_2 : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {v w : V} (x v_1 : V) (r : G.Adj v v_1) (p : G.Walk v_1 w)
  (x_1 : x ∈ (SimpleGraph.Walk.cons r p).support),
  (SimpleGraph.Walk.cons r p).dropUntil x x_1 =
    if hx : v = x then
      Eq.ndrec (motive := fun u => u ∈ (SimpleGraph.Walk.cons r p).support → G.Walk u w)
        (fun h => SimpleGraph.Walk.cons r p) hx x_1
    else p.dropUntil x ⋯
-- Init.Data.SInt.Lemmas
Int8.toInt_inj : ∀ {x y : Int8}, x.toInt = y.toInt ↔ x = y
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- If `N` acts additively continuously and ergodically on `X` and `M` acts minimally on `N`,
then the corresponding action of `M` on `X` is ergodic.  -/
ErgodicVAdd.trans_isMinimal : ∀ {M : Type u_1} {X : Type u_2} [inst : AddMonoid M] [inst_1 : VAdd M X] [inst_2 : TopologicalSpace X] [R1Space X]
  [inst_4 : MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ]
  [μ.InnerRegular] (N : Type u_3) [inst_8 : AddAction M N] [inst_9 : AddMonoid N] [inst_10 : TopologicalSpace N]
  [AddAction.IsMinimal M N] [inst_12 : AddAction N X] [VAddAssocClass M N X] [ContinuousVAdd N X] [ErgodicVAdd N X μ],
  ErgodicVAdd M X μ
-- Init.Data.Option.Lemmas
Option.merge_le : ∀ {α : Type u_1} [inst : LE α] {f : α → α → α} {o₁ o₂ o₃ : Option α},
  (∀ (a b c : α), a ≤ c → b ≤ c → f a b ≤ c) → o₁ ≤ o₃ → o₂ ≤ o₃ → Option.merge f o₁ o₂ ≤ o₃
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.hom_hom_comp : ∀ {X Y Z : FinPartOrd} (f : X ⟶ Y) (g : Y ⟶ Z),
  PartOrd.Hom.hom (CategoryTheory.CategoryStruct.comp f g).hom = (PartOrd.Hom.hom g.hom).comp (PartOrd.Hom.hom f.hom)
-- Mathlib.Topology.Algebra.Module.LocallyConvex
LocallyConvexSpace.inf : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {t₁ t₂ : TopologicalSpace E},
  LocallyConvexSpace 𝕜 E → LocallyConvexSpace 𝕜 E → LocallyConvexSpace 𝕜 E
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.apply_symm_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) (x : N), e (e.symm x) = x
-- Mathlib.Order.Hom.Bounded
/-- Turn an element of a type `F` satisfying `BotHomClass F α β` into an actual
`BotHom`. This is declared as the default coercion from `F` to `BotHom α β`.  -/
BotHomClass.toBotHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} → [inst : FunLike F α β] → [inst_1 : Bot α] → [inst_2 : Bot β] → [BotHomClass F α β] → F → BotHom α β
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.isSubgraph_iff_le : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H.IsSubgraph G ↔ H ≤ G
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
/-- The functor `Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C`, on morphisms.  -/
AlgebraicTopology.DoldKan.Γ₀.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        {K K' : ChainComplex C ℕ} →
          (K ⟶ K') → (AlgebraicTopology.DoldKan.Γ₀.obj K ⟶ AlgebraicTopology.DoldKan.Γ₀.obj K')
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k a : α}
  {h₁ : a ∈ t.insert k}, (t.insert k).get a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then k else t.get a ⋯
-- Lean.CoreM
Lean.withAtLeastMaxRecDepth : {m : Type → Type u_1} → {α : Type} → [MonadFunctorT Lean.CoreM m] → ℕ → m α → m α
-- Mathlib.Data.Finite.Prod
AddEquiv.finite_left : ∀ {α : Type u_3} {β : Type u_4} [inst : Add α] [inst_1 : Add β] [Finite α], Finite (α ≃+ β)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_eq_nil : ∀ {m n : ℕ}, n ≤ m → (m<...=n).toList = []
-- Mathlib.Geometry.Convex.Set
Convexity.isAffineMap_subtypeVal : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] (s : Set X) (hs : Convexity.IsConvexSet R s), Convexity.IsAffineMap R Subtype.val
-- Mathlib.Algebra.Order.Sub.Defs
tsub_tsub : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] (b a c : α),
  b - a - c = b - (a + c)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.range_eq_top : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {f : R →ₙ+* S},
  f.range = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.Analysis.ODE.Transform
isIntegralCurve_comp_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {dt : ℝ},
  IsIntegralCurve (γ ∘ fun x => x + dt) (v ∘ fun x => x + dt) ↔ IsIntegralCurve γ v
-- Lean.Parser.Term
Lean.Parser.Term.letExpr.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Ideal.Maps
Ideal.eq_bot_of_comap_eq_bot' : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S},
  Function.Surjective ⇑f → ∀ {I : Ideal S}, Ideal.comap f I = ⊥ → I = ⊥
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.erase : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {a : α},
  m.WF → (m.erase a).WF
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_singleton_univ : ∀ {G : Type u_1} [inst : AddGroup G] {g : G}, AddSubgroup.IsComplement {g} Set.univ
-- Mathlib.Data.Fintype.EquivFin
finite_iff_nonempty_fintype : ∀ (α : Type u_4), Finite α ↔ Nonempty (Fintype α)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.pow_nc.eq_def : ∀ (p : Lean.Grind.CommRing.Poly) (k : ℕ),
  p.pow_nc k =
    match k with
    | 0 => Lean.Grind.CommRing.Poly.num 1
    | 1 => p
    | k.succ => (p.pow_nc k).mul_nc p
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α},
  (Std.Internal.List.eraseKey k l).isEmpty = (l.isEmpty || l.length == 1 && Std.Internal.List.containsKey k l)
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.instMkEvalHorizontalCompBicategoryM : Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp Mathlib.Tactic.Bicategory.BicategoryM
-- Mathlib.Analysis.Convex.Side
AffineSubspace.isConnected_setOfPred_wOppSide : ∀ {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),
  (↑s).Nonempty → IsConnected {y | s.WOppSide x y}
-- Lean.Elab.Command
Lean.Elab.Command.State.infoState : Lean.Elab.Command.State → Lean.Elab.InfoState
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.map.eq_1 : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S)
  (x : AddMonoidAlgebra R M), AddMonoidAlgebra.map f x = AddMonoidAlgebra.ofCoeff (Finsupp.mapRange ⇑f ⋯ x.coeff)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedArg.default : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Arg pu
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.mapMapIso_inverse : ∀ {X Y : TopCat} (H : X ≅ Y), (TopologicalSpace.Opens.mapMapIso H).inverse = TopologicalSpace.Opens.map H.inv
-- Lean.Elab.Tactic.Try
/-- `evalSuggest` for `first` tactic.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestFirst : Array (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Mathlib.Algebra.Module.Equiv.Opposite
MulOpposite.coe_opLinearEquiv_symm_addEquiv : ∀ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑(MulOpposite.opLinearEquiv R).symm = MulOpposite.opAddEquiv.symm
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.flattenList.toNatAux.match_1.eq_2 : ∀ {n : ℕ} (motive : List (BitVec n) → Sort u_1) (x : BitVec n) (h_1 : Unit → motive [])
  (h_2 : (x : BitVec n) → motive [x]) (h_3 : (x y : BitVec n) → (rest : List (BitVec n)) → motive (x :: y :: rest)),
  (match [x] with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: y :: rest => h_3 x y rest) =
    h_2 x
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.List.forIn'_eq_foldlM.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.yield b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_1 b
-- Init.Data.Float.Float
/-- Computes the arc cosine (inverse cosine) of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`acos`.
 -/
Float.acos : Float → Float
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {U : TopCat}
  (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V),
  CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)
      (X.restrictStalkIso h x).inv =
    (X.restrict h).presheaf.germ V x hx
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.IsParabolic.sub_eigenvalue_sq_eq_zero : ∀ {K : Type u_1} [inst : Field K] {m : Matrix (Fin 2) (Fin 2) K} [NeZero 2],
  m.IsParabolic → (m - (Matrix.scalar (Fin 2)) m.parabolicEigenvalue) ^ 2 = 0
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.d₂.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄),
  HomologicalComplex.mapBifunctor₂₃.d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j =
    HomologicalComplex.mapBifunctor₂₃.d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j
-- Init.Data.BitVec.Lemmas
BitVec.flattenList.toNatAux_eq : ∀ {n : ℕ} (xs : List (BitVec n)), BitVec.flattenList.toNatAux xs = (BitVec.flattenList xs).toNat
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero' : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X 0 κ ν → X =ᵐ[ν.bind ⇑κ] 0
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.mapₗ.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (f : α → β),
  MeasureTheory.Measure.mapₗ f =
    if hf : Measurable f then MeasureTheory.Measure.liftLinear (MeasureTheory.OuterMeasure.map f) ⋯ else 0
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.tsumNormRPowBound_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  (L : Submodule ℤ E) [inst_3 : DiscreteTopology ↥L], 0 < ZLattice.tsumNormRPowBound L
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.copy_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' u'' v'' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') (hu' : u' = u'')
  (hv' : v' = v''), (p.copy hu hv).copy hu' hv' = p.copy ⋯ ⋯
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Functional equation formulated for `Λ`.  -/
WeakFEPair.functional_equation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) (s : ℂ),
  P.Λ (↑P.k - s) = P.ε • P.symm.Λ s
-- Mathlib.Order.Fin.Basic
Fin.rev_zero_eq_top : ∀ (n : ℕ) [inst : NeZero n], Fin.rev 0 = ⊤
-- Lean.Elab.Util
Lean.MacroScopesView.format : Lean.MacroScopesView → Lean.Name → Std.Format
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.loopyOn_indep_iff : ∀ {α : Type u_1} {E I : Set α}, (Matroid.loopyOn E).Indep I ↔ I = ∅
-- Mathlib.Data.List.MinMax
List.argmax_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] {f : α → β} {a : α},
  List.argmax f [a] = some a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₁.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.CooperSplit),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₁ c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₁ c_1) =
    (c = c_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.insertManyIfNewUnit_nil : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit},
  m.WF → Std.DHashMap.Raw.Const.insertManyIfNewUnit m [] = m
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
ArithmeticFunction.ofPowerSeries_apply_zero : ∀ {R : Type u_1} [inst : CommSemiring R] (q : ℕ) (f : PowerSeries R), ((ArithmeticFunction.ofPowerSeries q) f) 0 = 0
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap : (CategoryTheory.forget₂ ProfiniteGrp.{u_1} Profinite).ReflectsIsomorphisms
-- Init.Prelude
MonadLift.mk : {m : semiOutParam (Type u → Type v)} → {n : Type u → Type w} → ({α : Type u} → m α → n α) → MonadLift m n
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNatCast : {R : Type u_1} → [inst : TopologicalSpace R] → [NatCast R] → NatCast (SeparationQuotient R)
-- Mathlib.Geometry.Manifold.Instances.Sphere
contDiffOn_stereoToFun : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} {n : WithTop ℕ∞},
  ContDiffOn ℝ n (stereoToFun v) {x | ((innerSL ℝ) v) x ≠ 1}
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.map_smul : ∀ {R : Type u_1} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : SeminormedAddCommGroup E₂] [inst_3 : Module R E] [inst_4 : Module R E₂] {e : E ≃ₗᵢ[R] E₂} (c : R) (x : E),
  e (c • x) = c • e x
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : TopologicalSpace γ] [inst_5 : Preorder γ] (f : β →Co γ)
  (g : α →Co β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.of.injEq : ∀ (carrier : Type u) [str : OmegaCompletePartialOrder carrier] (carrier_1 : Type u)
  (str_1 : OmegaCompletePartialOrder carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Topology.Separation.CompletelyRegular
isEmbedding_stoneCechUnit : ∀ {X : Type u} [inst : TopologicalSpace X] [T35Space X], Topology.IsEmbedding stoneCechUnit
-- Mathlib.Algebra.Order.Monovary
Monovary.pow_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Monovary f g → ∀ (n : ℕ), Monovary (f ^ n) g
-- Mathlib.Algebra.BigOperators.Fin
Fin.mul_prod_removeNth : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (i : Fin (n + 1)) (f : Fin (n + 1) → M),
  f i * ∏ j, i.removeNth f j = ∏ j, f j
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.iff_exists_prime_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α],
  UniqueFactorizationMonoid α ↔ ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
-- Lean.Parser.Attr
Lean.Parser.Attr.recursor.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Field.Defs
Rat.smul_one_eq_cast : ∀ (A : Type u_2) [inst : DivisionRing A] (m : ℚ), m • 1 = ↑m
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.isEmpty_inter_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.not_isNontrivial_iff : ∀ {R : Type u_5} [inst : Semiring R] {S : Type u_6} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (v : AbsoluteValue R S), ¬v.IsNontrivial ↔ ∀ (x : R), x ≠ 0 → v x = 1
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.mem_mk : ∀ {M : Type u_1} [inst : Mul M] {s : Set M} {x : M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s),
  x ∈ { carrier := s, mul_mem' := h_mul } ↔ x ∈ s
-- Lean.Message
/-- Eagerly formatted text.  -/
Lean.MessageData.ofFormat : Std.Format → Lean.MessageData
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.Measure.completion_apply : ∀ {α : Type u_2} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), μ.completion s = μ s
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.Indep.encard_le_eRk_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.Indep I → I ⊆ X → I.encard ≤ M.eRk X
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A graph is *acyclic* (or a *forest*) if it has no cycles.  -/
SimpleGraph.IsAcyclic : {V : Type u_1} → SimpleGraph V → Prop
-- Init.Data.List.Lemmas
List.head_filter_of_pos : ∀ {α : Type u_1} {p : α → Bool} {l : List α} (w : l ≠ []) (h : p (l.head w) = true), (List.filter p l).head ⋯ = l.head w
-- Mathlib.Analysis.Complex.Basic
Complex.dist_conj_conj : ∀ (z w : ℂ), dist ((starRingEnd ℂ) z) ((starRingEnd ℂ) w) = dist z w
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.forIn_filter : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {n : Type w → Type w''} [inst_1 : Monad n] [LawfulMonad n]
  [Std.Iterators.Finite α Id] [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β}
  {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)},
  forIn (Std.Iter.filter f it) init g =
    forIn it init fun out acc => if f out = true then g out acc else pure (ForInStep.yield acc)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.δ_naturality_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ f')
  (β : CategoryTheory.ComposableArrows.mk₁ g ⟶ CategoryTheory.ComposableArrows.mk₁ g') (n₀ n₁ : ℤ),
  autoParam (α.app 1 = β.app 0) CategoryTheory.Abelian.SpectralObject.δ_naturality._auto_1 →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δ_naturality._auto_3) {Z : C}
      (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f') ⟶ Z),
      CategoryTheory.CategoryStruct.comp ((X.H n₀).map β) (CategoryTheory.CategoryStruct.comp (X.δ f' g' n₀ n₁ hn₁) h) =
        CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (CategoryTheory.CategoryStruct.comp ((X.H n₁).map α) h)
-- Lean.Meta.Sym.Arith.Poly
/-- `divides m₁ m₂` returns `true` if monomial `m₁` divides `m₂`
Example: `x^2.z` divides `w.x^3.y^2.z`
 -/
Lean.Grind.CommRing.Mon.divides : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Bool
-- Batteries.Tactic.Lint.Misc
/-- A linter for checking whether statements of declarations are well-typed.  -/
Batteries.Tactic.Lint.checkType : Batteries.Tactic.Lint.Linter
-- Mathlib.Analysis.MeanInequalities
/-- **Minkowski inequality**: the `L_p` seminorm of the sum of two vectors is less than or equal
to the sum of the `L_p`-seminorms of the summands. A version for `ℝ`-valued nonnegative
functions.  -/
Real.Lp_add_le_of_nonneg : ∀ {ι : Type u} (s : Finset ι) {f g : ι → ℝ} {p : ℝ},
  1 ≤ p →
    (∀ i ∈ s, 0 ≤ f i) →
      (∀ i ∈ s, 0 ≤ g i) →
        (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.attachCellsιFunctorObj_g₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).g₁ = CategoryTheory.SmallObject.functorObjTop f πX
-- Mathlib.FieldTheory.AxGrothendieck
/-- The collection of first-order formulas corresponding to the Ax-Grothendieck theorem.  -/
FirstOrder.genericPolyMapSurjOnOfInjOn : {ι : Type u_1} →
  {α : Type u_2} →
    [Finite α] →
      [Finite ι] → FirstOrder.Language.ring.Formula (α ⊕ ι) → (ι → Finset (ι →₀ ℕ)) → FirstOrder.Language.ring.Sentence
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : α → β) (h : ∀ (x : β), MeasurableSet (f ⁻¹' {x}))
  (h' : (Set.range f).Finite), ⇑{ toFun := f, measurableSet_fiber' := h, finite_range' := h' } = f
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_le_cons : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (i : Fin (n + 1)) → Preorder (α i)] {x₀ y₀ : α 0}
  {x y : (i : Fin n) → α i.succ}, Fin.cons x₀ x ≤ Fin.cons y₀ y ↔ x₀ ≤ y₀ ∧ x ≤ y
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix_symm : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α]
  [inst_3 : One α] (f : m ≃. n), f.symm.toMatrix = f.toMatrix.transpose