mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- Given two functors which have equivalent categories of cones, we can transport evidence of
a weak limit cone across the equivalence.
 -/
CategoryTheory.Limits.IsWeakLimit.iff_of_cone_equiv : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {K : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J C} {D : Type u_5} [inst_3 : CategoryTheory.Category.{v_5, u_5} D]
  {G : CategoryTheory.Functor K D} (h : CategoryTheory.Limits.Cone G ≌ CategoryTheory.Limits.Cone F)
  {c : CategoryTheory.Limits.Cone G},
  Nonempty (CategoryTheory.Limits.IsWeakLimit (h.functor.obj c)) ↔ Nonempty (CategoryTheory.Limits.IsWeakLimit c)
-- Lean.Parser.Do
Lean.Parser.Term.doLetRec.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.UniformSpace.Cauchy
Function.Bijective.cauchySeq_comp_iff : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : ℕ → ℕ},
  Function.Bijective f → ∀ (u : ℕ → α), CauchySeq (u ∘ f) ↔ CauchySeq u
-- Mathlib.Data.Finset.NAry
Finset.card_le_card_image₂_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} (s : Finset α) {b : β}
  {t : Finset β}, b ∈ t → (Function.Injective fun x => f x b) → s.card ≤ (Finset.image₂ f s t).card
-- Mathlib.CategoryTheory.Subfunctor.Image
/-- The image of a subfunctor by a morphism of type-valued functors.  -/
CategoryTheory.Subfunctor.image : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F F' : CategoryTheory.Functor C (Type w)} → CategoryTheory.Subfunctor F → (F ⟶ F') → CategoryTheory.Subfunctor F'
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.imageIsoImage_hom_comp_image_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.imageIsoImage f).hom (CategoryTheory.Limits.image.ι f) =
    CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.π f)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_mapIso_hom_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) {Z : C} (h : ∐ g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.mapIso p).hom h) =
    CategoryTheory.CategoryStruct.comp (p b).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι g b) h)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.toString.match_1.eq_1 : ∀ (motive : Substring.Raw → Sort u_1) (s : String) (b e : String.Pos.Raw)
  (h_1 : (s : String) → (b e : String.Pos.Raw) → motive { str := s, startPos := b, stopPos := e }),
  (match { str := s, startPos := b, stopPos := e } with
    | { str := s, startPos := b, stopPos := e } => h_1 s b e) =
    h_1 s b e
-- Mathlib.Order.Filter.CardinalInter
Filter.cardinalInterFilter_principal : ∀ {α : Type u} {c : Cardinal.{u}} (s : Set α), CardinalInterFilter (Filter.principal s) c
-- Mathlib.Topology.Separation.Basic
Function.update_eventuallyEq_nhdsNE : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [T1Space α] [inst_2 : DecidableEq α] (f : α → β) (a a' : α)
  (b : β), Function.update f a b =ᶠ[nhdsWithin a' {a'}ᶜ] f
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inr_f : ∀ {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] (i : ι),
  (HomologicalComplex.homotopyCofiber.inr φ).f i = HomologicalComplex.homotopyCofiber.inrX φ i
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.multiplicativeAdditive_symm_apply : ∀ (H : Type u_3) [inst : MulOneClass H] (a : H),
  (MulEquiv.multiplicativeAdditive H).symm a = Multiplicative.ofAdd (Additive.ofMul a)
-- Mathlib.Algebra.Jordan.Basic
IsJordan.lmul_comm_rmul_rmul : ∀ {A : Type u_1} {inst : Mul A} [self : IsJordan A] (a b : A), a * b * (a * a) = a * (b * (a * a))
-- Mathlib.LinearAlgebra.BilinearForm.Basic
/-- The `flip` of a bilinear form over a commutative ring, obtained by exchanging the left and
right arguments.  -/
LinearMap.BilinForm.flip : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R M → LinearMap.BilinForm R M
-- Init.Data.Int.DivMod.Lemmas
Int.neg_self_le_ediv_of_nonneg_of_nonpos : ∀ (x y : ℤ), 0 ≤ x → y ≤ 0 → -x ≤ x / y
-- Mathlib.Data.Sum.Basic
Sum.update_inr_comp_inr : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq β] [inst_1 : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : β}
  {x : γ}, Function.update f (Sum.inr i) x ∘ Sum.inr = Function.update (f ∘ Sum.inr) i x
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- An `n`-independent set is an `n`-clique in the complement graph and vice versa.  -/
SimpleGraph.isNClique_compl : ∀ {α : Type u_1} (G : SimpleGraph α) {n : ℕ} {s : Finset α}, Gᶜ.IsNClique n s ↔ G.IsNIndepSet n s
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
/-- The tail of a well-formed basis is well-formed.  -/
Tactic.ComputeAsymptotics.WellFormedBasis.tail : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis (basis_hd :: basis_tl) → Tactic.ComputeAsymptotics.WellFormedBasis basis_tl
-- Lean.Meta.HasAssignableMVar
_private.Lean.Meta.HasAssignableMVar.0.Lean.Meta.hasAssignableMVar.visit : Lean.Expr → StateRefT' IO.RealWorld Lean.ExprSet Lean.MetaM Bool
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.alter_eq_alter! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] {t : Std.DTreeMap.Internal.Impl α β} {a : α}
  {f : Option (β a) → Option (β a)} (htb : t.Balanced),
  (Std.DTreeMap.Internal.Impl.alter a f t htb).impl = Std.DTreeMap.Internal.Impl.alter! a f t
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
/-- The preadditive coyoneda functor for the category `AddCommGrpCat` agrees with
`AddCommGrpCat.coyoneda`.  -/
AddCommGrpCat.preadditiveCoyonedaIso : CategoryTheory.preadditiveCoyoneda ≅ AddCommGrpCat.coyoneda
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan_coe : ∀ (x : ℝ), (↑x).tan = Real.tan x
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- A functor is *coreflective*, or *a coreflective inclusion*, if it is fully faithful and left
adjoint.
 -/
CategoryTheory.Coreflective : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Type (max (max (max u₁ u₂) v₁) v₂)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.fold.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (r : RBTree.RBNode α) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (match RBTree.RBNode.node c l v r with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c l v r => h_2 c l v r) =
    h_2 c l v r
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.nnnorm_le_of_ae_bound : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] {f : ↥(MeasureTheory.Lp E p μ)} {C : NNReal},
  (∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ C) → ‖f‖₊ ≤ MeasureTheory.measureUnivNNReal μ ^ p.toReal⁻¹ * C
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Pos.Raw.isValidForSlice_prevAuxGo.elim : ∀ {P : String.Pos.Raw → Prop} {h : False}, P h.elim
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.card_complex_embeddings : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Fintype.card { φ // ¬NumberField.ComplexEmbedding.IsReal φ } = 2 * NumberField.InfinitePlace.nrComplexPlaces K
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.below.comp : ∀ {motive : {n : ℕ} → (a : List.Vector ℕ n → ℕ) → Nat.Primrec' a → Prop} {m n : ℕ} {f : List.Vector ℕ n → ℕ}
  (g : Fin n → List.Vector ℕ m → ℕ) (a : Nat.Primrec' f) (a_1 : ∀ (i : Fin n), Nat.Primrec' (g i)),
  Nat.Primrec'.below a →
    motive f a → (∀ (i : Fin n), Nat.Primrec'.below ⋯) → (∀ (i : Fin n), motive (g i) ⋯) → Nat.Primrec'.below ⋯
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coeff_subst_X_zero_add_X_one : ∀ {R : Type u_2} [inst : CommRing R] (f : PowerSeries R) (e : Fin 2 →₀ ℕ),
  (MvPowerSeries.coeff e) (PowerSeries.subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    ↑((e 0 + e 1).choose (e 0)) * (PowerSeries.coeff (e 0 + e 1)) f
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (P : Ideal ↥A) [inst_1 : P.IsPrime] (x : ↥A),
  (A.ofPrime P).valuation ↑x = 1 ↔ x ∈ P.primeCompl
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [inst : Preorder ι] {s : ι → Set Ω},
  (∀ (n : ι), MeasurableSet (s n)) →
    ProbabilityTheory.Kernel.iIndepSet s κ μ →
      ∀ (i : ι) {k : ι},
        i < k →
          ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom {s k})
            (MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}) κ μ
-- Mathlib.Topology.Bornology.Basic
/-- **Alias** of the forward direction of `Filter.disjoint_cobounded_iff`. -/
Disjoint.exists_isBounded : ∀ {α : Type u_2} [inst : Bornology α] {l : Filter α},
  Disjoint l (Bornology.cobounded α) → ∃ s ∈ l, Bornology.IsBounded s
-- Mathlib.Analysis.Convex.Cone.InnerDual
ProperCone.map.congr_simp : ∀ {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 f_1 : E →L[R] F), f = f_1 → ∀ (C C_1 : ProperCone R E), C = C_1 → ProperCone.map f C = ProperCone.map f_1 C_1
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ord_lt_top : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [Ring.KrullDimLE 1 R] {a : R},
  a ∈ nonZeroDivisors R → Ring.ord R a < ⊤
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.instToString : ToString Lean.Meta.RecursorInfo
-- Mathlib.Algebra.Group.End
MulAut.congr.eq_1 : ∀ {G : Type u_3} [inst : Group G] {H : Type u_7} [inst_1 : Group H] (ϕ : G ≃* H),
  MulAut.congr ϕ =
    { toFun := fun f => ϕ.symm.trans (MulEquiv.trans f ϕ), invFun := fun f => ϕ.trans (MulEquiv.trans f ϕ.symm),
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Group.Equiv.Opposite
MulEquiv.inv'.eq_1 : ∀ (G : Type u_3) [inst : DivisionMonoid G],
  MulEquiv.inv' G = { toEquiv := Equiv.trans (Equiv.inv G) MulOpposite.opEquiv, map_mul' := ⋯ }
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.preimage_image : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α),
  ⇑e ⁻¹' ⇑e '' s = s
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aevalEquiv_apply : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
  (Polynomial.aevalEquiv R A) x = Polynomial.aeval x
-- Mathlib.Order.Hom.CompleteLattice
/-- Reinterpret a `CompleteLatticeHom` as a `BoundedLatticeHom`.  -/
CompleteLatticeHom.toBoundedLatticeHom : {α : Type u_2} →
  {β : Type u_3} →
    [inst : CompleteLattice α] → [inst_1 : CompleteLattice β] → CompleteLatticeHom α β → BoundedLatticeHom α β
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages do not change when replacing the radius by its negative.  -/
Real.circleAverage_neg_radius : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ},
  Real.circleAverage f c (-R) = Real.circleAverage f c R
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.liftCLM.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] {G : Type u_5} [inst_8 : AddCommGroup G]
  [inst_9 : Module 𝕜 G] [inst_10 : TopologicalSpace G] [inst_11 : ContinuousConstSMul 𝕜 F]
  (f f_1 : G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x => E) F) (e_f : f = f_1)
  (hf : ∀ (x : G) (v : ι → E) (i j : ι), v i = v j → i ≠ j → (f x) v = 0),
  ContinuousAlternatingMap.liftCLM f hf = ContinuousAlternatingMap.liftCLM f_1 ⋯
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_eq_iff : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b c : α}, toIocMod hp a b = c ↔ c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p
-- Mathlib.Tactic.Abel
/-- Interpret an expression as an atom for `abel`'s normal form.  -/
Mathlib.Tactic.Abel.evalAtom : Lean.Expr → Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The first homotopy group at `x` is in bijection with the fundamental group.  -/
HomotopyGroup.pi1EquivFundamentalGroup : {X : Type u_2} → [inst : TopologicalSpace X] → {x : X} → HomotopyGroup.Pi 1 X x ≃ FundamentalGroup X x
-- Mathlib.Topology.Separation.Regular
nhdsKer.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X), nhdsKer s = (nhdsSet s).ker
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.bind : {ι α β : Type} → Std.Internal.Parsec ι α → (α → Std.Internal.Parsec ι β) → Std.Internal.Parsec ι β
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_nat_mul_pi_sub : ∀ (x : ℂ) (n : ℕ), Complex.tan (↑n * ↑Real.pi - x) = -Complex.tan x
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [inst_2 : P.HasPullbacksAlong f] {g : X ⟶ Y}
  [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : Q.IsStableUnderBaseChange] (h : f = g) (A : P.Over Q Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Over.pullbackCongr h).hom.app A).left
      (CategoryTheory.Limits.pullback.fst A.hom g) =
    CategoryTheory.Limits.pullback.fst A.hom f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_modify : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ [inst_3 : Inhabited α] {k k' : α} {f : β k → β k},
      (m.modify k f).getKey! k' = if (k == k') = true then if m.contains k = true then k else default else m.getKey! k'
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
/-- `limsup (xᵢ - c) = (limsup xᵢ) - c`.  -/
limsup_sub_const : ∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] (F : Filter ι) [inst_3 : AddCommSemigroup R] [inst_4 : Sub R] [ContinuousSub R] [OrderedSub R]
  (f : ι → R) (c : R),
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f →
    Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f → Filter.limsup (fun i => f i - c) F = Filter.limsup f F - c
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.mem_verts_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v), w ∈ p.toSubgraph.verts ↔ w ∈ p.support
-- Mathlib.Data.FunLike.Group
FunLike.addCancelMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : SMul ℕ F] [inst_4 : AddCancelMonoid β] [inst_5 : IsZeroApply F α β] [inst_6 : IsAddApply F α β]
  [inst_7 : IsSMulApply ℕ F α β], FunLike.addCancelMonoid = Function.Injective.addCancelMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯
-- Init.Data.Nat.ToString
Nat.seven_eq_digitChar : ∀ {n : ℕ}, '7' = n.digitChar ↔ n = 7
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isStrictlyGE_shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyGE n] (a n' : ℤ),
  a + n' = n → ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsStrictlyGE n'
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- Asymptotically, the characteristic function of a sum `∑ a, f a` at `⊤` is less than or equal to the
sum of the characteristic functions of `f ·`.
 -/
ValueDistribution.characteristic_sum_top_eventuallyLE : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {α : Type u_2} (s : Finset α) (f : α → ℂ → E),
  (∀ a ∈ s, Meromorphic (f a)) →
    ValueDistribution.characteristic (∑ a ∈ s, f a) ⊤ ≤ᶠ[Filter.atTop]
      ∑ a ∈ s, ValueDistribution.characteristic (f a) ⊤ + fun x => Real.log ↑s.card
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.topEquiv.eq_1 : ∀ {G : Type u_1} [inst : Group G], Subgroup.topEquiv = Submonoid.topEquiv
-- Aesop.Tree.Data
Aesop.GoalUnsafe.brecOn.eq : ∀ {motive_1 : Aesop.GoalUnsafe → Sort u} {motive_2 : Aesop.MVarClusterUnsafe → Sort u}
  {motive_3 : Aesop.RappUnsafe → Sort u} {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u}
  {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u}
  {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u}
  {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} (t : Aesop.GoalUnsafe)
  (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t) (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t)
  (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_1 t (Aesop.GoalUnsafe.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Init.Data.Option.Lemmas
Option.lt.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (x : Option α) (x_1 : Option β),
  (∀ (val : β), x = none → x_1 = some val → False) →
    (∀ (x_2 : α) (y : β), x = some x_2 → x_1 = some y → False) → Option.lt r x x_1 = False
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- An auxiliary definition for `descHomotopyZero`.  -/
CategoryTheory.InjectiveResolution.descHomotopyZeroOne : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        {I : CategoryTheory.InjectiveResolution Y} →
          {J : CategoryTheory.InjectiveResolution Z} →
            (f : I.cocomplex ⟶ J.cocomplex) →
              CategoryTheory.CategoryStruct.comp I.ι f = 0 → (I.cocomplex.X 2 ⟶ J.cocomplex.X 1)
-- Mathlib.Analysis.Matrix.Normed
Matrix.norm_lt_iff : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] {r : ℝ}, 0 < r → ∀ {A : Matrix m n α}, ‖A‖ < r ↔ ∀ (i : m) (j : n), ‖A i j‖ < r
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft'_assoc : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {x y : D} (f : x ⟶ y)
  [inst_4 : CategoryTheory.IsIso f] (z : C) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (CategoryTheory.inv f) z) h) =
    h
-- Mathlib.FieldTheory.Fixed
FixedPoints.rank_le_card : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [inst_3 : Fintype G],
  Module.rank (↥(FixedPoints.subfield G F)) F ≤ ↑(Fintype.card G)
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.flattenListFast.eq_1 : ∀ {n : ℕ} (xs : List (BitVec n)),
  BitVec.flattenListFast xs = BitVec.ofNat (n * xs.length) (BitVec.flattenList.toNatAux xs)
-- Init.Data.List.SplitOn.Basic
/-- Split a list at every element satisfying a predicate. The separators are not in the result.

Examples:

* `[1, 1, 2, 3, 2, 4, 4].splitOnP (· == 2) = [[1, 1], [3], [4, 4]]`
 -/
List.splitOnP : {α : Type u_1} → (α → Bool) → List α → List (List α)
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.get?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α] (a : α) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.get? ⟨{ size := size, buckets := buckets }, hm⟩ a =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ => Std.DHashMap.Internal.AssocList.getCast? a buckets[i]
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The open `n`-cell given by the index `i`. Use this instead of `map n i '' ball 0 1` whenever
possible.  -/
Topology.RelCWComplex.openCell : {X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} → [inst : Topology.RelCWComplex C D] → (n : ℕ) → Topology.RelCWComplex.cell C n → Set X
-- Mathlib.Order.Shrink
instTopShrink.eq_1 : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Top α], instTopShrink = { top := (equivShrink α) ⊤ }
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_Ioc_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (b : α i), Pi.single i '' Set.Ioc 0 b = Set.Ioc 0 (Pi.single i b)
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_unit_prod : ∀ {α : Type u_1} {f : α → ℚ → ℝ} (a : α),
  ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux (fun p => f p.2) ((), a) =
    ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a