mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.Expanded.const.sizeOf_spec : ∀ (c : Lean.Term), sizeOf (Mathlib.Tactic.LinearCombinationPrime.Expanded.const c) = 1 + sizeOf c
-- Init.GetElem
/-- The syntax `arr[i]?` gets the `i`'th element of the collection `arr` or
returns `none` if `i` is out of bounds.


Conventions for notations in identifiers:

 * The recommended spelling of `xs[i]?` in identifiers is `getElem?`. -/
«term__[_]_?» : Lean.TrailingParserDescr
-- Mathlib.Probability.Kernel.Disintegration.Basic
/-- A conditional kernel is almost everywhere a probability measure.  -/
ProbabilityTheory.Kernel.IsCondKernel.isProbabilityMeasure_ae : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} (κ : ProbabilityTheory.Kernel α (β × Ω)) (κCond : ProbabilityTheory.Kernel (α × β) Ω)
  [ProbabilityTheory.IsFiniteKernel κ.fst] [κ.IsCondKernel κCond] (a : α),
  ∀ᵐ (b : β) ∂κ.fst a, MeasureTheory.IsProbabilityMeasure (κCond (a, b))
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev_toSlice : ∀ {s : String} {p : s.Pos} {h : p.toSlice ≠ s.toSlice.startPos}, p.toSlice.prev h = (p.prev ⋯).toSlice
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instSub.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  LowerSet.instSub = { sub := fun s t => { carrier := Set.image2 (fun x1 x2 => x1 - x2) ↑s ↑t, lower' := ⋯ } }
-- Mathlib.Algebra.Group.Basic
left_ne_mul : ∀ {M : Type u_4} [inst : Monoid M] [IsLeftCancelMul M] {a b : M}, a ≠ a * b ↔ b ≠ 1
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- `f : X ⟶ Y` is right homotopic to itself relative to any path object.  -/
HomotopicalAlgebra.PathObject.RightHomotopy.refl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        (P : HomotopicalAlgebra.PathObject Y) → (f : X ⟶ Y) → P.RightHomotopy f f
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.insidePart_add : ∀ {p q : DyckWord}, p ≠ 0 → (p + q).insidePart = p.insidePart
-- Mathlib.Data.Bool.Basic
Bool.eq_not_iff : ∀ {a b : Bool}, a = !b ↔ a ≠ b
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.matcherName : Lean.Meta.MatcherApp → Lean.Name
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.Y_eq_iff' : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  P 2 ≠ 0 → Q 2 ≠ 0 → (P 1 * Q 2 = W.negY Q * P 2 ↔ P 1 / P 2 = W.toAffine.negY (Q 0 / Q 2) (Q 1 / Q 2))
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- The map to an object from the initial object.  -/
CategoryTheory.Limits.initial.to : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → [inst_1 : CategoryTheory.Limits.HasInitial C] → (P : C) → ⊥_ C ⟶ P
-- Mathlib.LinearAlgebra.TensorProduct.Basis
Module.Basis.baseChange.eq_1 : ∀ {R : Type u_1} {M : Type u_3} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (S : Type u_7) [inst_3 : Semiring S] [inst_4 : Algebra R S] (b : Module.Basis ι R M),
  Module.Basis.baseChange S b = ((Module.Basis.singleton Unit S).tensorProduct b).reindex (Equiv.punitProd ι)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mk_surjective : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R}, Function.Surjective ⇑(AdjoinRoot.mk g)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.instDecidablePredMemSubgroupStabilizerOfDecidableEq.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : DecidableEq α] (a : α) (x : G),
  MulAction.instDecidablePredMemSubgroupStabilizerOfDecidableEq a x =
    MulAction.instDecidablePredMemSubgroupStabilizerOfDecidableEq._aux_1 a x
-- Mathlib.Order.Filter.IndicatorFunction
Monotone.tendsto_mulIndicator : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} [inst : Preorder ι] [inst_1 : One β] (s : ι → Set α),
  Monotone s →
    ∀ (f : α → β) (a : α),
      Filter.Tendsto (fun i => (s i).mulIndicator f a) Filter.atTop (pure ((⋃ i, s i).mulIndicator f a))
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- The `sInf` of a bounded-below set is its greatest lower bound for a conditionally
complete lattice with a top.  -/
WithTop.isGLB_sInf' : ∀ {β : Type u_5} [inst : ConditionallyCompleteLattice β] {s : Set (WithTop β)}, BddBelow s → IsGLB s (sInf s)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.basicOpen_one : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens}, X.basicOpen 1 = U
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- Morphisms `homotopyCofiber φ ⟶ K` are uniquely determined by
a morphism `α : G ⟶ K` and a homotopy from `φ ≫ α` to `0`.  -/
HomologicalComplex.homotopyCofiber.descEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) →
              [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
                [inst_3 : DecidableRel c.Rel] →
                  (K : HomologicalComplex C c) →
                    (∀ (j : ι), ∃ i, c.Rel i j) →
                      (α : G ⟶ K) × Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0 ≃
                        (HomologicalComplex.homotopyCofiber φ ⟶ K)
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.DiagnosticsState.mk : IO.Ref (Lean.PersistentArray Lean.Widget.InteractiveDiagnostic) →
  Lean.PersistentArray Lean.Widget.InteractiveDiagnostic → Bool → ℕ → Lean.Server.FileWorker.DiagnosticsState
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Clz
Std.Tactic.BVDecide.BVExpr.bitblast.blastClz : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.sum_single_index : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {N : Type u_3} [inst_1 : AddCommMonoid N] {a : G} {b : k}
  {h : G → k → N}, h a 0 = 0 → (SkewMonoidAlgebra.single a b).sum h = h a b
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapCocycles₁_comp_i_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{max u u_1, u, u} k H}
  {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k}
  (h : (groupCohomology.shortComplexH1 B).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.mapCocycles₁ f φ)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH1 B).moduleCatLeftHomologyData.i h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.i
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap₁ f φ) h)
-- Mathlib.CategoryTheory.Action.Basic
CategoryTheory.Functor.mapActionComp_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} W] (G : Type u_3) [inst_2 : Monoid G] {T : Type u_4}
  [inst_3 : CategoryTheory.Category.{v_3, u_4} T] (F : CategoryTheory.Functor V W) (F' : CategoryTheory.Functor W T),
  (CategoryTheory.Functor.mapActionComp G F F').hom =
    { app := fun X => CategoryTheory.CategoryStruct.id (((F.comp F').mapAction G).obj X), naturality := ⋯ }
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coordChangeHomeomorph.congr_simp : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e₁ e₁_1 : Bundle.Trivialization F proj) (e_e₁ : e₁ = e₁_1)
  (e₂ e₂_1 : Bundle.Trivialization F proj) (e_e₂ : e₂ = e₂_1) {b b_1 : B} (e_b : b = b_1) (h₁ : b ∈ e₁.baseSet)
  (h₂ : b ∈ e₂.baseSet), e₁.coordChangeHomeomorph e₂ h₁ h₂ = e₁_1.coordChangeHomeomorph e₂_1 ⋯ ⋯
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.mul.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (q₁ q₂ : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.mul q₁ q₂ =
    q₁.liftOn₂ q₂
      (fun x x_1 =>
        match x with
        | (a, b) =>
          match x_1 with
          | (c, d) => Lean.Grind.Ring.OfSemiring.Q.mk (a * c + b * d, a * d + b * c))
      ⋯
-- Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
/-- If `a : ℂ` has norm smaller than one, then `circleAverage (log ‖· - a‖) 0 1` vanishes.
 -/
circleAverage_log_norm_sub_const₀ : ∀ {a : ℂ}, ‖a‖ < 1 → Real.circleAverage (fun x => Real.log ‖x - a‖) 0 1 = 0
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.zero_beq_xor_iff : ∀ {w : ℕ} (a b : BitVec w), (0#w == a ^^^ b) = (a == b)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s₁ s₂ : Finset β} {f : β → α},
  s₁ ⊆ s₂ → s₂.inf f ≤ s₁.inf f
-- Mathlib.Order.Interval.Multiset
Multiset.Icc_self : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a : α), Multiset.Icc a a = {a}
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.toOrderHom : {α : Type u} → [inst : Preorder α] → OmegaCompletePartialOrder.Chain α → ℕ →o α
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Whether the parameter is an autoparam (i.e., whether it uses a tactic for the default value).  -/
Lean.PrettyPrinter.Delaborator.ParamKind.isAutoParam : Lean.PrettyPrinter.Delaborator.ParamKind → Bool
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo.eToInt : Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo → Lean.Expr
-- Mathlib.Algebra.Star.Unitary
Unitary.star_eq_inv : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (U : ↥(unitary R)), star U = U⁻¹
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_le_size_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, m.size ≤ (m.insertIfNew k v).size
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.numeratorHom.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S],
  OreLocalization.numeratorHom = { toFun := fun r => r /ₒ 1, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Order.Defs.Unbundled
/-- A version of `antisymm'` with `r` explicit.

This lemma matches the lemmas from lean core in `Init.Algebra.Classes`, but is missing there.  -/
antisymm_of' : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Antisymm r] {a b : α}, r a b → r b a → b = a
-- Mathlib.Analysis.Normed.Module.Bases
/-- The norm of any projection is bounded by the basis constant.  -/
SchauderBasis.norm_proj_le_nnnormProjBound : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) [CompleteSpace X] (n : ℕ), ‖b.proj n‖ ≤ ↑b.nnnormProjBound
-- Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
/-- Being an open immersion satisfies fpqc descent.  -/
AlgebraicGeometry.descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact' : AlgebraicGeometry.IsOpenImmersion.DescendsAlong
  (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkAppS₃ : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Algebra.FreeMonoid.Count
FreeAddMonoid.countP'_add : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l₁ l₂ : FreeAddMonoid α),
  FreeAddMonoid.countP' p (l₁ + l₂) = FreeAddMonoid.countP' p l₁ + FreeAddMonoid.countP' p l₂
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_adj_compl : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ}
  [inst_2 : DecidableEq V],
  G.IsSRGWith n k ℓ μ → ∀ {v w : V}, Gᶜ.Adj v w → Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - μ) - 2
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.coverOfIsIso_f : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.ContainsIdentities] [inst_1 : P.RespectsIso]
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f] (x : PUnit.{v + 1}),
  (AlgebraicGeometry.Scheme.coverOfIsIso f).f x = f
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- The (unique) isomorphism between the chosen initial object and any other initial object.  -/
CategoryTheory.Limits.initialIsoIsInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasInitial C] → {P : C} → CategoryTheory.Limits.IsInitial P → (⊥_ C ≅ P)
-- Lean.Meta.Tactic.Grind.Extension
/-- The `kind` is used for generating the `patterns`. We save it here to implement `grind?`.  -/
Lean.Meta.Grind.EMatchTheorem.kind : Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.EMatchTheoremKind
-- Init.Data.SInt.Lemmas
Int64.ne_of_lt : ∀ {a b : Int64}, a < b → a ≠ b
-- Mathlib.Algebra.Exact.Basic
Function.MulExact.of_comp_eq_one_of_ker_in_range : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : One P],
  g ∘ f = 1 → (∀ (y : N), g y = 1 → y ∈ Set.range f) → Function.MulExact f g
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.isUpperSet_preimage_coe : ∀ {α : Type u_1} [inst : LE α] {s t : Set α},
  IsLowerSet s → (IsUpperSet (Subtype.val ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t)
-- Std.Http.Data.URI
/-- Parses a URI path from the given string. Returns the root path `"/"` if parsing fails.
 -/
Std.Http.URI.Path.parseOrRoot : String → Std.Http.URI.Path
-- Mathlib.Topology.Connected.Clopen
IsClopen.connectedComponentIn_eq : ∀ {α : Type u} [inst : TopologicalSpace α] {U : Set α},
  IsClopen U → ∀ {x : α}, x ∈ U → connectedComponentIn U x = connectedComponent x
-- Mathlib.RingTheory.Flat.Basic
IsSMulRegular.of_flat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [Module.Flat R S] {x : R}, IsSMulRegular R x → IsSMulRegular S ((algebraMap R S) x)
-- Aesop.Tree.Data
Aesop.NormalizationState.normal.injEq : ∀ (postGoal : Lean.MVarId) (postState : Lean.Meta.SavedState)
  (script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))) (postGoal_1 : Lean.MVarId)
  (postState_1 : Lean.Meta.SavedState)
  (script_1 : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))),
  (Aesop.NormalizationState.normal postGoal postState script =
      Aesop.NormalizationState.normal postGoal_1 postState_1 script_1) =
    (postGoal = postGoal_1 ∧ postState = postState_1 ∧ script = script_1)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.mkHom_asNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e f : C ≌ D} (η : e.functor ⟶ f.functor),
  CategoryTheory.Equivalence.mkHom (CategoryTheory.Equivalence.asNatTrans η) = η
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
MonoidWithZeroHom.ValueGroup₀.restrict₀.eq_1 : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : GroupWithZero B] (f : A →*₀ B),
  MonoidWithZeroHom.ValueGroup₀.restrict₀ f =
    { toFun := fun a => if h : f a = 0 then 0 else ↑⟨Units.mk0 (f a) h, ⋯⟩, map_zero' := ⋯, map_one' := ⋯,
      map_mul' := ⋯ }
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.mutuallySingular_iff_disjoint : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ.MutuallySingular ν ↔ Disjoint μ ν
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- The `atBot` filter for `↑(Iio a)` comes from the `atBot` filter in the ambient order.  -/
Filter.atBot_Iio_eq : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] (a : α), Filter.atBot = Filter.comap Subtype.val Filter.atBot
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `a` and `b`, the derivative `f'` is nonpositive on
`Ioo a b` and nonnegative on `Ioi b`. Then `f` attains its minimum on `Ici a` at `b`.  -/
isMinOn_Ici_of_deriv : ∀ {f : ℝ → ℝ} {a b : ℝ},
  ContinuousAt f a →
    ContinuousAt f b →
      DifferentiableOn ℝ f (Set.Ioo a b) →
        DifferentiableOn ℝ f (Set.Ioi b) →
          (∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioi b, 0 ≤ deriv f x) → IsMinOn f (Set.Ici a) b
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep.meas_biInter : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ι → Set Ω}
  {S : Finset ι},
  ProbabilityTheory.Kernel.iIndep m κ μ →
    (∀ i ∈ S, MeasurableSet (s i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balLeft.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α) (z : α)
  (c : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (b : RBTree.RBNode α) →
          (z : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c))
  (h_3 : (r : RBTree.RBNode α) → motive r),
  (match RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c with
    | RBTree.RBNode.node RBTree.RBColor.black a y b => h_1 a y b
    | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c => h_2 a y b z c
    | r => h_3 r) =
    h_2 a y b z c
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_eq_top_of_not_connected : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α], ¬G.Connected → G.ediam = ⊤
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.toMatrix'_comp : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  {m : Type w} [inst_4 : DecidableEq m] [inst_5 : Fintype m] (Q : QuadraticForm R (m → R)) (f : (n → R) →ₗ[R] m → R),
  QuadraticForm.toMatrix' (QuadraticMap.comp Q f) =
    (LinearMap.toMatrix' f).transpose * Q.toMatrix' * LinearMap.toMatrix' f
-- Mathlib.Algebra.GroupWithZero.TransferInstance
/-- Transfer `MulZeroOneClass` across an `Equiv`  -/
Equiv.mulZeroOneClass : {α : Type u} → {β : Type v} → α ≃ β → [MulZeroOneClass β] → MulZeroOneClass α
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.lt_iff_lt : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {a : α} {b : β}, b < l a ↔ u b < a
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.match.injEq : ∀ (ref gen discrs optMotive : Lean.Syntax) (alts : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code))
  (ref_1 gen_1 discrs_1 optMotive_1 : Lean.Syntax) (alts_1 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)),
  (Lean.Elab.Term.Do.Code.match ref gen discrs optMotive alts =
      Lean.Elab.Term.Do.Code.match ref_1 gen_1 discrs_1 optMotive_1 alts_1) =
    (ref = ref_1 ∧ gen = gen_1 ∧ discrs = discrs_1 ∧ optMotive = optMotive_1 ∧ alts = alts_1)
-- Mathlib.CategoryTheory.Limits.Cones
/-- `mapCocone` is the right inverse to `mapCoconeInv`.  -/
CategoryTheory.Functor.mapCoconeInvMapCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {F : CategoryTheory.Functor J D} →
              (H : CategoryTheory.Functor D C) →
                [inst_3 : H.IsEquivalence] → (c : CategoryTheory.Limits.Cocone F) → H.mapCoconeInv (H.mapCocone c) ≅ c
-- Mathlib.AlgebraicTopology.MooreComplex
AlgebraicTopology.NormalizedMooreComplex.objD.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.SimplicialObject C),
  AlgebraicTopology.NormalizedMooreComplex.objD X 0 =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.NormalizedMooreComplex.objX X (0 + 1)).arrow
      (CategoryTheory.CategoryStruct.comp (X.δ 0) (CategoryTheory.inv ⊤.arrow))
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.self_algebra_algebraMap : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  algebraMap (MvPolynomial S R) S = (MvPolynomial.aeval id).toRingHom
-- Mathlib.CategoryTheory.Presentable.StrongGenerator
CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.IsCardinalLocallyPresentable C κ ↔
    ∃ P,
      ∃ (_ : CategoryTheory.ObjectProperty.Small.{w, v, u} P),
        P.IsStrongGenerator ∧ P ≤ CategoryTheory.isCardinalPresentable C κ
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instDecidableLTIProp : DecidableLT Mathlib.Tactic.ITauto.IProp
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.inf' : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] [inst_1 : SemilatticeInf M] {ι : Type u_3} {f : ι → α → M}
  (s : Finset ι),
  (∀ i ∈ s, Function.HasFiniteMulSupport (f i)) →
    ∀ (hs : s.Nonempty), Function.HasFiniteMulSupport fun a => s.inf' hs fun x => f x a
-- Mathlib.Topology.MetricSpace.Isometry
PseudoMetricSpace.isometry_induced : ∀ {α : Type u} {β : Type v} (f : α → β) [m : PseudoMetricSpace β], Isometry f
-- Std.Sync.Broadcast
Std.Broadcast.Receiver.instAsyncReadOptionOfInhabited : {α : Type} → [Inhabited α] → Std.Async.IO.AsyncRead (Std.Broadcast.Receiver α) (Option α)
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- proof that the `parts` sum to `n`  -/
Nat.Partition.parts_sum : ∀ {n : ℕ} (self : n.Partition), self.parts.sum = n
-- Init.Data.List.Sublist
List.isPrefixOf_replicate : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {n : ℕ} {a : α},
  l.isPrefixOf (List.replicate n a) = (decide (l.length ≤ n) && l.all fun x => x == a)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_sub_le : ∀ {R' : Type u_2} {A : Type u_3} {B : Type u_5} [inst : Ring R'] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {f g : AddMonoidAlgebra R' A},
  AddMonoidAlgebra.supDegree D (f - g) ≤ AddMonoidAlgebra.supDegree D f ⊔ AddMonoidAlgebra.supDegree D g
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_map : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'}
  {Y : Ω' → Ω} {X : Ω → ℝ},
  AEMeasurable Y μ →
    ∀ {t : ℝ},
      MeasureTheory.AEStronglyMeasurable (fun ω => Real.exp (t * X ω)) (MeasureTheory.Measure.map Y μ) →
        ProbabilityTheory.mgf X (MeasureTheory.Measure.map Y μ) t = ProbabilityTheory.mgf (X ∘ Y) μ t
-- Mathlib.Analysis.InnerProductSpace.Basic
_private.Mathlib.Analysis.InnerProductSpace.Basic.0.«term⟪_,_⟫_3» : Lean.ParserDescr
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.ofDual.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ}
  (x : GaloisCoinsertion l u), x.ofDual = { choice := x.choice, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.inductionOn₂ : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}
  {motive : Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α β cmp → Prop} (t₁ t₂ : Std.ExtDTreeMap α β cmp),
  (∀ (a b : Std.DTreeMap α β cmp), motive (Std.ExtDTreeMap.mk a) (Std.ExtDTreeMap.mk b)) → motive t₁ t₂
-- Mathlib.LinearAlgebra.LinearPMap
/-- The tuple `(x, f x)` is contained in the graph of `f`.  -/
LinearPMap.mem_graph : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F) (x : ↥f.domain), (↑x, ↑f x) ∈ f.graph