mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Option.Lemmas
Option.isNone_filter : ∀ {α : Type u_1} {p : α → Bool} {o : Option α}, (Option.filter p o).isNone = Option.all (fun a => !p a) o
-- Init.Data.Array.Range
Array.snd_lt_of_mem_zipIdx : ∀ {α : Type u_1} {x : α × ℕ} {k : ℕ} {xs : Array α}, x ∈ xs.zipIdx k → x.2 < xs.size + k
-- Mathlib.Order.SuccPred.Basic
Order.max_of_succ_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α}, Order.succ a ≤ a → IsMax a
-- Lean.Meta.Basic
Lean.PPContext.runMetaM : {α : Type} → Lean.PPContext → Lean.MetaM α → IO α
-- Init.Data.List.Nat.Count
List.count_set : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {l : List α} {i : ℕ} (h : i < l.length),
  List.count b (l.set i a) = (List.count b l - if (l[i] == b) = true then 1 else 0) + if (a == b) = true then 1 else 0
-- Mathlib.Data.Nat.Init
Nat.decreasingInduction_succ : ∀ {m n : ℕ} {motive : (m : ℕ) → m ≤ n + 1 → Sort u_1}
  (of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯) (self : motive (n + 1) ⋯) (mn : m ≤ n)
  (msn : m ≤ n + 1),
  Nat.decreasingInduction of_succ self msn = Nat.decreasingInduction (fun x x_1 => of_succ x ⋯) (of_succ n ⋯ self) mn
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Cycle.formPerm_reverse : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (h : s.Nodup), s.reverse.formPerm ⋯ = (s.formPerm h)⁻¹
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono : ∀ {G : Type u_3} [inst : LinearOrderedCommGroupWithZero G] [inst_1 : LocallyFiniteOrder Gˣ],
  StrictMono ⇑(LocallyFiniteOrder.orderMonoidWithZeroHom G)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, k ∉ t₁ → (t₁ \ t₂).get! k = default
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_f_idem_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n : ℕ) {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.sum_repr' : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E),
  ∑ i, inner 𝕜 (b i) x • b i = x
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_add_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (c : F), fderiv 𝕜 (fun y => f y + c) x = fderiv 𝕜 f x
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
/-- The content induced by the linear functional `Λ`.  -/
rieszContent : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    [T2Space X] →
      [LocallyCompactSpace X] → (CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) → MeasureTheory.Content X
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instCompleteSemilatticeInf : {α : Type u_1} → {x : MeasurableSpace α} → CompleteSemilatticeInf (MeasureTheory.Measure α)
-- Init.Data.SInt.Lemmas
Int32.toInt_mul : ∀ (a b : Int32), (a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ 32)
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castAdd_Iio : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Finset.image (Fin.castAdd m) (Finset.Iio i) = Finset.Iio (Fin.castAdd m i)
-- Mathlib.Topology.NhdsSet
nhdsSet_univ : ∀ {X : Type u_2} [inst : TopologicalSpace X], nhdsSet Set.univ = ⊤
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.sSup_empty : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SupSet α], sSup ∅ = ⊥
-- Std.Data.DTreeMap.Internal.Def
/-- The "ratio" parameter of the size-bounded tree. Controls how aggressive the rebalancing
operations are.  -/
Std.DTreeMap.Internal.ratio : ℕ
-- Mathlib.Data.PEquiv
PEquiv.single_subsingleton_eq_refl : ∀ {α : Type u} [inst : DecidableEq α] [Subsingleton α] (a b : α), PEquiv.single a b = PEquiv.refl α
-- Mathlib.NumberTheory.Dioph
/-- The type of multivariate integer polynomials  -/
Poly : Type u → Type (max 0 u)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.mk.injEq : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  (toDiagram : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ) (top : J)
  (isTerminal : toDiagram.IsTerminal top) (uniq_terminal : ∀ (j : J) (hj : toDiagram.IsTerminal j), j = top)
  (toDiagram_1 : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ) (top_1 : J)
  (isTerminal_1 : toDiagram_1.IsTerminal top_1)
  (uniq_terminal_1 : ∀ (j : J) (hj : toDiagram_1.IsTerminal j), j = top_1),
  ({ toDiagram := toDiagram, top := top, isTerminal := isTerminal, uniq_terminal := uniq_terminal } =
      { toDiagram := toDiagram_1, top := top_1, isTerminal := isTerminal_1, uniq_terminal := uniq_terminal_1 }) =
    (toDiagram = toDiagram_1 ∧ top = top_1 ∧ isTerminal ≍ isTerminal_1)
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.integral_id_projectiveFamily : ∀ (I : Finset NNReal), ∫ (x : ↥I → ℝ), x ∂ProbabilityTheory.BrownianReal.projectiveFamily I = 0
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_sub_C : ∀ {R : Type u} {a : R} [inst : Ring R] {p : Polynomial R}, 0 < p.degree → (p - Polynomial.C a).degree = p.degree
-- Init.Data.Int.LemmasAux
Int.natAbs_pow_two : ∀ (a : ℤ), ↑a.natAbs ^ 2 = a ^ 2
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.rightUnitor_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Oplax.OplaxTrans.rightUnitor η).inv.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv
-- Mathlib.Algebra.Order.Monoid.Basic
/-- The order embedding sending `b` to `a + b`, for some fixed `a`.
See also `OrderIso.addLeft` when working in an additive ordered group.  -/
OrderEmbedding.addLeft : {α : Type u_2} → [inst : Add α] → [inst_1 : LinearOrder α] → [AddLeftStrictMono α] → α → α ↪o α
-- Mathlib.Order.Lattice.Nat
Nat.iInf_le_succ' : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ),
  ⨅ k, ⨅ (_ : k ≤ n + 1), u k = u 0 ⊓ ⨅ k, ⨅ (_ : k ≤ n), u (k + 1)
-- Mathlib.Algebra.Group.Action.Defs
MulOpposite.smul_eq_mul_unop : ∀ {α : Type u_5} [inst : Mul α] (a : αᵐᵒᵖ) (b : α), a • b = b * MulOpposite.unop a
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.tendsto_atTop_one : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G},
  Multipliable f → Filter.Tendsto f Filter.atTop (nhds 1)
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.fst : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {M' : Type u_3} [inst_1 : One M'] {f : α → M × M'},
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport fun a => (f a).1
-- Batteries.Data.Random.MersenneTwister
/-- 32 bit Mersenne Twister (MT19937) configuration.  -/
Batteries.Random.MersenneTwister.mt19937 : Batteries.Random.MersenneTwister.Config
-- Mathlib.Logic.Basic
Decidable.not_forall₂ : ∀ {α : Sort u_1} {p : α → Prop} {P : (x : α) → p x → Prop} [Decidable (∃ x, ∃ (h : p x), ¬P x h)]
  [(x : α) → (h : p x) → Decidable (P x h)], (¬∀ (x : α) (h : p x), P x h) ↔ ∃ x, ∃ (h : p x), ¬P x h
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Getting a constant LSB from a `BitVec`.
 -/
Std.Tactic.BVDecide.BVPred.getLsbD : {w : ℕ} → Std.Tactic.BVDecide.BVExpr w → ℕ → Std.Tactic.BVDecide.BVPred
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.CompleteEquipartiteSubgraph.verts.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (K : G.CompleteEquipartiteSubgraph r t),
  K.verts = K.parts.disjiUnion id ⋯
-- Mathlib.Algebra.Lie.Basic
/-- Lie algebra equivalences are reflexive.  -/
LieEquiv.refl : {R : Type u} → {L₁ : Type v} → [inst : CommRing R] → [inst_1 : LieRing L₁] → [inst_2 : LieAlgebra R L₁] → L₁ ≃ₗ⁅R⁆ L₁
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.instSubtypeMemSubgroup : ∀ {G : Type u_1} [inst : Group G] [IsZGroup G] (H : Subgroup G), IsZGroup ↥H
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.singleRuleTac.inj : ∀ {decl decl_1 : Lean.Name},
  Aesop.RuleTacDescr.singleRuleTac decl = Aesop.RuleTacDescr.singleRuleTac decl_1 → decl = decl_1
-- Mathlib.Topology.Bases
/-- In a separable space, a family of nonempty disjoint open sets is countable.  -/
Pairwise.countable_of_isOpen_disjoint : ∀ {α : Type u} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] {ι : Type u_2} {s : ι → Set α},
  Pairwise (Function.onFun Disjoint s) → (∀ (i : ι), IsOpen (s i)) → (∀ (i : ι), (s i).Nonempty) → Countable ι
-- Mathlib.GroupTheory.IsSubnormal
_private.Mathlib.GroupTheory.IsSubnormal.0.Subgroup.IsSubnormal.isSubnormal_iff.match_1_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Init.Data.Range.Polymorphic.Iterators
Std.Rxo.Iterator.upwardEnumerableLe_of_isPlausibleIndirectOutput : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] {it : Std.Iter α} {out : α},
  it.IsPlausibleIndirectOutput out → ∃ a, it.internalState.next = some a ∧ Std.PRange.UpwardEnumerable.LE a out
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] (ι : Type w)
  [inst_2 : CategoryTheory.Limits.HasFiniteProducts C] [inst_3 : Finite ι] (X : C) (j : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).hom
      (CategoryTheory.Limits.Pi.π (fun x => X) j) =
    CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.mulSingle_op : ∀ {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} [inst : (i : ι) → One (M i)] [inst_1 : (i : ι) → One (N i)]
  [inst_2 : DecidableEq ι] (op : (i : ι) → M i → N i),
  (∀ (i : ι), op i 1 = 1) → ∀ (i : ι) (x : M i), Pi.mulSingle i (op i x) = fun j => op j (Pi.mulSingle i x j)
-- Lean.Parser.Syntax
Lean.Parser.Command.infixr.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Meta.Tactic.SolveByElim
/-- Create or modify a `Config` which only accept solutions
for which every expression in `use` appears as a subexpression.
 -/
Lean.Meta.SolveByElim.SolveByElimConfig.requireUsingAll : optParam Lean.Meta.SolveByElim.SolveByElimConfig { } → List Lean.Expr → Lean.Meta.SolveByElim.SolveByElimConfig
-- Lean.Server.AsyncList
/-- Spawns a `Task` waiting on all elements.  -/
Lean.AsyncList.waitAll : {ε : Type u_1} → {α : Type u_2} → Lean.AsyncList ε α → Lean.Server.ServerTask (List α × Option ε)
-- Mathlib.Analysis.BoxIntegral.Basic
/-- If `f` is integrable on `I`, then `fun J ↦ integral J l f vol` is box-additive on subboxes of
`I`: if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, the sum of integrals
of `f` over the boxes of `π₁` is equal to the sum of integrals of `f` over the boxes of `π₂`.

See also `BoxIntegral.Integrable.toBoxAdditive` for a bundled version.  -/
BoxIntegral.Integrable.sum_integral_congr : ∀ {ι : 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 ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  [CompleteSpace F],
  BoxIntegral.Integrable I l f vol →
    ∀ {π₁ π₂ : BoxIntegral.Prepartition I},
      π₁.iUnion = π₂.iUnion →
        ∑ J ∈ π₁.boxes, BoxIntegral.integral J l f vol = ∑ J ∈ π₂.boxes, BoxIntegral.integral J l f vol
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.rightHom_inr : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (g : G),
  SemidirectProduct.rightHom (SemidirectProduct.inr g) = g
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instAntisymmLe : Std.Antisymm fun x1 x2 => x1 ⊆ x2
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_midpoint_left : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V]
  [inst_5 : Invertible 2] (p₁ p₂ : P), nndist (midpoint 𝕜 p₁ p₂) p₁ = ‖2‖₊⁻¹ * nndist p₁ p₂
-- Mathlib.GroupTheory.PGroup
IsPGroup.of_exponent_dvd_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {n : ℕ}, Monoid.exponent G ∣ p ^ n → IsPGroup p G
-- Mathlib.NumberTheory.PrimeCounting
Nat.primeCounting_one : Nat.primeCounting 1 = 0
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_comp_flip_mk : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {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 : N →ₗ[R] P) (m : M),
  LinearMap.rTensor M f ∘ₗ (TensorProduct.mk R N M).flip m = (TensorProduct.mk R P M).flip m ∘ₗ f
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.coe_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R], ↑1 = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- The obvious map `Cofork f g → Fork f.unop g.unop`  -/
CategoryTheory.Limits.Cofork.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : Cᵒᵖ} → {f g : X ⟶ Y} → CategoryTheory.Limits.Cofork f g → CategoryTheory.Limits.Fork f.unop g.unop
-- Lean.Util.Recognizers
Lean.Expr.eqOrIff? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Mathlib.Data.Nat.Factors
/-- The sets of factors of coprime `a` and `b` are disjoint  -/
Nat.coprime_primeFactorsList_disjoint : ∀ {a b : ℕ}, a.Coprime b → a.primeFactorsList.Disjoint b.primeFactorsList
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsTorsionFree : ∀ (K : Type u_1) [inst : Field K], Module.IsTorsionFree (NumberField.RingOfIntegers K) K
-- Mathlib.Order.Grade
/-- Lifts a graded order along a strictly monotone function.  -/
GradeMaxOrder.liftLeft : {𝕆 : Type u_1} →
  {ℙ : Type u_2} →
    {α : Type u_3} →
      [inst : Preorder 𝕆] →
        [inst_1 : Preorder ℙ] →
          [inst_2 : Preorder α] →
            [GradeMaxOrder 𝕆 α] →
              (f : 𝕆 → ℙ) →
                StrictMono f → (∀ (a b : 𝕆), a ⋖ b → f a ⋖ f b) → (∀ (a : 𝕆), IsMax a → IsMax (f a)) → GradeMaxOrder ℙ α
-- Mathlib.NumberTheory.Padics.PadicVal.Defs
/-- **Alias** of `padicValNat_def'`. -/
padicValNat.maxPowDiv_eq_multiplicity : ∀ {p n : ℕ}, p ≠ 1 → n ≠ 0 → padicValNat p n = multiplicity p n
-- Mathlib.RingTheory.WittVector.Teichmuller
_private.Mathlib.RingTheory.WittVector.Teichmuller.0.WittVector.teichmuller_mul_aux₁ : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {R : Type u_3} (x y : MvPolynomial R ℚ),
  WittVector.teichmullerFun p (x * y) = WittVector.teichmullerFun p x * WittVector.teichmullerFun p y
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instLEOrdinal : LE Std.Time.Millisecond.Ordinal
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.comp_d_eq_zero_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j k : ι}
  {j' k' : ι'} (hj' : e.f j = j'),
  c.next j = k →
    c'.next j' = k' →
      ∀ ⦃W : C⦄ (φ : W ⟶ K.X j),
        CategoryTheory.CategoryStruct.comp φ (K.d j k) = 0 ↔
          CategoryTheory.CategoryStruct.comp φ
              (CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').inv ((K.extend e).d j' k')) =
            0
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.whisker_extension : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  (t : CategoryTheory.Bicategory.LeftExtension f g) {x : B} (h : c ⟶ x),
  (t.whisker h).extension = CategoryTheory.CategoryStruct.comp t.extension h
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α],
  -a < b ↔ -b < a
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.locallyCompactSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], LocallyCompactSpace (TopologicalSpace.Compacts α) ↔ LocallyCompactSpace α
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_map_piCurry_symm : ∀ {ι : Type u_3} {κ : ι → Type u_4} {X : (i : ι) → κ i → Type u_5} {mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)}
  (μ : (i : ι) → (j : κ i) → MeasureTheory.Measure (X i j))
  [hμ : ∀ (i : ι) (j : κ i), MeasureTheory.IsProbabilityMeasure (μ i j)],
  MeasureTheory.Measure.map (⇑(MeasurableEquiv.piCurry X).symm)
      (MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.infinitePi fun j => μ i j) =
    MeasureTheory.Measure.infinitePi fun p => μ p.fst p.snd
-- Mathlib.Data.Set.Basic
Set.not_top_subset : ∀ {α : Type u} {s : Set α}, ¬⊤ ⊆ s ↔ ∃ a, a ∉ s
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.eventually_add_left_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddLeftInvariant] (t : G) {p : G → Prop}, (∀ᵐ (x : G) ∂μ, p (t + x)) ↔ ∀ᵐ (x : G) ∂μ, p x
-- Mathlib.Condensed.Solid
/-- The functor `Profinite.{u} ⥤ CondensedMod.{u} R` is a pointwise
right Kan extension of `finFree R : FintypeCat.{u} ⥤ CondensedMod.{u} R`
along `FintypeCat.toProfinite`.  -/
Condensed.profiniteSolidIsPointwiseRightKanExtension : (R : Type (u + 1)) →
  [inst : Ring R] →
    (CategoryTheory.Functor.RightExtension.mk (Condensed.profiniteSolid R)
        (Condensed.profiniteSolidCounit R)).IsPointwiseRightKanExtension
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.Braided.braided : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {D : Type u₂} {inst_3 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_4 : CategoryTheory.MonoidalCategory D} {inst_5 : CategoryTheory.BraidedCategory D}
  {F : CategoryTheory.Functor C D} [self : F.Braided] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.map (β_ X Y).hom) =
    CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.Functor.LaxMonoidal.μ F Y X)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.edist_eq_of_L1 : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)]
  (x y : PiLp 1 β), edist x y = ∑ i, edist (x.ofLp i) (y.ofLp i)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
_private.Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing.0.AlgebraicGeometry.PresheafedSpace.GlueData.«termπ₂_,_,_» : Lean.ParserDescr
-- Init.Omega.IntList
Lean.Omega.IntList.nil_add : ∀ (xs : Lean.Omega.IntList), [] + xs = xs
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_empty : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (w : ι → R) (z : ι → E), ∅.centerMass w z = 0
-- Mathlib.CategoryTheory.Monoidal.Subcategory
/-- This is the property that `P : ObjectProperty C` holds
for the unit of the monoidal category structure.  -/
CategoryTheory.ObjectProperty.ContainsUnit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.MonoidalCategory C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_eval_zero : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.eval 0 (Polynomial.Chebyshev.U R n) = ↑(if Even n then ↑(n / 2).negOnePow else 0)
-- Init.MetaTypes
/-- If `suggestions` is `true`, `simp?` will invoke the currently configured library suggestion engine on the current goal,
and attempt to use the resulting suggestions as parameters to the `simp` tactic.
 -/
Lean.Meta.Simp.Config.suggestions : Lean.Meta.Simp.Config → Bool
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- `Functor.map` of a monoidal functor as a `MonoidHom`.  -/
CategoryTheory.Functor.homMonoidHom : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v, u_1} C] →
      [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{w, u_2} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {M X : C} →
              [inst_4 : CategoryTheory.MonObj M] →
                (F : CategoryTheory.Functor C D) → [inst_5 : F.Monoidal] → (X ⟶ M) →* (F.obj X ⟶ F.obj M)
-- Mathlib.Analysis.Calculus.Deriv.Prod
HasDerivWithinAt.finCons : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : F' 0} {φs' : (i : Fin n) → F' i.succ},
  HasDerivWithinAt φ φ' s x →
    HasDerivWithinAt φs φs' s x → HasDerivWithinAt (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') s x
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
preserves binary coproducts.  -/
CategoryTheory.Limits.preservesBinaryCoproducts_of_preservesBinaryBiproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBinaryBiproducts F],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.algHomOfRightFDRepComp.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Finite G]
  (η η_1 : CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)),
  η = η_1 → TannakaDuality.FiniteGroup.algHomOfRightFDRepComp η = TannakaDuality.FiniteGroup.algHomOfRightFDRepComp η_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α}, t.WF → (Std.DTreeMap.Raw.map f t).getKey? k = t.getKey? k
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciInf_neg : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {p : Prop} {f : p → α}, ¬p → ⨅ (h : p), f h = sInf ∅
-- Mathlib.Order.Concept
lowerPolar_upperPolar_lowerPolar : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β),
  lowerPolar r (upperPolar r (lowerPolar r t)) = lowerPolar r t
-- Mathlib.Algebra.Quaternion
Quaternion.sub_im_self : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), a - a.im = ↑a.re
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_edist_eq_of_L1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x y : WithLp 1 (α × β)), edist x y = edist x.fst y.fst + edist x.snd y.snd
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSemigroupOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : Semigroup Mᵐᵒᵖ], DomMulAct.instSemigroupOfMulOpposite = inst