mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- **Alias** of `RootPairing.EmbeddedG2.setOfPred_index_eq_univ`. -/
RootPairing.EmbeddedG2.setOf_index_eq_univ : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible],
  {RootPairing.EmbeddedG2.long P, -RootPairing.EmbeddedG2.long P, RootPairing.EmbeddedG2.short P,
      -RootPairing.EmbeddedG2.short P, RootPairing.EmbeddedG2.shortAddLong P, -RootPairing.EmbeddedG2.shortAddLong P,
      RootPairing.EmbeddedG2.twoShortAddLong P, -RootPairing.EmbeddedG2.twoShortAddLong P,
      RootPairing.EmbeddedG2.threeShortAddLong P, -RootPairing.EmbeddedG2.threeShortAddLong P,
      RootPairing.EmbeddedG2.threeShortAddTwoLong P, -RootPairing.EmbeddedG2.threeShortAddTwoLong P} =
    Set.univ
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Cases.clear : ∀ {σs : List (Type u_1)} {Q H T : Std.Do.SPred σs}, (Q ∧ ⌜True⌝ ⊢ₛ T) → Q ∧ H ⊢ₛ T
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
AddMonoidAlgebra.toDirectSum_ofNat : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring M] (n : ℕ)
  [inst_3 : n.AtLeastTwo], (OfNat.ofNat n).toDirectSum = OfNat.ofNat n
-- Lean.Data.Lsp.Basic
/-- Reference to the progress of some in-flight piece of work.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#progress)
 -/
Lean.Lsp.ProgressToken : Type
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost_hom_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X X_1 : C),
  ((CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost F).hom.app X).app X_1 =
    CategoryTheory.Functor.LaxMonoidal.μ F X X_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.keysArray.size = t.size
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.cokernel.π_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  (CategoryTheory.Limits.cokernel.π g.unop).op =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.cokernelUnopOp g).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Order.WithBot
WithBot.top_eq_coe : ∀ {α : Type u_1} [inst : Top α] {a : α}, ⊤ = ↑a ↔ ⊤ = a
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x` is a right cancel additive
semigroup if `β` is a right cancel additive semigroup.  -/
FunLike.addRightCancelSemigroup : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] → [inst_2 : AddRightCancelSemigroup β] → [IsAddApply F α β] → AddRightCancelSemigroup F
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.isOver_toRationalMap_iff_of_isSeparated : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] [AlgebraicGeometry.IsReduced X]
  [S.IsSeparated] {f : X.PartialMap Y},
  AlgebraicGeometry.Scheme.RationalMap.IsOver S f.toRationalMap ↔ AlgebraicGeometry.Scheme.PartialMap.IsOver S f
-- Std.Time.DateTime.Timestamp
/-- Subtracts a `Day.Offset` from the given `Timestamp`.
 -/
Std.Time.Timestamp.subDays : Std.Time.Timestamp → Std.Time.Day.Offset → Std.Time.Timestamp
-- Mathlib.CategoryTheory.Iso
CategoryTheory.eq_of_inv_eq_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [inst_1 : CategoryTheory.IsIso f]
  [inst_2 : CategoryTheory.IsIso g], CategoryTheory.inv f = CategoryTheory.inv g → f = g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.comp_right : ∀ {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} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [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'}
  {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [inst_6 : CategoryTheory.Category.{v₇, u₇} A'']
  [inst_7 : CategoryTheory.Category.{v₈, u₈} B''] [inst_8 : CategoryTheory.Category.{v₉, u₉} C'']
  {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''}
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  (ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''), (ψ.comp ψ').right = ψ.right.comp ψ'.right
-- Mathlib.Topology.Algebra.Monoid
/-- Construct a bundled semigroup homomorphism from a pointwise limit of semigroup homomorphisms.  -/
mulHomOfTendsto : {α : Type u_2} →
  {M₁ : Type u_6} →
    {M₂ : Type u_7} →
      [inst : TopologicalSpace M₂] →
        [T2Space M₂] →
          [inst_2 : Mul M₁] →
            [inst_3 : Mul M₂] →
              [ContinuousMul M₂] →
                {F : Type u_8} →
                  [inst_5 : FunLike F M₁ M₂] →
                    [MulHomClass F M₁ M₂] →
                      {l : Filter α} →
                        (f : M₁ → M₂) →
                          (g : α → F) → [l.NeBot] → Filter.Tendsto (fun a x => (g a) x) l (nhds f) → M₁ →ₙ* M₂
-- Mathlib.Data.List.Lattice
List.Sublist.inter_left : ∀ {α : Type u_1} [inst : DecidableEq α] {l₁ l₂ l₃ : List α}, l₂.Sublist l₃ → (l₁ ∩ l₂).Sublist (l₁ ∩ l₃)
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise multiplication of `f` and `g`,
which monovary together, is unchanged by a permutation if and only if `f ∘ σ` and `g` monovary
together. Stated by permuting the entries of `g`.  -/
Monovary.sum_comp_perm_mul_eq_sum_mul_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {σ : Equiv.Perm ι} {f g : ι → α} [inst_4 : Fintype ι],
  Monovary f g → (∑ i, f (σ i) * g i = ∑ i, f i * g i ↔ Monovary (f ∘ ⇑σ) g)
-- Mathlib.Analysis.Calculus.Deriv.Basic
differentiableAt_of_deriv_ne_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, deriv f x ≠ 0 → DifferentiableAt 𝕜 f x
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
PiTensorProduct.dualDistrib.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Finite ι],
  PiTensorProduct.dualDistrib =
    LinearMap.compRight R (PiTensorProduct.constantBaseRingEquiv ι R).toLinearMap ∘ₗ PiTensorProduct.piTensorHomMap
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.CommaMorphism.ext_iff : ∀ {A : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} A} {B : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} B}
  {T : Type u₃} {inst_2 : CategoryTheory.Category.{v₃, u₃} T} {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} {x y : CategoryTheory.CommaMorphism X Y},
  x = y ↔ x.left = y.left ∧ x.right = y.right
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_intCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIcoMod hp a (b + ↑m * p) = toIcoMod hp a b
-- Aesop.Tree.Check
_private.Aesop.Tree.Check.0.Aesop.MVarClusterRef.checkMVars.checkGoalMVars : Lean.Meta.SavedState → Aesop.Goal → Lean.MetaM Unit
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a `G`-representation `(V, ρ)` and a type `α`, this is the linear equivalence
`(α →₀ V)_G ≃ₗ (α →₀ V_G)` sending `⟦single a v⟧ ↦ single a ⟦v⟧`.  -/
Representation.coinvariantsFinsuppLEquiv : {k : Type u_6} →
  {G : Type u_7} →
    {V : Type u_8} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) → (α : Type u_9) → (ρ.finsupp α).Coinvariants ≃ₗ[k] α →₀ ρ.Coinvariants
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBumpBase.smooth : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (self : ContDiffBumpBase E),
  ContDiffOn ℝ (↑⊤) (Function.uncurry self.toFun) (Set.Ioi 1 ×ˢ Set.univ)
-- Mathlib.Order.Concept
Concept.intent_ofAttributes : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β),
  (Concept.ofAttributes r t).intent = upperPolar r (lowerPolar r t)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
prod_eq_tprod_mulIndicator : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) (s : Finset β)
  (L : optParam (SummationFilter β) (SummationFilter.unconditional β)) [L.LeAtTop],
  ∏ x ∈ s, f x = ∏'[L] (x : β), (↑s).mulIndicator f x
-- Mathlib.Data.List.AList
/-- Erase a key from the map. If the key is not present, do nothing.  -/
AList.erase : {α : Type u} → {β : α → Type v} → [DecidableEq α] → α → AList β → AList β
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_eq_isSome_get? : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {a : α}, m.contains a = (Std.DHashMap.Internal.Raw₀.Const.get? m a).isSome
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.adjoin_image_leastExt : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  (i : (Module.rank F E).ord.ToType),
  IntermediateField.adjoin F
      (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E '' Set.Iio i) =
    IntermediateField.adjoin F
      (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) '' Set.Iio (Field.Emb.Cardinal.leastExt F E i))
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.instNoncompactSpace : NoncompactSpace UpperHalfPlane
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Constructor for morphisms in `Grp C`.  -/
CategoryTheory.Grp.homMk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → {A B : CategoryTheory.Grp C} → (A.toMon ⟶ B.toMon) → (A ⟶ B)
-- Mathlib.RingTheory.Jacobson.Ideal
TwoSidedIdeal.mem_jacobson_iff : ∀ {R : Type u} [inst : Ring R] {x : R} {I : TwoSidedIdeal R}, x ∈ I.jacobson ↔ ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
-- Mathlib.Topology.UnitInterval
unitInterval.symm_zero : unitInterval.symm 0 = 1
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.lt_iff_exists_lt : ∀ {α : Type u_1} {a b : α} [inst : LinearOrder α], Order.IsSuccPrelimit b → (a < b ↔ ∃ c < b, a < c)
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.mk.sizeOf_spec : ∀ {M : Type u_10} {N : Type u_11} [inst : Add M] [inst_1 : Add N] [inst_2 : SizeOf M] [inst_3 : SizeOf N]
  (toFun : M → N) (map_add' : ∀ (x y : M), toFun (x + y) = toFun x + toFun y),
  sizeOf { toFun := toFun, map_add' := map_add' } = 1
-- Init.Control.Lawful.MonadLift.Lemmas
monadLift_seqLeft : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  [LawfulMonadLiftT m n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β),
  monadLift (x <* y) = monadLift x <* monadLift y
-- Mathlib.Order.JordanHolder
CompositionSeries.ext_iff : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ : CompositionSeries X},
  s₁ = s₂ ↔ ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f f_1 : F),
  f = f_1 → ∀ (S S_1 : Submonoid N), S = S_1 → Submonoid.comap f S = Submonoid.comap f_1 S_1
-- Mathlib.Algebra.Vertex.VertexOperator
VertexOperator.coeff_eq_zero_of_lt_order : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : VertexOperator R V) (n : ℤ) (x : V), n < ((HahnModule.of R).symm (A x)).order → (HVertexOperator.coeff A n) x = 0
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_sq' : ∀ (x : ℂ), Complex.cos x ^ 2 = 1 - Complex.sin x ^ 2
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
lt_or_le_of_mul_le_mul : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Mul α] [MulLeftStrictMono α] [MulRightMono α] {a₁ a₂ b₁ b₂ : α},
  a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂
-- Batteries.Data.String.Legacy
/-- Creates a new string that contains the longest prefix of `s` in which `p` returns `true` for all
characters.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`. Its runtime behavior is equivalent to that of `String.takeWhile`.

Examples:
* `"red green blue".takeWhile (·.isLetter) = "red"`
* `"red green blue".takeWhile (· == 'r') = "r"`
* `"red green blue".takeWhile (· != 'n') = "red gree"`
* `"red green blue".takeWhile (fun _ => true) = "red green blue"`
 -/
String.Legacy.takeWhile : String → (Char → Bool) → String
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ` is
`p` if `p ≠ 2`.  -/
IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  p ≠ 2 → (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.le_of_lt_minimalPeriod_of_iterate_eq : ∀ {α : Type u_1} {f : α → α} {x : α} {m n : ℕ}, m < Function.minimalPeriod f x → f^[m] x = f^[n] x → m ≤ n
-- Lean.Parser.Types
/-- Run `p` with a fresh cache, restore outer cache afterwards.
`p` may access the entire syntax stack.
 -/
Lean.Parser.withResetCache : Lean.Parser.Parser → Lean.Parser.Parser
-- Aesop.Util.Basic
Aesop.runTermElabMAsCoreM : {α : Type} → Lean.Elab.TermElabM α → Lean.CoreM α
-- Mathlib.Logic.Function.DependsOn
/-- A function `f` depends on `s` if, whenever `x` and `y` coincide over `s`, `f x = f y`.

It should be interpreted as "`f` _potentially_ depends only on variables in `s`".
However it might be the case that `f` does not depend at all on variables in `s`,
for example if `f` is constant. As a consequence, `DependsOn f univ` is always true,
see `dependsOn_univ`.  -/
DependsOn : {ι : Type u_1} → {α : ι → Type u_2} → {β : Type u_3} → (((i : ι) → α i) → β) → Set ι → Prop
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- For `1 ≤ r`, the logarithmic counting function for the poles of `f + g` is less than or equal to the
sum of the logarithmic counting functions for the poles of `f` and `g`, respectively.
 -/
ValueDistribution.logCounting_add_top_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {r : ℝ},
  Meromorphic f₁ →
    Meromorphic f₂ →
      1 ≤ r →
        ValueDistribution.logCounting (f₁ + f₂) ⊤ r ≤
          (ValueDistribution.logCounting f₁ ⊤ + ValueDistribution.logCounting f₂ ⊤) r
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil.eq_1 : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil = Stream'.Seq.nil
-- Mathlib.Order.Hom.BoundedLattice
/-- `BoundedLatticeHomClass F α β` states that `F` is a type of bounded lattice morphisms.

You should extend this class when you extend `BoundedLatticeHom`.  -/
BoundedLatticeHomClass : (F : Type u_6) →
  (α : Type u_7) →
    (β : Type u_8) →
      [inst : Lattice α] → [inst_1 : Lattice β] → [BoundedOrder α] → [BoundedOrder β] → [FunLike F α β] → Prop
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredLimit_of_not_isPredPrelimit : ∀ {α : Type u_1} {a : α} [inst : Preorder α], ¬Order.IsPredPrelimit a → ¬Order.IsPredLimit a
-- Init.Data.Array.Range
Array.self_mem_range_succ : ∀ {n : ℕ}, n ∈ Array.range (n + 1)
-- Init.System.IO
IO.instToStringTaskState : ToString IO.TaskState
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.IsRelIff.rel' : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} [self : e.IsRelIff]
  (i₁ i₂ : ι), c'.Rel (e.f i₁) (e.f i₂) → c.Rel i₁ i₂
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.comp_assoc : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {C : Type u_4} [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : TopologicalSpace C] {D : Type u_5}
  [inst_10 : Semiring D] [inst_11 : Algebra R D] [inst_12 : TopologicalSpace D] (h : C →A[R] D) (g : B →A[R] C)
  (f : A →A[R] B), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.zero_eq_mk : ∀ {α : Type u}, 0 = FreeAddGroup.mk []
-- Lean.Expr
/-- Given `a : Nat`, returns `NatCast.natCast (R := Int) a`  -/
Lean.mkIntNatCast : Lean.Expr → Lean.Expr
-- Std.Data.Iterators.Combinators.Monadic.Zip
/-- `it.PlausibleStep step` is the proposition that `step` is a possible next step from the
`zip` iterator `it`. This is mostly internally relevant, except if one needs to manually
prove termination (`Finite` or `Productive` instances, for example) of a `zip` iterator.
 -/
Std.Iterators.Types.Zip.PlausibleStep : {m : Type w → Type w'} →
  {α₁ β₁ : Type w} →
    [inst : Std.Iterator α₁ m β₁] →
      {α₂ β₂ : Type w} →
        [Std.Iterator α₂ m β₂] → Std.IterM m (β₁ × β₂) → Std.IterStep (Std.IterM m (β₁ × β₂)) (β₁ × β₂) → Prop
-- Mathlib.GroupTheory.Exponent
Commute.of_orderOf_dvd_two : ∀ {G : Type u} [inst : Monoid G] [IsCancelMul G], (∀ (g : G), orderOf g ∣ 2) → ∀ (a b : G), Commute a b
-- Mathlib.CategoryTheory.Monoidal.Opposite
Quiver.Hom.mop_inj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}, Function.Injective Quiver.Hom.mop
-- Std.Data.DTreeMap.Lemmas
/-- Simpler variant of `getD_filterMap` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Const.getD_filterMap' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α} {fallback : γ},
  Std.DTreeMap.Const.getD (Std.DTreeMap.filterMap f t) k fallback =
    ((Std.DTreeMap.Const.get? t k).bind (f k)).getD fallback
-- Mathlib.Computability.PartrecCode
/-- Returns a code for the constant function outputting a particular natural.  -/
Nat.Partrec.Code.const : ℕ → Nat.Partrec.Code
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.smulLeft_apply_apply : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] {G : Type u_9} [inst_4 : Group G] [inst_5 : DistribMulAction G M₁]
  [inst_6 : ContinuousConstSMul G M₁] [inst_7 : SMulCommClass G R₁ M₁] (g : G) (a : M₁),
  (ContinuousLinearEquiv.smulLeft g) a = g • a
-- Mathlib.Control.Bitraversable.Instances
Bitraversable.const : Bitraversable Functor.Const
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- Basic hypothesis to talk about a `C^n` (Lie) monoid or a `C^n` semigroup.
A `C^n` monoid over `G`, for example, is obtained by requiring both the instances `Monoid G`
and `ContMDiffMul I n G`.

See also `ContMDiffSMul I I' n G M` for `C^n` actions of `G` on a manifold `M`.  -/
ContMDiffMul : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              ModelWithCorners 𝕜 E H →
                WithTop ℕ∞ → (G : Type u_4) → [Mul G] → [inst : TopologicalSpace G] → [ChartedSpace H G] → Prop
-- Mathlib.Topology.Order.Lattice
Filter.Tendsto.finset_inf_nhds_apply : ∀ {L : Type u_1} [inst : TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ι → α → L} {l : Filter α}
  {g : ι → L} [inst_1 : SemilatticeInf L] [inst_2 : OrderTop L] [ContinuousInf L],
  (∀ i ∈ s, Filter.Tendsto (f i) l (nhds (g i))) → Filter.Tendsto (fun a => s.inf fun x => f x a) l (nhds (s.inf g))
-- Lean.Meta.Tactic.Grind.PP
Lean.Meta.Grind.instInhabitedResult.default : Lean.Meta.Grind.Result✝
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.le_iff : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.PartialEquiv M N},
  f ≤ g ↔
    ∃ (dom_le_dom : f.dom ≤ g.dom) (cod_le_cod : f.cod ≤ g.cod),
      ∀ (x : ↥f.dom),
        (FirstOrder.Language.Substructure.inclusion cod_le_cod) (f.toEquiv x) =
          g.toEquiv ((FirstOrder.Language.Substructure.inclusion dom_le_dom) x)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.isNewAnswer : Array Lean.Meta.SynthInstance.Answer → Lean.Meta.SynthInstance.Answer → Bool
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- In a space with second countable topology and a sigma-finite measure,
`AEFinStronglyMeasurable` and `AEMeasurable` are equivalent.  -/
MeasureTheory.aefinStronglyMeasurable_iff_aemeasurable : ∀ {α : Type u_1} {G : Type u_5} [inst : SeminormedAddCommGroup G] [inst_1 : MeasurableSpace G] [BorelSpace G]
  [SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α)
  [MeasureTheory.SigmaFinite μ], MeasureTheory.AEFinStronglyMeasurable f μ ↔ AEMeasurable f μ
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion within a ball, then the partial sums
`p.partialSum n z` converge to `f (x + y)` as `n → ∞` and `z → y`. Note that `x + z` doesn't need
to belong to the set where the power series expansion holds.  -/
HasFPowerSeriesWithinOnBall.tendsto_partialSum_prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {y : E},
  HasFPowerSeriesWithinOnBall f p s x r →
    y ∈ Metric.eball 0 r →
      x + y ∈ insert x s → Filter.Tendsto (fun z => p.partialSum z.1 z.2) (Filter.atTop ×ˢ nhds y) (nhds (f (x + y)))
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius_apply_prime : ∀ {p : ℕ}, Nat.Prime p → ArithmeticFunction.moebius p = -1
-- Plausible.Gen
_private.Plausible.Gen.0.Plausible.Gen.sumFst : {α : Type u_1} → List (ℕ × α) → ℕ
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
/-- Applies the given variable permutation to `e`  -/
Int.Internal.Linear.Expr.applyPerm : Lean.Perm → Int.Internal.Linear.Expr → Int.Internal.Linear.Expr
-- Mathlib.Condensed.Light.Module
instAbelianLightCondMod : (R : Type u) → [inst : Ring R] → CategoryTheory.Abelian (LightCondMod R)
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.diagramMap.eq_3 : ∀ {ι : Type v} {α : Type u} (U : ι → α) [inst : SemilatticeInf α] (i j : ι),
  CategoryTheory.Pairwise.diagramMap U (CategoryTheory.Pairwise.Hom.left i j) = CategoryTheory.homOfLE ⋯
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  (1 - Polynomial.X ^ 2) * Polynomial.Chebyshev.U R n =
    Polynomial.X * Polynomial.Chebyshev.T R (n + 1) - Polynomial.Chebyshev.T R (n + 2)