mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.hasPushout_of_right_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.IsIso g],
  CategoryTheory.Limits.HasPushout f g
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The underlying object in the base category.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.base : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} → F.CoGrothendieck → 𝒮
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- The isomorphism `E ⧸ S.inl.range ≃* G` induced by `S.rightHom`  -/
GroupExtension.quotientRangeInlEquivRight : {N : Type u_1} →
  {G : Type u_2} →
    [inst : Group N] →
      [inst_1 : Group G] → {E : Type u_3} → [inst_2 : Group E] → (S : GroupExtension N E G) → E ⧸ S.inl.range ≃* G
-- Mathlib.Order.Filter.Basic
Filter.eventuallyEq_iff_sub : ∀ {α : Type u} {β : Type v} [inst : AddGroup β] {f g : α → β} {l : Filter α}, f =ᶠ[l] g ↔ f - g =ᶠ[l] 0
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_eq_erase_univ : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableEq V] [inst_2 : DecidableRel G.Adj] (v : V),
  G.neighborFinset v = Finset.univ.erase v ↔ G.IsUniversal v
-- Lean.Parser.Types
Lean.Parser.TokenCacheEntry.mk.injEq : ∀ (startPos stopPos : String.Pos.Raw) (token : Lean.Syntax) (startPos_1 stopPos_1 : String.Pos.Raw)
  (token_1 : Lean.Syntax),
  ({ startPos := startPos, stopPos := stopPos, token := token } =
      { startPos := startPos_1, stopPos := stopPos_1, token := token_1 }) =
    (startPos = startPos_1 ∧ stopPos = stopPos_1 ∧ token = token_1)
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.instInhabitedHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (r : HomRel C) → (a : CategoryTheory.Quotient r) → Inhabited (CategoryTheory.Quotient.Hom r a a)
-- Mathlib.Data.Set.Subsingleton
Set.Nonempty.exists_eq_singleton_or_nontrivial : ∀ {α : Type u} {s : Set α}, s.Nonempty → (∃ a, s = {a}) ∨ s.Nontrivial
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequence_exact₃ : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [inst_8 : F.IsHomological] [inst_9 : F.ShiftSequence ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
  { X₁ := (F.shift n₀).obj T.obj₂, X₂ := (F.shift n₀).obj T.obj₃, X₃ := (F.shift n₁).obj T.obj₁,
      f := (F.shift n₀).map T.mor₂, g := F.homologySequenceδ T n₀ n₁ h, zero := ⋯ }.Exact
-- Mathlib.Data.Set.Lattice
Set.ofPred_exists : ∀ {β : Type u_2} {ι : Sort u_5} (p : ι → β → Prop), {x | ∃ i, p i x} = ⋃ i, {x | p i x}
-- Init.Data.UInt.Bitwise
UInt16.shiftRight_eq_shiftRight_mod : ∀ (a b : UInt16), a >>> b = a >>> (b % 16)
-- Mathlib.Algebra.FreeMonoid.Basic
_private.Mathlib.Algebra.FreeMonoid.Basic.0.FreeMonoid.prodAux.match_1.eq_2 : ∀ {M : Type u_1} (motive : List M → Sort u_2) (x : M) (xs : List M) (h_1 : Unit → motive [])
  (h_2 : (x : M) → (xs : List M) → motive (x :: xs)),
  (match x :: xs with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_2 x xs
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgsResult.simprocs : Lean.Elab.Tactic.ElabSimpArgsResult → Lean.Meta.Simp.SimprocsArray
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiStruct.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X Y : C} {f : Y ⟶ X}
  {desc :
    {W : C} →
      (e : Y ⟶ W) →
        (∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
            CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
              CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) →
          (X ⟶ W)}
  {fac :
    ∀ {W : C} (e : Y ⟶ W)
      (h :
        ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
          CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
            CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e),
      CategoryTheory.CategoryStruct.comp f (desc e ⋯) = e}
  {uniq :
    ∀ {W : C} (e : Y ⟶ W)
      (h :
        ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
          CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
            CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)
      (m : X ⟶ W), CategoryTheory.CategoryStruct.comp f m = e → m = desc e ⋯}
  {desc_1 :
    {W : C} →
      (e : Y ⟶ W) →
        (∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
            CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
              CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) →
          (X ⟶ W)}
  {fac_1 :
    ∀ {W : C} (e : Y ⟶ W)
      (h :
        ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
          CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
            CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e),
      CategoryTheory.CategoryStruct.comp f (desc_1 e ⋯) = e}
  {uniq_1 :
    ∀ {W : C} (e : Y ⟶ W)
      (h :
        ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
          CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
            CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)
      (m : X ⟶ W), CategoryTheory.CategoryStruct.comp f m = e → m = desc_1 e ⋯},
  { desc := desc, fac := fac, uniq := uniq } = { desc := desc_1, fac := fac_1, uniq := uniq_1 } → desc = desc_1
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.zpow_mem : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {x : G}, x ∈ K → ∀ (n : ℤ), x ^ n ∈ K
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.imageMulHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Mul α] [inst_2 : Mul β]
  [inst_3 : FunLike F α β] [inst_4 : MulHomClass F α β] (f : F) [inst_5 : DecidableEq β] (s : Finset α),
  (Finset.imageMulHom f) s = Finset.image (⇑f) s
-- Mathlib.Data.Finsupp.Order
Finsupp.orderBot : {ι : Type u_1} →
  {α : Type u_3} → [inst : AddCommMonoid α] → [inst_1 : PartialOrder α] → [IsBotZeroClass α] → OrderBot (ι →₀ α)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.AbelNF.Config.mk.sizeOf_spec : ∀ (toConfig : Mathlib.Tactic.AtomM.Recurse.Config) (mode : Mathlib.Tactic.Abel.AbelMode),
  sizeOf { toConfig := toConfig, mode := mode } = 1 + sizeOf toConfig + sizeOf mode
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.mk_of_mem_addSubgroup_toFun : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddGroup Y] (f : X → Y)
  (hf : f ∈ Function.locallyFinsuppWithin.addSubgroup U) (a : X),
  (Function.locallyFinsuppWithin.mk_of_mem_addSubgroup f hf) a = f a
-- Mathlib.RingTheory.Kaehler.Basic
/-- The lift of the map `Ω[A⁄R] →ₗ[A] Ω[B⁄R]` to the base change along `A → B`.
This is the first map in the exact sequence `B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0`.  -/
KaehlerDifferential.mapBaseChange : (R : Type u) →
  [inst : CommRing R] →
    (A : Type u_2) →
      (B : Type u_3) →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra A B] →
                [inst_5 : Algebra R B] → [IsScalarTower R A B] → TensorProduct A B Ω[A⁄R] →ₗ[B] Ω[B⁄R]
-- Mathlib.Algebra.GroupWithZero.Basic
zero_zpow_eq_one₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {n : ℤ}, 0 ^ n = 1 ↔ n = 0
-- Init.Data.UInt.Basic
/-- Converts an `Int` to a `UInt32` by taking the (non-negative remainder of the division by `2 ^ 32`.  -/
UInt32.ofInt : ℤ → UInt32
-- Batteries.Lean.Meta.DiscrTree
/-- Merge two `DiscrTree`s. Duplicate values are preserved.
 -/
Lean.Meta.DiscrTree.mergePreservingDuplicates : {α : Type} → Lean.Meta.DiscrTree α → Lean.Meta.DiscrTree α → Lean.Meta.DiscrTree α
-- Mathlib.Data.List.MinMax
List.argmax.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] (f : α → β) (l : List α),
  List.argmax f l = List.foldl (List.argAux fun b c => f c < f b) none l
-- Mathlib.Topology.WithTopology
WithTopology.instDistribLattice : {X : Type u_1} → (t : TopologicalSpace X) → [DistribLattice X] → DistribLattice (WithTopology X t)
-- Mathlib.Computability.StateTransition
StateTransition.Reaches₀.head : ∀ {σ : Type u_1} {f : σ → Option σ} {a b c : σ},
  b ∈ f a → StateTransition.Reaches₀ f b c → StateTransition.Reaches₀ f a c
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.BinaryRefVec w → Std.Sat.AIG.RefVecEntry α w
-- Lean.Environment
_private.Lean.Environment.0.Lean.finalizeImport.unsafe_impl_9 : Lean.Environment → BaseIO Lean.Environment
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.m_pos : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α → 0 < Fintype.card α / SzemerediRegularity.stepBound P.parts.card
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.span_eq_toSubmodule : ∀ {A : Type v} [inst : NonUnitalSemiring A] [inst_1 : StarRing A] {R : Type u_1} [inst_2 : CommSemiring R]
  [inst_3 : Module R A] (s : NonUnitalStarSubalgebra R A), Submodule.span R ↑s = s.toSubmodule
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.Loopless.mk : ∀ {α : Type u_1} {M : Matroid α}, M.loops = ∅ → M.Loopless
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.closure_prod_one : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (s : Set M),
  Submonoid.closure (s ×ˢ {1}) = (Submonoid.closure s).prod ⊥
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- `Monoid.Pow` is measurable.  -/
Monoid.measurablePow : ∀ (M : Type u_2) [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M], MeasurablePow M ℕ
-- Std.Time.DateTime
/-- Creates a new `DateTime` out of a `PlainDateTime` and a `TimeZone`. It assumes `PlainDateTime` is
the local time.
 -/
Std.Time.DateTime.ofPlainDateTimeWithZone : Std.Time.PlainDateTime → Std.Time.TimeZone → Std.Time.DateTime
-- Mathlib.Analysis.Normed.Operator.Extend
/-- Extension of a linear equivalence `f : E ≃ₛₗ[σ₁₂] F` to a continuous linear equivalence
`Eₗ ≃SL[σ₁₂] Fₗ`, where `E` and `F` are normed spaces and `Eₗ` and `Fₗ` are Banach spaces,
using dense maps `e₁ : E →ₗ[𝕜₁] Eₗ` and `e₂ : F →ₗ[𝕜₂] F₂` together with bounds
`‖e₂ (f x)‖ ≤ C * ‖e₁ x‖` for all `x : E` and `‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖` for all `x : F`.  -/
LinearEquiv.extend : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {Eₗ : Type u_4} →
        {F : Type u_5} →
          {Fₗ : Type u_6} →
            [inst : NormedDivisionRing 𝕜] →
              [inst_1 : NormedDivisionRing 𝕜₂] →
                [inst_2 : AddCommGroup E] →
                  [inst_3 : NormedAddCommGroup Eₗ] →
                    [inst_4 : AddCommGroup F] →
                      [inst_5 : NormedAddCommGroup Fₗ] →
                        [inst_6 : Module 𝕜 E] →
                          [inst_7 : Module 𝕜 Eₗ] →
                            [IsBoundedSMul 𝕜 Eₗ] →
                              [inst_9 : Module 𝕜₂ F] →
                                [inst_10 : Module 𝕜₂ Fₗ] →
                                  [IsBoundedSMul 𝕜₂ Fₗ] →
                                    [CompleteSpace Eₗ] →
                                      [CompleteSpace Fₗ] →
                                        {σ₁₂ : 𝕜 →+* 𝕜₂} →
                                          {σ₂₁ : 𝕜₂ →+* 𝕜} →
                                            [inst_14 : RingHomInvPair σ₁₂ σ₂₁] →
                                              [inst_15 : RingHomInvPair σ₂₁ σ₁₂] →
                                                (f : E ≃ₛₗ[σ₁₂] F) →
                                                  (e₁ : E →ₗ[𝕜] Eₗ) →
                                                    (e₂ : F →ₗ[𝕜₂] Fₗ) →
                                                      DenseRange ⇑e₁ →
                                                        (∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖) →
                                                          DenseRange ⇑e₂ →
                                                            (∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖) →
                                                              Eₗ ≃SL[σ₁₂] Fₗ
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.val_mulMap_tmul : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (H : A.LinearDisjoint B) (a : ↥A) (b : ↥B), ↑(H.mulMap (a ⊗ₜ[R] b)) = ↑a * ↑b
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.instSubHom : {M N : AddCommGrpCat} → Sub (M ⟶ N)
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.instReflectsFiniteCoproductsOfReflectsFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteColimits F],
  CategoryTheory.Limits.ReflectsFiniteCoproducts F
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_singleton_mul_left_unit : ∀ {α : Type u} [inst : Semiring α] {a : α}, IsUnit a → ∀ (x : α), Ideal.span {a * x} = Ideal.span {x}
-- Mathlib.Topology.Defs.Filter
/-- Type class for compact spaces. Separation is sometimes included in the definition, especially
in the French literature, but we do not include it here.  -/
CompactSpace : (X : Type u_1) → [TopologicalSpace X] → Prop
-- Mathlib.CategoryTheory.SingleObj
/-- Reinterpret a monoid homomorphism `f : M → N` as a functor `(single_obj M) ⥤ (single_obj N)`.
See also `CategoryTheory.SingleObj.mapHom` for an equivalence between these types.  -/
MonoidHom.toFunctor : {M : Type u} →
  {N : Type v} →
    [inst : Monoid M] →
      [inst_1 : Monoid N] → (M →* N) → CategoryTheory.Functor (CategoryTheory.SingleObj M) (CategoryTheory.SingleObj N)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isNClique_singleton : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {a : α}, G.IsNClique n {a} ↔ n = 1
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.nullHomotopicMap_f : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₂ k₁ k₀ : ι},
  c.Rel k₂ k₁ →
    c.Rel k₁ k₀ →
      ∀ (hom : (i j : ι) → C.X i ⟶ D.X j),
        (Homotopy.nullHomotopicMap hom).f k₁ =
          CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (hom k₀ k₁) +
            CategoryTheory.CategoryStruct.comp (hom k₁ k₂) (D.d k₂ k₁)
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableAdd.measurable_const_add : ∀ {M : Type u_2} {inst : MeasurableSpace M} {inst_1 : Add M} [self : MeasurableAdd M] (c : M), Measurable fun x => c + x
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_inverse : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂),
  (CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence Φ X₂).inverse =
    (CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor Φ (Opposite.op X₂)).rightOp
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitBall.coe_eq_zero : ∀ {𝕜 : Type u_1} [inst : Zero 𝕜] [inst_1 : PseudoMetricSpace 𝕜] {a : ↑(Metric.ball 0 1)}, ↑a = 0 ↔ a = 0
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.ennrealOfReal : ∀ {p q r : ℝ}, p.HolderTriple q r → (ENNReal.ofReal p).HolderTriple (ENNReal.ofReal q) (ENNReal.ofReal r)
-- Mathlib.NumberTheory.Padics.RingHoms
_private.Mathlib.NumberTheory.Padics.RingHoms.0.PadicInt.appr.match_1.splitter : {p : ℕ} →
  [hp_prime : Fact (Nat.Prime p)] →
    (motive : ℤ_[p] → ℕ → Sort u_1) →
      (x : ℤ_[p]) → (x_1 : ℕ) → ((_x : ℤ_[p]) → motive _x 0) → ((x : ℤ_[p]) → (n : ℕ) → motive x n.succ) → motive x x_1
-- Mathlib.Algebra.Group.AddChar
/-- Additive characters `A → M` are the same thing as additive homomorphisms from `A` to
`Additive M`.  -/
AddChar.toAddMonoidHomEquiv : {A : Type u_1} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : Monoid M] → AddChar A M ≃ (A →+ Additive M)
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.HomRel.instIsStableUnderPostcompCompClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C),
  CategoryTheory.HomRel.IsStableUnderPostcomp (CategoryTheory.HomRel.CompClosure r)
-- Mathlib.FieldTheory.Galois.Profinite
/-- The categorical isomorphism between `profiniteGalGrp` and `lim Gal(L/k)` where `L` is a
`FiniteGaloisIntermediateField` ordered by inverse inclusion  -/
InfiniteGalois.profiniteGalGrpIsoLimit : (k : Type u_3) →
  (K : Type u_4) →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          [inst_3 : IsGalois k K] →
            InfiniteGalois.profiniteGalGrp k K ≅ ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.disjoint : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ.MutuallySingular ν → Disjoint μ ν
-- Mathlib.Data.Finset.NoncommProd
/-- Product of a `s : Finset α` mapped with `f : α → β` with `[Monoid β]`,
given a proof that `*` commutes on all elements `f x` for `x ∈ s`.  -/
Finset.noncommProd : {α : Type u_3} →
  {β : Type u_4} → [inst : Monoid β] → (s : Finset α) → (f : α → β) → (↑s).Pairwise (Function.onFun Commute f) → β
-- Init.Data.Option.Lemmas
Option.get_none : ∀ {α : Type u_1} (a : α) {h : none.isSome = true}, none.get h = a
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- A vertex group in a free connected groupoid is free. With some work one could drop the
connectedness assumption, by looking at connected components.  -/
IsFreeGroupoid.endIsFreeOfConnectedFree : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [CategoryTheory.IsConnected G] [IsFreeGroupoid G] (r : G),
  IsFreeGroup (CategoryTheory.End r)
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instSMulApply : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_2} [inst : SMul α ℝ] [inst_1 : SMul α ℂ]
  [inst_2 : IsScalarTower α ℝ ℂ], IsSMulApply α (CuspForm Γ k) UpperHalfPlane ℂ
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffAt_extChartAt : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {x : M},
  ContMDiffAt I (modelWithCornersSelf 𝕜 E) n (↑(extChartAt I x)) x
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.colimit.toCostructuredArrow_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : J),
  (CategoryTheory.Limits.colimit.toCostructuredArrow F).obj j =
    CategoryTheory.CostructuredArrow.mk (CategoryTheory.Limits.colimit.ι F j)
-- Std.Time.Duration
Std.Time.Duration.instCoeOffset_2 : Coe Std.Time.Minute.Offset Std.Time.Duration
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isValidSearchFrom_iff_isValidSearchFrom_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos}
  {l : List (String.Slice.Pattern.SearchStep s)},
  String.Slice.Pattern.Model.IsValidSearchFrom p pos l ↔
    String.Slice.Pattern.Model.IsValidSearchFrom (fun x => decide (p x)) pos l
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.comp_mapMon_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal]
  (X : CategoryTheory.Mon C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) X.X X.X)
      ((F.comp G).map CategoryTheory.MonObj.mul)
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- Given a face of a simplex, if a point bisects the angle between that face and each other face,
as measured at points shared between those faces between that point and its projections onto the
faces, that point is an excenter of the simplex.  -/
Affine.Simplex.exists_excenterExists_and_eq_excenter_of_forall_angle_orthogonalProjectionSpan_eq : ∀ {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) →
    ∀ {i₁ : Fin (n + 1)},
      (∀ (i₂ : Fin (n + 1)),
          i₂ ≠ i₁ →
            ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points),
              p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧
                EuclideanGeometry.angle p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) =
                  EuclideanGeometry.angle p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)) →
        ∃ signs, s.ExcenterExists signs ∧ p = s.excenter signs
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_zero : ∀ {w start len : ℕ}, BitVec.extractLsb' start len 0#w = 0#len
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.InferControlInfo.ofLetOrReassign : Array Lean.Ident →
  Option Lean.DoElem →
    Option (Lean.TSyntax `Lean.Parser.Term.doSeqIndent) →
      Option (Lean.TSyntax `Lean.Parser.Term.doSeqIndent) → Lean.Elab.TermElabM Lean.Elab.Do.ControlInfo
-- Mathlib.Data.Bool.Count
List.IsChain.length_sub_one_le_two_mul_count_bool : ∀ {l : List Bool}, List.IsChain (fun x1 x2 => x1 ≠ x2) l → ∀ (b : Bool), l.length - 1 ≤ 2 * List.count b l
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- The pointwise `star` of a non-unital subalgebra is a non-unital subalgebra.  -/
NonUnitalSubalgebra.instInvolutiveStar : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : StarRing A] → [inst_4 : Module R A] → [StarModule R A] → InvolutiveStar (NonUnitalSubalgebra R A)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.contains t.maxKey! = true
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
/-- a weaker version of `step_filterMap` that does not use dependent `match`
 -/
Std.Iter.val_step_filterMap : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {f : β → Option γ},
  ↑(Std.Iter.filterMap f it).step =
    match ↑it.step with
    | Std.IterStep.yield it' out =>
      match f out with
      | none => Std.IterStep.skip (Std.Iter.filterMap f it')
      | some out' => Std.IterStep.yield (Std.Iter.filterMap f it') out'
    | Std.IterStep.skip it' => Std.IterStep.skip (Std.Iter.filterMap f it')
    | Std.IterStep.done => Std.IterStep.done
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.antidiagonalTuple_zero_zero : List.Nat.antidiagonalTuple 0 0 = [![]]