mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Path
Path.hasBasis_uniformity : ∀ {X : Type u_1} [inst : UniformSpace X] {x y : X},
  (uniformity (Path x y)).HasBasis (fun x => x ∈ uniformity X) fun x_1 =>
    {γ | ∀ (t : ↑unitInterval), (γ.1 t, γ.2 t) ∈ x_1}
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.isProbabilityMeasure_trajFun : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1)))
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ) (x₀ : (i : ↥(Finset.Iic a)) → X ↑i),
  MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.Kernel.trajFun κ a x₀)
-- Batteries.Data.String.Lemmas
String.posOfAux_eq : ∀ (s : String) (c : Char), String.Legacy.posOfAux s c = String.Legacy.findAux s fun x => x == c
-- Mathlib.Algebra.Group.Defs
succ_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (n : ℕ), (n + 1) • a = n • a + a
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.right_induction : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) {P : CliffordAlgebra Q → Prop},
  (∀ (r : R), P ((algebraMap R (CliffordAlgebra Q)) r)) →
    (∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)) →
      (∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (CliffordAlgebra.ι Q) m)) → ∀ (x : CliffordAlgebra Q), P x
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_inf_mul_relfinrank_of_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (C : IntermediateField F E), A ≤ B → A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.piecewise_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {s : Set α} (hs : MeasurableSet sᶜ)
  (f g : MeasureTheory.SimpleFunc α β),
  MeasureTheory.SimpleFunc.piecewise sᶜ hs f g = MeasureTheory.SimpleFunc.piecewise s ⋯ g f
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.foldl_filterMap'.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive x
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j))
  ⦃Y Y' : C⦄ (g : Y' ⟶ Y) (q : Y ⟶ S) (q' : Y' ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (gf₁ : Y' ⟶ X i₁)
  (gf₂ : Y' ⟶ X i₂)
  (hq :
    autoParam (CategoryTheory.CategoryStruct.comp g q = q')
      CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'._auto_1)
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'._auto_3)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'._auto_5)
  (hgf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp g f₁ = gf₁)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'._auto_7)
  (hgf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp g f₂ = gf₂)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'._auto_9)
  {Z : ↑(F.obj { as := Opposite.op Y' })} (h : (F.map gf₂.op.toLoc).toFunctor.obj (obj' i₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom
        (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q f₁ f₂ hf₁ hf₂) g gf₁ gf₂ ⋯ ⋯)
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q' gf₁ gf₂ ⋯ ⋯) h
-- Init.Data.List.Lemmas
List.length_insert_of_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∈ l → (List.insert a l).length = l.length
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_eq_zero : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω}, μ[|s] = 0 ↔ μ s = ⊤ ∨ μ s = 0
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- A crude upper bound: `σ_k(n) ≤ n ^ (k + 1)`.  -/
ArithmeticFunction.sigma_le_pow_succ : ∀ (k n : ℕ), (ArithmeticFunction.sigma k) n ≤ n ^ (k + 1)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.topEquiv_apply : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (a : ↥⊤),
  IntermediateField.topEquiv a = ↑a
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.range'TR.go.match_1.splitter : (motive : ℕ → ℕ → List ℕ → Sort u_1) →
  (x x_1 : ℕ) →
    (x_2 : List ℕ) →
      ((x : ℕ) → (acc : List ℕ) → motive 0 x acc) →
        ((n e : ℕ) → (acc : List ℕ) → motive n.succ e acc) → motive x x_1 x_2
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.Model.0.Lean.Meta.Grind.Arith.Cutsat.natCastToInt? : Lean.Expr → Option Lean.Expr
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.mul_def : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n m : ℕ} {χ : DirichletCharacter R n} {ψ : DirichletCharacter R m},
  χ.primitive_mul ψ = (χ.mul ψ).primitiveCharacter
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.mono' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β} {g : α → ℝ},
  MeasureTheory.HasFiniteIntegral g μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a) → MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso_inv_hom : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) (E : L.RightExtension F) (c : C),
  (CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso G F L E c).inv.hom =
    CategoryTheory.CategoryStruct.id (G.obj (E.left.obj c))
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- The equivalence relation of being almost everywhere equal for almost everywhere strongly
measurable functions.  -/
MeasureTheory.Measure.aeEqSetoid : {α : Type u_1} →
  (β : Type u_2) →
    [inst : MeasurableSpace α] →
      [inst_1 : TopologicalSpace β] →
        (μ : MeasureTheory.Measure α) → Setoid { f // MeasureTheory.AEStronglyMeasurable f μ }
-- Mathlib.Order.Partition.Basic
Partition.removeBot.congr_simp : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] (P P_1 : Set α) (e_P : P = P_1) (indep : sSupIndep P)
  (hsSup : sSup P = s), Partition.removeBot P indep hsSup = Partition.removeBot P_1 ⋯ ⋯
-- Mathlib.Geometry.Euclidean.Triangle
/-- The **Exterior angle theorem**. an exterior angle of a triangle is equal to the sum of the
measures of the remote interior angles.  -/
EuclideanGeometry.exterior_angle_eq_angle_add_angle : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P} (p : P),
  Sbtw ℝ p p₁ p₂ → EuclideanGeometry.angle p₃ p₁ p = EuclideanGeometry.angle p₁ p₃ p₂ + EuclideanGeometry.angle p₃ p₂ p₁
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Traverses `P` and `goal` simultaneously, proving `goal`.  -/
_private.Mathlib.Tactic.Simproc.ExistsAndEq.0.ExistsAndEq.mkBeforeToAfter.go : {goal P : Q(Prop)} →
  Q(«$P») →
    List ExistsAndEq.VarQ →
      List ExistsAndEq.HypQ →
        ExistsAndEq.Path →
          {u : Lean.Level} → {α : Q(Sort u)} → {a a' : Q(«$α»)} → Q(«$a» = «$a'») → Lean.MetaM Q(«$goal»)
-- Mathlib.Data.ZMod.Basic
/-- The canonical ring homomorphism from `ZMod n` to a ring of characteristic dividing `n`.

See also `ZMod.lift` for a generalized version working in `AddGroup`s.
 -/
ZMod.castHom : {n m : ℕ} → m ∣ n → (R : Type u_2) → [inst : Ring R] → [CharP R m] → ZMod n →+* R
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.clear.sizeOf_spec : sizeOf Lean.Parser.Tactic.MCasesPat.clear = 1
-- Mathlib.Data.ZMod.Basic
/-- The range of `(m * · + k)` on natural numbers is the set of elements `≥ k` in the
residue class of `k` mod `m`.  -/
Nat.range_mul_add : ∀ (m k : ℕ), (Set.range fun n => m * n + k) = {n | ↑n = ↑k ∧ k ≤ n}
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.uri : Lean.Lsp.CreateFile → Lean.Lsp.DocumentUri
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_neg_pi_div_two : ∀ (c : ℂ) (R : ℝ), circleMap c R (-Real.pi / 2) = c - ↑R * Complex.I
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.eq_of_forall_proj_eq : ∀ {X : Type u_2} [inst : TopologicalSpace X] [T2Space X] [CompactSpace X] [disc : TotallyDisconnectedSpace X] {x y : X},
  (∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y) → x = y
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.hom_ext_nonempty : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [inst : Monoid K] [inst_1 : (i : ι) → Monoid (G i)]
  [inst_2 : Monoid H] {φ : (i : ι) → H →* G i} [hn : Nonempty ι] {f g : Monoid.PushoutI φ →* K},
  (∀ (i : ι), f.comp (Monoid.PushoutI.of i) = g.comp (Monoid.PushoutI.of i)) → f = g
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : SeminormedAddGroup E]
  {ι : Type u_3} [Nonempty ι] [Countable ι] [inst_3 : LinearOrder ι] {f : ι → α → E} {f_lim : α → E},
  (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) →
    MeasureTheory.eLpNorm f_lim ⊤ μ ≤ Filter.liminf (fun n => MeasureTheory.eLpNorm (f n) ⊤ μ) Filter.atTop
-- Mathlib.CategoryTheory.Elements
/-- The forward direction of the equivalence `F.Elementsᵒᵖ ≅ (yoneda, F)`,
given by `CategoryTheory.yonedaEquiv`.
 -/
CategoryTheory.CategoryOfElements.toCostructuredArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      CategoryTheory.Functor F.Elementsᵒᵖ (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic.0.Tactic.ComputeAsymptotics.MultiseriesExpansion.const.match_1.splitter : (motive : Tactic.ComputeAsymptotics.Basis → Sort u_1) →
  (basis : Tactic.ComputeAsymptotics.Basis) →
    (Unit → motive []) → ((basis_hd : ℝ → ℝ) → (basis_tl : List (ℝ → ℝ)) → motive (basis_hd :: basis_tl)) → motive basis
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Counting.0.SimpleGraph.badVertices.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α) [inst : DecidableRel G.Adj] (ε : ℝ) (s t : Finset α),
  SimpleGraph.badVertices✝ G ε s t = {x ∈ s | ↑{y ∈ t | G.Adj x y}.card < (↑(G.edgeDensity s t) - ε) * ↑t.card}
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- The determinant of a 2×2 block matrix with the lower-left block equal to zero is the product of
the determinants of the diagonal blocks. For the generalization to any number of blocks, see
`Matrix.det_of_isUpperTriangular`.  -/
Matrix.det_fromBlocks_zero₂₁ : ∀ {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] {R : Type v} [inst_4 : CommRing R] (A : Matrix m m R) (B : Matrix m n R) (D : Matrix n n R),
  (Matrix.fromBlocks A B 0 D).det = A.det * D.det
-- Mathlib.Data.Finset.Fold
_private.Mathlib.Data.Finset.Fold.0.Finset.«term_*_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.add_le_add_left : ∀ {d : ℕ} (a b : ℤ√↑d), a ≤ b → ∀ (c : ℤ√↑d), a + c ≤ b + c
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_toPartialMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  (AlgebraicGeometry.Scheme.Hom.toPartialMap f).fromSpecStalkOfMem trivial =
    CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) f
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.inv_hom_id_app_app_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E']
  {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (e : F ≅ G) (X₁ : C)
  (X₂ : D) (X₃ : E) {Z : E'} (h : ((G.obj X₁).obj X₂).obj X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((e.inv.app X₁).app X₂).app X₃)
      (CategoryTheory.CategoryStruct.comp (((e.hom.app X₁).app X₂).app X₃) h) =
    h
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Connected.coe : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph}, H.Connected → H.coe.Connected
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_alterKey_eq_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : Option (β k) → Option (β k)} {he : (Std.Internal.List.alterKey k f l).isEmpty = false},
      Std.Internal.List.minKey (Std.Internal.List.alterKey k f l) he = k ↔
        (f (Std.Internal.List.getValueCast? k l)).isSome = true ∧
          ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_comapDomain_nat_add_one : ∀ {M : Type u_5} [inst : AddCommMonoid M] (l : ℕ →₀ M),
  Finsupp.mapDomain (fun x => x + 1) ((Finsupp.comapDomain.addMonoidHom ⋯) l) = Finsupp.erase 0 l
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.map_homMk'_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y P Q : C} {k : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage k] {l : P ⟶ Q} [inst_2 : CategoryTheory.Limits.HasImage l] {m : X ⟶ P}
  {n : Y ⟶ Q} (w : CategoryTheory.CategoryStruct.comp m l = CategoryTheory.CategoryStruct.comp k n)
  [inst_3 : CategoryTheory.Limits.HasImageMap (CategoryTheory.Arrow.homMk' m n w)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map (CategoryTheory.Arrow.homMk' m n w))
      (CategoryTheory.Limits.image.ι l) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι k) n
-- Init.Data.List.Nat.Modify
List.modifyHead_id : ∀ {α : Type u_1}, List.modifyHead id = id
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHAddOffset_1 : HAdd Std.Time.PlainDateTime Std.Time.Week.Offset Std.Time.PlainDateTime
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.inradius_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)), (s.reindex e).inradius = s.inradius
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp], t.WF → ∀ {l : List α} {k : α}, k ∈ t.insertManyIfNewUnit l ↔ k ∈ t ∨ l.contains k = true
-- Mathlib.RingTheory.PicardGroup
/-- The class of an invertible module in the Picard group.  -/
CommRing.Pic.mk : (R : Type u) →
  (M : Type v) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [Module.Invertible R M] → CommRing.Pic R
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.instIsMultiplicativeIsLocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C),
  P.isLocal.IsMultiplicative
-- Mathlib.Algebra.Homology.DerivedCategory.Fractions
/-- Any morphism `f : Q.obj X ⟶ Q.obj Y` in the derived category with `Y` strictly `≥ n`
can be written as `f = Q.map g ≫ inv (Q.map s)` with `g : X ⟶ Y'` and `s : Y ⟶ Y'`
a quasi-isomorphism with `Y'` strictly `≥ n`.  -/
DerivedCategory.left_fac_of_isStrictlyGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {X Y : CochainComplex C ℤ} (f : DerivedCategory.Q.obj X ⟶ DerivedCategory.Q.obj Y)
  (n : ℤ) [Y.IsStrictlyGE n],
  ∃ Y',
    ∃ (_ : Y'.IsStrictlyGE n),
      ∃ g s,
        ∃ (x : CategoryTheory.IsIso (DerivedCategory.Q.map s)),
          f =
            CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map g) (CategoryTheory.inv (DerivedCategory.Q.map s))
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.coe_eq_zero_iff : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : Zero α] [T0Space α] {x : α}, ↑x = 0 ↔ x = 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Coercing a subspace to a set then taking the affine span produces the original subspace.  -/
AffineSubspace.affineSpan_coe : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s : AffineSubspace k P), affineSpan k ↑s = s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback fallback' : α}, t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.sInf_def : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] (s : Set (MeasureTheory.Filtration ι m))
  (i : ι), ↑(sInf s) i = if s.Nonempty then sInf ((fun f => ↑f i) '' s) else m
-- Mathlib.NumberTheory.ModularForms.Basic
/-- Copy of a `ModularForm` with a new `toFun` equal to the old one, optionally transporting
along an equality of subgroups. Useful to fix definitional equalities.  -/
ModularForm.copy : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} →
    {Γ' : Subgroup (GL (Fin 2) ℝ)} →
      (f : ModularForm Γ k) →
        (f' : UpperHalfPlane → ℂ) → f' = ⇑f → autoParam (Γ' = Γ) ModularForm.copy._auto_1 → ModularForm Γ' k
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.IsInitial.card_lt_card : ∀ {a b : Ordinal.{u_1}}, b.IsInitial → (a.card < b.card ↔ a < b)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.ι_comp_sigmaComparison : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C)
  [inst_2 : CategoryTheory.Limits.HasCoproduct f] [inst_3 : CategoryTheory.Limits.HasCoproduct fun b => G.obj (f b)]
  (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun b => G.obj (f b)) b)
      (CategoryTheory.Limits.sigmaComparison G f) =
    G.map (CategoryTheory.Limits.Sigma.ι f b)
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.splits_prev : ∀ {s : String.Slice} (p : s.Pos) (hp : p ≠ s.startPos),
  (p.prev hp).Splits (s.sliceTo (p.prev hp)).copy (String.singleton ((p.prev hp).get ⋯) ++ (s.sliceFrom p).copy)
-- Mathlib.Algebra.Group.Basic
sub_left_injective : ∀ {G : Type u_3} [inst : AddGroup G] {b : G}, Function.Injective fun a => a - b
-- Mathlib.Topology.Order.Basic
tendsto_nhds_bot_mono' : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace β] [inst_1 : Preorder β] [inst_2 : OrderBot β] [OrderTopology β]
  {l : Filter α} {f g : α → β}, Filter.Tendsto f l (nhds ⊥) → g ≤ f → Filter.Tendsto g l (nhds ⊥)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_add' : ∀ {x y z : ℝ}, 0 ≤ x → y + z ≠ 0 → x ^ (y + z) = x ^ y * x ^ z
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonSnippetString.fromJson : Lean.Json → Except String Lean.Lsp.SnippetString
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.of_coe : ∀ (R : Type u) [inst : Semiring R] (X : SemimoduleCat R), SemimoduleCat.of R ↑X = X
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- For any element `x : A` and any set `B` in the submodule basis on `A`,
there is another basis element `B'` such that `x * B'` is in `B`.  -/
RingSubgroupsBasis.rightMul : ∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] {B : ι → AddSubgroup A},
  RingSubgroupsBasis B → ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.enorm_def : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), ‖f‖ₑ = MeasureTheory.eLpNorm (↑↑f) p μ
-- Mathlib.Combinatorics.Additive.Dissociation
addDissociated_iff_sum_eq_subsingleton : ∀ {α : Type u_1} [inst : AddCommGroup α] {s : Set α},
  AddDissociated s ↔ ∀ (a : α), {t | ↑t ⊆ s ∧ ∑ x ∈ t, x = a}.Subsingleton
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.associator_neg_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.AddMon C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom =
    (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).inv
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldlM_toListModel_eq_foldlM : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {m : Type u_1 → Type u_2} {δ : Type u_1}
  [inst : Monad m] [LawfulMonad m] {f : δ → (a : α) × β a → m δ} {init : δ},
  List.foldlM f init t.toListModel = Std.DTreeMap.Internal.Impl.foldlM (fun acc k v => f acc ⟨k, v⟩) init t
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- The cardinality of the multiset `nthRoots ↑n (1 : R)` is `n`
if there is a primitive root of unity in `R`.  -/
IsPrimitiveRoot.card_nthRoots_one : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
  IsPrimitiveRoot ζ n → (Polynomial.nthRoots n 1).card = n
-- Init.Data.Rat.Lemmas
Rat.normalize.eq_1 : ∀ (num : ℤ) (den : ℕ) (den_nz : den ≠ 0),
  Rat.normalize num den den_nz = Rat.maybeNormalize num den (num.natAbs.gcd den) ⋯ ⋯ ⋯ ⋯
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_symm : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] (e : Equiv.Perm α),
  Equiv.Perm.sign (Equiv.symm e) = Equiv.Perm.sign e
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeights_empty_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  0 < s.excenterWeights ∅ i
-- Mathlib.Data.ZMod.Defs
ZMod.fintype : (n : ℕ) → [NeZero n] → Fintype (ZMod n)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.simp : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.Analysis.Complex.Norm
Complex.re_neg_ne_zero_of_re_pos : ∀ {s : ℂ}, 0 < s.re → (-s).re ≠ 0
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.continuous_lintegral_boundedContinuousFunction : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [inst_2 : OpensMeasurableSpace X]
  (f : BoundedContinuousFunction X NNReal), Continuous fun μ => ∫⁻ (x : X), ↑(f x) ∂↑μ