mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β}, LeftOrdContinuous g → LeftOrdContinuous f → LeftOrdContinuous (g ∘ f)
-- Lean.Elab.DocString
/-- An identifier  -/
Lean.Doc.DocArg.ident : Lean.Ident → Lean.Doc.DocArg
-- Mathlib.Order.Basic
Ne.le_iff_lt : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≠ b → (a ≤ b ↔ a < b)
-- Mathlib.Order.Concept
Order.IsIntent.iInter : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Set β),
  (∀ (i : ι), Order.IsIntent r (f i)) → Order.IsIntent r (⋂ i, f i)
-- Init.Conv
/-- `rw [rules]` applies the given list of rewrite rules to the target.
See the `rw` tactic for more information.  -/
Lean.Parser.Tactic.Conv.convRw__ : Lean.ParserDescr
-- Mathlib.Data.Matrix.Reflection
_private.Mathlib.Data.Matrix.Reflection.0.Matrix.transposeᵣ.match_1.eq_2 : ∀ {α : Type u_1} (motive : (x x_1 : ℕ) → Matrix (Fin x) (Fin x_1) α → Sort u_2) (x n : ℕ)
  (A : Matrix (Fin x) (Fin (n + 1)) α) (h_1 : (x : ℕ) → (x_1 : Matrix (Fin x) (Fin 0) α) → motive x 0 x_1)
  (h_2 : (x n : ℕ) → (A : Matrix (Fin x) (Fin (n + 1)) α) → motive x n.succ A),
  (match x, n.succ, A with
    | x, 0, x_1 => h_1 x x_1
    | x, n.succ, A => h_2 x n A) =
    h_2 x n A
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The morphism in C underlying the morphism in the Kleisli category.  -/
CategoryTheory.Cokleisli.Hom.of : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {U : CategoryTheory.Comonad C} → {c c' : CategoryTheory.Cokleisli U} → c.Hom c' → (U.obj c.of ⟶ c'.of)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_inv : ∀ {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.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)]
  {j : J} {k : K},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).obj j) k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) j)
        (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).inv) =
    CategoryTheory.Limits.colimit.ι G (j, k)
-- Mathlib.Logic.Equiv.Defs
/-- `Sigma` type with a constant fiber is equivalent to the product.  -/
Equiv.sigmaEquivProd : (α : Type u_1) → (β : Type u_2) → (_ : α) × β ≃ α × β
-- Mathlib.Analysis.Convex.Between
/-- The point `y` is strictly between `x` and `z`.  -/
Sbtw : (R : Type u_1) →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : Ring R] → [PartialOrder R] → [inst_2 : AddCommGroup V] → [Module R V] → [AddTorsor V P] → P → P → P → Prop
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.node4L_lemma₄ : ∀ {a b c d : ℕ}, 3 * a ≤ b + c + 1 + d → b + c + 1 ≤ 3 * d → b ≤ 3 * c → a + b + 1 ≤ 3 * (c + d + 1)
-- Mathlib.Algebra.Order.Field.Basic
abs_div : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b : α), |a / b| = |a| / |b|
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.iteratedDerivWithin_cosh_Ioo : ∀ (n : ℕ) {a b x : ℝ}, x ∈ Set.Ioo a b → iteratedDerivWithin n Real.cosh (Set.Ioo a b) x = iteratedDeriv n Real.cosh x
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.inr.eq_1 : ∀ {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂),
  CategoryTheory.Limits.Types.Pushout.inr f g =
    TypeCat.ofHom fun x => Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) (Sum.inr x)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.finiteType : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] (f : Polynomial R) [inst_1 : CommSemiring S] [inst_2 : Algebra S R]
  [Algebra.FiniteType S R], Algebra.FiniteType S (AdjoinRoot f)
-- Mathlib.Data.List.GetD
List.getD_reverse : ∀ {α : Type u} {l : List α}, ∀ i < l.length, l.reverse.getD i = l.getD (l.length - 1 - i)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Theory.model_union_iff : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {T T' : L.Theory}, M ⊨ T ∪ T' ↔ M ⊨ T ∧ M ⊨ T'
-- Init.Data.Bool
Bool.or_not_eq_right_iff_and : ∀ {a b : Bool}, (a || !b) = b ↔ a = true ∧ b = true
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.mk : ∀ {p q r : NNReal}, p⁻¹ + q⁻¹ = r⁻¹ → 0 < p → 0 < q → p.HolderTriple q r
-- Init.Data.Nat.Lcm
Nat.dvd_lcm_left : ∀ (m n : ℕ), m ∣ m.lcm n
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_eq_lineMap : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c : P) (R : ℝ) (x : P),
  EuclideanGeometry.inversion c R x = (AffineMap.lineMap c x) ((R / dist x c) ^ 2)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLT.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (lowerBound : α),
  Std.DTreeMap.Internal.Impl.pruneLT✝ Std.DTreeMap.Internal.Impl.leaf lowerBound = Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.Algebra.Module.Equiv.Basic
/-- If `M₂` and `M₃` are linearly isomorphic then the two spaces of linear maps from `M` into `M₂`
and `M` into `M₃` are linearly isomorphic.  -/
LinearEquiv.congrRight : {R : Type u_1} →
  {M : Type u_5} →
    {M₂ : Type u_7} →
      {M₃ : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R M₂] → [inst_6 : Module R M₃] → (M₂ ≃ₗ[R] M₃) → (M →ₗ[R] M₂) ≃ₗ[R] M →ₗ[R] M₃
-- Mathlib.Analysis.Normed.Group.Basic
NormedCommGroup.uniformity_basis_dist : ∀ {E : Type u_5} [inst : SeminormedCommGroup E], (uniformity E).HasBasis (fun ε => 0 < ε) fun ε => {p | ‖p.1 / p.2‖ < ε}
-- Mathlib.Order.Hom.WithTopBot
/-- Taking the dual then adding `⊤` is the same as adding `⊥` then taking the dual.
This is the order iso form of `WithTop.ofDual`, as proven by `coe_toDualBotEquiv`.  -/
WithTop.toDualBotEquiv : {α : Type u_1} → [inst : LE α] → WithTop αᵒᵈ ≃o (WithBot α)ᵒᵈ
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.tensorKer_tmul : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f : N →ₗ[R] P) (m : M) (x : ↥f.ker), ↑((LinearMap.tensorKer S M f) (m ⊗ₜ[R] x)) = m ⊗ₜ[R] ↑x
-- Mathlib.Algebra.Order.SuccPred
strictMono_of_sub_one_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Sub α] [inst_3 : One α]
  [inst_4 : PredSubOrder α] [IsPredArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMin a → f (a - 1) < f a) → StrictMono f
-- Mathlib.Order.Hom.Lattice
SupHom.instSemilatticeSup.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β],
  SupHom.instSemilatticeSup = Function.Injective.semilatticeSup DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_localizationToStalk_assoc : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) {Z : ModuleCat R}
  (h : (AlgebraicGeometry.structurePresheafInModuleCat R M).stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.stalkToLocalizationₗ✝ R M x)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ✝ R M x) h) =
    h
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonNatIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [inst_5 : F'.LaxMonoidal] (e e_1 : F ≅ F')
  (e_e : e = e_1) [inst_6 : CategoryTheory.NatTrans.IsMonoidal e.hom],
  CategoryTheory.Functor.mapMonNatIso e = CategoryTheory.Functor.mapMonNatIso e_1
-- Mathlib.Order.Hom.Basic
OrderEmbedding.lt_iff_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) {a b : α}, f a < f b ↔ a < b
-- Init.Data.BitVec.Bitblast
/-- Show that `x <<< y` can be written in terms of `shiftLeftRec`.
This can be unfolded in terms of `shiftLeftRec_zero`, `shiftLeftRec_succ` for bit blasting.
 -/
BitVec.shiftLeft_eq_shiftLeftRec : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂), x <<< y = x.shiftLeftRec y (w₂ - 1)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.nsmul_mk : ∀ {R : Type u_1} {a b : R} [inst : NonAssocSemiring R] (n : ℕ) (x y : R),
  ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.fvar.inj : ∀ {fvarId fvarId_1 : Lean.FVarId}, Lean.Meta.Origin.fvar fvarId = Lean.Meta.Origin.fvar fvarId_1 → fvarId = fvarId_1
-- Mathlib.Analysis.Normed.Order.Hom.Ultra
/-- Proves that when a `SeminormedAddGroup` structure is constructed from an
`AddGroupSeminormClass` that satisfies `IsNonarchimedean`, the group has an `IsUltrametricDist`.  -/
AddGroupSeminormClass.isUltrametricDist : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : AddGroup α] [inst_2 : AddGroupSeminormClass F α ℝ]
  [inst_3 : Dist α] {f : F},
  IsNonarchimedean ⇑f →
    autoParam (inst_3 = (AddGroupSeminormClass.toSeminormedAddGroup f).toDist)
        AddGroupSeminormClass.isUltrametricDist._auto_1 →
      IsUltrametricDist α
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.const : ∀ {τ : Type u_3} {S : Type u_4} [inst : CommRing S] {a : MvPowerSeries τ S},
  PowerSeries.HasSubst a → MvPowerSeries.HasSubst fun x => a
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.quot_mk_eq_coe : ∀ {M : Type u_4} [inst : Add M] (c : AddCon M) (x : M), Quot.mk (⇑c) x = ↑x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.commutator.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.GrpObj G],
  CategoryTheory.GrpObj.commutator G =
    CategoryTheory.SemiCartesianMonoidalCategory.fst G G * CategoryTheory.SemiCartesianMonoidalCategory.snd G G *
        (CategoryTheory.SemiCartesianMonoidalCategory.fst G G)⁻¹ *
      (CategoryTheory.SemiCartesianMonoidalCategory.snd G G)⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.map'_comp_map : ∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C} {g h : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g]
  [inst_3 : CategoryTheory.Limits.HasCoproduct h] (p : α → β) (q : (a : α) → f a ⟶ g (p a)) (q' : (b : β) → g b ⟶ h b),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map' p q) (CategoryTheory.Limits.Sigma.map q') =
    CategoryTheory.Limits.Sigma.map' p fun a => CategoryTheory.CategoryStruct.comp (q a) (q' (p a))
-- Mathlib.Topology.Algebra.Star
Continuous.star : ∀ {α : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Star R] [ContinuousStar R]
  [inst_3 : TopologicalSpace α] {f : α → R}, Continuous f → Continuous fun x => star (f x)
-- Mathlib.Algebra.Homology.Homotopy
/-- `f (c.next i) i`.  -/
fromNext : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} → (i : ι) → ((i j : ι) → C.X i ⟶ D.X j) →+ (C.xNext i ⟶ D.X i)
-- Init.Data.Ord.Basic
Ordering.eq_eq_of_eq_swap : ∀ {o : Ordering}, o = o.swap → o = Ordering.eq
-- Mathlib.Topology.Constructions.SumProd
/-- Precomposing `f` with `Prod.fst` is continuous at `(x, y)`  -/
ContinuousAt.fst' : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {x : X} {y : Y}, ContinuousAt f x → ContinuousAt (fun x => f x.1) (x, y)
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- The epimorphism condition on `f`  -/
CategoryTheory.StrongEpi.epi : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P Q : C} {f : P ⟶ Q} [self : CategoryTheory.StrongEpi f],
  CategoryTheory.Epi f
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- `HahnEmbedding.Seed.baseEmbedding` is a partial Hahn embedding.  -/
HahnEmbedding.Seed.isPartial_baseEmbedding : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R) [IsOrderedAddMonoid R],
  HahnEmbedding.IsPartial seed seed.baseEmbedding
-- Mathlib.Topology.UrysohnsLemma
/-- Urysohn's lemma: if `s` and `t` are two disjoint sets in a regular locally compact topological
space `X`, with `s` compact and `t` closed, then there exists a continuous compactly supported
function `f : X → ℝ` such that

* `f` equals one on `s`;
* `f` equals zero on `t`;
* `0 ≤ f x ≤ 1` for all `x`.
 -/
exists_continuous_one_zero_of_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] [LocallyCompactSpace X] {s t : Set X},
  IsCompact s →
    IsClosed t →
      Disjoint s t → ∃ f, Set.EqOn (⇑f) 1 s ∧ Set.EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiff_finsetProd`. -/
contMDiff_finset_prod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n fun x => ∏ i ∈ t, f i x
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.TriggerCondition.continue.injEq : ∀ {ctx : Type u_1} (context context_1 : ctx),
  (Mathlib.TacticAnalysis.TriggerCondition.continue context =
      Mathlib.TacticAnalysis.TriggerCondition.continue context_1) =
    (context = context_1)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- There is an induced injective homomorphism of a subgraph of `G` as
a spanning subgraph into `G`.  -/
SimpleGraph.Subgraph.spanningHom : {V : Type u} → {G : SimpleGraph V} → (x : G.Subgraph) → x.spanningCoe →g G
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `NonUnitalNonAssocRing` across an `Equiv`  -/
Equiv.nonUnitalNonAssocRing : {α : Type u_1} → {β : Type u_2} → α ≃ β → [NonUnitalNonAssocRing β] → NonUnitalNonAssocRing α
-- Mathlib.Algebra.DualNumber
DualNumber.lift_comp_inlHom : ∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  (fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }),
  (DualNumber.lift fe).comp (TrivSqZeroExt.inlAlgHom R A A) = (↑fe).1
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → t.get? k = t.get? k'
-- Mathlib.Data.Opposite
/-- The type-level equivalence between a type and its opposite.  -/
Opposite.equivToOpposite : {α : Sort u} → α ≃ αᵒᵖ
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.cosPoly.eq_def : ∀ (x : ℕ),
  cosPoly✝ x =
    match x with
    | 0 => 0
    | 1 => (Polynomial.monomial 1) (-4)
    | n.succ.succ => (2 * (2 * ↑n + 3)) • cosPoly✝ (n + 1) + (Polynomial.monomial 2) (-4) * cosPoly✝ n
-- Mathlib.Probability.HasLaw
ProbabilityTheory.hasLaw_dirac_iff : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] [MeasurableSingletonClass 𝓧] {x : 𝓧},
  ProbabilityTheory.HasLaw X (MeasureTheory.Measure.dirac x) P ↔ X =ᵐ[P] fun x_1 => x
-- Init.Data.UInt.Bitwise
UInt8.shiftLeft_zero : ∀ {a : UInt8}, a <<< 0 = a
-- Mathlib.Order.Filter.ENNReal
ENNReal.limsup_mul_const_of_ne_top : ∀ {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal},
  a ≠ ⊤ → Filter.limsup (fun x => u x * a) f = a * Filter.limsup u f
-- Init.Data.String.Lemmas.Pattern.Split.Basic
String.Slice.Pattern.toList_splitToSubslice_eq_modelSplit : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {σ : String.Slice → Type}
  [inst_2 : String.Slice.Pattern.ToForwardSearcher pat σ]
  [inst_3 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_4 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id]
  [String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat] (s : String.Slice),
  (s.splitToSubslice pat).toList = String.Slice.Pattern.Model.split pat s.startPos s.startPos ⋯
-- Mathlib.Computability.Primrec.Basic
Primrec.dom_denumerable : ∀ {α : Type u_4} {β : Type u_5} [inst : Denumerable α] [inst_1 : Primcodable β] {f : α → β},
  Primrec f ↔ Nat.Primrec fun n => Encodable.encode (f (Denumerable.ofNat α n))
-- Lean.Server.InfoUtils
Lean.Elab.InfoTree.termGoalAt? : Lean.Elab.InfoTree → String.Pos.Raw → Option Lean.Elab.InfoWithCtx
-- Init.Data.UInt.Lemmas
UInt8.ofNat_lt_iff_lt : ∀ {a b : ℕ}, a < UInt8.size → b < UInt8.size → (UInt8.ofNat a < UInt8.ofNat b ↔ a < b)
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.auxLemmasExt : Lean.EnvExtension Lean.Meta.AuxLemmas
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_ofInt_of_le : ∀ {n : ℤ}, -2 ^ 31 ≤ n → n < 2 ^ 31 → (ISize.ofInt n).toNatClampNeg = n.toNat
-- Mathlib.Tactic.WLOG
Mathlib.Tactic.WLOGResult.mk.injEq : ∀ (reductionGoal : Lean.MVarId) (reductionFVarIds : Lean.FVarId × Lean.FVarId) (hypothesisGoal : Lean.MVarId)
  (hypothesisFVarId : Lean.FVarId) (revertedFVarIds : Array Lean.FVarId) (reductionGoal_1 : Lean.MVarId)
  (reductionFVarIds_1 : Lean.FVarId × Lean.FVarId) (hypothesisGoal_1 : Lean.MVarId) (hypothesisFVarId_1 : Lean.FVarId)
  (revertedFVarIds_1 : Array Lean.FVarId),
  ({ reductionGoal := reductionGoal, reductionFVarIds := reductionFVarIds, hypothesisGoal := hypothesisGoal,
        hypothesisFVarId := hypothesisFVarId, revertedFVarIds := revertedFVarIds } =
      { reductionGoal := reductionGoal_1, reductionFVarIds := reductionFVarIds_1, hypothesisGoal := hypothesisGoal_1,
        hypothesisFVarId := hypothesisFVarId_1, revertedFVarIds := revertedFVarIds_1 }) =
    (reductionGoal = reductionGoal_1 ∧
      reductionFVarIds = reductionFVarIds_1 ∧
        hypothesisGoal = hypothesisGoal_1 ∧ hypothesisFVarId = hypothesisFVarId_1 ∧ revertedFVarIds = revertedFVarIds_1)
-- Mathlib.Data.Rel
Function.graph_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (g : α → β),
  Function.graph (f ∘ g) = (Function.graph g).comp (Function.graph f)
-- Mathlib.Logic.Relation
/-- **Alias** of `refl_iff_eq_le`. -/
reflexive_iff_subrelation_eq : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Refl r ↔ Eq ≤ r
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.measure_eq_tsum' : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ → ∀ (t : Set α), μ t = ∑' (g : G), μ (t ∩ g • s)
-- Mathlib.Tactic.Widget.StringDiagram
/-- The `Expr` presenter for displaying string diagrams.  -/
Mathlib.Tactic.Widget.StringDiagram.stringPresenter : ProofWidgets.ExprPresenter
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.GrothendieckTopology.OneHypercover.cylinder_toPreOneHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  {E : J.OneHypercover S} {F : J.OneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F),
  (CategoryTheory.GrothendieckTopology.OneHypercover.cylinder f g).toPreOneHypercover =
    CategoryTheory.PreOneHypercover.cylinder f g
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The orthocenter lies in the altitudes.  -/
Affine.Triangle.orthocenter_mem_altitude : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ : Fin 3}, t.orthocenter ∈ Affine.Simplex.altitude t i₁
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.jp.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl : Lean.Compiler.LCNF.FunDecl pu) (k : Lean.Compiler.LCNF.Code pu),
  sizeOf (Lean.Compiler.LCNF.Code.jp decl k) = 1 + sizeOf decl + sizeOf k
-- Mathlib.Order.Atoms
isCoatom_dual_iff_isAtom : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, IsCoatom (OrderDual.toDual a) ↔ IsAtom a
-- Init.Data.String.Basic
String.Pos.ofSlice_endPos : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁}, String.Pos.ofSlice (s.slice p₀ p₁ h).endPos = p₁
-- Mathlib.CategoryTheory.Iso
/-- Composition of the two directions of an isomorphism in reverse order
is the identity on the target.  -/
CategoryTheory.Iso.inv_hom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y),
  CategoryTheory.CategoryStruct.comp self.inv self.hom = CategoryTheory.CategoryStruct.id Y
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductCone_pt_map_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) {X Y : C} (f : X ⟶ Y)
  (a : F.obj X × G.obj X),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryProductCone F G).pt.map f)) a =
    ((CategoryTheory.ConcreteCategory.hom (F.map f)) a.1, (CategoryTheory.ConcreteCategory.hom (G.map f)) a.2)
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.ComonadicityInternal.unitFork_pt : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (B : C),
  (CategoryTheory.Comonad.ComonadicityInternal.unitFork adj B).pt = B
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toContinuousLinearMap_symm_lidIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ↑↑(TensorProduct.lidIsometry 𝕜 E).symm = (TensorProduct.mkL 𝕜 𝕜 E) 1
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- For every function, the given argument index  -/
Lean.Elab.WF.GuessLex.MutualMeasure.args : Array ℕ → Lean.Elab.WF.GuessLex.MutualMeasure
-- Batteries.Data.Fin.Coding
/-- Decode `Fin n ⊕ Fin m` from `Fin (n + m)`.  -/
Fin.decodeSum : {n m : ℕ} → Fin (n + m) → Fin n ⊕ Fin m
-- Mathlib.Data.Fin.Tuple.Finset
Finset.card_consEquiv_filter_piFinset : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} (S : (i : Fin (n + 1)) → Finset (α i)) (P : ((i : Fin n) → α i.succ) → Prop)
  [inst : DecidablePred P],
  {r ∈ Fintype.piFinset S | P (Fin.tail r)}.card = (S 0).card * {r ∈ Fintype.piFinset (Fin.tail S) | P r}.card