mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedMonoid.toContinuousENorm : {E : Type u_8} → {inst : TopologicalSpace E} → [self : ESeminormedMonoid E] → ContinuousENorm E
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- Given `E : Functor.LeftExtension L F`, this is the property of objects where
`E` is a pointwise left Kan extension.  -/
CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAt : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} → L.LeftExtension F → CategoryTheory.ObjectProperty D
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_subset_uIcc_right : ∀ {α : Type u_1} [inst : Lattice α] {a b x : α}, x ∈ Set.uIcc a b → Set.uIcc x b ⊆ Set.uIcc a b
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.residue_def : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (x : R),
  (IsLocalRing.residue R) x = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R)) x
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.open_eq_sUnion : ∀ {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis B → ∀ {u : Set α}, IsOpen u → ∃ S ⊆ B, u = ⋃₀ S
-- Mathlib.Data.Set.Basic
Set.sep_union : ∀ {α : Type u} {s t : Set α} {p : α → Prop}, {x | (x ∈ s ∨ x ∈ t) ∧ p x} = {x | x ∈ s ∧ p x} ∪ {x | x ∈ t ∧ p x}
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extInv_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F} (φ : c.pt ≅ c'.pt)
  (w :
    autoParam (∀ (j : J), c.ι.app j = CategoryTheory.CategoryStruct.comp (c'.ι.app j) φ.inv)
      CategoryTheory.Limits.Cocone.extInv._auto_1),
  (CategoryTheory.Limits.Cocone.extInv φ w).hom.hom = φ.hom
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The action of `(𝓞 K)ˣ` on the mixed space `ℝ^r₁ × ℂ^r₂` defined, for `u : (𝓞 K)ˣ`, by
multiplication component by component with `mixedEmbedding K u`.  -/
NumberField.mixedEmbedding.unitSMul : (K : Type u_1) → [inst : Field K] → SMul (NumberField.RingOfIntegers K)ˣ (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.mk₂_apply : ∀ (R : Type u_2) [inst : CommSemiring R] {M : Type u_5} {Nₗ : Type u_8} {Pₗ : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid Nₗ] [inst_3 : AddCommMonoid Pₗ] [inst_4 : Module R M] [inst_5 : Module R Nₗ]
  [inst_6 : Module R Pₗ] (f : M → Nₗ → Pₗ) {H1 : ∀ (m₁ m₂ : M) (n : Nₗ), f (m₁ + m₂) n = f m₁ n + f m₂ n}
  {H2 : ∀ (c : R) (m : M) (n : Nₗ), f (c • m) n = c • f m n}
  {H3 : ∀ (m : M) (n₁ n₂ : Nₗ), f m (n₁ + n₂) = f m n₁ + f m n₂}
  {H4 : ∀ (c : R) (m : M) (n : Nₗ), f m (c • n) = c • f m n} (m : M) (n : Nₗ),
  ((LinearMap.mk₂ R f H1 H2 H3 H4) m) n = f m n
-- Mathlib.Data.List.TakeDrop
List.span.loop.eq_2 : ∀ {α : Type u} (p : α → Bool) (a : List α) (a_1 : α) (l : List α),
  List.span.loop p (a_1 :: l) a =
    match p a_1 with
    | true => List.span.loop p l (a_1 :: a)
    | false => (a.reverse, a_1 :: l)
-- Mathlib.Tactic.Core
/-- Return the modifiers of declaration `nm` with (optional) docstring `newDoc`.
Currently, recursive or partial definitions are not supported, and no attributes are provided.
 -/
Lean.toModifiers : Lean.Name → optParam (Option (Lean.TSyntax `Lean.Parser.Command.docComment)) none → Lean.CoreM Lean.Elab.Modifiers
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.mul_toMatrix_mul`. -/
BilinForm.mul_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} {o : Type u_6} [inst_3 : Fintype n] [inst_4 : Fintype o] [inst_5 : DecidableEq n]
  (b : Module.Basis n R₁ M₁) {M₂' : Type u_7} [inst_6 : AddCommMonoid M₂'] [inst_7 : Module R₁ M₂']
  (c : Module.Basis o R₁ M₂') [inst_8 : DecidableEq o] (B : LinearMap.BilinForm R₁ M₁) (M : Matrix o n R₁)
  (N : Matrix n o R₁),
  M * (LinearMap.BilinForm.toMatrix b) B * N =
    (LinearMap.BilinForm.toMatrix c) (B.comp ((Matrix.toLin c b) M.transpose) ((Matrix.toLin c b) N))
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- **Alias** of `MeasureTheory.IntegrableOn.of_forall_sdiff_eq_zero`.

---

If a function is integrable on a set `s`, and vanishes on `t \ s`, then it is integrable on `t`
if `t` is measurable.  -/
MeasureTheory.IntegrableOn.of_forall_diff_eq_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} {s t : Set α} {μ : MeasureTheory.Measure α} {ε' : Type u_7}
  [inst : TopologicalSpace ε'] [inst_1 : ENormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε'] {f : α → ε'},
  MeasureTheory.IntegrableOn f s μ → MeasurableSet t → (∀ x ∈ t \ s, f x = 0) → MeasureTheory.IntegrableOn f t μ
-- Mathlib.NumberTheory.NumberField.Basic
/-- A number field is a field which has characteristic zero and is finite
dimensional over ℚ.  -/
NumberField : (K : Type u_1) → [Field K] → Prop
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instAdd : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] → [inst_3 : AddZeroClass R] → [ContinuousAdd R] → Add (ContinuousMapZero X R)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasStrictDerivAt.csinh : ∀ {f : ℂ → ℂ} {f' x : ℂ},
  HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) * f') x
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toArray_rco_eq_fallback : ∀ {m n fallback : ℤ} {i : ℕ}, (n - m).toNat ≤ i → (m...n).toArray.getD i fallback = fallback
-- Std.Time.Date.PlainDate
/-- Creates a `PlainDate` by rolling over the extra days to the next month.
 -/
Std.Time.PlainDate.rollOver : Std.Time.Year.Offset → Std.Time.Month.Ordinal → Std.Time.Day.Ordinal → Std.Time.PlainDate
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_eq_zero : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x : WithVal v), x.ofVal = 0 ↔ x = 0
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instVAdd.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X], AddOreLocalization.instVAdd = { vadd := AddOreLocalization.vadd }
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk₁_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1}
  (left :
    F.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 ≅ G.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4)
  (right :
    F.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 ≅ G.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5)
          right.hom =
        CategoryTheory.CategoryStruct.comp left.hom
          (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5))
      CategoryTheory.ComposableArrows.isoMk₁._auto_1)
  (i : Fin (1 + 1)),
  (CategoryTheory.ComposableArrows.isoMk₁ left right w).inv.app i =
    match i with
    | ⟨0, isLt⟩ => left.inv
    | ⟨1, isLt⟩ => right.inv
-- Init.Data.BitVec.Lemmas
BitVec.toNat_sub' : ∀ {n : ℕ} (x y : BitVec n), (x - y).toNat = (x.toNat + (2 ^ n - y.toNat)) % 2 ^ n
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_nil : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Inhabited β] {a : α}, Std.Internal.List.getValue! a [] = default
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RiiSliceData.mk.inj : ∀ {α : Type u} {treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit} {range : Std.Rii α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit} {range_1 : Std.Rii α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Analysis.BoxIntegral.Basic
/-- **Henstock-Sacks inequality**. Let `r : ℝⁿ → (0, ∞)` be a function such that for any tagged
*partition* of `I` subordinate to `r`, the integral sum of `f` over this partition differs from the
integral of `f` by at most `ε`. Then for any tagged *prepartition* `π` subordinate to `r`, the
integral sum of `f` over this prepartition differs from the integral of `f` over the part of `I`
covered by `π` by at most `ε`.

The actual statement

- uses `BoxIntegral.Integrable.convergenceR` instead of a predicate assumption on `r`;
- uses `BoxIntegral.IntegrationParams.MemBaseSet` instead of “subordinate to `r`” to
  account for additional requirements like being a Henstock partition or having a bounded
  distortion;
 -/
BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι}
  {π : BoxIntegral.TaggedPrepartition I} [inst_4 : Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E}
  {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {c : NNReal} {ε : ℝ} [CompleteSpace F]
  (h : BoxIntegral.Integrable I l f vol),
  0 < ε →
    l.MemBaseSet I c (h.convergenceR ε c) π →
      dist (BoxIntegral.integralSum f vol π) (∑ J ∈ π.boxes, BoxIntegral.integral J l f vol) ≤ ε
-- Mathlib.Topology.NhdsWithin
nhdsWithin_union : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (s t : Set α),
  nhdsWithin a (s ∪ t) = nhdsWithin a s ⊔ nhdsWithin a t
-- Mathlib.Combinatorics.Additive.Corner.Roth
/-- **Roth's theorem** for `ℕ`.

The maximum density of a 3AP-free set in `{1, ..., n}` goes to zero as `n` tends to infinity.  -/
roth_3ap_theorem_nat : ∀ {n : ℕ} (ε : ℝ), 0 < ε → cornersTheoremBound (ε / 3) ≤ n → ∀ A ⊆ Finset.range n, ε * ↑n ≤ ↑A.card → ¬ThreeAPFree ↑A
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
NonUnitalStarSubalgebra.topologicalClosure.congr_simp : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : Star A]
  [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A] [inst_5 : ContinuousStar A] [inst_6 : ContinuousConstSMul R A]
  [inst_7 : IsSemitopologicalSemiring A] (s s_1 : NonUnitalStarSubalgebra R A),
  s = s_1 → s.topologicalClosure = s_1.topologicalClosure
-- Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
/-- The obvious term in `Φ.Iteration ε ⊥` that is given by `Φ.X₀`.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfBot : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (Φ : CategoryTheory.SmallObject.SuccStruct C) →
      (J : Type u) →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] → [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] → Φ.Iteration ⊥
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_const_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {c : β}, MeasureTheory.Integrable (fun x => c) μ ↔ c = 0 ∨ MeasureTheory.IsFiniteMeasure μ
-- Mathlib.ModelTheory.Basic
/-- The sum of two languages consists of the disjoint union of their symbols.  -/
FirstOrder.Language.sum : FirstOrder.Language → FirstOrder.Language → FirstOrder.Language
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.size.eq_1 : ∀ {α : Type u} [inst : Std.Rxi.HasSize α] (r : Std.Rci α), r.size = Std.Rxi.HasSize.size r.lower
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_anti_mono_homogeneousIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {s t : HomogeneousIdeal 𝒜},
  s ≤ t → ProjectiveSpectrum.zeroLocus 𝒜 ↑t ⊆ ProjectiveSpectrum.zeroLocus 𝒜 ↑s
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- The isomorphism from `(mk' X₀ X₁ d₀ succ').X (n + 2)` that is given by
the inductive construction.  -/
ChainComplex.mk'XIso : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (X₀ X₁ : V) →
        (d₀ : X₁ ⟶ X₀) →
          (succ' :
              {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0) →
            (n : ℕ) →
              (ChainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').X (n + 2) ≅
                (succ' ((ChainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').d (n + 1) n)).fst
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_two_one_eq_chebyshev_S : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ), Polynomial.dickson 2 1 n = Polynomial.Chebyshev.S R ↑n
-- Lean.Meta.Sym.Arith.Types
/-- No algebraic structure found.  -/
Lean.Meta.Sym.Arith.ClassifyResult.none : Lean.Meta.Sym.Arith.ClassifyResult
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instCoproductsOfShapeDisjointSchemeOfSmall : ∀ {σ : Type v} [Small.{u, v} σ], CategoryTheory.Limits.CoproductsOfShapeDisjoint AlgebraicGeometry.Scheme σ
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.mkOfCompact_sub : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : CompactSpace α]
  (f g : C(α, β)),
  BoundedContinuousFunction.mkOfCompact (f - g) =
    BoundedContinuousFunction.mkOfCompact f - BoundedContinuousFunction.mkOfCompact g
-- Std.Data.TreeSet.Raw.Lemmas
_private.Std.Data.TreeSet.Raw.Lemmas.0.Std.TreeSet.Raw.ext : ∀ {α : Type u} {cmp : α → α → Ordering} {t t' : Std.TreeSet.Raw α cmp}, t.inner = t'.inner → t = t'
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.utf8ByteSize'.go.match_1.eq_1 : ∀ (motive : List Char → Sort u_1) (h_1 : Unit → motive []) (h_2 : (c : Char) → (cs : List Char) → motive (c :: cs)),
  (match [] with
    | [] => h_1 ()
    | c :: cs => h_2 c cs) =
    h_1 ()
-- Mathlib.MeasureTheory.Measure.Lebesgue.Integral
integral_comp_neg_Iic : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (c : ℝ) (f : ℝ → E),
  ∫ (x : ℝ) in Set.Iic c, f (-x) = ∫ (x : ℝ) in Set.Ioi (-c), f x
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- The representation of `s` in a local frame at `x` only depends on `s` at `x`.  -/
Bundle.Trivialization.localFrameCoeff_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7}
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_14 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F)
  [inst_15 : ContMDiffVectorBundle 1 F V I] {x : M} {s s' : (x : M) → V x} {i : ι},
  s x = s' x →
    (Bundle.Trivialization.localFrameCoeff I e b i x) (s x) = (Bundle.Trivialization.localFrameCoeff I e b i x) (s' x)
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.mapCoconeToOver_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F),
  c.mapCoconeToOver.inv.hom = CategoryTheory.CategoryStruct.id c.pt
-- Mathlib.Order.BoundedOrder.Basic
/-- An order is (noncomputably) either an `OrderTop` or a `NoTopOrder`. Use as
`cases topOrderOrNoTopOrder α`.  -/
topOrderOrNoTopOrder : (α : Type u_1) → [inst : LE α] → OrderTop α ⊕' NoTopOrder α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.mk.congr_simp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left left_1 : ψ.left ⟶ ψ'.left) (e_left : left = left_1)
  (right right_1 : ψ.right ⟶ ψ'.right) (e_right : right = right_1) (base base_1 : ψ.base ⟶ ψ'.base)
  (e_base : base = base_1)
  (left_coherence :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
        (CategoryTheory.Functor.whiskerRight left F') =
      CategoryTheory.CategoryStruct.comp (F.whiskerLeft base) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
  (right_coherence :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
        (CategoryTheory.Functor.whiskerRight right G') =
      CategoryTheory.CategoryStruct.comp (G.whiskerLeft base) (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom),
  { left := left, right := right, base := base, left_coherence := left_coherence, right_coherence := right_coherence } =
    { left := left_1, right := right_1, base := base_1, left_coherence := ⋯, right_coherence := ⋯ }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.any_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [LawfulHashable α] [EquivBEq α] {p : α → β → Bool},
  (↑m).WF →
    ((↑m).any p = false ↔
      ∀ (a : α) (h : m.contains a = true), p (m.getKey a h) (Std.DHashMap.Internal.Raw₀.Const.get m a h) = false)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.BinaryBiconeMorphism.wfst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B),
  CategoryTheory.CategoryStruct.comp self.hom B.fst = A.fst
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.sup_eq_closure_mul : ∀ {G : Type u_2} [inst : Group G] (H K : Subgroup G), H ⊔ K = Subgroup.closure (↑H * ↑K)
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.qParam.eq_1 : ∀ (h : ℝ) (z : ℂ), Function.Periodic.qParam h z = Complex.exp (2 * ↑Real.pi * Complex.I * z / ↑h)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpToOn.mono : ∀ {𝕜 : 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} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s → ∀ {t : Set E}, t ⊆ s → HasFTaylorSeriesUpToOn n f p t
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_39 : HAdd Std.Time.Week.Offset Std.Time.Minute.Offset Std.Time.Minute.Offset
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_of_mem_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∈ m.toList → k ∈ m
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofCommandInfo.injEq : ∀ (i i_1 : Lean.Elab.CommandInfo), (Lean.Elab.Info.ofCommandInfo i = Lean.Elab.Info.ofCommandInfo i_1) = (i = i_1)
-- Init.Data.SInt.IntToBitVec
Int64.toBitVec32_toISize : ∀ (n : Int64) (h : System.Platform.numBits = 32), n.toISize.toBitVec32 h = BitVec.signExtend 32 n.toBitVec
-- Std.Internal.Do.Order.Basic
/-- Binary meet (infimum)  -/
Lean.Order.meet : {α : Type u} → [Lean.Order.CompleteLattice α] → α → α → α
-- Mathlib.Topology.MetricSpace.Bounded
Bornology.IsBounded.closure : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α], Bornology.IsBounded s → Bornology.IsBounded (closure s)
-- Mathlib.Algebra.Notation.Lemmas
ite_nonneg : ∀ {α : Type u_1} [inst : Zero α] {p : Prop} [inst_1 : Decidable p] {a b : α} [inst_2 : LE α],
  0 ≤ a → 0 ≤ b → 0 ≤ if p then a else b
-- Mathlib.Combinatorics.Quiver.SingleObj
_private.Mathlib.Combinatorics.Quiver.SingleObj.0.Quiver.SingleObj.listToPath.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match a :: l with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_2 a l
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} {f g : sq₁ ⟶ sq₂},
  f = g ↔ f.τ₁ = g.τ₁ ∧ f.τ₂ = g.τ₂ ∧ f.τ₃ = g.τ₃ ∧ f.τ₄ = g.τ₄
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to the pullback of `f₁` and `f₂`.  -/
CategoryTheory.Limits.ChosenPullback₃.p₁₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {f₃ : X₃ ⟶ S} →
            {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
              {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃} →
                {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} →
                  (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) → h.pullback ⟶ h₁₂.pullback
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Equiv.prodCongrLeft.eq_1 : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂),
  Equiv.prodCongrLeft e =
    { toFun := fun ab => ((e ab.2) ab.1, ab.2), invFun := fun ab => ((e ab.2).symm ab.1, ab.2), left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.isFiniteMeasureZero : ∀ {α : Type u_1} {m0 : MeasurableSpace α}, MeasureTheory.IsFiniteMeasure 0
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.le : ℝ → ℝ → Prop
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.adjoin_toSubmodule : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (s : Set A),
  (NonUnitalAlgebra.adjoin R s).toSubmodule = Submodule.span R ↑(NonUnitalSubsemiring.closure s)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instLE : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [LE β] → LE (MeasureTheory.SimpleFunc α β)
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- The composition of two cocontinuous functors is cocontinuous.  -/
CategoryTheory.isCocontinuous_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (G : CategoryTheory.Functor C D) (G' : CategoryTheory.Functor D E) (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) {L : CategoryTheory.GrothendieckTopology E} [G.IsCocontinuous J K]
  [G'.IsCocontinuous K L], (G.comp G').IsCocontinuous J L
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.impIff.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_eq_ofNat : ∀ (n : ℕ) {h : n < UInt64.size}, UInt64.ofNatLT n h = UInt64.ofNat n
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_inter_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₂.isEmpty = true → (t₁ ∩ t₂).isEmpty = true