mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Internal.Order.Basic
_private.Init.Internal.Order.Basic.0.Lean.Order.flat_csup.eq_1 : ∀ {α : Sort u} {b : α} (c : Lean.Order.FlatOrder b → Prop),
  Lean.Order.flat_csup c = if h : ∃ x, c x ∧ x ≠ b then Classical.choose h else Lean.Order.FlatOrder.mk b b
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.measure_closedBall_div_le_integral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) (μ : MeasureTheory.Measure E) [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsAddHaarMeasure] (K : ℝ),
  f.rOut ≤ K * f.rIn → μ.real (Metric.closedBall c f.rOut) / K ^ Module.finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ
-- Mathlib.Data.Multiset.AddSub
Multiset.add_le_add_iff_right : ∀ {α : Type u_1} {s t u : Multiset α}, s + u ≤ t + u ↔ s ≤ t
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- If two ring homomorphisms are equal on a set, then they are equal on its
`NonUnitalSubring` closure.  -/
NonUnitalRingHom.eqOn_set_closure : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {f g : R →ₙ+* S}
  {s : Set R}, Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(NonUnitalSubring.closure s)
-- Lean.Meta.Tactic.Try.Collect
/-- Unfolding candidates.  -/
Lean.Meta.Try.Collector.Result.unfoldCandidates : Lean.Meta.Try.Collector.Result → Lean.Meta.Try.Collector.OrdSet Lean.Name
-- Init.Data.Rat.Lemmas
Rat.add_left_comm : ∀ (a b c : ℚ), a + (b + c) = b + (a + c)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_isBase_eq : ∀ {α : Type u_1} {M : Matroid α}, M.removeLoops.IsBase = M.IsBase
-- Mathlib.RepresentationTheory.Coinduced
/-- Given a monoid morphism `φ : G →* H` and a morphism of `G`-representations `f : A ⟶ B`, there
is a natural `H`-representation morphism `coind' φ A ⟶ coind' φ B`, given by postcomposition
by `f`.  -/
Rep.coindMap' : {k : Type u} →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            (φ : G →* H) → {A B : Rep.{max u w, u, v} k G} → (A ⟶ B) → (Rep.coind' φ A ⟶ Rep.coind' φ B)
-- Mathlib.Analysis.Complex.Hadamard
/-- A bound to the norm of `f` on the line `z.re = u` induces a bound to the norm of `scale f l u z`
on the line `z.re = 1`.  -/
Complex.HadamardThreeLines.scale_bound_right : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {l u b : ℝ},
  (∀ z ∈ Complex.re ⁻¹' {u}, ‖f z‖ ≤ b) → ∀ z ∈ Complex.re ⁻¹' {1}, ‖Complex.HadamardThreeLines.scale f l u z‖ ≤ b
-- Mathlib.Order.MinMax
min_lt_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, min b c < a ↔ b < a ∨ c < a
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_ite_eq_of_mem' : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M),
  a ∈ s → (∑ x ∈ s, if x = a then b x else 0) = b a
-- Init.Data.Int.Order
Int.lt_of_not_ge : ∀ {a b : ℤ}, ¬a ≤ b → b < a
-- Mathlib.Algebra.Category.MonCat.Limits
/-- If `J` is `u`-small, the forgetful functor from `AddCommMonCat.{u}`
preserves limits of shape `J`.  -/
AddCommMonCat.forget_preservesLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget AddCommMonCat)
-- Mathlib.Analysis.Normed.Module.Dual
NormedSpace.polar_ball : ∀ {𝕜 : Type u_3} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ},
  0 < r → StrongDual.polar 𝕜 (Metric.ball 0 r) = Metric.closedBall 0 r⁻¹
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- `α + β` is short.  -/
RootPairing.EmbeddedG2.shortAddLongRoot_shortRoot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.EmbeddedG2] (B : P.InvariantForm),
  (B.form (RootPairing.EmbeddedG2.shortAddLongRoot P)) (RootPairing.EmbeddedG2.shortAddLongRoot P) =
    (B.form (RootPairing.EmbeddedG2.shortRoot P)) (RootPairing.EmbeddedG2.shortRoot P)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.isAddUnit_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddGroup α] (a : α), IsAddUnit {a}
-- Mathlib.Order.Hom.WithTopBot
OrderIso.withTopCongr_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (e : α ≃o β),
  e.symm.withTopCongr = e.withTopCongr.symm
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.comp_eq_of_monotoneOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {β : Type u_3}
  [inst_2 : LinearOrder β] (f : α → E) {t : Set β} (φ : β → α),
  MonotoneOn φ t →
    ∀ {x y : β}, x ∈ t → y ∈ t → variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.rightInverse_symm : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆ₐ[R] B),
  Function.RightInverse ⇑e.symm ⇑e
-- Mathlib.LinearAlgebra.Pi
LinearMap.proj_apply : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] (i : ι) (b : (i : ι) → φ i), (LinearMap.proj i) b = b i
-- Aesop.Search.ExpandSafePrefix
Aesop.SafeExpansionM.State.mk.inj : ∀ {numRapps numRapps_1 : ℕ}, { numRapps := numRapps } = { numRapps := numRapps_1 } → numRapps = numRapps_1
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.inverseImage_op_underObj : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] (W : CategoryTheory.MorphismProperty T) {X : T},
  W.underObj.op.inverseImage (CategoryTheory.Over.opEquivOpUnder X).functor = W.op.overObj
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.isSpecThmLikeSuffix : Lean.Name → String → Bool
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.alter_eq_empty_iff_erase_eq_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, m.alter k f = ∅ ↔ m.erase k = ∅ ∧ f (m.get? k) = none
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans_assoc : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace Z'] (e : OpenPartialHomeomorph X Y)
  (e' : OpenPartialHomeomorph Y Z) (e'' : OpenPartialHomeomorph Z Z'), (e.trans e').trans e'' = e.trans (e'.trans e'')
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₁_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) {X Y : Fin (1 + 1)}
  (g : X ⟶ Y), (CategoryTheory.ComposableArrows.mk₁ f).map g = CategoryTheory.ComposableArrows.Mk₁.map f X Y ⋯
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicRing.instIsTorsionFreeOfIsDomainOfIsFractionRing : ∀ (n : ℕ) (A : Type u) (K : Type w) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsDomain A]
  [IsFractionRing A K], Module.IsTorsionFree A (CyclotomicRing n A K)
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsBrownianReal.toIsPreBrownianReal : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsBrownianReal._auto_1},
  ProbabilityTheory.IsBrownianReal X P → ProbabilityTheory.IsPreBrownianReal X P
-- Mathlib.Data.NNReal.Defs
NNReal.instCoeReal : Coe NNReal ℝ
-- Mathlib.Data.List.OfFn
/-- Useful if `rw [← map_ofFn]` complains that `g ∘ f` is not the same as `fun i => g (f i)`.  -/
List.ofFn_comp' : ∀ {α : Type u} {β : Type u_1} {n : ℕ} (f : Fin n → α) (g : α → β),
  (List.ofFn fun i => g (f i)) = List.map g (List.ofFn f)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.spanningCoe_induce_eq_self : ∀ {V : Type u_1} (G : SimpleGraph V) (s : Set V), (SimpleGraph.induce s G).spanningCoe = G ↔ G.support ⊆ s
-- Mathlib.Algebra.Category.MonCat.Basic
CategoryTheory.Iso.addMonCatIsoToAddEquiv.eq_1 : ∀ {X Y : AddMonCat} (i : X ≅ Y),
  i.addMonCatIsoToAddEquiv = (AddMonCat.Hom.hom i.hom).toAddEquiv (AddMonCat.Hom.hom i.inv) ⋯ ⋯
-- Mathlib.Order.Filter.Pointwise
Filter.frequently_inv_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter β} {a : α} {p : β → Prop},
  (∃ᶠ (y : β) in a • f, p y) ↔ ∃ᶠ (x : β) in f, p (a • x)
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.cons.sizeOf_spec : ∀ {V : Type u} [inst : Quiver V] {a : V} [inst_1 : SizeOf V] {b c : V} (a_1 : Quiver.Path a b) (a_2 : b ⟶ c),
  sizeOf (a_1.cons a_2) = 1 + sizeOf b + sizeOf c + sizeOf a_1 + sizeOf a_2
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.eq_1 : ∀ {α : Type u_1} (M : Matroid α) (e : α), M.IsLoop e = (e ∈ M.loops)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.ofReal_cpow_of_nonpos : ∀ {x : ℝ}, x ≤ 0 → ∀ (y : ℂ), ↑x ^ y = (-↑x) ^ y * Complex.exp (↑Real.pi * Complex.I * y)
-- Mathlib.Order.Interval.Set.Pi
Set.pi_univ_Icc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x y : (i : ι) → α i),
  (Set.univ.pi fun i => Set.Icc (x i) (y i)) = Set.Icc x y
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.List.Sublist.filter_mono : ∀ {α : Type u} {l : List α} {P Q : α → Bool},
  (∀ (a : α), P a = true → Q a = true) → (List.filter P l).Sublist (List.filter Q l)
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordSeparatingSet_comm : ∀ {α : Type u_1} [inst : LinearOrder α] (s t : Set α), s.ordSeparatingSet t = t.ordSeparatingSet s
-- Mathlib.Analysis.Calculus.Implicit
/-- Derivative of the right function  -/
ImplicitFunctionData.rightDeriv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : CompleteSpace F] →
                    {G : Type u_4} →
                      [inst_7 : NormedAddCommGroup G] →
                        [inst_8 : NormedSpace 𝕜 G] →
                          [inst_9 : CompleteSpace G] → ImplicitFunctionData 𝕜 E F G → E →L[𝕜] G
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_apply : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  (i j : n), M.charmatrix i j = Matrix.diagonal (fun x => Polynomial.X) i j - Polynomial.C (M i j)
-- Init.Data.Vector.FinRange
Vector.finRange_succ_last : ∀ {n : ℕ}, Vector.finRange (n + 1) = Vector.map Fin.castSucc (Vector.finRange n) ++ #v[Fin.last n]
-- Mathlib.Order.Filter.Basic
Filter.Iic_principal : ∀ {α : Type u} (s : Set α), Set.Iic (Filter.principal s) = {l | s ∈ l}
-- Init.Data.Vector.Lemmas
Vector.singleton_def : ∀ {α : Type u_1} {v : α}, Vector.singleton v = #v[v]
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If M is the midpoint of the segment AB and C is the same distance from A as it is from B
then ∠CMB = π / 2.  -/
EuclideanGeometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq : ∀ {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},
  dist p₃ p₁ = dist p₃ p₂ → EuclideanGeometry.angle p₃ (midpoint ℝ p₁ p₂) p₂ = Real.pi / 2
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
/-- If a function has a non-zero strict derivative at all points, then it is an open map.  -/
isOpenMap_of_hasStrictDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {f f' : 𝕜 → 𝕜},
  (∀ (x : 𝕜), HasStrictDerivAt f (f' x) x) → (∀ (x : 𝕜), f' x ≠ 0) → IsOpenMap f
-- Aesop.Forward.State
Aesop.RawHyp.fvarId.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Aesop.RawHyp.fvarId fvarId) = 1 + sizeOf fvarId
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The subobject of `𝒞.Ω` corresponding to the `truth` morphism.  -/
CategoryTheory.Subobject.Classifier.truth_as_subobject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (𝒞 : CategoryTheory.Subobject.Classifier C) → CategoryTheory.Subobject 𝒞.Ω
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.Simps.coe.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : UpperSet α), UpperSet.Simps.coe s = ↑s
-- Init.System.IOError
IO.Error.noFileOrDirectory.inj : ∀ {filename : String} {osCode : UInt32} {details filename_1 : String} {osCode_1 : UInt32} {details_1 : String},
  IO.Error.noFileOrDirectory filename osCode details = IO.Error.noFileOrDirectory filename_1 osCode_1 details_1 →
    filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- The homotopy category of fibrant objects.  -/
HomotopicalAlgebra.FibrantObject.HoCat : (C : Type u_1) → [inst : CategoryTheory.Category.{v_1, u_1} C] → [HomotopicalAlgebra.ModelCategory C] → Type u_1
-- Mathlib.Data.Analysis.Filter
/-- Construct a realizer for the product of filters  -/
Filter.Realizer.prod : {α : Type u_1} → {f g : Filter α} → f.Realizer → g.Realizer → (f ×ˢ g).Realizer
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyGE_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h' : ∃ a ∈ t₁, (cmp a k).isGE = true} (h : t₁.Equiv t₂), t₁.getKeyGE k h' = t₂.getKeyGE k ⋯
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.sorrySource : Lean.Option Bool
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.IsCorepresentable.has_corepresentation : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {F : CategoryTheory.Functor C (Type v)}
  [self : F.IsCorepresentable], ∃ X, Nonempty (F.CorepresentableBy X)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.min_eq_left_of_lt : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {p q : (a : α) × β a}, compare p.fst q.fst = Ordering.lt → p ⊓ q = p
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- Restrict a non-unital star algebra homomorphism with a left inverse to an algebra isomorphism
to its range.

This is a computable alternative to `StarAlgEquiv.ofInjective`.  -/
StarAlgEquiv.ofLeftInverse' : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalSemiring B] →
                  [inst_5 : Module R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] →
                        [inst_8 : NonUnitalAlgHomClass F R A B] →
                          [inst_9 : StarHomClass F A B] →
                            {g : B → A} → {f : F} → Function.LeftInverse g ⇑f → A ≃⋆ₐ[R] ↥(NonUnitalStarAlgHom.range f)
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.castSucc_mem_finset_iff : ∀ {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) (i : Fin (n + 1)),
  i.castSucc ∈ SimplexCategory.II.finset f x ↔ x ≤ (f i).castSucc
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Comma.costructuredArrowSndInclusion_obj_left_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)),
  ((CategoryTheory.Comma.costructuredArrowSndInclusion L R b).obj X).left.left = X.left
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.intCastFn? : Lean.Meta.Sym.Arith.Ring → Option Lean.Expr
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residue_descResidueField : ∀ {K : Type u} [inst : Field K] {X : AlgebraicGeometry.Scheme} {x : ↥X} (f : X.presheaf.stalk x ⟶ CommRingCat.of K)
  [inst_1 : IsLocalHom (CommRingCat.Hom.hom f)],
  CategoryTheory.CategoryStruct.comp (X.residue x) (AlgebraicGeometry.Scheme.descResidueField f) = f
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instStarModule : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [StarModule R A], StarModule R (Unitization R A)
-- Mathlib.CategoryTheory.Preadditive.Schur
/-- Endomorphisms of a simple object form a field if they are finite dimensional.
This can't be an instance as `𝕜` would be undetermined.
 -/
CategoryTheory.fieldEndOfFiniteDimensional : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (𝕜 : Type u_2) →
        [inst_2 : Field 𝕜] →
          [IsAlgClosed 𝕜] →
            [inst_4 : CategoryTheory.Linear 𝕜 C] →
              [CategoryTheory.Limits.HasKernels C] →
                (X : C) → [CategoryTheory.Simple X] → [I : FiniteDimensional 𝕜 (X ⟶ X)] → Field (CategoryTheory.End X)
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.mcast_eq_zero_iff : ∀ {a b : ℤ} {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (hΓ : Γ' = Γ) (f : ModularForm Γ a),
  ModularForm.mcast h f hΓ = 0 ↔ f = 0
-- Init.Data.BitVec.Bitblast
/-- Shifts `x` arithmetically (signed) to the right by the first `n` bits of `y`.

The theorem `BitVec.sshiftRight_eq_sshiftRightRec` proves the equivalence of `(x.sshiftRight y)` and
`BitVec.sshiftRightRec x y`. Together with equations `BitVec.sshiftRightRec_zero`, and
`BitVec.sshiftRightRec_succ`, this allows `BitVec.sshiftRight` to be unfolded into a circuit for
bit blasting.
 -/
BitVec.sshiftRightRec : {w₁ w₂ : ℕ} → BitVec w₁ → BitVec w₂ → ℕ → BitVec w₁
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instInsertSigma : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Insert ((a : α) × β a) (Std.DTreeMap α β cmp)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.instPartialOrder : {α : Type u_1} → PartialOrder (MeasurableSpace α)
-- Mathlib.Analysis.Normed.Module.Span
/-- Given a nonzero element `x` of a normed space `E₁` over a field `𝕜`, the natural
continuous linear equivalence from `𝕜` to the span of `x`.  -/
ContinuousLinearEquiv.toSpanNonzeroSingleton : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : NormedField 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → (x : E) → x ≠ 0 → 𝕜 ≃L[𝕜] ↥(𝕜 ∙ x)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coeFn_injective : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2], Function.Injective DFunLike.coe
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.sign_of_cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (f : Equiv.Perm α),
  Equiv.Perm.sign f = (-1) ^ (f.cycleType.sum + f.cycleType.card)
-- Mathlib.Order.Filter.Map
Filter.gc_comap_kernMap : ∀ {α : Type u_1} {β : Type u_2} (m : α → β), GaloisConnection (Filter.comap m) (Filter.kernMap m)
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.snd_apply_coe : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀] (x : G₀ˣ × H₀ˣ),
  (MonoidWithZeroHom.snd G₀ H₀) ↑x = ↑x.2
-- Mathlib.Topology.Category.LightProfinite.Basic
instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone : ∀ (S : LightDiagram), SecondCountableTopology ↑S.cone.pt.toTop
-- Lean.Level
Lean.PersistentLevelSet : Type
-- Lean.Parser.Do
Lean.Parser.Term.doFinally.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
MeasureTheory.measure_lt_one_eq_integral_div_gamma : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [FiniteDimensional ℝ E] [mE : MeasurableSpace E]
  [tE : TopologicalSpace E] [IsTopologicalAddGroup E] [BorelSpace E] [T2Space E] [ContinuousSMul ℝ E]
  (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {g : E → ℝ},
  g 0 = 0 →
    (∀ (x : E), g (-x) = g x) →
      (∀ (x y : E), g (x + y) ≤ g x + g y) →
        (∀ {x : E}, g x = 0 → x = 0) →
          (∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x) →
            ∀ {p : ℝ},
              0 < p →
                μ {x | g x < 1} =
                  ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p) ∂μ) / Real.Gamma (↑(Module.finrank ℝ E) / p + 1))
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.filterMap.match_1.splitter : {α : Type u_1} →
  {γ : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl.BalancedTree α γ → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl.BalancedTree α γ) →
        ((r' : Std.DTreeMap.Internal.Impl α γ) → (hr' : r'.Balanced) → motive { impl := r', balanced_impl := hr' }) →
          motive x
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_map_apply : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : R),
  Polynomial.eval (f x) (Polynomial.map f p) = f (Polynomial.eval x p)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- For any `c : F`, given `a ≠ 0` and `a² ≠ 1`, the transvection `transvection i₁ i₂ hij c` is
a commutator in `SL ι F`, hence lies in `commutator (SL ι F)`.  -/
Matrix.transvection_mem_commutator₀ : ∀ {F : Type u_1} [inst : Field F] {a : F},
  a ≠ 0 →
    a ^ 2 ≠ 1 → ∀ (c : F), Matrix.SpecialLinearGroup.transvection ⋯ c ∈ commutator (Matrix.SpecialLinearGroup (Fin 2) F)
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Presieve.FactorsThruAlong.pullbackArrows : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) (R : CategoryTheory.Presieve Y)
  [inst_1 : R.HasPullbacks f], (CategoryTheory.Presieve.pullbackArrows f R).FactorsThruAlong R f
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.instDecidableEval : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] →
      (p : α → Bool) → (c : β) → Decidable (Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c)
-- Mathlib.NumberTheory.RamificationInertia.Galois
/-- If `L / K` is a Galois extension, it can be seen from
the theorem `Ideal.inertiaDeg_eq_of_isGaloisGroup` that all `Ideal.inertiaDeg` over a fixed
maximal ideal `p` of `A` are the same, which we define as `Ideal.inertiaDegIn`.  -/
Ideal.inertiaDegIn : {A : Type u_1} → [inst : CommRing A] → Ideal A → (B : Type u_2) → [inst_1 : CommRing B] → [Algebra A B] → ℕ
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.sup.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (𝒮 : Set (CategoryTheory.Sieve X)),
  CategoryTheory.Sieve.sup 𝒮 = { arrows := fun x f => ∃ S ∈ 𝒮, S.arrows f, downward_closed := ⋯ }
-- Mathlib.CategoryTheory.Limits.Cones
/-- Whisker a cone by precomposition of a functor.  -/
CategoryTheory.Limits.Cone.whisker : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              (E : CategoryTheory.Functor K J) → CategoryTheory.Limits.Cone F → CategoryTheory.Limits.Cone (E.comp F)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.fvar.sizeOf_spec : ∀ (fvarId : Lean.FVarId) (nargs : ℕ),
  sizeOf (Lean.Meta.RefinedDiscrTree.Key.fvar fvarId nargs) = 1 + sizeOf fvarId + sizeOf nargs
-- Mathlib.Analysis.Complex.Convex
convex_halfSpace_im_lt : ∀ (r : ℝ), Convex ℝ {c | c.im < r}
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pattern.Model.BackwardSliceSearcher.instLawfulBackwardPatternModel : ∀ {pat : String.Slice}, String.Slice.Pattern.Model.LawfulBackwardPatternModel pat