mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.PersistentArray
Lean.PersistentArray.findSomeRevM? : {α : Type u} →
  {m : Type v → Type w} → [Monad m] → {β : Type v} → Lean.PersistentArray α → (α → m (Option β)) → m (Option β)
-- Mathlib.Order.UpperLower.Principal
UpperSet.coe_Ioi : ∀ {α : Type u_1} [inst : Preorder α] (a : α), ↑(UpperSet.Ioi a) = Set.Ioi a
-- Mathlib.Topology.Bases
TopologicalSpace.countable_countableBasis : ∀ (α : Type u) [t : TopologicalSpace α] [inst : SecondCountableTopology α],
  (TopologicalSpace.countableBasis α).Countable
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_id : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), deriv id x = 1
-- Mathlib.CategoryTheory.Core
CategoryTheory.Iso.coreWhiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G H : CategoryTheory.Functor D E} (η : G ≅ H),
  (F.isoWhiskerLeft η).core = F.coreComp G ≪≫ F.core.isoWhiskerLeft η.core ≪≫ (F.coreComp H).symm
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- The additive group homomorphism from `G` to `G/N`.  -/
QuotientAddGroup.mk' : {G : Type u_1} → [inst : AddGroup G] → (N : AddSubgroup G) → [nN : N.Normal] → G →+ G ⧸ N
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionDisabled.fromJson : Lean.Json → Except String Lean.Lsp.CodeActionDisabled
-- Mathlib.Analysis.Convex.SpecificFunctions.Basic
/-- **Bernoulli's inequality** for real exponents, strict version: for `0 < p < 1` and `-1 ≤ s`,
with `s ≠ 0`, we have `(1 + s) ^ p < 1 + p * s`.  -/
rpow_one_add_lt_one_add_mul_self : ∀ {s : ℝ}, -1 ≤ s → s ≠ 0 → ∀ {p : ℝ}, 0 < p → p < 1 → (1 + s) ^ p < 1 + p * s
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The coequalizer condition.  -/
CategoryTheory.IsRegularEpi.w : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.IsRegularEpi f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.left f) f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.right f) f
-- Mathlib.Computability.AkraBazzi.AkraBazzi
AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn : ∀ {p : ℝ},
  p ≠ 0 →
    Asymptotics.IsEquivalent Filter.atTop (deriv fun z => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) fun z =>
      p * z ^ (p - 1)
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.zipWithM'.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List β → Sort u_3) →
      (x : List α) →
        (x_1 : List β) →
          ((x : α) → (xs : List α) → (y : β) → (ys : List β) → motive (x :: xs) (y :: ys)) →
            ((x : List α) →
                (x_2 : List β) →
                  (∀ (x_3 : α) (xs : List α) (y : β) (ys : List β), x = x_3 :: xs → x_2 = y :: ys → False) →
                    motive x x_2) →
              motive x x_1
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.Tree.mk.injEq : ∀ {α : Type u} {β : α → Type v} {size : ℕ} (impl : Std.DTreeMap.Internal.Impl α β) (balanced_impl : impl.Balanced)
  (size_impl : impl.size = size) (impl_1 : Std.DTreeMap.Internal.Impl α β) (balanced_impl_1 : impl_1.Balanced)
  (size_impl_1 : impl_1.size = size),
  ({ impl := impl, balanced_impl := balanced_impl, size_impl := size_impl } =
      { impl := impl_1, balanced_impl := balanced_impl_1, size_impl := size_impl_1 }) =
    (impl = impl_1)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.instDiscreteUniformity : ∀ {α : Type u_1} [inst : UniformSpace α] [DiscreteUniformity α],
  DiscreteUniformity (TopologicalSpace.NonemptyCompacts α)
-- Aesop.Search.Expansion
Aesop.RuleResult.proved : Array Aesop.RappRef → Aesop.RuleResult
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.instSemiring : {R : Type u_1} →
  [inst : Semiring R] → {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → Semiring (OreLocalization S R)
-- Mathlib.Data.Nat.Log
Nat.log_zero_right : ∀ (b : ℕ), Nat.log b 0 = 0
-- Init.Control.Lawful.Basic
Functor.map_map : ∀ {f : Type u_1 → Type u_2} {α β γ : Type u_1} [inst : Functor f] [LawfulFunctor f] (m : α → β) (g : β → γ) (x : f α),
  g <$> m <$> x = (fun a => g (m a)) <$> x
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.swap_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α ↪ β) (x y z : α),
  (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)
-- Mathlib.CategoryTheory.Subfunctor.Finite
/-- A presheaf is "finite" if it is generated by finitely many sections.  -/
CategoryTheory.PresheafIsFinite : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor Cᵒᵖ (Type w) → Prop
-- Mathlib.RingTheory.Filtration
Ideal.mem_iInf_smul_pow_eq_bot_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  [IsNoetherianRing R] [Module.Finite R M] (x : M), x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.rescale_eq_subst : ∀ {R : Type u_2} [inst : CommRing R] (r : R) (f : PowerSeries R),
  (PowerSeries.rescale r) f = PowerSeries.subst (r • PowerSeries.X) f
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.mem_inv_smul_set_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {A : Set β} {a : α} {x : β},
  x ∈ a⁻¹ • A ↔ a • x ∈ A
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_of_mem_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, a ∈ m.insert k v → (k == a) = false → a ∈ m
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instMax : {E : Type u_3} → [inst : AddGroup E] → Max (AddGroupSeminorm E)
-- Lean.Elab.Tactic.ElabTerm
/-- If `allowNaturalHoles == true`, then we allow the resultant expression to contain unassigned "natural" metavariables.
Recall that "natural" metavariables are created for explicit holes `_` and implicit arguments. They are meant to be
filled by typing constraints.
"Synthetic" metavariables are meant to be filled by tactics and are usually created using the synthetic hole notation `?<hole-name>`.  -/
Lean.Elab.Tactic.refineCore : Lean.Syntax → Lean.Name → Bool → Lean.Elab.Tactic.TacticM Unit
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Collector.main : Lean.Meta.FunIndInfo → Lean.MVarId → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Order.Minimal
Maximal.eq_of_superset : ∀ {α : Type u_2} {P : Set α → Prop} {s t : Set α}, Maximal P s → P t → s ⊆ t → t = s
-- Mathlib.Topology.Instances.Sign
instDiscreteTopologySignType : DiscreteTopology SignType
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.property_trans : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] {i j : 𝒰.I₀} (hij : i ⟶ j),
  P (𝒰.trans hij)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.ofList_singleton : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {k : α}, Std.HashSet.Raw.ofList [k] = ∅.insert k
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_inter_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → (m₁.inter m₂).getKey! k = default
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α] {l : List α}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.DHashMap.Const.unitOfList l).getKey! k' = k
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_one : ∀ {α : Type u} [inst : Lean.Grind.Ring α], ↑1 = 1
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_sum_one : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {α : Type u_2} (s : Finset α) (f : α → σ →₀ ℕ),
  (MvPolynomial.monomial (∑ i ∈ s, f i)) 1 = ∏ i ∈ s, (MvPolynomial.monomial (f i)) 1
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiff_finsetSum`. -/
contMDiff_finset_sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n fun x => ∑ i ∈ t, f i x
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestMatchAt_startPos_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat s.startPos endPos ↔
    String.Slice.Pattern.Model.IsLongestMatch pat endPos
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.HorizontalComp.of.injEq : ∀ (η η_1 : Mathlib.Tactic.BicategoryLike.WhiskerRight),
  (Mathlib.Tactic.BicategoryLike.HorizontalComp.of η = Mathlib.Tactic.BicategoryLike.HorizontalComp.of η_1) = (η = η_1)
-- Init.Data.List.Lex
List.lt_asymm : ∀ {α : Type u_1} [inst : LT α] [i : Std.Asymm fun x1 x2 => x1 < x2] {l₁ l₂ : List α}, l₁ < l₂ → ¬l₂ < l₁
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.any_eq_false_iff_forall_mem_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  {p : α → β → Bool}, m.WF → (m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p a (Std.DHashMap.Raw.Const.get m a h) = false)
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.isPrefixOf.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (as : List α) (b : α) (bs : List α)
  (h_1 : (x : List α) → motive [] x) (h_2 : (x : List α) → motive x [])
  (h_3 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)),
  (match a :: as, b :: bs with
    | [], x => h_1 x
    | x, [] => h_2 x
    | a :: as, b :: bs => h_3 a as b bs) =
    h_3 a as b bs
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.numDenom.eq_1 : ∀ {K : Type u} [inst : Field K] (x : RatFunc K),
  x.numDenom =
    x.liftOn'
      (fun p q =>
        if q = 0 then (0, 1)
        else
          have r := gcd p q;
          (Polynomial.C (q / r).leadingCoeff⁻¹ * (p / r), Polynomial.C (q / r).leadingCoeff⁻¹ * (q / r)))
      ⋯
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RciSlice : (α : Type u_1) → (α → Type u_2) → [Ord α] → Type (max u_2 u_1)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.applyAsHom_comm_assoc : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : CommMonoid G] {A B : Rep.{u_1, u, v} k G} (f : A ⟶ B) (g : G)
  {Z : Rep.{u_1, u, v} k G} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (A.applyAsHom g) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (B.applyAsHom g) h)
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.interSmallerFn.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m sofar : Std.DHashMap.Internal.Raw₀ α β) (k : α),
  m.interSmallerFn sofar k =
    match m.getEntry? k with
    | some kv' => sofar.insert kv'.fst kv'.snd
    | none => sofar
-- Init.Data.SInt.Lemmas
Int64.neg_mul_comm : ∀ (a b : Int64), -a * b = a * -b
-- Mathlib.Topology.Category.Profinite.Extend
/-- Given a cone in `Profinite`, consisting of finite sets and indexed by a cofiltered category,
we obtain a functor from the indexing category to `StructuredArrow c.pt toProfinite`.
 -/
Profinite.Extend.functor : {I : Type u} →
  [inst : CategoryTheory.SmallCategory I] →
    {F : CategoryTheory.Functor I FintypeCat} →
      (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) →
        CategoryTheory.Functor I (CategoryTheory.StructuredArrow c.pt FintypeCat.toProfinite)
-- Std.Data.Internal.List.Associative
Std.Internal.List.modifyKey_eq_alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k : α) (f : β k → β k)
  (l : List ((a : α) × β a)),
  Std.Internal.List.modifyKey k f l = Std.Internal.List.alterKey k (fun x => Option.map f x) l
-- Lean.Util.CollectMVars
Lean.Expr.collectMVars : Lean.CollectMVars.State → Lean.Expr → Lean.CollectMVars.State
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The distinguished point of `A` is mapped to the distinguished point of `B`.  -/
CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F}
  (self : A.Hom B), (CategoryTheory.ConcreteCategory.hom (F.map self.val)) A.pt = B.pt
-- Init.Data.List.Lemmas
List.any_eq_true : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, l.any p = true ↔ ∃ x ∈ l, p x = true
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
/-- A filter `f` is measurably generated if each `s ∈ f` includes a measurable `t ∈ f`.  -/
Filter.IsMeasurablyGenerated : {α : Type u_1} → [MeasurableSpace α] → Filter α → Prop
-- Mathlib.Analysis.Normed.Group.Uniform
LocallyLipschitzOn.add : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {f g : α → E}
  {s : Set α}, LocallyLipschitzOn s f → LocallyLipschitzOn s g → LocallyLipschitzOn s fun x => f x + g x
-- Mathlib.Data.Complex.Basic
Complex.im_qsmul : ∀ (q : ℚ) (z : ℂ), (q • z).im = q • z.im
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rootD_rootD : ∀ {self : Batteries.UnionFind} {x : ℕ}, self.rootD (self.rootD x) = self.rootD x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negDblY_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P →
    P 2 ≠ 0 →
      Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 = Q 1 * P 2 → P 1 * Q 2 = W.negY Q * P 2 → W.negDblY P = -W.dblU P
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Polynomial.nthRootsFinset.eq_1 : ∀ (n : ℕ) {R : Type u_1} (a : R) [inst : CommRing R] [inst_1 : IsDomain R],
  Polynomial.nthRootsFinset n a = (Polynomial.nthRoots n a).toFinset
-- Mathlib.Data.Set.Image
Set.range_eq_singleton_iff : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} [Nonempty ι] {y : α}, Set.range f = {y} ↔ ∀ (x : ι), f x = y
-- Lean.Meta.PProdN
/-- `PProd.snd` or `And.right` (using `.proj`)  -/
Lean.Meta.mkPProdSnd : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Topology.Algebra.ConstMulAction
ContinuousAt.const_vadd : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α]
  [inst_3 : TopologicalSpace β] {g : β → α} {b : β}, ContinuousAt g b → ∀ (c : M), ContinuousAt (c +ᵥ g) b
-- Mathlib.Util.TermReduce
/-- `beta% t` elaborates `t` and then if the result is in the form
`f x1 ... xn` where `f` is a (nested) lambda expression,
it will substitute all of its arguments by beta reduction.
This does not recursively do beta reduction, nor will it do
beta reduction of subexpressions.

In particular, `t` is elaborated, its metavariables are instantiated,
and then `Lean.Expr.headBeta` is applied.  -/
Mathlib.Util.TermReduce.betaStx : Lean.ParserDescr
-- Init.Data.UInt.Bitwise
UInt16.toNat_not : ∀ (a : UInt16), (~~~a).toNat = UInt16.size - 1 - a.toNat
-- Init.Data.UInt.Bitwise
instAssociativeUInt32HXor : Std.Associative fun x1 x2 => x1 ^^^ x2
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSubOfPoint_smul : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_4}
  {G : Type u_6} [inst_3 : Group G] [inst_4 : DistribMulAction G V] [SMulCommClass G k V] (s : Finset ι) (w : ι → k)
  (p : ι → V) (b : V) (a : G), (s.weightedVSubOfPoint (a • p) b) w = a • (s.weightedVSubOfPoint p (a⁻¹ • b)) w
-- Mathlib.Computability.Reduce
ManyOneDegree.le_add_right : ∀ (d₁ d₂ : ManyOneDegree), d₂ ≤ d₁ + d₂
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_ofList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.DHashMap.Raw.Const.ofList l).getKey? k' = some k
-- Mathlib.Data.Set.Basic
Set.instInhabited : {α : Type u} → Inhabited (Set α)
-- Mathlib.Algebra.Opposites
AddOpposite.op.eq_1 : ∀ {α : Type u_1}, AddOpposite.op = PreOpposite.op'
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
add_neg_neg_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, b + -a < 0 ↔ b < a
-- Lean.Data.PersistentArray
Lean.PersistentArray.Stats.mk.inj : ∀ {numNodes depth tailSize numNodes_1 depth_1 tailSize_1 : ℕ},
  { numNodes := numNodes, depth := depth, tailSize := tailSize } =
      { numNodes := numNodes_1, depth := depth_1, tailSize := tailSize_1 } →
    numNodes = numNodes_1 ∧ depth = depth_1 ∧ tailSize = tailSize_1
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.mk₀_id_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {n : ℕ} (α : CategoryTheory.Abelian.Ext X Y n),
  (CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.CategoryStruct.id X)).comp α ⋯ = α
-- Mathlib.LinearAlgebra.Dimension.OrzechProperty
linearIndependent_of_top_le_span_of_card_eq_finrank : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [OrzechProperty R] [inst_2 : AddCommMonoid M] [inst_3 : Module R M]
  {ι : Type u_3} [inst_4 : Fintype ι] {b : ι → M},
  ⊤ ≤ Submodule.span R (Set.range b) → Fintype.card ι = Module.finrank R M → LinearIndependent R b
-- Mathlib.Order.Hom.Basic
/-- Transport an `OrderIso` across a pair of `OrderIso`s, by pre- and post-composition.

This is `Equiv.equivCongr`/`RelIso.relIsoCongr` for `OrderIso`.  -/
OrderIso.orderIsoCongr : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      {δ : Type u_5} →
        [inst : LE α] → [inst_1 : LE β] → [inst_2 : LE γ] → [inst_3 : LE δ] → α ≃o γ → β ≃o δ → α ≃o β ≃ (γ ≃o δ)
-- Mathlib.Data.Set.Function
Set.MapsTo.extendDomain : ∀ {α : Type u_1} {β : Type u_2} {p : β → Prop} [inst : DecidablePred p] {f : α ≃ Subtype p} {g : Equiv.Perm α}
  {s t : Set α}, Set.MapsTo (⇑g) s t → Set.MapsTo (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)
-- Mathlib.Data.Sym.Sym2
Sym2.map_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Q : β → Prop} (f : α → β) (g : (b : β) → Q b → γ) (z : Sym2 α)
  (h : ∀ b ∈ Sym2.map f z, Q b), Sym2.pmap g (Sym2.map f z) h = Sym2.pmap (fun a ha => g (f a) ⋯) z ⋯
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.map_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.PreservesMonomorphisms] {X Y : C} (f : Y ⟶ X) [CategoryTheory.Mono f],
  CategoryTheory.Mono (F.map f)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Z : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv)
      (CategoryTheory.ChosenPullbacksAlong.fst (CategoryTheory.CategoryStruct.id X) Z.hom) =
    Z.hom
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_restoreM_trans_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m n o : Type u → Type v} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : (α : Type u) → Std.Internal.Do.WP (o α) α Pred EPred]
  {α : Type u} {post : α → Pred} {epost : EPred} [inst_3 : MonadControl n o] [inst_4 : MonadControlT m n]
  (x : stM m o α),
  Std.Internal.Do.wp (restoreM x) post epost = Std.Internal.Do.wp (MonadControl.restoreM (restoreM x)) post epost
-- Init.Data.Vector.OfFn
Vector.getElem_ofFn : ∀ {i : ℕ} {α : Type u_1} {n : ℕ} {f : Fin n → α} (h : i < n), (Vector.ofFn f)[i] = f ⟨i, h⟩
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_add_left : ∀ {b : ByteArray} {i j : ℕ}, b.extract (i + j) i = ByteArray.empty
-- Mathlib.Topology.Spectral.ConstructibleTopology
IsCompact.isOpen_constructibleTopology_of_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsCompact s → IsOpen s → IsOpen s
-- Mathlib.Algebra.Group.Prod
Prod.instRightCancelSemigroup : {G : Type u_1} → {H : Type u_2} → [RightCancelSemigroup G] → [RightCancelSemigroup H] → RightCancelSemigroup (G × H)
-- Mathlib.Algebra.Colimit.Module
/-- **Alias** of `DirectedSystem.map_self'`. -/
Module.DirectedSystem.map_self : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] ⦃i : ι⦄ (x : F i), (f i i ⋯) x = x
-- Mathlib.Algebra.Algebra.Defs
RingHom.smulOneHom_eq_algebraMap : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  RingHom.smulOneHom = algebraMap R A
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₂_hom_comp_i : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₂ A).hom
      (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.i =
    CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 2) (groupCohomology.cochainsIso₂ A).hom
-- Init.Data.Int.Linear
Int.Internal.Linear.of_var_eq_var_cert.eq_1 : ∀ (x y : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.of_var_eq_var_cert x y p =
    p.beq' (Int.Internal.Linear.Poly.add 1 x (Int.Internal.Linear.Poly.add (-1) y (Int.Internal.Linear.Poly.num 0)))
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_five : Nat.Prime 5
-- Lean.Util.Diff
Lean.Diff.instBEqAction : BEq Lean.Diff.Action
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.measure_subtype_coe_eq_zero_of_comap_eq_zero : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    ∀ {t : Set ↑s}, (MeasureTheory.Measure.comap Subtype.val μ) t = 0 → μ (Subtype.val '' t) = 0
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_finVal : ∀ (n : Fin UInt16.size), UInt16.ofNatLT ↑n ⋯ = UInt16.ofFin n
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.mk.congr_simp : ∀ {α : Type u_4} (vertexSet vertexSet_1 : Set α) (e_vertexSet : vertexSet = vertexSet_1)
  (edgeSet edgeSet_1 : Set (Set α)) (e_edgeSet : edgeSet = edgeSet_1)
  (subset_vertexSet_of_mem_edgeSet' : ∀ ⦃e : Set α⦄, e ∈ edgeSet → e ⊆ vertexSet),
  { vertexSet := vertexSet, edgeSet := edgeSet, subset_vertexSet_of_mem_edgeSet' := subset_vertexSet_of_mem_edgeSet' } =
    { vertexSet := vertexSet_1, edgeSet := edgeSet_1, subset_vertexSet_of_mem_edgeSet' := ⋯ }
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.integral_div_right_eq_self : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure G} [inst_3 : Group G] [MeasurableMul G] [μ.IsMulRightInvariant] (f : G → E) (g : G),
  ∫ (x : G), f (x / g) ∂μ = ∫ (x : G), f x ∂μ