mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.UInt.Lemmas
UInt64.ofNat_add : ∀ (a b : ℕ), UInt64.ofNat (a + b) = UInt64.ofNat a + UInt64.ofNat b
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_pi : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Preorder (α i)] {s : Set ι} {t : (i : ι) → Set (α i)},
  (∀ i ∈ s, (t i).OrdConnected) → (s.pi t).OrdConnected
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sUnion_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] (S : Set (Set β)) (t : Set β), ⋃₀ S -ᵥ t = ⋃ s ∈ S, s -ᵥ t
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.equivPair_symm : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] (i : ι) (p : Monoid.CoprodI.Word.Pair M i),
  (Monoid.CoprodI.Word.equivPair i).symm p = Monoid.CoprodI.Word.rcons p
-- Aesop.Rule.Basic
Aesop.Rule.mk.injEq : ∀ {α : Type} (name : Aesop.RuleName) (indexingMode : Aesop.IndexingMode) (pattern? : Option Aesop.RulePattern)
  (extra : α) (tac : Aesop.RuleTacDescr) (name_1 : Aesop.RuleName) (indexingMode_1 : Aesop.IndexingMode)
  (pattern?_1 : Option Aesop.RulePattern) (extra_1 : α) (tac_1 : Aesop.RuleTacDescr),
  ({ name := name, indexingMode := indexingMode, pattern? := pattern?, extra := extra, tac := tac } =
      { name := name_1, indexingMode := indexingMode_1, pattern? := pattern?_1, extra := extra_1, tac := tac_1 }) =
    (name = name_1 ∧ indexingMode = indexingMode_1 ∧ pattern? = pattern?_1 ∧ extra = extra_1 ∧ tac = tac_1)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasDerivWithinAt.cpow_const : ∀ {f : ℂ → ℂ} {s : Set ℂ} {f' x c : ℂ},
  HasDerivWithinAt f f' s x → f x ∈ Complex.slitPlane → HasDerivWithinAt (fun x => f x ^ c) (c * f x ^ (c - 1) * f') s x
-- Mathlib.RingTheory.RingHomProperties
RingHom.CodescendsAlong.includeRight : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  (Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) (R S T : Type u)
  [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T],
  (RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => P) fun {R S} [CommRing R] [CommRing S] => Q) →
    Q (algebraMap R T) → P Algebra.TensorProduct.includeRight.toRingHom → P (algebraMap R S)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_naturality_left_assoc : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.BraidedCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
      (CategoryTheory.CategoryStruct.comp (β_ Y Z).hom h) =
    CategoryTheory.CategoryStruct.comp (β_ X Z).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) h)
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
associatedPrimes.eq_empty_of_subsingleton : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Subsingleton M], associatedPrimes R M = ∅
-- Std.Sync.Notify
Std.Notify.Consumer.select.inj : ∀ {α : Type} {finished finished_1 : Std.Async.Waiter α},
  Std.Notify.Consumer.select finished = Std.Notify.Consumer.select finished_1 → finished = finished_1
-- Mathlib.Geometry.Euclidean.MongePoint
/-- **Sylvester's theorem**: The position of the Monge point relative to the circumcenter via the
sum of vectors to the vertices.  -/
Affine.Simplex.smul_mongePoint_vsub_circumcenter_eq_sum_vsub : ∀ {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 : ℕ} (s : Affine.Simplex ℝ P (n + 2)),
  (n + 1) • (s.mongePoint -ᵥ s.circumcenter) = ∑ i, (s.points i -ᵥ s.circumcenter)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Comma.costructuredArrowSndInclusion_obj_left_hom : ∀ {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) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)),
  ((CategoryTheory.Comma.costructuredArrowSndInclusion L R b).obj X).left.hom = X.hom
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.instIsRegularEpiUnopOfIsRegularMonoOpposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [CategoryTheory.IsRegularMono f],
  CategoryTheory.IsRegularEpi f.unop
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The differential on the `r`th page of the spectral sequence.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    (r : ℤ) →
                      (pq pq' : κ) →
                        (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD._auto_1) →
                          CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX X data r pq hr ⟶
                            CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX X data r pq' hr
-- Mathlib.Order.Filter.Finite
Filter.mem_iInf : ∀ {α : Type u} {ι : Type u_2} {s : ι → Filter α} {U : Set α},
  U ∈ ⨅ i, s i ↔ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote'.go.eq_def : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (r : α)
  (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.Poly.denote'.go ctx r p =
    match p with
    | Lean.Grind.Linarith.Poly.nil => r
    | Lean.Grind.Linarith.Poly.add 1 v p =>
      Lean.Grind.Linarith.Poly.denote'.go ctx (r + Lean.Grind.Linarith.Var.denote ctx v) p
    | Lean.Grind.Linarith.Poly.add k v p =>
      Lean.Grind.Linarith.Poly.denote'.go ctx (r + k • Lean.Grind.Linarith.Var.denote ctx v) p
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.mem_inv_smul_finset_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  {s : Finset β} {a : α} {b : β}, a ≠ 0 → (b ∈ a⁻¹ • s ↔ a • b ∈ s)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.arrowArrowEquivalence_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Square.arrowArrowEquivalence.inverse = CategoryTheory.Square.fromArrowArrowFunctor
-- Mathlib.Algebra.Field.Subfield.Basic
/-- Product of a list of elements in a subfield is in the subfield.  -/
Subfield.list_prod_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {l : List K}, (∀ x ∈ l, x ∈ s) → l.prod ∈ s
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.FibrantObject.homMk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] {X Y : C} [inst_3 : HomotopicalAlgebra.IsFibrant X]
  [inst_4 : HomotopicalAlgebra.IsFibrant Y]
  (f : HomotopicalAlgebra.FibrantObject.mk X ⟶ HomotopicalAlgebra.FibrantObject.mk Y),
  ∃ g, f = HomotopicalAlgebra.FibrantObject.homMk g
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.adj_le_reachable : ∀ {V : Type u} (G : SimpleGraph V), G.Adj ≤ G.Reachable
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.binaryProductLimitCone_cone_pt : ∀ (G H : AddCommGrpCat), (G.binaryProductLimitCone H).cone.pt = AddCommGrpCat.of (↑G × ↑H)
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidalFunctorComp_isMonoidal : ∀ {M : Type u} [inst : Monoid M] {N : Type u'} [inst_1 : Monoid N] {K : Type u} [inst_2 : Monoid K] (F : M →* N)
  (G : N →* K), CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.Discrete.monoidalFunctorComp F G).hom
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceTypeDefinitionParams : Lean.Lsp.FileSource Lean.Lsp.TypeDefinitionParams
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.map_surjective_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (Q : Type u_4) [inst_4 : CommSemiring Q] [inst_5 : Algebra P Q] (f : R →+* P) (r : R)
  [inst_6 : IsLocalization.Away r S] [inst_7 : IsLocalization.Away (f r) Q],
  Function.Surjective ⇑(IsLocalization.Away.map S Q f r) ↔ ∀ (a : P), ∃ b m, f b = f r ^ m * a
-- Mathlib.Topology.Algebra.Group.Matrix
Matrix.SpecialLinearGroup.range_toGL : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {A : Type u_4} [inst_2 : CommRing A],
  Set.range ⇑Matrix.SpecialLinearGroup.toGL = ⇑Matrix.GeneralLinearGroup.det ⁻¹' {1}
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- An alternate constructor for strictly unitary pseudofunctors that does not
require the `mapId` fields, and that adapts the `map₂_leftUnitor` and
`map₂_rightUnitor` to the fact that the functor is strictly unitary.  -/
CategoryTheory.StrictlyUnitaryPseudofunctor.mk' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.StrictlyUnitaryPseudofunctorCore B C → CategoryTheory.StrictlyUnitaryPseudofunctor B C
-- Mathlib.Algebra.Field.ZMod
/-- Field structure on `ZMod p` if `p` is prime.  -/
ZMod.instField : (p : ℕ) → [hp : Fact (Nat.Prime p)] → Field (ZMod p)
-- Lean.IdentifierSuggestion
/-- Create the extension mapping incorrect identifiers to the existing identifiers we want to suggest as
replacements. This association is the opposite of the usual mapping for `ParametricAttribute`
attributes.
 -/
_private.Lean.IdentifierSuggestion.0.Lean.mkIncorrectToExisting : IO (Lean.PersistentEnvExtension (Lean.Name × Array Lean.Name) (Lean.Name × Array Lean.Name) (Lean.NameMap Lean.NameSet))
-- Mathlib.GroupTheory.Congruence.Defs
/-- Additive congruence relations equal the
smallest additive congruence relation in which they are contained.  -/
AddCon.addConGen_of_addCon : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M), addConGen ⇑c = c
-- Lean.Server.FileWorker.Utils
/-- Diagnostics accumulated during snapshot reporting.  -/
Lean.Server.FileWorker.DiagnosticsState.diags : Lean.Server.FileWorker.DiagnosticsState → Lean.PersistentArray Lean.Widget.InteractiveDiagnostic
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_inter!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.inter! m₂).getKey! k = default
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent_bot : ∀ {α : Type u_1} [Nontrivial α] (u : α), ⊥.eccent u = ⊤
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.mk : (carrier : Type u) → [str : Monoid carrier] → MonCat
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- The covering homotopy theorem: if `p : E ⟶ B` is a fibration,
`l₀ : A ⟶ E` is a morphism, if there is a left homotopy `h` between
the composition `f₀ := l₀ ≫ p` and a morphism `f₁ : A ⟶ B`,
then there exists a morphism `l₁ : A ⟶ E` and a left homotopy `h'` from
`l₀` to `l₁` which is compatible with `h` (in particular, `l₁ ≫ p = f₁`).  -/
HomotopicalAlgebra.Cylinder.LeftHomotopy.covering_homotopy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A E B : C}
  {P : HomotopicalAlgebra.Cylinder A} {f₀ f₁ : A ⟶ B} [HomotopicalAlgebra.IsCofibrant A] [P.IsGood]
  (h : P.LeftHomotopy f₀ f₁) (p : E ⟶ B) [HomotopicalAlgebra.Fibration p] (l₀ : A ⟶ E),
  autoParam (CategoryTheory.CategoryStruct.comp l₀ p = f₀)
      HomotopicalAlgebra.Cylinder.LeftHomotopy.covering_homotopy._auto_1 →
    ∃ l₁ h', CategoryTheory.CategoryStruct.comp h'.h p = h.h
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAt.of_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} {s₁ e₁ : s.Pos}
  {s₂ e₂ : t.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat s₁ e₁ →
    ∀ (h₁ : s.copy = t.copy),
      s₁.cast h₁ = s₂ → e₁.cast h₁ = e₂ → String.Slice.Pattern.Model.IsLongestRevMatchAt pat s₂ e₂
-- Aesop.Tree.State
Aesop.RappRef.markProven : Aesop.RappRef → BaseIO Unit
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_intCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (z : ℤ), ⌊↑z⌋ = z
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- A section of the projection `I → I/I²`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.f : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b → P.toExtension.Cotangent → ↥P.toExtension.ker
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- `eval r`, regarded as a ring homomorphism from `R[X]` to `R`.  -/
Polynomial.evalRingHom : {R : Type u} → [inst : CommSemiring R] → R → Polynomial R →+* R
-- Mathlib.Data.Nat.Factorization.Induction
/-- Given `P 0`, `P 1`, `P p` for all primes, and a way to extend `P a` and `P b` to
`P (a * b)`, we can define `P` for all natural numbers.  -/
Nat.recOnMul : {motive : ℕ → Sort u_1} →
  motive 0 →
    motive 1 →
      ((p : ℕ) → Nat.Prime p → motive p) → ((a b : ℕ) → motive a → motive b → motive (a * b)) → (a : ℕ) → motive a
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
LinearMap.dualProd.toQuadraticForm : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.BilinMap.toQuadraticMap (LinearMap.dualProd R M) = 2 • QuadraticForm.dualProd R M
-- Mathlib.CategoryTheory.Sites.Whiskering
_private.Mathlib.CategoryTheory.Sites.Whiskering.0.CategoryTheory.GrothendieckTopology.Cover.multicospanComp.match_1.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (S : J.Cover X) (motive : CategoryTheory.Limits.WalkingMulticospan S.shape → Sort u_3) (a : S.shape.R)
  (h_1 : (a : S.shape.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left a))
  (h_2 : (a : S.shape.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right a)),
  (match CategoryTheory.Limits.WalkingMulticospan.right a with
    | CategoryTheory.Limits.WalkingMulticospan.left a => h_1 a
    | CategoryTheory.Limits.WalkingMulticospan.right a => h_2 a) =
    h_2 a
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The forgetful functor from additive group objects to additive monoid objects
is fully faithful.  -/
CategoryTheory.AddGrp.fullyFaithfulForget₂Mon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → (CategoryTheory.AddGrp.forget₂Mon C).FullyFaithful
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_add_eq_top_iff : ∀ {α : Type u} [inst : Add α] {y : WithTop α} {a : α}, ↑a + y = ⊤ ↔ y = ⊤
-- Init.Data.AC
Lean.Data.AC.evalList.eq_def : ∀ {α : Sort u_1} (β : Sort u) [inst : Lean.Data.AC.EvalInformation α β] (ctx : α) (x : List ℕ),
  Lean.Data.AC.evalList β ctx x =
    match x with
    | [] => Lean.Data.AC.EvalInformation.arbitrary ctx
    | [x] => Lean.Data.AC.EvalInformation.evalVar ctx x
    | x :: xs =>
      Lean.Data.AC.EvalInformation.evalOp ctx (Lean.Data.AC.EvalInformation.evalVar ctx x)
        (Lean.Data.AC.evalList β ctx xs)
-- Std.Time.Internal.Bounded
/-- Convert a `Fin` to a `Bounded.LE`.
 -/
Std.Time.Internal.Bounded.LE.ofFin' : {hi lo : ℕ} → Fin hi.succ → lo ≤ hi → Std.Time.Internal.Bounded.LE ↑lo ↑hi
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- The normed algebra structure on `Matrix n n 𝕜` arising from the operator norm given by the
identification with (continuous) linear endomorphisms of `EuclideanSpace 𝕜 n`.  -/
Matrix.instL2OpNormedSpace : {𝕜 : Type u_1} →
  {m : Type u_2} →
    {n : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : Fintype m] → [inst_2 : Fintype n] → [inst_3 : DecidableEq n] → NormedSpace 𝕜 (Matrix m n 𝕜)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_inv_rpow : ∀ {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] (a : A) (x : ℝ),
  x ≠ 0 → autoParam (IsStrictlyPositive a) CFC.rpow_inv_rpow._auto_1 → (a ^ x⁻¹) ^ x = a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_eq_minKeyD_default : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.minKey! = t.minKeyD default
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁ : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ}
  (s :
    CategoryTheory.Limits.Cone
      ((CategoryTheory.StructuredArrow.proj (Opposite.op { len := n }) (SimplexCategory.Truncated.inclusion 2).op).comp
        ((SimplexCategory.Truncated.inclusion 2).op.comp X)))
  (x : s.pt) (i : ℕ) (hi : i < n),
  (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc ⟨i, hi⟩).op))
      (SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift sx s x) =
    (CategoryTheory.ConcreteCategory.hom
        (s.π.app
          (SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂ (SimplexCategory.mkOfSucc ⟨i, hi⟩)
            SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁._proof_1)))
      x
-- Mathlib.CategoryTheory.LocallyDirected
/-- **Alias** of `CategoryTheory.Functor.IsLocallyDirected.cond`. -/
CategoryTheory.Functor.exists_map_eq_of_isLocallyDirected : ∀ {J : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} J} (F : CategoryTheory.Functor J (Type u_2))
  [self : F.IsLocallyDirected] {i j k : J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j),
  (CategoryTheory.ConcreteCategory.hom (F.map fi)) xi = (CategoryTheory.ConcreteCategory.hom (F.map fj)) xj →
    ∃ l fli flj x,
      (CategoryTheory.ConcreteCategory.hom (F.map fli)) x = xi ∧
        (CategoryTheory.ConcreteCategory.hom (F.map flj)) x = xj
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered additive monoids M, N, the natural inclusion
ordered homomorphism from M to M × N.  -/
OrderAddMonoidHom.inl : (α : Type u_1) →
  (β : Type u_2) →
    [inst : AddMonoid α] → [inst_1 : PartialOrder α] → [inst_2 : AddMonoid β] → [inst_3 : Preorder β] → α →+o α × β
-- Init.Data.Array.Lemmas
/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts.  -/
Array.reverse_flatten : ∀ {α : Type u_1} {xss : Array (Array α)}, xss.flatten.reverse = (Array.map Array.reverse xss).reverse.flatten
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardNatIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] [inst_3 : G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S)
  (α : F ≅ G), (SheafOfModules.pushforwardNatIso φ α).hom = SheafOfModules.pushforwardNatTrans φ α.hom
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.mk.injEq : ∀ {dir : Std.Http.Protocol.H1.Direction} (state : Std.Http.Protocol.H1.Reader.State dir) (input : ByteArray.Iterator)
  (messageHead : Std.Http.Protocol.H1.Message.Head dir) (messageCount bodyBytesRead headerBytesRead : ℕ)
  (noMoreInput : Bool) (state_1 : Std.Http.Protocol.H1.Reader.State dir) (input_1 : ByteArray.Iterator)
  (messageHead_1 : Std.Http.Protocol.H1.Message.Head dir) (messageCount_1 bodyBytesRead_1 headerBytesRead_1 : ℕ)
  (noMoreInput_1 : Bool),
  ({ state := state, input := input, messageHead := messageHead, messageCount := messageCount,
        bodyBytesRead := bodyBytesRead, headerBytesRead := headerBytesRead, noMoreInput := noMoreInput } =
      { state := state_1, input := input_1, messageHead := messageHead_1, messageCount := messageCount_1,
        bodyBytesRead := bodyBytesRead_1, headerBytesRead := headerBytesRead_1, noMoreInput := noMoreInput_1 }) =
    (state = state_1 ∧
      input = input_1 ∧
        messageHead = messageHead_1 ∧
          messageCount = messageCount_1 ∧
            bodyBytesRead = bodyBytesRead_1 ∧ headerBytesRead = headerBytesRead_1 ∧ noMoreInput = noMoreInput_1)
-- Mathlib.Topology.Category.CompactlyGenerated
/-- The underlying topological space of an object of `CompactlyGenerated`.  -/
CompactlyGenerated.toTop : CompactlyGenerated → TopCat
-- Mathlib.Analysis.Convex.Body
ConvexBody.instDistribMulActionReal : {V : Type u_1} →
  [inst : TopologicalSpace V] →
    [inst_1 : AddCommGroup V] →
      [inst_2 : Module ℝ V] → [ContinuousSMul ℝ V] → [inst_4 : ContinuousAdd V] → DistribMulAction ℝ (ConvexBody V)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidOpenTextDocumentParams.mk.sizeOf_spec : ∀ (textDocument : Lean.Lsp.TextDocumentItem), sizeOf { textDocument := textDocument } = 1 + sizeOf textDocument
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type is an additive group if `β` is an additive group.  -/
FunLike.addGroup : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] →
            [inst_3 : SMul ℕ F] →
              [inst_4 : Neg F] →
                [inst_5 : Sub F] →
                  [inst_6 : SMul ℤ F] →
                    [inst_7 : AddGroup β] →
                      [IsZeroApply F α β] →
                        [IsAddApply F α β] →
                          [IsNegApply F α β] →
                            [IsSubApply F α β] → [IsSMulApply ℕ F α β] → [IsSMulApply ℤ F α β] → AddGroup F
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `ContDiffOn.inv` -/
ContDiffOn.fun_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝕜' : Type u_4} [inst_3 : NormedField 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'},
  ContDiffOn 𝕜 n f s → (∀ x ∈ s, f x ≠ 0) → ContDiffOn 𝕜 n (fun i => (f i)⁻¹) s
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instLeftCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : LeftCancelMonoid α],
  OrderDual.instLeftCancelMonoid = { toMonoid := OrderDual.instMonoid, toIsLeftCancelMul := ⋯ }
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_stabilizer : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {α : Type u_2} [inst_1 : MulAction G α] (a : α),
  (∀ (h : ↥H), h • a = a → h = 1) → (∀ (g : G), ∃ h, h • g • a = a) → H.IsComplement' (MulAction.stabilizer G a)
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.cast.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {i j : ℕ}
  (h : i = j), TensorPower.cast R M h = PiTensorProduct.reindex R (fun x => M) (finCongr h)