mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Homotopy.Equiv
/-- The backward map of a homotopy.

Do NOT use `e.invFun` directly. Use the coercion of `e.symm` instead.  -/
ContinuousMap.HomotopyEquiv.invFun : {X : Type u} →
  {Y : Type v} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → ContinuousMap.HomotopyEquiv X Y → C(Y, X)
-- Mathlib.Data.Num.Basic
ZNum.neg.sizeOf_spec : ∀ (a : PosNum), sizeOf (ZNum.neg a) = 1 + sizeOf a
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.disjoint_iff_add_eq_zero : ∀ {G : Type u_1} [inst : AddGroup G] {H₁ H₂ : AddSubgroup G},
  Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x + y = 0 → x = 0 ∧ y = 0
-- Mathlib.CategoryTheory.Limits.Final
/-- When `F` is final, and `t : Cocone (F ⋙ G)`,
`extendCocone.obj t` is a colimit cocone exactly when `t` is.
 -/
CategoryTheory.Functor.Final.isColimitExtendCoconeEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.Final] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  (t : CategoryTheory.Limits.Cocone (F.comp G)) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Functor.Final.extendCocone.obj t) ≃
                      CategoryTheory.Limits.IsColimit t
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_uint32 : ∀ (x : UInt32), ↑x = ↑x.toNat
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.toIsUniformAddGroup : ∀ {R : Type u} {inst : Ring R} {Γ₀ : outParam (Type v)} {inst_1 : LinearOrderedCommGroupWithZero Γ₀}
  [self : Valued R Γ₀], IsUniformAddGroup R
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.Context.mk.injEq : ∀ (symPrios : Lean.Meta.Grind.SymbolPriorities) (minPrio : ℕ) (symPrios_1 : Lean.Meta.Grind.SymbolPriorities)
  (minPrio_1 : ℕ),
  ({ symPrios := symPrios, minPrio := minPrio } = { symPrios := symPrios_1, minPrio := minPrio_1 }) =
    (symPrios = symPrios_1 ∧ minPrio = minPrio_1)
-- Mathlib.Order.Circular
/-- If `b` is between `a` and `c` and also between `c` and `a`, then at least one pair of points
among `a`, `b`, `c` are identical.  -/
CircularPartialOrder.btw_antisymm : ∀ {α : Type u_1} [self : CircularPartialOrder α] {a b c : α}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = a
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.D₂_totalShift₂XIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁'),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁)
      (K.totalShift₂XIso y n₁ n₁' h₁).hom =
    y.negOnePow •
      CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.continuous_posPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : Fact (1 ≤ p)],
  Continuous fun f => MeasureTheory.Lp.posPart f
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_union_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂).get k ⋯ = m₂.get k mem
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj.map_obj : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [self : P.IsClosedUnderMapObj] {X Y : B} {M : ↑(F.obj X)},
  P.prop X M → ∀ (f : X ⟶ Y), P.prop Y ((F.map f).toFunctor.obj M)
-- Init.Data.String.Iterator
/-- Creates an iterator at the beginning of the string.

This is a no-longer-supported legacy API that will be removed in a future release. You should use
`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
 -/
String.Legacy.mkIterator : String → String.Legacy.Iterator
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel_c₆_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (algebraMap R K) (WeierstrassCurve.integralModel R W).c₆ = W.c₆
-- Mathlib.Data.Rel
SetRel.isRefl_inter : ∀ {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsRefl] [R₂.IsRefl], (R₁ ∩ R₂).IsRefl
-- Mathlib.Data.List.Dedup
List.dedup_nil : ∀ {α : Type u_1} [inst : DecidableEq α], [].dedup = []
-- Init.Data.List.Find
List.IsSuffix.findSome?_eq_none : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f : α → Option β},
  l₁ <:+ l₂ → List.findSome? f l₂ = none → List.findSome? f l₁ = none
-- Mathlib.Order.CompleteBooleanAlgebra
codisjoint_iInf_iff : ∀ {α : Type u} {ι : Sort w} [inst : Order.Coframe α] {a : α} {f : ι → α},
  Codisjoint a (⨅ i, f i) ↔ ∀ (i : ι), Codisjoint a (f i)
-- Std.Http.Test.Helpers
_private.Std.Http.Test.Helpers.0.Std.Http.Internal.Test.withTimeout : {α : Type} → String → ℕ → IO α → IO α
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries_prod`. -/
lowerCentralSeries_prod : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Group G₁] [inst_1 : Group G₂] (S₁ : Subgroup G₁) (S₂ : Subgroup G₂) (n : ℕ),
  (S₁.prod S₂).lowerCentralSeries n = (S₁.lowerCentralSeries n).prod (S₂.lowerCentralSeries n)
-- Init.Data.List.Impl
List.zipIdx.eq_def : ∀ {α : Type u} (x : List α) (x_1 : ℕ),
  x.zipIdx x_1 =
    match x, x_1 with
    | [], x => []
    | x :: xs, n => (x, n) :: xs.zipIdx (n + 1)
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_set_mk : ∀ {G : Type u_1} [inst : Group G] {s : Submonoid G} (h_inv : ∀ {x : G}, x ∈ s.carrier → x⁻¹ ∈ s.carrier),
  ↑{ toSubmonoid := s, inv_mem' := h_inv } = ↑s
-- Mathlib.Data.Nat.Pairing
Nat.surjective_unpair : Function.Surjective Nat.unpair
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instPreorder : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → Preorder (WithVal v)
-- Mathlib.ModelTheory.Definability
Set.DefinableFun.of_empty : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u_2} {A : Set M} {f : (α → M) → M},
  Set.DefinableFun L ∅ f → Set.DefinableFun L A f
-- Mathlib.RingTheory.Radical.NatInt
UniqueFactorizationMonoid.primeFactors_eq_primeFactors_natAbs : ∀ {z : ℤ}, UniqueFactorizationMonoid.primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors
-- Mathlib.Analysis.Complex.Poisson
_private.Mathlib.Analysis.Complex.Poisson.0.DiffContOnCl.circleAverage_re_smul_on_ball_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {w : ℂ} [CompleteSpace E],
  DiffContOnCl ℂ f (Metric.ball 0 R) →
    w ∈ Metric.ball 0 R → Real.circleAverage (fun z => ((z + w) / (z - w)).re • f z) 0 R = f w
-- Mathlib.Data.Finsupp.MonomialOrder
/-- **Alias** of `MonomialOrder.isOrderedCancelAddMonoid_syn`. -/
MonomialOrder.iocam : ∀ {σ : Type u_1} (m : MonomialOrder σ), IsOrderedCancelAddMonoid m.syn
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] {c : CategoryTheory.Limits.Cone F}
  (hc : CategoryTheory.Limits.IsLimit c) (j : J),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.isLimit F).conePointUniqueUpToIso hc).inv
      (CategoryTheory.Limits.limit.π F j) =
    c.π.app j
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Formula for `sinZeta` as a Dirichlet series in the convergence range, with sum over `ℕ`.  -/
HurwitzZeta.hasSum_nat_sinZeta : ∀ (a : ℝ) {s : ℂ}, 1 < s.re → HasSum (fun n => ↑(Real.sin (2 * Real.pi * a * ↑n)) / ↑n ^ s) (HurwitzZeta.sinZeta (↑a) s)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Viewing a module as an affine space modelled on itself, a `weightedVSub` is just a linear
combination.  -/
Finset.weightedVSub_eq_linear_combination : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_6}
  (s : Finset ι) {w : ι → k} {p : ι → V}, s.sum w = 0 → (s.weightedVSub p) w = ∑ i ∈ s, w i • p i
-- Mathlib.Probability.Kernel.WithDensity
/-- Kernel with image `(κ a).withDensity (f a)` if `Function.uncurry f` is measurable, and
with image 0 otherwise. If `Function.uncurry f` is measurable, it satisfies
`∫⁻ b, g b ∂(withDensity κ f hf a) = ∫⁻ b, f a b * g b ∂(κ a)`.  -/
ProbabilityTheory.Kernel.withDensity : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        (κ : ProbabilityTheory.Kernel α β) →
          [ProbabilityTheory.IsSFiniteKernel κ] → (α → β → ENNReal) → ProbabilityTheory.Kernel α β
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.coordinate_eval_5 : ∀ {a0 a1 a2 a3 a4 a5 : ℤ} {t : List ℤ},
  (Lean.Omega.LinearCombo.coordinate 5).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: t)) = a5
-- Mathlib.MeasureTheory.Measure.Dirac
/-- **Alias** of the reverse direction of `MeasureTheory.ext_iff_measureReal_singleton`. -/
MeasureTheory.Measure.ext_of_measureReal_singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Countable α] {μ1 μ2 : MeasureTheory.Measure α}
  [MeasureTheory.SigmaFinite μ1] [MeasureTheory.SigmaFinite μ2], (∀ (x : α), μ1.real {x} = μ2.real {x}) → μ1 = μ2
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_sub : ∀ {a b : ℕ} (ha : a < 2 ^ 32) (hab : b ≤ a), UInt32.ofNatLT (a - b) ⋯ = UInt32.ofNatLT a ha - UInt32.ofNatLT b ⋯
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.mulMon' : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Mon → optParam (Option ℕ) none → Lean.Grind.CommRing.Poly
-- Mathlib.Order.Lattice
sup_inf_le : ∀ {α : Type u} [inst : Lattice α] {a b c : α}, a ⊔ b ⊓ c ≤ (a ⊔ b) ⊓ (a ⊔ c)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.mk : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_6} →
                      [inst_6 : TopologicalSpace H'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {M : Type u_9} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_10} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {n : WithTop ℕ∞} →
                                          (toEquiv : M ≃ M') →
                                            ContMDiff I I' n ⇑toEquiv →
                                              ContMDiff I' I n ⇑toEquiv.symm → Diffeomorph I I' M M' n
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.push.injEq : ∀ (k : Turing.PartrecToTM2.K') (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ')
  (q : Turing.PartrecToTM2.Λ') (k_1 : Turing.PartrecToTM2.K')
  (s_1 : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') (q_1 : Turing.PartrecToTM2.Λ'),
  (Turing.PartrecToTM2.Λ'.push k s q = Turing.PartrecToTM2.Λ'.push k_1 s_1 q_1) = (k = k_1 ∧ s = s_1 ∧ q = q_1)
-- Mathlib.CategoryTheory.Limits.Sifted
/-- A sifted category is connected.  -/
CategoryTheory.IsSifted.instIsConnected : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsSifted C], CategoryTheory.IsConnected C
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.linkTarget.notRefEnd : Lean.Parser.ParserFn
-- Mathlib.Algebra.Group.Hom.Defs
/-- The identity map from a type with multiplication to itself.  -/
MulHom.id : (M : Type u_10) → [inst : Mul M] → M →ₙ* M
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_X_pow_add_C : ∀ {R : Type u} (a : R) [inst : Semiring R] {n : ℕ}, n ≠ 0 → (Polynomial.X ^ n + Polynomial.C a).Monic
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instIsOrderedAddMonoidCastInt : ∀ {d : ℕ}, IsOrderedAddMonoid (ℤ√↑d)
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- If `G ≤ H` then `G.degree v ≤ H.degree v` for any vertex `v`.  -/
SimpleGraph.degree_le_of_le : ∀ {V : Type u_1} {G : SimpleGraph V} {v : V} [inst : Fintype ↑(G.neighborSet v)] {H : SimpleGraph V}
  [inst_1 : Fintype ↑(H.neighborSet v)], G ≤ H → G.degree v ≤ H.degree v
-- Lean.Expr
/-- Return `true` if the given expression is a projection `.proj ..`  -/
Lean.Expr.isProj : Lean.Expr → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
/-- The (simplicial) chain complex of a simplicial set `X` with
coefficients in `R : C`. Its homology is the simplicial homology
of `X`.  -/
SSet.chainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] → [inst_2 : CategoryTheory.Preadditive C] → SSet → C → ChainComplex C ℕ
-- Mathlib.Analysis.Complex.Exponential
Real.exp_list_sum : ∀ (l : List ℝ), Real.exp l.sum = (List.map Real.exp l).prod
-- Mathlib.Algebra.Ring.GeomSum
op_geom_sum₂ : ∀ {R : Type u_1} [inst : Semiring R] (x y : R) (n : ℕ),
  ∑ i ∈ Finset.range n, MulOpposite.op y ^ (n - 1 - i) * MulOpposite.op x ^ i =
    ∑ i ∈ Finset.range n, MulOpposite.op y ^ i * MulOpposite.op x ^ (n - 1 - i)
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Turn an element of a type `F` satisfying `AddEquivClass F α β` into an actual
`AddEquiv`. This is declared as the default coercion from `F` to `α ≃+ β`.  -/
AddEquivClass.toAddEquiv : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} → [inst : EquivLike F α β] → [inst_1 : Add α] → [inst_2 : Add β] → [AddEquivClass F α β] → F → α ≃+ β
-- Lean.Parser.Term
Lean.Parser.Term.scoped.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Multiset.Bind
Multiset.sum_join : ∀ {α : Type u_1} [inst : AddCommMonoid α] {S : Multiset (Multiset α)}, S.join.sum = (Multiset.map Multiset.sum S).sum
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E}
  (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented) (x : E),
  (↑(HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker) x).1 = f x
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁.eq_6 : ∀ (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.trStmts₁ q.succ =
    insert q.succ (insert (Turing.PartrecToTM2.unrev q) (Turing.PartrecToTM2.trStmts₁ q))
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_self_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x : E}, inner 𝕜 x x = 0 ↔ x = 0
-- Mathlib.Topology.Order.ScottTopology
Topology.IsLower.scottHausdorff_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α],
  Topology.scottHausdorff α Set.univ ≤ inst_1
-- Lean.Elab.Do.Basic
Lean.Elab.Do.mapTermElabM : ({α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α) →
  {α : Type} → Lean.Elab.Do.DoElabM α → Lean.Elab.Do.DoElabM α
-- Init.Core
ne_false_of_self : ∀ {p : Prop}, p → p ≠ False
-- Mathlib.Order.WithBot
WithTop.decidableLT.eq_2 : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] (a_1 : α), WithTop.decidableLT (some a_1) none = isTrue ⋯
-- Mathlib.Algebra.Lie.Quotient
/-- Two `LieModuleHom`s from a quotient lie module are equal if their compositions with
`LieSubmodule.Quotient.mk'` are equal.

See note [partially-applied ext lemmas].  -/
LieSubmodule.Quotient.lieModuleHom_ext : ∀ {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] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  [inst_6 : LieModule R L M] ⦃f g : M ⧸ N →ₗ⁅R,L⁆ M⦄,
  f.comp (LieSubmodule.Quotient.mk' N) = g.comp (LieSubmodule.Quotient.mk' N) → f = g
-- Init.Prelude
/-- The Boolean value `false`, not to be confused with the proposition `False`.  -/
Bool.false : Bool
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat : ∀ {k : ℕ} {x : ℝ},
  k ≠ 0 →
    x ∈ Set.Icc 0 1 →
      HurwitzZeta.hurwitzZetaOdd (↑x) (-(2 * ↑k)) =
        -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
-- Init.Data.SInt.Bitwise
Int8.xor_not : ∀ {a b : Int8}, a ^^^ ~~~b = ~~~(a ^^^ b)
-- Batteries.Data.ByteArray
ByteArray.data_copySlice : ∀ (a : ByteArray) (i : ℕ) (b : ByteArray) (j len : ℕ) (exact : Bool),
  (a.copySlice i b j len exact).data =
    b.data.extract 0 j ++ a.data.extract i (i + len) ++ b.data.extract (j + min len (a.data.size - i))
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- Given a sequence `L = [ i 0, ..., i b ]`, `standardσ m L` i is the morphism
`σ (i b) ≫ … ≫ σ (i 0)`. The construction is provided for any list of natural numbers,
but it is intended to behave well only when the list is admissible.  -/
SimplexCategoryGenRel.standardσ : (L : List ℕ) → {m₁ m₂ : ℕ} → m₂ + L.length = m₁ → (SimplexCategoryGenRel.mk m₁ ⟶ SimplexCategoryGenRel.mk m₂)
-- Init.Data.Format.Basic
Std.Format.append.sizeOf_spec : ∀ (a a_1 : Std.Format), sizeOf (a.append a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.ModelTheory.Semantics
/-- A special case of `realize_restrictVarLeft`, included because we can add the `simp` attribute
to it  -/
FirstOrder.Language.Term.realize_restrictVarLeft' : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} [inst_1 : DecidableEq α] {γ : Type u_4}
  {t : L.Term (α ⊕ γ)} {s : Set α} (h : ↑t.varFinsetLeft ⊆ s) {v : α → M} {xs : γ → M},
  FirstOrder.Language.Term.realize (Sum.elim (v ∘ Subtype.val) xs) (t.restrictVarLeft (Set.inclusion h)) =
    FirstOrder.Language.Term.realize (Sum.elim v xs) t
-- Lean.Environment
Lean.ModuleData.mk.injEq : ∀ (isModule : Bool) (imports : Array Lean.Import) (constNames : Array Lean.Name) (constants : Array Lean.ConstantInfo)
  (extraConstNames : Array Lean.Name) (entries : Array (Lean.Name × Array Lean.EnvExtensionEntry)) (isModule_1 : Bool)
  (imports_1 : Array Lean.Import) (constNames_1 : Array Lean.Name) (constants_1 : Array Lean.ConstantInfo)
  (extraConstNames_1 : Array Lean.Name) (entries_1 : Array (Lean.Name × Array Lean.EnvExtensionEntry)),
  ({ isModule := isModule, imports := imports, constNames := constNames, constants := constants,
        extraConstNames := extraConstNames, entries := entries } =
      { isModule := isModule_1, imports := imports_1, constNames := constNames_1, constants := constants_1,
        extraConstNames := extraConstNames_1, entries := entries_1 }) =
    (isModule = isModule_1 ∧
      imports = imports_1 ∧
        constNames = constNames_1 ∧ constants = constants_1 ∧ extraConstNames = extraConstNames_1 ∧ entries = entries_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A convenience function for `ReflectsColimit`, which takes the functor as an explicit argument to
guide typeclass resolution.
 -/
CategoryTheory.Limits.isColimitOfReflects : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              (F : CategoryTheory.Functor C D) →
                {c : CategoryTheory.Limits.Cocone K} →
                  CategoryTheory.Limits.IsColimit (F.mapCocone c) →
                    [CategoryTheory.Limits.ReflectsColimit K F] → CategoryTheory.Limits.IsColimit c
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Reorder a sum.

The difference with `Finset.sum_bij` is that the bijection is specified with an inverse, rather than
as a surjective injection.

The difference with `Finset.sum_nbij'` is that the bijection and its inverse are allowed to use
membership of the domains of the sums, rather than being non-dependent functions.  -/
Finset.sum_bij' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (i : (a : ι) → a ∈ s → κ) (j : (a : κ) → a ∈ t → ι) (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t)
  (hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s),
  (∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a) →
    (∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a) →
      (∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) → ∑ x ∈ s, f x = ∑ x ∈ t, g x
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
/-- The preimage of a finite-index normal subgroup under a group homomorphism.  -/
FiniteIndexNormalSubgroup.comap : {G : Type u_1} →
  [inst : Group G] →
    {H : Type u_2} → [inst_1 : Group H] → (G →* H) → FiniteIndexNormalSubgroup H → FiniteIndexNormalSubgroup G
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The completed L-function of a non-trivial Dirichlet character is differentiable everywhere.  -/
DirichletCharacter.differentiable_completedLFunction : ∀ {N : ℕ} [inst : NeZero N] {χ : DirichletCharacter ℂ N},
  χ ≠ 1 → Differentiable ℂ (DirichletCharacter.completedLFunction χ)
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- Let `T / S / R` be a tower of algebras, `p, P, I` be ideals in `R, S, T`, respectively,
and `p` and `P` are maximal. If `p = P ∩ S` and `P = I ∩ S`,
then `f (I | p) = f (P | p) * f (I | P)`.  -/
Ideal.inertiaDeg'_algebra_tower : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [IsScalarTower R S T] (p : Ideal R) (P : Ideal S)
  (I : Ideal T) [p.IsMaximal] [P.IsMaximal] [P.LiesOver p] [I.LiesOver P],
  p.inertiaDeg' I = p.inertiaDeg' P * P.inertiaDeg' I
-- Batteries.Data.List.Lemmas
List.countBefore_cons_succ_of_not_beq : ∀ {α : Type u_1} {x : α} {xs : List α} {i : ℕ} [inst : BEq α] {a : α},
  (a == x) = false → List.countBefore x (a :: xs) (i + 1) = List.countBefore x xs i
-- Mathlib.Data.List.Basic
List.forall_mem_iff_get : ∀ {α : Type u} {l : List α} {p : α → Prop}, (∀ x ∈ l, p x) ↔ ∀ (i : Fin l.length), p (l.get i)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_rightUnitor_hom_snd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {a b : B × C}
  (f : a ⟶ b), (CategoryTheory.Bicategory.rightUnitor f).hom.2 = (CategoryTheory.Bicategory.rightUnitor f.2).hom
-- Mathlib.Tactic.NormNum.Prime
/-- The `norm_num` extension which identifies expressions of the form `Nat.Prime n`.  -/
Mathlib.Meta.NormNum.evalNatPrime : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.orderOf : ∀ {α : Type u_2} {f : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α], f.IsCycle → orderOf f = f.support.card