mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Perm.List
List.zipWith_swap_prod_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (l l' : List α),
  (List.zipWith Equiv.swap l l').prod.support ⊆ l.toFinset ⊔ l'.toFinset
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).contains k = (f (t.get? k)).isSome
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.instIsOpenImmersionToNormalizationOfLocallyQuasiFiniteOfLocallyOfFiniteType : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f]
  [AlgebraicGeometry.LocallyOfFiniteType f] [inst : AlgebraicGeometry.IsSeparated f]
  [inst_1 : AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.Hom.toNormalization f)
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.not_dvd_mul : ∀ {p m n : ℕ}, Nat.Prime p → ¬p ∣ m → ¬p ∣ n → ¬p ∣ m * n
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.EStateM.run_bind.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (x : α) → (s : σ) → motive (EStateM.Result.ok x s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.error e s with
    | EStateM.Result.ok x s => h_1 x s
    | EStateM.Result.error e s => h_2 e s) =
    h_2 e s
-- Std.Async.System
Std.Async.System.UserId.mk : ℕ → Std.Async.System.UserId
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasFDerivWithinAt.rpow_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {s : Set E} {p : ℝ},
  HasFDerivWithinAt f f' s x → f x ≠ 0 ∨ 1 ≤ p → HasFDerivWithinAt (fun x => f x ^ p) ((p * f x ^ (p - 1)) • f') s x
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariation.exists_Finpartition_sum_ge : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s : Set X} (hs : MeasurableSet s) {ε : NNReal},
  0 < ε → MeasureTheory.preVariationFun f s ≠ ⊤ → ∃ P, MeasureTheory.preVariationFun f s ≤ ∑ p ∈ P.parts, f ↑p + ↑ε
-- Mathlib.Probability.Distributions.Fernique
/-- Auxiliary lemma for `exists_integrable_exp_sq_of_map_rotation_eq_self`.
The assumptions on `a` and `μ {x | ‖x‖ ≤ a}` are not needed and will be removed in that more
general theorem.  -/
ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self' : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    ∀ {a : ℝ},
      0 < a →
        2⁻¹ < μ {x | ‖x‖ ≤ a} →
          μ {x | ‖x‖ ≤ a} < 1 → ∃ C, 0 < C ∧ MeasureTheory.Integrable (fun x => Real.exp (C * ‖x‖ ^ 2)) μ
-- Init.Data.Array.Lemmas
Array.flatMap_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β}, Array.flatMap f xs = #[] ↔ ∀ x ∈ xs, f x = #[]
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanExt_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
  (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.cospanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingCospan.left = iX
-- Mathlib.Algebra.Order.Floor.Div
Finsupp.ceilDiv_apply : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : AddCommMonoid β] [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : CeilDiv α β] (f : ι →₀ β)
  (a : α) (i : ι), (f ⌈/⌉ a) i = f i ⌈/⌉ a
-- Init.Data.UInt.Bitwise
USize.ofBitVec_not : ∀ (a : BitVec System.Platform.numBits), { toBitVec := ~~~a } = ~~~{ toBitVec := a }
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.restrictScalarsₗ.congr_simp : ∀ (R : Type u_14) (S : Type u_15) (M : Type u_16) (N : Type u_17) [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module S M] [inst_7 : Module S N] [inst_8 : LinearMap.CompatibleSMul M N R S] (R₁ : Type u_19)
  [inst_9 : Semiring R₁] [inst_10 : Module R₁ N] [inst_11 : SMulCommClass S R₁ N] [inst_12 : SMulCommClass R R₁ N],
  LinearMap.restrictScalarsₗ R S M N R₁ = LinearMap.restrictScalarsₗ R S M N R₁
-- Mathlib.Tactic.Cases
Mathlib.Tactic.ElimApp.evalNames : Lean.Meta.ElimInfo →
  Array Lean.Elab.Tactic.ElimApp.Alt →
    Lean.Syntax →
      optParam ℕ 0 →
        optParam (Array Lean.FVarId) #[] →
          optParam (Array Lean.FVarId) #[] →
            optParam (Array (Lean.Ident × Lean.FVarId)) #[] → Lean.Elab.TermElabM (Array Lean.MVarId)
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- For each object in `C`, there is a triangle of the form `(X,X,0,𝟙 X,0,0)`
 -/
CategoryTheory.Pretriangulated.contractibleTriangle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [CategoryTheory.Limits.HasZeroObject C] →
        [CategoryTheory.Limits.HasZeroMorphisms C] → C → CategoryTheory.Pretriangulated.Triangle C
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.of.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (a : C), sizeOf (CategoryTheory.WithInitial.of a) = 1 + sizeOf a
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.restrictDom_comp_subtype : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set α) [inst_3 : DecidablePred fun x => x ∈ s],
  Finsupp.restrictDom M R s ∘ₗ (Finsupp.supported M R s).subtype = LinearMap.id
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.coeff_mem_contentIdeal : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (n : ℕ), p.coeff n ∈ p.contentIdeal
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.groupWithZeroConcreteCategory : CategoryTheory.ConcreteCategory GrpWithZero fun x1 x2 => x1.carrier →*₀ x2.carrier
-- Mathlib.Analysis.Convex.SpecificFunctions.Basic
convexOn_rpow : ∀ {p : ℝ}, 1 ≤ p → ConvexOn ℝ (Set.Ici 0) fun x => x ^ p
-- Batteries.Recycling.MonadSatisfying.Basic
_private.Batteries.Recycling.MonadSatisfying.Basic.0.SatisfiesM_EStateM_eq.match_1_3.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s' : σ)
  (h_1 :
    (a : α) → (s'_1 : σ) → EStateM.Result.error e s' = EStateM.Result.ok a s'_1 → motive (EStateM.Result.ok a s'_1))
  (h_2 :
    (e_1 : ε) →
      (s'_1 : σ) → EStateM.Result.error e s' = EStateM.Result.error e_1 s'_1 → motive (EStateM.Result.error e_1 s'_1)),
  (match q : EStateM.Result.error e s' with
    | EStateM.Result.ok a s'_1 => h_1 a s'_1 q
    | EStateM.Result.error e_1 s'_1 => h_2 e_1 s'_1 q) =
    h_2 e s' ⋯
-- Mathlib.Data.Set.Function
Set.SurjOn.preimage : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.SurjOn f s t → Set.SurjOn f (f ⁻¹' t) t
-- Mathlib.FieldTheory.Finite.Trace
/-- An explicit formula for the norm map: `norm[L/K](x) = ∏ i < [L:K], x ^ ((#K) ^ i)`.  -/
FiniteField.algebraMap_norm_eq_prod_pow : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [Finite L] [inst_3 : Algebra K L] (x : L),
  (algebraMap K L) ((Algebra.norm K) x) = ∏ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i
-- Mathlib.Algebra.BigOperators.Expect
/-- Expectation over a product set equals the expectation of the fiberwise expectations.

For rewriting in the reverse direction, use `Finset.expect_product`.  -/
Finset.expect_product' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] (s : Finset ι)
  (t : Finset κ) (f : ι → κ → M), ((s ×ˢ t).expect fun i => f i.1 i.2) = s.expect fun i => t.expect fun j => f i j
-- Lean.Compiler.IR.Basic
Lean.IR.CtorInfo.ssize : Lean.IR.CtorInfo → ℕ
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_univ : ∀ {R : Type u} [inst : NonAssocRing R], Subring.closure Set.univ = ⊤
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb_convexCombPair_comm_right : ∀ {R : Type u_9} {M : Type u_10} {I : Type u_11} [inst : PartialOrder R] [inst_1 : CommSemiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t)
  (h : s + t = 1) (f : Convexity.StdSimplex R I) (m : M) (e : I → M),
  (Convexity.iConvexComb f fun x => Convexity.convexCombPair s t hs ht h m (e x)) =
    Convexity.convexCombPair s t hs ht h m (Convexity.iConvexComb f e)
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.mulTSupport_extend_one : ∀ {α : Type u_2} {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace α']
  [inst_2 : One β] {f : α → β} [T2Space α'],
  HasCompactMulSupport f →
    ∀ {g : α → α'}, Continuous g → Function.Injective g → mulTSupport (Function.extend g f 1) = g '' mulTSupport f
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- A functor `F : C ⥤ D` is faithful if for each `X Y : C`, `F.map` is injective.  -/
CategoryTheory.Functor.Faithful : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Tactic.Determinant.Bird.Cert
Mathlib.Tactic.Determinant.Cert.mk : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      {subject : Q(«$α»)} → Mathlib.Tactic.Determinant.CertResult rα subject → Bool → Mathlib.Tactic.Determinant.Cert rα
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instSymmetricCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C],
  CategoryTheory.AddMon.instSymmetricCategory =
    { braiding := fun X Y => CategoryTheory.AddMon.mkIso' (β_ X.X Y.X), braiding_naturality_right := ⋯,
      braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯, symmetry := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A bicone over a pair is a limit cone if and only if the corresponding binary bicone is a limit
cone.  -/
CategoryTheory.Limits.Bicone.toBinaryBiconeIsLimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)) →
          CategoryTheory.Limits.IsLimit b.toBinaryBicone.toCone ≃ CategoryTheory.Limits.IsLimit b.toCone
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.norm_toL1_eq_lintegral_enorm : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : α → β) (hf : MeasureTheory.Integrable f μ), ‖MeasureTheory.Integrable.toL1 f hf‖ = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_finset : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] (s : Finset α)
  (f : α → ENNReal), ∫⁻ (x : α) in ↑s, f x ∂μ = ∑ x ∈ s, f x * μ {x}
-- Lean.Meta.Instances
Lean.Meta.Instances.eraseCore : Lean.Meta.Instances → Lean.Name → Lean.Meta.Instances
-- Lean.Server.Utils
/-- Constructs a `$/lean/fileProgress` notification from the given position onwards.  -/
Lean.Server.mkFileProgressAtPosNotification : Lean.Server.DocumentMeta →
  String.Pos.Raw →
    optParam Lean.Lsp.LeanFileProgressKind Lean.Lsp.LeanFileProgressKind.processing →
      Lean.JsonRpc.Notification Lean.Lsp.LeanFileProgressParams
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
ContinuousFunctionalCalculus.compactSpace_spectrum : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : StarRing R}
  {inst_2 : MetricSpace R} {inst_3 : IsTopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A}
  {inst_6 : StarRing A} {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A} [self : ContinuousFunctionalCalculus R A p]
  (a : A), CompactSpace ↑(spectrum R a)
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
/-- The support of a ring preordering `P` in a commutative ring `R` is
the set of elements `x` in `R` such that both `x` and `-x` lie in `P`.
 -/
RingPreordering.support : {R : Type u_1} → [inst : CommRing R] → (P : RingPreordering R) → [P.HasIdealSupport] → Ideal R
-- Std.Http.Server.Connection
/-- Represents the remote address of a client connection.
 -/
Std.Http.Server.RemoteAddr : Type
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {l : Filter α} {f : α → β}
  {μ : MeasureTheory.Measure α}, MeasureTheory.AEStronglyMeasurable f μ → StronglyMeasurableAtFilter f l μ
-- Mathlib.Algebra.Ring.Opposite
RingHom.op_apply_apply : ∀ {R : Type u_2} {S : Type u_3} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (a : Rᵐᵒᵖ),
  (RingHom.op f) a = MulOpposite.op (f (MulOpposite.unop a))
-- Mathlib.Topology.Algebra.Ring.Compact
instFiniteQuotientIdealOfIsMaximal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R]
  [IsNoetherianRing R] (I : Ideal R) [I.IsMaximal], Finite (R ⧸ I)
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.conj_rootsOfUnity : ∀ {ζ : ℂˣ} {n : ℕ} [NeZero n], ζ ∈ rootsOfUnity n ℂ → (starRingEnd ℂ) ↑ζ = ↑ζ⁻¹
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_X_mul : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (Polynomial.X * p).coeff (n + 1) = p.coeff n
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrictₗ_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {R : Type u_4} [inst_2 : Semiring R] [inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M]
  [inst_5 : ContinuousAdd M] (i : Set α) (v : MeasureTheory.VectorMeasure α M),
  (MeasureTheory.VectorMeasure.restrictₗ i) v = v.restrict i
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.toSubmodule_injective : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W}, Function.Injective Subrepresentation.toSubmodule
-- Init.Notation
/-- The `nat_lit n` macro constructs "raw numeric literals". This corresponds to the
`Expr.lit (.natVal n)` constructor in the `Expr` data type.

Normally, when you write a numeral like `#check 37`, the parser turns this into
an application of `OfNat.ofNat` to the raw literal `37` to cast it into the
target type, even if this type is `Nat` (so the cast is the identity function).
But sometimes it is necessary to talk about the raw numeral directly,
especially when proving properties about the `ofNat` function itself.
 -/
rawNatLit : Lean.ParserDescr
-- Mathlib.Algebra.GroupWithZero.Divisibility
/-- Given an element `a` of a commutative semigroup with zero, there exists another element whose
product with zero equals `a` iff `a` equals zero.  -/
zero_dvd_iff : ∀ {α : Type u_1} [inst : SemigroupWithZero α] {a : α}, 0 ∣ a ↔ a = 0
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.Hom.mk : {X Y : SFinKer} → (hom : ProbabilityTheory.Kernel X.carrier Y.carrier) → ProbabilityTheory.IsSFiniteKernel hom → X.Hom Y
-- Std.Http.Data.URI.Basic
/-- The port number.
 -/
Std.Http.URI.Builder.port : Std.Http.URI.Builder → Std.Http.URI.Port
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.ContinuousRiemannianMetric.continuous : ∀ {B : Type u_4} [inst : TopologicalSpace B] {F : Type u_5} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_6} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (b : B) → TopologicalSpace (E b)]
  [inst_5 : (b : B) → AddCommGroup (E b)] [inst_6 : (b : B) → Module ℝ (E b)] [inst_7 : FiberBundle F E]
  [inst_8 : VectorBundle ℝ F E] (self : Bundle.ContinuousRiemannianMetric F E), Continuous fun b => ⟨b, self.inner b⟩
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the numerator of the first right fraction  -/
CategoryTheory.MorphismProperty.RightFraction₂.f : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.RightFraction₂ X Y) → self.X' ⟶ Y
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
/-- If `A` is irreducible and `n` is non-trivial then every row has a positive entry.  -/
Matrix.IsIrreducible.exists_pos : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] {A : Matrix n n R} [Nontrivial n],
  A.IsIrreducible → ∀ (i : n), ∃ j, 0 < A i j
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_mul_symm_re_eq_norm : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F), RCLike.re (inner 𝕜 x y * inner 𝕜 y x) = ‖inner 𝕜 x y * inner 𝕜 y x‖
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivAtFilter.fun_sum : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {L : Filter (𝕜 × 𝕜)} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F},
  (∀ i ∈ u, HasDerivAtFilter (A i) (A' i) L) → HasDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) L
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ordCompare_maxKey!_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.ExtTreeMap α β compare}
  [inst_2 : Inhabited α] {k : α} {f : β → β}, compare (t.modify k f).maxKey! t.maxKey! = Ordering.eq
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Cell.Const.alter.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] {k : α} (f : Option β → Option β)
  (c : Std.DTreeMap.Internal.Cell α (fun x => β) (compare k)),
  Std.DTreeMap.Internal.Cell.Const.alter f c =
    match c.inner with
    | none => Std.DTreeMap.Internal.Cell.ofOption k (f none)
    | some ⟨fst, v'⟩ => Std.DTreeMap.Internal.Cell.ofOption k (f (some v'))
-- Mathlib.RingTheory.PicardGroup
instInvertibleReprₛ : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Invertible R M], Module.Invertible R (Module.Finite.reprₛ R M)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivLeft_symm_C_X : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (x : S₁),
  (MvPolynomial.optionEquivLeft R S₁).symm (Polynomial.C (MvPolynomial.X x)) = MvPolynomial.X (some x)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.zero_hom : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (M N : CategoryTheory.AddMon D),
  CategoryTheory.AddMon.Hom.hom 0 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit M.X)
      CategoryTheory.AddMonObj.zero
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct a morphism between whiskered lifts.  -/
CategoryTheory.Bicategory.RightLift.whiskerHom : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {s t : CategoryTheory.Bicategory.RightLift f g} → (s ⟶ t) → {x : B} → (h : x ⟶ c) → s.whisker h ⟶ t.whisker h
-- Init.Data.List.Range
List.map_snd_add_zipIdx_eq_zipIdx : ∀ {α : Type u_1} {l : List α} {n k : ℕ}, List.map (Prod.map id fun x => x + n) (l.zipIdx k) = l.zipIdx (n + k)
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.CheckResult.le : Lean.Meta.Grind.CheckResult → Lean.Meta.Grind.CheckResult → Bool
-- Init.Data.UInt.Lemmas
UInt8.toUInt8_toUSize : ∀ (n : UInt8), n.toUSize.toUInt8 = n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.nonsingular_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [Nontrivial R], W'.Nonsingular ![1, 1, 0]
-- Init.Data.List.Lemmas
List.flatMap_reverse : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β},
  List.flatMap f l.reverse = (List.flatMap (List.reverse ∘ f) l).reverse
-- Mathlib.Topology.Convenient.HomSpace
/-- The bijection between the type of `X`-continuous maps `Y × Z → T` and the type of
`X`-continuous maps `Z → ContinuousMapGeneratedBy X Y T`.  -/
Topology.ContinuousMapGeneratedBy.curryEquiv : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} →
        [inst_1 : TopologicalSpace Y] →
          {Z : Type v'} →
            [inst_2 : TopologicalSpace Z] →
              {T : Type v''} →
                [inst_3 : TopologicalSpace T] →
                  [∀ (i : ι), LocallyCompactSpace (X i)] →
                    [∀ (i j : ι), Topology.IsGeneratedBy X (X i × X j)] →
                      Topology.ContinuousMapGeneratedBy X (Y × Z) T ≃
                        Topology.ContinuousMapGeneratedBy X Z (Topology.ContinuousMapGeneratedBy X Y T)
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_iInf : ∀ {ι : Sort u_1} {R : Type u_2} [inst : NonAssocRing R] (S : ι → Subring R), (iInf S).op = ⨅ i, (S i).op
-- Init.Data.UInt.Bitwise
UInt8.ofFin_shiftLeft : ∀ (a b : Fin UInt8.size), ↑b < 8 → UInt8.ofFin (a <<< b) = UInt8.ofFin a <<< UInt8.ofFin b
-- Lean.Declaration
Lean.Constructor.name : Lean.Constructor → Lean.Name
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : F.obj a ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp f g)) (α.app c) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.naturality (CategoryTheory.CategoryStruct.comp f g)).inv h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (α.app a) (G.mapComp f g).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (α.app a) (G.map f) (G.map g)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (α.naturality f).inv (G.map g))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (α.app b) (G.map g)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (α.naturality g).inv)
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (α.app c)).inv
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).inv (α.app c)) h))))))
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- The slash invariant form of weight `k₁ + k₂` given by the product of two slash-invariant forms
of weights `k₁` and `k₂`.  -/
SlashInvariantForm.mul : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  [Γ.HasDetPlusMinusOne] →
    {k₁ k₂ : ℤ} → SlashInvariantForm Γ k₁ → SlashInvariantForm Γ k₂ → SlashInvariantForm Γ (k₁ + k₂)
-- Mathlib.GroupTheory.Index
AddSubgroup.index_prod : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) (K : AddSubgroup G'),
  (H.prod K).index = H.index * K.index
-- Init.Data.BitVec.Lemmas
/-- Zero extending `1#v` to `1#w` equals `1#w` when `v > 0`.  -/
BitVec.setWidth_ofNat_one_eq_ofNat_one_of_lt : ∀ {v w : ℕ}, 0 < v → BitVec.setWidth w 1#v = 1#w