mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.UInt.Bitwise
USize.ofNatLT_shiftLeft : ∀ {a b : ℕ} (ha : a <<< b < USize.size) (hb : b < System.Platform.numBits),
  USize.ofNatLT (a <<< b) ha = USize.ofNatLT a ⋯ <<< USize.ofNatLT b ⋯
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.toPartialEquivOfImageEq.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (e e_1 : α ≃ β) (e_e : e = e_1) (s s_1 : Set α) (e_s : s = s_1) (t t_1 : Set β)
  (e_t : t = t_1) (h : ⇑e '' s = t), e.toPartialEquivOfImageEq s t h = e_1.toPartialEquivOfImageEq s_1 t_1 ⋯
-- Mathlib.MeasureTheory.Integral.Prod
/-- The Bochner integral is measurable. This shows that the integrand of (the right-hand-side of)
Fubini's theorem is measurable.
This version has `f` in curried form.  -/
MeasureTheory.StronglyMeasurable.integral_prod_right : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [MeasureTheory.SFinite ν]
  ⦃f : α → β → E⦄,
  MeasureTheory.StronglyMeasurable (Function.uncurry f) → MeasureTheory.StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν
-- Mathlib.Order.Filter.CountablyGenerated
/-- If `f` is countably generated and `f.HasBasis p s`, then `f` admits a decreasing basis
enumerated by natural numbers such that all sets have the form `s i`. More precisely, there is a
sequence `i n` such that `p (i n)` for all `n` and `s (i n)` is a decreasing sequence of sets which
forms a basis of `f`.  -/
Filter.HasBasis.exists_antitone_subbasis : ∀ {α : Type u_1} {ι' : Sort u_5} {f : Filter α} [h : f.IsCountablyGenerated] {p : ι' → Prop} {s : ι' → Set α},
  f.HasBasis p s → ∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)
-- Mathlib.Algebra.IsPrimePow
IsPrimePow.ne_one : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : R}, IsPrimePow n → n ≠ 1
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.lt_length' : ∀ {n : ℕ} (c : CompositionAsSet n) (i : Fin c.length), ↑i < c.boundaries.card
-- Mathlib.RingTheory.Localization.Integral
/-- If the field `L` is an algebraic extension of the integral domain `A`,
the integral closure of `A` in `L` has fraction field `L`.  -/
integralClosure.isFractionRing_of_algebraic : ∀ {A : Type u_3} [inst : CommRing A] {L : Type u_5} [inst_1 : Field L] [inst_2 : Algebra A L] [Algebra.IsAlgebraic A L],
  (∀ (x : A), (algebraMap A L) x = 0 → x = 0) → IsFractionRing (↥(integralClosure A L)) L
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_nonneg : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {a : A}
  {x : NNReal}, 0 ≤ a ^ x
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instCommRing : {R : Type u_1} → [CommRing R] → CommRing Rᵐᵒᵖ
-- Std.Data.HashMap.Lemmas
Std.HashMap.get_union_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (contains_right : k ∈ m₂), (m₁ ∪ m₂).get k ⋯ = m₂.get k contains_right
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.commAlgEquiv.eq_1 : ∀ (R : Type u_2) (S₁ : Type u_3) (S₂ : Type u_4) [inst : CommSemiring R],
  MvPolynomial.commAlgEquiv R S₁ S₂ = AddMonoidAlgebra.commAlgEquiv R
-- Init.Prelude
/-- Creates an info-less node of the given kind and children.  -/
Lean.mkNode : (k : Lean.SyntaxNodeKind) → Array Lean.Syntax → Lean.TSyntax k
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- The unit of the multiplication is `single 1 1`, i.e. the function that is `1` at `1` and
zero elsewhere.  -/
SkewMonoidAlgebra.instOne : {k : Type u_1} → {G : Type u_2} → [One G] → [inst : AddMonoidWithOne k] → One (SkewMonoidAlgebra k G)
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.gen.eq_1 : ∀ {α : Type u} [inst : UniformSpace α] (s : SetRel α α), CauchyFilter.gen s = {p | s ∈ ↑p.1 ×ˢ ↑p.2}
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {x y : F.Elements}
  {f g : x ⟶ y}, f = g ↔ ↑f = ↑g
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_nsmul : ∀ {x : ℝ} {n : ℕ}, ENNReal.ofReal (n • x) = n • ENNReal.ofReal x
-- Mathlib.Data.List.Basic
List.bind_eq_flatMap : ∀ {α β : Type u_2} (f : α → List β) (l : List α), l >>= f = List.flatMap f l
-- Std.Sat.AIG.Lemmas
/-- The AIG produced by `AIG.mkAtom` agrees with the input AIG on all indices that are valid for both.
 -/
Std.Sat.AIG.mkAtom_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (var : α) (idx : ℕ)
  {h : idx < aig.decls.size} {hbound : idx < (aig.mkAtom var).aig.decls.size},
  (aig.mkAtom var).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
CochainComplex.isIso_homologyπ₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℕ) [inst_2 : HomologicalComplex.HasHomology K 0],
  CategoryTheory.IsIso (HomologicalComplex.homologyπ K 0)
-- Lean.Message
/-- Wrap the given message in `l` and `r`. See also `Format.bracket`.   -/
Lean.MessageData.bracket : String → Lean.MessageData → String → Lean.MessageData
-- Mathlib.Data.Set.Basic
Set.union_def : ∀ {α : Type u} {s₁ s₂ : Set α}, s₁ ∪ s₂ = {a | a ∈ s₁ ∨ a ∈ s₂}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.isUnit_Δ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsElliptic], IsUnit W.Δ
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.isRoot_of_aeval_algebraMap_eq_zero : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] [FaithfulSMul R S]
  {p : Polynomial R} {r : R}, (Polynomial.aeval ((algebraMap R S) r)) p = 0 → p.IsRoot r
-- Init.Data.BitVec.Bitblast
BitVec.getMsbD_sub : ∀ {w i : ℕ} {i_lt : i < w} {x y : BitVec w},
  (x - y).getMsbD i = (x.getMsbD i ^^ ((~~~y + 1).getMsbD i ^^ BitVec.carry (w - 1 - i) x (~~~y + 1) false))
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- If `f` only depends on the variables uo to rank `a`, integrating beyond rank `a` is the same
as integrating up to rank `a`.  -/
DependsOn.lmarginalPartialTraj_const_right : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a b c : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {d : ℕ} {f : ((n : ℕ) → X n) → ENNReal},
  Measurable f →
    DependsOn f ↑(Finset.Iic a) →
      a ≤ c →
        a ≤ d →
          ProbabilityTheory.Kernel.lmarginalPartialTraj κ b c f = ProbabilityTheory.Kernel.lmarginalPartialTraj κ b d f
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : SeminormedAddGroup E] {f : ℕ → α → E},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    ∀ (f_lim : α → E),
      (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) →
        MeasureTheory.eLpNorm f_lim p μ ≤ Filter.liminf (fun n => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Show that `G` preserves left Kan extensions if it maps some left Kan extension to a left
Kan extension, phrased in terms of `IsUniversal`.  -/
CategoryTheory.Functor.PreservesLeftKanExtension.mk_of_preserves_isUniversal : ∀ {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.LeftExtension F) (hE : CategoryTheory.StructuredArrow.IsUniversal E),
  Nonempty
      (CategoryTheory.StructuredArrow.IsUniversal ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj E)) →
    G.PreservesLeftKanExtension F L
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp : ∀ {R : Type u_4} {E : Type u_6} {V₁ : Type u_8} {V₂ : Type u_9} {V₃ : Type u_10} [inst : LineDeriv E V₁ V₂]
  [inst_1 : LineDeriv E V₂ V₃] [inst_2 : AddCommGroup V₁] [inst_3 : AddCommGroup V₂] [inst_4 : AddCommGroup V₃]
  [inst_5 : CommRing R] [inst_6 : AddCommGroup E] [inst_7 : Module R E] [inst_8 : Module R V₂] [inst_9 : Module R V₃]
  [inst_10 : LineDerivAdd E V₂ V₃] [inst_11 : LineDerivAdd E V₁ V₂] [inst_12 : LineDerivSMul R E V₂ V₃]
  [inst_13 : LineDerivLeftSMul R E V₁ V₂] [inst_14 : LineDerivLeftSMul R E V₂ V₃] (f : V₁) (v w : E),
  (LineDeriv.tensorLineDerivTwo R f) (v ⊗ₜ[R] w) = LineDeriv.lineDerivOp v (LineDeriv.lineDerivOp w f)
-- Lean.Meta.Sym.AbstractS
/-- Abstracts free variables `xs` in expression `e`, converting them to de Bruijn indices.

It is an abbreviation for `abstractFVarsRange e 0 xs`.
 -/
Lean.Meta.Sym.abstractFVars : Lean.Expr → Array Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.eraseManyEntries.eq_1 : ∀ {α : Type u} {β : α → Type v} {ρ : Type w} [inst : ForIn Id ρ ((a : α) × β a)] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (l : ρ),
  m.eraseManyEntries l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, snd⟩ =>
              have r := ⟨(↑r).erase a, ⋯⟩;
              pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : Std.DHashMap.Internal.Raw₀ α β → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α β} {a : α}, P m'' → P (m''.erase a)) → P m → P m' } :=
        __s
      pure r).run
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- A function `f` maps upwards closed sets (atTop sets) to upwards closed sets when it is a
Galois insertion. The Galois "insertion" and "connection" is weakened to only require it to be an
insertion and a connection above `b`.  -/
Filter.map_atTop_eq_of_gc : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] [inst_2 : PartialOrder β] [IsDirectedOrder β]
  {f : α → β} (g : β → α) (b : β),
  Monotone f →
    (∀ (a : α) (c : β), b ≤ c → (f a ≤ c ↔ a ≤ g c)) →
      (∀ (c : β), b ≤ c → c ≤ f (g c)) → Filter.map f Filter.atTop = Filter.atTop
-- Mathlib.Order.BooleanAlgebra.Basic
GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra : {α : Type u} → [GeneralizedBooleanAlgebra α] → GeneralizedCoheytingAlgebra α
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.balanceₘ.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.size > Std.DTreeMap.Internal.delta * l.size → Sort u_3)
  (h : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * l.size)
  (h_1 :
    (h : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * l.size) →
      motive Std.DTreeMap.Internal.Impl.leaf h)
  (h_2 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rl rr : Std.DTreeMap.Internal.Impl α β) →
            (h : (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size > Std.DTreeMap.Internal.delta * l.size) →
              motive (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr) h),
  (match Std.DTreeMap.Internal.Impl.leaf, h with
    | Std.DTreeMap.Internal.Impl.leaf, h => h_1 h
    | Std.DTreeMap.Internal.Impl.inner size rk rv rl rr, h => h_2 size rk rv rl rr h) =
    h_1 h
-- Mathlib.Data.Finset.Image
Finset.map_eq_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α}, Finset.map f s = ∅ ↔ s = ∅
-- Mathlib.Analysis.Calculus.Taylor
/-- Calculate the derivative of the Taylor polynomial with respect to `x`.  -/
hasDerivAt_taylorWithinEval_succ : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x₀ x : ℝ} {s : Set ℝ} (f : ℝ → E) (n : ℕ),
  HasDerivAt (taylorWithinEval f (n + 1) s x₀) (taylorWithinEval (derivWithin f s) n s x₀ x) x
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- A uniform upper bound for `jacobiTheta₂'_term` on compact subsets.  -/
norm_jacobiTheta₂'_term_le : ∀ {S T : ℝ},
  0 < T →
    ∀ {z τ : ℂ},
      |z.im| ≤ S →
        T ≤ τ.im →
          ∀ (n : ℤ), ‖jacobiTheta₂'_term n z τ‖ ≤ 2 * Real.pi * ↑|n| * Real.exp (-Real.pi * (T * ↑n ^ 2 - 2 * S * ↑|n|))
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.match_1.congr_eq_3 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (x : Lean.Grind.Linarith.Expr)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a)) (k : ℤ)
  (a : Lean.Grind.Linarith.Expr),
  x = Lean.Grind.Linarith.Expr.intMul k a →
    (match x with
      | a.sub b => h_1 a b
      | a.neg => h_2 a
      | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
      | Lean.Grind.Linarith.Expr.zero => h_4 ()
      | Lean.Grind.Linarith.Expr.var v => h_5 v
      | a.add b => h_6 a b
      | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) ≍
      h_3 k a
-- Mathlib.Order.Preorder.Chain
IsChain.directedOn : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Refl r], IsChain r s → DirectedOn r s
-- Mathlib.Topology.Connected.LocallyConnected
locallyConnectedSpace_iff_subsets_isOpen_isConnected : ∀ {α : Type u} [inst : TopologicalSpace α],
  LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ nhds x, ∃ V ⊆ U, IsOpen V ∧ x ∈ V ∧ IsConnected V
-- Mathlib.GroupTheory.GroupAction.Hom
DistriMulActionHom.zero_apply : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_11}
  [inst_2 : AddMonoid A] [inst_3 : DistribMulAction M A] {B : Type u_12} [inst_4 : AddMonoid B]
  [inst_5 : DistribMulAction N B] (a : A), 0 a = 0
-- Mathlib.Analysis.InnerProductSpace.NormDet
/-- `LinearMap.normDet` is well-defined under any pair of orthonormal basis.
 -/
LinearMap.normDet_eq_norm_det_toMatrix_rangeRestrict : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] {ι : Type u_5} [inst_6 : Fintype ι] [inst_7 : DecidableEq ι] (f : U →ₗ[𝕜] V)
  (bu : OrthonormalBasis ι 𝕜 U) (bv : OrthonormalBasis ι 𝕜 ↥f.range),
  f.normDet = ‖((LinearMap.toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instMulOneClass : MulOneClass ℕ
-- Mathlib.Data.Finset.Sups
Finset.diffs_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s₁ s₂ t₁ t₂ : Finset α},
  s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁.diffs t₁ ⊆ s₂.diffs t₂
-- Mathlib.RingTheory.Filtration
Ideal.iInf_pow_smul_eq_bot_of_le_jacobson : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  [IsNoetherianRing R] [Module.Finite R M], I ≤ ⊥.jacobson → ⨅ i, I ^ i • ⊤ = ⊥
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
_private.Mathlib.LinearAlgebra.Matrix.FixedDetMatrices.0.FixedDetMatrices.A_d_ne_zero : ∀ {m : ℤ} {A : FixedDetMatrix (Fin 2) ℤ m}, ↑A 1 0 = 0 → m ≠ 0 → ↑A 1 1 ≠ 0
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.presheafFiber_hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ : J.Point}
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {T : A}
  {f g : Φ.presheafFiber.obj P ⟶ T},
  f = g ↔
    ∀ (X : C) (x : Φ.fiber.obj X),
      CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) f =
        CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) g
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The adjunction associated to a functor known to be a right adjoint.  -/
CategoryTheory.Adjunction.ofIsRightAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (right : CategoryTheory.Functor C D) → [inst_2 : right.IsRightAdjoint] → right.leftAdjoint ⊣ right
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0)
  (hg₂ : S₂.g = 0), (CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φQ = φ.τ₂
-- Mathlib.RingTheory.KrullDimension.Regular
ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] {x : R},
  IsSMulRegular R x → x ∈ IsLocalRing.maximalIdeal R → ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R
-- Mathlib.Topology.Separation.Hausdorff
Pi.isCompact_closure_iff : ∀ {ι : Type u_4} {X : ι → Type u_5} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), R1Space (X i)]
  {s : Set ((i : ι) → X i)}, IsCompact (closure s) ↔ ∀ (i : ι), IsCompact (closure (Function.eval i '' s))
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
instIsBotZeroClass : ∀ {α : Type u} [inst : AddZeroClass α] [inst_1 : LE α] [CanonicallyOrderedAdd α], IsBotZeroClass α
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableSpace.comap_compl : ∀ {α : Type u_1} {β : Type u_2} {m' : MeasurableSpace β} [inst : BooleanAlgebra β],
  Measurable compl →
    ∀ (f : α → β), MeasurableSpace.comap (fun a => (f a)ᶜ) inferInstance = MeasurableSpace.comap f inferInstance
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
CliffordAlgebra.ofProd_ι_mk : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (Q₁ : QuadraticForm R M₁)
  (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂),
  (CliffordAlgebra.ofProd Q₁ Q₂) ((CliffordAlgebra.ι (QuadraticMap.prod Q₁ Q₂)) (m₁, m₂)) =
    (CliffordAlgebra.ι Q₁) m₁ ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (CliffordAlgebra.ι Q₂) m₂
-- Mathlib.Algebra.Notation.Defs
dite_add_dite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Add α] (a : P → α) (b : ¬P → α) (c : P → α) (d : ¬P → α),
  ((if h : P then a h else b h) + if h : P then c h else d h) = if h : P then a h + c h else b h + d h
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_id_obj' : ∀ {X : TopCat} (U : Set ↑X) (p : IsOpen U),
  (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X)).obj { carrier := U, is_open' := p } =
    { carrier := U, is_open' := p }
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.sieveOfUliftSubfunctor_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))}
  (f : R ⟶ CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X) (Y : C) (g : Y ⟶ X),
  (CategoryTheory.Sieve.sieveOfUliftSubfunctor f).arrows g =
    ∃ t, (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op Y))) t = { down := g }
-- Lean.Meta.Tactic.Grind.Main
/-- Walks the proof term collecting `Origin`s of E-matching instances that appear,
using the `mdata` markers placed by `markTheoremInstanceProof`.
 -/
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.collectUsedOrigins : Lean.Expr → Lean.Meta.Grind.EMatch.InstanceMap → Std.HashSet Lean.Meta.Grind.Origin
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The map from the third isomorphism theorem for groups: `(G / N) / (M / N) → G / M`.  -/
QuotientGroup.quotientQuotientEquivQuotientAux : {G : Type u} →
  [inst : Group G] →
    (N : Subgroup G) →
      [nN : N.Normal] →
        (M : Subgroup G) → [nM : M.Normal] → N ≤ M → (G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M →* G ⧸ M
-- Std.Http.Data.Request
/-- The raw request-target string (commonly origin-form path/query, `"*"`, or authority-form).
 -/
Std.Http.Request.Head.uri : Std.Http.Request.Head → Std.Http.RequestTarget
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.faceOppositeCentroid_map : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [CharZero k] {V₂ : Type u_4} {P₂ : Type u_5} [inst_5 : AddCommGroup V₂]
  [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] {n : ℕ} [inst_8 : NeZero n] (s : Affine.Simplex k P n)
  (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) {i : Fin (n + 1)},
  (s.map f hf).faceOppositeCentroid i = f (s.faceOppositeCentroid i)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
/-- The integral representation of the function `x ↦ x ^ p` (where `p ∈ (0, 1)`).  -/
CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ : ∀ (A : Type u_1) [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : SMulCommClass ℝ A A] [inst_4 : IsScalarTower ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [CompleteSpace A] {p : NNReal},
  p ∈ Set.Ioo 0 1 →
    ∃ μ,
      ∀ a ∈ Set.Ici 0,
        MeasureTheory.IntegrableOn (fun t => cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Set.Ioi 0) μ ∧
          a ^ p = ∫ (t : ℝ) in Set.Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ
-- Init.Data.String.Decode
UInt8.utf8ByteSize.eq_def : ∀ (c : UInt8) (_h : c.IsUTF8FirstByte),
  c.utf8ByteSize _h = if c &&& 128 = 0 then 1 else if c &&& 224 = 192 then 2 else if c &&& 240 = 224 then 3 else 4
-- Mathlib.CategoryTheory.Action.Continuous
/-- The subcategory of `ContAction V G` where the topology is discrete.  -/
DiscreteContAction : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [CategoryTheory.HasForget₂ V TopCat] →
              (G : Type u_4) → [Monoid G] → [TopologicalSpace G] → Type (max (max u_1 u_4) v_1)
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.one_sub : ∀ {R : Type u_1} {p : R} [inst : NonAssocRing R] [inst_1 : StarRing R], IsStarProjection p → IsStarProjection (1 - p)
-- Lean.Syntax
Lean.Syntax.Traverser.parents : Lean.Syntax.Traverser → Array Lean.Syntax
-- Lean.Compiler.LCNF.Basic
/-- Projecting USize scalars out of a value.
 -/
Lean.Compiler.LCNF.LetValue.uproj : {pu : Lean.Compiler.LCNF.Purity} →
  ℕ →
    Lean.FVarId →
      autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_9 →
        Lean.Compiler.LCNF.LetValue pu
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmullerFun_eq_teichmuller₀ : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R], Perfection.teichmullerFun = ⇑(Perfection.teichmuller₀ p I)
-- Std.Http.Data.Chunk
Std.Http.Chunk.ExtensionValue.mk : (value : String) →
  autoParam (Std.Http.Chunk.IsValidExtensionValue value)
      Std.Http.Chunk.ExtensionValue.isValidExtensionValue._autoParam →
    Std.Http.Chunk.ExtensionValue