mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.comp_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A A' A'' : G.Coalgebra}
  (f : A ⟶ A') (g : A' ⟶ A''), (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
-- Mathlib.Topology.Algebra.Indicator
Continuous.mulIndicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  [inst_2 : One β], (∀ a ∈ frontier s, f a = 1) → Continuous f → Continuous (s.mulIndicator f)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs.0.BirdDet.Spec.birdDet.match_1.eq_1 : ∀ {R : Type u_1} (motive : (n : ℕ) → Matrix (Fin n) (Fin n) R → Sort u_2) (A : Matrix (Fin 0) (Fin 0) R)
  (h_1 : (A : Matrix (Fin 0) (Fin 0) R) → motive 0 A)
  (h_2 : (k : ℕ) → (A : Matrix (Fin (k + 1)) (Fin (k + 1)) R) → motive k.succ A),
  (match 0, A with
    | 0, A => h_1 A
    | k.succ, A => h_2 k A) =
    h_1 A
-- Mathlib.Algebra.DirectSum.Module
DirectSum.apply_eq_component : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] (f : DirectSum ι fun i => M i) (i : ι), f i = (DirectSum.component R ι M i) f
-- Mathlib.Algebra.Order.Group.PosPart
negPart_anti : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α], Antitone negPart
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.isLowerSet_orderDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α], Topology.IsLowerSet αᵒᵈ ↔ Topology.IsUpperSet α
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.image_symm_image : ∀ {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₂) (s : Set P₂), ⇑e '' ⇑e.symm '' s = s
-- Mathlib.RingTheory.LocalProperties.Projective
instProjectiveLocalizationLocalizedModule : ∀ {R : Type u_1} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submonoid R)
  [Module.Projective R M], Module.Projective (Localization S) (LocalizedModule S M)
-- Init.Data.UInt.Lemmas
UInt8.ofFin_mod : ∀ (a b : Fin UInt8.size), UInt8.ofFin (a % b) = UInt8.ofFin a % UInt8.ofFin b
-- Mathlib.Analysis.Analytic.RadiusLiminf
/-- The radius of a formal multilinear series is equal to
$\liminf_{n\to\infty} \frac{1}{\sqrt[n]{‖p n‖}}$. The actual statement uses `ℝ≥0` and some
coercions.  -/
FormalMultilinearSeries.radius_eq_liminf : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F), p.radius = Filter.liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) Filter.atTop
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.sup_disjoint' : ∀ {G : Type w} [inst : TopologicalSpace G] (self : MeasureTheory.Content G) (K₁ K₂ : TopologicalSpace.Compacts G),
  Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → self.toFun (K₁ ⊔ K₂) = self.toFun K₁ + self.toFun K₂
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If `p₃` bisects the angle `∡ p₁ p₂ p₄`, and `p₃` and `p₄` lie on the same side of the line
`p₁ p₂`, then the unoriented angle `∠ p₁ p₂ p₃` is half `∠ p₁ p₂ p₄`.  -/
EuclideanGeometry.angle_eq_angle_div_two_of_oangle_eq_of_sSameSide : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ : P},
  p₁ ≠ p₂ →
    EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₃ p₂ p₄ →
      line[ℝ, p₁, p₂].SSameSide p₃ p₄ → EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₂ p₄ / 2
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
/-- The cohomology class of a 1-cocycle.  -/
CategoryTheory.PresheafOfGroups.OneCocycle.class : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : CategoryTheory.Functor Cᵒᵖ GrpCat} →
      {I : Type w'} →
        {U : I → C} → CategoryTheory.PresheafOfGroups.OneCocycle G U → CategoryTheory.PresheafOfGroups.H1 G U
-- Std.Time.Format
/-- The AscTime format, which follows the pattern `EEE MMM d HH:mm:ss uuuu`. This format
is often used in older systems for logging and time-stamping events.
 -/
Std.Time.Formats.ascTime : Std.Time.GenericFormat (Std.Time.Awareness.only Std.Time.TimeZone.GMT)
-- Mathlib.CategoryTheory.Join.Sum
CategoryTheory.Join.inrCompFromSum_inv_app : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (X : D),
  (CategoryTheory.Join.inrCompFromSum C D).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right X)
-- Mathlib.Order.Category.BddLat
BddLat.mk.inj : ∀ {toLat : Lat} {isBoundedOrder : BoundedOrder ↑toLat} {toLat_1 : Lat} {isBoundedOrder_1 : BoundedOrder ↑toLat_1},
  { toLat := toLat, isBoundedOrder := isBoundedOrder } = { toLat := toLat_1, isBoundedOrder := isBoundedOrder_1 } →
    toLat = toLat_1 ∧ isBoundedOrder ≍ isBoundedOrder_1
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization
CategoryTheory.Limits.instAB5IndOfHasFiniteLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C],
  CategoryTheory.AB5 (CategoryTheory.Ind C)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.map_genWeightSpace_eq : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] {M₂ : Type u_5} [inst_8 : AddCommGroup M₂] [inst_9 : Module R M₂]
  [inst_10 : LieRingModule L M₂] [inst_11 : LieModule R L M₂] {χ : L → R} (e : M ≃ₗ⁅R,L⁆ M₂),
  LieSubmodule.map e.toLieModuleHom (LieModule.genWeightSpace M χ) = LieModule.genWeightSpace M₂ χ
-- Mathlib.Order.Heyting.Basic
/-- `(q → r) → (p → q) → q → r`  -/
himp_le_himp_himp_himp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.map : {α : Type u_1} → {β : Type u_2} → (α → β) → Lean.Widget.TaggedText α → Lean.Widget.TaggedText β
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_zero : Int.negOnePow 0 = 1
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, if `e₁` and `e₂` are compatible with the
unit of the adjunction `adj`, then we get a formula for `e₂.inv` in terms of `e₁`.
 -/
CategoryTheory.Adjunction.CommShift.compatibilityUnit_right : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] {a : A}
  (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (e₂ : (CategoryTheory.shiftFunctor D a).comp G ≅ G.comp (CategoryTheory.shiftFunctor C a)),
  CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj e₁ e₂ →
    ∀ (Y : D),
      e₂.inv.app Y =
        CategoryTheory.CategoryStruct.comp (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj (G.obj Y)))
          (CategoryTheory.CategoryStruct.comp (G.map (e₁.hom.app (G.obj Y)))
            (G.map ((CategoryTheory.shiftFunctor D a).map (adj.counit.app Y))))
-- Mathlib.NumberTheory.FLT.Basic
dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT : ∀ {n : ℕ} {p : ℤ}, Prime p → ∀ {a b c : ℤ}, p ∣ a → p ∣ b → a ^ n + b ^ n + c ^ n = 0 → p ∣ c
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.toLocalizationMap.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S],
  IsLocalization.toLocalizationMap M S = IsLocalization.toLocalizationMap M S
-- Mathlib.Computability.Encoding
/-- An encoding function of `ℕ` in `Bool`.  -/
Computability.encodeNat : ℕ → List Bool
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ord_le_ord_mul : ∀ {R : Type u_1} [inst : CommRing R] (a x : R), Ring.ord R x ≤ Ring.ord R (a * x)
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
ModularForm.discriminant_mul_discriminantEquiv : ∀ {k : ℤ} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k),
  ModularForm.discriminant * ⇑(CuspForm.discriminantEquiv f) = ⇑f
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.bot_mem_propQCPrecoverage : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (X : AlgebraicGeometry.Scheme) [IsEmpty ↥X],
  ⊥ ∈ (AlgebraicGeometry.Scheme.propQCPrecoverage P).coverings X
-- Std.Sat.AIG.RelabelNat
/-- The next number to use for identifying an atom.
 -/
Std.Sat.AIG.RelabelNat.State.max : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      {decls : Array (Std.Sat.AIG.Decl α)} → {idx : ℕ} → Std.Sat.AIG.RelabelNat.State α decls idx → ℕ
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.below_of_lt : ∀ {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}}, e.repr < b → (e.oadd n a).NF → (e.oadd n a).NFBelow b
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.one_eq_ofENat : ∀ {m : ℕ∞}, 1 = ↑m ↔ m = 1
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.exfalso'.inj : ∀ {p p_1 : Mathlib.Tactic.ITauto.Proof}, p.exfalso' = p_1.exfalso' → p = p_1
-- Std.Time.Format.Modifier
/-- Nanosecond precision (up to 9 digits)
 -/
Std.Time.Fraction.nano : Std.Time.Fraction
-- Mathlib.Dynamics.Minimal
isMinimal_iff_isClosed_smul_invariant : ∀ (M : Type u_1) {α : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α],
  MulAction.IsMinimal M α ↔ ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = Set.univ
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.eval_add : ∀ (b : Ordinal.{u_1}) {f₁ f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}},
  (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) →
    Ordinal.CNF.eval b (f₁ + f₂) = Ordinal.CNF.eval b f₁ + Ordinal.CNF.eval b f₂
-- Mathlib.Data.Num.Bitwise
PosNum.shiftr_eq_shiftRight : ∀ (p : PosNum) (n : ℕ), p.shiftr n = p >>> n
-- Mathlib.Data.W.Cardinal
WType.cardinalMk_eq_sum : ∀ {α : Type u} {β : α → Type u}, Cardinal.mk (WType β) = Cardinal.sum fun a => Cardinal.mk (WType β) ^ Cardinal.mk (β a)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getDoLetRecVars : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.mk.injEq : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (toTheory : (L.withConstants α).Theory)
  (subset' : (L.lhomWithConstants α).onTheory T ⊆ toTheory) (isMaximal' : toTheory.IsMaximal)
  (toTheory_1 : (L.withConstants α).Theory) (subset'_1 : (L.lhomWithConstants α).onTheory T ⊆ toTheory_1)
  (isMaximal'_1 : toTheory_1.IsMaximal),
  ({ toTheory := toTheory, subset' := subset', isMaximal' := isMaximal' } =
      { toTheory := toTheory_1, subset' := subset'_1, isMaximal' := isMaximal'_1 }) =
    (toTheory = toTheory_1)
-- Mathlib.GroupTheory.Congruence.Defs
Con.hasMul.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (c : Con M), c.hasMul = { mul := Quotient.map₂ (fun x1 x2 => x1 * x2) ⋯ }
-- Mathlib.Order.Defs.Unbundled
transitive_of_trans : ∀ {α : Sort u_1} (r : α → α → Prop) [IsTrans α r], Transitive r
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmooth.out : ∀ {R : Type u} {S : Type v} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  [self : Algebra.IsStandardSmooth R S],
  ∃ ι σ, ∃ (x : Finite σ), Finite ι ∧ Nonempty (Algebra.SubmersivePresentation R S ι σ)
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_ofReal_re : ∀ (x : ℝ), (Complex.exp ↑x).re = Real.exp x
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.nonempty_right : ∀ {G : Type u_1} [inst : Group G] {S T : Set G}, Subgroup.IsComplement S T → T.Nonempty
-- Mathlib.Analysis.BoxIntegral.Basic
/-- The integral sum of `f : ℝⁿ → E` over a tagged prepartition `π` w.r.t. box-additive volume `vol`
with codomain `E →L[ℝ] F` is the sum of `vol J (f (π.tag J))` over all boxes of `π`.  -/
BoxIntegral.integralSum : {ι : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              {I : BoxIntegral.Box ι} →
                ((ι → ℝ) → E) → BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤ → BoxIntegral.TaggedPrepartition I → F
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.instReprDaylightSavingRule.repr : Std.Time.TimeZone.DaylightSavingRule → ℕ → Std.Format
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.leftUnitor_hom_right_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : C),
  φ.leftUnitor.hom.right.app X = CategoryTheory.CategoryStruct.id (φ.right.obj X)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instDiv.eq_1 : ∀ {α : Type u_1} [inst : Div α], Lex.instDiv = inst
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.expandNatValuePattern : Lean.Meta.Match.Problem → Lean.MetaM Lean.Meta.Match.Problem
-- Mathlib.Algebra.Free
FreeAddMagma.add_eq : ∀ {α : Type u} (x y : FreeAddMagma α), x.add y = x + y
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- In the presence of the strict Segal condition, a path of length `m` can be
"composed" by taking the diagonal edge of the resulting `m`-simplex.  -/
SSet.Truncated.StrictSegal.spineToDiagonal : {n : ℕ} →
  {X : SSet.Truncated (n + 1)} →
    X.StrictSegal →
      (m : ℕ) → autoParam (m ≤ n + 1) _auto_41✝ → X.Path m → X.obj (Opposite.op { obj := { len := 1 }, property := ⋯ })
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.limitAddGroup.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections],
  AddGrpCat.limitAddGroup F =
    { add := AddGrpCat.limitAddGroup._aux_1 F, add_assoc := ⋯, zero := AddGrpCat.limitAddGroup._aux_4 F, zero_add := ⋯,
      add_zero := ⋯, nsmul := AddGrpCat.limitAddGroup._aux_8 F, nsmul_zero := ⋯, nsmul_succ := ⋯,
      neg := AddGrpCat.limitAddGroup._aux_12 F, sub := AddGrpCat.limitAddGroup._aux_14 F,
      zsmul := AddGrpCat.limitAddGroup._aux_16 F, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯,
      zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_val_Ici : ∀ {n : ℕ} (a : Fin n), Finset.image Fin.val (Finset.Ici a) = Finset.Ico (↑a) n
-- Init.MetaTypes
/-- Configuration for which occurrences that match an expression should be rewritten.  -/
Lean.Meta.Occurrences : Type
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.lt_slope_of_hasDerivAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivAt f f' y → f' < slope f x y
-- Lean.DocString.Syntax
Lean.Doc.Syntax.arg_val.quot : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termF₂ : Lean.ParserDescr
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticOn.aeval_polynomial : ∀ {𝕜 : Type u_1} {E : Type u_2} {A : Type u_3} {B : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : CommSemiring A] {s : Set E}
  [inst_4 : NormedRing B] [inst_5 : NormedAlgebra 𝕜 B] [inst_6 : Algebra A B] {f : E → B},
  AnalyticOn 𝕜 f s → ∀ (p : Polynomial A), AnalyticOn 𝕜 (fun x => (Polynomial.aeval (f x)) p) s
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `s : Cocone F` whiskered by an equivalence `e` is a colimit cocone, so is `s`.  -/
CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {s : CategoryTheory.Limits.Cocone F} →
                (e : K ≌ J) →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cocone.whisker e.functor s) →
                    CategoryTheory.Limits.IsColimit s
-- Mathlib.Order.Bounds.Basic
/-- If `a` is the greatest element of a set `s`, then subtype `s` is an order with top element.  -/
IsGreatest.orderTop : {α : Type u_1} → [inst : Preorder α] → {s : Set α} → {a : α} → IsGreatest s a → OrderTop ↑s
-- Aesop.Frontend.Extension.Init
Aesop.instInhabitedDeclaredRuleSets.default : Aesop.DeclaredRuleSets
-- Mathlib.NumberTheory.LSeries.Convolution
toArithmeticFunction.eq_1 : ∀ {R : Type u_1} [inst : Zero R] (f : ℕ → R),
  toArithmeticFunction f = { toFun := fun n => if n = 0 then 0 else f n, map_zero' := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.toInt_zero_append : ∀ {n m : ℕ} {x : BitVec n}, (0#m ++ x).toInt = if m = 0 then x.toInt else ↑x.toNat
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.ShortExact.moduleCat_injective_f : ∀ {R : Type u} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.ShortExact → Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom S.f)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns a proof that `a = True`.
It assumes `a` and `True` are in the same equivalence class.
 -/
Lean.Meta.Grind.mkEqTrueProof : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.sin_eq_neg_one_iff : ∀ {x : ℂ}, Complex.sin x = -1 ↔ ∃ k, -(↑Real.pi / 2) + ↑k * (2 * ↑Real.pi) = x
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.coe_restrictScalarsIsometry : ∀ (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_6) [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ] (𝕜' : Type u_9)
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜' 𝕜] [inst_7 : NormedSpace 𝕜' E]
  [inst_8 : IsScalarTower 𝕜' 𝕜 E] [inst_9 : NormedSpace 𝕜' Fₗ] [inst_10 : IsScalarTower 𝕜' 𝕜 Fₗ] {𝕜'' : Type u_10}
  [inst_11 : Ring 𝕜''] [inst_12 : Module 𝕜'' Fₗ] [inst_13 : ContinuousConstSMul 𝕜'' Fₗ]
  [inst_14 : SMulCommClass 𝕜 𝕜'' Fₗ] [inst_15 : SMulCommClass 𝕜' 𝕜'' Fₗ],
  ⇑(ContinuousLinearMap.restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'') = ContinuousLinearMap.restrictScalars 𝕜'
-- Mathlib.Algebra.Polynomial.Roots
/-- **Alias** of `Polynomial.finite_setOfPred_isRoot`. -/
Polynomial.finite_setOf_isRoot : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {p : Polynomial R}, p ≠ 0 → {x | p.IsRoot x}.Finite
-- Batteries.Data.List.Lemmas
List.mem_findIdxs_iff_pos_getElem : ∀ {i : ℕ} {α : Type u_1} {xs : List α} {p : α → Bool} (hi : i < xs.length), i ∈ List.findIdxs p xs ↔ p xs[i] = true
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.r_iff_oreEqv_r : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {x y : M × ↥S},
  (Localization.r S) x y ↔ (OreLocalization.oreEqv S M) x y
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_single : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (h : J ≤ I), (BoxIntegral.Prepartition.single I J h).iUnion = ↑J
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_le_add_iff_left : ∀ {a b c : ENNReal}, a ≠ ⊤ → (a + b ≤ a + c ↔ b ≤ c)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.foldr_eq_foldr_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {δ : Type w} {f : α → δ → δ} {init : δ},
  Std.TreeSet.foldr f init t = List.foldr f init t.toList
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- A topological space `X` is compactly generated if its topology is finer than (and thus equal to)
the compactly generated topology, i.e. it is coinduced by the continuous maps from compact
Hausdorff spaces to `X`.

This version includes an explicit universe parameter `u` which should always be specified. It is
intended for categorical purposes. See `CompactlyGeneratedSpace` for the version without this
parameter, intended for topological purposes.
 -/
UCompactlyGeneratedSpace : (X : Type v) → [t : TopologicalSpace X] → Prop
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_sup : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I J : Ideal R), ↑(I ⊔ J) = ↑I + ↑J
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.instMinOfLinearOrder.eq_1 : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : LinearOrder α],
  AddUnits.instMinOfLinearOrder = { min := fun a b => if a ≤ b then a else b }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S}
  (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S)
  {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.equalizer.ι f g)
          (CategoryTheory.Limits.pullback.fst s v))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.equalizer.ι
        (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
        (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst s v) h)
-- Mathlib.Combinatorics.Matroid.Basic
_private.Mathlib.Combinatorics.Matroid.Basic.0.Matroid.insert_subset_ground : ∀ {α : Type u_1} {e : α} {X : Set α} {M : Matroid α}, e ∈ M.E → X ⊆ M.E → insert e X ⊆ M.E
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mk_mul_mk : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Mul γ] [inst_3 : ContinuousMul γ] (f g : α → γ) (hf : MeasureTheory.AEStronglyMeasurable f μ)
  (hg : MeasureTheory.AEStronglyMeasurable g μ),
  MeasureTheory.AEEqFun.mk f hf * MeasureTheory.AEEqFun.mk g hg = MeasureTheory.AEEqFun.mk (f * g) ⋯
-- Mathlib.CategoryTheory.Filtered.FinallySmall
CategoryTheory.FinallySmall.instCategoryFilteredFinalModel : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFiltered C] →
      [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] →
        [inst_3 : CategoryTheory.FinallySmall C] →
          CategoryTheory.Category.{w, w} (CategoryTheory.FinallySmall.FilteredFinalModel C)
-- Mathlib.Data.Fintype.Defs
Fintype.decidableInjectiveFintype : {α : Type u_1} → {β : Type u_2} → [DecidableEq β] → [Fintype α] → DecidablePred Function.Injective