mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Multilinear.TensorProduct
MultilinearMap.domCoprodDep_apply : ∀ {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [inst : CommSemiring R] {N₁ : Type u_6} [inst_1 : AddCommMonoid N₁]
  [inst_2 : Module R N₁] {N₂ : Type u_7} [inst_3 : AddCommMonoid N₂] [inst_4 : Module R N₂] {N : ι₁ ⊕ ι₂ → Type u_8}
  [inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)] [inst_6 : (i : ι₁ ⊕ ι₂) → Module R (N i)]
  (a : MultilinearMap R (fun i₁ => N (Sum.inl i₁)) N₁) (b : MultilinearMap R (fun i₂ => N (Sum.inr i₂)) N₂)
  (v : (i : ι₁ ⊕ ι₂) → N i), (a.domCoprodDep b) v = (a fun i₁ => v (Sum.inl i₁)) ⊗ₜ[R] b fun i₂ => v (Sum.inr i₂)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.isEmpty = true → t.minKey? = none
-- Mathlib.Order.Basic
subrelation_iff_le : ∀ {α : Type u_2} {r s : α → α → Prop}, Subrelation r s ↔ r ≤ s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} [inst_1 : Inhabited (β a)] {b : β a}, (t.insert a b).get! a = b
-- Mathlib.Data.List.Lattice
List.Sublist.inter_right : ∀ {α : Type u_1} [inst : DecidableEq α] {l₁ l₂ l₃ : List α}, l₁.Sublist l₂ → (l₁ ∩ l₃).Sublist (l₂ ∩ l₃)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α}
  [inst_2 : Inhabited (β a)],
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → Std.Internal.List.getValueCast! a l = Std.Internal.List.getValueCast! a l'
-- Mathlib.Algebra.Ring.Regular
/-- A ring is Dedekind-finite if and only if every element has at most one right inverse.  -/
IsDedekindFiniteMonoid.iff_eq_of_mul_left_eq_one : ∀ {α : Type u_1} [inst : Ring α], IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.BifibrantObject.homMk_homMk_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [inst_5 : HomotopicalAlgebra.IsCofibrant X]
  [inst_6 : HomotopicalAlgebra.IsCofibrant Y] [inst_7 : HomotopicalAlgebra.IsCofibrant Z]
  [inst_8 : HomotopicalAlgebra.IsFibrant X] [inst_9 : HomotopicalAlgebra.IsFibrant Y]
  [inst_10 : HomotopicalAlgebra.IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : HomotopicalAlgebra.BifibrantObject C}
  (h : HomotopicalAlgebra.BifibrantObject.mk Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.BifibrantObject.homMk f)
      (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.BifibrantObject.homMk g) h) =
    CategoryTheory.CategoryStruct.comp
      (HomotopicalAlgebra.BifibrantObject.homMk (CategoryTheory.CategoryStruct.comp f g)) h
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `HasProdUniformly f g` means that
the product `∏ i, f i b` converges uniformly (wrt `b`) to `g`.  -/
HasProdUniformly : {α : Type u_1} → {β : Type u_2} → {ι : Type u_3} → [CommMonoid α] → (ι → β → α) → (β → α) → [UniformSpace α] → Prop
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.natCast_opow : ∀ (m n : ℕ), ↑(m ^ n) = ↑m ^ ↑n
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Construct an object of `P.CostructuredArrow Q F X` from a morphism `F.obj A ⟶ X`.  -/
CategoryTheory.MorphismProperty.CostructuredArrow.mk : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} D] →
        {P : CategoryTheory.MorphismProperty D} →
          (Q : CategoryTheory.MorphismProperty C) →
            {F : CategoryTheory.Functor C D} → {X : D} → {A : C} → (f : F.obj A ⟶ X) → P f → P.CostructuredArrow Q F X
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Annotates the term with the current expression position and registers `TermInfo`
to associate the term to the current expression, unless the syntax has a synthetic position
and associated `Info` already.
 -/
Lean.PrettyPrinter.Delaborator.annotateTermInfoUnlessAnnotated : Lean.Term → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.ball.eq_1 : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α) (ε : ℝ), Metric.ball x ε = {y | dist y x < ε}
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_zero : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] (g : α → F)
  (l : Filter α), (fun _x => 0) =O[l] g
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ` and `f''` is strictly positive on `D`,
then `f` is strictly convex on `D`.
Note that we don't require twice differentiability explicitly as it is already implied by the second
derivative being strictly positive, except at at most one point.  -/
strictConvexOn_of_deriv2_pos' : ∀ {D : Set ℝ}, Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ D, 0 < deriv^[2] f x) → StrictConvexOn ℝ D f
-- Init.Grind.AC
Lean.Grind.AC.Seq.endsWithVar_k.eq_1 : ∀ (s : Lean.Grind.AC.Seq) (x : Lean.Grind.AC.Var),
  s.endsWithVar_k x = Lean.Grind.AC.Seq.rec (fun y => Nat.beq x y) (fun x x_1 ih => ih) s
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.toLax_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b c : B} (f : a ⟶ b) (g : b ⟶ c), F.toLax.mapComp f g = (F.mapComp f g).inv
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.diag_conjTranspose : ∀ {n : Type u_3} {α : Type v} [inst : Star α] (A : Matrix n n α), A.conjTranspose.diag = star A.diag
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabNamespace : Lean.Elab.Command.CommandElab
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Ring
/-- The Euler function is related to $A_0$ by

$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) = 1 - x - x^2 A_0 $$  -/
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.Ring.0.Pentagonal.tprod_one_sub_pow_eq_powMulProdOneSubPow_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [T2Space R] {x : R},
  (∀ (k : ℕ), Summable fun x_1 => Pentagonal.powMulProdOneSubPow✝ k x_1 x) →
    (∀ (k : ℕ), Multipliable fun n => 1 - x ^ (n + k + 1)) →
      ∏' (n : ℕ), (1 - x ^ (n + 1)) = 1 - x - x ^ 2 * ∑' (n : ℕ), Pentagonal.powMulProdOneSubPow✝ 0 n x
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- The measure is σ-additive  -/
MeasureTheory.VectorMeasure.m_iUnion' : ∀ {α : Type u_3} [inst : MeasurableSpace α] {M : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  (self : MeasureTheory.VectorMeasure α M) ⦃f : ℕ → Set α⦄,
  (∀ (i : ℕ), MeasurableSet (f i)) →
    Pairwise (Function.onFun Disjoint f) → HasSum (fun i => self.measureOf' (f i)) (self.measureOf' (⋃ i, f i))
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.rpow : ∀ {f : ℝ → ℝ} (p : ℝ),
  AkraBazziRecurrence.GrowsPolynomially f →
    (∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) → AkraBazziRecurrence.GrowsPolynomially fun x => f x ^ p
-- Mathlib.Order.MinMax
lt_max_of_lt_right : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < c → a < max b c
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.instIsClosedUnderIsomorphismsIsCardinalPresentable : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular],
  (CategoryTheory.isCardinalPresentable C κ).IsClosedUnderIsomorphisms
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.ker.eq_1 : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N), f.ker = LieSubmodule.comap f ⊥
-- Mathlib.Topology.Separation.Connected
subsingleton_iff_discrete_and_indiscrete : ∀ {X : Type u_1} [inst : TopologicalSpace X], Subsingleton X ↔ DiscreteTopology X ∧ IndiscreteTopology X
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.mk.injEq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f g : ℝ → E) (k : ℝ) (ε : ℂ) (f₀ g₀ : E)
  (hf_int : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume)
  (hg_int : MeasureTheory.LocallyIntegrableOn g (Set.Ioi 0) MeasureTheory.volume) (hk : 0 < k) (hε : ε ≠ 0)
  (h_feq : ∀ x ∈ Set.Ioi 0, f (1 / x) = (ε * ↑(x ^ k)) • g x)
  (hf_top : ∀ (r : ℝ), (fun x => f x - f₀) =O[Filter.atTop] fun x => x ^ r)
  (hg_top : ∀ (r : ℝ), (fun x => g x - g₀) =O[Filter.atTop] fun x => x ^ r) (f_1 g_1 : ℝ → E) (k_1 : ℝ) (ε_1 : ℂ)
  (f₀_1 g₀_1 : E) (hf_int_1 : MeasureTheory.LocallyIntegrableOn f_1 (Set.Ioi 0) MeasureTheory.volume)
  (hg_int_1 : MeasureTheory.LocallyIntegrableOn g_1 (Set.Ioi 0) MeasureTheory.volume) (hk_1 : 0 < k_1) (hε_1 : ε_1 ≠ 0)
  (h_feq_1 : ∀ x ∈ Set.Ioi 0, f_1 (1 / x) = (ε_1 * ↑(x ^ k_1)) • g_1 x)
  (hf_top_1 : ∀ (r : ℝ), (fun x => f_1 x - f₀_1) =O[Filter.atTop] fun x => x ^ r)
  (hg_top_1 : ∀ (r : ℝ), (fun x => g_1 x - g₀_1) =O[Filter.atTop] fun x => x ^ r),
  ({ f := f, g := g, k := k, ε := ε, f₀ := f₀, g₀ := g₀, hf_int := hf_int, hg_int := hg_int, hk := hk, hε := hε,
        h_feq := h_feq, hf_top := hf_top, hg_top := hg_top } =
      { f := f_1, g := g_1, k := k_1, ε := ε_1, f₀ := f₀_1, g₀ := g₀_1, hf_int := hf_int_1, hg_int := hg_int_1,
        hk := hk_1, hε := hε_1, h_feq := h_feq_1, hf_top := hf_top_1, hg_top := hg_top_1 }) =
    (f = f_1 ∧ g = g_1 ∧ k = k_1 ∧ ε = ε_1 ∧ f₀ = f₀_1 ∧ g₀ = g₀_1)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.con_inv_mul_cancel : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (x : FreeMonoid (G ⊕ H)),
  (Monoid.coprodCon G H) (FreeMonoid.ofList (List.map (Sum.map Inv.inv Inv.inv) (FreeMonoid.toList x)).reverse * x) 1
-- Mathlib.Topology.Category.Sequential
Sequential.sequentialToTop_obj : ∀ (self : Sequential), Sequential.sequentialToTop.obj self = self.toTop
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.instAddCommGroupCotangent : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → AddCommGroup I.Cotangent
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.derivative_U_eval_one_eq_div : ∀ {𝔽 : Type u_3} [inst : Field 𝔽] [neZero3 : NeZero 3] (n : ℤ),
  Polynomial.eval 1 (Polynomial.derivative (Polynomial.Chebyshev.U 𝔽 n)) = (↑n + 2) * (↑n + 1) * ↑n / 3
-- Batteries.Data.Stream
_private.Batteries.Data.Stream.0.Std.Stream.drop.match_3.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toFun_tendsto_top_of_firstNonzeroIsPos : ∀ {m : Tactic.ComputeAsymptotics.UnitMonomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    List.length m = List.length basis → m.FirstNonzeroIsPos → Filter.Tendsto (m.toFun basis) Filter.atTop Filter.atTop
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.sInter : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {x : X} {S : Set (Set X)},
  (∀ s ∈ S, Convexity.IsStarConvexSet R x s) → Convexity.IsStarConvexSet R x (⋂₀ S)
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.toTopologicalSpace : {α : Type u} → [inst : Group α] → GroupTopology α → TopologicalSpace α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.Algebra.Homology.CommSq
/-- A commutative square in a preadditive category is a pullback square iff
the corresponding diagram `0 ⟶ X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0` makes `X₁` a kernel.  -/
CategoryTheory.CommSq.isLimitEquivIsLimitKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X₁ X₂ X₃ X₄ : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] →
          {fst : X₁ ⟶ X₂} →
            {snd : X₁ ⟶ X₃} →
              {f : X₂ ⟶ X₄} →
                {g : X₃ ⟶ X₄} →
                  (sq : CategoryTheory.CommSq fst snd f g) →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk fst snd ⋯) ≃
                      CategoryTheory.Limits.IsLimit sq.kernelFork
-- Mathlib.Algebra.Algebra.Hom
AlgHom.mul_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (φ ψ : A →ₐ[R] A)
  (x : A), (φ * ψ) x = φ (ψ x)
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, Polynomial.toLaurent f ≠ 0 ↔ f ≠ 0
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.topology_eq_lowerSetTopology : ∀ {α : Type u_4} {t : TopologicalSpace α} {inst : Preorder α} [self : Topology.IsLowerSet α], t = Topology.lowerSet α
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- The Weierstrass curve over `R` induced by an admissible linear change of variables
`(X, Y) ↦ (u²X + r, u³Y + u²sX + t)` for some `u` in `Rˣ` and some `r, s, t` in `R`.  -/
WeierstrassCurve.variableChange_def : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  C • W =
    { a₁ := ↑C.u⁻¹ * (W.a₁ + 2 * C.s), a₂ := ↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2),
      a₃ := ↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t),
      a₄ := ↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t),
      a₆ := ↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁) }
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
/-- Nested intervals lemma: if `[f n, g n]` is an antitone sequence of nonempty
closed intervals, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`.  -/
ciSup_mem_iInter_Icc_of_antitone_Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderSup α] [inst_1 : Preorder β]
  [IsDirectedOrder β] {f g : β → α},
  (Antitone fun n => Set.Icc (f n) (g n)) → (∀ (n : β), f n ≤ g n) → ⨆ n, f n ∈ ⋂ n, Set.Icc (f n) (g n)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.sub_lt_of_lt_add : ∀ {a b c : Ordinal.{u_4}}, a < b + c → 0 < c → a - b < c
-- Mathlib.Algebra.Order.Antidiag.Finsupp
Finset.mem_finsuppAntidiag' : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] {s : Finset ι} {n : μ} {f : ι →₀ μ},
  f ∈ s.finsuppAntidiag n ↔ (f.sum fun x x_1 => x_1) = n ∧ f.support ⊆ s
-- Mathlib.GroupTheory.GroupAction.FixedPoints
AddAction.fixedBy_add : ∀ (α : Type u_1) {M : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] (m₁ m₂ : M),
  AddAction.fixedBy α m₁ ∩ AddAction.fixedBy α m₂ ⊆ AddAction.fixedBy α (m₁ + m₂)
-- Mathlib.CategoryTheory.Types.Basic
/-- **Alias** of `CategoryTheory.Functor.map_hom_inv_apply`. -/
CategoryTheory.FunctorToTypes.map_inv_map_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f] {F_1 : D → D → Type uF}
  {carrier : D → Type w} {instFunLike : (X Y : D) → FunLike (F_1 X Y) (carrier X) (carrier Y)}
  [inst_3 : CategoryTheory.ConcreteCategory D F_1] (x : carrier (F.obj X)),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.inv f)))
      ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    x
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι_app : ∀ {X : AlgebraicGeometry.Scheme} (U V : X.Opens),
  AlgebraicGeometry.Scheme.Hom.app U.ι V = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.δ_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {A : C} (x₃ : A ⟶ S.L₀.X₃) (x₂ : A ⟶ S.L₁.X₂) (x₁ : A ⟶ S.L₂.X₁),
  CategoryTheory.CategoryStruct.comp x₂ S.L₁.g = CategoryTheory.CategoryStruct.comp x₃ S.v₀₁.τ₃ →
    CategoryTheory.CategoryStruct.comp x₁ S.L₂.f = CategoryTheory.CategoryStruct.comp x₂ S.v₁₂.τ₂ →
      CategoryTheory.CategoryStruct.comp x₃ S.δ = CategoryTheory.CategoryStruct.comp x₁ S.v₂₃.τ₁
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.getMatchOptMotive : Lean.Syntax → Lean.Syntax
-- Mathlib.Topology.Category.TopCat.Adjunctions
TopCat.adj₂_unit : TopCat.adj₂.unit =
  { app := fun X => TopCat.ofHom { toFun := id, continuous_toFun := ⋯ }, naturality := TopCat.adj₂._proof_1 }
-- Mathlib.Order.Filter.Basic
Set.EqOn.eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f g : α → β}, Set.EqOn f g s → f =ᶠ[Filter.principal s] g
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, k ∈ m₂ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.coe_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f g : CauSeq β abv), ↑(f - g) = ↑f - ↑g
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.ret : {K : Type u_1} → {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → Turing.TM2.Stmt Γ Λ σ → Turing.TM2to1.Λ' K Γ Λ σ
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceRErase.eq_4 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (hrb_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced) (size : ℕ) (rk : α)
  (rv : β rk) (size_1 : ℕ) (rlk : α) (rlv : β rlk) (l r_3 : Std.DTreeMap.Internal.Impl α β)
  (hrb_4 :
    (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r_3)
        Std.DTreeMap.Internal.Impl.leaf).Balanced)
  (hlr_3 :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
      (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r_3)
          Std.DTreeMap.Internal.Impl.leaf).size
      Std.DTreeMap.Internal.Impl.leaf.size),
  Std.DTreeMap.Internal.Impl.balanceRErase k v Std.DTreeMap.Internal.Impl.leaf
      (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r_3)
        Std.DTreeMap.Internal.Impl.leaf)
      hrb_2 hrb_4 hlr_3 =
    Std.DTreeMap.Internal.Impl.inner 3 rlk rlv
      (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
      (Std.DTreeMap.Internal.Impl.inner 1 rk rv Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Extract an isomorphism `rightKanExtension L F ⋙ G ≅ rightKanExtension L (F ⋙ G)` when `G`
preserves right Kan extensions.  -/
CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves : {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) →
                      [inst_4 : G.PreservesRightKanExtension F L] →
                        [inst_5 : L.HasRightKanExtension F] →
                          (L.rightKanExtension F).comp G ≅ L.rightKanExtension (F.comp G)
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ici_eq_Icc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : OrderTop α] (a : α),
  Finset.Ici a = Finset.Icc a ⊤
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, k ∈ m₂ → (m₁ ∩ m₂).get! k = m₁.get! k
-- Mathlib.Data.Nat.Squarefree
Nat.squarefree_iff_nodup_primeFactorsList : ∀ {n : ℕ}, n ≠ 0 → (Squarefree n ↔ n.primeFactorsList.Nodup)
-- Batteries.Recycling.RBTree.Alter
/-- Same as `fill` but taking its arguments in a pair for easier composition with `zoom`.  -/
RBTree.RBNode.Path.fill' : {α : Type u_1} → RBTree.RBNode α × RBTree.RBNode.Path α → RBTree.RBNode α
-- Mathlib.Topology.Constructions.SumProd
/-- `X ⊕ Y` is homeomorphic to `Y ⊕ X`.  -/
Homeomorph.sumComm : (X : Type u) → (Y : Type v) → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → X ⊕ Y ≃ₜ Y ⊕ X
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a family of pairwise disjoint finite sets `t i` indexed by a finite type, the product of
`f a` over the union `⋃ i, t i` is equal to the product over all indexes `i` of the products of
`f a` over `a ∈ t i`.  -/
finprod_mem_iUnion : ∀ {α : Type u_1} {ι : Type u_3} {M : Type u_5} [inst : CommMonoid M] {f : α → M} [Finite ι] {t : ι → Set α},
  Pairwise (Function.onFun Disjoint t) →
    (∀ (i : ι), (t i).Finite) → ∏ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.instInhabitedResult.default : Lean.Meta.Sym.DSimp.Result
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabForallParamsWithSignature.delabParams : {α : Type} →
  (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder → Lean.Term → Lean.PrettyPrinter.Delaborator.DelabM α) →
    Lean.NameSet → Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder → Lean.PrettyPrinter.Delaborator.DelabM α
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceAdd : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.RingHom.Finite
RingHom.finite_respectsIso : RingHom.RespectsIso @RingHom.Finite
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_le_zpow_left₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀]
  {n : ℤ}, 0 ≤ n → 0 ≤ a → a ≤ b → a ^ n ≤ b ^ n
-- Mathlib.Algebra.GroupWithZero.Commute
Ring.inverse_pow_mul_eq_iff_eq_mul : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} (b c : M₀),
  IsUnit a → ∀ {k : ℕ}, Ring.inverse a ^ k * b = c ↔ b = a ^ k * c
-- Init.Data.ByteArray.Bootstrap
List.toByteArray.match_1.congr_eq_2 : ∀ (motive : List UInt8 → ByteArray → Sort u_1) (x : List UInt8) (x_1 : ByteArray) (h_1 : (r : ByteArray) → motive [] r)
  (h_2 : (b : UInt8) → (bs : List UInt8) → (r : ByteArray) → motive (b :: bs) r) (b : UInt8) (bs : List UInt8)
  (r : ByteArray),
  x = b :: bs →
    x_1 = r →
      (match x, x_1 with
        | [], r => h_1 r
        | b :: bs, r => h_2 b bs r) ≍
        h_2 b bs r
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.div : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : StarRing R] {x y : R},
  IsSelfAdjoint x → IsSelfAdjoint y → IsSelfAdjoint (x / y)
-- Mathlib.Order.Atoms
/-- A lattice that is a `BoundedOrder` is a distributive lattice.
This is not an instance to prevent loops  -/
IsSimpleOrder.distribLattice : {α : Type u_2} → [inst : Lattice α] → [inst_1 : BoundedOrder α] → [IsSimpleOrder α] → DistribLattice α
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} [inst_3 : Inhabited (β k)], (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k)
-- Init.Data.SInt.Lemmas
Int64.toInt16_mul : ∀ (a b : Int64), (a * b).toInt16 = a.toInt16 * b.toInt16
-- Qq.Macro
/-- `q(t)` quotes the Lean expression `t` into a `Q(α)` (if `t : α`)  -/
Qq.«termQ(__)» : Lean.ParserDescr