mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nontrivial.nsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddCancelMonoid α] {s : Finset α},
  s.Nontrivial → ∀ {n : ℕ}, n ≠ 0 → (n • s).Nontrivial
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.continuousOn_cosKernel : ∀ (a : UnitAddCircle), ContinuousOn (HurwitzZeta.cosKernel a) (Set.Ioi 0)
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.ext : ∀ {ι : Type u_1} {x y : ComplexShape ι}, x.Rel = y.Rel → x = y
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmoothOfRelativeDimension_algebraMap : ∀ (n : ℕ) {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  RingHom.IsStandardSmoothOfRelativeDimension n (algebraMap R S) ↔ Algebra.IsStandardSmoothOfRelativeDimension n R S
-- Mathlib.Data.EReal.Operations
/-- Extension for the `positivity` tactic: product of two `EReal`s.  -/
Mathlib.Meta.Positivity.evalERealMul : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.monoidWithZeroHomClass : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S] [IsDomain S]
  [Nontrivial R], MonoidWithZeroHomClass (AbsoluteValue R S) R S
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_toNNReal_iff : ∀ {α : Type u_1} {a : ENNReal} {f : α → ENNReal} {u : Filter α},
  a ≠ ⊤ →
    (∀ (x : α), f x ≠ ⊤) → (Filter.Tendsto (ENNReal.toNNReal ∘ f) u (nhds a.toNNReal) ↔ Filter.Tendsto f u (nhds a))
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_set_biInter : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal]
  [inst_1 : MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set β},
  s.Countable → ∀ {t t' : β → Set α}, (∀ b ∈ s, t b =ᵐ[μ] t' b) → ⋂ b ∈ s, t b =ᵐ[μ] ⋂ b ∈ s, t' b
-- Mathlib.Topology.Order.Basic
/-- A version of `isOpen_Ioi` that doesn't require a `LinearOrder`.  -/
isOpen_Ioi' : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] (a : α), IsOpen (Set.Ioi a)
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.instIsStableUnderRetractsBot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊥.IsStableUnderRetracts
-- Mathlib.Algebra.Group.Irreducible.Lemmas
AddIrreducible.not_even : ∀ {M : Type u_2} [inst : AddMonoid M] {x : M}, AddIrreducible x → ¬Even x
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight.injEq : ∀ (e : Lean.Expr) (isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift) (f g : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η : Mathlib.Tactic.BicategoryLike.Mor₂) (h : Mathlib.Tactic.BicategoryLike.Mor₁) (e_1 : Lean.Expr)
  (isoLift?_1 : Option Mathlib.Tactic.BicategoryLike.IsoLift) (f_1 g_1 : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η_1 : Mathlib.Tactic.BicategoryLike.Mor₂) (h_1 : Mathlib.Tactic.BicategoryLike.Mor₁),
  (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight e isoLift? f g η h =
      Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight e_1 isoLift?_1 f_1 g_1 η_1 h_1) =
    (e = e_1 ∧ isoLift? = isoLift?_1 ∧ f = f_1 ∧ g = g_1 ∧ η = η_1 ∧ h = h_1)
-- Mathlib.SetTheory.Cardinal.Basic
/-- **Alias** of the reverse direction of `Cardinal.lt_aleph0_iff_set_finite`. -/
Set.Finite.lt_aleph0 : ∀ {α : Type u} {S : Set α}, S.Finite → Cardinal.mk ↑S < Cardinal.aleph0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₁ → (t₁ ∩ t₂).getKeyD k fallback = fallback
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.id.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.Mon C), M.id = { hom := CategoryTheory.CategoryStruct.id M.X, isMonHom_hom := ⋯ }
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.ker_eq_maximalIdeal : ∀ {R : Type u_1} {K : Type u_3} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : DivisionRing K] (φ : R →+* K),
  Function.Surjective ⇑φ → RingHom.ker φ = IsLocalRing.maximalIdeal R
-- Mathlib.Order.Atoms
isSimpleOrder_iff_isSimpleOrder_orderDual : ∀ {α : Type u_2} [inst : LE α] [inst_1 : BoundedOrder α], IsSimpleOrder α ↔ IsSimpleOrder αᵒᵈ
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.instIsEquivalenceSheafEtaleSmallEtaleTopologyAffineEtaleTopologySheafPushforwardContinuousSpec_1 : ∀ {S : AlgebraicGeometry.Scheme} {A : Type u'} [inst : CategoryTheory.Category.{u, u'} A]
  [CategoryTheory.Limits.HasLimits A],
  ((AlgebraicGeometry.Scheme.AffineEtale.Spec S).sheafPushforwardContinuous A
      (AlgebraicGeometry.Scheme.AffineEtale.topology S) S.smallEtaleTopology).IsEquivalence
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ \ m₂).get? k = none
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.reduceCyclically.singleton : ∀ {α : Type u} [inst : DecidableEq α] {a : α × Bool}, FreeAddGroup.reduceCyclically [a] = [a]
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.colimitGroup.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat),
  GrpCat.FilteredColimits.colimitGroup F =
    { toMonoid := (GrpCat.FilteredColimits.G F).str, toInv := GrpCat.FilteredColimits.colimitInv F,
      div := DivInvMonoid.div', zpow := zpowRec, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯,
      inv_mul_cancel := ⋯ }
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
/-- The fppf precoverage on the category of schemes. The covering families are jointly-surjective
families of flat morphisms, locally of finite presentation.  -/
AlgebraicGeometry.Scheme.fppfPrecoverage : CategoryTheory.Precoverage AlgebraicGeometry.Scheme
-- Init.Data.Fin.Lemmas
Fin.forall_fin_succ : ∀ {n : ℕ} {P : Fin (n + 1) → Prop}, (∀ (i : Fin (n + 1)), P i) ↔ P 0 ∧ ∀ (i : Fin n), P i.succ
-- Lean.Elab.DeclNameGen
/-- Keeps track of expressions already visited so that we do not include them again.  -/
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.MkNameState.seen : Lean.Elab.Command.NameGen.MkNameState✝ → Lean.ExprSet
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift.congr_simp : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f f_1 : X ⟶ Z) (e_f : f = f_1) (g g_1 : Y ⟶ Z) (e_g : g = g_1)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (H' :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)),
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H' =
    AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f_1 g_1 ⋯
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.self_le_max_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (cmp k ((t.insert k).max ⋯)).isLE = true
-- Mathlib.Analysis.SpecialFunctions.FrullaniIntegral
Frullani.tendsto_integral_inv_smul_nhdsWithin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {L : E}
  [CompleteSpace E],
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    0 < a →
      0 < b →
        Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) (nhds L) →
          Filter.Tendsto (fun ε => ∫ (x : ℝ) in a * ε..b * ε, x⁻¹ • f x) (nhdsWithin 0 (Set.Ioi 0))
            (nhds (Real.log (b / a) • L))
-- Mathlib.NumberTheory.MahlerMeasure
/-- If an integer polynomial has Mahler measure equal to 1, then all its complex nonzero roots are
roots of unity.  -/
Polynomial.pow_eq_one_of_mahlerMeasure_eq_one : ∀ {p : Polynomial ℤ},
  (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure = 1 → ∀ {z : ℂ}, z ≠ 0 → z ∈ p.aroots ℂ → ∃ n, 0 < n ∧ z ^ n = 1
-- Mathlib.LinearAlgebra.Dual.Defs
/-- The `dualRestrict` of a submodule `W` of `M` is the linear map from the
dual of `M` to the dual of `W` such that the domain of each linear map is
restricted to `W`.  -/
Submodule.dualRestrict : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (W : Submodule R M) → Module.Dual R M →ₗ[R] Module.Dual R ↥W
-- Lean.Environment
Lean.getMaxHeight : Lean.Environment → Lean.Expr → UInt32
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.Hom.sub.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'] (f f_1 : P.Hom P'),
  f = f_1 → ∀ (g g_1 : P.Hom P'), g = g_1 → f.sub g = f_1.sub g_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.toList_insert_perm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {k : α} {v : β}, (t.insert k v).toList.Perm ((k, v) :: List.filter (fun x => decide ¬(k == x.1) = true) t.toList)
-- Mathlib.CategoryTheory.Dialectica.Basic
_private.Mathlib.CategoryTheory.Dialectica.Basic.0.CategoryTheory.Dial.termπ₂ : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
/-- Simplification of the integral of `sin x ^ m * cos x ^ n`, case `m` is odd.  -/
integral_sin_pow_odd_mul_cos_pow : ∀ {a b : ℝ} (m n : ℕ),
  ∫ (x : ℝ) in a..b, Real.sin x ^ (2 * m + 1) * Real.cos x ^ n =
    ∫ (u : ℝ) in Real.cos b..Real.cos a, u ^ n * (1 - u ^ 2) ^ m
-- Init.Tactics
/-- The tactic `sleep ms` sleeps for `ms` milliseconds and does nothing.
It is used for debugging purposes only.
 -/
Lean.Parser.Tactic.sleep : Lean.ParserDescr
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMapM.match_1.splitter : {β : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {β' : Type u_1} →
      {f : β → n (Option β')} →
        [inst : MonadAttach n] →
          (out : β) →
            (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) →
              (__do_lift : Subtype (MonadAttach.CanReturn (f out))) →
                ((hf : MonadAttach.CanReturn (f out) none) → motive ⟨none, hf⟩) →
                  ((out' : β') → (hf : MonadAttach.CanReturn (f out) (some out')) → motive ⟨some out', hf⟩) →
                    motive __do_lift
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅}, t.max he ∈ t
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_le_of_mem_supp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, ∀ a ∈ p.support, p.natTrailingDegree ≤ a
-- Init.Data.Fin.Lemmas
Fin.ne_of_gt : ∀ {n : ℕ} {a b : Fin n}, a < b → b ≠ a
-- Mathlib.Order.Hom.CompleteLattice
/-- `sInfHomClass F α β` states that `F` is a type of `⨅`-preserving morphisms.

You should extend this class when you extend `sInfHom`.  -/
sInfHomClass : (F : Type u_8) → (α : Type u_9) → (β : Type u_10) → [InfSet α] → [InfSet β] → [FunLike F α β] → Prop
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.State.insts : Lean.Elab.Tactic.ElimApp.State✝ → Array Lean.MVarId
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `cpop` (population count) on `BitVec`.  -/
BitVec.reduceCpop : Lean.Meta.Simp.DSimproc
-- Mathlib.Logic.Equiv.Embedding
/-- A combination of the above results, allowing us to turn one embedding over a sum type
into two dependent embeddings, the second of which avoids any members of the range
of the first. This is helpful for constructing larger embeddings out of smaller ones.  -/
Equiv.sumEmbeddingEquivSigmaEmbeddingRestricted : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α ⊕ β ↪ γ) ≃ (f : α ↪ γ) × (β ↪ ↑(Set.range ⇑f)ᶜ)
-- Init.Tactics
/-- The `fun_cases` tactic is a convenience wrapper of the `cases` tactic when using a functional
cases principle.

The tactic invocation
```
fun_cases f x ... y ...`
```
is equivalent to
```
cases y, ... using f.fun_cases_unfolding x ...
```
where the arguments of `f` are used as arguments to `f.fun_cases_unfolding` or targets of the case
analysis, as appropriate.

The form
```
fun_cases f
```
(with no arguments to `f`) searches the goal for a unique eligible application of `f`, and uses
these arguments. An application of `f` is eligible if it is saturated and the arguments that will
become targets are free variables.

The form `fun_cases f x y with | case1 => tac₁ | case2 x' ih => tac₂` works like with `cases`.

Under `set_option tactic.fun_induction.unfolding true` (the default), `fun_induction` uses the
`f.fun_cases_unfolding` theorem, which will try to automatically unfold the call to `f` in
the goal. With `set_option tactic.fun_induction.unfolding false`, it uses `f.fun_cases` instead.
 -/
Lean.Parser.Tactic.funCases : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.contains.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.eq) → motive x
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.sumPiEquivProdPi_apply : ∀ (R : Type u_9) [inst : Semiring R] (S : Type u_10) (T : Type u_11) (A : S ⊕ T → Type u_12)
  [inst_1 : (st : S ⊕ T) → AddCommMonoid (A st)] [inst_2 : (st : S ⊕ T) → Module R (A st)],
  ⇑(LinearEquiv.sumPiEquivProdPi R S T A) = ⇑(Equiv.sumPiEquivProdPi A)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.mem_leAddSubgroup_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {γ : Γ₀} {x : R}, x ∈ v.leAddSubgroup γ ↔ v x ≤ γ
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.sumArrowLequivProdArrow_apply_snd : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_5}
  {β : Type u_6} (f : α ⊕ β → M) (b : β), ((LinearEquiv.sumArrowLequivProdArrow α β R M) f).2 b = f (Sum.inr b)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Equivalences between measurable spaces. Main application is the simplification of measurability
statements along measurable equivalences.  -/
MeasurableEquiv : (α : Type u_6) → (β : Type u_7) → [MeasurableSpace α] → [MeasurableSpace β] → Type (max u_6 u_7)
-- Mathlib.LinearAlgebra.Projection
/-- The idempotent endomorphisms of a module with range equal to a submodule are in 1-1
correspondence with linear maps to the submodule that restrict to the identity on the submodule.  -/
Submodule.isIdempotentElemEquiv : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] →
          (p : Submodule R E) → { f // IsIdempotentElem f ∧ LinearMap.range f = p } ≃ { f // ∀ (x : ↥p), f ↑x = x }
-- Mathlib.Topology.Order.Compact
/-- An unordered closed interval is compact.  -/
isCompact_uIcc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [CompactIccSpace α] {a b : α},
  IsCompact (Set.uIcc a b)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_roo_eq_none_iff : ∀ {m n i : ℕ}, (m<...n).toList[i]? = none ↔ n ≤ i + (m + 1)
-- Lean.Elab.Term.TermElabM
/-- Execute `x` without converting errors (i.e., exceptions) to `sorry` applications.
Recall that when `errToSorry = true`, the method `elabTerm` catches exceptions and converts them into `sorry` applications.
 -/
Lean.Elab.Term.withoutErrToSorry : {m : Type → Type u_1} → {α : Type} → [MonadFunctorT Lean.Elab.TermElabM m] → m α → m α
-- Mathlib.Data.Fintype.Fin
Fin.card_filter_val_lt : ∀ {n m : ℕ}, {i | ↑i < m}.card = min n m
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_add_measure_iff : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop} {ν : MeasureTheory.Measure α},
  (∀ᵐ (x : α) ∂μ + ν, p x) ↔ (∀ᵐ (x : α) ∂μ, p x) ∧ ∀ᵐ (x : α) ∂ν, p x
-- Init.Data.Dyadic.Basic
Dyadic.ofOdd.inj : ∀ {n k : ℤ} {hn : n % 2 = 1} {n_1 k_1 : ℤ} {hn_1 : n_1 % 2 = 1},
  Dyadic.ofOdd n k hn = Dyadic.ofOdd n_1 k_1 hn_1 → n = n_1 ∧ k = k_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.isIso_snd_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f f)
-- Mathlib.Data.Bool.Basic
Bool.decide_iff : ∀ (p : Prop) [d : Decidable p], decide p = true ↔ p
-- Mathlib.RingTheory.Polynomial.Chebyshev
/-- Induction principle used for proving facts about Chebyshev polynomials.  -/
Polynomial.Chebyshev.induct : ∀ (motive : ℤ → Prop),
  motive 0 →
    motive 1 →
      (∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)) →
        (∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)) → ∀ (a : ℤ), motive a
-- Mathlib.Analysis.ODE.PicardLindelof
/-- A time-independent, continuously differentiable ODE satisfies the hypotheses of the
Picard-Lindelöf theorem.  -/
IsPicardLindelof.of_contDiffAt_one : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → E} {x₀ : E},
  ContDiffAt ℝ 1 f x₀ →
    ∃ ε, ∃ (hε : 0 < ε), ∃ a r L K, ∃ (_ : 0 < r), ∀ (t₀ : ℝ), IsPicardLindelof (fun x => f) ⟨t₀, ⋯⟩ x₀ a r L K
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableWithinAt_add_const_iff : ∀ {𝕜 : 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] {f : E → F}
  {x : E} {s : Set E} (c : F), DifferentiableWithinAt 𝕜 (fun y => f y + c) s x ↔ DifferentiableWithinAt 𝕜 f s x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_eq_of_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k fallback : α}, k ∈ m → m.getKeyD k fallback = k
-- Init.Data.Ord.Basic
instInhabitedOrdering : Inhabited Ordering
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.InitResults.instAppendInitResults : {α : Type} → Append (Lean.Meta.RefinedDiscrTree.InitResults✝ α)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {a b : F.CoGrothendieck}
  (f g : a ⟶ b) (hfg₁ : f.base = g.base),
  f.fiber = CategoryTheory.CategoryStruct.comp g.fiber (CategoryTheory.eqToHom ⋯) → f = g
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.map_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : CategoryTheory.HasShift D M] {X Y Z : C} {a b c : M}
  (f : CategoryTheory.ShiftedHom X Y a) (g : CategoryTheory.ShiftedHom Y Z b) (h : b + a = c)
  (F : CategoryTheory.Functor C D) [inst_5 : F.CommShift M], (f.comp g h).map F = (f.map F).comp (g.map F) h
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.isTranscendenceBasis_iff : ∀ {ι : Type u} {R : Type u_1} {A : Type w} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Nontrivial R],
  AlgebraicIndependent R x →
    (IsTranscendenceBasis R x ↔
      ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Function.Surjective j)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- If all elements of `s : Set A` commute pairwise and with elements of `star s`, then `adjoin R s`
is a non-unital commutative ring.

See note [reducible non-instances].  -/
NonUnitalStarAlgebra.adjoinNonUnitalCommRingOfComm : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalRing A] →
          [inst_3 : StarRing A] →
            [inst_4 : Module R A] →
              [inst_5 : IsScalarTower R A A] →
                [inst_6 : SMulCommClass R A A] →
                  [inst_7 : StarModule R A] →
                    {s : Set A} →
                      (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) →
                        (∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) →
                          NonUnitalCommRing ↥(NonUnitalStarAlgebra.adjoin R s)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.eval_inv : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (l : Mathlib.Tactic.FieldSimp.NF M), l⁻¹.eval = l.eval⁻¹
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleMk_precomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {X' : C} (g : X' ⟶ X) {p q : ℤ}
  (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q),
  CochainComplex.HomComplex.Cochain.fromSingleMk (CategoryTheory.CategoryStruct.comp g f) h =
    (CochainComplex.HomComplex.Cochain.ofHom ((CochainComplex.singleFunctor C p).map g)).comp
      (CochainComplex.HomComplex.Cochain.fromSingleMk f h) ⋯
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.instIsMonHomOverSchemeSpecOfAsOverHomTransPullbackSymmetryOverInferInstanceOverClassPullbackSpecIso' : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Bialgebra R T],
  CategoryTheory.IsMonHom
    (AlgebraicGeometry.Scheme.Hom.asOver
      (CategoryTheory.Limits.pullbackSymmetry
            (AlgebraicGeometry.Spec (CommRingCat.of T) ↘ AlgebraicGeometry.Spec (CommRingCat.of R))
            (AlgebraicGeometry.Spec (CommRingCat.of S) ↘ AlgebraicGeometry.Spec (CommRingCat.of R)) ≪≫
          AlgebraicGeometry.pullbackSpecIso' R S T).hom
      (AlgebraicGeometry.Spec (CommRingCat.of S)))
-- Init.Data.String.Basic
String.Slice.Pos.ofSlice_lt_ofSlice_iff : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {q r : (s.slice p₀ p₁ h).Pos},
  String.Slice.Pos.ofSlice q < String.Slice.Pos.ofSlice r ↔ q < r
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.norm : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- A fork is a limit cone in `Cᵒᵖ` if and only if the corresponding cofork in `C` is
a colimit cocone.  -/
CategoryTheory.Limits.Fork.isLimitEquivIsColimitUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : Cᵒᵖ} →
      {f g : X ⟶ Y} →
        (c : CategoryTheory.Limits.Fork f g) → CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsColimit c.unop
-- Qq.Macro
Qq.Impl.MVarSynth.synth : Qq.Impl.MVarSynth → Qq.Impl.QuoteM Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.sum_repr_symm : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (v : EuclideanSpace 𝕜 ι),
  ∑ i, v.ofLp i • b i = b.repr.symm v
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_pi_div_two : Real.tan (Real.pi / 2) = 0
-- Std.Data.DHashMap.Raw
/-- Checks whether a key is present in a map, and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.DHashMap.Raw.containsThenInsert : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → (a : α) → β a → Bool × Std.DHashMap.Raw α β