mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.RuleSet
Aesop.BaseRuleSet.mk.injEq : ∀ (normRules : Aesop.Index Aesop.NormRuleInfo) (unsafeRules : Aesop.Index Aesop.UnsafeRuleInfo)
  (safeRules : Aesop.Index Aesop.SafeRuleInfo) (unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name))
  (forwardRules : Aesop.ForwardIndex) (forwardRuleNames : Lean.PHashSet Aesop.RuleName)
  (rulePatterns : Aesop.RulePatternIndex) (erased : Lean.PHashSet Aesop.RuleName)
  (ruleNames : Lean.PHashMap Lean.Name (Aesop.UnorderedArraySet Aesop.RuleName))
  (normRules_1 : Aesop.Index Aesop.NormRuleInfo) (unsafeRules_1 : Aesop.Index Aesop.UnsafeRuleInfo)
  (safeRules_1 : Aesop.Index Aesop.SafeRuleInfo) (unfoldRules_1 : Lean.PHashMap Lean.Name (Option Lean.Name))
  (forwardRules_1 : Aesop.ForwardIndex) (forwardRuleNames_1 : Lean.PHashSet Aesop.RuleName)
  (rulePatterns_1 : Aesop.RulePatternIndex) (erased_1 : Lean.PHashSet Aesop.RuleName)
  (ruleNames_1 : Lean.PHashMap Lean.Name (Aesop.UnorderedArraySet Aesop.RuleName)),
  ({ normRules := normRules, unsafeRules := unsafeRules, safeRules := safeRules, unfoldRules := unfoldRules,
        forwardRules := forwardRules, forwardRuleNames := forwardRuleNames, rulePatterns := rulePatterns,
        erased := erased, ruleNames := ruleNames } =
      { normRules := normRules_1, unsafeRules := unsafeRules_1, safeRules := safeRules_1, unfoldRules := unfoldRules_1,
        forwardRules := forwardRules_1, forwardRuleNames := forwardRuleNames_1, rulePatterns := rulePatterns_1,
        erased := erased_1, ruleNames := ruleNames_1 }) =
    (normRules = normRules_1 ∧
      unsafeRules = unsafeRules_1 ∧
        safeRules = safeRules_1 ∧
          unfoldRules = unfoldRules_1 ∧
            forwardRules = forwardRules_1 ∧
              forwardRuleNames = forwardRuleNames_1 ∧
                rulePatterns = rulePatterns_1 ∧ erased = erased_1 ∧ ruleNames = ruleNames_1)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_roo_eq_zero : ∀ {m n i : ℕ}, n ≤ i + (m + 1) → (m<...n).toList[i]! = 0
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmodRepr_eq_zero_iff_dvd : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {x : ℤ_[p]}, x.zmodRepr = 0 ↔ ↑p ∣ x
-- Aesop.Rule.Name
Aesop.ScopeName.global : Aesop.ScopeName
-- Std.Time.Date.Unit.Month
Std.Time.Month.instLawfulEqOrdOffset : Std.LawfulEqOrd Std.Time.Month.Offset
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instRxcIsAlwaysFinite : ∀ {n : ℕ}, Std.Rxc.IsAlwaysFinite (BitVec n)
-- Mathlib.Analysis.Normed.Ring.Basic
nnnormHom_apply : ∀ {α : Type u_2} [inst : SeminormedRing α] [inst_1 : NormOneClass α] [inst_2 : NormMulClass α] (x : α),
  nnnormHom x = ‖x‖₊
-- Mathlib.Order.Category.BddOrd
/-- Constructs an equivalence between bounded orders from an order isomorphism between them.  -/
BddOrd.Iso.mk : {α β : BddOrd} → ↑α.toPartOrd ≃o ↑β.toPartOrd → (α ≅ β)
-- Mathlib.Analysis.Complex.Exponential
Real.pow_div_factorial_le_exp : ∀ (x : ℝ), 0 ≤ x → ∀ (n : ℕ), x ^ n / ↑n.factorial ≤ Real.exp x
-- Init.Sym.Lemmas
Lean.Sym.dite_false : ∀ {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬c → α) {ht : ¬c}, dite c a b = b ht
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.toCoalgebra : {R : Type u} → {A : Type v} → {inst : CommSemiring R} → {inst_1 : Semiring A} → [self : Bialgebra R A] → Coalgebra R A
-- Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
Finset.prod_inv_index : ∀ {α : Type u_1} {ι : Type u_2} [inst : CommMonoid α] [inst_1 : DecidableEq ι] [inst_2 : InvolutiveInv ι] (s : Finset ι)
  (f : ι → α), ∏ i ∈ s⁻¹, f i = ∏ i ∈ s, f i⁻¹
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- If `H` is a characteristic additive subgroup of `G` and `K` is a characteristic additive
subgroup of `H`, then `K` is a characteristic additive subgroup of `G`.  -/
AddSubgroup.characteristic_of_characteristic_of_characteristic : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} [H.Characteristic] {K : AddSubgroup ↥H}
  [hK : K.Characteristic], (AddSubgroup.map H.subtype K).Characteristic
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_finsetProd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {g : ι → E → 𝔸'} [inst_5 : DecidableEq ι] {x : E},
  UniqueDiffWithinAt 𝕜 s x →
    (∀ i ∈ u, DifferentiableWithinAt 𝕜 (g i) s x) →
      fderivWithin 𝕜 (fun x => ∏ i ∈ u, g i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • fderivWithin 𝕜 (g i) s x
-- Mathlib.Topology.Constructions
/-- Let `s, t ⊆ X` be two subsets of a topological space `X`.  If `t ⊆ s` and `s` is discrete,
then `t` is discrete.

(Compare `DiscreteTopology.of_subset` which is the same thing stated in terms of subtypes.)  -/
IsDiscrete.mono : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsDiscrete s → t ⊆ s → IsDiscrete t
-- Init.Data.Option.Lemmas
Option.bind_eq_none' : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β},
  o.bind f = none ↔ ∀ (b : β) (a : α), o = some a → f a ≠ some b
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.freeMonoidCongr_of : ∀ {α : Type u_6} {β : Type u_7} (e : α ≃ β) (a : α),
  (FreeMonoid.freeMonoidCongr e) (FreeMonoid.of a) = FreeMonoid.of (e a)
-- Mathlib.Data.QPF.Multivariate.Constructions.Comp
/-- Composition of an `n`-ary functor with `n` `m`-ary
functors gives us one `m`-ary functor  -/
MvQPF.Comp : {n m : ℕ} → (TypeVec.{u} n → Type u_1) → (Fin2 n → TypeVec.{u} m → Type u) → TypeVec.{u} m → Type u_1
-- Init.Data.String.Lemmas.Modify
String.toList_map : ∀ {f : Char → Char} {s : String}, (String.map f s).toList = List.map f s.toList
-- Lean.Attributes
Lean.Attribute.Builtin.getPrio : Lean.Syntax → Lean.AttrM ℕ
-- Mathlib.Algebra.Group.TypeTags.Hom
/-- Reinterpret `α →+ β` as `Multiplicative α →* Multiplicative β`.  -/
AddMonoidHom.toMultiplicative : {α : Type u_3} →
  {β : Type u_4} →
    [inst : AddZeroClass α] → [inst_1 : AddZeroClass β] → (α →+ β) ≃ (Multiplicative α →* Multiplicative β)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.unit_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G] {x x' y y' : C}
  (f : x ⟶ x') (g : y ⟶ y'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (G.map g))
      ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x', y')) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
      ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [inst_5 : CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)]
  {j : J} {k : K},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).obj k) j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimit.ι
          ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).comp CategoryTheory.Limits.colim)
          k)
        (CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim G).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).obj j) k)
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) j)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.mk : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} →
        (toFunctor : CategoryTheory.Functor 𝒳.obj 𝒴.obj) →
          autoParam (toFunctor.comp 𝒴.p = 𝒳.p) CategoryTheory.BasedFunctor.w._autoParam →
            CategoryTheory.BasedFunctor 𝒳 𝒴
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.dvd_of_squarefree_of_mul_dvd_mul_left : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {x y d : R} [DecompositionMonoid R],
  Squarefree y → d * d ∣ x * y → d ∣ x
-- Mathlib.Algebra.CharP.Defs
ExpChar.congr : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] {p : ℕ} (q : ℕ) [hq : ExpChar R q], q = p → ExpChar R p
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {v : β}, Std.DTreeMap.Const.get? t k = some v ↔ ∃ k', cmp k k' = Ordering.eq ∧ (k', v) ∈ Std.DTreeMap.Const.toList t
-- Mathlib.Logic.Relation
Relation.map_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → β → Prop} {f : α → γ} {g : β → δ} {c : γ}
  {d : δ}, Relation.Map r f g c d ↔ ∃ a b, r a b ∧ f a = c ∧ g b = d
-- Mathlib.Data.Vector.Basic
List.Vector.traverse_def : ∀ {n : ℕ} {F : Type u → Type u} [inst : Applicative F] {α β : Type u} (f : α → F β) (x : α) (xs : List.Vector α n),
  List.Vector.traverse f (x ::ᵥ xs) = List.Vector.cons <$> f x <*> List.Vector.traverse f xs
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (K L : CategoryTheory.Functor C D) (X : C) (f : L ⟶ L)
  (x :
    CategoryTheory.MonoidalCategoryStruct.tensorObj ((K.functorHom L).obj X)
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Type (max (max u v) v')))),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          ((K.homObjFunctor L).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))
          ((CategoryTheory.Functor.natTransEquiv.symm f).app X)))
      x =
    (x.1, CategoryTheory.Functor.HomObj.ofNatTrans f)
-- Mathlib.Order.Cover
/-- **Alias** of the forward direction of `covBy_iff_lt_iff_le_right`. -/
CovBy.lt_iff_le_right : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α}, y ⋖ x → ∀ {z : α}, y < z ↔ x ≤ z
-- Batteries.Data.String.Lemmas
String.utf8Len_le_of_infix : ∀ {cs₁ cs₂ : List Char}, cs₁ <:+: cs₂ → String.utf8Len cs₁ ≤ String.utf8Len cs₂
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.of.eq_1 : ∀ (G : Type u) [inst : AddGroup G] [inst_1 : Finite G],
  FiniteAddGrp.of G = { toAddGrp := AddGrpCat.of G, isFinite := inst_1 }
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.map_map_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)} (α : F₁ ⟶ F₂)
  {t₁ t₂ : F₁.Elements} (k : t₁ ⟶ t₂), ↑((CategoryTheory.CategoryOfElements.map α).map k) = ↑k
-- Mathlib.Algebra.Group.Prod
MonoidHom.inr_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] (y : N), (MonoidHom.inr M N) y = (1, y)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ringEq.inj : ∀ {c : Lean.Meta.Grind.Arith.Linear.RingEqCnstr} {lhs : Lean.Meta.Grind.Arith.Linear.LinExpr}
  {c_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstr} {lhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ringEq c lhs =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ringEq c_1 lhs_1 →
    c = c_1 ∧ lhs = lhs_1
-- Std.Data.HashMap.Lemmas
Std.HashMap.unitOfList_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {hd : α} {tl : List α},
  Std.HashMap.unitOfList (hd :: tl) = (∅.insertIfNew hd ()).insertManyIfNewUnit tl
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.minEntry_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → ∀ (h : t₁.Equiv t₂) {he : t₁.isEmpty = false}, t₁.minEntry he = t₂.minEntry ⋯
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] [inst : TopologicalSpace β] {m₀ : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {s : ι → Set α},
  (∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ.restrict (s i))) →
    MeasureTheory.AEStronglyMeasurable f (μ.restrict (⋃ i, s i))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {a : α}, t.getKey! a = (t.getKey? a).get!
-- Batteries.Data.List.Lemmas
List.max!.eq_1 : ∀ {α : Type u_1} [inst : Inhabited α] [inst_1 : Max α] (xs : List α),
  xs.max! =
    match xs.max? with
    | none => panicWithPosWithDecl "Batteries.Data.List.Basic" "List.max!" 20 12 "List.max! called on empty list"
    | some x => x
-- Mathlib.RingTheory.FractionalIdeal.Operations
IsLocalization.IsInteger.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (a : S),
  IsLocalization.IsInteger R a = (a ∈ (algebraMap R S).rangeS)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.equalizerSubobject_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobjectIso f g).hom
      (CategoryTheory.Limits.equalizer.ι f g) =
    (CategoryTheory.Limits.equalizerSubobject f g).arrow
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_ne_coe : ∀ {p q : NNReal}, ↑p ≠ ↑q ↔ p ≠ q
-- Mathlib.LinearAlgebra.Basis.Fin
/-- The basis of `R × R` given by the two vectors `(1, 0)` and `(0, 1)`.  -/
Module.Basis.finTwoProd : (R : Type u_7) → [inst : Semiring R] → Module.Basis (Fin 2) R (R × R)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.integral_tendsto_of_countably_generated : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → E},
      MeasureTheory.Integrable f μ → Filter.Tendsto (fun i => ∫ (x : α) in φ i, f x ∂μ) l (nhds (∫ (x : α), f x ∂μ))
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNormEssSup_indicator_const_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] (s : Set α) (c : ε), MeasureTheory.eLpNormEssSup (s.indicator fun x => c) μ ≤ ‖c‖ₑ
-- Mathlib.Order.ScottContinuity
ScottContinuous.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {g : β → γ}, ScottContinuous f → ScottContinuous g → ScottContinuous (g ∘ f)
-- Lean.Meta.Tactic.Simp.Types
Lean.TransformStep.toStep : Lean.TransformStep → Lean.Meta.Simp.Step
-- Lean.Parser.Extra
Lean.Parser.many1.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Convex.Deriv
/-- If `f` is convex on `S` and differentiable at all points of `S`, then its derivative is monotone
on `S`.  -/
ConvexOn.monotoneOn_deriv : ∀ {S : Set ℝ} {f : ℝ → ℝ}, ConvexOn ℝ S f → (∀ x ∈ S, DifferentiableAt ℝ f x) → MonotoneOn (deriv f) S
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {v : β k}, t.isEmpty = true → (t.insertIfNew k v).minKey! = k
-- Mathlib.FieldTheory.Finite.Basic
/-- In a finite field of odd characteristic, not every element is a square.  -/
FiniteField.exists_nonsquare : ∀ {F : Type u_3} [inst : Field F] [Finite F], ringChar F ≠ 2 → ∃ a, ¬IsSquare a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R),
  ((CategoryTheory.StructuredArrow.map₂ α β).obj X).right = F.obj X.right
-- Aesop.Tree.Data
Aesop.Goal.setMVars : Aesop.UnorderedArraySet Lean.MVarId → Aesop.Goal → Aesop.Goal
-- Mathlib.Order.Interval.Basic
/-- Recursor for `Interval` using the preferred forms `⊥` and `↑a`.  -/
Interval.recBotCoe : {α : Type u_1} →
  [inst : LE α] → {C : Interval α → Sort u_6} → C ⊥ → ((a : NonemptyInterval α) → C ↑a) → (n : Interval α) → C n
-- Mathlib.Data.Fintype.Basic
Fin.univ_def : ∀ (n : ℕ), Finset.univ = { val := ↑(List.finRange n), nodup := ⋯ }
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isIntTangent_self_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [Nontrivial V] {s : EuclideanGeometry.Sphere P}, s.IsIntTangent s ↔ 0 ≤ s.radius
-- Lean.Meta.Tactic.Grind.Types
/-- A `grind` goal, combining shared state with a specific metavariable.

See `GoalState` for details on why the state is factored out.
**Note**: The `Goal` internal representation is just a pair `GoalState` and `MVarId`.
 -/
Lean.Meta.Grind.Goal : Type
-- Lean.Meta.WHNF
Lean.Meta.reduceBoolNativeUnsafe : Lean.Name → Lean.MetaM Bool
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.compare_get?_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, Option.all (fun x => decide (cmp x k = Ordering.eq)) (t.get? k) = true
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.div_tendsto_atBot_zero_iff_degree_lt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Q ≠ 0 →
    (Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atBot (nhds 0) ↔ P.degree < Q.degree)
-- Mathlib.CategoryTheory.CopyDiscardCategory.Deterministic
/-- A morphism is deterministic if it preserves the comonoid structure.

In probabilistic contexts, these are morphisms without randomness.  -/
CategoryTheory.Deterministic : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.CopyDiscardCategory C] → {X Y : C} → (X ⟶ Y) → Prop
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.bullet.go : List Lean.Doc.Parser.UnorderedListType → Lean.Parser.ParserFn
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.le_eLpNorm_of_bddBelow : ∀ {α : Type u_1} {F : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F],
  p ≠ 0 →
    p ≠ ⊤ →
      ∀ {f : α → F} (C : NNReal) {s : Set α},
        MeasurableSet s → (∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊) → C • μ s ^ (1 / p.toReal) ≤ MeasureTheory.eLpNorm f p μ
-- Mathlib.Data.FunLike.Group
FunLike.addCommSemigroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : AddCommSemigroup β]
  [inst_3 : IsAddApply F α β], FunLike.addCommSemigroup = Function.Injective.addCommSemigroup (fun f => ⇑f) ⋯ ⋯
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
OrderIso.map_ciSup_set_of_directedOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompletePartialOrderSup α]
  [inst_1 : ConditionallyCompletePartialOrderSup β] (e : α ≃o β) {s : Set γ} {f : γ → α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) (f '' s) → BddAbove (f '' s) → s.Nonempty → e (⨆ i, f ↑i) = ⨆ i, e (f ↑i)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 2-boundaries `B₂(G, A)` of `A : Rep k G`, defined as the image of the map
`(G³ →₀ A) → (G² →₀ A)` defined by
`a·(g₁, g₂, g₃) ↦ ρ_A(g₁⁻¹)(a)·(g₂, g₃) - a·(g₁g₂, g₃) + a·(g₁, g₂g₃) - a·(g₁, g₂)`.  -/
groupHomology.boundaries₂ : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → Submodule k (G × G →₀ ↑A)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_characteristic : ∀ {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G) [S.Characteristic] (n : ℕ),
  (S.lowerCentralSeries n).Characteristic
-- Mathlib.Analysis.Asymptotics.TVS
/-- Eta-expanded form of `Asymptotics.IsLittleOTVS.add` -/
Asymptotics.IsLittleOTVS.fun_add : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {f₁ f₂ : α → E} {g : α → F}
  {l : Filter α}, f₁ =o[𝕜; l] g → f₂ =o[𝕜; l] g → (fun i => f₁ i + f₂ i) =o[𝕜; l] g
-- Mathlib.GroupTheory.Index
Subgroup.exists_pow_mem_of_index_ne_zero : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index ≠ 0 → ∀ (a : G), ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H
-- Mathlib.SetTheory.Cardinal.Finite
Nat.instNeZeroCardOfNonemptyOfFinite : ∀ {α : Type u_1} [Nonempty α] [Finite α], NeZero (Nat.card α)
-- Mathlib.GroupTheory.NoncommPiCoprod
AddMonoidHom.independent_range_of_coprime_order : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → Type u_3} [inst_1 : (i : ι) → AddGroup (H i)]
  (ϕ : (i : ι) → H i →+ G),
  (Pairwise fun i j => ∀ (x : H i) (y : H j), AddCommute ((ϕ i) x) ((ϕ j) y)) →
    ∀ [Finite ι] [inst_3 : (i : ι) → Fintype (H i)],
      (Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))) → iSupIndep fun i => (ϕ i).range
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- **Alias** of `LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete`. -/
LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Nontrivial G] {g : G},
  ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃+o ℤ)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.Mono S.v₀₁.τ₂
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_id : ∀ {𝕜 : Type u_1} {E : Type u_2} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G],
  ContinuousLinearMap.lTensor G (ContinuousLinearMap.id 𝕜 E) = ContinuousLinearMap.id 𝕜 (TensorProduct 𝕜 G E)
-- Mathlib.Data.Nat.Prime.Defs
Nat.fact_prime_two : Fact (Nat.Prime 2)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.mulR.inj : ∀ {a : Nat.Internal.Linear.Expr} {k : ℕ} {a_1 : Nat.Internal.Linear.Expr} {k_1 : ℕ},
  a.mulR k = a_1.mulR k_1 → a = a_1 ∧ k = k_1
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.isPrimitive_one_level_one : ∀ {R : Type u_1} [inst : CommMonoidWithZero R], DirichletCharacter.IsPrimitive 1