mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.supp_inj : ∀ {V : Type u} {G : SimpleGraph V} {C D : G.ConnectedComponent}, C.supp = D.supp ↔ C = D
-- Mathlib.GroupTheory.OrderOfElement
orderOf_le_card : ∀ {G : Type u_1} [inst : Monoid G] {x : G} [Finite G], orderOf x ≤ Nat.card G
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
CategoryTheory.Functor.hasRightDerivedFunctor_of_hasPointwiseRightDerivedFunctor : ∀ {C : Type u₁} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₃, u₃} H]
  (F : CategoryTheory.Functor C H) (W : CategoryTheory.MorphismProperty C) [F.HasPointwiseRightDerivedFunctor W],
  F.HasRightDerivedFunctor W
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- An orthonormal set in an `InnerProductSpace` is maximal, if and only if the orthogonal
complement of its span is empty.  -/
maximal_orthonormal_iff_orthogonalComplement_eq_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {v : Set E}, Orthonormal 𝕜 Subtype.val → ((∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ (Submodule.span 𝕜 v)ᗮ = ⊥)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp : ∀ {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E']
  [inst_2 : InnerProductSpace 𝕜 E'] [inst_3 : CompleteSpace E'] [inst_4 : NormedSpace ℝ E'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E'),
  ↑((MeasureTheory.condExpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) =
    (ContinuousLinearMap.toSpanSingleton ℝ x).compLp
      ↑((MeasureTheory.condExpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1))
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.disjoint_def' : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ : Subgroup G}, Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.unop_zsmul : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : Cᵒᵖ}
  (k : ℤ) (f : X ⟶ Y), (k • f).unop = k • f.unop
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (toMonoidHom : α →* β) (monotone' : Monotone (↑toMonoidHom).toFun) (toMonoidHom_1 : α →* β)
  (monotone'_1 : Monotone (↑toMonoidHom_1).toFun),
  ({ toMonoidHom := toMonoidHom, monotone' := monotone' } =
      { toMonoidHom := toMonoidHom_1, monotone' := monotone'_1 }) =
    (toMonoidHom = toMonoidHom_1)
-- Init.Data.UInt.Lemmas
UInt64.le_ofNat_iff : ∀ {n : UInt64} {m : ℕ}, m < UInt64.size → (n ≤ UInt64.ofNat m ↔ n.toNat ≤ m)
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_fst : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor (A ⊕ A') B),
  (CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso.hom.app X).1 =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Sum.inl_ A' A).associator (CategoryTheory.Sum.swap A' A) X).inv
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.Sum.swapCompInl A' A).hom X)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.keys_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {f : α → β → Bool} (h : m.WF),
  (Std.HashMap.Raw.filter f m).keys.Perm
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x m[x])
        m.keys.attach).unattach
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.uncurry0_apply : ∀ (𝕜 : Type u) {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (x : G') (m : Fin 0 → G),
  (ContinuousMultilinearMap.uncurry0 𝕜 G x) m = x
-- Lean.MetavarContext
/-- See comment at `CheckAssignment` `Meta/ExprDefEq.lean`  -/
Lean.MetavarDecl.numScopeArgs : Lean.MetavarDecl → ℕ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_two_pi : Complex.sin (2 * ↑Real.pi) = 0
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.pow_comp : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) (n : ℕ), (p ^ n).comp q = p.comp q ^ n
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.whiskerBottom_app : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B B' : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  (α : B ⟶ B') (X : C₁),
  (w.whiskerBottom α).app X = CategoryTheory.CategoryStruct.comp (w.natTrans.app X) (α.app (L.obj X))
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.distribMulAction : {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) →
      {m : Monoid α} →
        {n : (i : I) → AddMonoid (f i)} → [(i : I) → DistribMulAction α (f i)] → DistribMulAction α ((i : I) → f i)
-- Std.Http.Data.Status
Std.Http.CustomStatus.mk : (code : UInt16) →
  (phrase : String) →
    autoParam (Std.Http.IsValidReasonPhrase phrase) Std.Http.CustomStatus.validReasonPhrase._autoParam →
      autoParam (100 ≤ code ∧ code ≤ 999) Std.Http.CustomStatus.validCode._autoParam →
        autoParam (¬Std.Http.isKnownStatusCode code = true) Std.Http.CustomStatus.validUnknown._autoParam →
          Std.Http.CustomStatus
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- This version imposes `ι` and `E` to live in the same universe, so you should instead use
`continuous_equivFun_basis` which gives the same result without universe restrictions.  -/
_private.Mathlib.Topology.Algebra.Module.FiniteDimension.0.continuous_equivFun_basis_aux : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] [T2Space E]
  {ι : Type v} [inst_7 : Finite ι] (ξ : Module.Basis ι 𝕜 E), Continuous ⇑ξ.equivFun
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- `eval₂AddMonoidHom (f : R →+* S) (x : S)` is the `AddMonoidHom` from
`R[X]` to `S` obtained by evaluating the pushforward of `p` along `f` at `x`.  -/
Polynomial.eval₂AddMonoidHom : {R : Type u} → {S : Type v} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) → S → Polynomial R →+ S
-- Mathlib.Combinatorics.Configuration
/-- Number of points on a given line.  -/
Configuration.lineCount : {P : Type u_1} → (L : Type u_2) → [Membership P L] → P → ℕ
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `NonAssocRing` instance along a surjective function.  -/
Function.Surjective.nonAssocRing : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : Neg S] →
                  [inst_5 : Sub S] →
                    [inst_6 : SMul ℕ S] →
                      [inst_7 : SMul ℤ S] →
                        [inst_8 : NatCast S] →
                          [inst_9 : IntCast S] →
                            [inst_10 : NonAssocRing R] →
                              f 0 = 0 →
                                f 1 = 1 →
                                  (∀ (x y : R), f (x + y) = f x + f y) →
                                    (∀ (x y : R), f (x * y) = f x * f y) →
                                      (∀ (x : R), f (-x) = -f x) →
                                        (∀ (x y : R), f (x - y) = f x - f y) →
                                          (∀ (n : ℕ) (x : R), f (n • x) = n • f x) →
                                            (∀ (n : ℤ) (x : R), f (n • x) = n • f x) →
                                              (∀ (n : ℕ), f ↑n = ↑n) → (∀ (n : ℤ), f ↑n = ↑n) → NonAssocRing S
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instIsPartialOrderOpposite : ∀ {α : Type u_1} {i : LE α} [Std.IsPartialOrder α], Std.IsPartialOrder α
-- Lean.Elab.Deriving.Basic
Lean.Elab.DerivingClassView.mk : Lean.Syntax → Bool → Lean.Term → Lean.Elab.DerivingClassView
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.GradedNatTrans.ext : ∀ {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}
  {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D}
  {x y : CategoryTheory.GradedNatTrans A F G}, x.app = y.app → x = y
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
CategoryTheory.IsGrothendieckAbelian.hasSeparator : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Abelian C}
  [self : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C], CategoryTheory.HasSeparator C
-- Init.Omega.Int
Lean.Omega.Int.ofNat_shiftRight_eq_div_pow : ∀ {x y : ℕ}, ↑(x >>> y) = ↑x / ↑(2 ^ y)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsMonHom.Normal.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H] {φ : H ⟶ G},
  autoParam (CategoryTheory.Mono φ) CategoryTheory.IsMonHom.Normal.mono._autoParam →
    autoParam (CategoryTheory.IsMonHom φ) CategoryTheory.IsMonHom.Normal.isMonHom._autoParam →
      (∃ ψ,
          CategoryTheory.CategoryStruct.comp ψ φ =
            CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G φ)
              (CategoryTheory.GrpObj.conj G)) →
        CategoryTheory.IsMonHom.Normal φ
-- Init.Prelude
/-- The homogeneous version of `HAdd`: `a + b : α` where `a b : α`.  -/
Add : Type u → Type u
-- Mathlib.ModelTheory.Substructures
/-- A first-order embedding `f : M → N` whose values lie in a substructure `p ⊆ N` can be restricted
to an embedding `M → p`.  -/
FirstOrder.Language.Embedding.codRestrict : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          (p : L.Substructure N) → (f : L.Embedding M N) → (∀ (c : M), f c ∈ p) → L.Embedding M ↥p
-- Plausible.Shrinkable
Plausible.Array.shrinkable : {α : Type u_1} → [Plausible.Shrinkable α] → Plausible.Shrinkable (Array α)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.registerSimproc : Lean.Name → Array Lean.Meta.SimpTheoremKey → Lean.CoreM Unit
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.coe_filter_univ : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p],
  ↑(Finset.filter p Finset.univ) = {x | p x}
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_eq_one_iff' : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] [Nontrivial A] (a : A),
  CFC.sqrt a = 1 ↔ a = 1
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_eq_of_bijective : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.Bijective f → Nat.card α = Nat.card β
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.getElem_rightInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ)
  (h : j < ω.length),
  (cs.rightInvSeq ω)[j] =
    (cs.wordProd (List.drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (List.drop (j + 1) ω)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.modify_eq_alter : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {a : α}
  {f : β → β} (htb : t.Balanced),
  Std.DTreeMap.Internal.Impl.Const.modify a f t =
    (Std.DTreeMap.Internal.Impl.Const.alter a (fun x => Option.map f x) t htb).impl
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact
ModuleCat.restrictScalars_map_exact : ∀ {R : Type u} [inst : CommRing R] {R' : Type u'} [inst_1 : CommRing R'] (f : R →+* R')
  (S : CategoryTheory.ShortComplex (ModuleCat R')), S.Exact → (S.map (ModuleCat.restrictScalars f)).Exact
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₀_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 0}
  (f :
    F.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1 ⟶ G.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1)
  (i : Fin (0 + 1)),
  (CategoryTheory.ComposableArrows.homMk₀ f).app i =
    match i with
    | ⟨0, isLt⟩ => f
-- Mathlib.Algebra.Category.Ring.Small
CommRingCat.essentiallySmall_of_localizationAway : ∀ {P Q : CategoryTheory.ObjectProperty CommRingCat} [CategoryTheory.ObjectProperty.EssentiallySmall.{u, u, u + 1} Q],
  (∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (CommRingCat.of (Localization.Away f))) →
    CategoryTheory.ObjectProperty.EssentiallySmall.{u, u, u + 1} P
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.valuesArray_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.valuesArray = t₂.valuesArray
-- Mathlib.Computability.Reduce
OneOneEquiv.trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, OneOneEquiv p q → OneOneEquiv q r → OneOneEquiv p r
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_one : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀),
  v 1 = 1
-- Mathlib.Order.Sublattice
Sublattice.inf_mem : ∀ {α : Type u_2} [inst : Lattice α] {L : Sublattice α} {a b : α}, a ∈ L → b ∈ L → a ⊓ b ∈ L
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.exists_isNilRegular : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup L] [inst_2 : Module R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M) [inst_5 : Module.Free R M]
  [inst_6 : Module.Finite R M] [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] [IsDomain R] [Infinite R],
  ∃ x, φ.IsNilRegular x
-- Mathlib.Data.List.Palindrome
List.Palindrome.brecOn : ∀ {α : Type u_1} {motive : (a : List α) → a.Palindrome → Prop} {a : List α} (t : a.Palindrome),
  (∀ (a : List α) (t : a.Palindrome), List.Palindrome.below t → motive a t) → motive a t
-- Init.Grind.ToInt
/-- The embedding function is injective.  -/
Lean.Grind.ToInt.toInt_inj : ∀ {α : Type u} {range : outParam Lean.Grind.IntInterval} [self : Lean.Grind.ToInt α range] (x y : α), ↑x = ↑y → x = y
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.CancelResult.mk.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {mα : Q(Mul «$α»)} {e v : Q(«$α»)} (cancelled : Q(«$α»))
  (pf : Q(«$v» * «$e» = «$cancelled»)), sizeOf { cancelled := cancelled, pf := pf } = 1 + sizeOf cancelled + sizeOf pf
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.instSMulNatHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier : (X : TopCat) → (R : TopCommRingCat) → SMul ℕ (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} {fallback : β k},
  (Std.DTreeMap.filter f t).getD k fallback = (Option.filter (f k) (t.get? k)).getD fallback
-- Mathlib.AlgebraicGeometry.Birational.Dominant
/-- A rational map is dominant if some (equivalently, any) representative partial map has
dominant underlying morphism.  -/
AlgebraicGeometry.Scheme.RationalMap.IsDominant : {X Y : AlgebraicGeometry.Scheme} → X.RationalMap Y → Prop
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.elabMatchSyntax : Lean.Elab.Term.TermElab
-- Init.MetaTypes
Lean.Meta.EtaStructMode.all.sizeOf_spec : sizeOf Lean.Meta.EtaStructMode.all = 1
-- Mathlib.Order.Interval.Set.Fin
Fin.image_addNat_Ico : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) '' Set.Ico i j = Set.Ico (i.addNat m) (j.addNat m)
-- Mathlib.Data.Set.Basic
/-- **Alias** of the reverse direction of `Set.nonempty_coe_sort`. -/
Set.Nonempty.coe_sort : ∀ {α : Type u} {s : Set α}, s.Nonempty → Nonempty ↑s
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
mdifferentiableOn_extChartAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I 1 M] {x : M},
  MDiff[(extChartAt I x).target] ↑(extChartAt I x).symm
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.InvariantForm.apply_eq_or_aux : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} [Finite ι]
  [CharZero R] [inst_7 : P.IsCrystallographic] [IsDomain R] [P.IsReduced] (B : P.InvariantForm) (i j : ι),
  P.pairingIn ℤ i j ≠ 0 →
    (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j) ∨
      (B.form (P.root i)) (P.root i) = 2 * (B.form (P.root j)) (P.root j) ∨
        (B.form (P.root i)) (P.root i) = 3 * (B.form (P.root j)) (P.root j) ∨
          (B.form (P.root j)) (P.root j) = 2 * (B.form (P.root i)) (P.root i) ∨
            (B.form (P.root j)) (P.root j) = 3 * (B.form (P.root i)) (P.root i)
-- Mathlib.Topology.Order.MonotoneConvergence
LinearOrder.infConvergenceClass : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α], InfConvergenceClass α
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  LeftOrdContinuous f = ∀ ⦃s : Set α⦄ ⦃x : α⦄, s.Nonempty → IsLUB s x → IsLUB (f '' s) (f x)
-- Mathlib.Data.Seq.Computation
Computation.bind_assoc : ∀ {α : Type u} {β : Type v} {γ : Type w} (s : Computation α) (f : α → Computation β) (g : β → Computation γ),
  (s.bind f).bind g = s.bind fun x => (f x).bind g
-- Mathlib.Algebra.Group.Defs
add_left_cancel_iff : ∀ {G : Type u_1} [inst : Add G] [IsLeftCancelAdd G] {a b c : G}, a + b = a + c ↔ b = c
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.not_bddAbove : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [NoMaxOrder α], IsUpperSet s → s.Nonempty → ¬BddAbove s
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.of_equiv : ∀ {R : Type u_2} {R' : Type u_3} {M : Type u_4} {M' : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M'] [inst_5 : Module R' M'] {σ : R →+* R'}
  {σ' : R' →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ] (e₂ : M ≃ₛₗ[σ] M') [Module.Free R M],
  Module.Free R' M'
-- Batteries.Data.String.Matcher
/-- Knuth-Morris-Pratt matcher type

This type is used to keep data for running the Knuth-Morris-Pratt (KMP) string matching algorithm.
KMP is a linear time algorithm to locate all substrings of a string that match a given pattern.
Generating the algorithm data is also linear in the length of the pattern but the data can be
re-used to match the same pattern over different strings.

The KMP data for a pattern string can be generated using `Matcher.ofString`. Then `Matcher.find?`
and `Matcher.findAll` can be used to run the algorithm on an input string.
```
def m := Matcher.ofString "abba"

#eval Option.isSome <| m.find? "AbbabbA" -- false
#eval Option.isSome <| m.find? "aabbaa" -- true

#eval Array.size <| m.findAll "abbabba" -- 2
#eval Array.size <| m.findAll "abbabbabba" -- 3
```
 -/
String.Matcher : Type
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a finite Haar measure under a continuous surjective group homomorphism is again
a Haar measure. See also `isHaarMeasure_map`.  -/
MeasureTheory.Measure.isHaarMeasure_map_of_isFiniteMeasure : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [BorelSpace G] [ContinuousMul G] {H : Type u_3} [inst_6 : Group H]
  [inst_7 : TopologicalSpace H] [inst_8 : MeasurableSpace H] [BorelSpace H] [ContinuousMul H]
  [MeasureTheory.IsFiniteMeasure μ] (f : G →* H),
  Continuous ⇑f → Function.Surjective ⇑f → (MeasureTheory.Measure.map (⇑f) μ).IsHaarMeasure
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.rfl_q : Lean.Meta.Grind.Arith.Linear.NatStruct → Lean.Expr
-- Mathlib.Data.Multiset.Bind
Multiset.Nodup.sigma : ∀ {α : Type u_1} {s : Multiset α} {σ : α → Type u_5} {t : (a : α) → Multiset (σ a)},
  s.Nodup → (∀ (a : α), (t a).Nodup) → (s.sigma t).Nodup
-- Mathlib.Order.Interval.Set.Fin
Fin.image_val_Ici : ∀ {n : ℕ} (i : Fin n), Fin.val '' Set.Ici i = Set.Ico (↑i) n
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.hom_ext_iff : ∀ {G : Type u} [inst : Group G] {A : Type v} [inst_1 : Monoid A] {φ ψ : Abelianization G →* A},
  φ = ψ ↔ φ.comp Abelianization.of = ψ.comp Abelianization.of
-- Mathlib.Topology.VectorBundle.Basic
continuousOn_coordChange : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E] [inst_9 : VectorBundle R F E]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_10 : MemTrivializationAtlas e]
  [inst_11 : MemTrivializationAtlas e'],
  ContinuousOn (fun b => ↑(Bundle.Trivialization.coordChangeL R e e' b)) (e.baseSet ∩ e'.baseSet)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.comp.eq_5 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.WithTerminal.comp = fun x x_1 => PUnit.unit
-- Lean.Environment
Lean.PersistentEnvExtension.mk.injEq : ∀ {α β σ : Type} (toEnvExtension : Lean.EnvExtension (Lean.PersistentEnvExtensionState α σ)) (name : Lean.Name)
  (addImportedFn : Array (Array α) → Lean.ImportM σ) (addEntryFn : σ → β → σ)
  (exportEntriesFn : Lean.Environment → σ → Lean.OLeanEntries (Array α)) (statsFn : σ → Std.Format)
  (toEnvExtension_1 : Lean.EnvExtension (Lean.PersistentEnvExtensionState α σ)) (name_1 : Lean.Name)
  (addImportedFn_1 : Array (Array α) → Lean.ImportM σ) (addEntryFn_1 : σ → β → σ)
  (exportEntriesFn_1 : Lean.Environment → σ → Lean.OLeanEntries (Array α)) (statsFn_1 : σ → Std.Format),
  ({ toEnvExtension := toEnvExtension, name := name, addImportedFn := addImportedFn, addEntryFn := addEntryFn,
        exportEntriesFn := exportEntriesFn, statsFn := statsFn } =
      { toEnvExtension := toEnvExtension_1, name := name_1, addImportedFn := addImportedFn_1,
        addEntryFn := addEntryFn_1, exportEntriesFn := exportEntriesFn_1, statsFn := statsFn_1 }) =
    (toEnvExtension = toEnvExtension_1 ∧
      name = name_1 ∧
        addImportedFn = addImportedFn_1 ∧
          addEntryFn = addEntryFn_1 ∧ exportEntriesFn = exportEntriesFn_1 ∧ statsFn = statsFn_1)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_one : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k], SkewMonoidAlgebra.coeff 1 = fun₀ | 1 => 1