mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.instIsScalarTower : ∀ {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {T : Type u_7} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_6 : DistribSMul S M₂] [inst_7 : SMulCommClass R₂ S M₂]
  [inst_8 : DistribSMul T M₂] [inst_9 : SMulCommClass R₂ T M₂] [inst_10 : SMul S T] [IsScalarTower S T M₂],
  IsScalarTower S T (M →ₛₗ[σ₁₂] M₂)
-- Mathlib.RingTheory.IsAdjoinRoot
/-- If `α` is primitive in `E/f`, then `E` is given by adjoining a root of `minpoly F α`.  -/
IsAdjoinRootMonic.mkOfPrimitiveElement : {F : Type u_1} →
  {E : Type u_2} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] → {α : E} → IsIntegral F α → F⟮α⟯ = ⊤ → IsAdjoinRootMonic E (minpoly F α)
-- Mathlib.Algebra.Module.LinearMap.Rat
/-- Reinterpret an additive homomorphism as a `ℚ`-linear map.  -/
AddMonoidHom.toRatLinearMap : {M : Type u_1} →
  {M₂ : Type u_2} →
    [inst : AddCommGroup M] →
      [inst_1 : Module ℚ M] → [inst_2 : AddCommGroup M₂] → [inst_3 : Module ℚ M₂] → (M →+ M₂) → M →ₗ[ℚ] M₂
-- Mathlib.Algebra.RingQuot
RingQuot.mk.inj : ∀ {R : Type uR} {inst : Semiring R} {r : R → R → Prop} {toQuot toQuot_1 : Quot (RingQuot.Rel r)},
  { toQuot := toQuot } = { toQuot := toQuot_1 } → toQuot = toQuot_1
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Call.expr : Lean.Meta.FunInd.Call → Lean.Expr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLED.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β) (fallback : (a : α) × β a),
  Std.DTreeMap.Internal.Impl.getEntryLED k t fallback = (Std.DTreeMap.Internal.Impl.getEntryLE? k t).getD fallback
-- Mathlib.Algebra.Category.Grp.IsFinite
AddCommGrpCat.prop_isFinite_iff : ∀ (M : AddCommGrpCat), M.isFinite ↔ Finite ↑M
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.DStep : Type
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
/-- The `S`-span of roots.  -/
RootPairing.rootSpan : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  RootPairing ι R M N → (S : Type u_6) → [inst : CommRing S] → [inst_5 : Module S M] → Submodule S M
-- Mathlib.Control.Traversable.Instances
Option.traverse_eq_map_id : ∀ {α β : Type u_1} (f : α → β) (x : Option α), Option.traverse (pure ∘ f) x = pure (f <$> x)
-- Mathlib.Data.ENNReal.Inv
ENNReal.ofReal_inv_of_pos : ∀ {x : ℝ}, 0 < x → ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_le_minKey?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k km kme : α}
  (hkme : (t.erase k).minKey? = some kme), t.minKey?.get ⋯ = km → (cmp km kme).isLE = true
-- Mathlib.Data.PFun
PFun.core_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β), f.core s = f.preimage s ∪ f.Domᶜ
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sheaf.toPushforwardOverPullback_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasPullbacks C]
  (F : CategoryTheory.Sheaf J A) {X Y : C} (f : X ⟶ Y) (U : (CategoryTheory.Over Y)ᵒᵖ),
  (F.toPushforwardOverPullback f).hom.app U = F.obj.map (CategoryTheory.Limits.pullback.fst (Opposite.unop U).hom f).op
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, k ∉ t₂ → (t₁ \ t₂).get! k = t₁.get! k
-- Mathlib.Data.Nat.Bitwise
/-- An alternative for `bitwise_bit` which replaces the `f false false = false` assumption
with assumptions that neither `bit a m` nor `bit b n` are `0`
(albeit, phrased as the implications `m = 0 → a = true` and `n = 0 → b = true`)  -/
Nat.bitwise_bit' : ∀ {f : Bool → Bool → Bool} (a : Bool) (m : ℕ) (b : Bool) (n : ℕ),
  (m = 0 → a = true) →
    (n = 0 → b = true) → Nat.bitwise f (Nat.bit a m) (Nat.bit b n) = Nat.bit (f a b) (Nat.bitwise f m n)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintTextEdit.mk.sizeOf_spec : ∀ (range : Lean.Syntax.Range) (newText : String),
  sizeOf { range := range, newText := newText } = 1 + sizeOf range + sizeOf newText
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_alter_eq_self_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∈ m → (f (Std.ExtDHashMap.Const.get? m k)).isSome = true → (Std.ExtDHashMap.Const.alter m k f).size = m.size
-- Mathlib.Topology.Compactness.SigmaCompact
/-- In a topological space with sigma compact topology, if `f` is a function that sends each point
`x` of a closed set `s` to a neighborhood of `x` within `s`, then for some countable set `t ⊆ s`,
the neighborhoods `f x`, `x ∈ t`, cover the whole set `s`.  -/
countable_cover_nhdsWithin_of_sigmaCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [SigmaCompactSpace X] {f : X → Set X} {s : Set X},
  IsClosed s → (∀ x ∈ s, f x ∈ nhdsWithin x s) → ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (x, - x + y)` is measure-preserving.  -/
MeasureTheory.measurePreserving_prod_neg_add : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [ν.IsAddLeftInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1, -z.1 + z.2)) (μ.prod ν) (μ.prod ν)
-- Aesop.Tracing
Aesop.instInhabitedTraceOption.default : Aesop.TraceOption
-- Mathlib.Order.Cover
WCovBy.eq_or_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b c : α}, a ⩿ b → a ≤ c → c ≤ b → c = a ∨ c = b
-- Mathlib.Algebra.Ring.Int.Units
Int.units_ne_iff_eq_neg : ∀ {u v : ℤˣ}, u ≠ v ↔ u = -v
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.mul_subset_iff_right : ∀ {α : Type u_2} [inst : Mul α] {s t u : Set α}, s * t ⊆ u ↔ ∀ b ∈ t, MulOpposite.op b • s ⊆ u
-- Mathlib.Data.Set.SMulAntidiagonal
Set.smulAntidiagonal_mono_left : ∀ {G : Type u_1} {P : Type u_2} [inst : SMul G P] {s₁ s₂ : Set G} {t : Set P} {a : P},
  s₁ ⊆ s₂ → s₁.smulAntidiagonal t a ⊆ s₂.smulAntidiagonal t a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.dist : ∀ {α : Type u_1} {x : MeasurableSpace α} {β : Type u_5} [inst : PseudoMetricSpace β] {f g : α → β},
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun x => dist (f x) (g x)
-- Init.Data.String.PosRaw
String.Pos.Raw.lt_of_le_of_lt : ∀ {a b c : String.Pos.Raw}, a ≤ b → b < c → a < c
-- Std.Async.Signal
Std.Async.Signal.noConfusionType : Sort v✝ → Std.Async.Signal → Std.Async.Signal → Sort v✝
-- Init.Data.String.Defs
String.offset_startPos : ∀ {s : String}, s.startPos.offset = 0
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The `changeLevel` map is injective (except in the degenerate case `m = 0`).  -/
DirichletCharacter.changeLevel_injective : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n m : ℕ} [NeZero m] (hm : n ∣ m),
  Function.Injective ⇑(DirichletCharacter.changeLevel hm)
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.mulConst.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G), A.mulConst B = ↑(A * B).card / ↑A.card
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The additive equivalence between the type of additive units of
`M` and the additive submonoid whose elements are the additive units of `M`.  -/
AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid : {M : Type u_4} → [inst : AddMonoid M] → AddUnits M ≃+ ↥(IsAddUnit.addSubmonoid M)
-- Lean.Server.FileWorker.SemanticHighlighting
/-- `SyntaxNodeKind`s for which the syntax node and its children receive no semantic highlighting.
 -/
Lean.Server.FileWorker.noHighlightKinds : Array Lean.SyntaxNodeKind
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.lift_comp_reindex : ∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E]
  [inst_4 : Module R E] (e : ι ≃ ι₂) (φ : MultilinearMap R (fun i => s (e.symm i)) E),
  PiTensorProduct.lift φ ∘ₗ ↑(PiTensorProduct.reindex R s e) =
    PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e).symm φ)
-- Mathlib.Data.Finset.Image
Finset.image_union : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] {f : α → β} (s₁ s₂ : Finset α),
  Finset.image f (s₁ ∪ s₂) = Finset.image f s₁ ∪ Finset.image f s₂
-- Init.Data.Int.Order
Int.natAbs_mul_self : ∀ {a : ℤ}, ↑(a.natAbs * a.natAbs) = a * a
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.charType : Char → Lean.FuzzyMatching.CharType
-- Lean.Meta.Sym.Simp.SimpM
/-- Saves and restores both caches and funext. Used by dischargers.  -/
Lean.Meta.Sym.Simp.withoutModifyingCache : {α : Type} → Lean.Meta.Sym.Simp.SimpM α → Lean.Meta.Sym.Simp.SimpM α
-- Mathlib.CategoryTheory.Limits.Pi
/-- Given a family of cones over the `F ⋙ Pi.eval C i`, we can assemble these together as a `Cone F`.
 -/
CategoryTheory.pi.coneOfConeCompEval : {I : Type v₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type v₁} →
        [inst_1 : CategoryTheory.SmallCategory J] →
          {F : CategoryTheory.Functor J ((i : I) → C i)} →
            ((i : I) → CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Pi.eval C i))) → CategoryTheory.Limits.Cone F
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The Pythagorean theorem, for an orthogonal projection.  -/
Submodule.norm_sq_eq_add_norm_sq_projection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E) (S : Submodule 𝕜 E) [inst_3 : S.HasOrthogonalProjection],
  ‖x‖ ^ 2 = ‖S.orthogonalProjectionOnto x‖ ^ 2 + ‖Sᗮ.orthogonalProjectionOnto x‖ ^ 2
-- Mathlib.Order.Filter.Extr
/-- If `f` is monotone on `Ioc a b` and antitone on `Ico b c`, then the maximum of `f` on
`Ioo a c` is attained at `b`.  -/
isMaxOn_Ioo_of_mono_anti : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b c : α} {f : α → β},
  MonotoneOn f (Set.Ioc a b) → AntitoneOn f (Set.Ico b c) → IsMaxOn f (Set.Ioo a c) b
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {f g : M → E'} {s : Set M}, MDiff[s] f → MDiff[s] g → MDiff[s] (f + g)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.structuralIsoOfExpr_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g h : C} (η : f ⟶ g) (η' : f ≅ g),
  η'.hom = η → ∀ (θ : g ⟶ h) (θ' : g ≅ h), θ'.hom = θ → (η' ≪≫ θ').hom = CategoryTheory.CategoryStruct.comp η θ
-- Mathlib.Analysis.Convex.Strict
Directed.strictConvex_iUnion : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : SMul 𝕜 E] {ι : Sort u_6} {s : ι → Set E},
  Directed (fun x1 x2 => x1 ⊆ x2) s → (∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)) → StrictConvex 𝕜 (⋃ i, s i)
-- Mathlib.Analysis.Convex.Between
wbtw_const_vsub_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (p : P), Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Wbtw R x y z
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instAdd : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Add (SlashInvariantForm Γ k)
-- Lean.Server.FileWorker.Utils
/-- Whether the next `publishDiagnostics` call should be incremental.  -/
Lean.Server.FileWorker.DiagnosticsState.isIncremental : Lean.Server.FileWorker.DiagnosticsState → Bool
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_iffₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  LinearIndependent R v ↔
    ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
-- Mathlib.Order.LiminfLimsup
Filter.le_limsSup_of_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f : Filter α} {a : α},
  autoParam (Filter.IsBounded (fun x1 x2 => x1 ≤ x2) f) Filter.le_limsSup_of_le._auto_1 →
    (∀ (b : α), (∀ᶠ (n : α) in f, n ≤ b) → a ≤ b) → a ≤ f.limsSup
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_range_update_add_smul : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_8}
  [inst_3 : DecidableEq ι] {i j : ι},
  i ≠ j →
    ∀ (v : ι → M) (r : R),
      Submodule.span R (Set.range (Function.update v j (v j + r • v i))) = Submodule.span R (Set.range v)
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigOWith_neg_left`. -/
Asymptotics.IsBigOWith.of_neg_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ} {g : α → F}
  {f' : α → E'} {l : Filter α}, Asymptotics.IsBigOWith c l (fun x => -f' x) g → Asymptotics.IsBigOWith c l f' g
-- Lean.Expr
/-- If `e` is an application `f a_1 ... a_n` annotate `f`, `a_1` ... `a_n` with `pp.explicit := false`,
and annotate `e` with `pp.explicit := true`.
 -/
Lean.Expr.setAppPPExplicit : Lean.Expr → Lean.Expr
-- Init.Data.Range.Polymorphic.RangeIterator
Std.IterM.Step.toPure.eq_1 : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.IterM Id β} (step : it.Step),
  step.toPure = ⟨Std.IterStep.mapIterator Std.IterM.toIter ↑step, ⋯⟩
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_smul_le : ∀ {R : Type u} [inst : Semiring R] {S : Type u_2} [inst_1 : SMulZeroClass S R] (a : S) (p : Polynomial R),
  (a • p).degree ≤ p.degree
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.smul_opposite_mul : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G} (x g : G) (h : ↥H.op), h • (g * x) = g * h • x
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.Faithful.mapCommGrp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F : CategoryTheory.Functor C D} [inst_6 : F.Braided] [F.Faithful], F.mapCommGrp.Faithful
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The cocone over the proposed colimit additive monoid.  -/
AddMonCat.FilteredColimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J AddMonCat) → [CategoryTheory.IsFiltered J] → CategoryTheory.Limits.Cocone F
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.range_fst : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S],
  NonUnitalRingHom.srange (NonUnitalRingHom.fst R S) = ⊤
-- Mathlib.Algebra.Order.IsBotOne
zero_max : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Zero α] [IsBotZeroClass α] (a : α), max 0 a = a
-- Init.Data.Vector.MapIdx
Vector.mapIdx_singleton : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {a : α}, Vector.mapIdx f #v[a] = #v[f 0 a]
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine'.match_3.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (fuel : ℕ) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ),
  fuel = 0 →
    (match fuel with
      | 0 => h_1 ()
      | fuel.succ => h_2 fuel) ≍
      h_1 ()
-- Init.NotationExtra
/-- Expands
```
class abbrev C <params> := D_1, ..., D_n
```
into
```
class C <params> extends D_1, ..., D_n
attribute [instance] C.mk
```
 -/
Lean.Parser.Command.classAbbrev : Lean.ParserDescr
-- Mathlib.Order.Hom.Bounded
BotHom.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : Bot α] → [inst_1 : Bot β] → FunLike (BotHom α β) α β
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.one_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.enorm_exp_I_mul_ofReal_sub_one_le : ∀ {x : ℝ}, ‖Complex.exp (Complex.I * ↑x) - 1‖ₑ ≤ ‖x‖ₑ
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
MeasureTheory.IsSeparable.mk : ∀ {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X},
  (∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜) → MeasureTheory.IsSeparable μ
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.ofIso_toLimitPresentation : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} (h : P.LimitOfShape J X) {Y : C} (e : X ≅ Y),
  (h.ofIso e).toLimitPresentation = h.ofIso e
-- Mathlib.RingTheory.Ideal.Prime
/-- If a product lies in the prime ideal, then at least one element lies in the prime ideal.  -/
Ideal.IsPrime.mem_or_mem' : ∀ {α : Type u} {inst : Semiring α} {I : Ideal α} [self : I.IsPrime] {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
/-- If `R` is of characteristic `p` and `¬p ∣ n`, then
`cyclotomic (n * p) R = (cyclotomic n R) ^ (p - 1)`.  -/
Polynomial.cyclotomic_mul_prime_eq_pow_of_not_dvd : ∀ (R : Type u_1) {p n : ℕ} [hp : Fact (Nat.Prime p)] [inst : Ring R] [CharP R p],
  ¬p ∣ n → Polynomial.cyclotomic (n * p) R = Polynomial.cyclotomic n R ^ (p - 1)
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the forward direction of the isomorphism
`PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂` w.r.t. the canonical maps to the limit.  -/
CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] (K₁ : CategoryTheory.Functor J₁ C₁)
  (K₂ : CategoryTheory.Functor J₂ C₂) (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] [inst_6 : CategoryTheory.Limits.HasLimit K₁]
  [inst_7 : CategoryTheory.Limits.HasLimit K₂] (j : J₁ × J₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂ K₁ K₂ G).hom
      (CategoryTheory.CategoryStruct.comp
        ((G.map (CategoryTheory.Limits.limit.π K₁ j.1)).app (CategoryTheory.Limits.limit K₂))
        ((G.obj (K₁.obj j.1)).map (CategoryTheory.Limits.limit.π K₂ j.2))) =
    CategoryTheory.Limits.limit.π
      (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemView.mk.injEq : ∀ (omitFields : Array (Lean.Ident × Lean.Name)) (handlers : Array Lean.Elab.ConfigEval.EvalConfigItemHandler)
  (omitFields_1 : Array (Lean.Ident × Lean.Name)) (handlers_1 : Array Lean.Elab.ConfigEval.EvalConfigItemHandler),
  ({ omitFields := omitFields, handlers := handlers } = { omitFields := omitFields_1, handlers := handlers_1 }) =
    (omitFields = omitFields_1 ∧ handlers = handlers_1)
-- Mathlib.GroupTheory.Coprod.Basic
/-- Map `M ∗ N` to `N ∗ M` by applying `Sum.swap` to each element of the underlying list.

See also `MulEquiv.coprodComm` for a `MulEquiv` version.  -/
Monoid.Coprod.swap : (M : Type u_1) →
  (N : Type u_2) → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → Monoid.Coprod M N →* Monoid.Coprod N M
-- Mathlib.Topology.Bases
/-- A point `a` is in the closure of `s` iff all basis sets containing `a` intersect `s`.  -/
TopologicalSpace.IsTopologicalBasis.mem_closure_iff : ∀ {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis b → ∀ {s : Set α} {a : α}, a ∈ closure s ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty
-- Mathlib.Order.Basic
/-- **Alias** of `lt_of_lt_of_eq`. -/
LT.lt.trans_eq : ∀ {α : Type u_1} {a b c : α} [inst : LT α], a < b → b = c → a < c
-- Mathlib.GroupTheory.Congruence.Defs
Con.hrecOn₂.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {cM : Con M} {cN : Con N}
  {φ : cM.Quotient → cN.Quotient → Sort u_4} (a : cM.Quotient) (b : cN.Quotient) (f : (x : M) → (y : N) → φ ↑x ↑y)
  (h : ∀ (x : M) (y : N) (x' : M) (y' : N), cM x x' → cN y y' → f x y ≍ f x' y'),
  Con.hrecOn₂ a b f h = Quotient.hrecOn₂' a b f h
-- Mathlib.Algebra.Category.ModuleCat.Free
/-- In the commutative diagram
```
    f     g
 X₁ --→ X₂ --→ X₃
 ↑      ↑      ↑
v|     u|     w|
 ι  → ι ⊕ ι' ← ι'
```
where the top row is an exact sequence of modules and the maps on the bottom are `Sum.inl` and
`Sum.inr`. If `v` spans `X₁` and `w` spans `X₃`, then `u` spans `X₂`.  -/
ModuleCat.span_exact : ∀ {ι : Type u_1} {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.Exact →
    ∀ {v : ι → ↑S.X₁} {β : Type u_4} {u : ι ⊕ β → ↑S.X₂},
      u ∘ Sum.inl = ⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v →
        ⊤ ≤ Submodule.span R (Set.range v) →
          ⊤ ≤ Submodule.span R (Set.range (⇑(CategoryTheory.ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)) →
            ⊤ ≤ Submodule.span R (Set.range u)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
MulEquiv.toContinuousMulEquiv_apply : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Mul G] [inst_3 : Mul H]
  (e : G ≃* H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (a : G), (e.toContinuousMulEquiv he) a = e a
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddSemigroup : {α : Type u_1} → [AddSemigroup α] → AddSemigroup (Lex α)
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.mk_eq_mk : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x y : L},
  ConjRootClass.mk K x = ConjRootClass.mk K y ↔ IsConjRoot K x y
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
MeasureTheory.Integrable.prodLp_snd : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  {f : X → WithLp q (E × F)}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun x => (f x).snd) μ
-- Mathlib.Dynamics.Ergodic.Ergodic
Ergodic.mk : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : autoParam (MeasureTheory.Measure α) Ergodic._auto_1},
  MeasureTheory.MeasurePreserving f μ μ → PreErgodic f μ → Ergodic f μ
-- Mathlib.Computability.TuringMachine.Tape
/-- Construct a tape from a left side and an inclusive right side.  -/
Turing.Tape.mk' : {Γ : Type u_1} → [inst : Inhabited Γ] → Turing.ListBlank Γ → Turing.ListBlank Γ → Turing.Tape Γ
-- Init.Try
Lean.Try.markerUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Util.Superscript
/-- Successfully delaborates only if the resulting expression can be superscripted.

See `Mapping.superscript` in this file for legal superscript characters.  -/
Mathlib.Tactic.delabSuperscript : Lean.PrettyPrinter.Delaborator.Delab