mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.anyTR.loop.match_1.splitter : (n : ℕ) →
  (motive : (x : ℕ) → x ≤ n → Sort u_1) →
    (x : ℕ) → (x_1 : x ≤ n) → ((h : 0 ≤ n) → motive 0 h) → ((m : ℕ) → (h : m.succ ≤ n) → motive m.succ h) → motive x x_1
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.apply_eq_iff_eq : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂) {p₁ p₂ : P₁}, e p₁ = e p₂ ↔ p₁ = p₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoPullback_hom_snd_assoc : ∀ {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} (h : CategoryTheory.IsPullback fst snd f g) [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C}
  (h_1 : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp h.isoPullback.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h_1) =
    CategoryTheory.CategoryStruct.comp snd h_1
-- Mathlib.Order.Hom.CompleteLattice
map_iInf₂ : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} {κ : ι → Sort u_7} [inst : FunLike F α β]
  [inst_1 : InfSet α] [inst_2 : InfSet β] [sInfHomClass F α β] (f : F) (g : (i : ι) → κ i → α),
  f (⨅ i, ⨅ j, g i j) = ⨅ i, ⨅ j, f (g i j)
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- The values before the squashed position stay the same.  -/
GenContFract.squashSeq_nth_of_lt : ∀ {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GenContFract.Pair K)} [inst : DivisionRing K] {m : ℕ},
  m < n → (GenContFract.squashSeq s n).get? m = s.get? m
-- Mathlib.Algebra.Group.Defs
/-- Addition is left cancellative (i.e. left regular).  -/
IsLeftCancelAdd.add_left_cancel : ∀ {G : Type u} {inst : Add G} [self : IsLeftCancelAdd G] (a : G), IsAddLeftRegular a
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddCancelCommMonoidOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddCancelCommMonoid Mᵃᵒᵖ], DomAddAct.instAddCancelCommMonoidOfAddOpposite = inst
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.SymbolPriorities.mk.injEq : ∀ (map map_1 : Lean.PHashMap Lean.Name ℕ), ({ map := map } = { map := map_1 }) = (map = map_1)
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.sum : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {ι : Type u_6} {s : Finset ι} {x y : ι → M}, (∀ i ∈ s, x i ≡ y i [SMOD U]) → ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.invertibleT : {R : Type u_1} → [inst : Semiring R] → (n : ℤ) → Invertible (LaurentPolynomial.T n)
-- Batteries.Recycling.RBTree.Basic
/-- `O(n₁ * log (n₁ + n₂))`. Intersects the maps `t₁` and `t₂`
using `mergeFn a b` to produce the new value.
 -/
RBTree.RBMap.intersectWith : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {γ : Type u_1} →
        {δ : Type u_2} → (α → β → γ → δ) → RBTree.RBMap α β cmp → RBTree.RBMap α γ cmp → RBTree.RBMap α δ cmp
-- Mathlib.Topology.DenseEmbedding
Dense.extend_eq_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : ↑s → β}
  [T2Space β] (hs : Dense s) {a : α} {b : β},
  Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b) → hs.extend f a = b
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.coeff_zero_eq_eval_zero : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.coeff 0 = Polynomial.eval 0 p
-- Mathlib.Algebra.Polynomial.Roots
Associated.roots_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p q : Polynomial R}, Associated p q → p.roots = q.roots
-- Mathlib.Data.Finset.Basic
Finset.erase_sdiff_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ≠ b → b ∈ s → s.erase a \ s.erase b = {b}
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_lt_iff_lt_toReal : ∀ {a : ℝ} {b : ENNReal}, 0 ≤ a → b ≠ ⊤ → (ENNReal.ofReal a < b ↔ a < b.toReal)
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- The rank of a matrix, defined as the dimension of its column space, as a term in `ℕ∞`.  -/
Matrix.eRank : {m : Type um} → {n : Type un} → {R : Type uR} → [Semiring R] → Matrix m n R → ℕ∞
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.HasEval.mono : ∀ {S : Type u_3} [inst : CommRing S] {a : S} {t u : TopologicalSpace S},
  t ≤ u → PowerSeries.HasEval a → PowerSeries.HasEval a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k}
  {h₁ : a ∈ (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.get a h₁ =
    if h₂ : compare k a = Ordering.eq then cast ⋯ v else t.get a ⋯
-- Init.Control.StateCps
StateCpsT.runK_lift : ∀ {α σ : Type u} {m : Type u → Type v} {β : Type u} [inst : Monad m] (x : m α) (s : σ) (k : α → σ → m β),
  (StateCpsT.lift x).runK s k = do
    let x ← x
    k x s
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State.namedArgs : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State → Array Lean.Name
-- Init.Data.Array.Nat
Array.sum_reverse_nat : ∀ (xs : Array ℕ), xs.reverse.sum = xs.sum
-- Lean.DocString.Parser
/-- Parses zero or more arguments to a role, directive, command, or code block.  -/
Lean.Doc.Parser.args : optParam (Option ℕ) none → Lean.Parser.ParserFn
-- Mathlib.Tactic.GCongr.Core
/-- This is used as the default side-goal discharger,
it calls the `gcongr_discharger` extensible tactic.
 -/
Mathlib.Tactic.GCongr.gcongrDischarger : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.ModelTheory.Syntax
/-- A bijection between terms with constants and terms with extra variables.  -/
FirstOrder.Language.Term.constantsVarsEquiv : {L : FirstOrder.Language} → {α : Type u'} → {γ : Type u_1} → (L.withConstants γ).Term α ≃ L.Term (γ ⊕ α)
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.le_lfpApprox : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}}, x ≤ OrdinalApprox.lfpApprox f x a
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.presheaf_map_apply_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : ↑(M.obj X)),
  (AddCommGrpCat.Hom.hom (M.presheaf.map f)) x = (CategoryTheory.ConcreteCategory.hom (M.map f)) x
-- Lean.Data.LOption
Lean.LOption.none : {α : Type u} → Lean.LOption α
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.mul_star_self_ne_zero_iff : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E] (x : E), x * star x ≠ 0 ↔ x ≠ 0
-- Std.Data.DTreeMap.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.getThenInsertIfNew? : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.LawfulEqCmp cmp] → Std.DTreeMap α β cmp → (a : α) → β a → Option (β a) × Std.DTreeMap α β cmp
-- Init.Data.SInt.Lemmas
Int32.toInt_mod : ∀ (a b : Int32), (a % b).toInt = a.toInt.tmod b.toInt
-- Mathlib.RingTheory.Polynomial.Vieta
Multiset.prod_X_add_C_coeff' : ∀ {R : Type u_1} [inst : CommSemiring R] {σ : Type u_2} (s : Multiset σ) (r : σ → R) {k : ℕ},
  k ≤ s.card →
    (Multiset.map (fun i => Polynomial.X + Polynomial.C (r i)) s).prod.coeff k = (Multiset.map r s).esymm (s.card - k)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiableOn_symm_coordChangeL : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_13 : MemTrivializationAtlas e]
  [inst_14 : MemTrivializationAtlas e'] [inst_15 : VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB],
  MDiff[e.baseSet ∩ e'.baseSet] fun b => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' b).symm
-- Mathlib.Data.Option.Basic
Option.joinM_eq_join : ∀ {α : Type u_1}, joinM = Option.join
-- Mathlib.Algebra.Star.Basic
Nat.instTrivialStar : TrivialStar ℕ
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- Smoothness of a `C^n` section at `x₀` within a set `a` can be determined
using any trivialisation whose `baseSet` contains `x₀`.  -/
Bundle.Trivialization.contMDiffWithinAt_section : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {s : (x : B) → E x} (a : Set B) {x₀ : B}
  {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e],
  x₀ ∈ e.baseSet →
    (ContMDiffWithinAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) a x₀ ↔
      ContMDiffWithinAt IB (modelWithCornersSelf 𝕜 F) n (fun x => (↑e ⟨x, s x⟩).2) a x₀)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.forallTelescopeReducingAuxAux.process : {α : Type} →
  Bool →
    Option ℕ →
      (Array Lean.Expr → Lean.Expr → Lean.MetaM α) →
        Bool → Bool → Lean.LocalContext → Array Lean.Expr → ℕ → Lean.Expr → Lean.MetaM α
-- Lean.Declaration
/-- It supports K-like reduction.
A recursor is said to support K-like reduction if one can assume it behaves
like `Eq` under axiom `K` --- that is, it is an inductive predicate (i.e., it lives in `Prop`),
it has exactly one constructor, and that constructor has 0 fields.

Examples of inductives with K-like reduction are `Eq`, `HEq`, and `True`.
Non-examples include those with multiple constructors (like `Or`)
and those whose constructor has one or more fields (like `And`, `Exists`,
and `Nonempty').
 -/
Lean.RecursorVal.k : Lean.RecursorVal → Bool
-- Mathlib.Tactic.NormNum.Basic
/-- Consider an `Option` as an object in the `MetaM` monad, by throwing an error on `none`.  -/
Mathlib.Meta.monadLiftOptionMetaM : MonadLift Option Lean.MetaM
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivativeFun_add : ∀ {R : Type u_1} [inst : CommSemiring R] (f g : PowerSeries R),
  (f + g).derivativeFun = f.derivativeFun + g.derivativeFun
-- Init.Data.String.Search
String.anyAux : String → String.Pos.Raw → (Char → Bool) → String.Pos.Raw → Bool
-- Mathlib.Combinatorics.Colex
/-- Being a nonempty initial segment of colex is equivalent to being an `initSeg`.  -/
Finset.Colex.isInitSeg_iff_exists_initSeg : ∀ {α : Type u_1} [inst : LinearOrder α] {𝒜 : Finset (Finset α)} {r : ℕ} [inst_1 : Fintype α],
  Finset.Colex.IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ s, s.card = r ∧ 𝒜 = Finset.Colex.initSeg s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.differentiable_iteratedDeriv_sin : ∀ (n : ℕ), Differentiable ℂ (iteratedDeriv n Complex.sin)
-- Init.Data.String.Lemmas.Pattern.Memcmp
_private.Init.Data.String.Lemmas.Pattern.Memcmp.0.String.Slice.Pattern.Internal.memcmpStr.go.eq_1 : ∀ (lhs rhs : String) (lstart rstart len : String.Pos.Raw) (h1 : len.offsetBy lstart ≤ lhs.rawEndPos)
  (h2 : len.offsetBy rstart ≤ rhs.rawEndPos) (curr : String.Pos.Raw),
  String.Slice.Pattern.Internal.memcmpStr.go✝ lhs rhs lstart rstart len h1 h2 curr =
    if h : curr < len then
      have hl := ⋯;
      have hr := ⋯;
      if (lhs.getUTF8Byte (curr.offsetBy lstart) hl == rhs.getUTF8Byte (curr.offsetBy rstart) hr) = true then
        String.Slice.Pattern.Internal.memcmpStr.go✝ lhs rhs lstart rstart len h1 h2 curr.inc
      else false
    else true
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.norm.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.norm c = Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.norm c_1) =
    (c = c_1)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Construct the normalized expression of a 2-morphism `α ≫ η ≫ ηs` recursively.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.cons : Mathlib.Tactic.BicategoryLike.Mor₂ →
  Mathlib.Tactic.BicategoryLike.Structural →
    Mathlib.Tactic.BicategoryLike.WhiskerLeft →
      Mathlib.Tactic.BicategoryLike.NormalExpr → Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instAddMonoid : {𝕜 : Type u_2} → {α : Type u_5} → [inst : AddMonoid 𝕜] → [inst_1 : LE α] → AddMonoid (IncidenceAlgebra 𝕜 α)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
measurable_coe_nnreal_ennreal_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal}, (Measurable fun x => ↑(f x)) ↔ Measurable f
-- Init.Data.Int.Linear
Int.Internal.Linear.cmod_gt_of_pos : ∀ (a : ℤ) {b : ℤ}, 0 < b → Int.Internal.Linear.cmod a b > -b
-- Mathlib.Order.PiLex
Pi.instDenselyOrderedLexForall : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → LT (β i)] [∀ (i : ι), DenselyOrdered (β i)],
  DenselyOrdered (Lex ((i : ι) → β i))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_of_mem_keysArray : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, k ∈ m.keysArray → m.contains k = true
-- Mathlib.Algebra.Ring.Subring.Defs
Subsemiring.toSubring_toSubsemiring : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subsemiring R) (hneg : -1 ∈ s), (s.toSubring hneg).toSubsemiring = s
-- Batteries.Data.String.Lemmas
String.drop_empty : ∀ {n : ℕ}, String.Legacy.drop "" n = ""
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- Naturally isomorphic endofunctors give equivalent categories of coalgebras.
Furthermore, they are equivalent as categories over `C`, that is,
we have `equiv_of_nat_iso h ⋙ forget = forget`.
 -/
CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C C} →
      (F ≅ G) → (CategoryTheory.Endofunctor.Coalgebra F ≌ CategoryTheory.Endofunctor.Coalgebra G)
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
/-- Consider the contravariant functors between compact Hausdorff spaces and commutative unital
C⋆algebras `F : Cpct → CommCStarAlg := X ↦ C(X, ℂ)` and
`G : CommCStarAlg → Cpct := A → characterSpace ℂ A` whose actions on morphisms are given by
`WeakDual.CharacterSpace.compContinuousMap` and `ContinuousMap.compStarAlgHom'`, respectively.

Then `η : id → G ∘ F := WeakDual.CharacterSpace.homeoEval` is a natural isomorphism implementing
(half of) the duality between these categories. That is, for compact Hausdorff spaces `X` and `Y`,
`f : C(X, Y)` the following diagram commutes:

```
X  --- η X ---> characterSpace ℂ C(X, ℂ)

|                     |

f                  (G ∘ F) f

|                     |
V                     V

Y  --- η Y ---> characterSpace ℂ C(Y, ℂ)
```
 -/
WeakDual.CharacterSpace.homeoEval_naturality : ∀ {X : Type u_1} {Y : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [inst_2 : CompactSpace X]
  [inst_3 : T2Space X] [inst_4 : TopologicalSpace Y] [inst_5 : CompactSpace Y] [inst_6 : T2Space Y] (f : C(X, Y)),
  (↑(WeakDual.CharacterSpace.homeoEval Y 𝕜)).comp f =
    (WeakDual.CharacterSpace.compContinuousMap (ContinuousMap.compStarAlgHom' 𝕜 𝕜 f)).comp
      ↑(WeakDual.CharacterSpace.homeoEval X 𝕜)
-- Mathlib.Order.Concept
Concept.intent_ofIsExtent : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) (hs : Order.IsExtent r s),
  (Concept.ofIsExtent r s hs).intent = upperPolar r s
-- Lean.MetavarContext
Lean.getLevelMVarAssignmentExp : Lean.MetavarContext → Lean.LMVarId → Option Lean.Level
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Negating both vectors passed to `oangle` does not change the angle.  -/
Orientation.oangle_neg_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), o.oangle (-x) (-y) = o.oangle x y
-- Mathlib.Algebra.Group.Action.Hom
Function.Surjective.addActionLeft.eq_1 : ∀ {R : Type u_4} {S : Type u_5} {M : Type u_6} [inst : AddMonoid R] [inst_1 : AddAction R M] [inst_2 : AddMonoid S]
  [inst_3 : VAdd S M] (f : R →+ S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x),
  Function.Surjective.addActionLeft f hf hsmul = { toVAdd := inst_3, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Probability.Independence.BoundedContinuousFunction
pi_indepFun_of_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4} {H : Type u_7}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] [inst_4 : TopologicalSpace H] [inst_5 : MeasurableSpace H] [BorelSpace H]
  [HasOuterApproxClosed H] {X : (s : S) → Ω → E s} {U : Ω → H} [MeasureTheory.IsFiniteMeasure P] [Finite S],
  (∀ (s : S), AEMeasurable (X s) P) →
    AEMeasurable U P →
      (∀ (f : BoundedContinuousFunction ((s : S) → E s) ℝ) (g : BoundedContinuousFunction H ℝ),
          ∫ (x : Ω), (fun ω => (f fun x => X x ω) * g (U ω)) x ∂P =
            (∫ (x : Ω), (fun ω => f fun x => X x ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P) →
        ProbabilityTheory.IndepFun (fun ω s => X s ω) U P
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon : ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instDecidableEqOfLawfulBEq : {α : Type u} → [inst : BEq α] → [LawfulBEq α] → [inst_2 : Hashable α] → DecidableEq (Std.ExtHashSet α)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The proposition that a sequence indexed by `ℤ` is an EDS.  -/
IsEllipticDvdSequence : {R : Type u_1} → [CommRing R] → (ℤ → R) → Prop
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.right_distrib : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F ((x.add y).mul z) ((x.mul z).add (y.mul z))
-- Init.Data.List.Nat.Modify
List.modify_modify_eq : ∀ {α : Type u_1} (f g : α → α) (i : ℕ) (l : List α), (l.modify i f).modify i g = l.modify i (g ∘ f)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseTR.go.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (l : List α) (a : α) (a_1 : Array α), List.eraseTR.go✝ l a [] a_1 = l
-- Mathlib.Topology.Order.LocalExtr
IsMaxOn.isLocalMax : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn f s a → s ∈ nhds a → IsLocalMax f a
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mk : {α : Type u_2} →
  [inst : BooleanAlgebra α] →
    (toSublattice : Sublattice α) →
      (∀ {a : α}, a ∈ toSublattice.carrier → aᶜ ∈ toSublattice.carrier) → ⊥ ∈ toSublattice.carrier → BooleanSubalgebra α
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp : ∀ {n : ℕ} [NeZero n] {A : Type w} {K : Type u} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra K A]
  [IsDomain A] {ζ : A} [IsCyclotomicExtension {n} K A],
  IsPrimitiveRoot ζ n →
    Irreducible (Polynomial.cyclotomic n K) → minpoly K (ζ - 1) = (Polynomial.cyclotomic n K).comp (Polynomial.X + 1)
-- Mathlib.GroupTheory.Subsemigroup.Center
/-- The center of a semigroup `M` is the set of elements that commute with everything in `M`  -/
Subsemigroup.center : (M : Type u_1) → [inst : Mul M] → Subsemigroup M
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- If all bifunctors `Jᵒᵖ ⥤ J ⥤ C` have an end, then the construction
`F ↦ end_ F` defines a functor `(Jᵒᵖ ⥤ J ⥤ C) ⥤ C`.  -/
CategoryTheory.Limits.endFunctor : (J : Type u) →
  [inst : CategoryTheory.Category.{v, u} J] →
    (C : Type u') →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        [∀ (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)), CategoryTheory.Limits.HasEnd F] →
          CategoryTheory.Functor (CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) C
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.edist_map : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (x y : P),
  edist (f x) (f y) = edist x y
-- Mathlib.Order.Category.LinOrd
LinOrd.hom_id : ∀ {X : LinOrd}, LinOrd.Hom.hom (CategoryTheory.CategoryStruct.id X) = OrderHom.id
-- Mathlib.Data.Sym.Basic
/-- This is the quotient map that takes a list of n elements as an n-tuple and produces an nth
symmetric power.
 -/
Sym.ofVector : {α : Type u_1} → {n : ℕ} → List.Vector α n → Sym α n
-- Init.Data.SInt.Lemmas
Int32.toISize_toInt64 : ∀ (n : Int32), n.toInt64.toISize = n.toISize
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {fallback : α}, t.getKey! (t.minKeyD fallback) = t.minKeyD fallback
-- Mathlib.Data.Rat.Init
/-- Canonical homomorphism from `ℚ≥0` to a division semiring `K`.

This is just the bare function in order to aid in creating instances of `DivisionSemiring`.  -/
NNRat.cast : {K : Type u_1} → [NNRatCast K] → ℚ≥0 → K
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Max α] [inst_1 : Max β] [inst_2 : Bot α] [inst_3 : Bot β]
  (toSupHom : SupHom α β) (map_bot' : toSupHom.toFun ⊥ = ⊥) (toSupHom_1 : SupHom α β)
  (map_bot'_1 : toSupHom_1.toFun ⊥ = ⊥),
  ({ toSupHom := toSupHom, map_bot' := map_bot' } = { toSupHom := toSupHom_1, map_bot' := map_bot'_1 }) =
    (toSupHom = toSupHom_1)
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- A split equalizer clearly induces a fork.  -/
CategoryTheory.IsSplitEqualizer.asFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} → {W : C} → {h : W ⟶ X} → CategoryTheory.IsSplitEqualizer f g h → CategoryTheory.Limits.Fork f g