mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf_inv_app : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor C 𝒳} (hF : F.comp p = (CategoryTheory.Functor.const C).obj S) (X : C),
  (CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf hF).inv.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.Functor.Fiber.fiberInclusion.obj ((CategoryTheory.Functor.Fiber.inducedFunctor hF).obj X))
-- Lean.Elab.PreDefinition.FixedParams
/-- This parameter is varying. Set and propagate that information.
 -/
Lean.Elab.FixedParams.Info.setVarying : ℕ → ℕ → Lean.Elab.FixedParams.Info → Lean.Elab.FixedParams.Info
-- Lean.Parser.Extra
Lean.Parser.decQuotDepth.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_eq_blsub_iff_lt_bsup : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}),
  o.bsup f = o.blsub f ↔ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < o.bsup f
-- Mathlib.Data.Bundle
Bundle.Pullback.lift_proj : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {B' : Type u_4} (f : B' → B) (a : Bundle.TotalSpace F (f *ᵖ E)),
  (Bundle.Pullback.lift f a).proj = f a.proj
-- Init.Data.Vector.Find
Vector.find?_push : ∀ {α : Type} {n : ℕ} {a : α} {p : α → Bool} {xs : Vector α n},
  Vector.find? p (xs.push a) = (Vector.find? p xs).or (if p a = true then some a else none)
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk_eq_mk_of_coe_ideal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R]
  {I J : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} {I' J' : Ideal R},
  ↑I = ↑I' →
    ↑J = ↑J' →
      ((ClassGroup.mk (FractionRing R)) I = (ClassGroup.mk (FractionRing R)) J ↔
        ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J')
-- Qq.SortLocalDecls
Qq.SortLocalDecls.M : Type → Type
-- Init.Data.Option.Lemmas
Option.filter_lt : ∀ {α : Type u_1} [inst : LT α],
  (∀ (x : α), ¬x < x) → ∀ {o : Option α} {p : α → Bool}, Option.filter p o < o ↔ Option.any (fun a => !p a) o = true
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Min α]
  [inst_2 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.toList.min? = t.min?
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveCodeProps.fmt : ProofWidgets.InteractiveCodeProps → Lean.Widget.CodeWithInfos
-- Mathlib.Data.ENNReal.Operations
/-- See `ENNReal.sub_eq_of_eq_add_rev'` for a version assuming that `a = b + c` itself is finite
rather than `b`.  -/
ENNReal.sub_eq_of_eq_add_rev : ∀ {a b c : ENNReal}, b ≠ ⊤ → a = b + c → a - b = c
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
AddCircle.toCircle_addChar.eq_1 : ∀ {T : ℝ}, AddCircle.toCircle_addChar = { toFun := AddCircle.toCircle, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }
-- Mathlib.Data.Ordmap.Invariants
Ordnode.node4R.eq_2 : ∀ {α : Type u_1} (x : Ordnode α) (x_1 x_2 : α) (x_3 : Ordnode α),
  x.node4R x_1 Ordnode.nil x_2 x_3 = x.node3R x_1 Ordnode.nil x_2 x_3
-- Mathlib.Order.Minimal
Maximal.eq_of_subset : ∀ {α : Type u_2} {P : Set α → Prop} {s t : Set α}, Maximal P s → P t → s ⊆ t → s = t
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is left distributive over addition  -/
NonUnitalNonAssocSemiring.left_distrib : ∀ {α : Type u} [self : NonUnitalNonAssocSemiring α] (a b c : α), a * (b + c) = a * b + a * c
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l),
  ‖p.changeOriginSeriesTerm k l s hs‖₊ = ‖p (k + l)‖₊
-- Batteries.Data.Array.Scan
Array.idRun_scanlM : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → Id β} {as : Array α},
  (Array.scanlM f init as).run = Array.scanl (fun x1 x2 => (f x1 x2).run) init as
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.instSmallFunctorObjIndex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S) [CategoryTheory.LocallySmall.{t, v, u} C] [Small.{t, w} I],
  Small.{t, max v w} (CategoryTheory.SmallObject.FunctorObjIndex f πX)
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
AddGroupSeminorm.mk.congr_simp : ∀ {G : Type u_6} [inst : AddGroup G] (toFun toFun_1 : G → ℝ) (e_toFun : toFun = toFun_1) (map_zero' : toFun 0 = 0)
  (add_le' : ∀ (r s : G), toFun (r + s) ≤ toFun r + toFun s) (neg' : ∀ (r : G), toFun (-r) = toFun r),
  { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' } =
    { toFun := toFun_1, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapBilipschitz_carrier : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ Y) (K₁ K₂ : NNReal)
  (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hf₁ : AntilipschitzWith K₁ ⇑f) (hf₂ : LipschitzWith K₂ ⇑f) (D : Delone.DeloneSet X),
  (Delone.DeloneSet.mapBilipschitz f K₁ K₂ hK₁ hK₂ hf₁ hf₂ D).carrier = ⇑f '' D.carrier
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.star_eq_inv : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A : ↥(Matrix.specialUnitaryGroup n α)), star A = A⁻¹
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.grindSeqBracketed : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_groupoid : ∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop},
  G.LocalInvariantProp G Q →
    (∀ (y : H), Q id Set.univ y) → ∀ {f : OpenPartialHomeomorph H H}, f ∈ G → ChartedSpace.LiftPropOn Q (↑f) f.source
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- Taking a colimit after whiskering by `G` is the same as using `G` and then taking a colimit.  -/
CategoryTheory.Limits.colimitCompWhiskeringLeftIsoCompColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {J : Type u₁} →
          [inst_2 : CategoryTheory.Category.{v₁, u₁} J] →
            {K : Type u₂} →
              [inst_3 : CategoryTheory.Category.{v₂, u₂} K] →
                (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
                  (G : CategoryTheory.Functor D K) →
                    [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C] →
                      CategoryTheory.Limits.colimit (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) ≅
                        G.comp (CategoryTheory.Limits.colimit F)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective.  -/
AddSubsemigroup.giMapComap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Add M] →
      [inst_1 : Add N] →
        {f : M →ₙ+ N} → Function.Surjective ⇑f → GaloisInsertion (AddSubsemigroup.map f) (AddSubsemigroup.comap f)
-- Init.Data.BitVec.Bitblast
BitVec.toInt_intMin_eq_bmod : ∀ {w : ℕ}, (BitVec.intMin w).toInt = (-2 ^ (w - 1)).bmod (2 ^ w)
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- A type is terminal if and only if it is isomorphic to `PUnit`.  -/
CategoryTheory.Limits.Types.isTerminalEquivIsoPUnit : (X : Type u) → CategoryTheory.Limits.IsTerminal X ≃ (X ≅ PUnit.{u + 1})
-- Mathlib.Logic.Encodable.Basic
Encodable.decode_ofEquiv : ∀ {α : Type u_3} {β : Type u_4} [inst : Encodable α] (e : β ≃ α) (n : ℕ),
  Encodable.decode n = Option.map (⇑e.symm) (Encodable.decode n)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun_iff_iCondIndep : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) {β : ι → Type u_3} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ω → β x)
  (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.iCondIndepFun m' hm' f μ ↔
    ProbabilityTheory.iCondIndep m' hm' (fun x => MeasurableSpace.comap (f x) (m x)) μ
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.mk.inj : ∀ {C₀ : Type u₀} {C : Type u} {inst : CategoryTheory.Category.{v₀, u₀} C₀} {inst_1 : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {X : C} {data : F.OneHypercoverDenseData J₀ J X} {X₀ : C₀}
  {f : F.obj X₀ ⟶ X} {Y₀ : C₀} {g : Y₀ ⟶ X₀} {i₀ : data.I₀} {q : F.obj Y₀ ⟶ F.obj (data.X i₀)}
  {fac :
    autoParam (CategoryTheory.CategoryStruct.comp q (data.f i₀) = CategoryTheory.CategoryStruct.comp (F.map g) f)
      CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac._autoParam}
  {i₀_1 : data.I₀} {q_1 : F.obj Y₀ ⟶ F.obj (data.X i₀_1)}
  {fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp q_1 (data.f i₀_1) = CategoryTheory.CategoryStruct.comp (F.map g) f)
      CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac._autoParam},
  { i₀ := i₀, q := q, fac := fac } = { i₀ := i₀_1, q := q_1, fac := fac_1 } → i₀ = i₀_1 ∧ q ≍ q_1
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.hilbertPoly_eq_zero_of_le_rootMultiplicity_one : ∀ {F : Type u_1} [inst : Field F] [CharZero F] {p : Polynomial F} {d : ℕ},
  d ≤ Polynomial.rootMultiplicity 1 p → p.hilbertPoly d = 0
-- Mathlib.GroupTheory.DoubleCoset
/-- The setoid defined by the `doubleCoset` relation  -/
DoubleCoset.setoid : {G : Type u_1} → [Group G] → Set G → Set G → Setoid G
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.foldM_filterMap : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad m]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad n Pred EPred] [inst_8 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : Std.IterM m β}
  {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b =>
          match f b with
          | some c => g d c
          | x => pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.IterM.filterMap f it) ⦃ Q; eQ ⦄
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.toPoly.eq_1 : ∀ (e : Nat.Internal.Linear.Expr), e.toPoly = Nat.Internal.Linear.Expr.toPoly.go 1 e []
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.Homotopic.trans : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} {f g h : ↑(GenLoop N X x)},
  GenLoop.Homotopic f g → GenLoop.Homotopic g h → GenLoop.Homotopic f h
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.congr_simp : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R], IsDiscreteValuationRing R = IsDiscreteValuationRing R
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.mem_resolventSet_of_norm_lt : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] [NormOneClass A] {a : A} {k : 𝕜}, ‖a‖ < ‖k‖ → k ∈ resolventSet 𝕜 a
-- Lean.Parser.Term.Basic
/-- A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
Delimiter-free indentation is determined by the *first* tactic of the sequence.  -/
Lean.Parser.Tactic.tacticSeq : Lean.Parser.Parser
-- Mathlib.Topology.ContinuousMap.Basic
/-- Right inverse to a continuous map from a homeomorphism, mirroring `Equiv.self_comp_symm`.  -/
Homeomorph.toContinuousMap_comp_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
  (↑f).comp ↑f.symm = ContinuousMap.id β
-- Lean.Setup
Lean.instFromJsonModuleHeader.fromJson : Lean.Json → Except String Lean.ModuleHeader
-- Init.Data.Int.Gcd
Int.lcm_mul_right_dvd_mul_lcm : ∀ (k m n : ℕ), (↑k).lcm (↑m * ↑n) ∣ (↑k).lcm ↑m * (↑k).lcm ↑n
-- Mathlib.Data.NNRat.Defs
NNRat.den_pow : ∀ (q : ℚ≥0) (n : ℕ), (q ^ n).den = q.den ^ n
-- Init.Prelude
/-- Create syntax node with 1 child  -/
Lean.Syntax.node1 : Lean.SourceInfo → Lean.SyntaxNodeKind → Lean.Syntax → Lean.Syntax
-- Mathlib.Algebra.Star.Basic
Units.instStarMul : {R : Type u} → [inst : Monoid R] → [StarMul R] → StarMul Rˣ
-- Mathlib.Algebra.Order.Hom.TypeTags
OrderAddMonoidIso.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (toAddEquiv toAddEquiv_1 : α ≃+ β) (e_toAddEquiv : toAddEquiv = toAddEquiv_1)
  (map_le_map_iff' : ∀ {a b : α}, toAddEquiv.toFun a ≤ toAddEquiv.toFun b ↔ a ≤ b),
  { toAddEquiv := toAddEquiv, map_le_map_iff' := map_le_map_iff' } =
    { toAddEquiv := toAddEquiv_1, map_le_map_iff' := ⋯ }
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.add_pf_add_lt : ∀ {R : Type u_1} [inst : CommSemiring R] {a₂ b c : R} (a₁ : R), a₂ + b = c → a₁ + a₂ + b = a₁ + c
-- Mathlib.CategoryTheory.Subobject.Types
Types.monoOverEquivalenceSet_functor_map : ∀ (α : Type u) {f g : CategoryTheory.MonoOver α} (t : f ⟶ g),
  (Types.monoOverEquivalenceSet α).functor.map t = CategoryTheory.homOfLE ⋯
-- Mathlib.Combinatorics.Additive.CovBySMul
CovBySMul.eq_1 : ∀ (M : Type u_1) {X : Type u_3} [inst : Monoid M] [inst_1 : MulAction M X] (K : ℝ) (A B : Set X),
  CovBySMul M K A B = ∃ F, ↑F.card ≤ K ∧ A ⊆ ↑F • B
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₂_map_one_fst : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : ↥(groupCohomology.cocycles₂ A))
  (g : G), f (1, g) = f (1, 1)
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddGroup.ofAddDist'.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : AddGroup E] [inst_2 : PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 0 x)
  (h₂ : ∀ (x y z : E), dist (z + x) (z + y) ≤ dist x y),
  SeminormedAddGroup.ofAddDist' h₁ h₂ =
    { toNorm := inst, toAddGroup := inst_1, toPseudoMetricSpace := inst_2, dist_eq := ⋯ }
-- Mathlib.Data.List.Basic
List.getElem_mem_tail : ∀ {α : Type u} {k : ℕ} (l : List α), k ≠ 0 → ∀ (hk : k < l.length), l[k] ∈ l.tail
-- Mathlib.Order.Filter.ENNReal
NNReal.toReal_liminf : ∀ {ι : Type u_1} {f : Filter ι} {u : ι → NNReal}, Filter.liminf (fun i => ↑(u i)) f = ↑(Filter.liminf u f)
-- Init.Data.Array.Subarray
/-- A subarray with the provided lower bound that extends to the rest of the array.  -/
Array.«term__[_:]» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.instSMulCommClassAEEqFun : ∀ {M : Type u_3} {N : Type u_1} {α : Type u_4} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : SMul M α] [inst_3 : MeasurableConstSMul M α]
  [inst_4 : MeasureTheory.SMulInvariantMeasure M α μ] [inst_5 : SMul N β] [inst_6 : ContinuousConstSMul N β],
  SMulCommClass Mᵈᵐᵃ N (α →ₘ[μ] β)
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_apply_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (f : Φ.presheafFiber.obj P ⟶ M) (X : Cᵒᵖ),
  (Φ.skyscraperPresheafHomEquiv f).app X =
    CategoryTheory.Limits.Pi.lift fun x =>
      CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber (Opposite.unop X) x P) f
-- Batteries.Tactic.PermuteGoals
/-- `swap` is a shortcut for `pick_goal 2`, which interchanges the 1st and 2nd goals.  -/
Batteries.Tactic.tacticSwap : Lean.ParserDescr
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.State.mk.sizeOf_spec : ∀ (stxTrav : Lean.Syntax.Traverser) (contPrec : Option ℕ) (contCat : Lean.Name) (minPrec trailPrec : Option ℕ)
  (trailCat : Lean.Name) (visitedToken : Bool),
  sizeOf
      { stxTrav := stxTrav, contPrec := contPrec, contCat := contCat, minPrec := minPrec, trailPrec := trailPrec,
        trailCat := trailCat, visitedToken := visitedToken } =
    1 + sizeOf stxTrav + sizeOf contPrec + sizeOf contCat + sizeOf minPrec + sizeOf trailPrec + sizeOf trailCat +
      sizeOf visitedToken
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₅.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  (app₀ app₀_1 : f.obj' 0 _proof_449✝ ⟶ g.obj' 0 _proof_449✝) (e_app₀ : app₀ = app₀_1)
  (app₁ app₁_1 : f.obj' 1 _proof_450✝ ⟶ g.obj' 1 _proof_450✝) (e_app₁ : app₁ = app₁_1)
  (app₂ app₂_1 : f.obj' 2 _proof_451✝ ⟶ g.obj' 2 _proof_451✝) (e_app₂ : app₂ = app₂_1)
  (app₃ app₃_1 : f.obj' 3 _proof_452✝ ⟶ g.obj' 3 _proof_452✝) (e_app₃ : app₃ = app₃_1)
  (app₄ app₄_1 : f.obj' 4 _proof_453✝ ⟶ g.obj' 4 _proof_453✝) (e_app₄ : app₄ = app₄_1)
  (app₅ app₅_1 : f.obj' 5 _proof_454✝ ⟶ g.obj' 5 _proof_454✝) (e_app₅ : app₅ = app₅_1)
  (w₀ :
    CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝) app₁ =
      CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝))
  (w₁ :
    CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_451✝) app₂ =
      CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_451✝))
  (w₂ :
    CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_452✝) app₃ =
      CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_452✝))
  (w₃ :
    CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_453✝) app₄ =
      CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_453✝))
  (w₄ :
    CategoryTheory.CategoryStruct.comp (f.map' 4 5 _proof_453✝ _proof_454✝) app₅ =
      CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 _proof_453✝ _proof_454✝)),
  CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄ =
    CategoryTheory.ComposableArrows.homMk₅ app₀_1 app₁_1 app₂_1 app₃_1 app₄_1 app₅_1 ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Lie.Classical
/-- The matrices with matching positive and negative elements on the diagonal are elements of
`sl n R`. Along with `single`, a subset of these form a basis for `sl n R`.  -/
LieAlgebra.SpecialLinear.singleSubSingle : {n : Type u_1} →
  {R : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → n → n → R →ₗ[R] ↥(LieAlgebra.SpecialLinear.sl n R)
-- Mathlib.Data.Matrix.Diagonal
Matrix.submatrix_diagonal_equiv : ∀ {l : Type u_1} {m : Type u_2} {α : Type v} [inst : Zero α] [inst_1 : DecidableEq m] [inst_2 : DecidableEq l]
  (d : m → α) (e : l ≃ m), (Matrix.diagonal d).submatrix ⇑e ⇑e = Matrix.diagonal (d ∘ ⇑e)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Constructor for isomorphisms of pre-`0`-hypercovers.  -/
CategoryTheory.PreZeroHypercover.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E F : CategoryTheory.PreZeroHypercover S} →
        (s₀ : E.I₀ ≃ F.I₀) →
          (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) →
            autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
                CategoryTheory.PreZeroHypercover.isoMk._auto_1 →
              (E ≅ F)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.isEmpty = true → m.getKey? a = none
-- Mathlib.Order.Interval.Set.Monotone
Monotone.Ioc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β},
  Monotone f → Antitone g → Antitone fun x => Set.Ioc (f x) (g x)
-- Mathlib.Topology.TietzeExtension
/-- **Alias** of `BoundedContinuousFunction.exists_forall_mem_domRestrict_eq_of_closed`.

---

**Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
set. Let `s` be a closed set in a normal topological space `Y`. Let `f` be a bounded continuous
real-valued function on `s`. Let `t` be a nonempty convex set of real numbers (we use
`OrdConnected` instead of `Convex` to automatically deduce this argument by typeclass search) such
that `f x ∈ t` for all `x : s`. Then there exists a bounded continuous real-valued function
`g : Y →ᵇ ℝ` such that `g y ∈ t` for all `y` and `g.domRestrict s = f`.  -/
BoundedContinuousFunction.exists_forall_mem_restrict_eq_of_closed : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction ↑s ℝ),
  IsClosed s →
    ∀ {t : Set ℝ} [t.OrdConnected], (∀ (x : ↑s), f x ∈ t) → t.Nonempty → ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.domRestrict s = f
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (t : CategoryTheory.Limits.Cone G) (w : F ≅ G) {Z : C}
  (h : CategoryTheory.Limits.limit F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift G t)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso w).inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.lift F ((CategoryTheory.Limits.Cone.postcompose w.inv).obj t)) h
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.clz.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVUnOp.clz = 1
-- Aesop.Search.Expansion.Norm
Aesop.NormSeqResult.unchanged : Aesop.NormSeqResult
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.ofIso_symm_apply : ∀ {R : Type u} [inst : CommRing R] {A B : CommHopfAlgCat R} (i : A ≅ B) (a : ↑B),
  (CommHopfAlgCat.ofIso i).symm a = (CategoryTheory.ConcreteCategory.hom i.inv) a
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.union_sdiff_cancel_left`. -/
Set.union_diff_cancel_left : ∀ {α : Type u_1} {s t : Set α}, s ∩ t ⊆ ∅ → (s ∪ t) \ s = t
-- Mathlib.Algebra.Group.Hom.Defs
/-- Composition of `OneHom`s as a `OneHom`.  -/
OneHom.comp : {M : Type u_4} →
  {N : Type u_5} →
    {P : Type u_6} → [inst : One M] → [inst_1 : One N] → [inst_2 : One P] → OneHom N P → OneHom M N → OneHom M P
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv_assoc : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [inst_1 : IsAlgClosed K]
  (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [inst_2 : AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X)
  (hx : IsClosed {x}) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.residueFieldIsoBase f x hx).inv) h =
    CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) (CategoryTheory.CategoryStruct.comp f h)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.toStream.eq_1 : ∀ {α : Type u_1} (x : RBTree.RBNode.Stream α), RBTree.RBNode.nil.toStream x = x
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) {n m : ℕ} (i : ℕ)
  (hi : n + i = m), X.σ₀Iter i hi = X.map (SimplexCategory.σ₀Iter i hi).op