mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Interval.Basic
Interval.mulOneClass.eq_1 : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  Interval.mulOneClass = { toOne := instOneInterval, toMul := instMulInterval, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.Topology.Algebra.Group.Quotient
/-- The quotient of a topological additive group `G` by a closed subgroup `N` is T1.

When `G` is normal, this implies (because `G ⧸ N` is a topological additive group) that the
quotient is T3 (see `QuotientAddGroup.instT3Space`).

Back to the general case, we will show later that the quotient is in fact T2
since `N` acts on `G` properly.  -/
QuotientAddGroup.instT1Space : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G}
  [hN : IsClosed ↑N], T1Space (G ⧸ N)
-- Mathlib.Analysis.Convex.PathConnected
Path.segment_injective_of_ne : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : ContinuousAdd E]
  [inst_4 : ContinuousSMul ℝ E] {a b : E}, a ≠ b → Function.Injective ⇑(Path.segment a b)
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Measure.setIntegral_condKernel_univ_left : ∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ] {E : Type u_3}
  {f : β × Ω → E} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace ℝ E] {t : Set Ω},
  MeasurableSet t →
    MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ρ →
      ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxoIterator.takeWhile_toList : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] [Std.TransOrd α] {z : Std.DTreeMap.Internal.Zipper α β} {bound : α}
  {z_ord : z.Ordered},
  List.takeWhile (fun e => (compare e.fst bound).isLT) z.toList =
    List.filter (fun e => (compare e.fst bound).isLT) z.toList
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inl.eq_1 : ∀ (x y : AugmentedSimplexCategory),
  x.inl y =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft x (CategoryTheory.WithInitial.starInitial.to y))
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.orderHomMap_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : PartialOrder X] [inst_1 : PartialOrder Y] (f : X →o Y)
  (s : PartialOrder.NonemptyFiniteChains X), (PartialOrder.NonemptyFiniteChains.orderHomMap f) s = s.map f
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.of_restrictScalars : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] [Algebra.QuasiFinite R T],
  Algebra.QuasiFinite S T
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
/-- A subgroup `H` of `G` determines a subgroup `H.op` of the opposite group `Gᵐᵒᵖ`.  -/
Subgroup.opEquiv : {G : Type u_2} → [inst : Group G] → Subgroup G ≃o Subgroup Gᵐᵒᵖ
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.ins.match_1.eq_4 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (parent : RBTree.RBNode.Path α) (y : α)
  (b a : RBTree.RBNode α) (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b) a)
  (h_3 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent) b)
  (h_4 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b) a)
  (h_5 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent) b),
  (match RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a => h_2 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b => h_3 a y parent b
    | RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a => h_4 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b => h_5 a y parent b) =
    h_4 parent y b a
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- A version of `Dist` that takes value in `ℝ≥0`.  -/
NNDist : Type u_3 → Type u_3
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Convert a measurable involutive function `f` to a measurable permutation with
`toFun = invFun = f`. See also `Function.Involutive.toPerm`.  -/
MeasurableEquiv.ofInvolutive : {α : Type u_1} → [inst : MeasurableSpace α] → (f : α → α) → Function.Involutive f → Measurable f → α ≃ᵐ α
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.sum_eq : ∀ {n d : ℕ}, ∑ i, d * (2 * d + 1) ^ ↑i = ((2 * d + 1) ^ n - 1) / 2
-- Mathlib.Order.Lattice
AntitoneOn.map_inf : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x y : α} [inst : LinearOrder α] [inst_1 : SemilatticeSup β],
  AntitoneOn f s → x ∈ s → y ∈ s → f (min x y) = f x ⊔ f y
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.IsComplete.models_not_iff : ∀ {L : FirstOrder.Language} {T : L.Theory},
  T.IsComplete → ∀ (φ : L.Sentence), T ⊨ᵇ FirstOrder.Language.Formula.not φ ↔ ¬T ⊨ᵇ φ
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.signals : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_smul : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P) (r : ℝ),
  ((signedDist (r • v)) p) q = ↑(SignType.sign r) * ((signedDist v) p) q
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The obvious map `PushoutCocone f g → PullbackCone f.unop g.unop`  -/
CategoryTheory.Limits.PushoutCocone.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : Cᵒᵖ} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} → CategoryTheory.Limits.PushoutCocone f g → CategoryTheory.Limits.PullbackCone f.unop g.unop
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.generateFrom_mono : ∀ {X : Type u_1} {g₁ g₂ : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))},
  g₁ ⊆ g₂ → DiffeologicalSpace.generateFrom g₁ ≤ DiffeologicalSpace.generateFrom g₂
-- Lean.Data.Options
Lean.OptionDeprecation.mk.injEq : ∀ (since : String) (text? : Option String) (since_1 : String) (text?_1 : Option String),
  ({ since := since, text? := text? } = { since := since_1, text? := text?_1 }) = (since = since_1 ∧ text? = text?_1)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLE.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β)
  (l r : Std.DTreeMap.Internal.Impl α fun x => β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.Const.getEntryLE k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    match hkky : compare k ky with
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getEntryLED k r (ky, y)
    | Ordering.eq => (ky, y)
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getEntryLE k l ⋯ ⋯
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.one_def : ∀ {α : Type u_2} {x : NonAssocSemiring α}, 1 = RingHom.id α
-- Lean.Meta.CoeAttr
Lean.Meta.CoeFnType.coeFun.sizeOf_spec : sizeOf Lean.Meta.CoeFnType.coeFun = 1
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.Small.of_surjective : ∀ (α : Type v) {β : Type w} (f : α → β) [Std.Internal.Small α], (∀ (b : β), ∃ a, f a = b) → Std.Internal.Small β
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        Std.DHashMap.Internal.Raw₀.Const.get! (m₁.inter m₂) k =
          if m₂.contains k = true then Std.DHashMap.Internal.Raw₀.Const.get! m₁ k else default
-- Mathlib.Data.Set.Lattice
sSup_iUnion : ∀ {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice β] (t : ι → Set β), sSup (⋃ i, t i) = ⨆ i, sSup (t i)
-- Mathlib.Topology.Sheaves.Presheaf
/-- attribute `sheaf_restrict` to mark lemmas related to restricting sheaves  -/
TopCat.Presheaf.attrSheaf_restrict : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.Basic
mem_closedBall_iff_norm : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ}, b ∈ Metric.closedBall a r ↔ ‖b - a‖ ≤ r
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.mk : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s → midpoint ℝ p₁ p₂ = s.center → s.IsDiameter p₁ p₂
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Fan.IsLimit.fac : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Fan F}
  (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) (i : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc f) (c.proj i) = f i
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.coe_toSubsemiring : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R), ↑↑P = ↑P
-- Mathlib.Data.Rat.Cast.CharZero
NNRat.cast_div : ∀ {α : Type u_3} [inst : DivisionSemiring α] [CharZero α] (p q : ℚ≥0), ↑(p / q) = ↑p / ↑q
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Ideal.adic_basis : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), SubmodulesRingBasis fun n => I ^ n • ⊤
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Polynomial.IsDistinguishedAt.algEquivQuotient_apply : ∀ {A : Type u_1} [inst : CommRing A] {g : Polynomial A} {I : Ideal A} (H : g.IsDistinguishedAt I)
  [inst_1 : IsAdicComplete I A] (a : Polynomial A ⧸ Ideal.span {g}),
  H.algEquivQuotient a = (Ideal.quotientMapₐ (Ideal.span {↑g}) (Polynomial.coeToPowerSeries.algHom A) ⋯) a
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.instIsContinuousOverCompObjPostMapOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} (X : C) (Y : D) (f : F.obj X ⟶ Y)
  [(CategoryTheory.Over.post F).IsContinuous (J.over X) (K.over (F.obj X))],
  ((CategoryTheory.Over.post F).comp (CategoryTheory.Over.map f)).IsContinuous (J.over X) (K.over Y)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mapsTo_insertNth_face : ∀ {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) {i : Fin (n + 1)} {x : ℝ},
  x ∈ Set.Ioc (I.lower i) (I.upper i) → Set.MapsTo (i.insertNth x) ↑(I.face i) ↑I
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.isPrestackFor_iff_of_sieve_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  {R R' : CategoryTheory.Presieve S},
  CategoryTheory.Sieve.generate R = CategoryTheory.Sieve.generate R' → (F.IsPrestackFor R ↔ F.IsPrestackFor R')
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
Unitary.conjStarAlgAut_mul_apply : ∀ {S : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : SMul S R]
  [inst_3 : IsScalarTower S R R] [inst_4 : SMulCommClass S R R] (u₁ u₂ : ↥(unitary R)) (x : R),
  ((Unitary.conjStarAlgAut S R) (u₁ * u₂)) x = ((Unitary.conjStarAlgAut S R) u₁) (((Unitary.conjStarAlgAut S R) u₂) x)
-- Mathlib.Data.Nat.Factorization.Divisors
Nat.coe_properDivisors_eq_prod_pow_lt_factorization : ∀ {n : ℕ}, ↑n.properDivisors = {x | ∃ f < n.factorization, (f.prod fun x1 x2 => x1 ^ x2) = x}
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.mk : {α : Type u} →
  [inst : AddGroup α] → (toTopologicalSpace : TopologicalSpace α) → IsTopologicalAddGroup α → AddGroupTopology α
-- Mathlib.Order.CompleteLattice.Basic
iInf₂_mono : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α] {f g : (i : ι) → κ i → α},
  (∀ (i : ι) (j : κ i), g i j ≤ f i j) → ⨅ i, ⨅ j, g i j ≤ ⨅ i, ⨅ j, f i j
-- Mathlib.Data.Set.Function
Equiv.bijOn_image : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) {s : Set α}, Set.BijOn (⇑e) s (⇑e '' s)
-- Mathlib.Algebra.DirectSum.Module
DirectSum.range_map : ∀ {ι : Type v} {M : ι → Type w} {N : ι → Type u_2} [inst : (i : ι) → AddCommGroup (M i)]
  [inst_1 : (i : ι) → AddCommGroup (N i)] (f : (i : ι) → M i →+ N i),
  (DirectSum.map f).range =
    AddSubgroup.comap (DirectSum.coeFnAddMonoidHom N) (AddSubgroup.pi Set.univ fun x => (f x).range)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The range of a ring homomorphism is a fintype if the domain is a fintype.
Note: this instance can form a diamond with `Subtype.fintype` in the
  presence of `Fintype S`.  -/
NonUnitalRingHom.fintypeRange : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocRing R] →
      [inst_1 : NonUnitalNonAssocRing S] → [Fintype R] → [DecidableEq S] → (f : R →ₙ+* S) → Fintype ↥f.range
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} (n : ℕ)
  (input input_1 : aig.RefVec w),
  input = input_1 →
    ∀ (curr : ℕ) (hcurr : curr ≤ n) (s s_1 : aig.RefVec (w * curr)),
      s = s_1 →
        Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go n input curr hcurr s =
          Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go n input_1 curr hcurr s_1
-- Mathlib.Order.Disjoint
IsCompl.right_unique : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y z : α}, IsCompl x y → IsCompl x z → y = z
-- Mathlib.Order.SetNotation
/-- Indexed infimum.  -/
«term⨅_,_» : Lean.ParserDescr
-- Init.Data.Random
/-- "Standard" random number generator.  -/
StdGen : Type
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.hom_ext_iff : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  {f g : S ⟶ S'}, f = g ↔ f.fst = g.fst ∧ f.snd = g.snd
-- Mathlib.Data.Finset.Sym
/-- `s.sym2` is the finset of all unordered pairs of elements from `s`.
It is the image of `s ×ˢ s` under the quotient `α × α → Sym2 α`.  -/
Finset.sym2 : {α : Type u_1} → Finset α → Finset (Sym2 α)
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero_assoc : ∀ {n : ℕ} (hn : autoParam ({ len := n }.len ≤ 2) SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero._auto_1)
  (hn' : autoParam ({ len := n + 1 }.len ≤ 2) SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero._auto_3)
  {Z : CategoryTheory.ObjectProperty.FullSubcategory fun a => a.len ≤ 2}
  (h : { obj := { len := n }, property := hn } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.δ₂ 0 hn hn')
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.σ₂ 0 hn' hn) h) =
    h
-- Mathlib.Logic.Equiv.Fin.Basic
finTwoArrowEquiv_symm_apply : ∀ (α : Type u_1), ⇑(finTwoArrowEquiv α).symm = fun x => ![x.1, x.2]
-- Mathlib.Logic.Relation
Relation.EqvGen.mono : ∀ {α : Type u_1} {r p : α → α → Prop}, r ≤ p → Relation.EqvGen r ≤ Relation.EqvGen p
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.withTopOrderIso_apply_coe : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  (A : FiniteMulArchimedeanClass M), (FiniteMulArchimedeanClass.withTopOrderIso M) ↑A = ↑A
-- Init.Data.Order.Lemmas
Std.max_le_iff : ∀ {α : Type u} [inst : Max α] [inst_1 : LE α] [Std.LawfulOrderSup α] {a b c : α}, a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.instMonoFKfSc : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' pq'' : κ) (i₀' i₀ i₁ i₂ i₃ : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  CategoryTheory.Mono
    (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂
        i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).f
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- A version of `Set.mem_finsetProd` with a simpler RHS for products over a Fintype.  -/
Set.mem_fintype_prod : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] [inst_1 : Fintype ι] (f : ι → Set α) (a : α),
  a ∈ ∏ i, f i ↔ ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), ∏ i, g i = a
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_le_comap_of_inv_on : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  {G : Type u_2} [inst_3 : FunLike G S R] [inst_4 : RingHomClass G S R] (g : G) (I : Ideal R),
  Set.LeftInvOn ⇑g ⇑f ↑I → Ideal.map f I ≤ Ideal.comap g I
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Construct a bundled `AddSemigrp` from the underlying type and typeclass.  -/
AddSemigrp.of : (M : Type u) → [AddSemigroup M] → AddSemigrp
-- Mathlib.Analysis.InnerProductSpace.PiL2
Module.Basis.coe_toOrthonormalBasis_repr_symm : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (v : Module.Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v),
  ⇑(v.toOrthonormalBasis hv).repr.symm = ⇑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜) ≪≫ₗ v.equivFun.symm)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.tendsto_abs_tan_of_cos_eq_zero : ∀ {x : ℝ}, Real.cos x = 0 → Filter.Tendsto (fun x => |Real.tan x|) (nhdsWithin x {x}ᶜ) Filter.atTop
-- Init.Data.Sum.Basic
Sum.getLeft?_inr : ∀ {α : Type u_1} {β : Type u_2} {x : β}, (Sum.inr x).getLeft? = none
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.RankFunction.mk.inj : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} {inst : PartialOrder α} {rank : ↑P.II → α}
  {lt : ∀ {x y : ↑P.II}, P.AncestralRel x y → rank x < rank y} {rank_1 : ↑P.II → α}
  {lt_1 : ∀ {x y : ↑P.II}, P.AncestralRel x y → rank_1 x < rank_1 y},
  { rank := rank, lt := lt } = { rank := rank_1, lt := lt_1 } → rank = rank_1
-- Mathlib.Computability.RE
/-- A recursively enumerable predicate is one which is the domain of a computable partial function.
 -/
REPred : {α : Type u_1} → [Primcodable α] → (α → Prop) → Prop
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.cosKernel_undef : ∀ (a : UnitAddCircle) {x : ℝ}, x ≤ 0 → HurwitzZeta.cosKernel a x = 0
-- Init.Data.BitVec.Bitblast
/-- The initial state is lawful.  -/
BitVec.DivModState.lawful_init : ∀ {w : ℕ} (args : BitVec.DivModArgs w), 0#w < args.d → BitVec.DivModState.Lawful args (BitVec.DivModState.init w)
-- Lean.Parser.Types
Lean.Parser.CacheableParserContext.mk : ℕ → ℕ → Bool → Option String.Pos.Raw → Option Lean.Parser.Token → Lean.Parser.CacheableParserContext
-- Lean.Elab.InfoTree.Types
Lean.Elab.MonadParentDecl.getParentDeclName? : {m : Type → Type} → [self : Lean.Elab.MonadParentDecl m] → m (Option Lean.Name)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.lemmaNames : Lean.Meta.SimpTheorems → Lean.PHashSet Lean.Meta.Origin
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.StrictOrLazy.strict : {α β : Type} → α → Lean.Widget.StrictOrLazy α β
-- Init.Data.Option.Attach
OptionT.instWeaklyLawfulMonadAttachOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m],
  WeaklyLawfulMonadAttach (OptionT m)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyRel.cast_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {S : Set X}
  {f₀ f₁ g₀ g₁ : C(X, Y)} (F : f₀.HomotopyRel f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X),
  (F.cast h₀ h₁) a = F a
-- Mathlib.Analysis.Distribution.Support
Distribution.dsupport_delta : ∀ {E : Type u_11} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞}
  [FiniteDimensional ℝ E], ∀ x ∈ Ω, Distribution.dsupport ⇑(Distribution.delta x) = {x}
-- Mathlib.Analysis.Convex.Between
wbtw_zero_one_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] {x : R}, Wbtw R 0 x 1 ↔ x ∈ Set.Icc 0 1
-- Mathlib.CategoryTheory.Limits.Connected
/-- (Impl). The obvious natural transformation from (X × K -) to X  -/
CategoryTheory.ProdPreservesConnectedLimits.γ₁ : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
      {J : Type v₂} →
        [inst_2 : CategoryTheory.SmallCategory J] →
          {K : CategoryTheory.Functor J C} →
            (X : C) → K.comp (CategoryTheory.Limits.prod.functor.obj X) ⟶ (CategoryTheory.Functor.const J).obj X
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.page_d : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r : ℤ) (hr : r₀ ≤ r) (pq pq' : κ),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X data r hr).d pq pq' =
    CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD X data r pq pq' ⋯