mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cosh θ` to the
value `cosh (n * θ)`.  -/
Polynomial.Chebyshev.T_real_cosh : ∀ (θ : ℝ) (n : ℤ), Polynomial.eval (Real.cosh θ) (Polynomial.Chebyshev.T ℝ n) = Real.cosh (↑n * θ)
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_eq_self_iff : ∀ {α : Type u_1} {M : Matroid α} {D : Set α}, M.delete D = M ↔ Disjoint D M.E
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Result.complexArgs : Lean.Elab.Tactic.ElimApp.Result → Array Lean.Expr
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.nhds_σ : ∀ {α : Type u_1} [inst : TopologicalSpace α] (F : Ctop.Realizer α) (a : α), (F.nhds a).σ = { s // a ∈ F.F.f s }
-- Mathlib.Data.List.OffDiag
/-- If `l : List α` is a list with no duplicates, then `x : α × α` belongs to `List.offDiag l`
iff both components of `x` belong to `l` and they are not equal.  -/
List.Nodup.mem_offDiag : ∀ {α : Type u_1} {l : List α}, l.Nodup → ∀ {x : α × α}, x ∈ l.offDiag ↔ x.1 ∈ l ∧ x.2 ∈ l ∧ x.1 ≠ x.2
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toEnd_zero : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α], CentroidHom.toEnd 0 = 0
-- Mathlib.MeasureTheory.Group.Arithmetic
IsUnit.aemeasurable_const_smul_iff : ∀ {M : Type u_4} {β : Type u_5} {α : Type u_6} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace α] {f : α → β}
  {μ : MeasureTheory.Measure α} [inst_2 : Monoid M] [inst_3 : MulAction M β] [MeasurableConstSMul M β] {c : M},
  IsUnit c → (AEMeasurable (fun x => c • f x) μ ↔ AEMeasurable f μ)
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.prodComparisonIso_algSpec_inv_left : ∀ {R : CommRingCat} (X Y : (CommAlgCat ↑R)ᵒᵖ),
  CategoryTheory.Over.Hom.left
      (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso (AlgebraicGeometry.algSpec R) X Y).inv =
    (AlgebraicGeometry.pullbackSpecIso ↑R ↑(Opposite.unop X) ↑(Opposite.unop Y)).hom
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toList_eq_match_rco : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.Rxo.IsAlwaysFinite α],
  r.toList =
    match Std.PRange.least? with
    | none => []
    | some least => (least...r.upper).toList
-- Mathlib.RingTheory.PowerSeries.WellKnown
/-- (1 + X + X^2 + ...) * (1 - X) = 1.

Note that the power series `1 + X + X^2 + ...` is written as `mk 1` where `1` is the constant
function so that `mk 1` is the power series with all coefficients equal to one.
 -/
PowerSeries.mk_one_mul_one_sub_eq_one : ∀ (S : Type u_1) [inst : CommRing S], PowerSeries.mk 1 * (1 - PowerSeries.X) = 1
-- Mathlib.Topology.SeparatedMap
IsSeparatedMap.const_of_comp : ∀ {X : Type u_1} {E : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace A] {p : E → X}
  {g : A → E},
  IsSeparatedMap p →
    IsLocallyInjective p →
      ∀ [PreconnectedSpace A], Continuous g → (∀ (a a' : A), p (g a) = p (g a')) → ∀ (a a' : A), g a = g a'
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {f : α → γ} {g : β → γ}
  {μ : autoParam (MeasureTheory.Measure α) ProbabilityTheory.IdentDistrib._auto_1}
  {ν : autoParam (MeasureTheory.Measure β) ProbabilityTheory.IdentDistrib._auto_3},
  AEMeasurable f μ →
    AEMeasurable g ν →
      MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g ν → ProbabilityTheory.IdentDistrib f g μ ν
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.IntegrableOn.swap : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite μ] {f : α × β → E} {s : Set α} {t : Set β},
  MeasureTheory.IntegrableOn f (s ×ˢ t) (μ.prod ν) → MeasureTheory.IntegrableOn (f ∘ Prod.swap) (t ×ˢ s) (ν.prod μ)
-- Mathlib.Computability.ContextFreeGrammar
/-- Rules for a grammar for a reversed language.  -/
ContextFreeRule.reverse : {T : Type u_1} → {N : Type u_2} → ContextFreeRule T N → ContextFreeRule T N
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.mulRightStrictMono : ∀ {α : Type u} [inst : LT α] [inst_1 : Mul α] [c : MulRightStrictMono α], MulRightStrictMono αᵒᵈ
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductIso_hom_comp_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.binaryProductIso F G).hom
      CategoryTheory.FunctorToTypes.prod.snd =
    CategoryTheory.Limits.prod.snd
-- Mathlib.Order.PrimeSeparator
DistribLattice.prime_ideal_of_disjoint_filter_ideal : ∀ {α : Type u_1} [inst : DistribLattice α] {F : Order.PFilter α} {I : Order.Ideal α},
  Disjoint ↑F ↑I → ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J
-- Mathlib.RepresentationTheory.Induced
Rep.indFunctor_map : ∀ (k : Type u) {G : Type v} {H : Type v'} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  {X Y : Rep.{w, u, v} k G} (f : X ⟶ Y), (Rep.indFunctor k φ).map f = Rep.indMap φ f
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.incl_map : ∀ {X Y : CategoryTheory.InducedCategory (Type u_1) CategoryTheory.ObjectProperty.FullSubcategory.obj} (f : X ⟶ Y),
  FintypeCat.incl.map f = f.hom
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {a : α} {c : ℕ},
  (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).get? a = none
-- Mathlib.RingTheory.Bialgebra.Hom
/-- Turn an element of a type `F` satisfying `BialgHomClass F R A B` into an actual
`BialgHom`. This is declared as the default coercion from `F` to `A →ₐc[R] B`.  -/
BialgHomClass.toBialgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {F : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R B] →
                  [inst_5 : CoalgebraStruct R A] →
                    [inst_6 : CoalgebraStruct R B] → [inst_7 : FunLike F A B] → [BialgHomClass F R A B] → F → A →ₐc[R] B
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_add_cancel_left : ∀ {x : ℤ} {n : ℕ} {y : ℤ} (i : ℤ), (i + x).bmod n = (i + y).bmod n ↔ x.bmod n = y.bmod n
-- Init.Data.Array.MapIdx
Array.mapFinIdx_eq_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β} {ys : Array β},
  xs.mapFinIdx f = ys ↔ ∃ (h : ys.size = xs.size), ∀ (i : ℕ) (h_1 : i < xs.size), ys[i] = f i xs[i] h_1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofZeros_K : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).K = S.X₂
-- Mathlib.Topology.Algebra.Support
continuous_of_mulTSupport : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] [inst_2 : TopologicalSpace β] {f : α → β},
  (∀ x ∈ mulTSupport f, ContinuousAt f x) → Continuous f
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Precoverage.toPretopology_toPrecoverage : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (J : CategoryTheory.Precoverage C) [inst_2 : J.HasIsos] [inst_3 : J.IsStableUnderBaseChange]
  [inst_4 : J.IsStableUnderComposition], (CategoryTheory.Precoverage.toPretopology C J).toPrecoverage = J
-- Lean.Server.Rpc.RequestHandling
Lean.Server.registerBuiltinRpcProcedure : Lean.Name →
  (paramType respType : Type) →
    [Lean.Server.RpcEncodable paramType] →
      [Lean.Server.RpcEncodable respType] →
        (paramType → Lean.Server.RequestM (Lean.Server.RequestTask respType)) → IO Unit
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHomClass.instLinearMapClass : ∀ {R : Type u} [inst : Semiring R] {A : Type u_1} {B : Type u_2} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] {F : Type u_3} [inst_4 : FunLike F A B]
  [inst_5 : Module R B] [NonUnitalAlgHomClass F R A B], LinearMapClass F R A B
-- Mathlib.Computability.Reduce
equivalence_of_manyOneEquiv : ∀ {α : Type u_1} [inst : Primcodable α], Equivalence ManyOneEquiv
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_congr : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s₁ s₂ : Finset β} {f g : β → α},
  s₁ = s₂ → (∀ a ∈ s₂, f a = g a) → s₁.inf f = s₂.inf g
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.forall : ∀ {α : Type u} {p : Multiplicative α → Prop}, (∀ (a : Multiplicative α), p a) ↔ ∀ (a : α), p (Multiplicative.ofAdd a)
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg_below_dvd : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.LiesOver q], q.inertiaDeg R ∣ r.inertiaDeg R
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Topology.IsInducing.summable_iff_tsum_comp_mem_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [inst_2 : AddCommMonoid γ] [inst_3 : TopologicalSpace γ] [T2Space γ] {G : Type u_4}
  [inst_5 : FunLike G α γ] [AddMonoidHomClass G α γ] {g : G},
  Topology.IsInducing ⇑g → ∀ (f : β → α), Summable f L ↔ Summable (⇑g ∘ f) L ∧ ∑'[L] (i : β), g (f i) ∈ Set.range ⇑g
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.le_ofPrime : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (P : Ideal ↥A) [inst_1 : P.IsPrime], A ≤ A.ofPrime P
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenConj_mul_goldenRatio : Real.goldenConj * Real.goldenRatio = -1