mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
fderivWithin_continuousAlternatingMap_apply_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F [⋀^ι]→L[𝕜] G} {g : ι → E → F} {s : Set E}
  {x : E} [inst_7 : Fintype ι] [inst_8 : DecidableEq ι],
  DifferentiableWithinAt 𝕜 f s x →
    (∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x) →
      UniqueDiffWithinAt 𝕜 s x →
        ∀ (dx : E),
          (fderivWithin 𝕜 (fun x => (f x) fun x_1 => g x_1 x) s x) dx =
            (((fderivWithin 𝕜 f s x) dx) fun x_1 => g x_1 x) +
              ∑ i, (f x) (Function.update (fun x_1 => g x_1 x) i ((fderivWithin 𝕜 (g i) s x) dx))
-- Mathlib.LinearAlgebra.Matrix.Orthogonal
Matrix.HasOrthogonalRows.hasOrthogonalCols : ∀ {α : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Mul α] [inst_1 : AddCommMonoid α] {A : Matrix m n α}
  [inst_2 : Fintype m], A.transpose.HasOrthogonalRows → A.HasOrthogonalCols
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Path.right.inj : ∀ {α : Type u} {c : RBTree.RBColor} {l : RBTree.RBNode α} {v : α} {parent : RBTree.RBNode.Path α} {c_1 : RBTree.RBColor}
  {l_1 : RBTree.RBNode α} {v_1 : α} {parent_1 : RBTree.RBNode.Path α},
  RBTree.RBNode.Path.right c l v parent = RBTree.RBNode.Path.right c_1 l_1 v_1 parent_1 →
    c = c_1 ∧ l = l_1 ∧ v = v_1 ∧ parent = parent_1
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.reachable_of_edist_ne_top : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.edist u v ≠ ⊤ → G.Reachable u v
-- Aesop.Frontend.Extension.Init
Aesop.DeclaredRuleSets.mk.inj : ∀ {ruleSets : Std.HashMap Aesop.RuleSetName (Aesop.RuleSetExtension × Lean.Name × Lean.Name)}
  {defaultRuleSets : Std.HashSet Aesop.RuleSetName}
  {ruleSets_1 : Std.HashMap Aesop.RuleSetName (Aesop.RuleSetExtension × Lean.Name × Lean.Name)}
  {defaultRuleSets_1 : Std.HashSet Aesop.RuleSetName},
  { ruleSets := ruleSets, defaultRuleSets := defaultRuleSets } =
      { ruleSets := ruleSets_1, defaultRuleSets := defaultRuleSets_1 } →
    ruleSets = ruleSets_1 ∧ defaultRuleSets = defaultRuleSets_1
-- Batteries.Data.List.Lemmas
List.dropPrefix?_append_of_beq : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α} (p : List α), (l₁ == l₂) = true → (l₁ ++ p).dropPrefix? l₂ = some p
-- Init.Data.Array.Lemmas
Array.size_reverse : ∀ {α : Type u_1} {xs : Array α}, xs.reverse.size = xs.size
-- Mathlib.Control.Random
/-- A monad to generate random objects using the generator type `g`.  -/
RandG : Type → Type u_1 → Type u_1
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- Given an adjunction `F ⊣ G` such that `F` preserves monos, `G` maps an injective presentation
of `X` to an injective presentation of `G(X)`.  -/
CategoryTheory.Adjunction.mapInjectivePresentation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              [F.PreservesMonomorphisms] →
                (X : D) → CategoryTheory.InjectivePresentation X → CategoryTheory.InjectivePresentation (G.obj X)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.coe_nnreal_real : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal}, Measurable f → Measurable fun x => ↑(f x)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_insertMany_emptyWithCapacity_list_le : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).size ≤ l.length
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_empty : ∀ {R : Type u} [inst : NonAssocRing R], Subring.closure ∅ = ⊥
-- Std.Data.Iterators.Combinators.DropWhile
/-- Given an iterator `it` and a predicate `P`, `it.dropWhile P` is an iterator that
emits the values emitted by `it` starting from the first value that is rejected by `P`.
The elements before are dropped.

In situations where `P` is monadic, use `dropWhileM` instead.

**Marble diagram:**

Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:

```text
it               ---a----b---c--d-e--⊥
it.dropWhile P   ------------c--d-e--⊥

it               ---a----⊥
it.dropWhile P   --------⊥
```

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite

Depending on `P`, it is possible that `it.dropWhileM P` is productive although
`it` is not. In this case, the `Productive` instance needs to be proved manually.

**Performance:**

This combinator calls `P` on each output of `it` until the predicate evaluates to false. After
that, the combinator incurs an additional O(1) cost for each value emitted by `it`.
 -/
Std.Iter.dropWhile : {α β : Type w} → (P : β → Bool) → Std.Iter β → Std.Iter β
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.instFaithfulRingObjCatForget₂RingObjCat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], (CategoryTheory.CommRingObjCat.forget₂RingObjCat C).Faithful
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.map_p₃_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] {Z : D} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ hf₁ f₂ f₃))
      (CategoryTheory.CategoryStruct.comp f₃ h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.relativelyRepresentable.pullback₃.π hf₁ f₂ f₃) h
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.instIsContinuous : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D)
  [CategoryTheory.Functor.IsDenseSubsite J K G], G.IsContinuous J K
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_Ico' : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, x ∈ Finset.Ico a b ↔ x < b ∧ a ≤ x
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.Smooth.formallySmooth : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, f.Smooth → f.FormallySmooth
-- Mathlib.Order.WellFounded
WellFoundedLT.toOrderBot.eq_1 : ∀ (α : Type u_4) [inst : LinearOrder α] [inst_1 : Nonempty α] [h : WellFoundedLT α],
  WellFoundedLT.toOrderBot α = { bot := ⋯.min Set.univ ⋯, bot_le := ⋯ }
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is meromorphic in normal form on `U` and nowhere locally constant zero,
then its zero set equals the support of the associated divisor.
 -/
MeromorphicNFOn.zero_set_eq_divisor_support : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicNFOn f U →
    (∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤) → U ∩ f ⁻¹' {0} = Function.support ⇑(MeromorphicOn.divisor f U)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.mk.injEq : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  (toFun : X → Y) (map_smul' : ∀ (m : M) (x : X), toFun (m • x) = φ m • toFun x) (toFun_1 : X → Y)
  (map_smul'_1 : ∀ (m : M) (x : X), toFun_1 (m • x) = φ m • toFun_1 x),
  ({ toFun := toFun, map_smul' := map_smul' } = { toFun := toFun_1, map_smul' := map_smul'_1 }) = (toFun = toFun_1)
-- Mathlib.Data.Prod.Basic
Prod.map_snd' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ),
  Prod.snd ∘ Prod.map f g = g ∘ Prod.snd
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instIsCentralScalar : ∀ {S : Type u_2} {R : Type u_3} {A : Type u_4} [inst : SMul S R] [inst_1 : SMul S A] [inst_2 : SMul Sᵐᵒᵖ R]
  [inst_3 : SMul Sᵐᵒᵖ A] [IsCentralScalar S R] [IsCentralScalar S A], IsCentralScalar S (Unitization R A)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instReflectsIsomorphismsForgetContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite : (CategoryTheory.forget ProfiniteAddGrp.{u}).ReflectsIsomorphisms
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.map_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} {α : F ⟶ G}
  (X : CategoryTheory.Grothendieck F),
  (CategoryTheory.Grothendieck.map α).obj X = { base := X.base, fiber := (α.app X.base).toFunctor.obj X.fiber }
-- Mathlib.CategoryTheory.Functor.Category
/-- `Functor.category C D` gives the category structure on functors and natural transformations
between categories `C` and `D`.

Notice that if `C` and `D` are both small categories at the same universe level,
this is another small category at that level.
However if `C` and `D` are both large categories at the same universe level,
this is a small category at the next higher level.
 -/
CategoryTheory.Functor.category : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (CategoryTheory.Functor C D)
-- Mathlib.Data.Multiset.Bind
Multiset.Nodup.product : ∀ {α : Type u_1} {β : Type v} {s : Multiset α} {t : Multiset β}, s.Nodup → t.Nodup → (s ×ˢ t).Nodup
-- Mathlib.Order.Category.NonemptyFinLinOrd
/-- **Alias** of `Fin.homSucc`.

---

The generating arrow `i ⟶ i+1` in the category `Fin n`  -/
Fin.hom_succ : {n : ℕ} → (i : Fin n) → i.castSucc ⟶ i.succ
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_ofNatLT : ∀ {n : ℕ} (hn : n < 2 ^ 64), { toBitVec := n#'hn } = UInt64.ofNatLT n hn
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mk.injEq : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (carrier : Set M)
  (fun_mem : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier) (carrier_1 : Set M)
  (fun_mem_1 : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier_1),
  ({ carrier := carrier, fun_mem := fun_mem } = { carrier := carrier_1, fun_mem := fun_mem_1 }) = (carrier = carrier_1)
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `HasStrictDerivAt.finsetProd`. -/
HasStrictDerivAt.finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι] {𝔸' : Type u_3}
  [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'} {f' : ι → 𝔸'},
  (∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x) →
    HasStrictDerivAt (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.natTrans_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁}
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ⟶ G.obj i)
  (i : CategoryTheory.Discrete I), (CategoryTheory.Discrete.natTrans f).app i = f i
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedMul.toIsOrderedMonoid : ∀ {α : Type u} [inst : CommMonoid α] [inst_1 : Preorder α] [CanonicallyOrderedMul α], IsOrderedMonoid α
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- A reflexive cofork is a colimit cocone if and only if the underlying cofork is.  -/
CategoryTheory.Limits.ReflexiveCofork.isColimitEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) →
      (G : CategoryTheory.Limits.ReflexiveCofork F) →
        CategoryTheory.Limits.IsColimit G.toCofork ≃ CategoryTheory.Limits.IsColimit G
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.Const.getThenInsertIfNew?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α fun x => β) (a : α) (b : β),
  Std.DHashMap.Raw.Const.getThenInsertIfNew? m a b =
    if h : 0 < m.buckets.size then
      match Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? ⟨m, h⟩ a b with
      | (replaced, ⟨r, property⟩) => (replaced, r)
    else (none, m)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- If `f : ι → G × G` converges to the uniformity, then any `g : ι → G × G` converges to the
uniformity iff `f * g` does. This is often useful when `f` is valued in the diagonal,
in which case its convergence is automatic.  -/
Filter.Tendsto.uniformity_mul_iff_right : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {f g : ι → α × α}
  {l : Filter ι},
  Filter.Tendsto f l (uniformity α) → (Filter.Tendsto (f * g) l (uniformity α) ↔ Filter.Tendsto g l (uniformity α))
-- Mathlib.Order.LatticeIntervals
Set.Iic.semilatticeInf : {α : Type u_1} → {a : α} → [inst : SemilatticeInf α] → SemilatticeInf ↑(Set.Iic a)
-- Mathlib.Combinatorics.Hindman
/-- The strong form of **Hindman's theorem**: in any finite
cover of an FS-set, one the parts contains an FS-set.  -/
Hindman.FS_partition_regular : ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M) (s : Set (Set M)),
  s.Finite → Hindman.FS a ⊆ ⋃₀ s → ∃ c ∈ s, ∃ b, Hindman.FS b ⊆ c
-- Mathlib.Data.FunLike.Graded
/-- The class `GradedEquivLike E 𝒜 ℬ` says that `E` is a type of grading-preserving isomorphisms
between `𝒜` and `ℬ`. It is the combination of `GradedFunLike E 𝒜 ℬ` and `EquivLike E A B`.  -/
GradedEquivLike : (E : Type u_1) →
  {A : outParam (Type u_2)} →
    {B : outParam (Type u_3)} →
      {σ : outParam (Type u_4)} →
        {τ : outParam (Type u_5)} →
          {ι : outParam (Type u_6)} →
            [SetLike σ A] → [SetLike τ B] → outParam (ι → σ) → outParam (ι → τ) → [EquivLike E A B] → Prop
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.orElse_Option : ∀ {α : Type} (x : Option α) (h : Unit → Option α) (post : α → Prop) (epost : Prop),
  ⦃ Std.Internal.Do.wp x post (Std.Internal.Do.wp (h ()) post epost) ⦄ OrElse.orElse x h ⦃ post; epost ⦄
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.symm_bijective : ∀ {ι : Type u_1}, Function.Bijective ComplexShape.symm
-- Init.Data.UInt.Bitwise
UInt8.ofNatLT_and : ∀ (a b : ℕ) (ha : a < 2 ^ 8) (hb : b < 2 ^ 8), UInt8.ofNatLT (a &&& b) ⋯ = UInt8.ofNatLT a ha &&& UInt8.ofNatLT b hb
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Ioi_iff : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ : α}, a₁ ≤ b₁ → (Set.Icc a₁ b₁ ⊆ Set.Ioi a₂ ↔ a₂ < a₁)
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.lift.congr_simp : ∀ {N : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group N] [inst_1 : Group G] [inst_2 : Group H]
  {φ : G →* MulAut N} (fn fn_1 : N →* H) (e_fn : fn = fn_1) (fg fg_1 : G →* H) (e_fg : fg = fg_1)
  (h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn),
  SemidirectProduct.lift fn fg h = SemidirectProduct.lift fn_1 fg_1 ⋯
-- Mathlib.Analysis.Normed.Group.Continuity
continuous_norm : ∀ {E : Type u_4} [inst : SeminormedAddGroup E], Continuous fun a => ‖a‖
-- Lean.Parser.Syntax
Lean.Parser.Command.mixfix : Lean.Parser.Parser
-- Mathlib.Data.Nat.Factorization.Root
Nat.ceilRoot_pow_self : ∀ {n : ℕ}, n ≠ 0 → ∀ (a : ℕ), n.ceilRoot (a ^ n) = a
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.instCoeOutToType : (o : Ordinal.{u_1}) → CoeOut o.ToType Ordinal.{u_1}
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
fderivWithin_comp_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {x : E} (c : 𝕜),
  UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (fun x => f (c • x)) s x = c • fderivWithin 𝕜 f (c • s) (c • x)
-- Mathlib.Data.Set.Function
Set.exists_image_eq_injOn_of_subset_range : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β}, t ⊆ Set.range f → ∃ s, f '' s = t ∧ Set.InjOn f s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF → ∀ {k a : α} {v : β}, (m.insert k v)[a]! = if (k == a) = true then v else m[a]!
-- Mathlib.Data.Countable.Defs
instCountablePUnit : Countable PUnit.{u}
-- Mathlib.Data.Rat.Lemmas
Rat.inv_intCast_den_of_pos : ∀ {a : ℤ}, 0 < a → ↑(↑a)⁻¹.den = a
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.TheoremsArray.insert : {α : Type} → [Lean.Meta.Grind.TheoremLike α] → Lean.Meta.Grind.TheoremsArray α → α → Lean.Meta.Grind.TheoremsArray α
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.prod.inl_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.inl X Y)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Net.Addr
Std.Net.IPv4Addr.instCoeIPAddr : Coe Std.Net.IPv4Addr Std.Net.IPAddr
-- Mathlib.GroupTheory.Schreier
/-- If `G` has `n` commutators `[g₁, g₂]`, then `|G'| ∣ [G : Z(G)] ^ ([G : Z(G)] * n + 1)`,
where `G'` denotes the commutator of `G`.  -/
Subgroup.card_commutator_dvd_index_center_pow : ∀ (G : Type u_1) [inst : Group G] [Finite ↑(commutatorSet G)],
  Nat.card ↥(commutator G) ∣ (Subgroup.center G).index ^ ((Subgroup.center G).index * Nat.card ↑(commutatorSet G) + 1)
-- Init.Data.BitVec.Lemmas
/-- Extracting a bitvector from `flattenList`, when we only extract from a single bitvector.
 -/
BitVec.extractLsb_flattenList : ∀ (hi lo : ℕ) {w : ℕ} (vs : List (BitVec w)) (w₁ : lo ≤ hi),
  hi < w * vs.length →
    ∀ (h : hi / w = lo / w),
      BitVec.extractLsb hi lo (BitVec.flattenList vs) =
        BitVec.cast ⋯ (BitVec.extractLsb (hi % w) (lo % w) (vs[vs.length - 1 - hi / w]?.getD 0#w))
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.sum_left : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) {α : Type u_7} (t : Finset α) (g : α → M) (w : M),
  (B (∑ i ∈ t, g i)) w = ∑ i ∈ t, (B (g i)) w
-- Mathlib.Data.PNat.Basic
PNat.add_sub : ∀ {a b : ℕ+}, a + b - b = a
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousAt_inv_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : CommGroup β] [IsOrderedMonoid β], UpperSemicontinuousAt f⁻¹ a ↔ LowerSemicontinuousAt f a
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.homEquivOfIso_symm_apply : ∀ {V W : CategoryTheory.Quiv} (e : V ≅ W) {X Y : ↑V} (g : e.hom.obj X ⟶ e.hom.obj Y),
  (CategoryTheory.Quiv.homEquivOfIso e).symm g = Quiver.homOfEq (e.inv.map g) ⋯ ⋯
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_apply_mono : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] (u : ι → Ω → β) (s : Set β)
  (ω : Ω), Monotone fun x => MeasureTheory.hittingAfter u s x ω
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.TM2.step.match_1.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Cfg Γ Λ σ → Sort u_5) (var : σ)
  (stk : (k : K) → List (Γ k))
  (h_1 : (var : σ) → (stk : (k : K) → List (Γ k)) → motive { l := none, var := var, stk := stk })
  (h_2 : (l : Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive { l := some l, var := v, stk := S }),
  (match { l := none, var := var, stk := stk } with
    | { l := none, var := var, stk := stk } => h_1 var stk
    | { l := some l, var := v, stk := S } => h_2 l v S) =
    h_1 var stk
-- Lean.Meta.AppBuilder
_private.Lean.Meta.AppBuilder.0.Lean.Meta.mkAndIntroN.go : List Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Init.Data.List.Lex
List.le_of_cons_le_cons : ∀ {α : Type u_1} [inst : LT α] [i₀ : Std.Irrefl fun x1 x2 => x1 < x2] [i₁ : Std.Asymm fun x1 x2 => x1 < x2]
  [i₂ : Std.Trichotomous fun x1 x2 => x1 < x2] {a : α} {l₁ l₂ : List α}, a :: l₁ ≤ a :: l₂ → l₁ ≤ l₂
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.mul_adjMatrix_apply : ∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] (M : Matrix V V α) (v w : V),
  (M * SimpleGraph.adjMatrix α G) v w = ∑ u ∈ G.neighborFinset w, M v u
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- For any `g ∈ GL(2, ℚ)` and `M ≠ 0`, there exists `N` such that `g x g⁻¹ ∈ Γ(M)` for all
`x ∈ Γ(N)`.  -/
CongruenceSubgroup.exists_Gamma_le_conj : ∀ (g : GL (Fin 2) ℚ) (M : ℕ) [NeZero M],
  ∃ N,
    N ≠ 0 ∧
      ∀ x ∈ CongruenceSubgroup.Gamma N,
        g * (Matrix.SpecialLinearGroup.mapGL ℚ) x * g⁻¹ ∈
          Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma M)
-- Init.Prelude
/-- The homogeneous version of `Pow` where the exponent is a `Nat`.
The purpose of this class is that it provides a default `Pow` instance,
which can be used to specialize the exponent to `Nat` during elaboration.

For example, if `x ^ 2` should preferentially elaborate with `2 : Nat` then `x`'s type should
provide an instance for this class.  -/
NatPow : Type u → Type u
-- Init.Prelude
Lean.MacroScopesView.mk : Lean.Name → Lean.Name → Lean.Name → List Lean.MacroScope → Lean.MacroScopesView
-- Init.Data.List.TakeDrop
List.take.eq_2 : ∀ {α : Type u} (n : ℕ), List.take n.succ [] = []
-- Mathlib.Topology.Order
/-- The `TopologicalSpace` structure on a type with discrete topology is equal to `⊥`.  -/
DiscreteTopology.eq_bot : ∀ {α : Type u_2} {t : TopologicalSpace α} [self : DiscreteTopology α], t = ⊥
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.map_add : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [inst : Add α] [inst_1 : Add β] (f : α → β),
  (∀ (a₁ a₂ : α), f (a₁ + a₂) = f a₁ + f a₂) → ∀ (M N : Matrix m n α), (M + N).map f = M.map f + N.map f
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.IsUniversallyEffectiveEquivalenceRelation.nonempty_universallyEffectiveEquivalenceRelation : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {R A : C} {p₁ p₂ : R ⟶ A}
  [self : CategoryTheory.IsUniversallyEffectiveEquivalenceRelation p₁ p₂],
  Nonempty (CategoryTheory.UniversallyEffectiveEquivalenceRelation p₁ p₂)
-- Lean.Parser.Term
Lean.Parser.Term.logNamedErrorAtMacro.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Complex.GammaSeq_mul : ∀ (z : ℂ) {n : ℕ},
  n ≠ 0 →
    z.GammaSeq n * (1 - z).GammaSeq n = ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.awayι.congr_simp : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m m_1 : ℕ} (e_m : m = m_1) (f_deg : f ∈ 𝒜 m) (hm : 0 < m),
  AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm = AlgebraicGeometry.Proj.awayι 𝒜 f ⋯ ⋯
-- Init.Data.Nat.Bitwise.Basic
Nat.instShiftRight : ShiftRight ℕ
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- If `p` is a submodule that is equal to `⊤`, then `LinearIsometryEquiv.ofTop p hp` is the
"identity" equivalence between `p` and `E`.  -/
LinearIsometryEquiv.ofTop : (E : Type u_5) →
  [inst : SeminormedAddCommGroup E] →
    {R : Type u_12} → [inst_1 : Ring R] → [inst_2 : Module R E] → (p : Submodule R E) → p = ⊤ → ↥p ≃ₗᵢ[R] E