mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.instMonadBacktrackSavedStateTryTacticM : Lean.MonadBacktrack Lean.Elab.Tactic.SavedState Lean.Elab.Tactic.Try.TryTacticM
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inr_comp_descCochain : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.HomComplex.Cochain L M n) (h : m + 1 = n),
  (↑(CochainComplex.mappingCocone.inr φ)).comp (CochainComplex.mappingCocone.descCochain φ α β h) ⋯ = β
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
intervalIntegral.inv_mul_integral_comp_sub_div : ∀ {a b : ℝ} {f : ℝ → ℝ} (c d : ℝ), c⁻¹ * ∫ (x : ℝ) in a..b, f (d - x / c) = ∫ (x : ℝ) in d - b / c..d - a / c, f x
-- Mathlib.Data.Set.Finite.Lattice
Set.Infinite.iUnion₂ : ∀ {α : Type u} {ι : Sort u_1} {κ : ι → Sort u_2} {s : (i : ι) → κ i → Set α} (i : ι) (j : κ i),
  (s i j).Infinite → (⋃ i, ⋃ j, s i j).Infinite
-- Aesop.Search.Expansion.Norm
Aesop.NormSeqResult.proved.injEq : ∀ (script script_1 : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))),
  (Aesop.NormSeqResult.proved script = Aesop.NormSeqResult.proved script_1) = (script = script_1)
-- Mathlib.FieldTheory.RatFunc.Defs
/-- Induction principle for `K⟮X⟯`: if `f p q : P (RatFunc.mk p q)` for all `p q`,
then `P` holds on all elements of `K⟮X⟯`.

See also `induction_on`, which is a recursion principle defined in terms of `algebraMap`.
 -/
RatFunc.induction_on' : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {P : RatFunc K → Prop} (x : RatFunc K),
  (∀ (p q : Polynomial K), q ≠ 0 → P (RatFunc.mk p q)) → P x
-- Init.Data.List.SplitOn.Lemmas
List.splitOn_eq_singleton : ∀ {α : Type u_1} {xs : List α} [inst : BEq α] [LawfulBEq α] {a : α}, a ∉ xs → List.splitOn a xs = [xs]
-- Init.Data.SInt.Bitwise
Int32.shiftRight_zero : ∀ {a : Int32}, a >>> 0 = a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a fallback : α} {c : ℕ},
  (Std.HashMap.emptyWithCapacity c).getKeyD a fallback = fallback
-- Lean.Attributes
Lean.ParametricAttributeImpl.toAttributeImplCore : {α : Type} → Lean.ParametricAttributeImpl α → Lean.AttributeImplCore
-- Mathlib.NumberTheory.FrobeniusNumber
FrobeniusNumber.eq_1 : ∀ (n : ℕ) (s : Set ℕ), FrobeniusNumber n s = IsGreatest {k | k ∉ AddSubmonoid.closure s} n
-- Init.Data.String.Defs
/-- Decodes an array of bytes that encode a string as [UTF-8](https://en.wikipedia.org/wiki/UTF-8) into
the corresponding string.
 -/
String.fromUTF8 : (a : ByteArray) → a.IsValidUTF8 → String
-- Mathlib.Topology.Constructions
/-- The image of a dense set under `Quotient.mk'` is a dense set.  -/
Dense.quotient : ∀ {X : Type u} [inst : Setoid X] [inst_1 : TopologicalSpace X] {s : Set X}, Dense s → Dense (Quotient.mk' '' s)
-- Mathlib.RingTheory.Ideal.Operations
Submodule.span_singleton_toAddSubgroup_eq_zmultiples : ∀ {M : Type u_1} [inst : AddCommGroup M] (a : M), (ℤ ∙ a).toAddSubgroup = AddSubgroup.zmultiples a
-- Mathlib.NumberTheory.NumberField.Basic
/-- The canonical map from `𝓞 K` to `K` is injective.

This is a convenient abbreviation for `map_ne_zero_iff` applied to
`FaithfulSMul.algebraMap_injective`.
 -/
NumberField.RingOfIntegers.coe_ne_zero_iff : ∀ {K : Type u_1} [inst : Field K] {x : NumberField.RingOfIntegers K},
  (algebraMap (NumberField.RingOfIntegers K) K) x ≠ 0 ↔ x ≠ 0
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.measurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β),
  Measurable ⇑κ
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
AlgebraicTopology.DoldKan.hσ'.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q q_1 : ℕ),
  q = q_1 →
    ∀ (n m : ℕ) (a : AlgebraicTopology.DoldKan.c.Rel m n),
      AlgebraicTopology.DoldKan.hσ' q n m a = AlgebraicTopology.DoldKan.hσ' q_1 n m a
-- Mathlib.Analysis.SpecificLimits.Normed
/-- In a normed ring, the powers of an element x with `‖x‖ < 1` tend to zero.  -/
tendsto_pow_atTop_nhds_zero_of_norm_lt_one : ∀ {R : Type u_2} [inst : SeminormedRing R] {x : R}, ‖x‖ < 1 → Filter.Tendsto (fun n => x ^ n) Filter.atTop (nhds 0)
-- Mathlib.Analysis.Normed.Group.Basic
norm_neg_add : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E), ‖-a + b‖ = ‖a - b‖
-- Mathlib.Algebra.Exact.Basic
/-- **Alias** of the forward direction of `Function.MulExact.iff_monoidHom_rangeRestrict`.

---

Two maps `f : M →* N` and `g : N →* P` are exact if and only if the induced maps
`MonoidHom.range f → N → MonoidHom.range g` are exact.  -/
Function.MulExact.monoidHom_rangeRestrict : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Group M] [inst_1 : Group N] [inst_2 : Group P] {f : M →* N}
  {g : N →* P}, Function.MulExact ⇑f ⇑g → Function.MulExact ⇑f.range.subtype ⇑g.rangeRestrict
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`.  -/
AddEquiv.apply_symm_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) (y : N), e (e.symm y) = y
-- Init.Data.AC
_private.Init.Data.AC.0.Option.isSome.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((val : α) → motive (some val)) → (Unit → motive none) → motive x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf'_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : SemilatticeInf β] (f : α → β), Finset.inf' 1 ⋯ f = f 1
-- Lean.Elab.PreDefinition.FixedParams
/-- If `xs` are arguments to the `funIdx`'s function, pick only the fixed ones, and reorder appropriately.
Expects `xs` to match the arity of the function.
 -/
Lean.Elab.FixedParamPerm.pickFixed : {α : Type u_1} → Lean.Elab.FixedParamPerm → Array α → Array α
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.assoc_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] (ρ : Representation A G V) (σ : Representation A G W)
  (τ : Representation A G U) (v : V) (w : W) (u : U),
  (Representation.TensorProduct.assoc ρ σ τ) (v ⊗ₜ[A] w ⊗ₜ[A] u) = v ⊗ₜ[A] (w ⊗ₜ[A] u)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial_right_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f : MvPolynomial σ R), m.sPolynomial f 0 = 0
-- Mathlib.Analysis.Convex.GaugeRescale
/-- The gauge rescale map `gaugeRescale s t` sends each point `x` to the point `y` on the same ray
that has the same gauge w.r.t. `t` as `x` has w.r.t. `s`.

The characteristic property is satisfied if `gauge t x ≠ 0`, see `gauge_gaugeRescale'`.
In particular, it is satisfied for all `x`,
provided that `t` is absorbent and von Neumann bounded.  -/
gaugeRescale : {E : Type u_1} → [inst : AddCommGroup E] → [Module ℝ E] → Set E → Set E → E → E
-- Mathlib.Logic.Equiv.Basic
Equiv.setValue.eq_1 : ∀ {α : Sort u_1} {β : Sort u_4} [inst : DecidableEq α] (f : α ≃ β) (a : α) (b : β),
  f.setValue a b = Equiv.trans (Equiv.swap a (f.symm b)) f
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- Given a basis of a module `M₁` over a commutative ring `R`, we get an algebra
equivalence between square matrices over `R` indexed by the basis and linear maps `M₁ →ₗ M₁`.  -/
Matrix.toLinAlgEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {n : Type u_4} →
      [inst_1 : Fintype n] →
        [inst_2 : DecidableEq n] →
          {M₁ : Type u_5} →
            [inst_3 : AddCommMonoid M₁] → [inst_4 : Module R M₁] → Module.Basis n R M₁ → Matrix n n R ≃ₐ[R] M₁ →ₗ[R] M₁
-- Mathlib.Topology.Order.DenselyOrdered
nhdsWithin_Iio_neBot' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {b c : α},
  (Set.Iio c).Nonempty → b ≤ c → (nhdsWithin b (Set.Iio c)).NeBot
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.coe_smul : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : SMul M X] [UniformContinuousConstSMul M X] (c : M)
  (x : X), ↑(c • x) = c • ↑x
-- Init.Data.Int.Linear
Int.Internal.Linear.diseq_eq_subst_cert : Int.Internal.Linear.Var → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f)
        (CategoryTheory.Limits.pullback.map
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))
        (CategoryTheory.CategoryStruct.comp i₂
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f i) h))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f)
        (CategoryTheory.Limits.pullback.map
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
      h
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_eq_top_iff' : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) (a : α) (x : γ),
  κ.rnDeriv η a x = ⊤ ↔ x ∈ κ.mutuallySingularSetSlice η a
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.instToString : ToString Std.Http.Header.Name
-- Mathlib.Topology.Separation.Basic
/-- If two sets coincide locally around `x`, except maybe at `y`, then it is equivalent to be
continuous at `x` within one set or the other.  -/
continuousWithinAt_congr_set' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space X] {x : X}
  {s t : Set X} {f : X → Y} (y : X), s =ᶠ[nhdsWithin x {y}ᶜ] t → (ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_addNat_Ioo_addNat : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) ⁻¹' Set.Ioo (i.addNat m) (j.addNat m) = Set.Ioo i j
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.ofRingEquiv_dpow : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] {I : Ideal A} [inst_1 : CommSemiring B] {J : Ideal B}
  {e : A ≃+* B} (h : Ideal.map e I = J) (hI : DividedPowers I) {n : ℕ} {b : B},
  (DividedPowers.ofRingEquiv h hI).dpow n b = e (hI.dpow n (e.symm b))
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.eventuallyEq_coe_comp_ofComplex : ∀ {z : ℂ}, 0 < z.im → UpperHalfPlane.coe ∘ ↑UpperHalfPlane.ofComplex =ᶠ[nhds z] id
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.coe_le_one : ∀ {α : Type u_1} (p : PMF α) (a : α), p a ≤ 1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsGreatest.nnnorm_cfcₙ_nnreal : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_8 : NonnegSpectrumClass ℝ A]
  (f : NNReal → NNReal) (a : A),
  autoParam (ContinuousOn f (quasispectrum NNReal a)) IsGreatest.nnnorm_cfcₙ_nnreal._auto_1 →
    autoParam (f 0 = 0) IsGreatest.nnnorm_cfcₙ_nnreal._auto_3 →
      autoParam (0 ≤ a) IsGreatest.nnnorm_cfcₙ_nnreal._auto_5 → IsGreatest (f '' quasispectrum NNReal a) ‖cfcₙ f a‖₊
-- Mathlib.Order.Bounds.Basic
directedOn_union_iff : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) (s ∪ t) ↔
    DirectedOn (fun x1 x2 => x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun x1 x2 => x1 ≤ x2) t ∧ IsCofinalFor s t
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.comp_familyOfBFamily' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] {o : Ordinal.{u}}
  (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → α) (g : α → β),
  g ∘ Ordinal.familyOfBFamily' r ho f = Ordinal.familyOfBFamily' r ho fun i hi => g (f i hi)
-- Lean.Class
Lean.ClassEntry.mk.inj : ∀ {name : Lean.Name} {outParams outLevelParams : Array ℕ} {name_1 : Lean.Name} {outParams_1 outLevelParams_1 : Array ℕ},
  { name := name, outParams := outParams, outLevelParams := outLevelParams } =
      { name := name_1, outParams := outParams_1, outLevelParams := outLevelParams_1 } →
    name = name_1 ∧ outParams = outParams_1 ∧ outLevelParams = outLevelParams_1
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the arithmetic function `ζ` equals the Riemann Zeta Function on its
domain of convergence `1 < re s`.  -/
ArithmeticFunction.LSeries_zeta_eq_riemannZeta : ∀ {s : ℂ}, 1 < s.re → LSeries (fun n => ↑(ArithmeticFunction.zeta n)) s = riemannZeta s
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.inductionOn : ∀ {C : Type u} {motive : {X Y : CategoryTheory.FreeMonoidalCategory C} → (X ⟶ Y) → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C} (t : X ⟶ Y),
  (∀ (X : CategoryTheory.FreeMonoidalCategory C), motive (CategoryTheory.CategoryStruct.id X)) →
    (∀ (X Y Z : CategoryTheory.FreeMonoidalCategory C),
        motive (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) →
      (∀ (X Y Z : CategoryTheory.FreeMonoidalCategory C),
          motive (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) →
        (∀ (X : CategoryTheory.FreeMonoidalCategory C),
            motive (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) →
          (∀ (X : CategoryTheory.FreeMonoidalCategory C),
              motive (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv) →
            (∀ (X : CategoryTheory.FreeMonoidalCategory C),
                motive (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) →
              (∀ (X : CategoryTheory.FreeMonoidalCategory C),
                  motive (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv) →
                (∀ {X Y Z : CategoryTheory.FreeMonoidalCategory C} (f : X ⟶ Y) (g : Y ⟶ Z),
                    motive f → motive g → motive (CategoryTheory.CategoryStruct.comp f g)) →
                  (∀ (X : CategoryTheory.FreeMonoidalCategory C) {Y Z : CategoryTheory.FreeMonoidalCategory C}
                      (f : Y ⟶ Z), motive f → motive (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)) →
                    (∀ {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X ⟶ Y)
                        (Z : CategoryTheory.FreeMonoidalCategory C),
                        motive f → motive (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)) →
                      motive t
-- Lean.Meta.Sym.ProofInstInfo
/-- Analyzes whether the given free variables (aka arguments) are proofs or instances.
Returns `none` if no arguments are proofs or instances.
 -/
Lean.Meta.Sym.mkProofInstArgInfo? : Array Lean.Expr → Lean.MetaM (Option Lean.Meta.Sym.ProofInstInfo)
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.subpresheafToTypes_obj : ∀ {X : TopCat} {T : ↑X → Type u_1} (P : TopCat.PrelocalPredicate T) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (TopCat.subpresheafToTypes P).obj U = { f // P.pred f }
-- Mathlib.ModelTheory.PartialEquiv
_private.Mathlib.ModelTheory.PartialEquiv.0.FirstOrder.Language.PartialEquiv.le_refl : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.PartialEquiv M N), f ≤ f
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instCommMonoidWithZero : {α : Type u_1} →
  [DecidableEq α] → [inst : CommMonoidWithZero α] → [NoZeroDivisors α] → [Nontrivial α] → CommMonoidWithZero (WithBot α)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_diff_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.Algebra.Order.GroupWithZero.Basic
le_self_pow₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} {n : ℕ} [ZeroLEOneClass M₀]
  [PosMulMono M₀], 1 ≤ a → n ≠ 0 → a ≤ a ^ n
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.comp_of : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Pith B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.CategoryStruct.comp f g).of = CategoryTheory.CategoryStruct.comp f.of g.of
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.subtypeCongr.refl : ∀ {ε : Type u_9} {p : ε → Prop} [inst : DecidablePred p],
  Equiv.Perm.subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a }) = Equiv.refl ε
-- Mathlib.Topology.Category.Stonean.EffectiveEpi
Stonean.effectiveEpi_tfae : ∀ {B X : Stonean} (π : X ⟶ B),
  [CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π,
      Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)].TFAE
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.lift_apply : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] (f : M →ₗ[A] N →ₗ[R] P)
  (a : TensorProduct R M N), (TensorProduct.AlgebraTensorModule.lift f) a = (TensorProduct.lift (↑R f)) a
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.ext_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] {f g : ZeroHom M N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.GroupTheory.NoncommCoprod
AddMonoidHom.noncommCoprod_comp_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)),
  (f.noncommCoprod g comm).comp (AddMonoidHom.inl M N) = f
-- Lean.HeadIndex
Lean.HeadIndex.lit.injEq : ∀ (litVal litVal_1 : Lean.Literal), (Lean.HeadIndex.lit litVal = Lean.HeadIndex.lit litVal_1) = (litVal = litVal_1)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_neg'' : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a : G₀} [PosMulMono G₀], a⁻¹ < 0 ↔ a < 0
-- Mathlib.Data.List.SplitBy
List.splitBy.eq_2 : ∀ {α : Type u} (R : α → α → Bool) (a : α) (as : List α), List.splitBy R (a :: as) = List.splitBy.loop R as a [] []
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.ofList_eq_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)}, Std.ExtDHashMap.Const.ofList l = List.foldl (fun acc p => acc.insert p.1 p.2) ∅ l
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_comp_cancel_right : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₂₃ : R₂ →+* R₃} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃]
  (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₁ →ₛₗ[σ₁₃] M₃), (f ∘ₛₗ ↑e.symm) ∘ₛₗ ↑e = f
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.map_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {X Y : C} (h : CategoryTheory.Retract X Y) (F : CategoryTheory.Functor C D), (h.map F).i = F.map h.i
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Repeatedly reduce while stripping lambda binders and introducing their variables  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.lambdaTelescopeReduce : {m : Type → Type u_1} →
  {α : Type} →
    [Nonempty (m α)] →
      [Monad m] →
        [MonadLiftT Lean.MetaM m] →
          [MonadControlT Lean.MetaM m] →
            Lean.Expr → List Lean.FVarId → (List Lean.FVarId → m α) → (Lean.Expr → List Lean.FVarId → m α) → m α
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.map_shift_unop : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] {X Y : Cᵒᵖ}
  (f : X ⟶ Y) (n : ℤ),
  F.map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F.op n).inv.app Y).unop
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Dᵒᵖ n).map (F.map f.unop).op).unop
        ((CategoryTheory.Functor.commShiftIso F.op n).hom.app X).unop)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.atTop_basis : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] [Nonempty α], Filter.atTop.HasBasis (fun x => True) Set.Ici
-- Std.Tactic.BVDecide.Syntax
/-- The various kinds of configurations offered for the SAT solver.
 -/
Lean.Elab.Tactic.BVDecide.SolverMode : Type
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_id : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], ⇑LieModuleHom.id = id
-- Mathlib.Analysis.Normed.Group.Pointwise
/-- **Alias** of `infEDist_inv`. -/
infEdist_inv : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (x : E) (s : Set E), Metric.infEDist x⁻¹ s = Metric.infEDist x s⁻¹
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.rightTruncate : ℕ → ℤ → optParam Bool false → String
-- Mathlib.Util.AtLocation
/-- Different settings of communicating about a tactic which made no progress:
do nothing (keep silent), print a warning or throw an error.  -/
Mathlib.Tactic.BehaviorIfUnchanged : Type