mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- The transitivity of homotopy between morphisms of short complexes.  -/
CategoryTheory.ShortComplex.Homotopy.trans : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ φ₃ : S₁ ⟶ S₂} →
          CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ →
            CategoryTheory.ShortComplex.Homotopy φ₂ φ₃ → CategoryTheory.ShortComplex.Homotopy φ₁ φ₃
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.keys_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → Bool}, (Std.ExtTreeMap.filter (fun k x => f k) t).keys = List.filter f t.keys
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.addSimpEntry : Lean.Meta.SimpTheorems → Lean.Meta.SimpEntry → Lean.Meta.SimpTheorems
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.relabel_bot : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ},
  FirstOrder.Language.BoundedFormula.relabel g ⊥ = ⊥
-- Batteries.Data.List.Basic
/-- `O(|l|)`. Inserts `a` in `l` right before the first element such that `p` is true, or at the end of
the list if `p` always false on `l`.
 -/
List.insertP : {α : Type u_1} → (α → Bool) → α → List α → List α
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id_assoc : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ)
  (h : CategoryTheory.Limits.IsZero ((X'.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₃₄))))
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id._auto_3) {Z : C}
  (h_1 :
    X'.E (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂) (CategoryTheory.homOfLE hi₂₃) n₀ n₁ n₂ hn₁ hn₂ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp
        (X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv h_1) =
    h_1
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.IsMulRightInvariant.mk : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] {μ : MeasureTheory.Measure G},
  (∀ (g : G), MeasureTheory.Measure.map (fun x => x * g) μ = μ) → μ.IsMulRightInvariant
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- If `g` maps a second argument of 0 to 0, summing it over the
result of `onFinset` is the same as summing it over the original `Finset`.  -/
Finsupp.onFinset_sum : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {s : Finset α} {f : α → M}
  {g : α → M → N} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s),
  (∀ (a : α), g a 0 = 0) → (Finsupp.onFinset s f hf).sum g = ∑ a ∈ s, g a (f a)
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
hasSum_div_const_iff : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a₁ a₂ : α}, a₂ ≠ 0 → (HasSum (fun i => f i / a₂) (a₁ / a₂) L ↔ HasSum f a₁ L)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Prod
MeasureTheory.MemLp.comp_snd : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {ν : MeasureTheory.Measure β} {p : ENNReal} {f : β → ε},
  MeasureTheory.MemLp f p ν →
    ∀ (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.SFinite ν],
      MeasureTheory.MemLp (fun x => f x.2) p (μ.prod ν)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instMonoidalCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.AddGrp.instMonoidalCategory =
    { toMonoidalCategoryStruct := CategoryTheory.AddGrp.instMonoidalCategoryStruct, tensorHom_def := ⋯,
      id_tensorHom_id := ⋯, tensorHom_comp_tensorHom := ⋯, whiskerLeft_id := ⋯, id_whiskerRight := ⋯,
      associator_naturality := ⋯, leftUnitor_naturality := ⋯, rightUnitor_naturality := ⋯, pentagon := ⋯,
      triangle := ⋯ }
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.toQ : {α : Type u} → [inst : Lean.Grind.Semiring α] → α → Lean.Grind.Ring.OfSemiring.Q α
-- Lean.Parser.Extra
Lean.Parser.withAntiquotSpliceAndSuffix.formatter : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableSMul₂_opposite_of_mul : ∀ {M : Type u_2} [inst : Mul M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M], MeasurableSMul₂ Mᵐᵒᵖ M
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.pIntegral_faulhaber_sum : ∀ {k p : ℕ},
  k > 0 →
    ∀ [inst : Fact (Nat.Prime p)],
      (∀ (m : ℕ),
          0 < m → m < k → Bernoulli.pIntegral✝ p (bernoulli (2 * m) + Bernoulli.vonStaudtIndicator✝ (2 * m) p / ↑p)) →
        Bernoulli.pIntegral✝ p
          (∑ i ∈ Finset.range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1))
-- Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Units.instChartedSpace : {R : Type u_1} → [inst : NormedRing R] → [CompleteSpace R] → ChartedSpace R Rˣ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
groupCohomology.mono_δ_of_isZero : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) (n : ℕ),
  CategoryTheory.Limits.IsZero (groupCohomology X.X₂ n) → CategoryTheory.Mono (groupCohomology.δ hX n (n + 1) ⋯)
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.comp_assoc : ∀ {V : Type u} [inst : Quiver V] {a b c d : V} (p : Quiver.Path a b) (q : Quiver.Path b c) (r : Quiver.Path c d),
  (p.comp q).comp r = p.comp (q.comp r)
-- Batteries.Data.List.Lemmas
List.findIdxNth_lt_findIdxNth_iff_of_lt_countP : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {m : ℕ} {xs : List α},
  n < List.countP p xs → (List.findIdxNth p xs n < List.findIdxNth p xs m ↔ n < m)
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_eq_bot : ∀ {V : Type u_1} {G : SimpleGraph V} {s : Set (Sym2 V)}, G.deleteEdges s = ⊥ ↔ G.edgeSet ⊆ s
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : SizeOf C] [inst_2 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W₁ x)]
  [inst_3 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W₂ x)] (Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C)
  (i : CategoryTheory.Arrow.leftFunc ⟶ Z) (p : Z ⟶ CategoryTheory.Arrow.rightFunc)
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp i p = CategoryTheory.Arrow.leftToRight)
      CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac._autoParam)
  (hi : ∀ (f : CategoryTheory.Arrow C), W₁ (i.app f)) (hp : ∀ (f : CategoryTheory.Arrow C), W₂ (p.app f)),
  sizeOf { Z := Z, i := i, p := p, fac := fac, hi := hi, hp := hp } = 1 + sizeOf Z + sizeOf i + sizeOf p + sizeOf fac
-- Batteries.Data.MLList.Basic
/-- Iterate through the elements of `Fin n`.  -/
MLList.fin : {m : Type → Type} → (n : ℕ) → MLList m (Fin n)
-- Mathlib.Algebra.Ring.Prod
Prod.instNonUnitalRing : {R : Type u_1} → {S : Type u_3} → [NonUnitalRing R] → [NonUnitalRing S] → NonUnitalRing (R × S)
-- Mathlib.Data.List.Fold
List.foldl1_eq_foldr1 : ∀ {α : Type u_1} {l : List α} {f : α → α → α} [ha : Std.Associative f] {a b : α},
  f (List.foldl f a l) b = f a (List.foldr f b l)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.IsAddMonHom.addMonoidHom.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (f f_1 : M ⟶ N) (e_f : f = f_1)
  [inst_4 : CategoryTheory.IsAddMonHom f] (X : C),
  CategoryTheory.IsAddMonHom.addMonoidHom f X = CategoryTheory.IsAddMonHom.addMonoidHom f_1 X
-- Init.Data.Dyadic.Basic
Dyadic.toRat_zero : Dyadic.toRat 0 = 0
-- Mathlib.Algebra.Colimit.DirectLimit
/-- The canonical map from a component to the direct limit.  -/
DirectLimit.NonUnitalStarRing.of : {ι : Type u_2} →
  [inst : Preorder ι] →
    (G : ι → Type u_3) →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)] →
                  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] →
                    [inst_6 : (i : ι) → StarRing (G i)] →
                      [inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] →
                        [inst_8 : Nonempty ι] → (i : ι) → G i →⋆ₙ+* DirectLimit G f
-- Init.GrindInstances.ToInt
Lean.Grind.instLEFinCoOfNatIntCast : ∀ {n : ℕ}, Lean.Grind.ToInt.LE (Fin n) (Lean.Grind.IntInterval.co 0 ↑n)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.mk_mul_mk : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Ring R] (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R),
  { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } * { re := b₁, imI := b₂, imJ := b₃, imK := b₄ } =
    { re := a₁ * b₁ + c₁ * a₂ * b₂ + c₃ * a₃ * b₃ + c₂ * c₃ * a₃ * b₄ - c₁ * c₃ * a₄ * b₄,
      imI := a₁ * b₂ + a₂ * b₁ + c₂ * a₂ * b₂ - c₃ * a₃ * b₄ + c₃ * a₄ * b₃,
      imJ := a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ + c₂ * a₃ * b₂ - c₁ * a₄ * b₂,
      imK := a₁ * b₄ + a₂ * b₃ + c₂ * a₂ * b₄ - a₃ * b₂ + a₄ * b₁ }
-- Mathlib.Data.Nat.Prime.Defs
/-- `Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  -/
Nat.Prime : ℕ → Prop
-- Mathlib.Analysis.Normed.Group.Basic
/-- An analogue of `norm_le_add_norm_add` for the addition from the left.  -/
norm_le_add_norm_add' : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (u v : E), ‖v‖ ≤ ‖u + v‖ + ‖u‖
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_pos : ∀ {x : ENNReal}, 0 < ↑x ↔ 0 < x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_eq_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k fallback : α}, t.contains k = true → t.getKeyD k fallback = k
-- Std.Sat.AIG.Basic
_private.Std.Sat.AIG.Basic.0.Std.Sat.AIG.toGraphviz.go.match_1.splitter : {α : Type} →
  (motive : Std.Sat.AIG.Decl α → Sort u_1) →
    (x : Std.Sat.AIG.Decl α) →
      (x = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false) →
        ((idx : α) → x = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx)) →
          ((lhs rhs : Std.Sat.AIG.Fanin) → x = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)) →
            motive x
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.algEquivOfTranscendental_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : L)
  (h : Transcendental K f) (u : RatFunc K),
  ↑((RatFunc.algEquivOfTranscendental f h) u) = (Polynomial.aeval f) u.num / (Polynomial.aeval f) u.denom
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mapCongr_rfl : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y),
  CategoryTheory.Over.mapCongr f f ⋯ = CategoryTheory.Iso.refl (CategoryTheory.Over.map f)
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
WeakDual.CharacterSpace.ext_ker : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommRing 𝕜] [inst_1 : NoZeroDivisors 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [inst_3 : ContinuousAdd 𝕜] [inst_4 : ContinuousConstSMul 𝕜 𝕜] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : Algebra 𝕜 A] {φ ψ : ↑(WeakDual.characterSpace 𝕜 A)}, RingHom.ker φ = RingHom.ker ψ → φ = ψ
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v))
  (Y : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)),
  (CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver A).obj Y =
    CategoryTheory.CostructuredArrow.mk (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA Y)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_union_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α},
  min a b < max c d → min c d < max a b → Set.Ioo a b ∪ Set.Ioo c d = Set.Ioo (min a c) (max b d)
-- Init.Data.Array.Lemmas
Array.foldrM_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → β → m β} {b : β}
  {xs ys : Array α},
  Array.foldrM f b (xs ++ ys) = do
    let init ← Array.foldrM f b ys
    Array.foldrM f init xs
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- For graphs `G`, `H`, `G ≤ H` iff `∀ a b, G.Adj a b → H.Adj a b`.  -/
SimpleGraph.instLE : {V : Type u} → LE (SimpleGraph V)
-- Mathlib.Analysis.Calculus.FDeriv.Comp
Differentiable.comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {g : F → G},
  Differentiable 𝕜 g → Differentiable 𝕜 f → Differentiable 𝕜 (g ∘ f)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_4.eq_9 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr) (k : ℕ)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match a.pow k with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.intCast k => h_2 k
    | Lean.Grind.CommRing.Expr.natCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_9 a k
-- Lean.DocString.Links
/-- The valid domain abbreviations in the manual.  -/
Lean.manualDomains : List String
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.mul_sub_left_left_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime (y * z - x) y ↔ IsRelPrime x y
-- Mathlib.Data.Set.Card
Set.ncard_eq_succ : ∀ {α : Type u_1} {s : Set α} {n : ℕ},
  autoParam s.Finite Set.ncard_eq_succ._auto_1 → (s.ncard = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n)
-- Mathlib.Topology.Compactness.SigmaCompact
/-- A subset `s ⊆ X` is called **σ-compact** if it is the union of countably many compact sets.  -/
IsSigmaCompact : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.mk.injEq : ∀ {β : Type} (machine : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving)
  (requestStream : Std.Http.Body.Stream) (keepAliveTimeout : Option Std.Time.Millisecond.Offset)
  (currentTimeout : Std.Time.Millisecond.Offset) (headerTimeout : Option Std.Time.Timestamp)
  (response : Std.Channel (Except IO.Error (Std.Http.Response β))) (respStream : Option β) (requiresData : Bool)
  (expectData : Option ℕ) (handlerDispatched : Bool) (pendingHead : Option Std.Http.Request.Head)
  (machine_1 : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving)
  (requestStream_1 : Std.Http.Body.Stream) (keepAliveTimeout_1 : Option Std.Time.Millisecond.Offset)
  (currentTimeout_1 : Std.Time.Millisecond.Offset) (headerTimeout_1 : Option Std.Time.Timestamp)
  (response_1 : Std.Channel (Except IO.Error (Std.Http.Response β))) (respStream_1 : Option β) (requiresData_1 : Bool)
  (expectData_1 : Option ℕ) (handlerDispatched_1 : Bool) (pendingHead_1 : Option Std.Http.Request.Head),
  ({ machine := machine, requestStream := requestStream, keepAliveTimeout := keepAliveTimeout,
        currentTimeout := currentTimeout, headerTimeout := headerTimeout, response := response,
        respStream := respStream, requiresData := requiresData, expectData := expectData,
        handlerDispatched := handlerDispatched, pendingHead := pendingHead } =
      { machine := machine_1, requestStream := requestStream_1, keepAliveTimeout := keepAliveTimeout_1,
        currentTimeout := currentTimeout_1, headerTimeout := headerTimeout_1, response := response_1,
        respStream := respStream_1, requiresData := requiresData_1, expectData := expectData_1,
        handlerDispatched := handlerDispatched_1, pendingHead := pendingHead_1 }) =
    (machine = machine_1 ∧
      requestStream = requestStream_1 ∧
        keepAliveTimeout = keepAliveTimeout_1 ∧
          currentTimeout = currentTimeout_1 ∧
            headerTimeout = headerTimeout_1 ∧
              response = response_1 ∧
                respStream = respStream_1 ∧
                  requiresData = requiresData_1 ∧
                    expectData = expectData_1 ∧ handlerDispatched = handlerDispatched_1 ∧ pendingHead = pendingHead_1)
-- Lean.Hygiene
Lean.Unhygienic.Context.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (scope : Lean.MacroScope), sizeOf { ref := ref, scope := scope } = 1 + sizeOf ref + sizeOf scope
-- Mathlib.Algebra.Azumaya.Basic
IsAzumaya.id : ∀ (R : Type u_1) [inst : CommSemiring R], IsAzumaya R R
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.smul_set_ae_le : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) {s t : Set α},
  c • s ≤ᵐ[μ] c • t ↔ s ≤ᵐ[μ] t
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
/-- **Alias** of `Asymptotics.isEquivalent_of_tendsto_one`. -/
Asymptotics.isEquivalent_of_tendsto_one' : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] {u v : α → β} {l : Filter α},
  Filter.Tendsto (u / v) l (nhds 1) → Asymptotics.IsEquivalent l u v
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.exists_le_of_sum_le : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] {f g : ι → M} {s : Finset ι}
  [IsOrderedCancelAddMonoid M], s.Nonempty → ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i → ∃ i ∈ s, f i ≤ g i
-- Mathlib.Algebra.Order.Module.Defs
smul_nonpos_iff_nonpos_of_pos_right : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosMono α β] [SMulPosReflectLE α β], 0 < b → (a • b ≤ 0 ↔ a ≤ 0)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.map_intCast : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M) (n : ℤ), D ↑n = 0
-- Mathlib.RingTheory.WittVector.IsPoly
_private.Mathlib.RingTheory.WittVector.IsPoly.0.WittVector.Tactic.getLocalOrIntro : Lean.Term → Lean.Elab.Tactic.TacticM Lean.FVarId
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_nnnorm_lt_one : ∀ (α : Type u_2) [inst : NontriviallyNormedField α], ∃ x, 0 < ‖x‖₊ ∧ ‖x‖₊ < 1
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.inv : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (self : CategoryTheory.Subgroupoid C) {c d : C} {p : c ⟶ d},
  p ∈ self.arrows c d → CategoryTheory.Groupoid.inv p ∈ self.arrows d c
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.zero_def : Real.zero✝ = { cauchy := 0 }
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.getKey?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α),
  m.getKey? a = if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.getKey? ⟨m, h⟩ a else none
-- Mathlib.Data.Set.Subsingleton
/-- A set `s` is `Set.Nontrivial` if it has at least two distinct elements.  -/
Set.Nontrivial : {α : Type u} → Set α → Prop
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.instPreservesLimitsOfSizeFunctorOppositeAbToPresheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u₁ v, max u₁ v, max (max (max u u₁) (v + 1)) v₁,
      max (max u₁ (v + 1)) v₁}
    (PresheafOfModules.toPresheaf R)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instMonoObjWalkingSpanCompSchemeSpanForgetNoneWalkingPairSomeMapInitOfIsOpenImmersion : ∀ {U X Y : AlgebraicGeometry.Scheme} (f : U ⟶ X) (g : U ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f]
  [AlgebraicGeometry.IsOpenImmersion g] (i : CategoryTheory.Limits.WalkingPair),
  CategoryTheory.Mono
    (((CategoryTheory.Limits.span f g).comp AlgebraicGeometry.Scheme.forget).map
      (CategoryTheory.Limits.WidePushoutShape.Hom.init i))
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.mk.inj : ∀ {α : Type u_4} {inst : TopologicalSpace α} {carrier : Set α} {isClopen' : IsClopen carrier} {carrier_1 : Set α}
  {isClopen'_1 : IsClopen carrier_1},
  { carrier := carrier, isClopen' := isClopen' } = { carrier := carrier_1, isClopen' := isClopen'_1 } →
    carrier = carrier_1
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- `HomClass F G H` asserts that `F` is a type of adjacency-preserving morphism.  -/
SimpleGraph.HomClass : {V : Type u_1} → {W : Type u_2} → (F : Type u_5) → SimpleGraph V → SimpleGraph W → [FunLike F V W] → Prop
-- Lean.Elab.Parallel
_private.Lean.Elab.Parallel.0.Std.Iterators.Types.Internal.TaskIterator.mk.inj : ∀ {α : Type w} {tasks tasks_1 : List (Task α)}, { tasks := tasks } = { tasks := tasks_1 } → tasks = tasks_1
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.π_ofπ : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {P : C} (π : Y ⟶ P)
  (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π),
  (CategoryTheory.Limits.Cotrident.ofπ π w).π = π
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the sign of the angle between two vectors is nonzero, the first vector is nonzero.  -/
Orientation.left_ne_zero_of_oangle_sign_ne_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, (o.oangle x y).sign ≠ 0 → x ≠ 0
-- Mathlib.FieldTheory.Galois.Profinite
/-- For `FiniteGaloisIntermediateField` s `L₁` and `L₂` with `L₂ ≤ L₁`
the restriction homomorphism from `Gal(L₁/k)` to `Gal(L₂/k)`  -/
finGaloisGroupMap : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          {L₁ L₂ : (FiniteGaloisIntermediateField k K)ᵒᵖ} →
            (L₁ ⟶ L₂) → ((Opposite.unop L₁).finGaloisGroup ⟶ (Opposite.unop L₂).finGaloisGroup)