mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_eq_sum_sq : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] [inst_2 : Fintype α] (s t : Finset α),
  s.addEnergy t = ∑ a, {xy ∈ s ×ˢ t | xy.1 + xy.2 = a}.card ^ 2
-- Mathlib.Algebra.BigOperators.Finprod
finprod_cond_nonneg : ∀ {α : Type u_1} {R : Type u_7} [inst : CommSemiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {p : α → Prop}
  {f : α → R}, (∀ (x : α), p x → 0 ≤ f x) → 0 ≤ ∏ᶠ (x : α) (_ : p x), f x
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.beq_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α]
  {m₃ m₄ : Std.HashSet α}, m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ == m₂) = (m₃ == m₄)
-- Init.Control.Lawful.Instances
ExceptT.run_bind : ∀ {m : Type u_1 → Type u_2} {ε α β : Type u_1} [inst : Monad m] (x : ExceptT ε m α) (f : α → ExceptT ε m β),
  (x >>= f).run = do
    let x ← x.run
    match x with
      | Except.ok x => (f x).run
      | Except.error e => pure (Except.error e)
-- Mathlib.Order.Category.BddOrd
BddOrd.forget_map : ∀ {X Y : BddOrd} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget BddOrd).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.NumberTheory.NumberField.Norm
RingOfIntegers.isUnit_norm : ∀ (K : Type u_2) [inst : Field K] {F : Type u_3} [inst_1 : Field F] [inst_2 : Algebra K F] [FiniteDimensional K F]
  [CharZero K] {x : NumberField.RingOfIntegers F}, IsUnit ((RingOfIntegers.norm K) x) ↔ IsUnit x
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.coe_smul : ∀ {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : NormedRing 𝕜] [inst_3 : Module 𝕜 E] [inst_4 : IsBoundedSMul 𝕜 E] (c : 𝕜)
  (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)), ↑(c • f) = c • ↑f
-- Init.Prelude
/-- An [applicative functor](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=monads-and-do) is more powerful than a `Functor`, but
less powerful than a `Monad`.

Applicative functors capture sequencing of effects with the `<*>` operator, overloaded as `seq`, but
not data-dependent effects. The results of earlier computations cannot be used to control later
effects.

Applicative functors should satisfy four laws. Instances of `Applicative` are not required to prove
that they satisfy these laws, which are part of the `LawfulApplicative` class.
 -/
Applicative : (Type u → Type v) → Type (max (u + 1) v)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_rcc : ∀ {m n i fallback : ℕ}, (m...=n).toArray.getD i fallback = if i < n + 1 - m then m + i else fallback
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.coeff_mapDomainLinearMap : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (f : M → N) (x : MonoidAlgebra S M),
  ((MonoidAlgebra.mapDomainLinearMap R S f) x).coeff = Finsupp.mapDomain f x.coeff
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- The data which allows to construct an `E₂`-cohomological spectral sequence
indexed by `ℕ × ℕ` from a spectral object indexed by `EInt`. (Note: additional
assumptions on the spectral object are required for the construction of
the spectral sequence from this.)  -/
CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore EInt
  (fun r => ComplexShape.spectralSequenceNat (r, 1 - r)) 2
-- Batteries.Data.Fin.Basic
/-- `min n m` as an element of `Fin (m + 1)`  -/
Fin.clamp : ℕ → (m : ℕ) → Fin (m + 1)
-- Mathlib.Control.Monad.Cont
ContT.run_bind : ∀ {r : Type u} {m : Type u → Type v} {α β : Type w} (x : ContT r m α) (f : α → ContT r m β) (k : β → m r),
  (x >>= f).run k = x.run fun x => (f x).run k
-- Mathlib.Topology.Compactness.Lindelof
/-- If `p : Set X → Prop` is stable under restriction and union, and each point `x`
of a Lindelöf set `s` has a neighborhood `t` within `s` such that `p t`, then `p s` holds.  -/
IsLindelof.induction_on : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsLindelof s →
    ∀ {p : Set X → Prop},
      (∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s) →
        (∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)) → (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, p t) → p s
-- Init.Data.List.Impl
/-- Tail recursive implementation of `finSomedRev?`. This is only used at runtime.  -/
List.findSomeRev?TR : {α : Type u_1} → {β : Type u_2} → (α → Option β) → List α → Option β
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.forget_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : CategoryTheory.Center C),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Center.forget C) X Y =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Center.forget C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.mul_eq_one_iff : ∀ {α : Type u_1} {σ τ : Equiv.Perm α}, σ.Disjoint τ → (σ * τ = 1 ↔ σ = 1 ∧ τ = 1)
-- Mathlib.Util.CompileInductive
_private.Mathlib.Util.CompileInductive.0.Mathlib.Util.compileStructOnly : Lean.InductiveVal → Lean.RecursorVal → Lean.MetaM Unit
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.prod_factor : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α]
  [CompleteSpace α] {f : β × γ → α}, Multipliable f → ∀ (b : β), Multipliable fun c => f (b, c)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHomotopy_ofEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {φ₁ φ₂ : F ⟶ G} (h : φ₁ = φ₂),
  CochainComplex.HomComplex.Cochain.ofHomotopy (Homotopy.ofEq h) = 0
-- Init.Prelude
Nat.le_antisymm : ∀ {n m : ℕ}, n ≤ m → m ≤ n → n = m
-- Mathlib.Algebra.Group.TypeTags.Basic
/-- If `α` carries some multiplicative structure, then `Additive α` carries the corresponding
additive structure.  -/
Additive : Type u_1 → Type u_1
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_x : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↥(CategoryTheory.Limits.pullback f g)),
  (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).x = (CategoryTheory.Limits.pullback.fst f g) t
-- Qq.Macro
Qq.Impl.mkAbstractedName : Lean.Expr → Qq.Impl.UnquoteM Lean.Name
-- Batteries.Data.Fin.Basic
/-- `findSome? f` returns `f i` for the first `i` for which `f i` is `some _`, or `none` if no such
element is found. The function `f` is not evaluated on further inputs after the first `i` is found.
 -/
Fin.findSome? : {n : ℕ} → {α : Type u_1} → (Fin n → Option α) → Option α
-- Mathlib.Order.Radical
/-- The infimum of all coatoms.

This notion specializes, e.g. in the subgroup lattice of a group to the Frattini subgroup,
or in the lattices of ideals in a ring `R` to the Jacobson ideal.
 -/
Order.radical : (α : Type u_1) → [inst : Preorder α] → [OrderTop α] → [InfSet α] → α
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.submodule_eq : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (v : Projectivization K V), v.submodule = K ∙ v.rep
-- Mathlib.Data.Sum.Interval
Sum.Ico_inr_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (a₂ : α) (b₁ : β), Finset.Ico (Sum.inr b₁) (Sum.inl a₂) = ∅
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tprod_of_add_one_of_neg_add_one : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] [T2Space M] {f : ℤ → M},
  (Multipliable fun n => f (↑n + 1)) →
    (Multipliable fun n => f (-(↑n + 1))) → ∏' (n : ℤ), f n = (∏' (n : ℕ), f (↑n + 1)) * f 0 * ∏' (n : ℕ), f (-(↑n + 1))
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.id_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor SimplexCategory C)
  (X : SimplexCategory), (CategoryTheory.CategoryStruct.id F).app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.GroupTheory.Perm.Cycle.Type
/-- The partition corresponding to a permutation  -/
Equiv.Perm.partition : {α : Type u_1} → [inst : Fintype α] → [DecidableEq α] → Equiv.Perm α → (Fintype.card α).Partition
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.mk.injEq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (points : Fin (n + 1) → P) (independent : AffineIndependent k points)
  (points_1 : Fin (n + 1) → P) (independent_1 : AffineIndependent k points_1),
  ({ points := points, independent := independent } = { points := points_1, independent := independent_1 }) =
    (points = points_1)
-- Mathlib.Computability.DFA
DFA.mk.sizeOf_spec : ∀ {α : Type u} {σ : Type v} [inst : SizeOf α] [inst_1 : SizeOf σ] (step : σ → α → σ) (start : σ) (accept : Set σ),
  sizeOf { step := step, start := start, accept := accept } = 1 + sizeOf start
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) (x : C), G.ι.app x = TypeCat.ofHom fun x_1 => ↑x_1
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toNonUnitalNonAssocRing : {R : Type u} →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : NonUnitalNonAssocRing A] →
        [inst_2 : Module R A] → (S : NonUnitalSubalgebra R A) → NonUnitalNonAssocRing ↥S
-- Mathlib.CategoryTheory.WithTerminal.FinCategory
/-- The equivalence between `Option C` and `WithTerminal C` (they are both the
type `C` plus an extra object `none` or `star`).  -/
CategoryTheory.WithTerminal.optionEquiv : (C : Type u) → Option C ≃ CategoryTheory.WithTerminal C
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.rootSpace_comap_eq_genWeightSpace : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] (χ : ↥H → R),
  LieSubmodule.comap H.incl' (LieAlgebra.rootSpace H χ) = LieModule.genWeightSpace (↥H) χ
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The internal state  -/
Turing.TM2.Cfg.var : {K : Type u_1} → {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → Turing.TM2.Cfg Γ Λ σ → σ
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.instFinalOfHasTerminalOfPreservesLimitDiscretePEmptyEmpty : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F], F.Final
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.unitIso_hom_inv_id_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X : C) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.unit.app X) (CategoryTheory.CategoryStruct.comp (e.unitInv.app X) h) = h
-- Mathlib.Analysis.Complex.Order
Complex.re_eq_norm : ∀ {z : ℂ}, z.re = ‖z‖ ↔ 0 ≤ z
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left)
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R) {Z : C} (h : I.right i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) (CategoryTheory.CategoryStruct.comp (d.proj i) h) =
    CategoryTheory.CategoryStruct.comp (c.proj (J.snd i)) (CategoryTheory.CategoryStruct.comp (I.snd i) h)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.rotateL.eq_2 : ∀ {α : Type u_1} (x : Ordnode α) (x_1 : α), x.rotateL x_1 Ordnode.nil = x.node' x_1 Ordnode.nil
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eval_iterate_derivative_eq_sum : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F},
  Set.InjOn v ↑s →
    ∀ {P : Polynomial F},
      P.degree < ↑s.card →
        ∀ {k : ℕ},
          k < s.card →
            ∀ (x : F),
              Polynomial.eval x ((⇑Polynomial.derivative)^[k] P) =
                ↑k.factorial *
                  ∑ i ∈ s,
                    (Polynomial.eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)) *
                      ∑ t ∈ Finset.powersetCard (s.card - (k + 1)) (s.erase i), ∏ a ∈ t, (x - v a)
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.get!_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited β]
  {m : Std.DHashMap.Raw α fun x => β} (h : m.WF) {a : α},
  Std.DHashMap.Raw.Const.get! m a = Std.DHashMap.Internal.Raw₀.Const.get! ⟨m, ⋯⟩ a
-- Mathlib.Data.Num.Bitwise
/-- Add a bit at the end of a `SNum`. This mimics `NzsNum.bit`.  -/
SNum.«term_::_» : Lean.TrailingParserDescr
-- Init.Data.Order.PackageFactories
Std.LinearOrderPackage.mk : {α : Type u} →
  [toLinearPreorderPackage : Std.LinearPreorderPackage α] →
    (∀ (a b : α), a ≤ b → b ≤ a → a = b) →
      [toMin : Min α] →
        [toMax : Max α] →
          [toLawfulOrderMin : Std.LawfulOrderMin α] →
            [toLawfulOrderMax : Std.LawfulOrderMax α] → Std.LinearOrderPackage α
-- Mathlib.Data.Holor
HolorIndex.drop.eq_1 : ∀ {ds₂ : List ℕ} (x : List ℕ) (x_1 : HolorIndex (x ++ ds₂)), x_1.drop = ⟨List.drop x.length ↑x_1, ⋯⟩
-- Mathlib.Data.Vector.Basic
List.Vector.toList_empty : ∀ {α : Type u_1} (v : List.Vector α 0), v.toList = []
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The canonical map from the underlying set to the prime spectrum of `Γ(X)`.  -/
AlgebraicGeometry.LocallyRingedSpace.toΓSpecFun : (X : AlgebraicGeometry.LocallyRingedSpace) →
  ↑X.toTopCat → PrimeSpectrum ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.self_comp_symm : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  ⇑h ∘ ⇑h.symm = id
-- Init.Data.Array.Lemmas
Array.contains_toList : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α} {x : α}, xs.toList.contains x = xs.contains x
-- Batteries.Data.Fin.Coding
Fin.decodeFun.eq_1 : ∀ {n : ℕ} (x_2 : Fin (n ^ 0)), Fin.decodeFun x_2 = fun x => nomatch x
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.val_algebraMap : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {ΓR : Type u_6}
  {ΓA : Type u_7} [inst_3 : LinearOrderedCommGroupWithZero ΓR] [inst_4 : LinearOrderedCommGroupWithZero ΓA]
  {vR : Valuation R ΓR} {vA : Valuation A ΓA} [inst_5 : vR.HasExtension vA] (r : ↥vR.integer),
  ↑((algebraMap ↥vR.integer ↥vA.integer) r) = (algebraMap R A) ↑r
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_natCast : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  (n : ℕ), ⌈↑n⌉₊ = n
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K K' : ChainComplex C ℕ} (f : K ⟶ K') {Δ Δ' : SimplexCategory} (i : Δ ⟶ Δ') [inst_2 : CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i) (f.f Δ.len) =
    CategoryTheory.CategoryStruct.comp (f.f Δ'.len) (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K' i)
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.inter : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {A B : Set E},
  Balanced 𝕜 A → Balanced 𝕜 B → Balanced 𝕜 (A ∩ B)
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.map_add_right_Ioc : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  [ExistsAddOfLE α] [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Finset.map (addRightEmbedding c) (Finset.Ioc a b) = Finset.Ioc (a + c) (b + c)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.integrable_approxOn_range : ∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  [inst_3 : BorelSpace E] {f : β → E} {μ : MeasureTheory.Measure β} (fmeas : Measurable f)
  [inst_4 : TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})],
  MeasureTheory.Integrable f μ →
    ∀ (n : ℕ), MeasureTheory.Integrable (⇑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n)) μ
-- Mathlib.Topology.LocallyClosed
IsLocallyClosed.image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X},
  IsLocallyClosed s → ∀ {f : X → Y}, Topology.IsInducing f → IsLocallyClosed (Set.range f) → IsLocallyClosed (f '' s)
-- Mathlib.Data.FinEnum
FinEnum.toList.eq_1 : ∀ (α : Type u_1) [inst : FinEnum α], FinEnum.toList α = List.map (⇑FinEnum.equiv.symm) (List.finRange (FinEnum.card α))
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.d_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (j j' : ι₄)
  [inst_20 : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄],
  ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).d j j' =
    HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' +
        HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' +
      HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j'
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.CofibrantObject.HoCat C),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit.app X)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_add_sin_I : ∀ (x : ℂ), Complex.cos x + Complex.sin x * Complex.I = Complex.exp (x * Complex.I)
-- Mathlib.Tactic.Translate.GuessName
/-- This function takes a String and splits it into separate parts based on the following
[naming conventions](https://leanprover-community.github.io/contribute/naming.html).

E.g. `#eval "InvHMulLEConjugate₂SMul_ne_top".splitCase` yields
`["Inv", "HMul", "LE", "Conjugate₂", "SMul", "_", "ne", "_", "top"]`.  -/
Mathlib.Tactic.GuessName.String.splitCase : String → optParam String.Pos.Raw 0 → optParam (List String) [] → List String
-- Mathlib.Order.SuccPred.Limit
WithTop.isSuccLimit_top : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] [NoMaxOrder α], Order.IsSuccLimit ⊤
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- The integral of a continuous function is differentiable on a real set `s`.  -/
intervalIntegral.differentiableOn_integral_of_continuous : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a : ℝ}
  {s : Set ℝ}, Continuous f → DifferentiableOn ℝ (fun u => ∫ (x : ℝ) in a..u, f x) s
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.mul.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] [inst_2 : (i : ι) → Module R (A i)]
  [inst_3 : ∀ (i : ι), SMulCommClass R (A i) (A i)] [inst_4 : ∀ (i : ι), IsScalarTower R (A i) (A i)],
  PiTensorProduct.mul = PiTensorProduct.piTensorHomMap₂ ((PiTensorProduct.tprod R) fun x => LinearMap.mul R (A x))
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchAltViews.containsFVar : Array Lean.Expr → Lean.FVarId → Bool
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.verticalStrip.eq_1 : ∀ (a b : ℝ), Complex.HadamardThreeLines.verticalStrip a b = Complex.re ⁻¹' Set.Ioo a b
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddAbove.inv : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G},
  BddAbove s → BddBelow s⁻¹
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoKernel_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] [inst_3 : CategoryTheory.Limits.HasKernel S.g],
  S.cyclesIsoKernel.inv = S.liftCycles (CategoryTheory.Limits.kernel.ι S.g) ⋯
-- Init.Data.SInt.Lemmas
ISize.toBitVec_inj : ∀ {a b : ISize}, a.toBitVec = b.toBitVec ↔ a = b
-- Mathlib.Algebra.Order.Group.Defs
inv_lt_one_of_one_lt : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a : α}, 1 < a → a⁻¹ < 1
-- Std.Time.Format.Modifier
Std.Time.Modifier.s.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.s presentation) = 1 + sizeOf presentation
-- Mathlib.Tactic.TFAE
/-- Generate a proof of `Chain (· → ·) P l`. We assume `P : Prop` and `l : List Prop`, and that `l`
is an explicit list.  -/
Mathlib.Tactic.TFAE.proveChain : Array (ℕ × ℕ × Lean.Expr) →
  Array Q(Prop) →
    ℕ → List ℕ → (P : Q(Prop)) → (l : Q(List Prop)) → Lean.MetaM Q(List.IsChain (fun x1 x2 => x1 → x2) («$P» :: «$l»))
-- Mathlib.Order.ULift
ULift.instLawfulBOrd_mathlib : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [inst_2 : BEq α] [inst_3 : Ord α] [inst_4 : Std.LawfulBOrd α],
  Std.LawfulBOrd (ULift.{v, u} α)
-- Lean.Elab.Tactic.Basic
/-- Disables automatic fallback of this tactic macro/elaborator to other macros/elaborators of the same
syntax on failure. An elaborator that does not handle the given syntax should still signal this by
throwing `unsupportedSyntax`, which is not affected by this attribute.
 -/
Lean.Elab.Tactic.noFallbackAttr : Lean.TagAttribute
-- Mathlib.Data.QPF.Multivariate.Basic
/-- does `abs` preserve `supp`?  -/
MvQPF.SuppPreservation : {n : ℕ} → {F : TypeVec.{u} n → Type u_1} → [q : MvQPF F] → Prop
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicRing.instIsTorsionFreeCyclotomicField : ∀ (n : ℕ) (A : Type u) (K : Type w) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K],
  Module.IsTorsionFree (CyclotomicRing n A K) (CyclotomicField n K)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_toHomAddUnits : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_8} [inst_1 : AddMonoid M] (f : G →+ M), f.toHomAddUnits.ker = f.ker