mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction_zero : ∀ {b : ByteArray} {hi : 0 < b.size}, String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ b 0 hi = 0
-- Mathlib.CategoryTheory.Shift.InducedShiftSequence
CategoryTheory.Functor.ShiftSequence.induced_shiftIso_hom_app_obj_assoc : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D A} {G : CategoryTheory.Functor C A} (e : L.comp F ≅ G)
  (M : Type u_4) [inst_3 : AddMonoid M] [inst_4 : CategoryTheory.HasShift C M] [inst_5 : G.ShiftSequence M]
  (F' : M → CategoryTheory.Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m)
  [inst_6 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Full]
  [inst_7 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Faithful] [inst_8 : CategoryTheory.HasShift D M]
  [inst_9 : L.CommShift M] (n a a' : M) (ha' : n + a = a') (X : C) {Z : A} (h : (F.shift a').obj (L.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app (L.obj X)) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.Functor.commShiftIso L n).inv.app X))
        (CategoryTheory.CategoryStruct.comp ((e' a).hom.app ((CategoryTheory.shiftFunctor C n).obj X))
          (CategoryTheory.CategoryStruct.comp ((G.shiftIso n a a' ha').hom.app X) ((e' a').inv.app X))))
      h
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
/-- `PInfty` induces a natural transformation, i.e. an endomorphism of
the functor `alternatingFaceMapComplex C`.  -/
AlgebraicTopology.DoldKan.natTransPInfty : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      AlgebraicTopology.alternatingFaceMapComplex C ⟶ AlgebraicTopology.alternatingFaceMapComplex C
-- Mathlib.Probability.Distributions.Beta
ProbabilityTheory.lintegral_betaPDF : ∀ {α β : ℝ},
  ∫⁻ (x : ℝ), ProbabilityTheory.betaPDF α β x =
    ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (1 / ProbabilityTheory.beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- This iso witnesses the fact that
given `f : X ⟶ Y`, `i : U ⟶ Y`, and `i₁ : V₁ ⟶ X ×[Y] U`, `i₂ : V₂ ⟶ X ×[Y] U`, the diagram

```
V₁ ×[X ×[Y] U] V₂ ⟶ V₁ ×[U] V₂
        |                 |
        |                 |
        ↓                 ↓
        X         ⟶   X ×[Y] X
```

is a pullback square.
Also see `pullback_fst_map_snd_isPullback`.
 -/
CategoryTheory.Limits.pullbackDiagonalMapIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
        {U V₁ V₂ : C} →
          (f : X ⟶ Y) →
            (i : U ⟶ Y) →
              (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) →
                (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) →
                  [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂] →
                    CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.diagonal f)
                        (CategoryTheory.Limits.pullback.map
                          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
                          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
                          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
                          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯) ≅
                      CategoryTheory.Limits.pullback i₁ i₂
-- Mathlib.Tactic.SetNotationForOrder
/-- Delaborate `x > y` into `x ⊃ y` if the type is tagged with `@[use_set_notation_for_order]`.  -/
Mathlib.Meta.SetNotationForOrder.delabGt : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.isInvertible_equiv : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M ≃L[R] M₂}, (↑f).IsInvertible
-- Mathlib.Order.FixedPoints
OrderHom.isGreatest_gfp_le : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), IsGreatest {a | a ≤ f a} (OrderHom.gfp f)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withTopCongr_symm : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β), e.withTopCongr.symm = e.symm.withTopCongr
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- See `MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero`
for a version that assumes `Infinite R`.  -/
MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card : ∀ {R : Type u_5} {σ : Type u_6} [inst : CommRing R] [IsDomain R] {F : MvPolynomial σ R} {n : ℕ},
  F.IsHomogeneous n → (∀ (r : σ → R), (MvPolynomial.eval r) F = 0) → ↑n ≤ Cardinal.mk R → F = 0
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.paren.injEq : ∀ (ref : Lean.Syntax) (a : Lean.Elab.Tactic.RCases.RCasesPatt) (ref_1 : Lean.Syntax)
  (a_1 : Lean.Elab.Tactic.RCases.RCasesPatt),
  (Lean.Elab.Tactic.RCases.RCasesPatt.paren ref a = Lean.Elab.Tactic.RCases.RCasesPatt.paren ref_1 a_1) =
    (ref = ref_1 ∧ a = a_1)
-- Mathlib.Analysis.InnerProductSpace.Basic
norm_eq_sqrt_real_inner : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F), ‖x‖ = √(inner ℝ x x)
-- Mathlib.Algebra.Order.Star.Basic
StarOrderedRing.toIsOrderedAddMonoid : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R],
  IsOrderedAddMonoid R
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_union_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂
-- Std.Sync.StreamMap
/-- A container that maps keys to async streams, enabling dynamic stream management
and unified selection operations across multiple named data sources.
 -/
Std.StreamMap : Type → Type → Type
-- Mathlib.RingTheory.Trace.Basic
/-- Given `pb : PowerBasis K S`, then the trace of `pb.gen` is
`((minpoly K pb.gen).aroots F).sum`.  -/
PowerBasis.trace_gen_eq_sum_roots : ∀ {S : Type u_2} [inst : CommRing S] {K : Type u_4} [inst_1 : Field K] {F : Type u_6} [inst_2 : Field F]
  [inst_3 : Algebra K S] [inst_4 : Algebra K F] [Nontrivial S] (pb : PowerBasis K S),
  (Polynomial.map (algebraMap K F) (minpoly K pb.gen)).Splits →
    (algebraMap K F) ((Algebra.trace K S) pb.gen) = ((minpoly K pb.gen).aroots F).sum
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.core_certC : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly → ℕ → Bool
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
_private.Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections.0.TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj.match_1.eq_2 : ∀ {ι : Type u_1} (motive : CategoryTheory.Pairwise ι → Sort u_2) (i j : ι)
  (h_1 : (i : ι) → motive (CategoryTheory.Pairwise.single i))
  (h_2 : (i j : ι) → motive (CategoryTheory.Pairwise.pair i j)),
  (match CategoryTheory.Pairwise.pair i j with
    | CategoryTheory.Pairwise.single i => h_1 i
    | CategoryTheory.Pairwise.pair i j => h_2 i j) =
    h_2 i j
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.hasEval : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : TopologicalSpace S] {a : S},
  PowerSeries.HasEval a → MvPowerSeries.HasEval fun x => a
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- This is another convenient method to verify that a pullback cone is a weak limit cone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same `s` for all parts.  -/
CategoryTheory.Limits.PullbackCone.isWeakLimitAux' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          (t : CategoryTheory.Limits.PullbackCone f g) →
            ((s : CategoryTheory.Limits.PullbackCone f g) →
                { l //
                  CategoryTheory.CategoryStruct.comp l t.fst = s.fst ∧
                    CategoryTheory.CategoryStruct.comp l t.snd = s.snd }) →
              CategoryTheory.Limits.IsWeakLimit t
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.ext_iff : ∀ {ι : Type u_1} {X : Type u_2} {inst : TopologicalSpace X} {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  {x y : ShrinkingLemma.PartialRefinement u s p}, x = y ↔ x.toFun = y.toFun ∧ x.carrier = y.carrier
-- Mathlib.Order.Antichain
IsAntichain.preimage : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α},
  IsAntichain r s →
    ∀ {f : β → α}, Function.Injective f → (∀ ⦃a b : β⦄, r' a b → r (f a) (f b)) → IsAntichain r' (f ⁻¹' s)
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.Integrable.comp_inv : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : Group G] [MeasurableInv G] [μ.IsInvInvariant] {f : G → F},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun t => f t⁻¹) μ
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_pow_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly)
  (k : ℕ),
  p.NonnegCoeffs → Lean.Grind.CommRing.Poly.denoteS ctx (p.pow_nc k) = Lean.Grind.CommRing.Poly.denoteS ctx p ^ k
-- Init.Prelude
/-- Retrieves the current value of the monad's mutable state.
 -/
MonadState.get : {σ : outParam (Type u)} → {m : Type u → Type v} → [self : MonadState σ m] → m σ
-- Init.Data.Fin.Lemmas
Fin.natAdd_zero : ∀ {n : ℕ}, Fin.natAdd 0 = Fin.cast ⋯
-- Lean.LibrarySuggestions.SineQuaNon
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.frequencyScore : Lean.Name → optParam Float 1e-2 → Lean.MetaM Float
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.num k) = ↑k
-- Mathlib.Analysis.Fourier.ZMod
ZMod.dft_mul_const : ∀ {N : ℕ} [inst : NeZero N] {R : Type u_2} [inst_1 : Ring R] [inst_2 : Algebra ℂ R] (Φ : ZMod N → R) (r : R),
  (ZMod.dft fun j => Φ j * r) = fun k => ZMod.dft Φ k * r
-- Mathlib.LinearAlgebra.InvariantBasisNumber
card_le_of_surjective' : ∀ (R : Type u) [inst : Semiring R] [RankCondition R] {α : Type u_1} {β : Type u_2} [inst_2 : Fintype α]
  [inst_3 : Fintype β] (f : (α →₀ R) →ₗ[R] β →₀ R), Function.Surjective ⇑f → Fintype.card β ≤ Fintype.card α
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_nsmul : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) {n : ℕ} {x : 𝕜}, ↑(n • x) = n • ↑x
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.sum_range_measure_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β)
  (μ : MeasureTheory.Measure α), ∑ y ∈ f.range, μ (⇑f ⁻¹' {y}) = μ Set.univ
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.Ordering.Compares.match_1.eq_2 : ∀ {α : Type u_2} (motive : Ordering → α → α → Sort u_1) (a b : α) (h_1 : (a b : α) → motive Ordering.lt a b)
  (h_2 : (a b : α) → motive Ordering.eq a b) (h_3 : (a b : α) → motive Ordering.gt a b),
  (match Ordering.eq, a, b with
    | Ordering.lt, a, b => h_1 a b
    | Ordering.eq, a, b => h_2 a b
    | Ordering.gt, a, b => h_3 a b) =
    h_2 a b
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instFromJsonFileSystemWatcher.fromJson : Lean.Json → Except String Lean.Lsp.FileSystemWatcher
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.CommaMorphism.ext : ∀ {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} {X Y : CategoryTheory.Comma L R} {x y : CategoryTheory.CommaMorphism X Y},
  x.left = y.left → x.right = y.right → x = y
-- Mathlib.Order.SupClosed
latticeClosure_singleton : ∀ {α : Type u_3} [inst : Lattice α] (a : α), latticeClosure {a} = {a}
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.denom_J_mul : ∀ (g : GL (Fin 2) ℝ) (τ : ℂ), UpperHalfPlane.denom (UpperHalfPlane.J * g) τ = UpperHalfPlane.denom g τ
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given congruence relations `c, d` on a monoid such that `d` contains `c`, the definition of
the homomorphism from the quotient by `c` to the quotient by `d` induced by `d`'s quotient map.  -/
Con.map_apply : ∀ {M : Type u_1} [inst : MulOneClass M] {c d : Con M} (h : c ≤ d) (x : c.Quotient), (c.map d h) x = (c.lift d.mk' ⋯) x
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_fun_zero : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup E] (p : ENNReal)
  (μ : MeasureTheory.Measure α), MeasureTheory.lpNorm (fun x => 0) p μ = 0
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.const_smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : AddMonoid α] [inst_1 : Neg β]
  [inst_2 : Group γ] [inst_3 : DistribMulAction γ α],
  Function.Antiperiodic f c → ∀ (a : γ), Function.Antiperiodic (fun x => f (a • x)) (a⁻¹ • c)
-- Init.Data.String.Substring
Substring.Raw.Internal.toStringImpl : Substring.Raw → String
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- In a compactly generated space `X`, a set `s` is open when `f ⁻¹' s` is
open for every continuous map `f : K → X`, where `K` is compact Hausdorff.  -/
UCompactlyGeneratedSpace.isOpen : ∀ {X : Type w} [tX : TopologicalSpace X] [UCompactlyGeneratedSpace X] {s : Set X},
  (∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)) → IsOpen s
-- Init.Data.Option.Lemmas
Option.or_eq_right_of_none : ∀ {α : Type u_1} {o o' : Option α}, o = none → o.or o' = o'
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The variation of a function on the union of two sets `s` and `t`, with `s` to the left of `t`,
bounds the sum of the variations along `s` and `t`.  -/
eVariationOn.add_le_union : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s t : Set α},
  (∀ x ∈ s, ∀ y ∈ t, x ≤ y) → eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
-- Mathlib.Logic.Relation
Relation.ReflTransGen.below.tail : ∀ {α : Type u_1} {r : α → α → Prop} {a : α} {motive : (a_1 : α) → Relation.ReflTransGen r a a_1 → Prop} {b c : α}
  (a_1 : Relation.ReflTransGen r a b) (a_2 : r b c),
  Relation.ReflTransGen.below a_1 → motive b a_1 → Relation.ReflTransGen.below ⋯
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_mod : ∀ {a b : UInt32}, (a % b).toBitVec = a.toBitVec % b.toBitVec
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
/-- If `R` is non-trivial and `M` is finite free of rank `r`, then
the `n`th exterior power of `M` is of finrank `Nat.choose r n`.  -/
exteriorPower.finrank_eq : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Nontrivial R] [Module.Free R M] [Module.Finite R M], Module.finrank R ↥(⋀[R]^n M) = (Module.finrank R M).choose n
-- Lean.Elab.DocString
Lean.Doc.DocArg.num.injEq : ∀ (val val_1 : Lean.NumLit), (Lean.Doc.DocArg.num val = Lean.Doc.DocArg.num val_1) = (val = val_1)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_ι_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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) (n₀ n₁ : ℤ) (h : n₀ ≤ n₁) (X : C) {Z : C} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.natTransTruncLEOfLE n₀ n₁ h).app X)
      (CategoryTheory.CategoryStruct.comp ((t.truncLEι n₁).app X) h_1) =
    CategoryTheory.CategoryStruct.comp ((t.truncLEι n₀).app X) h_1
-- Mathlib.Topology.EMetricSpace.Weak
instWeakPseudoEMetricSpaceWithTop.eq_1 : ∀ {α : Type u} [t : TopologicalSpace α] [inst : LinearOrder α] [inst_1 : OrderTopology α]
  [m : WeakPseudoEMetricSpace α],
  instWeakPseudoEMetricSpaceWithTop =
    { toEDist := instEDistWithTop, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, topology_le := ⋯,
      topology_eq_on_restrict := ⋯ }
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentContentChangeEvent.fullChange.injEq : ∀ (text text_1 : String),
  (Lean.Lsp.TextDocumentContentChangeEvent.fullChange text =
      Lean.Lsp.TextDocumentContentChangeEvent.fullChange text_1) =
    (text = text_1)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- A free group basis for `G` over `ι` is associated to a map `ι → G` recording the images of
the generators.  -/
FreeGroupBasis.instFunLike : {ι : Type u_1} → {G : Type u_3} → [inst : Group G] → FunLike (FreeGroupBasis ι G) ι G
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Since `OverArrows η s` can be thought of to contain certain morphisms `yoneda.obj X ⟶ F`, the
Yoneda lemma yields elements `F.obj (op X)`.  -/
CategoryTheory.OverPresheafAux.OverArrows.val : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {η : F ⟶ A} →
        {X : C} →
          {s : CategoryTheory.yoneda.obj X ⟶ A} → CategoryTheory.OverPresheafAux.OverArrows η s → F.obj (Opposite.op X)
-- Mathlib.Algebra.Torsor.Defs
Equiv.coe_constSDiv_symm : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [inst_1 : Torsor G P] (p : P),
  ⇑(Equiv.constSDiv p).symm = fun v => v⁻¹ • p
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- An abbreviation for `prodToProdTop`, with some types already in place to help the
typechecker. In particular, the first path should be on the ulifted unit interval.  -/
ContinuousMap.Homotopy.prodToProdTopI : {X : TopCat} →
  {a₁ a₂ : ↑(TopCat.of (ULift.{u, 0} ↑unitInterval))} →
    {b₁ b₂ : ↑X} →
      (FundamentalGroupoid.fromTop a₁ ⟶ FundamentalGroupoid.fromTop a₂) →
        (FundamentalGroupoid.fromTop b₁ ⟶ FundamentalGroupoid.fromTop b₂) →
          ((FundamentalGroupoidFunctor.prodToProdTop (TopCat.of (ULift.{u, 0} ↑unitInterval)) X).obj
              ({ as := a₁ }, { as := b₁ }) ⟶
            (FundamentalGroupoidFunctor.prodToProdTop (TopCat.of (ULift.{u, 0} ↑unitInterval)) X).obj
              ({ as := a₂ }, { as := b₂ }))
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.mul_of_commute : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {S T : E →ₗ[𝕜] E}, S.IsSymmetric → T.IsSymmetric → Commute S T → (S * T).IsSymmetric
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.exact_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) (n : ℕ),
  { X₁ := I.cocomplex.X n, X₂ := I.cocomplex.X (n + 1), X₃ := I.cocomplex.X (n + 2), f := I.cocomplex.d n (n + 1),
      g := I.cocomplex.d (n + 1) (n + 2), zero := ⋯ }.Exact
-- Init.Data.SInt.Lemmas
Int32.ofInt_add : ∀ (a b : ℤ), Int32.ofInt (a + b) = Int32.ofInt a + Int32.ofInt b
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.coe_inj : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] {f g : MultilinearMap R M₁ M₂}, ⇑f = ⇑g ↔ f = g
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mergeSimp? : Lean.TSyntax `tactic → Lean.TSyntax `tactic → Option (Lean.TSyntax `tactic)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.cellFrontier_subset_finite_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  ∃ I, Topology.RelCWComplex.cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, Topology.RelCWComplex.closedCell m j
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_diff_le_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ \ t₂).size ≤ t₁.size
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1_sub : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {f g : α → F'},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ →
      MeasureTheory.condExpL1 hm μ (f - g) = MeasureTheory.condExpL1 hm μ f - MeasureTheory.condExpL1 hm μ g
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.coe_addLeft : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), ⇑(Equiv.addLeft a) = fun x => a + x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.continuous_expMap : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Continuous ↑NumberField.mixedEmbedding.fundamentalCone.expMap
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {p : P},
  p ∈ affineSpan ℝ (Set.range s.points) →
    ((∃ r, ∀ (i : Fin (n + 1)), dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p) = r) ↔
      ∃ signs, s.ExcenterExists signs ∧ p = s.excenter signs)
-- Init.Data.List.Lemmas
List.filter_append : ∀ {α : Type u_1} {p : α → Bool} (l₁ l₂ : List α), List.filter p (l₁ ++ l₂) = List.filter p l₁ ++ List.filter p l₂
-- Init.Data.List.Attach
List.unattach_reverse : ∀ {α : Type u_1} {p : α → Prop} {l : List { x // p x }}, l.reverse.unattach = l.unattach.reverse
-- Init.Data.SInt.Lemmas
ISize.toInt32_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt32 = OfNat.ofNat n
-- Mathlib.MeasureTheory.SetAlgebra
/-- If `𝒜` is an algebra of sets, then it contains the algebra generated by itself.  -/
MeasureTheory.IsSetAlgebra.generateSetAlgebra_subset_self : ∀ {α : Type u_1} {𝒜 : Set (Set α)}, MeasureTheory.IsSetAlgebra 𝒜 → MeasureTheory.generateSetAlgebra 𝒜 ⊆ 𝒜
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_of_contains_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α}, (m.erase k).contains a = true → m.contains a = true
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      ∀ {f : 𝕜 → F} {R : Type u_3} [inst_3 : DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
        ContDiffWithinAt 𝕜 (↑n) f s x → iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
-- Lean.DocString.Extension
Lean.VersoModuleDocs.add! : Lean.VersoModuleDocs → Lean.VersoModuleDocs.Snippet → Lean.VersoModuleDocs
-- Mathlib.Data.Nat.Squarefree
Nat.minSqFacAux.eq_1 : ∀ (x x_1 : ℕ),
  x.minSqFacAux x_1 =
    if h : x < x_1 * x_1 then none
    else
      have this := ⋯;
      if x_1 ∣ x then
        let n' := x / x_1;
        have this := ⋯;
        if x_1 ∣ n' then some x_1 else n'.minSqFacAux (x_1 + 2)
      else x.minSqFacAux (x_1 + 2)