mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_f' : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_f'._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_f'._auto_3),
  (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f' = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
-- ProofWidgets.Data.Html
ProofWidgets.Html.text.inj : ∀ {a a_1 : String}, ProofWidgets.Html.text a = ProofWidgets.Html.text a_1 → a = a_1
-- Init.Data.String.Lemmas.Basic
String.sliceFrom_startPos : ∀ {s : String}, s.sliceFrom s.startPos = s.toSlice
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.mem_supported' : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  {s : Set M} {x : MonoidAlgebra S M}, x ∈ MonoidAlgebra.supported R S s ↔ ∀ m ∉ s, x.coeff m = 0
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The type of arrows for the shape indexing a wide pullback.  -/
CategoryTheory.Limits.WidePullbackShape.Hom : {J : Type w} → CategoryTheory.Limits.WidePullbackShape J → CategoryTheory.Limits.WidePullbackShape J → Type w
-- Mathlib.Data.Set.Card
Set.ncard_map : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} (f : α ↪ β), (⇑f '' s).ncard = s.ncard
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- Two subgroups are equal if they have the same elements.  -/
Subgroup.ext : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, (∀ (x : G), x ∈ H ↔ x ∈ K) → H = K
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mul_le_mul_left : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R}, M ≤ N → M * P ≤ N * P
-- Mathlib.Data.Setoid.Basic
Setoid.comm' : ∀ {α : Type u_1} (s : Setoid α) {x y : α}, s x y ↔ s y x
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instInsertSigma : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Insert ((a : α) × β a) (Std.DTreeMap.Raw α β cmp)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.mk.sizeOf_spec : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  [inst_4 : SizeOf V] [inst_5 : SizeOf C] [inst_6 : SizeOf D] (obj : C → D)
  (map : (X Y : C) → (X ⟶[V] Y) ⟶ obj X ⟶[V] obj Y)
  (map_id :
    autoParam
      (∀ (X : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (map X X) = CategoryTheory.eId V (obj X))
      CategoryTheory.EnrichedFunctor.map_id._autoParam)
  (map_comp :
    autoParam
      (∀ (X Y Z : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (map X Z) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (map X Y) (map Y Z))
            (CategoryTheory.eComp V (obj X) (obj Y) (obj Z)))
      CategoryTheory.EnrichedFunctor.map_comp._autoParam),
  sizeOf { obj := obj, map := map, map_id := map_id, map_comp := map_comp } = 1
-- Mathlib.GroupTheory.Transfer
Subgroup.transferTransversal_apply'' : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (g : G)
  (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H))
  (k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))),
  ↑(⋯.leftQuotientEquiv (g ^ k.cast • Quotient.out q)) =
    if k = 0 then g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)
-- Lean.Attributes
_private.Lean.Attributes.0.Lean.AttributeExtension.mkInitial : IO Lean.AttributeExtensionState
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {D₁ : Type u_1} {D₂ : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D₁] [inst_3 : CategoryTheory.Category.{v_2, u_2} D₂]
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
  (F : CategoryTheory.Functor D₁ D₂) [Φ.HasLeftResolutions] (e : Φ.functor.comp L₂ ≅ L₁.comp F),
  Φ.IsLeftDerivabilityStructure ↔ CategoryTheory.TwoSquare.GuitartExact e.inv
-- Mathlib.Topology.Category.LightProfinite.Basic
LightDiagram.mk.injEq : ∀ (diagram : CategoryTheory.Functor ℕᵒᵖ FintypeCat)
  (cone : CategoryTheory.Limits.Cone (diagram.comp FintypeCat.toProfinite))
  (isLimit : CategoryTheory.Limits.IsLimit cone) (diagram_1 : CategoryTheory.Functor ℕᵒᵖ FintypeCat)
  (cone_1 : CategoryTheory.Limits.Cone (diagram_1.comp FintypeCat.toProfinite))
  (isLimit_1 : CategoryTheory.Limits.IsLimit cone_1),
  ({ diagram := diagram, cone := cone, isLimit := isLimit } =
      { diagram := diagram_1, cone := cone_1, isLimit := isLimit_1 }) =
    (diagram = diagram_1 ∧ cone ≍ cone_1 ∧ isLimit ≍ isLimit_1)
-- Lean.Meta.Sym.Arith.MonadCanon
/-- Synthesize an instance, returning `none` on failure.
In `SymM`, this is `Sym.synthInstance?`. In `PP.M`, this is `Meta.synthInstance?`.
 -/
Lean.Meta.Sym.Arith.MonadCanon.synthInstance? : {m : Type → Type} → [self : Lean.Meta.Sym.Arith.MonadCanon m] → Lean.Expr → m (Option Lean.Expr)
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.typeEquiv_counitIso_hom_app_hom_app_hom_apply : ∀ (X : CategoryTheory.Sheaf CategoryTheory.typesGrothendieckTopology (Type u)) (X_1 : Type uᵒᵖ)
  (x : Opposite.unop X_1 ⟶ X.obj.obj (Opposite.op PUnit.{u + 1})),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.typeEquiv.counitIso.hom.app X).hom.app X_1)) x =
    (CategoryTheory.evalEquiv X.obj ⋯ (Opposite.unop X_1)).symm x
-- Mathlib.Order.KrullDimension
Order.krullDim_nonneg : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], 0 ≤ Order.krullDim α
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryGT : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        (k : α) →
          (t : Std.DTreeMap.Internal.Impl α β) → t.Ordered → (∃ a ∈ t, compare a k = Ordering.gt) → (a : α) × β a
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- If `X` and `Y` are isomorphic, then `X` is initial iff `Y` is.  -/
CategoryTheory.Limits.IsInitial.equivOfIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (X ≅ Y) → CategoryTheory.Limits.IsInitial X ≃ CategoryTheory.Limits.IsInitial Y
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
/-- The entropy of an entourage `U`, defined as the exponential rate of growth of the size
of the smallest `(U, n)`-refined cover of `F`. Takes values in the space of extended real numbers
`[-∞, +∞]`. This second version uses a `liminf`, and is chosen as an alternative definition.  -/
Dynamics.coverEntropyInfEntourage : {X : Type u_1} → (X → X) → Set X → SetRel X X → EReal
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.quasiIso_truncLEMap_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] [inst_4 : ∀ (i : ℤ), HomologicalComplex.HasHomology L i]
  (n : ℤ), QuasiIso (CochainComplex.truncLEMap φ n) ↔ ∀ i ≤ n, QuasiIsoAt φ i
-- Init.Data.Vector.Attach
Vector.unattach_flatten : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xss : Vector (Vector { x // p x } n) n},
  xss.flatten.unattach = (Vector.map Vector.unattach xss).flatten
-- Mathlib.Data.Finset.Sups
Finset.diffs_inter_subset_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t₁ t₂ : Finset α},
  s.diffs (t₁ ∩ t₂) ⊆ s.diffs t₁ ∩ s.diffs t₂
-- Mathlib.NumberTheory.Dioph
/-- A function is Diophantine if its graph is Diophantine.  -/
Dioph.DiophFn : {α : Type u} → ((α → ℕ) → ℕ) → Prop
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- A morphism property is `IsStableUnderCobaseChange` if the cobase change of such a morphism
still falls in the class.  -/
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G),
  ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).right.left = Y.left.right
-- Mathlib.LinearAlgebra.Dimension.Finite
rank_pos : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] [Nontrivial M], 0 < Module.rank R M
-- Mathlib.Data.FunLike.Group
FunLike.coeAddHom_injective : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [inst_3 : IsAddApply F α β], Function.Injective ⇑(FunLike.coeAddHom F α β)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instAddCommMonoid : {R : Type u_1} →
  [inst : AddCommMonoid R] →
    {S : AddSubmonoid R} → [inst_1 : AddOreLocalization.AddOreSet S] → AddCommMonoid (AddOreLocalization S R)
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.aestronglyMeasurable : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {m : MeasurableSpace E} [OpensMeasurableSpace E]
  {μ : MeasureTheory.Measure E} (f : TestFunction Ω F n), MeasureTheory.AEStronglyMeasurable (⇑f) μ
-- Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.Abelian D] (G : CategoryTheory.Functor D C)
  [inst_4 : CategoryTheory.Limits.PreservesFiniteLimits G] [inst_5 : CategoryTheory.Limits.PreservesFiniteColimits G],
  G.kernel.isoModSerre = (CategoryTheory.MorphismProperty.isomorphisms C).inverseImage G
-- Mathlib.Control.Monad.Cont
_private.Mathlib.Control.Monad.Cont.0.ExceptT.run_bind.match_1.eq_1 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (x : α) (h_1 : (x : α) → motive (Except.ok x))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok x with
    | Except.ok x => h_1 x
    | Except.error e => h_2 e) =
    h_1 x
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.instIsLeftAdjointLeftAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R : CategoryTheory.Functor D C) [inst_2 : R.IsRightAdjoint], R.leftAdjoint.IsLeftAdjoint
-- Mathlib.RingTheory.Binomial
Ring.choose_zero_ite : ∀ (R : Type u_2) [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [NatPowAssoc R] [inst_3 : BinomialRing R] (k : ℕ),
  Ring.choose 0 k = if k = 0 then 1 else 0
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Submodule.finrank_add_eq_of_isCompl : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {U W : Submodule K V},
  IsCompl U W → Module.finrank K ↥U + Module.finrank K ↥W = Module.finrank K V
-- Mathlib.Analysis.Normed.Module.Connected
/-- **Alias** of `Metric.contractibleSpace_ball`. -/
Metric.ball_contractible : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ},
  0 < r → ContractibleSpace ↑(Metric.ball x r)
-- Mathlib.Algebra.Group.ULift
ULift.addCommGroup : {α : Type u} → [AddCommGroup α] → AddCommGroup (ULift.{u_1, u} α)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sub_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f g : CauSeq β abv) (i : ℕ), ↑(f - g) i = ↑f i - ↑g i
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.rightUnitor_inv_left_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (Y : CategoryTheory.Over X) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd Y.hom (CategoryTheory.CategoryStruct.id X)) h) =
    CategoryTheory.CategoryStruct.comp Y.hom h
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.preimage_coe_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithTop.some ⁻¹' Set.Ioc ↑a ↑b = Set.Ioc a b
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.comp_eq_sum_of_countable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [Countable α] [MeasurableSingletonClass α],
  μ.bind ⇑κ = MeasureTheory.Measure.sum fun ω => μ {ω} • κ ω
-- Mathlib.RingTheory.LocalRing.Quotient
IsLocalRing.basisQuotient_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [inst_4 : Module.Finite R S] [inst_5 : Module.Free R S] {ι : Type u_3} [inst_6 : Fintype ι]
  (b : Module.Basis ι R S) (i : ι),
  (IsLocalRing.basisQuotient b) i = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) (b i)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.exists_walk_of_dist_ne_zero : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.dist u v ≠ 0 → ∃ p, p.length = G.dist u v
-- Std.Time.Format
Std.Time.PlainDateTime.instRepr : Repr Std.Time.PlainDateTime
-- Init.Internal.Order.Basic
Lean.Order.PartialOrder.mk : {α : Sort u} →
  (rel : α → α → Prop) →
    (∀ {x : α}, rel x x) →
      (∀ {x y z : α}, rel x y → rel y z → rel x z) →
        (∀ {x y : α}, rel x y → rel y x → x = y) → Lean.Order.PartialOrder α
-- Mathlib.Topology.UniformSpace.Basic
/-- **Alias** of the forward direction of `uniformContinuousOn_iff_restrict`. -/
UniformContinuousOn.restrict : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α},
  UniformContinuousOn f s → UniformContinuous (s.domRestrict f)
-- Mathlib.Data.Nat.PrimeFin
Nat.nonempty_primeFactors : ∀ {n : ℕ}, n.primeFactors.Nonempty ↔ 1 < n
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.smul_equiv_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {G : Type u_3} [inst_5 : SMul G β]
  [inst_6 : IsScalarTower G β β] {f1 f2 : CauSeq β abv} (c : G), f1 ≈ f2 → c • f1 ≈ c • f2
-- Lean.Parser.Types
Lean.Parser.SyntaxStack.push : Lean.Parser.SyntaxStack → Lean.Syntax → Lean.Parser.SyntaxStack
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- For each `Δ`, `X.obj Δ` identifies to the coproduct of the objects `N A.1.unop.len`
for all `A : IndexSet Δ`.  -/
CategoryTheory.SimplicialObject.Splitting.isColimit' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (self : X.Splitting) →
        (Δ : SimplexCategoryᵒᵖ) →
          CategoryTheory.Limits.IsColimit (CategoryTheory.SimplicialObject.Splitting.cofan' self.N X self.ι Δ)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- Positivity extension for integrals.

This extension only proves non-negativity, strict positivity is more delicate for integration and
requires more assumptions.  -/
Mathlib.Meta.Positivity.evalIntegral : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Data.Sym.Basic
Sym.cast_rfl : ∀ {α : Type u_1} {n : ℕ} {s : Sym α n}, (Sym.cast ⋯) s = s
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.mrefinePat_ : Lean.ParserDescr
-- Mathlib.RingTheory.Valuation.Basic
Valuation.ofAddValuation_toAddValuation : ∀ {R : Type u_3} {Γ₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀),
  Valuation.ofAddValuation (Valuation.toAddValuation v) = v
-- Mathlib.Data.Setoid.Partition
IndexedPartition.equivQuotient_index : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s), ⇑hs.equivQuotient ∘ hs.index = hs.proj
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.supp.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent), C.supp = {v | G.connectedComponentMk v = C}
-- Aesop.Forward.State
/-- Add any enqueued hyps to the rule state, potentially generating new
complete matches in the process.  -/
Aesop.RuleState.update : Lean.MVarId → Aesop.RuleState → Aesop.BaseM (Aesop.RuleState × Array Aesop.ForwardRuleMatch)
-- Mathlib.Data.Finset.Image
/-- Given an equivalence `α` to `β`, produce an equivalence between `Finset α` and `Finset β`.  -/
Equiv.finsetCongr : {α : Type u_1} → {β : Type u_2} → α ≃ β → Finset α ≃ Finset β
-- Mathlib.ModelTheory.Algebra.Field.CharP
FirstOrder.Field.eqZero.eq_1 : ∀ (n : ℕ), FirstOrder.Field.eqZero n = (FirstOrder.Ring.termOfFreeCommRing ↑n).equal 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.filter_eq_self_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool},
  Std.ExtDHashMap.filter f m = m ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) (Std.ExtDHashMap.Const.get m k h) = true
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.hasRightDualLeftDual : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X : C} → [inst_2 : CategoryTheory.HasLeftDual X] → CategoryTheory.HasRightDual ᘁX
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.preimage_symm_preimage : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁), ⇑e ⁻¹' ⇑e.symm ⁻¹' s = s
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {f : α → Bool} {k fallback : α},
  (Std.ExtHashSet.filter f m).getD k fallback = (Option.filter f (m.get? k)).getD fallback
-- Mathlib.Order.SymmDiff
le_symmDiff_sup_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), b ≤ symmDiff a b ⊔ a
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.Pair.toPair : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} →
              {i : ι} → Monoid.PushoutI.NormalWord.Pair d i → Monoid.CoprodI.Word.Pair G i
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- **Alias** of the forward direction of `Set.MapsTo.lipschitzOnWith_iff_restrict`. -/
LipschitzOnWith.mapsToRestrict : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β} {t : Set β} (h : Set.MapsTo f s t), LipschitzOnWith K f s → LipschitzWith K (Set.MapsTo.restrict f s t h)
-- Mathlib.Tactic.Linter.Header
/-- Collect all atom values from a syntax tree.  -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.Style.header.collectAtoms : Lean.Syntax → Array String
-- Mathlib.Tactic.Linter.TextBased
/-- A line contains a space before a semicolon  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.semicolon : Mathlib.Linter.TextBased.StyleError✝
-- Batteries.Data.Array.Match
/-- Inner iterator.  -/
Array.Matcher.Iterator.inner : {σ : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {α : Type u_1} →
      [inst : BEq α] →
        {m : Array.Matcher α} → [inst_1 : Std.Iterator σ n α] → Array.Matcher.Iterator σ n α m → Std.IterM n α
-- Init.Data.SInt.Lemmas
ISize.neg_ne_zero : ∀ {a : ISize}, -a ≠ 0 ↔ a ≠ 0
-- Mathlib.Data.List.Basic
List.insert_neg : ∀ {α : Type u} [inst : DecidableEq α] {x : α} {l : List α}, x ∉ l → insert x l = x :: l
-- Mathlib.Data.Finset.Sym
Finset.val_prod_eq_prod_count_pow : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommMonoid α] {n : ℕ} {k : Sym α n} {s : Finset α},
  k ∈ s.sym n → (↑k).prod = ∏ d ∈ s, d ^ Multiset.count d ↑k
-- Mathlib.GroupTheory.Index
/-- A subgroup has index two if and only if there exists `a` such that for all `b`, exactly one
of `a * b` and `b` belong to `H`.  -/
Subgroup.index_eq_two_iff' : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 2 ↔ ∃ a, ∀ (b : G), Xor (a * b ∈ H) (b ∈ H)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.ofSet_univ_eq_refl : ∀ {X : Type u_1} [inst : TopologicalSpace X], OpenPartialHomeomorph.ofSet Set.univ ⋯ = OpenPartialHomeomorph.refl X
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.nsmul_right : ∀ {M : Type u_2} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (n : ℕ), AddCommute a (n • b)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F) (x : E),
  ‖A x‖ = √(RCLike.re (inner 𝕜 x ((ContinuousLinearMap.adjoint A ∘SL A) x)))
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instBEqPosition.beq : Lean.Lsp.Position → Lean.Lsp.Position → Bool
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- If a function is locally integrable, then it is integrable on any compact set.  -/
MeasureTheory.LocallyIntegrable.integrableOn_isCompact : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε]
  {k : Set X}, MeasureTheory.LocallyIntegrable f μ → IsCompact k → MeasureTheory.IntegrableOn f k μ
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.neg : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E}, MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (-f) p μ
-- Mathlib.Algebra.Group.Pi.Lemmas
OneHom.mulSingle.eq_1 : ∀ {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst_1 : (i : I) → One (f i)] (i : I),
  OneHom.mulSingle f i = { toFun := Pi.mulSingle i, map_one' := ⋯ }
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.end_cons : ∀ {V : Type u_1} [inst : Quiver V] {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c), (p.cons e).end = c