mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Star.LinearMap
ContinuousLinearMap.intrinsicStarModule : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : ContinuousStar E]
  [inst_13 : ContinuousStar F] [inst_14 : SMulCommClass R R F] [inst_15 : ContinuousConstSMul R F],
  StarModule R (WithConv (E →L[R] F))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfcₙ_nnreal_le : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_8 : NonnegSpectrumClass ℝ A]
  {f : NNReal → NNReal} {a : A} {c : NNReal}, (∀ x ∈ quasispectrum NNReal a, f x ≤ c) → ‖cfcₙ f a‖₊ ≤ c
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.closure_pow : ∀ {R : Type u_2} [inst : Semiring R] (s : Set R) (n : ℕ), AddSubmonoid.closure s ^ n = AddSubmonoid.closure (s ^ n)
-- Init.Data.UInt.Lemmas
USize.toUInt32_mod_of_dvd : ∀ (a b : USize), b.toNat ∣ 4294967296 → (a % b).toUInt32 = a.toUInt32 % b.toUInt32
-- Mathlib.Algebra.Homology.Factorizations.Basic
CochainComplex.degreewiseEpiWithInjectiveKernel.epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} {f : K ⟶ L}, CochainComplex.degreewiseEpiWithInjectiveKernel f → CategoryTheory.Epi f
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.toNonUnitalSubring_eq_top : ∀ {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  {S : NonUnitalSubalgebra R A}, S.toNonUnitalSubring = ⊤ ↔ S = ⊤
-- Std.Time.Time.PlainTime
/-- Converts a `PlainTime` value to the total number of nanoseconds.
 -/
Std.Time.PlainTime.toNanoseconds : Std.Time.PlainTime → Std.Time.Nanosecond.Offset
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.toLieModuleHom : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → (M ≃ₗ⁅R,L⁆ N) → M →ₗ⁅R,L⁆ N
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.m : Lean.Elab.Do.ControlStack → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C],
  autoParam (CategoryTheory.Limits.HasTerminal C) CategoryTheory.PreGaloisCategory.hasTerminal._autoParam →
    autoParam (CategoryTheory.Limits.HasPullbacks C) CategoryTheory.PreGaloisCategory.hasPullbacks._autoParam →
      autoParam (CategoryTheory.Limits.HasFiniteCoproducts C)
          CategoryTheory.PreGaloisCategory.hasFiniteCoproducts._autoParam →
        autoParam
            (∀ (G : Type u₂) [inst_1 : Group G] [Finite G],
              CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) C)
            CategoryTheory.PreGaloisCategory.hasQuotientsByFiniteGroups._autoParam →
          (∀ {X Y : C} (i : X ⟶ Y) [CategoryTheory.Mono i],
              ∃ Z u, Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk i u))) →
            CategoryTheory.PreGaloisCategory C
-- Mathlib.Data.ENNReal.Basic
ENNReal.iUnion_Icc_coe_nat : ∀ {a : ENNReal}, ⋃ n, Set.Icc a ↑n = Set.Ici a \ {⊤}
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
CategoryTheory.Limits.hasFiniteLimits_of_hasTerminal_and_pullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C]
  [CategoryTheory.Limits.HasPullbacks C], CategoryTheory.Limits.HasFiniteLimits C
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.mk : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] →
          [inst_2 : AddGroup G] →
            {S : AddGroupExtension N E G} →
              {E' : Type u_4} →
                [inst_3 : AddGroup E'] →
                  {S' : AddGroupExtension N E' G} →
                    (toAddEquiv : E ≃+ E') →
                      ⇑toAddEquiv ∘ ⇑S.inl = ⇑S'.inl → ⇑S'.rightHom ∘ ⇑toAddEquiv = ⇑S.rightHom → S.Equiv S'
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.eq_top_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S : Subalgebra R A},
  S = ⊤ ↔ ∀ (x : A), x ∈ S
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.lift_inr_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.lift Monoid.Coprod.inr Monoid.Coprod.inl = Monoid.Coprod.swap M N
-- Init.Data.SInt.Basic
/-- The modulo operator for 32-bit signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by `Int32.div`. Usually accessed via the `%`
operator.

When the divisor is `0`, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int32.mod 5 2 = 1`
* `Int32.mod 5 (-2) = 1`
* `Int32.mod (-5) 2 = (-1)`
* `Int32.mod (-5) (-2) = (-1)`
* `Int32.mod 4 2 = 0`
* `Int32.mod 4 (-2) = 0`
* `Int32.mod 4 0 = 4`
* `Int32.mod (-4) 0 = (-4)`
 -/
Int32.mod : Int32 → Int32 → Int32
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} {h : k' ∈ Std.DHashMap.Const.modify m k f},
  (Std.DHashMap.Const.modify m k f).getKey k' h = if (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.transport_δ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (i : F ≅ G) (X Y : C) {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (G.obj X) (G.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ G X Y) h =
    CategoryTheory.CategoryStruct.comp (i.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom (i.hom.app X) (i.hom.app Y)) h))
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.equivalence_counitIso : AddMonCat.equivalence.counitIso =
  CategoryTheory.Iso.refl
    ({ obj := fun X => AddMonCat.of (Additive ↑X),
          map := fun {X Y} f => AddMonCat.ofHom (MonoidHom.toAdditive (MonCat.Hom.hom f)),
          map_id := AddMonCat.equivalence._proof_3, map_comp := @AddMonCat.equivalence._proof_4 }.comp
      { obj := fun X => MonCat.of (Multiplicative ↑X),
        map := fun {X Y} f => MonCat.ofHom (AddMonoidHom.toMultiplicative (AddMonCat.Hom.hom f)),
        map_id := AddMonCat.equivalence._proof_1, map_comp := @AddMonCat.equivalence._proof_2 })
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset.congr_simp : ∀ {α : Type u} {s s_1 : Set α} (e_s : s = s_1) (h : s.Finite), h.toFinset = ⋯.toFinset
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.inhabitedCocone : {C : Type u₃} →
  [inst : CategoryTheory.Category.{v₃, u₃} C] →
    (F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) C) →
      Inhabited (CategoryTheory.Limits.Cocone F)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.StackEntry.expr.inj : ∀ {info info_1 : Lean.Meta.RefinedDiscrTree.ExprInfo},
  Lean.Meta.RefinedDiscrTree.StackEntry.expr info = Lean.Meta.RefinedDiscrTree.StackEntry.expr info_1 → info = info_1
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_succ_right_eq_cons_map : ∀ {m n : ℤ}, m < n → (m<...n + 1).toList = (m + 1) :: List.map (fun x => x + 1) (m<...n).toList
-- Mathlib.Probability.ProbabilityMassFunction.Monad
/-- The pure `PMF` is the `PMF` where all the mass lies in one point.
The value of `pure a` is `1` at `a` and `0` elsewhere.  -/
PMF.pure : {α : Type u_1} → α → PMF α
-- Mathlib.Analysis.Normed.Order.UpperLower
closure_upperClosure_comm_pi : ∀ {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)}, BddBelow s → closure ↑(upperClosure s) = ↑(upperClosure (closure s))
-- Mathlib.Data.Int.Init
Int.div_le_iff_of_dvd_of_neg : ∀ {a b c : ℤ}, b < 0 → b ∣ a → (a / b ≤ c ↔ b * c ≤ a)
-- Mathlib.Tactic.SetNotationForOrder
/-- Strict subset relation: `a ⊂ b`.
For types tagged with `@[use_set_notation_for_order]`,
the relation `LT.lt` is used instead of `SSubset`.
The hover info shows which one is used. 

Conventions for notations in identifiers:

 * The recommended spelling of `⊂` in identifiers is `ssubset`. -/
Mathlib.Meta.SetNotationForOrder.ssubsetStx' : Lean.TrailingParserDescr
-- Batteries.Data.Array.Match
/-- Extend a prefix table by one element

If `t` is the prefix table for `xs` then `t.extend x` is the prefix table for `xs.push x`.
 -/
Array.PrefixTable.extend : {α : Type u_1} → [BEq α] → Array.PrefixTable α → α → Array.PrefixTable α
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.ofFun_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : Sub β] (f g : α → β),
  UniformFun.ofFun (f - g) = UniformFun.ofFun f - UniformFun.ofFun g
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- `symm` is `true` when rewriting from right to left  -/
Mathlib.Tactic.LibraryRewrite.RewriteLemma.symm : Mathlib.Tactic.LibraryRewrite.RewriteLemma → Bool
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- **Alias** of `BoundedContinuousFunction.domRestrict_apply`. -/
BoundedContinuousFunction.restrict_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  (f : BoundedContinuousFunction α β) (s : Set α) (x : ↑s), (f.domRestrict s) x = f ↑x
-- Init.Data.Vector.Lemmas
Vector.getElem?_toArray : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, xs.toArray[i]? = xs[i]?
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) {Z : AddCommGrpCat}
  (h_1 : F.H' n₁ S.X₂ ⊞ F.H' n₁ S.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.δ F n₀ n₁ h) (CategoryTheory.CategoryStruct.comp (S.toBiprod F n₁) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.powerFunctor.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (α α_1 : Type t) (e_α : α = α_1)
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C],
  CategoryTheory.Limits.FormalCoproduct.powerFunctor α = CategoryTheory.Limits.FormalCoproduct.powerFunctor α_1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.neg.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr},
  Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.neg c = Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.neg c_1 → c = c_1
-- Mathlib.RingTheory.Localization.Defs
/-- Map a homomorphism `g : R →+* P` to `S →+* Q`, where `S` and `Q` are
localizations of `R` and `P` at `M` and `T` respectively,
such that `g(M) ⊆ T`.

We send `z : S` to `algebraMap P Q (g x) * (algebraMap P Q (g y))⁻¹`, where
`(x, y) : R × M` are such that `z = f x * (f y)⁻¹`.  -/
IsLocalization.map : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Submonoid R} →
      {S : Type u_2} →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            {P : Type u_3} →
              [inst_3 : CommSemiring P] →
                [IsLocalization M S] →
                  {T : Submonoid P} →
                    (Q : Type u_4) →
                      [inst_5 : CommSemiring Q] →
                        [inst_6 : Algebra P Q] →
                          [IsLocalization T Q] → (g : R →+* P) → M ≤ Submonoid.comap g T → S →+* Q
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.card_edgeFinset_replaceVertex_of_adj : ∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} [inst : DecidableEq V] [inst_1 : Fintype V]
  [inst_2 : DecidableRel G.Adj],
  G.Adj s t → (G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t - 1
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHSubOffset_3 : HSub Std.Time.WallTime Std.Time.Minute.Offset Std.Time.WallTime
-- Aesop.RuleTac.GoalDiff
Aesop.GoalDiff.mk.sizeOf_spec : ∀ (oldGoal newGoal : Lean.MVarId) (addedFVars removedFVars : Std.HashSet Lean.FVarId) (targetChanged : Bool),
  sizeOf
      { oldGoal := oldGoal, newGoal := newGoal, addedFVars := addedFVars, removedFVars := removedFVars,
        targetChanged := targetChanged } =
    1 + sizeOf oldGoal + sizeOf newGoal + sizeOf addedFVars + sizeOf removedFVars + sizeOf targetChanged
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp.eq_2 : ∀ (C : Type u) (x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C CategoryTheory.FreeMonoidalCategory.unit x =
    CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := x.as })
-- Mathlib.Data.Nat.Log
Nat.clog.eq_1 : ∀ (b n : ℕ), Nat.clog b n = if 1 < b ∧ 1 < n then (Nat.clog.go n b n).2 + 1 else 0
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_right_injective : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : (i : Fin n) → α i.castSucc), Function.Injective (Fin.snoc x)
-- Lean.SubExpr
Lean.SubExpr.instFromJsonFVarId : Lean.FromJson Lean.FVarId
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhdsLT_neBot : ∀ {x : ENNReal} [NeZero x], (nhdsWithin x (Set.Iio x)).NeBot
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.encodeSubtype.match_1.splitter : {α : Type u_1} →
  {P : α → Prop} →
    (motive : { a // P a } → Sort u_2) →
      (x : { a // P a }) → ((v : α) → (property : P v) → motive ⟨v, property⟩) → motive x
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.zero_def : ∀ {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)},
  0 =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.mk Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
      fun x => 0
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
CategoryTheory.HasForget₂.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : outParam (C → C → Type u_2)} →
      {CC : outParam (C → Type w)} →
        [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {D : Type u_3} →
              [inst_3 : CategoryTheory.Category.{v_2, u_3} D] →
                {FD : outParam (D → D → Type u_4)} →
                  {CD : outParam (D → Type w)} →
                    [inst_4 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] →
                      [inst_5 : CategoryTheory.ConcreteCategory D FD] →
                        (forget₂ : CategoryTheory.Functor C D) →
                          autoParam (forget₂.comp (CategoryTheory.forget D) = CategoryTheory.forget C)
                              CategoryTheory.HasForget₂.forget_comp._autoParam →
                            CategoryTheory.HasForget₂ C D
-- Init.Data.String.Termination
String.Slice.Pos.remainingBytes_eq_byteDistance : ∀ {s : String.Slice} {p : s.Pos}, p.remainingBytes = p.offset.byteDistance s.endPos.offset
-- Mathlib.Logic.Function.Basic
Function.RightInverse.injective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.RightInverse f g → Function.Injective f
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.invEquivalence_counitIso : ∀ (C : Type u) [inst : CategoryTheory.Groupoid C],
  (CategoryTheory.Groupoid.invEquivalence C).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          (({ obj := Opposite.unop, map := fun {x y} f => CategoryTheory.Groupoid.inv f.unop, map_id := ⋯,
                    map_comp := ⋯ }.comp
                { obj := Opposite.op, map := fun {x x_1} f => (CategoryTheory.Groupoid.inv f).op, map_id := ⋯,
                  map_comp := ⋯ }).obj
            x))
      ⋯
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the right adjoint is fully faithful, then the counit is an isomorphism.  -/
CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.Full] [R.Faithful],
  CategoryTheory.IsIso h.counit
-- Mathlib.Tactic.DeriveCountable
/-- Initialize the injectivity argument. Pops the constructor tag.
 -/
Mathlib.Deriving.Countable.cons_eq_imp_init : ∀ {p : Prop} {a b b' : ℕ}, (b = b' → p) → Nat.pair a b = Nat.pair a b' → p
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_neg_index : ∀ {α : Type u_1} {M : Type u_8} {G : Type u_12} [inst : SubtractionMonoid G] [inst_1 : AddCommMonoid M] {g : α →₀ G}
  {h : α → G → M}, (∀ (a : α), h a 0 = 0) → (-g).sum h = g.sum fun a b => h a (-b)
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {x y : αᵒᵈ},
  Set.Ioo (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Ioo x y
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.isoOfEquiv_hom : ∀ {C D : CategoryTheory.Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X)
  (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y)
  (h₃ : autoParam (∀ (X : ↑C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯) CategoryTheory.Cat.isoOfEquiv._auto_1)
  (h₄ : autoParam (∀ (Y : ↑D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯) CategoryTheory.Cat.isoOfEquiv._auto_3),
  (CategoryTheory.Cat.isoOfEquiv e h₁ h₂ h₃ h₄).hom = e.functor.toCatHom
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Seq.unionFuel.match_1.eq_3 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq)
  (x₂ : Lean.Grind.AC.Var)
  (h_1 : (x₁ x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.var x₂))
  (h_2 :
    (x₁ x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.cons x s))
  (h_3 :
    (x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x₂))
  (h_4 :
    (x₁ : Lean.Grind.AC.Var) →
      (s₁ : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) →
          (s₂ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x₁ s₁) (Lean.Grind.AC.Seq.cons x₂ s₂)),
  (match Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x₂ with
    | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.var x₂ => h_1 x₁ x₂
    | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.cons x s => h_2 x₁ x s
    | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x₂ => h_3 x s x₂
    | Lean.Grind.AC.Seq.cons x₁ s₁, Lean.Grind.AC.Seq.cons x₂ s₂ => h_4 x₁ s₁ x₂ s₂) =
    h_3 x s x₂
-- Mathlib.GroupTheory.GroupAction.Pointwise
/-- `preimage_smul_setₛₗ` when `c` is a unit and `σ` is a monoid homomorphism.  -/
IsUnit.preimage_smul_setₛₗ : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Monoid M] [inst_1 : Monoid N]
  [inst_2 : MulAction M α] [inst_3 : MulAction N β] {c : M} {F : Type u_6} {G : Type u_7} [inst_4 : FunLike G M N]
  [MonoidHomClass G M N] (σ : G) [inst_6 : FunLike F α β] [MulActionSemiHomClass F (⇑σ) α β] (f : F),
  IsUnit c → ∀ (t : Set β), ⇑f ⁻¹' (σ c • t) = c • ⇑f ⁻¹' t
-- Init.Core
/-- `break s` means that `break` was called, meaning that we should exit
from the containing loop  -/
DoResultBC.break : {σ : Type u} → σ → DoResultBC σ
-- Lean.DocString.Markdown
/-- The current code is inside a link's display text.  -/
Lean.Doc.MarkdownM.InlineCtx.inLink : Lean.Doc.MarkdownM.InlineCtx → Bool
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.norm_kahler : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), ‖(o.kahler x) y‖ = ‖x‖ * ‖y‖
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `f` is a monotone function taking values in a conditionally complete linear order
and `g` tends to `atTop` along a nontrivial filter,
then the indexed supremum of `f ∘ g` is equal to the indexed supremum of `f`.  -/
Monotone.ciSup_comp_tendsto_atTop_of_linearOrder : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : ConditionallyCompleteLinearOrder γ]
  {l : Filter α} [l.NeBot] {f : β → γ},
  Monotone f → ∀ {g : α → β}, Filter.Tendsto g l Filter.atTop → ⨆ a, f (g a) = ⨆ b, f b
-- Mathlib.Data.Set.Function
Set.Subsingleton.injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Subsingleton → ∀ (f : α → β), Set.InjOn f s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Equivalence.mapMon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [inst_6 : e.IsMonoidal],
  e.mapMon =
    { functor := e.functor.mapMon, inverse := e.inverse.mapMon,
      unitIso :=
        CategoryTheory.Functor.mapMonIdIso.symm ≪≫
          CategoryTheory.Functor.mapMonNatIso e.unitIso ≪≫ CategoryTheory.Functor.mapMonCompIso,
      counitIso :=
        CategoryTheory.Functor.mapMonCompIso.symm ≪≫
          CategoryTheory.Functor.mapMonNatIso e.counitIso ≪≫ CategoryTheory.Functor.mapMonIdIso,
      functor_unitIso_comp := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Walk.Chord
SimpleGraph.Walk.IsChordless.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.IsChordless = ∀ ⦃e : Sym2 V⦄, ¬p.IsChord e
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.tensorUnit_whiskerLeft_comp_leftUnitor_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) f)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Functor.LaxMonoidal.ε F) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
        (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom))
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.isoBiproductEmbedding_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (M : CategoryTheory.Mat_ C),
  M.isoBiproductEmbedding.inv =
    CategoryTheory.Limits.biproduct.desc fun i x k => if h : i = k then CategoryTheory.eqToHom ⋯ else 0