mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.isStrong_hurwitzOddFEPair : ∀ (a : UnitAddCircle), IsStrongFEPair (HurwitzZeta.hurwitzOddFEPair a)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CtorInfo.mk.inj : ∀ {name : Lean.Name} {cidx size usize ssize : ℕ} {name_1 : Lean.Name} {cidx_1 size_1 usize_1 ssize_1 : ℕ},
  { name := name, cidx := cidx, size := size, usize := usize, ssize := ssize } =
      { name := name_1, cidx := cidx_1, size := size_1, usize := usize_1, ssize := ssize_1 } →
    name = name_1 ∧ cidx = cidx_1 ∧ size = size_1 ∧ usize = usize_1 ∧ ssize = ssize_1
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.Hom.toLieHom : {R : Type u_1} →
  {A₁ : Type u_2} →
    {A₂ : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : CommRing A₁] →
          [inst_2 : CommRing A₂] →
            [inst_3 : Algebra R A₁] →
              [inst_4 : Algebra R A₂] →
                {σ : A₁ →ₐ[R] A₂} →
                  {L₁ : Type u_8} →
                    {L₂ : Type u_9} →
                      [inst_5 : LieRing L₁] →
                        [inst_6 : Module A₁ L₁] →
                          [inst_7 : LieRingModule L₁ A₁] →
                            [inst_8 : LieAlgebra R L₁] →
                              [inst_9 : LieRing L₂] →
                                [inst_10 : Module A₂ L₂] →
                                  [inst_11 : LieRingModule L₂ A₂] →
                                    [inst_12 : LieAlgebra R L₂] → LieRinehartAlgebra.Hom σ L₁ L₂ → L₁ →ₗ⁅R⁆ L₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqMon.beq.eq_def : ∀ (x x_1 : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.instBEqMon.beq x x_1 =
    match x, x_1 with
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => true
    | Lean.Grind.CommRing.Mon.mult a a_1, Lean.Grind.CommRing.Mon.mult b b_1 =>
      a == b && Lean.Grind.CommRing.instBEqMon.beq a_1 b_1
    | x, x_2 => false
-- Mathlib.NumberTheory.FactorisationProperties
Nat.not_abundant_zero : ¬Nat.Abundant 0
-- Mathlib.Analysis.Normed.Group.Rat
Int.norm_cast_rat : ∀ (m : ℤ), ‖↑m‖ = ‖m‖
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_zero' : ∀ {α : Type u_1} (M : Type u_3) [inst : Zero M] {s : Set α}, s.indicator 0 = 0
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
UniqueDiffOn.eq_1 : ∀ (R : Type u) {E : Type v} [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : TopologicalSpace E] (s : Set E), UniqueDiffOn R s = ∀ x ∈ s, UniqueDiffWithinAt R s x
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.NatTrans.CommShift F.mapDerivedCategoryFactors.hom ℤ
-- Mathlib.Analysis.Normed.Module.WeakDual
WeakDual.re_extendRCLikeL_apply_apply : ∀ {𝕜 : Type u_5} {F : Type u_7} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (f : WeakDual ℝ F) (x : F), RCLike.re ((WeakDual.extendRCLikeL f) x) = f x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.shift_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ₁ γ₂ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ),
  (γ₁ + γ₂).shift a = γ₁.shift a + γ₂.shift a
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.norm_compLp_le : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] (L : E →SL[σ] F)
  (f : ↥(MeasureTheory.Lp E p μ)), ‖L.compLp f‖ ≤ ‖L‖ * ‖f‖
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.pow : ∀ {α : Type u_1} {n : Type u_3} [inst : CommSemiring α] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {A : Matrix n n α}, A.IsSymm → ∀ (k : ℕ), (A ^ k).IsSymm
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.coe_le_coe : ∀ {E : Type u_3} [inst : Group E] {p q : GroupSeminorm E}, ⇑p ≤ ⇑q ↔ p ≤ q
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.prodProdProdComm_symm : ∀ (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄],
  (LinearEquiv.prodProdProdComm R M M₂ M₃ M₄).symm = LinearEquiv.prodProdProdComm R M M₃ M₂ M₄
-- Mathlib.Analysis.Complex.Conformal
isConformalMap_conj : IsConformalMap ↑↑Complex.conjLIE
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_sSup : ∀ {G : Type u_1} [inst : Group G] {Hs : Set (Subgroup G)}, (∀ H ∈ Hs, H.Characteristic) → (sSup Hs).Characteristic
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx!.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Inhabited (α × β)] (x : ℕ),
  Std.DTreeMap.Internal.Impl.Const.entryAtIdx! Std.DTreeMap.Internal.Impl.leaf x =
    panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.Const.entryAtIdx!" 870 16
      "Out-of-bounds access"
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that
1) `b` is an upper bound
2) every other upper bound `b'` satisfies `b ≤ b'`.  -/
csSup_eq_of_is_forall_le_of_forall_le_imp_ge : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {b : α},
  s.Nonempty → (∀ a ∈ s, a ≤ b) → (∀ (ub : α), (∀ a ∈ s, a ≤ ub) → b ≤ ub) → sSup s = b
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.ite_ae_eq_of_measure_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {γ : Type u_5} (f g : α → γ) (s : Set α)
  [inst : DecidablePred fun x => x ∈ s], μ s = 0 → (fun x => if x ∈ s then f x else g x) =ᵐ[μ] g
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_eq_empty : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.ball x ε = ∅ ↔ ε ≤ 0
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_cast_uIcc : ∀ {n m : ℕ} (h : n = m) (i j : Fin n),
  Finset.image (Fin.cast h) (Finset.uIcc i j) = Finset.uIcc (Fin.cast h i) (Fin.cast h j)
-- Mathlib.Geometry.Euclidean.Projection
/-- The orthogonal projection of a point onto a nonempty affine subspace.  -/
EuclideanGeometry.orthogonalProjection : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            [inst_3 : MetricSpace P] →
              [inst_4 : NormedAddTorsor V P] →
                (s : AffineSubspace 𝕜 P) → [inst_5 : Nonempty ↥s] → [s.direction.HasOrthogonalProjection] → P →ᴬ[𝕜] ↥s
-- Mathlib.Data.EReal.Operations
/-- Induction principle for `EReal`s splitting into cases `↑(x : ℝ≥0∞)` and `-↑(x : ℝ≥0∞)`.
In the latter case, we additionally assume `0 < x`.  -/
EReal.recENNReal : {motive : EReal → Sort u_1} →
  ((x : ENNReal) → motive ↑x) → ((x : ENNReal) → 0 < x → motive (-↑x)) → (x : EReal) → motive x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The map `S → T` when `S` is a non-unital subalgebra contained in the non-unital subalgebra `T`.

This is the non-unital subalgebra version of `Submodule.inclusion`, or `Subring.inclusion`  -/
NonUnitalSubalgebra.inclusion : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → {S T : NonUnitalSubalgebra R A} → S ≤ T → ↥S →ₙₐ[R] ↥T
-- Mathlib.Algebra.Order.Group.PosPart
Pi.negPart_def : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Lattice (α i)] [inst_1 : (i : ι) → AddGroup (α i)]
  (f : (i : ι) → α i), f⁻ = fun i => (f i)⁻
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curry0_norm : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (f : G [×0]→L[𝕜] G'),
  ‖f.curry0‖ = ‖f‖
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.descOpcycles_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A A' : C}
  (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) (α : A ⟶ A')
  {Z : C} (h : A' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.descOpcycles k j hj hk) (CategoryTheory.CategoryStruct.comp α h) =
    CategoryTheory.CategoryStruct.comp (K.descOpcycles (CategoryTheory.CategoryStruct.comp k α) j hj ⋯) h
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- The continuous functional calculus commutes with integration.
For a version with stronger assumptions which in practice are often easier to verify, see
`cfcₙ_setIntegral`.  -/
cfcₙ_setIntegral' : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NonUnitalNormedRing A] [inst_3 : StarRing A] [inst_4 : NormedSpace 𝕜 A]
  [inst_5 : IsScalarTower 𝕜 A A] [inst_6 : SMulCommClass 𝕜 A A] [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p]
  [inst_8 : CompleteSpace A] {s : Set X} [inst_9 : NormedSpace ℝ A] (f : X → 𝕜 → 𝕜) (a : A),
  (∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (quasispectrum 𝕜 a)) →
    (∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0) →
      MeasureTheory.IntegrableOn (fun x => ContinuousMapZero.mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) s μ →
        autoParam (p a) cfcₙ_setIntegral'._auto_1 →
          cfcₙ (fun z => ∫ (x : X) in s, f x z ∂μ) a = ∫ (x : X) in s, cfcₙ (f x) a ∂μ
-- Mathlib.CategoryTheory.Equivalence
/-- The functor of an equivalence of categories is fully faithful.  -/
CategoryTheory.Equivalence.fullyFaithfulFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {E : Type u₃} → [inst_1 : CategoryTheory.Category.{v₃, u₃} E] → (e : C ≌ E) → e.functor.FullyFaithful
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
CategoryTheory.Square.IsPullback.of_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {sq : CategoryTheory.Square C} (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F],
  (sq.map F).IsPullback → sq.IsPullback
-- Init.Data.Int.Lemmas
Int.natCast_zero : ↑0 = 0
-- Mathlib.RepresentationTheory.Coinvariants
Rep.instAdditiveModuleCatObjFunctorCoinvariantsTensor : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] (A : Rep.{u, u, v} k G),
  ((Rep.coinvariantsTensor k G).obj A).Additive
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonnegative on `Iio b` and
nonpositive on `Ioi b`. Then `f` attains its maximum on `ℝ` at `b`.  -/
isMaxOn_univ_of_deriv : ∀ {f : ℝ → ℝ} {b : ℝ},
  ContinuousAt f b →
    DifferentiableOn ℝ f (Set.Iio b) →
      DifferentiableOn ℝ f (Set.Ioi b) →
        (∀ x ∈ Set.Iio b, 0 ≤ deriv f x) → (∀ x ∈ Set.Ioi b, deriv f x ≤ 0) → IsMaxOn f Set.univ b
-- Mathlib.Order.Filter.Map
Filter.instCommApplicative : CommApplicative Filter
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_div_le : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Div α] [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] {s t : Finset α} {f : α → β} {a : β}, (s / t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x / y) ≤ a
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_transpose_apply' : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂)
  (j : n), ((LinearMap.toMatrix v₁ v₂) f).transpose j = ⇑(v₂.repr (f (v₁ j)))
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.freeVarFinset.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : DecidableEq α] (x : ℕ) (x_1 : L.BoundedFormula α x),
  x_1.freeVarFinset =
    match x, x_1 with
    | _n, FirstOrder.Language.BoundedFormula.falsum => ∅
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => t₁.varFinsetLeft ∪ t₂.varFinsetLeft
    | _n, FirstOrder.Language.BoundedFormula.rel _R ts => Finset.univ.biUnion fun i => (ts i).varFinsetLeft
    | _n, f₁.imp f₂ => f₁.freeVarFinset ∪ f₂.freeVarFinset
    | _n, f.all => f.freeVarFinset
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {a b : α}, cmp a b = Ordering.eq → Std.DTreeMap.Const.get! t a = Std.DTreeMap.Const.get! t b
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.inv : {R : Type u} → Rack.PreEnvelGroup R → Rack.PreEnvelGroup R
-- Mathlib.Order.Category.HeytAlg
/-- The underlying `HeytingHom`.  -/
HeytAlg.Hom.hom' : {X Y : HeytAlg} → X.Hom Y → HeytingHom ↑X ↑Y
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- A set used to index `Basis.ofVectorSpace`.  -/
Module.Basis.ofVectorSpaceIndex : (K : Type u_3) → (V : Type u_4) → [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [Module K V] → Set V
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.symm_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.symm.inverse = e.functor
-- Init.Classical
Classical.choose.congr_simp : ∀ {α : Sort u} {p p_1 : α → Prop} (e_p : p = p_1) (h : ∃ x, p x), Classical.choose h = Classical.choose ⋯
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- **Fermat's Theorem**: the derivative of a function at a local maximum equals zero.  -/
IsLocalMax.hasDerivAt_eq_zero : ∀ {f : ℝ → ℝ} {f' a : ℝ}, IsLocalMax f a → HasDerivAt f f' a → f' = 0
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.mul_subst : ∀ {α : Type u_1} [inst : CommRing α] {n1 n2 k e1 e2 t1 t2 : α},
  n1 * e1 = t1 → n2 * e2 = t2 → n1 * n2 = k → k * (e1 * e2) = t1 * t2
-- Aesop.Search.Main
Aesop.checkRappLimit : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q (Option Lean.MessageData)
-- Lean.Parser.Command
Lean.Parser.Command.initialize.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂)[k]? = t₂[k]?.or t₁[k]?
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_bot : ∀ {M : Type u_2} [inst : MulOneClass M], ⊥.op = ⊥
-- Mathlib.Topology.Order.Monotone
/-- In a second countable space, the set of points where a monotone function is not continuous
is at most countable.  -/
Monotone.countable_not_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {f : α → β} [inst_4 : TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β],
  Monotone f → {x | ¬ContinuousAt f x}.Countable
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The sine of the angle between three points is 1 if and only if the angle is π / 2.  -/
EuclideanGeometry.sin_eq_one_iff_angle_eq_pi_div_two : ∀ {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},
  Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffWithinAt.div_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : DivInvMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G]
  {E' : Type u_5} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6}
  [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H' M] {f : M → G} {s : Set M} {x : M} (c : G),
  ContMDiffWithinAt I' I n f s x → ContMDiffWithinAt I' I n (fun x => f x / c) s x
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instDecidableEqOrderRel : {a : ℕ} → DecidableEq (FirstOrder.Language.orderRel a)
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
/-- `I : Ideal R` is an associated prime of a submodule `N : Submodule R M` if `I` is prime
and `I = (colon N {x}).radical` for some `x : M`.  -/
Submodule.IsAssociatedPrime : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Ideal R → Prop
-- Std.Http.Data.Status
/-- Proof that the code is a valid HTTP status code (100–999), i.e. a three-digit integer
as required by RFC 9112 §4.
 -/
Std.Http.CustomStatus.validCode : ∀ (self : Std.Http.CustomStatus), 100 ≤ self.code ∧ self.code ≤ 999
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The type underlying the multicoequalizer diagram.  -/
CategoryTheory.Limits.WalkingMultispan : CategoryTheory.Limits.MultispanShape → Type (max w w')
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.instIsCyclicOfFiniteOfIsNilpotent : ∀ {G : Type u_1} [inst : Group G] [Finite G] [IsZGroup G] [hG : Group.IsNilpotent G], IsCyclic G
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.opNorm_mapL : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5}
  [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)]
  (f : (i : ι) → E i →L[𝕜] E' i), ‖PiTensorProduct.mapL f‖ ≤ ∏ i, ‖f i‖
-- Init.Data.Nat.Lemmas
Nat.mul_lt_mul_of_le_of_lt : ∀ {a c b d : ℕ}, a ≤ c → b < d → 0 < c → a * b < c * d
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- `simp`-normal form is `tangentBundleCore_localTriv_baseSet`.  -/
tangentBundleCore_baseSet : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (i : ↑(atlas H M)),
  (tangentBundleCore I M).baseSet i = (↑i).source
-- Batteries.Data.Array.Match
Array.Matcher.modifyStep.eq_1 : ∀ {α σ : Type u_1} {n : Type u_1 → Type u_2} [inst : BEq α] (m : Array.Matcher α) [inst_1 : Std.Iterator σ n α]
  (it : Std.IterM n σ) (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done),
  m.modifyStep it ⟨Std.IterStep.done, property⟩ = Std.IterStep.done
-- Mathlib.FieldTheory.Extension
IntermediateField.exists_algHom_adjoin_of_splits' : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {S : Set E} {L : Type u_4} [inst_5 : Field L] [inst_6 : Algebra F L]
  [inst_7 : Algebra L E] [inst_8 : IsScalarTower F L E] (f : L →ₐ[F] K),
  (∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits) → ∃ φ, AlgHom.domRestrict L φ = f
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_one : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : One β], ⇑1 = 1
-- Mathlib.CategoryTheory.Limits.MorphismProperty
/-- Let `P` be stable under composition and cobase change. If `P` satisfies cancellation on the
left, the subcategory of `Under X` defined by `P` is closed under pushouts.  -/
CategoryTheory.Under.closedUnderColimitsOfShape_pushout : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {X : T}
  [CategoryTheory.Limits.HasPushouts T] [P.IsStableUnderComposition] [P.IsStableUnderCobaseChange]
  [P.HasOfPrecompProperty P], P.underObj.IsClosedUnderColimitsOfShape CategoryTheory.Limits.WalkingSpan
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.constₗ_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (R : Type u_6) [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid Y] [inst_3 : Module R Y] (y : Y) (a : X), ((LocallyConstant.constₗ R) y) a = y
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- The concatenation of the reverse of the first walk with the second walk.  -/
SimpleGraph.Walk.reverseAux : {V : Type u} → {G : SimpleGraph V} → {u v w : V} → G.Walk u v → G.Walk u w → G.Walk v w
-- Mathlib.RepresentationTheory.Induced
/-- Given a group homomorphism `φ : G →* H`, an `H`-representation `B`, and a `G`-representation
`A`, there is a `k`-linear equivalence between the `H`-representation morphisms `ind φ A ⟶ B` and
the `G`-representation morphisms `A ⟶ B`.  -/
Rep.indResHomEquiv : {k : Type u} →
  {G : Type v} →
    {H : Type v'} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : Group H] →
            (φ : G →* H) →
              (A : Rep.{max w v' u, u, v} k G) →
                (B : Rep.{max w v' u, u, v'} k H) → (Rep.ind φ A ⟶ B) ≃ₗ[k] A ⟶ Rep.res φ B
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- For a linear map `f` from `M` to `N`,
`ExteriorAlgebra.map g` is a retraction of `ExteriorAlgebra.map f` iff
`g` is a retraction of `f`.  -/
ExteriorAlgebra.leftInverse_map_iff : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u4}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M},
  Function.LeftInverse ⇑(ExteriorAlgebra.map g) ⇑(ExteriorAlgebra.map f) ↔ Function.LeftInverse ⇑g ⇑f
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_mul_monomial : ∀ {R : Type u} {a b : R} {n : ℕ} [inst : Semiring R],
  Polynomial.C a * (Polynomial.monomial n) b = (Polynomial.monomial n) (a * b)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.whisker_right.inj : ∀ {B : Type u} {inst : Quiver B} {a b c : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} {h : b ⟶ c}
  {η η_1 : CategoryTheory.FreeBicategory.Hom₂ f g},
  CategoryTheory.FreeBicategory.Hom₂.whisker_right h η = CategoryTheory.FreeBicategory.Hom₂.whisker_right h η_1 →
    η = η_1
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
/-- `f +ₗ g` is the composite `X ⟶ Y ⊞ Y ⟶ Y`, where the first map is `(f, g)` and the second map
is `(𝟙 𝟙)`.  -/
CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] → (X Y : C) → (X ⟶ Y) → (X ⟶ Y) → (X ⟶ Y)
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hV3 : {k : Type u} →
  {G : Type v} →
    [inst : Ring k] → [inst_1 : TopologicalSpace k] → [inst_2 : Monoid G] → (self : TopRep k G) → TopologicalSpace ↑self