mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.FindPos
_private.Init.Data.String.Lemmas.FindPos.0.String.Slice.Pos.prevn.eq_2 : ∀ {s : String.Slice} (p : s.Pos) (n_2 : ℕ), p.prevn n_2.succ = if h : p ≠ s.startPos then (p.prev h).prevn n_2 else p
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The composite of `(coprod.inl ▷ X) : Y ⊗ X ⟶ (Y ⨿ Z) ⊗ X` and
`(∂R X Y Z).inv :  (Y ⨿ Z) ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X)` is equal to the left coprojection
`coprod.inl : Y ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X)`.  -/
CategoryTheory.whiskerRight_coprod_inl_rightDistrib_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalRightDistrib C] {X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inl X) (∂R X Y Z).inv =
    CategoryTheory.Limits.coprod.inl
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.instOverPullbackCoverOverProp : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
                        [inst_6 : Q.HasOfPostcompProperty Q] →
                          [inst_7 : Q.IsStableUnderBaseChange] →
                            [inst_8 : Q.IsStableUnderComposition] →
                              (hX : Q (X ↘ S)) →
                                (hW : Q (W ↘ S)) →
                                  (hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) →
                                    AlgebraicGeometry.Scheme.Cover.Over S
                                      (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.instNontrivialOfNonempty : ∀ {α : Type u_2} [inst : TopologicalSpace α] [Nonempty α], Nontrivial (TopologicalSpace.Opens α)
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.toLinearMap_comm : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W),
  (↑(Representation.TensorProduct.comm ρ σ)).toLinearMap = ↑(TensorProduct.comm A V W)
-- Mathlib.Data.List.MinMax
List.le_of_mem_argmax : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] {f : α → β} {l : List α} {a m : α},
  a ∈ l → m ∈ List.argmax f l → f a ≤ f m
-- Mathlib.Data.List.Range
List.ranges.eq_2 : ∀ (a : ℕ) (l : List ℕ), (a :: l).ranges = List.range a :: List.map (List.map fun x => a + x) l.ranges
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.dummy : Lean.Meta.Sym.AlphaKey
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.Sign.instDecidableForall_batteries : {p : Float.Model.UnpackedFloat.Sign → Prop} →
  [(s : Float.Model.UnpackedFloat.Sign) → Decidable (p s)] → Decidable (∀ (s : Float.Model.UnpackedFloat.Sign), p s)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_from_quotient : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {s : Setoid α}
  {f : Quotient s → β}, Measurable f ↔ Measurable (f ∘ Quotient.mk'')
-- Lean.Server.Rpc.Basic
Lean.Lsp.instBEqRpcRef.beq : Lean.Lsp.RpcRef → Lean.Lsp.RpcRef → Bool
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compl₁₂_id_id : ∀ {R₁ : Type u_3} {R₂ : Type u_4} [inst : Semiring R₁] [inst_1 : Semiring R₂] {Mₗ : Type u_6} {N : Type u_7}
  {Pₗ : Type u_9} [inst_2 : AddCommMonoid Mₗ] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid Pₗ]
  [inst_5 : Module R₁ Mₗ] [inst_6 : Module R₂ N] [inst_7 : Module R₂ Pₗ] [inst_8 : Module R₁ Pₗ]
  [inst_9 : SMulCommClass R₂ R₁ Pₗ] (f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ), f.compl₁₂ LinearMap.id LinearMap.id = f
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.cond.match_1.splitter : (motive : Bool → Sort u_1) → (c : Bool) → (Unit → motive true) → (Unit → motive false) → motive c
-- Lean.Meta.Tactic.SolveByElim
/-- Solve a collection of goals by repeatedly applying lemmas, backtracking as necessary.

Arguments:
* `cfg : SolveByElimConfig` additional configuration options
  (options for `apply`, maximum depth, and custom flow control)
* `lemmas : List (TermElabM Expr)` lemmas to apply.
  These are thunks in `TermElabM` to avoid stuck metavariables.
* `ctx : TermElabM (List Expr)` monadic function returning the local hypotheses to use.
* `goals : List MVarId` the initial list of goals for `solveByElim`

Returns a list of suspended goals, if it succeeded on all other subgoals.
By default `cfg.suspend` is `false,` `cfg.discharge` fails, and `cfg.failAtMaxDepth` is `true`,
and so the returned list is always empty.
Custom wrappers (e.g. `apply_assumption` and `apply_rules`) may modify this behaviour.
 -/
Lean.Meta.SolveByElim.solveByElim : Lean.Meta.SolveByElim.SolveByElimConfig →
  List (Lean.Elab.TermElabM Lean.Expr) →
    (Lean.Meta.SolveByElim.SolveByElimConfig → Lean.Elab.TermElabM (List Lean.Expr)) →
      List Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_tensor_left_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).inv Y)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).inv)
            (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)))
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_eq_nil_iff : ∀ {m n : ℤ}, (m<...n).toList = [] ↔ n ≤ m + 1
-- Mathlib.Data.Fin.Tuple.Basic
_private.Mathlib.Data.Fin.Tuple.Basic.0.Fin.findX.go : {n : ℕ} →
  (p : Fin n → Prop) →
    [DecidablePred p] →
      (h : ∃ k, p k) → (m : ℕ) → (∀ (j : ℕ) (hm : j < n - m), ¬p ⟨j, ⋯⟩) → { i // p i ∧ ∀ j < i, ¬p j }
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `HasSumLocallyUniformly f g` means that the (potentially infinite) sum
`∑' i, f i b` for `b : β` converges locally uniformly to `g b` (in the sense of
`TendstoLocallyUniformly`).  -/
HasSumLocallyUniformly : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_3} → [AddCommMonoid α] → (ι → β → α) → (β → α) → [UniformSpace α] → [TopologicalSpace β] → Prop
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- Weak convergence of probability measures is equivalent to the property that the integrals of
every bounded Lipschitz function converge to the integral of the function against
the limit measure.  -/
MeasureTheory.tendsto_iff_forall_lipschitz_integral_tendsto : ∀ {γ : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : PseudoEMetricSpace Ω] [inst_1 : OpensMeasurableSpace Ω]
  {F : Filter γ} [F.IsCountablyGenerated] {μs : γ → MeasureTheory.ProbabilityMeasure Ω}
  {μ : MeasureTheory.ProbabilityMeasure Ω},
  Filter.Tendsto μs F (nhds μ) ↔
    ∀ (f : Ω → ℝ),
      (∃ C, ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
        (∃ L, LipschitzWith L f) → Filter.Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (nhds (∫ (ω : Ω), f ω ∂↑μ))
-- Mathlib.Algebra.Group.Action.Basic
AddAction.toFun.eq_1 : ∀ (M : Type u_2) (α : Type u_5) [inst : AddMonoid M] [inst_1 : AddAction M α],
  AddAction.toFun M α = { toFun := fun y x => x +ᵥ y, inj' := ⋯ }
-- Mathlib.Order.Bounded
Set.bounded_lt_inter_not_lt : ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
  Set.Bounded (fun x1 x2 => x1 < x2) (s ∩ {b | ¬b < a}) ↔ Set.Bounded (fun x1 x2 => x1 < x2) s
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnitsTopEquiv.eq_1 : ∀ {M : Type u_1} [inst : Monoid M], Subgroup.ofUnitsTopEquiv = ⊤.ofUnitsEquivType.trans Subgroup.topEquiv
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
/-- Explicit formula for `ζ (2 * k)`, for `k ∈ ℕ`, in terms of the Bernoulli number
`bernoulli (2 * k)`. Compare `riemannZeta_two_mul_nat` which avoids a cast in an exponent
but requires `k ≠ 0`.  -/
riemannZeta_two_mul_nat' : ∀ {k : ℕ},
  riemannZeta (2 * ↑k) =
    (-1) ^ (k + 1) * 2 ^ (2 * ↑k - 1) * ↑Real.pi ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k).factorial
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
LipschitzWith.compLp_zero : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {g : E → F} {c : NNReal} (hg : LipschitzWith c g)
  (g0 : g 0 = 0), hg.compLp g0 0 = 0
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.mk.injEq : ∀ {α : Type u} [inst : Preorder α] (toOrderHom toOrderHom_1 : ℕ →o α),
  ({ toOrderHom := toOrderHom } = { toOrderHom := toOrderHom_1 }) = (toOrderHom = toOrderHom_1)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.coconeOfPredicateSet_pt : ∀ {α : PartOrdEmb} (P : Set ↑α → Prop), (PartOrdEmb.coconeOfPredicateSet P).pt = α
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.instLaxBraidedForallPi' : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [inst_2 : (i : I) → CategoryTheory.BraidedCategory (C i)] →
          {D : Type u_1} →
            [inst_3 : CategoryTheory.Category.{v_1, u_1} D] →
              [inst_4 : CategoryTheory.MonoidalCategory D] →
                [inst_5 : CategoryTheory.BraidedCategory D] →
                  (F : (i : I) → CategoryTheory.Functor D (C i)) →
                    [(i : I) → (F i).LaxBraided] → (CategoryTheory.Functor.pi' F).LaxBraided
-- Mathlib.Topology.Homotopy.TopCat.Path
TopCat.Path.ext : ∀ {X : TopCat} {x y : ↑X} {x_1 y_1 : X.Path x y}, x_1.hom = y_1.hom → x_1 = y_1
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.map_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ.[σ] F), ↑f 0 = 0
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_inter' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜},
  t ∈ nhdsWithin x s → (HasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x)
-- Std.Time.DateTime
/-- The timezone associated with this datetime.
 -/
Std.Time.DateTime.timezone : Std.Time.DateTime → Std.Time.TimeZone
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.instName : Lean.Elab.ConfigEval.EvalExpr Lean.Name
-- Mathlib.CategoryTheory.ObjectProperty.SiteLocal
CategoryTheory.ObjectProperty.IsLocal.top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}, ⊤.IsLocal K
-- Std.Time.Format.Modifier
Std.Time.Modifier.D.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.D presentation = Std.Time.Modifier.D presentation_1) = (presentation = presentation_1)
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The counit morphism of a comonoid object.  -/
CategoryTheory.ComonObj.termε : Lean.ParserDescr
-- Init.Data.SInt.Basic
Int32.instNeg : Neg Int32
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.mem_map : ∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] [inst_6 : AddCommMonoid F]
  [inst_7 : TopologicalSpace F] [inst_8 : Module R F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul R F]
  {f : E →L[R] F} {C : ProperCone R E} {y : F}, y ∈ ProperCone.map f C ↔ y ∈ (PointedCone.map ↑f ↑C).closure
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_self`.  -/
hammingDist_self : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] (x : (i : ι) → β i),
  hammingDist x x = 0
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.fst_comp_toProd : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  (MonoidHom.fst M N).comp Monoid.Coprod.toProd = Monoid.Coprod.fst
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.nonempty_support_iff : ∀ {X : Type u_1} {a : FreeAbelianGroup X}, a.support.Nonempty ↔ a ≠ 0
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.instDecidableEqDeclMod : DecidableEq Lean.Meta.LibrarySearch.DeclMod
-- Lean.CompactedRegion
/-- Size in bytes of the region's mapping (the backing `.olean` file).  -/
Lean.CompactedRegion.size : Lean.CompactedRegion → USize
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.toBilin'Aux_toMatrixAux : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (B₂ : LinearMap.BilinForm R₁ (n → R₁)), ((LinearMap.BilinForm.toMatrixAux fun j => Pi.single j 1) B₂).toBilin'Aux = B₂
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.instIsLeftAdjointExtendScalars : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  (ModuleCat.extendScalars f).IsLeftAdjoint
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.spanning_iff_eRk_le : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite],
  autoParam (X ⊆ M.E) Matroid.spanning_iff_eRk_le._auto_1 → (M.Spanning X ↔ M.eRank ≤ M.eRk X)
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.toList : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → List α
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_empty : Cardinal.mk Empty = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_of_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.getValueCastD k (Std.Internal.List.insertList l toInsert) fallback =
        Std.Internal.List.getValueCastD k toInsert (Std.Internal.List.getValueCastD k l fallback)
-- Mathlib.Control.EquivFunctor
EquivFunctor.mapEquiv_refl : ∀ (f : Type u₀ → Type u₁) [inst : EquivFunctor f] (α : Type u₀),
  EquivFunctor.mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
-- Init.Data.List.MinMaxIdx
List.lt_length_of_minIdxOn?_eq_some : ∀ {β : Type u_1} {α : Type u_2} {i : ℕ} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α},
  List.minIdxOn? f xs = some i → i < xs.length
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coe_degree : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : ↑G'.verts) [inst : Fintype ↑(G'.coe.neighborSet v)]
  [inst_1 : Fintype ↑(G'.neighborSet ↑v)], G'.coe.degree v = G'.degree ↑v
-- Mathlib.Analysis.Distribution.DerivNotation
/-- The iterated line derivative as a continuous linear map.  -/
LineDeriv.iteratedLineDerivOpCLM : (R : Type u_4) →
  {V : Type u_5} →
    (E : Type u_6) →
      [inst : LineDeriv V E E] →
        [inst_1 : TopologicalSpace E] →
          [inst_2 : Ring R] →
            [inst_3 : AddCommGroup V] →
              [inst_4 : AddCommGroup E] →
                [inst_5 : Module R E] →
                  [LineDerivAdd V E E] →
                    [LineDerivSMul R V E E] → [ContinuousLineDeriv V E E] → {n : ℕ} → (Fin n → V) → E →L[R] E
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) {Z : CommRingCat}
  (h : X.residueField x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.Γevaluation ((CategoryTheory.ConcreteCategory.hom f.base) x))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x) h) =
    CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op ⊤))
      (CategoryTheory.CategoryStruct.comp (X.Γevaluation x) h)
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.comapEvalIsoEval_hom_app : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I)
  (j : J) (X : (i : I) → C i),
  (CategoryTheory.Pi.comapEvalIsoEval C h j).hom.app X = CategoryTheory.CategoryStruct.id (X (h j))
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- If the sequence has not terminated before position `n + 1`, the value at `n + 1` gets
squashed into position `n`.  -/
GenContFract.squashSeq_nth_of_not_terminated : ∀ {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GenContFract.Pair K)} [inst : DivisionRing K]
  {gp_n gp_succ_n : GenContFract.Pair K},
  s.get? n = some gp_n →
    s.get? (n + 1) = some gp_succ_n →
      (GenContFract.squashSeq s n).get? n = some { a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b }
-- Init.Data.Vector.Lemmas
Vector.pop_append : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m},
  (xs ++ ys).pop = if h : m = 0 then Vector.cast ⋯ xs.pop else Vector.cast ⋯ (xs ++ ys.pop)
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instOrd : Ord Std.Time.Weekday
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_eq_of_eq_mul_det_one : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {A B : Matrix n n R}
  (C : Matrix n n R), C.det = 1 → A = B * C → A.det = B.det
-- Init.Prelude
/-- `Except ε α` is a type which represents either an error of type `ε` or a successful result with a
value of type `α`.

`Except ε : Type u → Type v` is a `Monad` that represents computations that may throw exceptions:
the `pure` operation is `Except.ok` and the `bind` operation returns the first encountered
`Except.error`.
 -/
Except : Type u → Type v → Type (max u v)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- Substitution `y = log x` in integrals over `Ioi a`  -/
MeasureTheory.integral_comp_log_Ioi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : ℝ → E) {a : ℝ},
  0 < a → ∫ (x : ℝ) in Set.Ioi a, x⁻¹ • g (Real.log x) = ∫ (y : ℝ) in Set.Ioi (Real.log a), g y
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH2_comp : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C),
  groupHomology.mapShortComplexH2 (g.comp f) (CategoryTheory.CategoryStruct.comp φ ((Rep.resFunctor f).map ψ)) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapShortComplexH2 f φ) (groupHomology.mapShortComplexH2 g ψ)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k' (Std.Internal.List.alterKey k f l) =
      if (k == k') = true then if (f (Std.Internal.List.getValueCast? k l)).isSome = true then some k else none
      else Std.Internal.List.getKey? k' l
-- Lean.Parser.Term
Lean.Parser.Term.matchExprAlt.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.atIdx?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {i : ℕ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.atIdx? i = t₂.atIdx? i
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitDiagInfo.mk.inj : ∀ {lctx : Lean.LocalContext} {c : Lean.Expr} {gen numCases : ℕ} {splitSource : Lean.Meta.Grind.SplitSource}
  {lctx_1 : Lean.LocalContext} {c_1 : Lean.Expr} {gen_1 numCases_1 : ℕ} {splitSource_1 : Lean.Meta.Grind.SplitSource},
  { lctx := lctx, c := c, gen := gen, numCases := numCases, splitSource := splitSource } =
      { lctx := lctx_1, c := c_1, gen := gen_1, numCases := numCases_1, splitSource := splitSource_1 } →
    lctx = lctx_1 ∧ c = c_1 ∧ gen = gen_1 ∧ numCases = numCases_1 ∧ splitSource = splitSource_1
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- Given a prime ideal `P`, `Localization.AtPrime P` is a localization of
`R` at the complement of `P`, as a quotient type.  -/
Localization.AtPrime : {R : Type u_1} → [inst : CommSemiring R] → (P : Ideal R) → [hp : P.IsPrime] → Type u_1
-- Mathlib.RingTheory.Finiteness.Descent
RingHom.FinitePresentation.codescendsAlong_faithfullyFlat : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => RingHom.FinitePresentation)
  fun {R S} [CommRing R] [CommRing S] => RingHom.FaithfullyFlat
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indep_self : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μα : MeasureTheory.Measure α} [h : ∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)],
  ProbabilityTheory.Kernel.Indep m m κ μα → ∀ {t : Set Ω}, MeasurableSet t → ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a finite set `s` and an element `a ∉ s`, the product of `f i` over `i ∈ insert a s` equals
`f a` times the product of `f i` over `i ∈ s`.  -/
finprod_mem_insert : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {a : α} {s : Set α} (f : α → M),
  a ∉ s → s.Finite → ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.all_eq_allM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool},
  Std.Iter.all p it = (Std.Iter.allM (fun x => pure (p x)) it).run
-- Mathlib.Data.Vector.Mem
List.Vector.notMem_zero : ∀ {α : Type u_1} (a : α) (v : List.Vector α 0), a ∉ v.toList
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKey?_alter_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.maxKey? = some k ↔
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.gc_map_comap : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (f : BoundedLatticeHom α β),
  GaloisConnection (BooleanSubalgebra.map f) (BooleanSubalgebra.comap f)
-- Init.GrindInstances.ToInt
Lean.Grind.instLEBitVecUint : ∀ {v : ℕ}, Lean.Grind.ToInt.LE (BitVec v) (Lean.Grind.IntInterval.uint v)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, Std.ExtDHashMap.Const.get (m.insert k v) k ⋯ = v
-- Mathlib.Order.Directed
/-- A subset of `α` is directed if there is an element of the set `≼`-above any
pair of elements in the set.  -/
DirectedOn : {α : Type u_1} → (α → α → Prop) → Set α → Prop