mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.mk.congr_simp : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (setsAt setsAt_1 : X → Set (Set X)) (e_setsAt : setsAt = setsAt_1)
  (measurableSet : ∀ (x : X), ∀ s ∈ setsAt x, MeasurableSet s)
  (nonempty_interior : ∀ (x : X), ∀ s ∈ setsAt x, (interior s).Nonempty)
  (nontrivial : ∀ (x : X), ∀ ε > 0, ∃ s ∈ setsAt x, s ⊆ Metric.closedBall x ε)
  (covering :
    ∀ (s : Set X) (f : X → Set (Set X)),
      (∀ x ∈ s, f x ⊆ setsAt x) →
        (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ Metric.closedBall x ε) →
          ∃ t,
            (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0),
  { setsAt := setsAt, measurableSet := measurableSet, nonempty_interior := nonempty_interior, nontrivial := nontrivial,
      covering := covering } =
    { setsAt := setsAt_1, measurableSet := ⋯, nonempty_interior := ⋯, nontrivial := ⋯, covering := ⋯ }
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.of_mul_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α}, (s * t).Nonempty → s.Nonempty
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc : ∀ {R : CommRingCat} (f g x : ↑R) (hx : x = f * g) {Z : AlgebraicGeometry.Scheme} (h : ↑(PrimeSpectrum.basicOpen f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.basicOpenIsoSpecAway x).inv
      (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).homOfLE ⋯) h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.basicOpenIsoSpecAway f).inv h)
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.instIsMarkovKernelBoolBoolKernelOfIsProbabilityMeasure : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν], ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.boolKernel μ ν)
-- Init.Data.Array.Lemmas
Array.forall_mem_filter : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} {P : α → Prop},
  (∀ i ∈ Array.filter p xs, P i) ↔ ∀ j ∈ xs, p j = true → P j
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyLE!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.Equiv t₂ → t₁.getKeyLE! k = t₂.getKeyLE! k
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.nonempty_isLimit_iff_eq_induced : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cone F) (hc : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget TopCat).mapCone c)),
  Nonempty (CategoryTheory.Limits.IsLimit c) ↔
    c.pt.str = ⨅ j, TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom (c.π.app j))) (F.obj j).str
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.EssentiallySmall.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  (∃ Q, ∃ (_ : CategoryTheory.ObjectProperty.Small.{w, v, u} Q), P ≤ Q.isoClosure) →
    CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_sub : ∀ {α : Type u_1} {G : Type u_8} [inst : AddGroup G] (p : α → Prop) [inst_1 : DecidablePred p] (f₁ f₂ : α →₀ G),
  Finsupp.filter p (f₁ - f₂) = Finsupp.filter p f₁ - Finsupp.filter p f₂
-- Lean.Meta.Sym.SymM
/-- Mutable state for the symbolic computation framework.  -/
Lean.Meta.Sym.State : Type
-- Batteries.Recycling.RBTree.Basic
/-- `O(n * log n)`. Constructs the set of all elements satisfying `p`.  -/
RBTree.RBMap.filter : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → (α → β → Bool) → RBTree.RBMap α β cmp
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.sSup_empty : sSup ∅ = 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {he : t.isEmpty = false}, t.get! (t.min he) = t.min he
-- Mathlib.Data.Finset.Range
Finset.nonempty_range_add_one : ∀ {n : ℕ}, (Finset.range (n + 1)).Nonempty
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_extend_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {a : α} {g : β → γ}, Function.Injective g → (HasSum (Function.extend g f 0) a ↔ HasSum f a)
-- Mathlib.NumberTheory.Height.Basic
/-- Only finitely many (nonarchimedean) absolute values are `≠ 1` for any nonzero `x : K`.  -/
Height.AdmissibleAbsValues.hasFiniteMulSupport : ∀ {K : Type u_1} {inst : Field K} [self : Height.AdmissibleAbsValues K] {x : K},
  x ≠ 0 → Function.HasFiniteMulSupport fun v => ↑v x
-- Mathlib.Order.Heyting.Hom
HeytingHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β]
  [inst_2 : HeytingAlgebra γ] (f : HeytingHom β γ) (g : HeytingHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.Order.WellQuasiOrder
WellQuasiOrderedLE.finite_of_isAntichain : ∀ {α : Type u_1} [inst : Preorder α] [WellQuasiOrderedLE α] {s : Set α}, IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
/-- If there are `ε * (card α)^2` disjoint triangles, then the graph is `ε`-far from being
triangle-free.  -/
SimpleGraph.farFromTriangleFree_of_disjoint_triangles : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  {ε : 𝕜} [inst_3 : Fintype α] [inst_4 : DecidableRel G.Adj] [inst_5 : DecidableEq α],
  ∀ tris ⊆ G.cliqueFinset 3,
    ((↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton) →
      ε * ↑(Fintype.card α ^ 2) ≤ ↑tris.card → G.FarFromTriangleFree ε
-- Std.Data.DTreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the largest key that is
less than or equal to the given key.
 -/
Std.DTreeMap.getKeyLE : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.DTreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isLE = true) → α
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.hasTemperateGrowth_norm_sq : ∀ (H : Type u_8) [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℝ H],
  Function.HasTemperateGrowth fun x => ‖x‖ ^ 2
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.mapUnit : ∀ {α : Type u} [inst : BEq α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l → Std.Internal.List.DistinctKeys (List.map (fun x => ⟨x, ()⟩) l)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.sdiff_finite_comm : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.IsBase B₁ → M.IsBase B₂ → ((B₁ \ B₂).Finite ↔ (B₂ \ B₁).Finite)
-- Mathlib.Data.Set.Insert
Set.insert_inter_of_notMem : ∀ {α : Type u_1} {s t : Set α} {a : α}, a ∉ t → insert a s ∩ t = s ∩ t
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.DiseqCnstr.satisfied : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Lean.Meta.Grind.Arith.Linear.LinearM Lean.LBool
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.toMatrix_mul`. -/
BilinForm.toMatrix_mul : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (M : Matrix n n R₁),
  (LinearMap.BilinForm.toMatrix b) B * M = (LinearMap.BilinForm.toMatrix b) (B.compRight ((Matrix.toLin b b) M))
-- Mathlib.Analysis.Matrix.Normed
Matrix.nnnorm_replicateCol : ∀ {m : Type u_3} {α : Type u_5} {ι : Type u_7} [inst : Fintype m] [inst_1 : Unique ι]
  [inst_2 : SeminormedAddCommGroup α] (v : m → α), ‖Matrix.replicateCol ι v‖₊ = ‖v‖₊
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.circumcenter_ne_point : ∀ {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 + 1)) (i : Fin (n + 2)), s.circumcenter ≠ s.points i
-- Mathlib.RingTheory.Spectrum.Prime.Noetherian
IsArtinianRing.instKrullDimLEOfNatNat : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R], Ring.KrullDimLE 0 R
-- Mathlib.Topology.Separation.Regular
disjoint_nhds_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] {x : X} {s : Set X},
  Disjoint (nhds x) (nhdsSet s) ↔ x ∉ closure s
-- Lean.Environment
Lean.Kernel.Environment.getDiagnostics : Lean.Kernel.Environment → Lean.Kernel.Diagnostics
-- Mathlib.Algebra.Category.MonCat.Adjunctions
AddMonCat.free.eq_1 : AddMonCat.free =
  { obj := fun α => AddMonCat.of (FreeAddMonoid α),
    map := fun {X Y} f => AddMonCat.ofHom (FreeAddMonoid.map ⇑(CategoryTheory.ConcreteCategory.hom f)),
    map_id := AddMonCat.free._proof_1, map_comp := @AddMonCat.free._proof_2 }
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
/-- Taking the product of an indicator function over a possibly larger finset is the same as
taking the original function over the original finset.  -/
Finset.prod_mulIndicator_subset : ∀ {ι : Type u_1} {β : Type u_4} [inst : CommMonoid β] (f : ι → β) {s t : Finset ι},
  s ⊆ t → ∏ i ∈ t, (↑s).mulIndicator f i = ∏ i ∈ s, f i
-- Mathlib.Data.Finset.Insert
Finset.insert_val : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), (insert a s).val = Multiset.ndinsert a s.val
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.lift_comp_inl : ∀ {N : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group N] [inst_1 : Group G] [inst_2 : Group H]
  {φ : G →* MulAut N} (fn : N →* H) (fg : G →* H)
  (h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn),
  (SemidirectProduct.lift fn fg h).comp SemidirectProduct.inl = fn
-- Aesop.Forward.RuleInfo
/-- Sort slots such that each slot has at least one variable in common with
the previous slots.  -/
_private.Aesop.Forward.RuleInfo.0.Aesop.ForwardRuleInfo.ofExpr.sortSlots : Array Aesop.Slot → Array Aesop.Slot
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.app_isHomLift : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} (α : CategoryTheory.BasedNatTrans F G)
  (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (α.app a)
-- Mathlib.Data.Rat.Defs
Rat.intCast_eq_one_iff : ∀ {n : ℤ}, ↑n = 1 ↔ n = 1
-- Mathlib.Data.Rel
SetRel.cod_empty : ∀ {α : Type u_1} {β : Type u_2}, ∅.cod = ∅
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DTreeMap.Raw.Const.get! (m₁ ∩ m₂) k = default
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.isCharTwoNF_of_isCharTwoJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF], W.IsCharTwoNF
-- Mathlib.Order.Filter.ENNReal
NNReal.limsInf_of_not_isCobounded : ∀ {f : Filter NNReal}, ¬Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) f → f.limsInf = 0
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- A function of temperate growth `f` defines a tempered distribution via integration, namely
`g ↦ ∫ (x : E), g x • f x ∂μ`.  -/
Function.HasTemperateGrowth.toTemperedDistribution : {E : Type u_3} →
  {F : Type u_4} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℂ F] →
            [inst_4 : MeasurableSpace E] →
              [BorelSpace E] →
                [SecondCountableTopology E] →
                  (μ : autoParam (MeasureTheory.Measure E) _auto_39✝) →
                    [hμ : μ.HasTemperateGrowth] → {f : E → F} → Function.HasTemperateGrowth f → TemperedDistribution E F
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicInterior_union_intrinsicFrontier : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : Set P),
  intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.Equiv.mk : ∀ {α : Type u} {m₁ m₂ : Std.HashSet.Raw α}, m₁.inner.Equiv m₂.inner → m₁.Equiv m₂
-- Mathlib.GroupTheory.Generators
/-- The generating family itself: `val i` is the element of `G` indexed by `i : ι`.  -/
Group.Generators.val : {G : Type u_5} → [inst : Group G] → {ι : Type u_6} → Group.Generators G ι → ι → G
-- Mathlib.Algebra.Group.End
MulAut.congr_apply : ∀ {G : Type u_3} [inst : Group G] {H : Type u_7} [inst_1 : Group H] (ϕ : G ≃* H) (f : MulAut G),
  (MulAut.congr ϕ) f = ϕ.symm.trans (MulEquiv.trans f ϕ)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → ∀ {h : k' ∈ Std.ExtHashMap.ofList l}, (Std.ExtHashMap.ofList l).getKey k' h = k
-- Mathlib.LinearAlgebra.Matrix.MvPolynomial
Matrix.mvPolynomialX.eq_1 : ∀ (m : Type u_1) (n : Type u_2) (R : Type u_3) [inst : CommSemiring R],
  Matrix.mvPolynomialX m n R = Matrix.of fun i j => MvPolynomial.X (i, j)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_ofNat : ∀ (n : ℕ) (h : System.Platform.numBits = 64), (OfNat.ofNat n).toBitVec64 h = BitVec.ofNat 64 n
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCodetector_iff_reflectsIsomorphisms_yoneda_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsCodetector G ↔ (CategoryTheory.yoneda.obj G).ReflectsIsomorphisms
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
MulOpposite.opLinearIsometryEquiv_symm_apply : ∀ (R : Type u_11) (H : Type u_12) [inst : Semiring R] [inst_1 : SeminormedAddCommGroup H] [inst_2 : Module R H]
  (a : Hᵐᵒᵖ), (MulOpposite.opLinearIsometryEquiv R H).symm a = MulOpposite.unop a
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.nthRootsFinset_zero : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (a : R), Polynomial.nthRootsFinset 0 a = ∅
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.op_smul_finset_mul_eq_mul_smul_finset : ∀ {α : Type u_2} [inst : Semigroup α] [inst_1 : DecidableEq α] (a : α) (s t : Finset α),
  MulOpposite.op a • s * t = s * a • t
-- Mathlib.Tactic.ReduceModChar
Tactic.ReduceModChar.CharP.neg_eq_sub_one_mul : ∀ {α : Type u_1} [inst : Ring α] (n : ℕ),
  CharP α n → ∀ (b : α) (a : ℕ) (a' : α), Mathlib.Meta.NormNum.IsNat (↑n - 1) a → ↑a = a' → -b = a' * b
-- Init.Data.String.Substring
Substring.Raw.takeWhileAux : String → String.Pos.Raw → (Char → Bool) → String.Pos.Raw → String.Pos.Raw
-- Mathlib.RingTheory.Coalgebra.Hom
LinearMap.copy.congr_simp : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f f_1 : M →ₛₗ[σ] M₃) (e_f : f = f_1) (f' f'_1 : M → M₃) (e_f' : f' = f'_1) (h : f' = ⇑f),
  f.copy f' h = f_1.copy f'_1 ⋯
-- Mathlib.Computability.Primrec.Basic
PrimrecRel.swap : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {r : α → β → Prop},
  PrimrecRel r → PrimrecRel (Function.swap r)
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.shift_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (A : Type u_2)
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [P.IsClosedUnderIsomorphisms], P.shift 0 = P
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.subtypeCongr.congr_simp : ∀ {ε : Type u_9} {p : ε → Prop} {inst : DecidablePred p} [inst_1 : DecidablePred p] (ep ep_1 : Equiv.Perm { a // p a }),
  ep = ep_1 → ∀ (en en_1 : Equiv.Perm { a // ¬p a }), en = en_1 → ep.subtypeCongr en = ep_1.subtypeCongr en_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If `X' ≅ X`, then `X × Y` also is the product of `X'` and `Y`.  -/
CategoryTheory.Limits.BinaryFan.isLimitCompLeftIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y X' : C} →
      (c : CategoryTheory.Limits.BinaryFan X Y) →
        (f : X ⟶ X') →
          [CategoryTheory.IsIso f] →
            CategoryTheory.Limits.IsLimit c →
              CategoryTheory.Limits.IsLimit
                (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp c.fst f) c.snd)
-- Init.System.ST
/-- Auxiliary definition for showing that `ST σ α` is inhabited when we have a `Ref σ α`  -/
_private.Init.System.ST.0.ST.Prim.inhabitedFromRef : {σ α : Type} → ST.Ref σ α → ST σ α
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_mul_mul_comm' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommMonObj M],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ M M M M)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
        CategoryTheory.MonObj.mul) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
      CategoryTheory.MonObj.mul
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.FunctionTheorems.mk.sizeOf_spec : ∀
  (theorems :
    Std.TreeMap Lean.Name (Std.TreeMap Lean.Name (Array Mathlib.Meta.FunProp.FunctionTheorem) Lean.Name.quickCmp)
      Lean.Name.quickCmp),
  sizeOf { theorems := theorems } = 1 + sizeOf theorems
-- Mathlib.Topology.Algebra.Ring.Basic
instIsSemitopologicalRingMulOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : TopologicalSpace R] [IsSemitopologicalRing R],
  IsSemitopologicalRing Rᵐᵒᵖ
-- Mathlib.SetTheory.Lists
Lists'.mem_equiv_left : ∀ {α : Type u_1} {l : Lists' α true} {a a' : Lists α}, a.Equiv a' → (a ∈ l ↔ a' ∈ l)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.alter_eq_alterₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α]
  {t : Std.DTreeMap.Internal.Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced),
  t.Ordered → (Std.DTreeMap.Internal.Impl.alter a f t htb).impl = Std.DTreeMap.Internal.Impl.alterₘ a f t htb
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
less than the given key.
 -/
Std.ExtDTreeMap.Const.getEntryLT : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [inst : Std.TransCmp cmp] →
        (t : Std.ExtDTreeMap α (fun x => β) cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.lt) → α × β
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a fallback : α}
  {v : β}, (t.insert k v).getKeyD a fallback = if cmp k a = Ordering.eq then k else t.getKeyD a fallback
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.normExt : Lean.Meta.SimpExtension
-- Mathlib.AlgebraicTopology.DoldKan.FunctorN
/-- The extension of `N₁` to the Karoubi envelope of `SimplicialObject C`.  -/
AlgebraicTopology.DoldKan.N₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C))
        (CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.ι_mapBifunctorShift₁Iso_hom_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.Additive]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ℤ) [inst_8 : K₁.HasMapBifunctor K₂ F] (n₁ n₂ n : ℤ)
  (h : n₁ + n₂ = n) (m₁ m : ℤ) (hm₁ : m₁ = n₁ + x) (hm : m = n + x),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).ιMapBifunctor K₂ F n₁ n₂ n h)
      ((K₁.mapBifunctorShift₁Iso K₂ F x).hom.f n) =
    CategoryTheory.CategoryStruct.comp ((F.map (K₁.shiftFunctorObjXIso x n₁ m₁ hm₁).hom).app (K₂.X n₂))
      (CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F m₁ n₂ m ⋯)
        ((K₁.mapBifunctor K₂ F).shiftFunctorObjXIso x n m hm).inv)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_zero : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A], CFC.sqrt 0 = 0
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_omega_iff_analyticOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F}, UniqueDiffOn 𝕜 s → (ContDiffOn 𝕜 ⊤ f s ↔ AnalyticOn 𝕜 f s)
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange.equiv_symm : ∀ {ι : Type u_3} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (e : M ≃ N) (hf : e 0 = 0),
  (Finsupp.mapRange.equiv e hf).symm = Finsupp.mapRange.equiv e.symm ⋯
-- Mathlib.Data.EReal.Operations
EReal.instInvolutiveNeg : InvolutiveNeg EReal
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfpFamily_fp : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι] {i : ι},
  Order.IsNormal (f i) → ∀ (a : Ordinal.{u}), f i (Ordinal.nfpFamily f a) = Ordinal.nfpFamily f a
-- Mathlib.Order.Types.Defs
OrderType.type_nat : OrderType.type ℕ = OrderType.omega0
-- Init.Data.Array.Attach
Array.foldl_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β} (H : ∀ a ∈ xs, P a)
  (g : γ → β → γ) (x : γ), Array.foldl g x (Array.pmap f xs H) = Array.foldl (fun acc a => g acc (f ↑a ⋯)) x xs.attach
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
aemeasurable_of_tendsto_metrizable_ae : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β] {ι : Type u_3}
  {μ : MeasureTheory.Measure α} {f : ι → α → β} {g : α → β} (u : Filter ι) [hu : u.NeBot] [u.IsCountablyGenerated],
  (∀ (n : ι), AEMeasurable (f n) μ) → (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) u (nhds (g x))) → AEMeasurable g μ
-- Mathlib.Algebra.Order.Round
round_eq : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α),
  round x = ⌊x + 1 / 2⌋
-- Mathlib.Data.Set.Pairwise.Lattice
Set.pairwiseDisjoint_iUnion : ∀ {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : PartialOrder α] [inst_1 : OrderBot α] {f : ι → α}
  {g : ι' → Set ι},
  Directed (fun x1 x2 => x1 ⊆ x2) g → ((⋃ n, g n).PairwiseDisjoint f ↔ ∀ ⦃n : ι'⦄, (g n).PairwiseDisjoint f)
-- Mathlib.Order.SymmDiff
Pi.symmDiff_apply : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → GeneralizedCoheytingAlgebra (π i)] (a b : (i : ι) → π i) (i : ι),
  symmDiff a b i = symmDiff (a i) (b i)