mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.FindPos
String.Slice.posGT_eq_posGE : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p < s.rawEndPos}, s.posGT p h = s.posGE p.inc ⋯
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.normSq_denom_pos : ∀ (g : GL (Fin 2) ℝ) {z : ℂ}, z.im ≠ 0 → 0 < Complex.normSq (UpperHalfPlane.denom g z)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.prod_apply : ∀ {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃] [inst_11 : AddTorsor V₃ P₃]
  [inst_12 : TopologicalSpace P₃] (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) (p : P₁), (f.prod g) p = (f p, g p)
-- Mathlib.CategoryTheory.Category.Preorder
OrderIso.equivalence_functor : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (e : X ≃o Y), e.equivalence.functor = ⋯.functor
-- Init.Data.UInt.Bitwise
UInt64.toUInt8_xor : ∀ (a b : UInt64), (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8
-- Mathlib.Algebra.Category.Grp.ZModuleEquivalence
ModuleCat.forget₂AddCommGroupIsEquivalence : (CategoryTheory.forget₂ (ModuleCat ℤ) AddCommGrpCat).IsEquivalence
-- Mathlib.Analysis.SpecificLimits.Normed
alternating_series_error_bound : ∀ {E : Type u_5} [inst : Ring E] [inst_1 : LinearOrder E] [IsOrderedRing E] [inst_3 : UniformSpace E]
  [IsUniformAddGroup E] [CompleteSpace E] [OrderClosedTopology E] (f : ℕ → E),
  Antitone f → Summable f → ∀ (n : ℕ), |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range n, (-1) ^ i * f i| ≤ f n
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Affine.CoordinateRing.mk_Ψ_sq : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ),
  (WeierstrassCurve.Affine.CoordinateRing.mk W) (W.Ψ n) ^ 2 =
    (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (W.ΨSq n))
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.isMax_of_noMin : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : PredOrder α] [IsPredArchimedean α] [NoMinOrder α],
  Order.IsPredPrelimit a → IsMax a
-- Mathlib.GroupTheory.Congruence.Defs
/-- Additive congruence relations preserve integer scaling.  -/
AddCon.zsmul : ∀ {M : Type u_1} [inst : AddGroup M] (c : AddCon M) (n : ℤ) {w x : M}, c w x → c (n • w) (n • x)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsLittleO.trans_isEquivalent : ∀ {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [inst : NormedAddCommGroup β] [inst_1 : Norm β₂] {l : Filter α}
  {f : α → β₂} {g₁ g₂ : α → β}, f =o[l] g₁ → Asymptotics.IsEquivalent l g₁ g₂ → f =o[l] g₂
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.instIsGoodSymmOfRespectsIsoFibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A)
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C] [P.IsGood]
  [(HomotopicalAlgebra.fibrations C).RespectsIso], P.symm.IsGood
-- Mathlib.Algebra.Group.Graph
/-- **Vertical line test** for monoid homomorphisms.

Let `f : G → H × I` be a homomorphism to a product of monoids. Assume that `f` is surjective on the
first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at most
once. Then the image of `f` is the graph of some monoid homomorphism `f' : H → I`.  -/
MonoidHom.exists_mrange_eq_mgraph : ∀ {G : Type u_1} {H : Type u_2} {I : Type u_3} [inst : Monoid G] [inst_1 : Monoid H] [inst_2 : Monoid I]
  {f : G →* H × I},
  Function.Surjective (Prod.fst ∘ ⇑f) →
    (∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) → ∃ f', MonoidHom.mrange f = f'.mgraph
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.add_isLittleO : ∀ {f g : ℝ → ℝ},
  AkraBazziRecurrence.GrowsPolynomially f →
    g =o[Filter.atTop] f → AkraBazziRecurrence.GrowsPolynomially fun x => f x + g x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.mk : {X : SSet} →
  {A : X.Subcomplex} →
    (ι : Type v) →
      (dim : ι → ℕ) →
        (simplex : (s : ι) → X.obj (Opposite.op { len := dim s + 1 })) →
          (index : (s : ι) → Fin (dim s + 2)) →
            (∀ (s : ι), simplex s ∈ X.nonDegenerate (dim s + 1)) →
              (∀ (s : ι),
                  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index s))) (simplex s) ∈
                    X.nonDegenerate (dim s)) →
                (∀ (s : ι), simplex s ∉ A.obj (Opposite.op { len := dim s + 1 })) →
                  (∀ (s : ι),
                      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index s)))
                          (simplex s) ∉
                        A.obj (Opposite.op { len := dim s })) →
                    (∀ {s t : ι},
                        { dim := dim s + 1, simplex := simplex s } = { dim := dim t + 1, simplex := simplex t } →
                          s = t) →
                      (∀ {s t : ι},
                          { dim := dim s,
                                simplex :=
                                  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index s)))
                                    (simplex s) } =
                              { dim := dim t,
                                simplex :=
                                  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index t)))
                                    (simplex t) } →
                            s = t) →
                        (∀ (s t : ι),
                            { dim := dim s + 1, simplex := simplex s } ≠
                              { dim := dim t,
                                simplex :=
                                  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index t)))
                                    (simplex t) }) →
                          (∀ (x : A.N),
                              ∃ s,
                                x.toS = { dim := dim s + 1, simplex := simplex s } ∨
                                  x.toS =
                                    { dim := dim s,
                                      simplex :=
                                        (CategoryTheory.ConcreteCategory.hom
                                            (CategoryTheory.SimplicialObject.δ X (index s)))
                                          (simplex s) }) →
                            A.PairingCore
-- Mathlib.Topology.Semicontinuity.Basic
/-- An upper semicontinuous function is bounded above on a compact set.  -/
UpperSemicontinuousOn.bddAbove_of_isCompact : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} [inst_1 : LinearOrder β] {f : α → β} [Nonempty β]
  {s : Set α}, IsCompact s → UpperSemicontinuousOn f s → BddAbove (f '' s)
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_I : ∀ {K : Type u_1} [inst : RCLike K], ‖RCLike.I‖ = if RCLike.I = 0 then 0 else 1
-- Mathlib.Probability.Kernel.Disintegration.Density
MeasurableSpace.countablePartitionSet.congr_simp : ∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α] (n n_1 : ℕ),
  n = n_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (a_2 a_3 : α),
          a_2 = a_3 → MeasurableSpace.countablePartitionSet n a a_2 = MeasurableSpace.countablePartitionSet n_1 a_1 a_3
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.fst.eq_1 : ∀ (M : Type u_1) (α : Type u_2) (β : Type u_3) [inst : SMul M α] [inst_1 : SMul M β],
  MulActionHom.fst M α β = { toFun := Prod.fst, map_smul' := ⋯ }
-- Mathlib.RingTheory.Valuation.Basic
Valuation.isEquiv_map_self_of_strictMono : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v : Valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀) (H : StrictMono ⇑f),
  (Valuation.map f ⋯ v).IsEquiv v
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.polar.eq_1 : ∀ (R : Type u_4) [inst : NormedCommRing R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M], StrongDual.polar R = (topDualPairing R M).flip.polar
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {obj : C → D} {map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)}
  {map_id :
    autoParam (∀ (X : C), map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj X))
      CategoryTheory.Functor.map_id._autoParam}
  {map_comp :
    autoParam
      (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
        map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map f) (map g))
      CategoryTheory.Functor.map_comp._autoParam}
  {obj_1 : C → D} {map_1 : {X Y : C} → (X ⟶ Y) → (obj_1 X ⟶ obj_1 Y)}
  {map_id_1 :
    autoParam (∀ (X : C), map_1 (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj_1 X))
      CategoryTheory.Functor.map_id._autoParam}
  {map_comp_1 :
    autoParam
      (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
        map_1 (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map_1 f) (map_1 g))
      CategoryTheory.Functor.map_comp._autoParam},
  { obj := obj, map := map, map_id := map_id, map_comp := map_comp } =
      { obj := obj_1, map := map_1, map_id := map_id_1, map_comp := map_comp_1 } →
    obj = obj_1 ∧ map ≍ map_1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.tensorObj_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S : CategoryTheory.Over X),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom S.hom) R.hom
-- Init.Data.SInt.Lemmas
Int8.ofNat_sub : ∀ (a b : ℕ), b ≤ a → Int8.ofNat (a - b) = Int8.ofNat a - Int8.ofNat b
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.mkNatCastFn : {m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Monad m] → [Lean.Meta.Sym.Arith.MonadCanon m] → Lean.Level → Lean.Expr → Lean.Expr → m Lean.Expr
-- Lean.Elab.Tactic.Omega.MinNatAbs
Lean.Elab.Tactic.Omega.List.minNatAbs_nil : Lean.Elab.Tactic.Omega.List.minNatAbs [] = 0
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.moduleObj : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          (j : J) → Module R ((F.comp (CategoryTheory.forget (ModuleCat R))).obj j)
-- Mathlib.Data.Set.Prod
Set.Disjoint.set_prod_right : ∀ {α : Type u_1} {β : Type u_2} {t₁ t₂ : Set β}, Disjoint t₁ t₂ → ∀ (s₁ s₂ : Set α), Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂)
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hom_comp : ∀ {R : Type u} [inst : Semiring R] {M N O : SemimoduleCat R} (f : M ⟶ N) (g : N ⟶ O),
  SemimoduleCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = SemimoduleCat.Hom.hom g ∘ₗ SemimoduleCat.Hom.hom f
-- Mathlib.RingTheory.IdealFilter.Basic
IdealFilter.isTorsionQuot_def : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A} {L K : Ideal A},
  F.IsTorsionQuot L K ↔ ∀ k ∈ ↑K, ∃ I ∈ F, I ≤ Submodule.colon L {k}
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.support_div' : ∀ {ι : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] (f g : ι → G₀),
  Function.support (f / g) = Function.support f ∩ Function.support g
-- Batteries.Tactic.Lint.TypeClass
/-- Lints for instances with arguments that cannot be filled in, like
```
instance {α β : Type} [Group α] : Mul α where ...
```
 -/
Batteries.Tactic.Lint.impossibleInstance : Batteries.Tactic.Lint.Linter
-- Init.System.IO
/-- The type of handles that can be used to communicate with a child process on its standard input,
output, or error streams.

For `IO.Process.Stdio.piped`, this type is `IO.FS.Handle`. Otherwise, it is `Unit`, because no
communication is possible.
 -/
IO.Process.Stdio.toHandleType : IO.Process.Stdio → Type
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
CategoryTheory.Abelian.Ext.eq_zero_of_projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {P Y : C} {n : ℕ} [CategoryTheory.Projective P]
  (e : CategoryTheory.Abelian.Ext P Y (n + 1)), e = 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {f : α → β → Bool} {k : α},
  (Std.ExtDHashMap.filter f m).getKey! k =
    ((m.getKey? k).pfilter fun x_2 h' => f x_2 (Std.ExtDHashMap.Const.get m x_2 ⋯)).get!
-- Mathlib.Tactic.FunProp.Elab
_private.Mathlib.Tactic.FunProp.Elab.0.Mathlib.Meta.FunProp.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Meta.FunProp.Config
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Small
CategoryTheory.StructuredArrow.small_inverseImage_proj_of_locallySmall : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.Small.{v₁, v₁, u₁} P] [CategoryTheory.LocallySmall.{v₁, v₂, u₂} D],
  CategoryTheory.ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (CategoryTheory.StructuredArrow.proj S T))
-- Mathlib.Data.Complex.Basic
Complex.normSq_inv : ∀ (z : ℂ), Complex.normSq z⁻¹ = (Complex.normSq z)⁻¹
-- Lean.Parser.Term.Basic
Lean.Parser.Term.strictImplicitLeftBracket.formatter : Lean.PrettyPrinter.Formatter
-- Init.System.IOError
IO.Error.mkInappropriateType : UInt32 → String → IO.Error
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.trans_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃),
  (e.trans e').inv = CategoryTheory.CategoryStruct.comp e'.inv e.inv
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
DFinsupp.sigmaCurryEquiv.eq_1 : ∀ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : DecidableEq ι]
  [inst_1 : (i : ι) → (j : α i) → Zero (δ i j)],
  DFinsupp.sigmaCurryEquiv =
    { toFun := DFinsupp.sigmaCurry, invFun := DFinsupp.sigmaUncurry, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerLeft_trans_isoWhiskerRight_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D}
  {H K : CategoryTheory.Functor D E} (α : F ≅ G) (β : H ≅ K) {Z : CategoryTheory.Functor C E} (h : G.comp K ≅ Z),
  F.isoWhiskerLeft β ≪≫ CategoryTheory.Functor.isoWhiskerRight α K ≪≫ h =
    CategoryTheory.Functor.isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β ≪≫ h
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_le_one_iff_subsingleton : ∀ (α : Type u_3), ENat.card α ≤ 1 ↔ Subsingleton α
-- Mathlib.Algebra.BigOperators.Finprod
finsum_cond_eq_left : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {a : α}, ∑ᶠ (i : α) (_ : i = a), f i = f a
-- Mathlib.Analysis.Complex.Isometry
linear_isometry_complex : ∀ (f : ℂ ≃ₗᵢ[ℝ] ℂ), ∃ a, f = rotation a ∨ f = Complex.conjLIE.trans (rotation a)
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
/-- Usually `RootPairing.weylGroup.induction` will be more useful than this lemma.  -/
RootPairing.weylGroup_toSubmonoid : ∀ {ι : 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),
  P.weylGroup.toSubmonoid = Submonoid.closure (Set.range (RootPairing.Equiv.reflection P))
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.StrictSegal.mk.sizeOf_spec : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)}
  (spineToSimplex :
    (m : ℕ) →
      (h : autoParam (m ≤ n + 1) SSet.Truncated.StrictSegal._auto_1) →
        X.Path m → X.obj (Opposite.op { obj := { len := m }, property := h }))
  (spine_spineToSimplex : ∀ (m : ℕ) (h : m ≤ n + 1), X.spine m h ∘ spineToSimplex m ⋯ = id)
  (spineToSimplex_spine : ∀ (m : ℕ) (h : m ≤ n + 1), spineToSimplex m ⋯ ∘ X.spine m h = id),
  sizeOf
      { spineToSimplex := spineToSimplex, spine_spineToSimplex := spine_spineToSimplex,
        spineToSimplex_spine := spineToSimplex_spine } =
    1
-- Mathlib.Data.Sum.Interval
Sum.Lex.Iio_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Fintype α]
  [inst_3 : LocallyFiniteOrderBot α] [inst_4 : LocallyFiniteOrderBot β] (a : α),
  Finset.Iio (Sum.inlₗ a) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Iio a)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.IntegrableOn.mul_continuousOn : ∀ {X : Type u_1} {R : Type u_8} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] {K : Set X} [inst_3 : NormedRing R] [SecondCountableTopologyEither X R] {g g' : X → R}
  [T2Space X],
  MeasureTheory.IntegrableOn g K μ →
    ContinuousOn g' K → IsCompact K → MeasureTheory.IntegrableOn (fun x => g x * g' x) K μ
-- Mathlib.Data.Nat.Totient
/-- When `p` is prime, then the totient of `p ^ n` is `p ^ (n - 1) * (p - 1)`  -/
Nat.totient_prime_pow : ∀ {p : ℕ}, Nat.Prime p → ∀ {n : ℕ}, 0 < n → (p ^ n).totient = p ^ (n - 1) * (p - 1)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.rotate.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] (c : G.Walk v v) (u : V) (h : u ∈ c.support),
  c.rotate u h = (c.dropUntil u h).append (c.takeUntil u h)
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
/-- The canonical map `T ⊗[R] P.H1Cotangent →ₗ[T] (P.baseChange).H1Cotangent`.  -/
Algebra.Extension.tensorToH1Cotangent : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (P : Algebra.Extension R S) →
            (T : Type u_3) →
              [inst_3 : CommRing T] →
                [inst_4 : Algebra R T] → TensorProduct R T P.H1Cotangent →ₗ[T] P.baseChange.H1Cotangent
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.prodL_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} (S : Type u_5) [inst : NormedField 𝕜]
  [inst_1 : Semiring S] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜 F] [inst_10 : AddCommGroup G] [inst_11 : Module 𝕜 G] [inst_12 : TopologicalSpace G]
  [inst_13 : IsTopologicalAddGroup G] [inst_14 : ContinuousConstSMul 𝕜 G] [inst_15 : Module S G]
  [inst_16 : SMulCommClass 𝕜 S G] [inst_17 : ContinuousConstSMul S G] [inst_18 : Module S F]
  [inst_19 : SMulCommClass 𝕜 S F] [inst_20 : ContinuousConstSMul S F] (a : (E →L[𝕜] F) × (E →L[𝕜] G)),
  (ContinuousLinearMap.prodL S) a = a.1.prod a.2
-- Mathlib.Data.Sign.Defs
SignType.LE.of_neg : ∀ (a : SignType), SignType.neg.LE a
-- Mathlib.RingTheory.SimpleModule.Basic
IsSimpleModule.ker_toSpanSingleton_isMaximal : ∀ (R : Type u_2) [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSimpleModule R M]
  {m : M}, m ≠ 0 → Ideal.IsMaximal (LinearMap.toSpanSingleton R M m).ker
-- Mathlib.Algebra.Homology.Square
/-- The limit kernel fork attached to a pullback square.  -/
CategoryTheory.Square.IsPullback.isLimitKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {sq : CategoryTheory.Square C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct sq.X₂ sq.X₃] →
          sq.IsPullback → CategoryTheory.Limits.IsLimit sq.kernelFork
-- Batteries.Tactic.Alias
Batteries.Tactic.Alias.AliasInfo.reverse.injEq : ∀ (n n_1 : Lean.Name),
  (Batteries.Tactic.Alias.AliasInfo.reverse n = Batteries.Tactic.Alias.AliasInfo.reverse n_1) = (n = n_1)
-- Mathlib.Data.QPF.Multivariate.Constructions.Const
MvQPF.Const.mk_get : ∀ {n : ℕ} {A : Type u} {α : TypeVec.{u} n} (x : MvQPF.Const n A α), MvQPF.Const.mk x.get = x
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- An open immersion is isomorphic to the induced open subscheme on its image.  -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict : {X Y : AlgebraicGeometry.LocallyRingedSpace} →
  (f : X ⟶ Y) → [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] → X ≅ Y.restrict ⋯
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.relabel_congr : ∀ {α : Type u_1} {β : Type u_2} {f : Std.Sat.CNF α} {r1 r2 : α → β},
  (∀ (v : α), Std.Sat.CNF.VarMem v f → r1 v = r2 v) → Std.Sat.CNF.relabel r1 f = Std.Sat.CNF.relabel r2 f
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.subst_into_negg : ∀ {α : Type u_1} [inst : AddCommGroup α] (a ta t : α), a = ta → -ta = t → -a = t
-- Init.Data.Range.Polymorphic.Basic
Std.Rci.mem_iff : ∀ {α : Type u} {r : Std.Rci α} {a : α} [inst : LE α], a ∈ r ↔ r.lower ≤ a
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_ge : ∀ {n : ℕ} {i j : Fin n}, i ≤ j → ∀ [NeZero n], j.cycleIcc i = 1
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.mem_edgeSet_image : ∀ {α : Type u_1} {β : Type u_2} {H : Hypergraph α} {f : α → β} {e : Set β},
  e ∈ (H.image f).edgeSet ↔ ∃ e' ∈ H.edgeSet, f '' e' = e
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_toReal_add_abs_toReal_eq_pi_of_two_nsmul_add_eq_zero_of_sign_eq : ∀ {θ ψ : Real.Angle}, 2 • (θ + ψ) = 0 → θ.sign = ψ.sign → θ.sign ≠ 0 → |θ.toReal| + |ψ.toReal| = Real.pi
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → SeparatedNhds t s
-- Mathlib.Algebra.Field.Periodic
Function.Periodic.const_mul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : DivisionSemiring α],
  Function.Periodic f c → ∀ (a : α), Function.Periodic (fun x => f (a * x)) (a⁻¹ * c)
-- Init.Data.Ord.Basic
/-- Constructs an `Ord` instance that compares values according to the results of `f`.

In particular, `ord.on f` compares `x` and `y` by comparing `f x` and `f y` according to `ord`.

The function `compareOn` can be used to perform this comparison without constructing an intermediate
`Ord` instance.
 -/
Ord.on : {β : Type u_1} → {α : Type u_2} → Ord β → (α → β) → Ord α
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the number of elements contained in the given closed range.
 -/
Std.Rio.size : {α : Type u} → [Std.Rxo.HasSize α] → [Std.PRange.Least? α] → Std.Rio α → ℕ
-- Lean.Parser.Types
Lean.Parser.ParserState.cache : Lean.Parser.ParserState → Lean.Parser.ParserCache
-- Mathlib.Algebra.Module.Projective
/-- A variant of `Projective.iff_split` allowing for a more flexible selection of the universe
for the free module `M`.  -/
Module.Projective.iff_split' : ∀ {R : Type u} [inst : Semiring R] {P : Type v} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] [Small.{w, u} R]
  [Small.{w, v} P], Module.Projective R P ↔ ∃ M x x_1, ∃ (_ : Module.Free R M), ∃ i s, s ∘ₗ i = LinearMap.id
-- Init.Data.UInt.Lemmas
USize.le_ofNat_iff : ∀ {n : USize} {m : ℕ}, m < USize.size → (n ≤ USize.ofNat m ↔ n.toNat ≤ m)
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.State.mk : Array (Lean.Expr × Lean.Expr × ℕ) → Std.HashSet Lean.FVarId → Aesop.RuleTac.ForwardM.State
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_subset_Ioc_union_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioo a c ⊆ Set.Ioc a b ∪ Set.Ioo b c