mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.MulticospanIndex.multicospan.match_1.eq_2 : ∀ {J : CategoryTheory.Limits.MulticospanShape}
  (motive : (x y : CategoryTheory.Limits.WalkingMulticospan J) → (x ⟶ y) → Sort u_3) (b : J.R)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingMulticospan J) → motive x x (CategoryTheory.Limits.WalkingMulticospan.Hom.id x))
  (h_2 :
    (b : J.R) →
      motive (CategoryTheory.Limits.WalkingMulticospan.left (J.fst b))
        (CategoryTheory.Limits.WalkingMulticospan.right b) (CategoryTheory.Limits.WalkingMulticospan.Hom.fst b))
  (h_3 :
    (b : J.R) →
      motive (CategoryTheory.Limits.WalkingMulticospan.left (J.snd b))
        (CategoryTheory.Limits.WalkingMulticospan.right b) (CategoryTheory.Limits.WalkingMulticospan.Hom.snd b)),
  (match CategoryTheory.Limits.WalkingMulticospan.left (J.fst b), CategoryTheory.Limits.WalkingMulticospan.right b,
      CategoryTheory.Limits.WalkingMulticospan.Hom.fst b with
    | x, .(x), CategoryTheory.Limits.WalkingMulticospan.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingMulticospan.left (J.fst b)), .(CategoryTheory.Limits.WalkingMulticospan.right b),
      CategoryTheory.Limits.WalkingMulticospan.Hom.fst b => h_2 b
    | .(CategoryTheory.Limits.WalkingMulticospan.left (J.snd b)), .(CategoryTheory.Limits.WalkingMulticospan.right b),
      CategoryTheory.Limits.WalkingMulticospan.Hom.snd b => h_3 b) =
    h_2 b
-- Mathlib.Algebra.Notation.Defs
VAdd.mk : {G : Type u} → {P : Type v} → (G → P → P) → VAdd G P
-- Mathlib.MeasureTheory.Measure.Dirac
/-- Dirac delta measures at two points are different if and only if the two points are different,
assuming the measurable space separates points.  -/
MeasureTheory.dirac_ne_dirac_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSpace.SeparatesPoints α] {x y : α},
  MeasureTheory.Measure.dirac x ≠ MeasureTheory.Measure.dirac y ↔ x ≠ y
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.instLinearMapClass : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N}, LinearMapClass (Q₁ →qᵢ Q₂) R M₁ M₂
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
contMDiffWithinAt_hom_bundle : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_5} {n : WithTop ℕ∞} {E₁ : B → Type u_6}
  {E₂ : B → Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_8} [inst_13 : NormedAddCommGroup EB]
  [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_9} [inst_15 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B] {EM : Type u_10} [inst_18 : NormedAddCommGroup EM]
  [inst_19 : NormedSpace 𝕜 EM] {HM : Type u_11} [inst_20 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  [inst_21 : TopologicalSpace M] [inst_22 : ChartedSpace HM M] [inst_23 : FiberBundle F₁ E₁]
  [inst_24 : VectorBundle 𝕜 F₁ E₁] [inst_25 : FiberBundle F₂ E₂] [inst_26 : VectorBundle 𝕜 F₂ E₂]
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  (f : M → Bundle.TotalSpace (F₁ →L[𝕜] F₂) fun b => E₁ b →L[𝕜] E₂ b) {s : Set M} {x₀ : M},
  ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂))) n f s x₀ ↔
    ContMDiffWithinAt IM IB n (fun x => (f x).proj) s x₀ ∧
      ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n
        (fun x => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ ⋯ ⋯ ⋯ ⋯ ⋯) s x₀
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_of_mul_apply_of_mem_zero : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddMonoid ι] [inst_5 : SetLike.GradedMonoid A] (r : ↥(A 0))
  (r' : DirectSum ι fun i => ↥(A i)) (j : ι), ↑(((DirectSum.of (fun i => ↥(A i)) 0) r * r') j) = ↑r * ↑(r' j)
-- Mathlib.Data.List.Lemmas
List.mapAccumr₂_eq_foldr : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} {φ : Type u_5} (f : α → β → σ → σ × φ) (as : List α) (bs : List β)
  (s : σ),
  List.mapAccumr₂ f as bs s =
    List.foldr
      (fun ab s =>
        have r := f ab.1 ab.2 s.1;
        (r.1, r.2 :: s.2))
      (s, []) (as.zip bs)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
CategoryTheory.Over.conePost_obj_pt : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) (i : J) (c : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Over.conePost F i).obj c).pt = CategoryTheory.Over.mk (c.π.app i)
-- Mathlib.Data.List.Rotate
List.IsRotated.map : ∀ {α : Type u} {β : Type u_1} {l₁ l₂ : List α}, l₁ ~r l₂ → ∀ (f : α → β), List.map f l₁ ~r List.map f l₂
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_smulc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : Zero β] [inst_3 : TopologicalSpace γ] [inst_4 : SMulZeroClass γ β] [inst_5 : ContinuousSMul γ β]
  {F : Type u_5} [inst_6 : FunLike F α γ] [inst_7 : ContinuousMapClass F α γ] (f : F)
  (g : CompactlySupportedContinuousMap α β), ⇑(f • g) = fun x => f x • g x
-- Mathlib.Data.Rat.Floor
/-- local copy tagged `meta` for evaluation of `round` below  -/
_private.Mathlib.Data.Rat.Floor.0.Rat.instFloorRing_1 : FloorRing ℚ
-- Aesop.Tree.Data
Aesop.GoalId.instHashable : Hashable Aesop.GoalId
-- Mathlib.Algebra.DirectSum.Module
DirectSum.congrLinearEquiv_toAddEquiv : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} {N : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (N i)]
  [inst_2 : (i : ι) → Module R (N i)] {P : ι → Type u_4} [inst_3 : (i : ι) → AddCommMonoid (P i)]
  [inst_4 : (i : ι) → Module R (P i)] (u : (i : ι) → N i ≃ₗ[R] P i),
  (DirectSum.congrLinearEquiv u).toAddEquiv = DirectSum.congrAddEquiv fun i => (u i).toAddEquiv
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.isOpen_iff_coe_preimage : ∀ {β : Type u_2} [inst : TopologicalSpace β] {ι : Type u_3} {U : ι → TopologicalSpace.Opens β} {s : Set β},
  TopologicalSpace.IsOpenCover U → (IsOpen s ↔ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' s))
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.isRat_zpow_pos : ∀ {α : Type u_1} [inst : DivisionRing α] {a : α} {b : ℤ} {nb : ℕ} {num : ℤ} {den : ℕ},
  Mathlib.Meta.NormNum.IsNat b nb →
    Mathlib.Meta.NormNum.IsRat (a ^ nb) num den → Mathlib.Meta.NormNum.IsRat (a ^ b) num den
-- Mathlib.RingTheory.Noetherian.Basic
Module.Finite.of_injective : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module S N] [IsNoetherian S N]
  {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (f : M →ₛₗ[σ] N),
  Function.Injective ⇑f → Module.Finite R M
-- Mathlib.Data.Finsupp.MonomialOrder
/-- Given a monomial order with bot, notation for the corresponding strict order relation on
`WithBot (σ →₀ ℕ)`  -/
MonomialOrder.«term_≺'[_]_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.image_eq_image : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c)
  [inst_2 : CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {i i' j : ι},
  c.Rel i j →
    c.Rel i' j → CategoryTheory.Limits.imageSubobject (C.d i j) = CategoryTheory.Limits.imageSubobject (C.d i' j)
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel_comp_mono : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) (g : B ⟶ C) [inst_2 : CategoryTheory.Limits.HasKernels V] [inst_3 : CategoryTheory.Limits.HasImages V]
  {D : V} (h : C ⟶ D) [inst_4 : CategoryTheory.Mono h]
  (w : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = 0),
  imageToKernel f (CategoryTheory.CategoryStruct.comp g h) w =
    CategoryTheory.CategoryStruct.comp (imageToKernel f g ⋯)
      ((CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp g h)).isoOfEq
          (CategoryTheory.Limits.kernelSubobject g) ⋯).inv
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.le_zpow_of_log_le : ∀ {x y : ℝ} {n : ℤ}, 0 < y → Real.log x ≤ ↑n * Real.log y → x ≤ y ^ n
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.mk : {α : Type u} →
  [toTopologicalSpace : TopologicalSpace α] →
    (uniformity : Filter (α × α)) →
      Filter.Tendsto Prod.swap uniformity uniformity →
        (uniformity.lift' fun s => SetRel.comp s s) ≤ uniformity →
          (∀ (x : α), nhds x = Filter.comap (Prod.mk x) uniformity) → UniformSpace α
-- Mathlib.Analysis.Calculus.DerivativeTest
deriv_neg_right_of_sign_deriv : ∀ {f : ℝ → ℝ} {x₀ : ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x₀ - x)) →
    ∀ᶠ (b : ℝ) in nhdsWithin x₀ (Set.Ioi x₀), deriv f b < 0
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_unitIso_hom_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (X : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (X_1 : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.equivComma.unitIso.hom.app X).app X_1 =
    (match X_1 with
      | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).hom
-- Mathlib.Order.Ideal
Order.Ideal.isMaximal_iff_isCoatom : ∀ {P : Type u_1} [inst : LE P] [inst_1 : IsDirectedOrder P] [inst_2 : Nonempty P] {I : Order.Ideal P},
  I.IsMaximal ↔ IsCoatom I
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.lt_largerSubobject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  (hG : CategoryTheory.IsSeparator G) {X : C} (A : CategoryTheory.Subobject X),
  A ≠ ⊤ → A < CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG A
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstr.h : Lean.Meta.Grind.AC.DiseqCnstr → Lean.Meta.Grind.AC.DiseqCnstrProof
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_sub_int_mul_pi : ∀ (x : ℝ) (n : ℤ), Real.sin (x - ↑n * Real.pi) = (-1) ^ n * Real.sin x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Helper function for reducing bitvector functions such as `getLsb` and `getMsb`.
 -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.reduceGetBit : Lean.Name → ({n : ℕ} → BitVec n → ℕ → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Algebra.Order.Ring.Defs
IsStrictOrderedRing.toCharZero : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R], CharZero R
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.degenerate_app_apply : ∀ {X Y : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := n })},
  x ∈ X.degenerate n →
    ∀ (f : X ⟶ Y), (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x ∈ Y.degenerate n
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.uniformContinuous_coe : ∀ (α : Type u_1) [inst : UniformSpace α], UniformContinuous UniformSpace.Completion.coe'
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_add_right_eq_map : ∀ {m n : ℕ}, (m<...m + 1 + n).toList = List.map (fun x => x + m + 1) (0...n).toList
-- Mathlib.Tactic.Conv
/-- `conv_lhs => cs` runs the `conv` tactic sequence `cs` on the left hand side of the target.

In general, for an `n`-ary operator as the target, it traverses into the second to last argument.
It is a synonym for `conv => arg -2; cs`.

* `conv_lhs at h => cs` runs `cs` on the left hand side of hypothesis `h`.
* `conv_lhs in pat => cs` first looks for a subexpression matching `pat` (see also the `pattern`
  conv tactic) and then traverses into the left hand side of this subexpression.
  This syntax also supports the `occs` clause for the pattern.
 -/
Mathlib.Tactic.Conv.convLHS : Lean.ParserDescr
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.SubarrayIterator.toList_eq : ∀ {α : Type u} {it : Std.Iter α},
  it.toList = List.drop it.internalState.xs.start (List.take it.internalState.xs.stop it.internalState.xs.array.toList)
-- Mathlib.RingTheory.Congruence.Hom
/-- The diagram describing the universal property for quotients of rings commutes.  -/
RingCon.lift_coe : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M} {f : M →+* P}
  (H : c ≤ RingCon.ker f) (x : M), (c.lift f H) ↑x = f x
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences_comm : ∀ {x y : NNReal}, x.agmSequences y = y.agmSequences x
-- Mathlib.RingTheory.Artinian.Module
/-- Any injective endomorphism of an Artinian module is bijective.  -/
IsArtinian.bijective_of_injective_endomorphism : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsArtinian R M]
  (f : M →ₗ[R] M), Function.Injective ⇑f → Function.Bijective ⇑f
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.instCreatesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfCreatesLimitOfIsCosplitPair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (adj : F ⊣ G) →
              [CategoryTheory.Comonad.CreatesLimitOfIsCosplitPair F] →
                (A : adj.toComonad.Coalgebra) →
                  CategoryTheory.CreatesLimit
                    (CategoryTheory.Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F
-- Lean.Setup
/-- Additional options for the module.  -/
Lean.ModuleSetup.options : Lean.ModuleSetup → Lean.LeanOptions
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKey_eq_get_maxKey? : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β} {he : l.isEmpty = false},
  l.maxKey he = l.maxKey?.get ⋯
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X A B Y : C} (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left
        (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso (CategoryTheory.Over.pullback f)
            (CategoryTheory.Over.mk gA) (CategoryTheory.Over.mk gB)).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst gA gB) gA) f)
        (CategoryTheory.Limits.pullback.snd gA gB)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk gA)).hom
        ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk gB)).hom)
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Over.mk gB).hom f)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin_symm : ∀ {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₁),
  (Matrix.toBilin b).symm = LinearMap.BilinForm.toMatrix b
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.Homotopy.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} {H : (i : E.I₀) → F.I₁ (f.s₀ i) (g.s₀ i)}
  {a : (i : E.I₀) → E.X i ⟶ F.Y (H i)}
  {wl : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a i) (F.p₁ (H i)) = f.h₀ i}
  {wr : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a i) (F.p₂ (H i)) = g.h₀ i}
  {H_1 : (i : E.I₀) → F.I₁ (f.s₀ i) (g.s₀ i)} {a_1 : (i : E.I₀) → E.X i ⟶ F.Y (H_1 i)}
  {wl_1 : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a_1 i) (F.p₁ (H_1 i)) = f.h₀ i}
  {wr_1 : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a_1 i) (F.p₂ (H_1 i)) = g.h₀ i},
  { H := H, a := a, wl := wl, wr := wr } = { H := H_1, a := a_1, wl := wl_1, wr := wr_1 } → H = H_1 ∧ a ≍ a_1
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_comp_equiv : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} (e : ι ≃ ι')
  (x : ι' → K), Height.logHeight (x ∘ ⇑e) = Height.logHeight x
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit : AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.counit =
  (CategoryTheory.NatIso.op AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity).inv
-- Mathlib.Order.DirSupClosed
DirSupInacc.of_isEmpty : ∀ {α : Type u_1} [inst : Preorder α] [IsEmpty α] {s : Set α}, DirSupInacc s
-- Mathlib.Order.Concept
Concept.intent_bot : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, ⊥.intent = Set.univ
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.splitMany_empty : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), BoxIntegral.Prepartition.splitMany I ∅ = ⊤
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.ZeroAtFilter.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero β] [inst_1 : TopologicalSpace β] (l : Filter α) (f : α → β),
  l.ZeroAtFilter f = Filter.Tendsto f l (nhds 0)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.starLift_symm_apply_apply : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : StarRing C]
  [inst_10 : StarModule R C] (φ : Unitization R A →⋆ₐ[R] C) (a : A), (Unitization.starLift.symm φ) a = φ ↑a
-- Mathlib.Order.CompleteLattice.Defs
sInf_le_of_le : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a b : α}, b ∈ s → b ≤ a → sInf s ≤ a
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.Hom.mk'.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnrichedOrdinary C}
  {f g : X ⟶ Y}
  (base' base'_1 : CategoryTheory.CatEnrichedOrdinary.homEquiv f ⟶ CategoryTheory.CatEnrichedOrdinary.homEquiv g),
  ({ base' := base' } = { base' := base'_1 }) = (base' = base'_1)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- If `s` is `C^k` on `e.baseSet`, so is its coefficient `b.localFrameCoeff e i`
in the local frame induced by `e`  -/
contMDiffOn_baseSet_localFrameCoeff : ∀ {𝕜 : 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]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {k : WithTop ℕ∞}
  [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I],
  ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x => ⟨x, s x⟩) e.baseSet →
    ∀ (i : ι),
      ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) k ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s)
        e.baseSet
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.Path.singleton.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v),
  SimpleGraph.Path.singleton h = SimpleGraph.Path.singleton h
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_add_right' : ∀ {α : Type u_2} [inst : AddGroup α] {t : Set α} {b : α}, (fun x => x + -b) '' t = (fun x => x + b) ⁻¹' t
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.adicAbv_natCast_le_one`.

---

The `v`-adic absolute value of a natural number is `≤ 1`.  -/
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (n : ℕ), (NumberField.HeightOneSpectrum.adicAbv K v) ↑n ≤ 1
-- Mathlib.Tactic.Polynomial.Core
/-- Read a `polynomial` extension from a declaration of the right type.  -/
Mathlib.Tactic.Polynomial.mkPolynomialExt : Lean.Name → Lean.ImportM Mathlib.Tactic.Polynomial.PolynomialExt
-- Mathlib.Computability.NFA
NFA.nil_mem_acceptsFrom : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) {S : Set σ}, [] ∈ M.acceptsFrom S ↔ ∃ s ∈ S, s ∈ M.accept
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.brecOn : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {motive : (a : L.BoundedFormula α n) → a.IsQF → Prop}
  {a : L.BoundedFormula α n} (t : a.IsQF),
  (∀ (a : L.BoundedFormula α n) (t : a.IsQF), FirstOrder.Language.BoundedFormula.IsQF.below t → motive a t) → motive a t
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- This typeclass expresses that the signs given by `[TotalComplexShapeSymmetry c₁ c₂ c₁₂]`
and by `[TotalComplexShapeSymmetry c₂ c₁ c₁₂]` are compatible.  -/
TotalComplexShapeSymmetrySymmetry : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) →
          (c₁₂ : ComplexShape I₁₂) →
            [inst : TotalComplexShape c₁ c₂ c₁₂] →
              [inst_1 : TotalComplexShape c₂ c₁ c₁₂] →
                [TotalComplexShapeSymmetry c₁ c₂ c₁₂] → [TotalComplexShapeSymmetry c₂ c₁ c₁₂] → Prop
-- Mathlib.Order.ULift
ULift.instPreorder : {α : Type u} → [Preorder α] → Preorder (ULift.{v, u} α)
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.eq_bot_of_equiv : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (p : Submodule R M) [inst_4 : Module R₂ M₂]
  (e : ↥p ≃ₛₗ[σ₁₂] ↥⊥), p = ⊥
-- Init.Data.Int.Gcd
Int.lcm_le_natAbs_mul : ∀ {a b : ℤ}, a ≠ 0 → b ≠ 0 → a.lcm b ≤ a.natAbs * b.natAbs
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.principalOpen_le : ∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] {x y : X},
  x ≤ y → Alexandrov.principalOpen y ≤ Alexandrov.principalOpen x