mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PowerBasis
PowerBasis.constr_pow_mul : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) {y : S'},
  (Polynomial.aeval y) (minpoly A pb.gen) = 0 →
    ∀ (x x' : S),
      ((pb.basis.constr A) fun i => y ^ ↑i) (x * x') =
        ((pb.basis.constr A) fun i => y ^ ↑i) x * ((pb.basis.constr A) fun i => y ^ ↑i) x'
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.Algebra.Algebra.Defs
/-- Let `R` be a commutative semiring, let `A` be a semiring with a `Module R` structure.
If `(r • 1) * x = x * (r • 1) = r • x` for all `r : R` and `x : A`, then `A` is an `Algebra`
over `R`.

See note [reducible non-instances].  -/
Algebra.ofModule' : {R : Type u} →
  {A : Type w} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Module R A] →
          (∀ (r : R) (x : A), r • 1 * x = r • x) → (∀ (r : R) (x : A), x * r • 1 = r • x) → Algebra R A
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.order_ne_zero_iff_constCoeff_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, φ.order ≠ 0 ↔ PowerSeries.constantCoeff φ = 0
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.homInhabited : {ι : Type v} →
  [inst : Inhabited ι] →
    Inhabited ((CategoryTheory.Pairwise.single default).Hom (CategoryTheory.Pairwise.single default))
-- Mathlib.Logic.Function.OfArity
Function.ofArity_zero : ∀ (α β : Type u), Function.OfArity α β 0 = β
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associator_naturality_right_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h')
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h').hom h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η)) h_1)
-- Init.Data.Array.Monadic
Array.filterM_congr : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] {as bs : Array α},
  as = bs → ∀ {p q : α → m Bool}, (∀ (a : α), p a = q a) → Array.filterM p as = Array.filterM q bs
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.isSymmetric_self_comp_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F),
  (T ∘ₗ LinearMap.adjoint T).IsSymmetric
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.deriv_sq_norm_pos : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    0 < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_toArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.toArray.size = t.size
-- Init.Data.Nat.MinMax
Nat.min_comm : ∀ (a b : ℕ), min a b = min b a
-- Mathlib.Data.Nat.Multiplicity
/-- The multiplicity of a prime `p` in `p ^ n` is the sum of `p ^ i`, where `i` ranges between `0`
and `n - 1`.  -/
Nat.Prime.multiplicity_factorial_pow : ∀ {n p : ℕ}, Nat.Prime p → multiplicity p (p ^ n).factorial = ∑ i ∈ Finset.range n, p ^ i
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.exists_seq_monotone_tendsto_atTop_atTop : ∀ (α : Type u_3) [inst : Preorder α] [Nonempty α] [IsDirectedOrder α] [Filter.atTop.IsCountablyGenerated],
  ∃ xs, Monotone xs ∧ Filter.Tendsto xs Filter.atTop Filter.atTop
-- Aesop.Search.Expansion.Norm
Aesop.NormM.Context.mk.injEq : ∀ (options : Aesop.Options') (ruleSet : Aesop.LocalRuleSet) (normSimpContext : Aesop.NormSimpContext)
  (options_1 : Aesop.Options') (ruleSet_1 : Aesop.LocalRuleSet) (normSimpContext_1 : Aesop.NormSimpContext),
  ({ options := options, ruleSet := ruleSet, normSimpContext := normSimpContext } =
      { options := options_1, ruleSet := ruleSet_1, normSimpContext := normSimpContext_1 }) =
    (options = options_1 ∧ ruleSet = ruleSet_1 ∧ normSimpContext = normSimpContext_1)
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.toList_valuesIter_eq_toList_map_snd : ∀ {α β : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap α fun x => β},
  m.valuesIter.toList = List.map Sigma.snd m.toList
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.addFactStep : Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.instToStringCastMode : ToString Mathlib.Tactic.DepRewrite.CastMode
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- An affine-independent subset of a finite-dimensional affine space is finite.  -/
finite_set_of_fin_dim_affineIndependent : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [FiniteDimensional k V] {s : Set ι} {f : ↑s → P},
  AffineIndependent k f → s.Finite
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isSup.injEq : ∀ (lhs rhs res lhs_1 rhs_1 res_1 : ℕ),
  (Mathlib.Tactic.Order.AtomicFact.isSup lhs rhs res = Mathlib.Tactic.Order.AtomicFact.isSup lhs_1 rhs_1 res_1) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ res = res_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addU_smul : ∀ {F : Type u} [inst : Field F] (P Q : Fin 3 → F) (u v : F),
  WeierstrassCurve.Projective.addU (u • P) (v • Q) = (u * v) ^ 2 * WeierstrassCurve.Projective.addU P Q
-- Lean.Message
Lean.MessageData.instCoeSyntax : Coe Lean.Syntax Lean.MessageData
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- If the sequence of Fourier coefficients of `f` is summable, then the Fourier series converges
uniformly to `f`.  -/
UnitAddTorus.hasSum_mFourier_series_of_summable : ∀ {d : Type u_1} [inst : Fintype d] {f : C(UnitAddTorus d, ℂ)},
  Summable (UnitAddTorus.mFourierCoeff ⇑f) →
    HasSum (fun i => UnitAddTorus.mFourierCoeff (⇑f) i • UnitAddTorus.mFourier i) f
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The homology map data associated to the zero morphism between two short complexes.  -/
CategoryTheory.ShortComplex.HomologyMapData.zero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (h₁ : S₁.HomologyData) → (h₂ : S₂.HomologyData) → CategoryTheory.ShortComplex.HomologyMapData 0 h₁ h₂
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntryD.eq_1 : ∀ {α : Type u} {β : Type v} (x : α × β),
  Std.DTreeMap.Internal.Impl.Const.maxEntryD Std.DTreeMap.Internal.Impl.leaf x = x
-- Lean.Elab.Term.TermElabM
/-- When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`.
The function `elabTerm` catches this exception and creates fresh synthetic metavariable `?m`, stores `?m` in
the list of pending synthetic metavariables, and returns `?m`.
 -/
Lean.Elab.Term.Context.mayPostpone : Lean.Elab.Term.Context → Bool
-- Mathlib.Tactic.Linarith.Datatypes
/-- Add two `Linexp`s together componentwise.
Preserves sorting and uniqueness of the first argument.
 -/
Mathlib.Tactic.Linarith.Linexp.add : Mathlib.Tactic.Linarith.Linexp → Mathlib.Tactic.Linarith.Linexp → Mathlib.Tactic.Linarith.Linexp
-- Mathlib.GroupTheory.OrderOfElement
orderOf_dvd_natCard : ∀ {G : Type u_6} [inst : Group G] (x : G), orderOf x ∣ Nat.card G
-- Mathlib.Data.PEquiv
PEquiv.trans_single_of_mem : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : DecidableEq γ]
  {a : α} {b : β} (c : γ) {f : α ≃. β}, b ∈ f a → f.trans (PEquiv.single b c) = PEquiv.single a c
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharTwoNF.of_j_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {W : WeierstrassCurve R} [W.IsCharTwoJEqZeroNF], W.IsCharTwoNF
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A subfield is closed under multiplicative inverses.  -/
Subfield.inv_mem' : ∀ {K : Type u} [inst : DivisionRing K] (self : Subfield K), ∀ x ∈ self.carrier, x⁻¹ ∈ self.carrier
-- Mathlib.RingTheory.ClassGroup.Basic
/-- The ideal class group of `R` is the group of invertible fractional ideals
modulo the principal ideals.  -/
ClassGroup : (R : Type u_1) → [inst : CommRing R] → [IsDomain R] → Type u_1
-- Mathlib.Order.Interval.Set.LinearOrder
/-- **Alias** of `Set.Iic_sdiff_Ioc`. -/
Set.Iic_diff_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iic b \ Set.Ioc a b = Set.Iic (min a b)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `zeroExtend` on `BitVec`s.  -/
BitVec.reduceZeroExtend : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.Category.TopCat.Adjunctions
TopCat.adj₁_unit : TopCat.adj₁.unit = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.id (Type u))
-- Mathlib.Geometry.Euclidean.MongePoint
/-- `mongePointWeightsWithCircumcenter` sums to 1.  -/
Affine.Simplex.sum_mongePointWeightsWithCircumcenter : ∀ (n : ℕ), ∑ i, Affine.Simplex.mongePointWeightsWithCircumcenter n i = 1
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.coe_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], ↑1 = 1
-- Init.Data.Bool
Bool.instLawfulIdentityBneFalse : Std.LawfulIdentity (fun x1 x2 => x1 != x2) false
-- Mathlib.RingTheory.Lasker
Submodule.decomposition_erase_inf : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {s : Finset (Submodule R M)},
  s.inf id = N → ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.IsAddModHom.map_vadd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {X : C} [inst_3 : CategoryTheory.AddModObj M X] {Y : C}
  [inst_4 : CategoryTheory.AddModObj M Y] (f : X ⟶ Y) [CategoryTheory.IsAddModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X),
  CategoryTheory.CategoryStruct.comp (m +ᵥ x) f = m +ᵥ CategoryTheory.CategoryStruct.comp x f
-- Mathlib.Computability.StateTransition
StateTransition.eval_maximal : ∀ {σ : Type u_1} {f : σ → Option σ} {a b : σ},
  b ∈ StateTransition.eval f a → ∀ {c : σ}, StateTransition.Reaches f b c ↔ c = b
-- Mathlib.Data.Fin.Tuple.Reflection
/-- Produce a term of the form `f 0 * f 1 * ... * f (n - 1)` and an application of `FinVec.prod_eq`
that shows it is equal to `∏ i, f i`.  -/
FinVec.mkProdEqQ : {u : Lean.Level} →
  {α : Q(Type u)} →
    (inst : Q(CommMonoid «$α»)) →
      (n : ℕ) → (f : Q(Fin «$n» → «$α»)) → Lean.MetaM ((val : Q(«$α»)) × Q(∏ i, «$f» i = «$val»))
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.addGroupMultiples.eq_1 : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} (hx : IsOfFinAddOrder x),
  hx.addGroupMultiples = And.casesOn ⋯ fun hpos hx_1 => AddSubmonoid.addGroupMultiples hpos hx_1
-- Lean.Server.Requests
/-- NB: This method may only be called in `initialize` blocks (user or builtin).

A registration consists of:
- a type of JSON-parsable request data `paramType`
- a `FileSource` instance for it so the system knows where to route requests
- a type of JSON-serializable response data `respType`
- an actual `handler` which runs in the `RequestM` monad and is expected
  to produce an asynchronous `RequestTask` which does any waiting/computation
- an optional `serialize` function which can be used to serialize `respType` directly to a string
  for performance reasons, skipping `Json`

A handler task may be cancelled at any time, so it should check the cancellation token when possible
to handle this cooperatively. Any exceptions thrown in a request handler will be reported to the client
as LSP error responses.  -/
Lean.Server.registerLspRequestHandler : String →
  (paramType : Type) →
    [Lean.FromJson paramType] →
      [Lean.Lsp.FileSource paramType] →
        (respType : Type) →
          [Lean.ToJson respType] →
            (paramType → Lean.Server.RequestM (Lean.Server.RequestTask respType)) →
              optParam (Option (respType → String)) none → IO Unit
-- Mathlib.CategoryTheory.Abelian.Opposite
/-- The opposite of the image of `f` is the image of `f.op`.  -/
CategoryTheory.imageOpOp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} → (f : X ⟶ Y) → Opposite.op (CategoryTheory.Limits.image f) ≅ CategoryTheory.Limits.image f.op
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.norm_charFun_le_one : ∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [inst : SeminormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] [MeasureTheory.IsProbabilityMeasure μ] (t : E), ‖MeasureTheory.charFun μ t‖ ≤ 1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono'_K : ∀ {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₂) (h : S₂.LeftHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).K = h.K
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_mul_I : ∀ (x : ℂ), Complex.sinh (x * Complex.I) = Complex.sin x * Complex.I
-- Std.Http.Server
Std.Http.Server.mk.inj : ∀ {context : Std.CancellationContext} {activeConnections : Std.Mutex ℕ} {connectionLimit : Option Std.Semaphore}
  {shutdownPromise : Std.Channel Unit} {config : Std.Http.Config} {localAddr : Option Std.Net.SocketAddress}
  {context_1 : Std.CancellationContext} {activeConnections_1 : Std.Mutex ℕ} {connectionLimit_1 : Option Std.Semaphore}
  {shutdownPromise_1 : Std.Channel Unit} {config_1 : Std.Http.Config} {localAddr_1 : Option Std.Net.SocketAddress},
  { context := context, activeConnections := activeConnections, connectionLimit := connectionLimit,
        shutdownPromise := shutdownPromise, config := config, localAddr := localAddr } =
      { context := context_1, activeConnections := activeConnections_1, connectionLimit := connectionLimit_1,
        shutdownPromise := shutdownPromise_1, config := config_1, localAddr := localAddr_1 } →
    context = context_1 ∧
      activeConnections = activeConnections_1 ∧
        connectionLimit = connectionLimit_1 ∧
          shutdownPromise = shutdownPromise_1 ∧ config = config_1 ∧ localAddr = localAddr_1
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The vector field is continuous in time within a closed ball.  -/
IsPicardLindelof.continuousOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E}
  {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K →
    ∀ x ∈ Metric.closedBall x₀ ↑a, ContinuousOn (fun x_1 => f x_1 x) (Set.Icc tmin tmax)
-- Mathlib.CategoryTheory.Yoneda
/-- The isomorphism `yoneda.obj Y ≅ F` induced by `e : F.RepresentableBy Y`.  -/
CategoryTheory.Functor.RepresentableBy.toIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} → {Y : C} → F.RepresentableBy Y → (CategoryTheory.yoneda.obj Y ≅ F)
-- Mathlib.Data.List.AList
AList.entries_insert_of_notMem : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s : AList β},
  a ∉ s → (AList.insert a b s).entries = ⟨a, b⟩ :: s.entries
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instSMulNat : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [AddSubmonoidClass σ A] → {𝒜 : ι → σ} → (x : Submonoid A) → SMul ℕ (HomogeneousLocalization 𝒜 x)
-- Mathlib.Order.SuccPred.Basic
Order.Icc_succ_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  a ≤ Order.succ b → Set.Icc a (Order.succ b) = insert (Order.succ b) (Set.Icc a b)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.InhabitedColimitType : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → Inhabited (RingCat.Colimits.ColimitType F)
-- Init.Data.SInt.Bitwise
ISize.toInt8_and : ∀ (a b : ISize), (a &&& b).toInt8 = a.toInt8 &&& b.toInt8
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.Hom.mk.sizeOf_spec : ∀ {X Y : Bipointed} (toFun : X.X → Y.X) (map_fst : toFun X.toProd.1 = Y.toProd.1)
  (map_snd : toFun X.toProd.2 = Y.toProd.2),
  sizeOf { toFun := toFun, map_fst := map_fst, map_snd := map_snd } = 1 + sizeOf map_fst + sizeOf map_snd
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a right-angled triangle is at most `π / 2`.  -/
EuclideanGeometry.angle_le_pi_div_two_of_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},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 → EuclideanGeometry.angle p₂ p₃ p₁ ≤ Real.pi / 2
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.card_mul_eq_card_mul : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β} {m n : ℕ}
  [inst : (a : α) → (b : β) → Decidable (r a b)],
  (∀ a ∈ s, (Finset.bipartiteAbove r t a).card = m) →
    (∀ b ∈ t, (Finset.bipartiteBelow r s b).card = n) → s.card * m = t.card * n
-- Mathlib.Data.Finsupp.Interval
Finsupp.card_Ioc : ∀ {ι : Type u_1} {α : Type u_2} [inst : PartialOrder α] [inst_1 : Zero α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq ι] [inst_4 : DecidableEq α] (f g : ι →₀ α),
  (Finset.Ioc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 1
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadCheck.shape.inj : ∀ {k : List Lean.SyntaxNodeKind} {arity : Option ℕ} {k_1 : List Lean.SyntaxNodeKind} {arity_1 : Option ℕ},
  Lean.Elab.Term.Quotation.HeadCheck.shape k arity = Lean.Elab.Term.Quotation.HeadCheck.shape k_1 arity_1 →
    k = k_1 ∧ arity = arity_1
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of `r : R` is less than 1 if and only if `r ∈ v`.  -/
IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
  (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑r < 1 ↔ r ∈ v.asIdeal
-- Std.Time.Format.Basic
/-- Parser for a format with a builder.
 -/
Std.Time.GenericFormat.builderParser : {α : Type} →
  (format : Std.Time.FormatString) →
    Std.Time.FormatConfig → Std.Time.FormatType (Option α) format → Std.Internal.Parsec.String.Parser α
-- Mathlib.Order.Max
/-- **Alias** of the reverse direction of `isTop_ofDual_iff`. -/
IsBot.ofDual : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsBot a → IsTop (OrderDual.ofDual a)
-- Init.Data.SInt.Bitwise
USize.toISize_not : ∀ (a : USize), (~~~a).toISize = ~~~a.toISize
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.throwCasesException : {α : Type} → Lean.Meta.Match.Problem → Lean.Exception → Lean.MetaM α
-- Mathlib.Order.CountableSupClosed
countableSupClosure_singleton : ∀ {α : Type u_2} [inst : PartialOrder α] {x : α}, countableSupClosure {x} = {x}
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeList.match_3.eq_1 : ∀ {α : Type u_1} (motive : List α → List ℕ → Sort u_2) (xs : List α) (h_1 : (xs : List α) → motive xs [])
  (h_2 : (xs : List α) → (n : ℕ) → (ns : List ℕ) → motive xs (n :: ns)),
  (match xs, [] with
    | xs, [] => h_1 xs
    | xs, n :: ns => h_2 xs n ns) =
    h_1 xs
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.setLIntegral_toKernel_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → StieltjesFunction ℝ}
  [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) {s : Set β},
  MeasurableSet s →
    ∀ {t : Set ℝ},
      MeasurableSet t →
        ∫⁻ (b : β) in s, ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.mk.inj : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} {inst : CommSemiring R} {inst_1 : CommSemiring A}
  {inst_2 : AddCommMonoid M} {inst_3 : Algebra R A} {inst_4 : Module A M} {inst_5 : Module R M}
  {toLinearMap : A →ₗ[R] M} {map_one_eq_zero' : toLinearMap 1 = 0}
  {leibniz' : ∀ (a b : A), toLinearMap (a * b) = a • toLinearMap b + b • toLinearMap a} {toLinearMap_1 : A →ₗ[R] M}
  {map_one_eq_zero'_1 : toLinearMap_1 1 = 0}
  {leibniz'_1 : ∀ (a b : A), toLinearMap_1 (a * b) = a • toLinearMap_1 b + b • toLinearMap_1 a},
  { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' } =
      { toLinearMap := toLinearMap_1, map_one_eq_zero' := map_one_eq_zero'_1, leibniz' := leibniz'_1 } →
    toLinearMap = toLinearMap_1
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_uIcc_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Lattice (α i)] [inst_1 : DecidableEq ι] (f : (i : ι) → α i)
  (i : ι) (b : α i), Function.update f i '' Set.uIcc (f i) b = Set.uIcc f (Function.update f i b)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a `G`-representation `A` on which a normal subgroup `S ≤ G` acts trivially, this is the
short complex `H₁(S, A) ⟶ H₁(G, A) ⟶ H₁(G ⧸ S, A)`. (This is a simplified expression for the
degree 1 corestriction-coinflation sequence when `A` is `S`-trivial.)  -/
groupHomology.H1CoresCoinfOfTrivial : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        (S : Subgroup G) →
          [S.Normal] →
            [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.toAddSubmonoid_inj : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s t : NonUnitalSubsemiring R},
  s.toAddSubmonoid = t.toAddSubmonoid ↔ s = t
-- Mathlib.Data.ZMod.Defs
ZMod.repr : (n : ℕ) → Repr (ZMod n)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Result.mk.inj : ∀ {expr : Lean.Expr} {proof? : Option Lean.Expr} {cache : Bool} {expr_1 : Lean.Expr} {proof?_1 : Option Lean.Expr}
  {cache_1 : Bool},
  { expr := expr, proof? := proof?, cache := cache } = { expr := expr_1, proof? := proof?_1, cache := cache_1 } →
    expr = expr_1 ∧ proof? = proof?_1 ∧ cache = cache_1
-- Lean.Parser.Command
Lean.Parser.Command.visibility.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
/-- [Stacks Tag 00GK](https://stacks.math.columbia.edu/tag/00GK) -/
RingHom.Finite.to_isIntegral : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, f.Finite → f.IsIntegral
-- Mathlib.Algebra.Lie.Extension
/-- The inclusion homomorphism `N →ₗ⁅R⁆ L`  -/
LieAlgebra.Extension.incl : {R : Type u_1} →
  {N : Type u_2} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing N] →
          [inst_2 : LieAlgebra R N] →
            [inst_3 : LieRing M] → [inst_4 : LieAlgebra R M] → (self : LieAlgebra.Extension R N M) → N →ₗ⁅R⁆ self.L