mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Covering.Basic
/-- Proposition 1.34 of [hatcher02].  -/
IsCoveringMap.eq_of_comp_eq : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f →
    ∀ {A : Type u_3} [inst_2 : TopologicalSpace A] {g₁ g₂ : A → E} [PreconnectedSpace A],
      Continuous g₁ → Continuous g₂ → f ∘ g₁ = f ∘ g₂ → ∀ (a : A), g₁ a = g₂ a → g₁ = g₂
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeffs_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.coeffs 0 = ∅
-- Init.Data.List.Impl
List.find?.eq_1 : ∀ {α : Type u} (p : α → Bool), List.find? p [] = none
-- Mathlib.Algebra.Group.Basic
add_sub_cancel_left : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a + b - a = b
-- Mathlib.Topology.Clopen
isClopen_iInter_of_finite : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Sort u_2} [Finite Y] {s : Y → Set X},
  (∀ (i : Y), IsClopen (s i)) → IsClopen (⋂ i, s i)
-- Mathlib.Data.Nat.Dist
Nat.eq_of_dist_eq_zero : ∀ {n m : ℕ}, n.dist m = 0 → n = m
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.hasLimitsOfSize : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, u₁} A]
  [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} B]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₂, v₃, u₂, u₃} R],
  CategoryTheory.Limits.HasLimitsOfSize.{w, w', max v₁ v₂, max (max u₂ u₁) v₃} (CategoryTheory.Comma L R)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.var : Lean.Grind.CommRing.Var → Lean.Grind.CommRing.Expr
-- Mathlib.Algebra.Group.Conj
ConjClasses.eq_1 : ∀ (α : Type u_1) [inst : Monoid α], ConjClasses α = Quotient (IsConj.setoid α)
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- An orthonormal basis, indexed by `Fin n`, with the given orientation.  -/
Orientation.finOrthonormalBasis : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      {n : ℕ} → 0 < n → Module.finrank ℝ E = n → Orientation ℝ E (Fin n) → OrthonormalBasis (Fin n) ℝ E
-- Mathlib.Analysis.Normed.Module.Bases
/-- The projection at `0` is the zero map.  -/
SchauderBasis.proj_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X), b.proj 0 = 0
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.principalOpen.congr_simp : ∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] (x x_1 : X),
  x = x_1 → Alexandrov.principalOpen x = Alexandrov.principalOpen x_1
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_map_erase : ∀ {ι : Type u_2} {M : Type u_5} [inst : CommMonoid M] {m : Multiset ι} {f : ι → M} [inst_1 : DecidableEq ι] {a : ι},
  a ∈ m → f a * (Multiset.map f (m.erase a)).prod = (Multiset.map f m).prod
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Param.binderName : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Param pu → Lean.Name
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α], Lex.instAddCommMonoid = { toAddMonoid := Lex.instAddMonoid, add_comm := ⋯ }
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.coe_one : ∀ (M : Type u_4) [inst : MulOne M], ⇑1 = id
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_self_removeNth : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (f : (j : Fin (n + 1)) → α j),
  p.insertNth (f p) (p.removeNth f) = f
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_sum_eq_of_linearIndepOn : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommRing R] {A : Type u_1} [inst_1 : CommRing A]
  [inst_2 : Algebra R A] {f : ι → Polynomial R} {v : ι → A},
  LinearIndepOn R v ↑s →
    (∑ i ∈ s, v i • Polynomial.map (algebraMap R A) (f i)).natDegree = s.sup fun i => (f i).natDegree
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.normedCommGroup : {E : Type u_2} → [NormedCommGroup E] → NormedCommGroup (ULift.{u_5, u_2} E)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_insert_natCast : ∀ {R : Type u} [inst : NonAssocRing R] (n : ℕ) (s : Set R), Subring.closure (insert (↑n) s) = Subring.closure s
-- Mathlib.LinearAlgebra.Dimension.Torsion.Basic
/-- Quotienting an additive commutative group by its torsion subgroup does not change its
`ℤ`-`finrank`.  -/
finrank_quotient_torsion_eq : ∀ {M : Type u_1} [inst : AddCommGroup M],
  Module.finrank ℤ (M ⧸ AddSubgroup.toIntSubmodule (AddCommGroup.torsion M)) = Module.finrank ℤ M
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_insert_of_notMem : ∀ {α : Type u_1} {s t : Set α} {a : α}, a ∉ s → s \ insert a t = s \ t
-- Mathlib.RingTheory.LocalIso
Algebra.IsLocalIso.iff_of_algEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {T : Type u_3}
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T), Algebra.IsLocalIso R S ↔ Algebra.IsLocalIso R T
-- Lean.ExtraModUses
/-- Records the module of the given declaration as an additional import dependency for the current
module, using `Environment.isExporting` as the visibility level. If the declaration itself is
already `meta`, the module dependency is recorded as a non-`meta` dependency.
 -/
Lean.recordExtraModUseFromDecl : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadTrace m] →
        [Lean.MonadOptions m] → [Lean.MonadRef m] → [Lean.AddMessageContext m] → Lean.Name → Bool → m Unit
-- Mathlib.Topology.Connected.Basic
PreirreducibleSpace.preconnectedSpace : ∀ (α : Type u) [inst : TopologicalSpace α] [PreirreducibleSpace α], PreconnectedSpace α
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.brecOn_2.eq : ∀ {motive_1 : Mathlib.Tactic.Translate.ArgReorder → Sort u}
  {motive_2 : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u}
  {motive_3 : List (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u}
  {motive_4 : ℕ × Mathlib.Tactic.Translate.ArgReorder → Sort u} (t : List (ℕ × Mathlib.Tactic.Translate.ArgReorder))
  (F_1 : (t : Mathlib.Tactic.Translate.ArgReorder) → t.below → motive_1 t)
  (F_2 :
    (t : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)) → Mathlib.Tactic.Translate.ArgReorder.below_1 t → motive_2 t)
  (F_3 :
    (t : List (ℕ × Mathlib.Tactic.Translate.ArgReorder)) → Mathlib.Tactic.Translate.ArgReorder.below_2 t → motive_3 t)
  (F_4 : (t : ℕ × Mathlib.Tactic.Translate.ArgReorder) → Mathlib.Tactic.Translate.ArgReorder.below_3 t → motive_4 t),
  Mathlib.Tactic.Translate.ArgReorder.brecOn_2 t F_1 F_2 F_3 F_4 =
    F_3 t (Mathlib.Tactic.Translate.ArgReorder.brecOn_2.go t F_1 F_2 F_3 F_4).2
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.mul_invOfUnit : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] (φ : MvPowerSeries σ R) (u : Rˣ),
  MvPowerSeries.constantCoeff φ = ↑u → φ * φ.invOfUnit u = 1
-- Mathlib.Order.SuccPred.Tree
IsPredArchimedean.isAtom_findAtom : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] [inst_3 : OrderBot α]
  [inst_4 : DecidableEq α] {r : α}, r ≠ ⊥ → IsAtom (IsPredArchimedean.findAtom r)
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd_apply : ∀ (X Y : Type u) (x : X ⨯ Y),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.binaryProductIso X Y).hom) x).2 =
    (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd) x
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.eq_liftNC : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {R : Type u_5} [inst_1 : NonUnitalNonAssocSemiring R]
  (f : k →+ R) (g : G → R) (l : SkewMonoidAlgebra k G →+ R),
  (∀ (a : G) (b : k), l (SkewMonoidAlgebra.single a b) = f b * g a) → l = SkewMonoidAlgebra.liftNC f g
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getThenInsertIfNew?!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (t : Std.DTreeMap.Internal.Impl α β) (k : α)
  (v : β k),
  t.getThenInsertIfNew?! k v =
    match t.get? k with
    | none => (none, Std.DTreeMap.Internal.Impl.insertIfNew! k v t)
    | some b => (some b, t)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a : ℤ),
  t.natTransTruncGEOfLE a a ⋯ = CategoryTheory.CategoryStruct.id (t.truncGE a)
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.varFinsetLeft.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_4} →
    {β : Type u_3} →
      (motive : L.Term (α ⊕ β) → Sort u_5) →
        (x : L.Term (α ⊕ β)) →
          ((i : α) → motive (FirstOrder.Language.var (Sum.inl i))) →
            ((_i : β) → motive (FirstOrder.Language.var (Sum.inr _i))) →
              ((l : ℕ) →
                  (_f : L.Functions l) → (ts : Fin l → L.Term (α ⊕ β)) → motive (FirstOrder.Language.func _f ts)) →
                motive x
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius_mul_coe_zeta : ArithmeticFunction.moebius * ↑ArithmeticFunction.zeta = 1
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.map_update_sub : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Ring R] [inst_1 : (i : ι) → AddCommGroup (M₁ i)]
  [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)] [inst_4 : Module R M₂]
  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂)
  [inst_7 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
  f (Function.update m i (x - y)) = f (Function.update m i x) - f (Function.update m i y)
-- Mathlib.Data.Stream.Defs
/-- Elements of a stream with odd indices.  -/
Stream'.odd : {α : Type u} → Stream' α → Stream' α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- A basis of `realSpace K` formed by the image of the fundamental units
(which form a basis of a subspace `{x : realSpace K | ∑ w, x w = 0}`) and the vector `(mult w)_w`.
For `i ≠ w₀`, the image of `completeBasis K i` by the natural restriction map
`realSpace K → logSpace K` is `basisUnitLattice K`
 -/
NumberField.mixedEmbedding.fundamentalCone.completeBasis : (K : Type u_1) →
  [inst : Field K] →
    [NumberField K] → Module.Basis (NumberField.InfinitePlace K) ℝ (NumberField.mixedEmbedding.realSpace K)
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.image_interior : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → ∀ (s : Set X), f '' interior s = interior (f '' s)
-- Mathlib.Analysis.Normed.Module.Basic
SeparationQuotient.instNormedAlgebra : (𝕜 : Type u_1) →
  {E : Type u_3} →
    [inst : NormedField 𝕜] → [inst_1 : SeminormedRing E] → [NormedAlgebra 𝕜 E] → NormedAlgebra 𝕜 (SeparationQuotient E)
-- Lean.Elab.DeprecatedSyntax
/-- Entry recording that a syntax kind has been deprecated.  -/
Lean.Elab.SyntaxDeprecationEntry : Type
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.toContinuousMapHom_apply_apply : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R] [inst_4 : IsTopologicalSemiring R] [inst_5 : StarRing R] [inst_6 : ContinuousStar R]
  (f : ContinuousMapZero X R) (a : X), (ContinuousMapZero.toContinuousMapHom f) a = f a
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- Substitution `y = x ^ p` in integrals over `Ioi 0`  -/
MeasureTheory.integral_comp_rpow_Ioi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : ℝ → E) {p : ℝ},
  p ≠ 0 → ∫ (x : ℝ) in Set.Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Set.Ioi 0, g y
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_antiperiodic : Function.Antiperiodic Complex.cos ↑Real.pi
-- Mathlib.Algebra.Group.Fin.Basic
Fin.sub_le_iff : ∀ {n : ℕ} {a b : Fin n}, a - b ≤ a ↔ b ≤ a
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_eq_prod_range : ∀ {M : Type u_3} [inst : CommMonoid M] (f : ℕ → M) (m n : ℕ),
  ∏ k ∈ Finset.Ico m n, f k = ∏ k ∈ Finset.range (n - m), f (m + k)
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- The maximum of locally Lipschitz functions is locally Lipschitz.  -/
LocallyLipschitz.max : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f g : α → ℝ},
  LocallyLipschitz f → LocallyLipschitz g → LocallyLipschitz fun x => max (f x) (g x)
-- Mathlib.Topology.Order.LeftRightNhds
mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a l' : α} {s : Set α},
  l' < a → (s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Ico l' a, Set.Ioo l a ⊆ s)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAlgebra : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          [inst_3 : TopologicalSpace A] →
            [inst_4 : IsTopologicalSemiring A] → [ContinuousConstSMul R A] → Algebra R (SeparationQuotient A)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- The identity map between `R` and `PreQuasiregular R`.  -/
PreQuasiregular.equiv : {R : Type u_1} → R ≃ PreQuasiregular R
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Compositional version of `Measurable.vadd` for use by `fun_prop`.  -/
Measurable.vadd' : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} {β : Type u_5} [inst : MeasurableSpace X] [inst_1 : VAdd M X]
  {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst_2 : MeasurableSpace M] [MeasurableVAdd₂ M X] {f : α → β → M}
  {g : α → β → X} {h : α → β}, Measurable ↿f → Measurable ↿g → Measurable h → Measurable fun a => (f a +ᵥ g a) (h a)
-- Mathlib.Analysis.Calculus.FDeriv.Extend
/-- If a real function `f` has a derivative `g` everywhere but at a point, and `f` and `g` are
continuous at this point, then `g` is the derivative of `f` everywhere.  -/
hasDerivAt_of_hasDerivAt_of_ne' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : ℝ → E} {x : ℝ},
  (∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y) → ContinuousAt f x → ContinuousAt g x → ∀ (y : ℝ), HasDerivAt f (g y) y
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.count_edges_le_one : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Walk u v},
  p.IsTrail → ∀ (e : Sym2 V), List.count e p.edges ≤ 1
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- `equiv.divLeft` as a `MeasurableEquiv`  -/
MeasurableEquiv.divLeft : {G : Type u_1} → [inst : Group G] → [inst_1 : MeasurableSpace G] → [MeasurableMul G] → [MeasurableInv G] → G → G ≃ᵐ G
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instBornology : {A : Type u_1} → [NonUnitalCStarAlgebra A] → {m : Type u_2} → {n : Type u_3} → Bornology (CStarMatrix m n A)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.revSkipWhile_prop_eq_self_iff_get : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos : s.Pos},
  pos.revSkipWhile P = pos ↔ ∀ (h : pos ≠ s.startPos), ¬P ((pos.prev h).get ⋯)
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.tsupport_subset_chartAt_source : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E] [T2Space M], tsupport ↑f ⊆ (chartAt H c).source
-- Mathlib.LinearAlgebra.Basis.Prod
Module.Basis.prod_apply_inl_snd : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') (i : ι), ((b.prod b') (Sum.inl i)).2 = 0
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_sub_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y Z : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      MeasureTheory.MemLp Z 2 μ →
        ProbabilityTheory.covariance X (Y - Z) μ =
          ProbabilityTheory.covariance X Y μ - ProbabilityTheory.covariance X Z μ
-- Mathlib.GroupTheory.Congruence.Defs
Con.rel_eq_coe : ∀ {M : Type u_1} [inst : Mul M] (c : Con M), ⇑c.toSetoid = ⇑c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (toCommSq : CategoryTheory.CommSq fst snd f g),
  Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk fst snd ⋯)) →
    CategoryTheory.IsPullback fst snd f g
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch.needlePos_le_size : ∀ {pat s : ByteArray} {needlePos stackPos : ℕ},
  String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos → needlePos ≤ pat.size
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_one : ∀ {X : Type u_1} [inst : MeasurableSpace X] (x y : X),
  ProbabilityTheory.bernoulliMeasure x y 1 = MeasureTheory.Measure.dirac x
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_apply_right : ∀ {α : Sort u_1} [inst : DecidableEq α] (a b : α), (Equiv.swap a b) b = a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
addLeftMono_of_addLeftStrictMono : ∀ (M : Type u_3) [inst : Add M] [inst_1 : PartialOrder M] [AddLeftStrictMono M], AddLeftMono M
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsRight.mk : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.MorphismProperty C},
  (∀ {X Y Z : C} (i : Y ⟶ Z), Q i → ∀ (f : X ⟶ Y), P f → P (CategoryTheory.CategoryStruct.comp f i)) → P.RespectsRight Q
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableWithinAt_ofNat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {x : E} {s : Set E} (n : ℕ) [inst_7 : OfNat F n],
  DifferentiableWithinAt 𝕜 (OfNat.ofNat n) s x
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_def_pos : ∀ {n : ℕ} [NeZero n] (x : ZMod n), x.valMinAbs = if x.val ≤ n / 2 then ↑x.val else ↑x.val - ↑n
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.congr_arg : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] {f : R ≃+* S}
  {x x' : R}, x = x' → f x = f x'
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (a : ↑A),
  (ModuleCat.Hom.hom ((Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso A g hg).inv.f i)) a =
    ((↑A.ρ.coinvariantsTprodLeftRegularLEquiv).inverse ⇑A.ρ.coinvariantsTprodLeftRegularLEquiv.symm ⋯ ⋯) a
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.map_id : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X], LocallyConstant.map id = id
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Raw.toList_valuesIter_eq_toList_map_snd : ∀ {α β : Type u} {m : Std.DHashMap.Raw α fun x => β}, m.valuesIter.toList = List.map Sigma.snd m.toList
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instBaseModule : {Γ' : Type u_2} →
  {R : Type u_3} →
    {V : Type u_5} →
      [inst : PartialOrder Γ'] →
        [inst_1 : AddCommMonoid V] → [inst_2 : Semiring R] → [inst_3 : Module R V] → Module R (HahnModule Γ' R V)
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.ofRingEquiv.congr_simp : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] {I : Ideal A} [inst_1 : CommSemiring B] {J : Ideal B}
  {e e_1 : A ≃+* B} (e_e : e = e_1) (h : Ideal.map e I = J) (hI hI_1 : DividedPowers I),
  hI = hI_1 → DividedPowers.ofRingEquiv h hI = DividedPowers.ofRingEquiv ⋯ hI_1
-- Mathlib.Lean.Thunk
Thunk.instDecidableEq_mathlib : {α : Type u} → [DecidableEq α] → DecidableEq (Thunk α)
-- Mathlib.Algebra.Ring.SumsOfSquares
AddSubmonoid.mem_sumSq : ∀ {T : Type u_2} [inst : AddMonoid T] [inst_1 : Mul T] {s : T}, s ∈ AddSubmonoid.sumSq T ↔ IsSumSq s
-- Mathlib.Data.Fin.Tuple.Reflection
_private.Mathlib.Data.Fin.Tuple.Reflection.0.FinVec.seq.match_1.splitter : {α : Type u_2} →
  {β : Type u_3} →
    (motive : (x : ℕ) → (Fin x → α → β) → (Fin x → α) → Sort u_1) →
      (x : ℕ) →
        (x_1 : Fin x → α → β) →
          (x_2 : Fin x → α) →
            ((x : Fin 0 → α → β) → (x_3 : Fin 0 → α) → motive 0 x x_3) →
              ((n : ℕ) → (f : Fin (n + 1) → α → β) → (v : Fin (n + 1) → α) → motive n.succ f v) → motive x x_1 x_2
-- Init.Prelude
Pow.mk : {α : Type u} → {β : Type v} → (α → β → α) → Pow α β
-- Mathlib.LinearAlgebra.Orientation
/-- Composing a basis with a linear equiv gives the same orientation if and only if the
determinant is positive.  -/
Module.Basis.orientation_comp_linearEquiv_eq_iff_det_pos : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (e : Module.Basis ι R M) (f : M ≃ₗ[R] M), (e.map f).orientation = e.orientation ↔ 0 < LinearMap.det ↑f
-- Mathlib.Analysis.RCLike.Basic
/-- Coercion from `ℝ` to an `RCLike` field.  -/
RCLike.ofReal : {K : Type u_1} → [RCLike K] → ℝ → K
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.bwd.inj : ∀ {gen gen_1 : Bool},
  Lean.Meta.Grind.EMatchTheoremKind.bwd gen = Lean.Meta.Grind.EMatchTheoremKind.bwd gen_1 → gen = gen_1
-- Init.Data.SInt.Bitwise
Int16.not_ne_self : ∀ {a : Int16}, ~~~a ≠ a
-- Lean.Parser.Command
Lean.Parser.Command.declSig.formatter : Lean.PrettyPrinter.Formatter
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.toCommandSuggestion : LeanSearchClient.SearchResult → Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.Lean.Meta
_private.Mathlib.Lean.Meta.0.Lean.Elab.Tactic.TacticM.runCore' : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.Context → Lean.Elab.Tactic.State → Lean.Elab.TermElabM α
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.norm_weightedSMul_le : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (s : Set α), ‖MeasureTheory.weightedSMul μ s‖ ≤ μ.real s
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- The 'unopposite' of a semigroup homomorphism `Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ`. Inverse to `MulHom.op`.  -/
MulHom.unop : {M : Type u_3} → {N : Type u_4} → [inst : Mul M] → [inst_1 : Mul N] → (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) ≃ (M →ₙ* N)
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.invOneSubPow_add : ∀ (S : Type u_1) [inst : CommRing S] (d e : ℕ),
  PowerSeries.invOneSubPow S (d + e) = PowerSeries.invOneSubPow S d * PowerSeries.invOneSubPow S e
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_comp_map : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ M') (g : N →+ N'),
  (AddMonoid.Coprod.swap M' N').comp (AddMonoid.Coprod.map f g) =
    (AddMonoid.Coprod.map g f).comp (AddMonoid.Coprod.swap M N)