mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.WittVector.Compare
/-- The following diagram commutes:
```text
TruncatedWittVector p n (ZMod p) ----> TruncatedWittVector p m (ZMod p)
            |                                        |
            |                                        |
            v                                        v
          ZMod (p^n) ----------------------------> ZMod (p^m)
```
Here the vertical arrows are `(TruncatedWittVector.zmodEquivTrunc p _).symm`,
the horizontal arrow at the top is `ZMod.castHom`,
and the horizontal arrow at the bottom is `TruncatedWittVector.truncate`.
 -/
TruncatedWittVector.commutes_symm : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m),
  (TruncatedWittVector.zmodEquivTrunc p n).symm.toRingHom.comp (TruncatedWittVector.truncate hm) =
    (ZMod.castHom ⋯ (ZMod (p ^ n))).comp (TruncatedWittVector.zmodEquivTrunc p m).symm.toRingHom
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : SeminormedCommRing R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S]
  [inst_3 : SizeOf R] [inst_4 : SizeOf S] (toMulRingNorm : MulRingNorm S)
  (smul' : ∀ (a : R) (x : S), toMulRingNorm.toFun (a • x) = ‖a‖ * toMulRingNorm.toFun x),
  sizeOf { toMulRingNorm := toMulRingNorm, smul' := smul' } = 1 + sizeOf toMulRingNorm
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
neg_abs_le : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] (a : α), -|a| ≤ a
-- Mathlib.Order.WithBot
WithTop.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), WithTop.map f = Option.map f
-- Mathlib.Topology.Separation.Regular
Homeomorph.t5Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T5Space X] (h : X ≃ₜ Y),
  T5Space Y
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.map_apply : ∀ {α : Type u_5} {α' : Type u_6} {ι : Type u_7} (f : α → α') (l : Combinatorics.Line α ι) (x : α),
  ↑(Combinatorics.Line.map f l) (f x) = f ∘ ↑l x
-- Lean.Meta.Tactic.SolveByElim
/-- Run either backtracking search, or repeated application, on the list of goals.  -/
_private.Lean.Meta.Tactic.SolveByElim.0.Lean.Meta.SolveByElim.solveByElim.run : List (Lean.Elab.TermElabM Lean.Expr) →
  (Lean.Meta.SolveByElim.SolveByElimConfig → Lean.Elab.TermElabM (List Lean.Expr)) →
    Lean.Meta.SolveByElim.SolveByElimConfig → List Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Logic.Relation
Relation.EqvGen.below.symm : ∀ {α : Type u_1} {r : α → α → Prop} {motive : (a a_1 : α) → Relation.EqvGen r a a_1 → Prop} (x y : α)
  (a : Relation.EqvGen r x y), Relation.EqvGen.below a → motive x y a → Relation.EqvGen.below ⋯
-- Lean.Compiler.LCNF.Types
Lean.Compiler.LCNF.mkBoxedName : Lean.Name → Lean.Name
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀)
  {Z_1 : AlgebraicGeometry.Scheme} (h : 𝒰.X i ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)) h
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoAdd'_isoZero : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {a : A}
  (e : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)),
  CategoryTheory.Functor.CommShift.isoAdd' ⋯ e (CategoryTheory.Functor.CommShift.isoZero F A) = e
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftRingHom_apply_div : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} [inst_2 : Field L] (φ : Polynomial K →+* L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p q : Polynomial K),
  (RatFunc.liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) =
    φ p / φ q
-- Mathlib.NumberTheory.LSeries.Basic
LSeriesSummable_congr : ∀ {f g : ℕ → ℂ} (s : ℂ), (∀ {n : ℕ}, n ≠ 0 → f n = g n) → (LSeriesSummable f s ↔ LSeriesSummable g s)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The definition of `cyclotomic n R` commutes with any ring homomorphism.  -/
Polynomial.map_cyclotomic : ∀ (n : ℕ) {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  Polynomial.map f (Polynomial.cyclotomic n R) = Polynomial.cyclotomic n S
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- An auxiliary morphism for the definition of the underlying morphism of the forward component of
the associator isomorphism.  -/
Bimod.AssociatorBimod.homAux : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        [inst_3 :
            ∀ (X : C),
              CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                (CategoryTheory.MonoidalCategory.tensorLeft X)] →
          [inst_4 :
              ∀ (X : C),
                CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                  (CategoryTheory.MonoidalCategory.tensorRight X)] →
            {R S T U : CategoryTheory.Mon C} →
              (P : Bimod R S) →
                (Q : Bimod S T) →
                  (L : Bimod T U) →
                    CategoryTheory.MonoidalCategoryStruct.tensorObj (P.tensorBimod Q).X L.X ⟶
                      (P.tensorBimod (Q.tensorBimod L)).X
-- Aesop.Rule
Aesop.SafeRuleInfo : Type
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
/-- `TopModuleCat.coker` is indeed the cokernel in `TopModuleCat R`.  -/
TopModuleCat.isColimitCoker : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {M N : TopModuleCat R} →
        (φ : M ⟶ N) →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (TopModuleCat.cokerπ φ) ⋯)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.ref : Lean.Elab.Command.InductiveView → Lean.Syntax
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.whiskerLeft_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b) {β β' : b ⟶ c}
  (y : β ⟶ β'), (CategoryTheory.Bicategory.whiskerLeft α y).τr = CategoryTheory.Bicategory.whiskerRight y.τr α.r
-- Mathlib.Order.RelIso.Basic
RelIso.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : r ≃r s}, f = g ↔ ∀ (x : α), f x = g x
-- Lean.Meta.WHNF
Lean.Meta.withNatValue : {α : Type} → Lean.Expr → (ℕ → Lean.MetaM (Option α)) → Lean.MetaM (Option α)
-- Init.Data.String.Basic
/-- Advances a valid position on a slice to the next valid position, or returns `none` if the
given position is the past-the-end position.  -/
String.Slice.Pos.next? : {s : String.Slice} → s.Pos → Option s.Pos
-- Init.Data.List.Sublist
List.Subset.trans : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁ ⊆ l₂ → l₂ ⊆ l₃ → l₁ ⊆ l₃
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.cast_eq_id : ∀ {α : Type u}, cast ⋯ = id
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.mapL_comp_lTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] {A : Type u_6} [inst_9 : NormedAddCommGroup A]
  [inst_10 : InnerProductSpace 𝕜 A] (f : E →L[𝕜] F) (g₁ : G →L[𝕜] H) (g₂ : A →L[𝕜] G),
  TensorProduct.mapL f g₁ ∘SL ContinuousLinearMap.lTensor E g₂ = TensorProduct.mapL f (g₁ ∘SL g₂)
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.comp_inj_left : ∀ {V : Type u} [inst : Quiver V] {a b c : V} {p₁ p₂ : Quiver.Path a b} {q : Quiver.Path b c},
  p₁.comp q = p₂.comp q ↔ p₁ = p₂
-- Mathlib.Algebra.Ring.Aut
RingAut.one_eq_refl : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R], 1 = RingEquiv.refl R
-- Mathlib.Data.Set.Card
Set.Finite.eq_of_subset_of_encard_le : ∀ {α : Type u_1} {s t : Set α}, s.Finite → s ⊆ t → t.encard ≤ s.encard → s = t
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fundamentalDomain_reindex : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] {ι' : Type u_4} (e : ι ≃ ι'),
  ZSpan.fundamentalDomain (b.reindex e) = ZSpan.fundamentalDomain b
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.forIn_filterWithPostcondition : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} [inst_1 : Monad n]
  [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o] [inst_5 : MonadLiftT n o] [LawfulMonadLiftT n o]
  [Std.Iterators.Finite α Id] [inst_8 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β}
  {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} {init : γ} {g : β → γ → o (ForInStep γ)},
  forIn (Std.Iter.filterWithPostcondition f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out).run
      if __do_lift.down = true then g out acc else pure (ForInStep.yield acc)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_tryCatch_EStateM_apply_eq : ∀ {ε σ α : Type} {post : α → σ → Prop} {epost : ε → σ → Prop} (x : EStateM ε σ α) (h : ε → EStateM ε σ α),
  Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) post epost = fun s =>
    Std.Internal.Do.wp x post (fun e s' => Std.Internal.Do.wp (h e) post epost s') s
-- Aesop.Script.GoalWithMVars
Aesop.GoalWithMVars : Type
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- `P` respects isomorphisms, if it respects the morphism property `isomorphisms C`, i.e.
it is stable under pre- and postcomposition with isomorphisms.  -/
CategoryTheory.MorphismProperty.RespectsIso : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Data.Set.Countable
Set.countable_isBot : ∀ (α : Type u_1) [inst : PartialOrder α], {x | IsBot x}.Countable
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.prod_left : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {c c' : ℝ} {f' : α → E'} {g' : α → F'}
  {k' : α → G'} {l : Filter α},
  Asymptotics.IsBigOWith c l f' k' →
    Asymptotics.IsBigOWith c' l g' k' → Asymptotics.IsBigOWith (max c c') l (fun x => (f' x, g' x)) k'
-- Mathlib.LinearAlgebra.Dimension.Constructions
finrank_range_le_card : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type u_2} [inst_4 : Fintype ι] (b : ι → M), Set.finrank R (Set.range b) ≤ Fintype.card ι
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.ofIso_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.MonObj M] (e : M ≅ X),
  CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom
-- Mathlib.Topology.Continuous
IsOpen.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ {t : Set Y}, IsOpen t → IsOpen (f ⁻¹' t)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.comp_id : ∀ {B : Type u} [inst : Quiver B] {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b}
  (η : CategoryTheory.FreeBicategory.Hom₂ f g),
  CategoryTheory.FreeBicategory.Rel (η.vcomp (CategoryTheory.FreeBicategory.Hom₂.id g)) η
-- Init.Data.Iterators.Basic
Std.PlausibleIterStep.yield.eq_1 : ∀ {α : Type u} {β : Type w} {IsPlausibleStep : Std.IterStep α β → Prop} (it' : α) (out : β)
  (h : IsPlausibleStep (Std.IterStep.yield it' out)),
  Std.PlausibleIterStep.yield it' out h = ⟨Std.IterStep.yield it' out, h⟩
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_natCast : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) (s : Set 𝕜) [inst_3 : NatCast F] (n : ℕ), HasDerivWithinAt (↑n) 0 s x
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.toOption.eq_2 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice}, String.Slice.SplitIterator.toOption✝ String.Slice.SplitIterator.atEnd = none
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.le_comap_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  (p' : Submodule R (M ⧸ p)), p ≤ Submodule.comap p.mkQ p'
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.r_lower_bound_on_verticalStrip : ∀ (z : UpperHalfPlane) {A B : ℝ} (h : 0 < B),
  z ∈ UpperHalfPlane.verticalStrip A B →
    EisensteinSeries.r { coe := { re := A, im := B }, coe_im_pos := h } ≤ EisensteinSeries.r z
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
  (Q : CategoryTheory.Limits.IsColimit t) (j : J),
  CategoryTheory.CategoryStruct.comp (t.ι.app j) (P.coconePointUniqueUpToIso Q).inv = s.ι.app j
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The unit associated to a representative of `P + Q` for two projective point representatives `P`
and `Q` on a Weierstrass curve `W` that are not `2`-torsion.

More specifically, the unit `u` such that `W.add P Q = u • ![0, 1, 0]` where `P x / P z = Q x / Q z`
but `P ≠ W.neg P`.  -/
WeierstrassCurve.Projective.addU : {F : Type u} → [Field F] → (Fin 3 → F) → (Fin 3 → F) → F
-- Init.Data.Vector.Lemmas
Vector.foldr_mk : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β → β} {b : β} {xs : Array α} (h : xs.size = n),
  Vector.foldr f b (Vector.mk xs h) = Array.foldr f b xs
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.min_bi_le : ∀ {α : Type u_1} [inst : Finite α] [inst_1 : Nonempty α] {b : α → ℝ} (i : α), b (AkraBazziRecurrence.min_bi b) ≤ b i
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepSets_of_condIndepSets_of_le_right : ∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s₁ s₂ s₃ : Set (Set Ω)},
  ProbabilityTheory.CondIndepSets m' hm' s₁ s₂ μ → s₃ ⊆ s₂ → ProbabilityTheory.CondIndepSets m' hm' s₁ s₃ μ
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_nonneg_of_nonpos_of_nonpos : ∀ {a b : ℤ}, a ≤ 0 → b ≤ 0 → 0 ≤ a.fdiv b
-- Mathlib.CategoryTheory.ConcreteCategory.Elementwise
CategoryTheory.Limits.kernel.lift_ι_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {W : C} (k : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp k f = 0) {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory C F]
  (x : carrier W),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.lift f k h)) x) =
    (CategoryTheory.ConcreteCategory.hom k) x
-- Batteries.Data.String.Basic
String.toAsciiByteArray.loop.eq_def : ∀ (s : String) (p : String.Pos.Raw) (out : ByteArray),
  String.toAsciiByteArray.loop s p out =
    if h : String.Pos.Raw.atEnd s p = true then out
    else
      have c := String.Pos.Raw.get s p;
      have this := ⋯;
      String.toAsciiByteArray.loop s (String.Pos.Raw.next s p) (out.push c.toUInt8)
-- Mathlib.Algebra.Polynomial.Degree.Domain
/-- This lemma is useful for working with the `intDegree` of a rational function.  -/
Polynomial.natDegree_sub_eq_of_prod_eq : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p₁ p₂ q₁ q₂ : Polynomial R},
  p₁ ≠ 0 → q₁ ≠ 0 → p₂ ≠ 0 → q₂ ≠ 0 → p₁ * q₂ = p₂ * q₁ → ↑p₁.natDegree - ↑q₁.natDegree = ↑p₂.natDegree - ↑q₂.natDegree
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.intercalate.match_1.eq_1 : ∀ (motive : List String → Sort u_1) (h_1 : Unit → motive [])
  (h_2 : (a : String) → (as : List String) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- Restrict a prepartition to a box.  -/
BoxIntegral.Prepartition.restrict : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} → BoxIntegral.Prepartition I → (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J
-- Mathlib.Algebra.Order.Floor.Extended
ENat.gc_toENNReal_floor : GaloisConnection ENat.toENNReal ENat.floor
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Unfold a coherence isomorphism.  -/
Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom.unfoldM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom m] →
    Mathlib.Tactic.BicategoryLike.CoherenceHom → m Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.InformationTheory.KullbackLeibler.ChainRule
InformationTheory.rnDeriv_compProd_mul_log_eq_mul_add : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  {κ η : ProbabilityTheory.Kernel 𝓧 𝓨} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η],
  (μ.compProd κ).AbsolutelyContinuous (μ.compProd η) →
    ∀ᵐ (p : 𝓧 × 𝓨) ∂ν.compProd η,
      ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal * Real.log ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal =
        ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal *
          (Real.log (μ.rnDeriv ν p.1).toReal + Real.log ((μ.compProd κ).rnDeriv (μ.compProd η) p).toReal)
-- Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (K : CochainComplex C ℤ),
  HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ↔
    ∀ (n : ℤ), HomologicalComplex.ExactAt K n
-- Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
/-- `Spec (R ⧸ I) ⟶ Spec R` is an open immersion iff `I` is generated by an idempotent.  -/
AlgebraicGeometry.isOpenImmersion_SpecMap_iff_of_surjective : ∀ {R S : CommRingCat} (f : R ⟶ S),
  Function.Surjective ⇑(CommRingCat.Hom.hom f) →
    (AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map f) ↔
      ∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e})
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- If `M` is faithfully flat, then exactness of `N₁ ⊗ M -> N₂ ⊗ M -> N₃ ⊗ M` implies that the
composition `N₁ -> N₂ -> N₃` is `0`.

Implementation detail, please use `rTensor_reflects_exact` instead.
 -/
Module.FaithfullyFlat.range_le_ker_of_exact_rTensor : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N1 : Type u_1}
  [inst_3 : AddCommGroup N1] [inst_4 : Module R N1] {N2 : Type u_2} [inst_5 : AddCommGroup N2] [inst_6 : Module R N2]
  {N3 : Type u_3} [inst_7 : AddCommGroup N3] [inst_8 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3)
  [fl : Module.FaithfullyFlat R M],
  Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23) → l12.range ≤ l23.ker
-- Mathlib.Data.Int.Cast.Lemmas
zpowersMulHom_symm_apply : ∀ {α : Type u_3} [inst : CommGroup α] (f : Multiplicative ℤ →* α), (zpowersMulHom α).symm f = f (Multiplicative.ofAdd 1)
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.edist_lt_of_edist_lt_div : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ {x y : α} {d : ENNReal}, edist x y < d / ↑K → edist (f x) (f y) < d
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle between two nonzero vectors is zero if and only if the unoriented angle
is zero.  -/
Orientation.oangle_eq_zero_iff_angle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, x ≠ 0 → y ≠ 0 → (o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.lift_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {W : C} {h : CategoryTheory.CategoryStruct.comp 0 f = 0},
  CategoryTheory.Limits.kernel.lift f 0 h = 0
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.range_id : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A], NonUnitalStarAlgHom.range (NonUnitalStarAlgHom.id R A) = ⊤
-- Mathlib.Probability.Distributions.Poisson.Basic
/-- The characteristic function of the Poisson distribution with rate `r` is
`t ↦ exp(r(exp(it) - 1))`.  -/
ProbabilityTheory.charFun_map_cast_poissonMeasure : ∀ (r : NNReal) (t : ℝ),
  MeasureTheory.charFun (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r)) t =
    Complex.exp (↑↑r * (Complex.exp (↑t * Complex.I) - 1))
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.text.injEq : ∀ {α : Type u} (a a_1 : String), (Lean.Widget.TaggedText.text a = Lean.Widget.TaggedText.text a_1) = (a = a_1)
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- If a presentation is finite, the corresponding quotient is
of finite presentation.  -/
Algebra.Presentation.instFinitePresentationQuotientOfFinite : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ) [Finite σ] [Finite ι], Algebra.FinitePresentation R P.Quotient
-- Init.Data.String.Lemmas.Pattern.Find.String
_private.Init.Data.String.Lemmas.Pattern.Find.String.0.String.Slice.contains.match_1.splitter : (s : String.Slice) →
  (motive : String.Slice.Pattern.SearchStep s → Sort u_1) →
    (x : String.Slice.Pattern.SearchStep s) →
      ((startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos)) →
        ((x : String.Slice.Pattern.SearchStep s) →
            (∀ (startPos endPos : s.Pos), x = String.Slice.Pattern.SearchStep.matched startPos endPos → False) →
              motive x) →
          motive x
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal
/-- A category has a conical terminal object
if it has a conical limit over the empty diagram.  -/
CategoryTheory.Enriched.HasConicalTerminal : (V : outParam (Type u_1)) →
  [inst : CategoryTheory.Category.{u_2, u_1} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u_3) →
        [inst_2 : CategoryTheory.Category.{u_4, u_3} C] → [CategoryTheory.EnrichedOrdinaryCategory V C] → Prop