mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.comp_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G)
  (adj₂ : H ⊣ I),
  (adj₁.comp adj₂).counit =
    CategoryTheory.CategoryStruct.comp ((I.comp G).associator F H).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (I.associator G F).hom H)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (I.whiskerLeft adj₁.counit) H)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight I.rightUnitor.hom H) adj₂.counit)))
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.prevD_zero_cochainComplex : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (f : (i j : ℕ) → P.X i ⟶ Q.X j), (prevD 0) f = 0
-- Mathlib.Topology.Order.LeftRightLim
Function.leftLim.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] (f : α → β) (a : α),
  Function.leftLim f a =
    if nhdsWithin a (Set.Iio a) = ⊥ ∨ ¬∃ y, Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds y) then f a
    else (nhdsWithin a (Set.Iio a)).limUnder f
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_compContinuousLinearMap_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i →L[𝕜] E₁ i), ‖g.compContinuousLinearMap f‖ ≤ ‖g‖ * ∏ i, ‖f i‖
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.toPiNat.injEq : ∀ {ι : Type u_2} {X : Type u_5} {Y : ι → Type u_6} {f : (i : ι) → X → Y i} (ofPiNat ofPiNat_1 : X),
  ({ ofPiNat := ofPiNat } = { ofPiNat := ofPiNat_1 }) = (ofPiNat = ofPiNat_1)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.comm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} (φ : D₁ ⟶ D₂) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q) CategoryTheory.Pseudofunctor.DescentData'.comm._auto_1)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q) CategoryTheory.Pseudofunctor.DescentData'.comm._auto_3)
  {Z : ↑(F.obj { as := Opposite.op Y })} (h : (F.map f₂.op.toLoc).toFunctor.obj (D₂.obj i₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (φ.hom i₁))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' D₂.hom q f₁ f₂ hf₁ hf₂)
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' D₁.hom q f₁ f₂ hf₁ hf₂)
      (CategoryTheory.CategoryStruct.comp ((F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)) h)
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- A seminorm on a group `G` is a function `f : G → ℝ` that sends one to zero, is submultiplicative
and such that `f x⁻¹ = f x` and `f x = 0 → x = 1` for all `x`.  -/
GroupNorm : (G : Type u_6) → [Group G] → Type u_6
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- The linear map between `n`th exterior powers induced by a linear map between the modules.  -/
exteriorPower.map : {R : Type u} →
  [inst : CommRing R] →
    (n : ℕ) →
      {M : Type u_1} →
        {N : Type u_2} →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (M →ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] ↥(⋀[R]^n N)
-- Mathlib.Tactic.Rify
Mathlib.Tactic.Rify.ratCast_lt : ∀ (a b : ℚ), a < b ↔ ↑a < ↑b
-- Std.Http.Internal.Char
Std.Http.Internal.Char.quotedStringChar_lt_0x80 : ∀ {c : Char}, Std.Http.Internal.Char.quotedStringChar c = true → c < ''
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.coe_toBotHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β] (f : SupBotHom α β),
  ⇑f.toBotHom = ⇑f
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
isMIntegralCurve_iff_isMIntegralCurveAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x}, IsMIntegralCurve γ v ↔ ∀ (t : ℝ), IsMIntegralCurveAt γ v t
-- Lean.Meta.Basic
Lean.Meta.AbstractMVarsResult.mk : Array Lean.Name → Array Lean.Expr → Lean.Expr → Lean.Meta.AbstractMVarsResult
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.method : Lean.Lsp.SemanticTokenType
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabEnd : Lean.Elab.Command.CommandElab
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getD t.max! fallback = t.max!
-- Mathlib.Data.Set.Pairwise.List
List.Nodup.pairwise_of_set_pairwise : ∀ {α : Type u_1} {l : List α} {r : α → α → Prop}, l.Nodup → {x | x ∈ l}.Pairwise r → List.Pairwise r l
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.val_vadd_of_tower : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] [inst_2 : VAdd S R]
  [inst_3 : VAdd S M] [inst_4 : VAddAssocClass S R M] (p : SubAddAction R M) (s : S) (x : ↥p), ↑(s +ᵥ x) = s +ᵥ ↑x
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.mk.sizeOf_spec : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : SizeOf R] [inst_9 : SizeOf L] [inst_10 : SizeOf M] (toFun : L → R)
  (genWeightSpace_ne_bot' : LieModule.genWeightSpace M toFun ≠ ⊥),
  sizeOf { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' } = 1
-- Mathlib.Topology.Inseparable
Tendsto.specializes : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace Y] {f g : X → Y} {l : Filter X} {y : Y},
  Filter.Tendsto g l (nhds y) → (∀ (x : X), f x ⤳ g x) → Filter.Tendsto f l (nhds y)
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.ofAdd_bot : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderBot α], Multiplicative.ofAdd ⊥ = ⊥
-- Mathlib.Order.Filter.CountableSeparatingOn
Filter.exists_eventuallyEq_const_of_eventually_mem_of_forall_separating : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f : α → β} [Nonempty β] (p : Set β → Prop)
  {s : Set β} [HasCountableSeparatingOn β p s],
  (∀ᶠ (x : α) in l, f x ∈ s) →
    (∀ (U : Set β), p U → (∀ᶠ (x : α) in l, f x ∈ U) ∨ ∀ᶠ (x : α) in l, f x ∉ U) → ∃ a, f =ᶠ[l] Function.const α a
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.exists_eq_natCast_of_iSup_eq : ∀ {ι : Type u} [Nonempty ι] (f : ι → Cardinal.{v}), BddAbove (Set.range f) → ∀ (n : ℕ), ⨆ i, f i = ↑n → ∃ i, f i = ↑n
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- The presentation of `M.restrict f` by restricting a presentation of `M`.  -/
AlgebraicGeometry.Scheme.Modules.presentationRestrict : {X Y : AlgebraicGeometry.Scheme} →
  (f : Y ⟶ X) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      {M : X.Modules} → SheafOfModules.Presentation M → SheafOfModules.Presentation (M.restrict f)
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zero_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b)
  (hsq : (n : ℤ) → ⋯.LiftStruct) (n m : ℤ)
  (hnm : autoParam (n + 1 = m) CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zero._auto_1) {Z : C} (h : Y.X m ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm)
      (CategoryTheory.CategoryStruct.comp (p.f m) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_iff_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, a ∈ m ↔ (m.getKey? a).isSome = true
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.singleton_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {t : Set β} {a : α}, {a} +ᵥ t = a +ᵥ t
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_inv_atTop_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] {l : Filter α}
  {f : α → G}, Filter.Tendsto (fun x => (f x)⁻¹) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- Together `Matrix.diagonalInvertible` and `Matrix.invertibleOfDiagonalInvertible` form an
equivalence, although both sides of the equiv are subsingleton anyway.  -/
Matrix.diagonalInvertibleEquivInvertible : {n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (v : n → α) → Invertible (Matrix.diagonal v) ≃ Invertible v
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOfCoconeUnop_π : ∀ {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.unop),
  (CategoryTheory.Limits.coneOfCoconeUnop c).π = CategoryTheory.NatTrans.removeUnop c.ι
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair.mk : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], CategoryTheory.Limits.HasEqualizer f g) →
    CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair F
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.CanonM : Type → Type
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformationLabel : Type
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Int.range_castAddHom : ∀ {A : Type u_4} [inst : AddGroupWithOne A], (Int.castAddHom A).range = AddSubgroup.zmultiples 1
-- Mathlib.Topology.ShrinkingLemma
/-- **Shrinking lemma**. A point-finite open cover of a closed subset of a normal space can be
"shrunk" to a new closed cover so that each new closed set is contained in the corresponding
original open set. See also `exists_subset_iUnion_closure_subset` for a stronger statement.  -/
exists_subset_iUnion_closed_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} [NormalSpace X],
  IsClosed s →
    (∀ (i : ι), IsOpen (u i)) →
      (∀ x ∈ s, {i | x ∈ u i}.Finite) →
        s ⊆ ⋃ i, u i → ∃ v, s ⊆ Set.iUnion v ∧ (∀ (i : ι), IsClosed (v i)) ∧ ∀ (i : ι), v i ⊆ u i
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_eq_zero_iff : ∀ {x : ENNReal} {y : ℝ}, x ^ y = 0 ↔ x = 0 ∧ 0 < y ∨ x = ⊤ ∧ y < 0
-- Mathlib.Order.SuccPred.Archimedean
SuccOrder.forall_ne_bot_iff : ∀ {α : Type u_1} [Nontrivial α] [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] (P : α → Prop), (∀ (i : α), i ≠ ⊥ → P i) ↔ ∀ (i : α), P (SuccOrder.succ i)
-- Mathlib.Order.WithBot
WithTop.untop_coe : ∀ {α : Type u_1} (x : α) (h : optParam (↑x ≠ ⊤) ⋯), (↑x).untop h = x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblZ_of_Y_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 = Q 1 * P 2 → P 1 * Q 2 = W'.negY Q * P 2 → W'.dblZ P = 0
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.toList_flatMapM : ∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α Id]
  [Std.Iterators.Finite α₂ m] {f : β → m (Std.IterM m γ)} {it₁ : Std.Iter β},
  (Std.Iter.flatMapM f it₁).toList =
    List.flatten <$>
      (Std.Iter.mapM
          (fun b => do
            let __do_lift ← f b
            __do_lift.toList)
          it₁).toList
-- Init.Data.Array.Find
Array.finIdxOf?_empty : ∀ {α : Type u_1} {a : α} [inst : BEq α], #[].finIdxOf? a = none
-- Init.Data.Nat.Lemmas
Nat.eq_sub_of_add_eq : ∀ {a b c : ℕ}, c + b = a → c = a - b
-- Mathlib.AlgebraicGeometry.QuasiAffine
AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine : ∀ {X : AlgebraicGeometry.Scheme} [X.IsQuasiAffine], AlgebraicGeometry.IsOpenImmersion X.toSpecΓ
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_smul_right : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] (r : R₂) (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂),
  TensorProduct.map f (r • g) = r • TensorProduct.map f g
-- Mathlib.Combinatorics.Hindman
/-- **Alias** of `Hindman.FS.finsetSum`. -/
Hindman.FS.finset_sum : ∀ {M : Type u_1} [inst : AddCommMonoid M] (a : Stream' M) (s : Finset ℕ), s.Nonempty → ∑ i ∈ s, a.get i ∈ Hindman.FS a
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.preimage_frontier : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set Y), e.source ∩ ↑e ⁻¹' frontier s = e.source ∩ frontier (↑e ⁻¹' s)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negDblY_of_Y_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  Q 2 ≠ 0 →
    P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
      P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 → P 1 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3 → W'.negDblY P = (-W'.dblU P) ^ 3
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalPi_η : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : I → Type u₂}
  [inst_2 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)]
  (F : (i : I) → CategoryTheory.Functor (D i) (C i)) [inst_4 : (i : I) → (F i).Monoidal] (i : I),
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Functor.pi F) i = CategoryTheory.Functor.OplaxMonoidal.η (F i)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.mk.injEq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cone F} (hom : A.pt ⟶ B.pt)
  (w :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp hom (B.π.app j) = A.π.app j)
      CategoryTheory.Limits.ConeMorphism.w._autoParam)
  (hom_1 : A.pt ⟶ B.pt)
  (w_1 :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp hom_1 (B.π.app j) = A.π.app j)
      CategoryTheory.Limits.ConeMorphism.w._autoParam),
  ({ hom := hom, w := w } = { hom := hom_1, w := w_1 }) = (hom = hom_1)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_insertMany_of_contains : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  {ρ : Type w} [inst_2 : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : ρ} {k : α}, m.contains k = true → (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).contains k = true
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.mk.injEq : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {f : Polynomial R}
  (toIsAdjoinRoot : IsAdjoinRoot S f) (monic : f.Monic) (toIsAdjoinRoot_1 : IsAdjoinRoot S f) (monic_1 : f.Monic),
  ({ toIsAdjoinRoot := toIsAdjoinRoot, monic := monic } = { toIsAdjoinRoot := toIsAdjoinRoot_1, monic := monic_1 }) =
    (toIsAdjoinRoot = toIsAdjoinRoot_1)
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.unop_nonpos : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] {a : αᵐᵒᵖ}, MulOpposite.unop a ≤ 0 ↔ a ≤ 0
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.LiftHom.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        (CategoryTheory.FreeBicategory.of.obj a ⟶ CategoryTheory.FreeBicategory.of.obj b) →
          Mathlib.Tactic.BicategoryCoherence.LiftHom f
-- Mathlib.Order.SuccPred.Archimedean
Set.OrdConnected.isPredArchimedean : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] (s : Set α)
  [inst_3 : s.OrdConnected], IsPredArchimedean ↑s
-- Mathlib.Order.Monotone.Defs
instDecidableStrictMonoOnOfForallForallMemSetForallForallForallLt : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {f : α → β} → {s : Set α} → [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a < b → f a < f b)] → Decidable (StrictMonoOn f s)
-- Mathlib.Data.EReal.Basic
EReal.coe_ne_bot : ∀ (x : ℝ), ↑x ≠ ⊥
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.dist_pointReflection_self' : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (x y : P),
  dist ((AffineIsometryEquiv.pointReflection 𝕜 x) y) y = ‖2 • (x -ᵥ y)‖
-- Mathlib.RingTheory.GradedAlgebra.Basic
/-- The projection maps of a graded ring  -/
GradedRing.proj : {ι : Type u_1} →
  {A : Type u_3} →
    {σ : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : Semiring A] →
            [inst_3 : SetLike σ A] → [inst_4 : AddSubmonoidClass σ A] → (𝒜 : ι → σ) → [GradedRing 𝒜] → ι → A →+ A
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.coe_comp_monoidHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulOneClass α] [inst_4 : MulOneClass β] [inst_5 : MulOneClass γ] (f : β →*o γ) (g : α →*o β),
  ↑(f.comp g) = (↑f).comp ↑g
-- Mathlib.Algebra.Ring.Hom.Defs
RingHomClass.toAddMonoidHomClass : ∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} {inst : NonAssocSemiring α}
  {inst_1 : NonAssocSemiring β} {inst_2 : FunLike F α β} [self : RingHomClass F α β], AddMonoidHomClass F α β
-- Lean.Elab.PreDefinition.Structural.BRecOn
/-- Given the `recArgInfos` and the `motives`, infer the types of the `F` arguments to the `.brecOn`
combinators. This assumes that all `.brecOn` functions of a mutual inductive have the same structure.

It also undoes the permutation and packing done by `packMotives`
 -/
Lean.Elab.Structural.inferBRecOnFTypes : Array Lean.Elab.Structural.RecArgInfo → Lean.Elab.Structural.Positions → (ℕ → Lean.Expr) → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Data.Fintype.Perm
MulEquiv.instFintype : {α : Type u_4} →
  {β : Type u_5} →
    [inst : Mul α] → [inst_1 : Mul β] → [DecidableEq α] → [DecidableEq β] → [Fintype α] → [Fintype β] → Fintype (α ≃* β)
-- Lean.Server.Rpc.Basic
Lean.Server.RpcObjectStore.mk.inj : ∀ {aliveRefs : Lean.PersistentHashMap Lean.Lsp.RpcRef Lean.Server.ReferencedObject}
  {refsById : Lean.PersistentHashMap USize Lean.Lsp.RpcRef} {nextRef : USize} {wireFormat : Lean.Lsp.RpcWireFormat}
  {aliveRefs_1 : Lean.PersistentHashMap Lean.Lsp.RpcRef Lean.Server.ReferencedObject}
  {refsById_1 : Lean.PersistentHashMap USize Lean.Lsp.RpcRef} {nextRef_1 : USize}
  {wireFormat_1 : Lean.Lsp.RpcWireFormat},
  { aliveRefs := aliveRefs, refsById := refsById, nextRef := nextRef, wireFormat := wireFormat } =
      { aliveRefs := aliveRefs_1, refsById := refsById_1, nextRef := nextRef_1, wireFormat := wireFormat_1 } →
    aliveRefs = aliveRefs_1 ∧ refsById = refsById_1 ∧ nextRef = nextRef_1 ∧ wireFormat = wireFormat_1
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn_obj_eq_univ : ∀ {n : ℕ} (i : Fin (n + 1)) (m : ℕ),
  autoParam (m + 1 < n) SSet.horn_obj_eq_univ._auto_1 → (SSet.horn n i).obj (Opposite.op { len := m }) = Set.univ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {f : α → Bool}
  {k : α}, (Std.DTreeMap.filter (fun k x => f k) t).getKey? k = Option.filter f (t.getKey? k)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.instMonoιPi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I]
  [inst_2 : CategoryTheory.Limits.HasProduct I.left] [inst_3 : CategoryTheory.Limits.HasProduct I.right],
  CategoryTheory.Mono (CategoryTheory.Limits.Multiequalizer.ιPi I)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- `VectorMeasure.restrict` as an additive monoid homomorphism.  -/
MeasureTheory.VectorMeasure.restrictGm : {M : Type u_3} →
  [inst : AddCommMonoid M] →
    [inst_1 : TopologicalSpace M] →
      [inst_2 : ContinuousAdd M] →
        {α : Type u_4} →
          [inst_3 : MeasurableSpace α] → Set α → MeasureTheory.VectorMeasure α M →+ MeasureTheory.VectorMeasure α M
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.inf : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Min β]
  [ContinuousInf β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f ⊓ g)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Contravariant.toLeftCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : PartialOrder α] [inst_2 : MulLeftReflectLE α],
  Contravariant.toLeftCancelSemigroup = { toSemigroup := inst, toIsLeftCancelMul := ⋯ }
-- Mathlib.Algebra.Group.Basic
leftInverse_mul_left_div : ∀ {G : Type u_3} [inst : Group G] (c : G), Function.LeftInverse (fun x => x * c) fun x => x / c
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.coeff_mul_single_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ},
  (x * (HahnSeries.single 0) r).coeff a = x.coeff a * r
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preLeft_map_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) {X Y : CategoryTheory.Comma (F.comp L) R} (f : X ⟶ Y),
  ((CategoryTheory.Comma.preLeft F L R).map f).left = F.map f.left