mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.NhdsSet
Ioo_mem_nhdsSet_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c d : α},
  a < b → c ≤ d → Set.Ioo a d ∈ nhdsSet (Set.Ico b c)
-- Init.Data.Option.List
Option.toList_filter : ∀ {α : Type u_1} {o : Option α} {p : α → Bool}, (Option.filter p o).toList = List.filter p o.toList
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
IsAdic.hasBasis_nhds : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] {I : Ideal R},
  IsAdic I → ∀ (x : R), (nhds x).HasBasis (fun x => True) fun n => (fun x_1 => x + x_1) '' ↑(I ^ n)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.summable_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {x : ℕ → MvPowerSeries σ R} [inst_3 : UniformSpace R]
  [DiscreteUniformity R] [inst_5 : UniformSpace S] [DiscreteUniformity S],
  Summable x → MvPowerSeries.HasSubst a → Summable fun i => MvPowerSeries.subst a (x i)
-- Mathlib.Algebra.Star.StarAlgHom
/-- Taking the product of two maps with the same domain is equivalent to taking the product of
their codomains.  -/
NonUnitalStarAlgHom.prodEquiv : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : Monoid R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : DistribMulAction R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalNonAssocSemiring B] →
                  [inst_5 : DistribMulAction R B] →
                    [inst_6 : Star B] →
                      [inst_7 : NonUnitalNonAssocSemiring C] →
                        [inst_8 : DistribMulAction R C] →
                          [inst_9 : Star C] → (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C) ≃ (A →⋆ₙₐ[R] B × C)
-- Init.Data.List.Perm
_private.Init.Data.List.Perm.0.List.foldl.match_1.eq_1 : ∀ {α : Type u_3} {β : Type u_1} (motive : α → List β → Sort u_2) (a : α) (h_1 : (a : α) → motive a [])
  (h_2 : (a : α) → (b : β) → (l : List β) → motive a (b :: l)),
  (match a, [] with
    | a, [] => h_1 a
    | a, b :: l => h_2 a b l) =
    h_1 a
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.brecOn_2.eq : ∀ {motive_1 : Aesop.Script.StepTree → Sort u} {motive_2 : Array Aesop.Script.StepTree → Sort u}
  {motive_3 : List Aesop.Script.StepTree → Sort u} (t : List Aesop.Script.StepTree)
  (F_1 : (t : Aesop.Script.StepTree) → t.below → motive_1 t)
  (F_2 : (t : Array Aesop.Script.StepTree) → Aesop.Script.StepTree.below_1 t → motive_2 t)
  (F_3 : (t : List Aesop.Script.StepTree) → Aesop.Script.StepTree.below_2 t → motive_3 t),
  Aesop.Script.StepTree.brecOn_2 t F_1 F_2 F_3 = F_3 t (Aesop.Script.StepTree.brecOn_2.go t F_1 F_2 F_3).2
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_containsKey_of_containsKey_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getKeyD k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) fallback = fallback
-- Lean.Elab.Do.Legacy
/-- Create a new join point for `c`, and jump to it with the variables `rs`  -/
Lean.Elab.Term.Do.mkSimpleJmp : Lean.Syntax →
  Lean.Elab.Term.Do.VarSet →
    Lean.Elab.Term.Do.Code →
      StateRefT' IO.RealWorld (Array Lean.Elab.Term.Do.JPDecl) Lean.Elab.TermElabM Lean.Elab.Term.Do.Code
-- Std.Time.Format.Basic
/-- Formats the date using the format into a String, using a `getInfo` function to get the information needed to build the `String`.
 -/
Std.Time.GenericFormat.formatGeneric : {aw : Std.Time.Awareness} →
  Std.Time.GenericFormat aw → ((typ : Std.Time.Modifier) → Option (Std.Time.TypeFormat typ)) → Option String
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.map_sub : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] {X Y : C} {f g : X ⟶ Y},
  F.map (f - g) = F.map f - F.map g
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the second of three points is weakly between the other two, the oriented angle at the
third point is zero.  -/
Wbtw.oangle₂₃₁_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, Wbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₂ p₃ p₁ = 0
-- Lean.Expr
/-- Return `true` if the given expression is of the form `.sort (.succ .zero)`.  -/
Lean.Expr.isType0 : Lean.Expr → Bool
-- Mathlib.CategoryTheory.Retract
/-- the split monomorphism  -/
CategoryTheory.Retract.i : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → CategoryTheory.Retract X Y → (X ⟶ Y)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → (m₁ \ m₂).get? k = none
-- Mathlib.CategoryTheory.CofilteredSystem
/-- The subfunctor of `F` obtained by restricting to the preimages of a set `s ∈ F.obj i`.  -/
CategoryTheory.Functor.toPreimages : {J : Type u} →
  [inst : CategoryTheory.Category.{v_1, u} J] →
    (F : CategoryTheory.Functor J (Type v)) → {i : J} → Set (F.obj i) → CategoryTheory.Functor J (Type v)
-- Mathlib.Analysis.Fourier.AddCircle
fourierLp.congr_simp : ∀ {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [inst : Fact (1 ≤ p)] (n n_1 : ℤ), n = n_1 → fourierLp p n = fourierLp p n_1
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.overToCoalgebra_map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {X_1 Y : CategoryTheory.Over X} (g : X_1 ⟶ Y),
  ((CategoryTheory.overToCoalgebra X).map g).f = CategoryTheory.Over.Hom.left g
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv.congr_simp : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p p_1 : α} (e_p : p = p_1) (hp : 0 < p) (a a_1 : α),
  a = a_1 → ∀ (b b_1 : α), b = b_1 → toIcoDiv hp a b = toIcoDiv ⋯ a_1 b_1
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_fst_eq_mul_inv : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) (g : G),
  ↑(hST.equiv g).1 = g * (↑(hST.equiv g).2)⁻¹
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below : {R : Type u_1} →
  {X : Type u_2} →
    [inst : CommSemiring R] →
      {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} →
        {a a_1 : FreeAlgebra.Pre R X} → FreeAlgebra.Rel R X a a_1 → Prop
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.functor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (T : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y),
  (CategoryTheory.CostructuredArrow.functor T).map f = (CategoryTheory.CostructuredArrow.map f).toCatHom
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
/-- The maps form a commuting triangle  -/
MonoidHom.CompTriple.comp_eq : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} {inst : Monoid M} {inst_1 : Monoid N} {inst_2 : Monoid P} {φ : M →* N}
  {ψ : N →* P} {χ : outParam (M →* P)} [self : φ.CompTriple ψ χ], ψ.comp φ = χ
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)],
  CategoryTheory.IsIso (HomotopicalAlgebra.CofibrantObject.HoCat.resolutionCompToLocalizationNatTrans L)
-- Mathlib.Topology.MetricSpace.CantorScheme
/-- If `x` is in the domain of the induced map of a scheme `A`,
its image under this map is in each set along the corresponding branch.  -/
CantorScheme.map_mem : ∀ {β : Type u_1} {α : Type u_2} {A : List β → Set α} (x : ↑(CantorScheme.inducedMap A).fst) (n : ℕ),
  (CantorScheme.inducedMap A).snd x ∈ A (PiNat.res (↑x) n)
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.invOneClass : {α : Type u_1} → [InvOneClass α] → InvOneClass (WithZero α)
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.partition_fst : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool},
  (Std.TreeSet.Raw.partition f t).1.WF
-- Init.Control.Lawful.Instances
ExceptT.bindCont.eq_1 : ∀ {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α β : Type u} (f : α → ExceptT ε m β) (a : α),
  ExceptT.bindCont f (Except.ok a) = f a
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Construct an isomorphism of additive group objects by giving an isomorphism between
the underlying objects and checking compatibility with zero and addition only in the
forward direction.  -/
CategoryTheory.AddGrp.mkIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G H : CategoryTheory.AddGrp C} →
        (e : G.X ≅ H.X) →
          autoParam
              (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero)
              CategoryTheory.AddGrp.mkIso._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
                    CategoryTheory.AddMonObj.add)
                CategoryTheory.AddGrp.mkIso._auto_3 →
              (G ≅ H)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trCfg.congr_simp : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (enc enc_1 : Γ → List.Vector Bool n) (e_enc : enc = enc_1)
  [inst : Inhabited Γ] (enc0 : enc default = List.Vector.replicate n false) (a a_1 : Turing.TM1.Cfg Γ Λ σ),
  a = a_1 → Turing.TM1to1.trCfg enc enc0 a = Turing.TM1to1.trCfg enc_1 ⋯ a_1
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_apply_mono_left : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] (u : ι → Ω → β) (s : Set β)
  (m : ι) (ω : Ω), Monotone fun x => MeasureTheory.hittingBtwn u s x m ω
-- Mathlib.Control.Monad.Cont
ContT.withContT : {r : Type u} → {m : Type u → Type v} → {α β : Type w} → ((β → m r) → α → m r) → ContT r m α → ContT r m β
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- `monomial` approximates the monomial function.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial_approximates : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {n : Fin (List.length basis)},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    (Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial basis ↑n).Approximates
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Characterization of multiplication  -/
HomotopyGroup.mul_spec : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] [inst_2 : Nonempty N]
  {i : N} {p q : ↑(GenLoop N X x)}, (fun x1 x2 => x1 * x2) ⟦p⟧ ⟦q⟧ = ⟦GenLoop.transAt i q p⟧
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_eq' : ∀ (a : ℤ) (b : ℕ), a <<< b = a * ↑(2 ^ b)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- For vector spaces `E`, there is a canonical map `StrongDual 𝕜 E → WeakDual 𝕜 E` (the "identity"
mapping). It is a linear equivalence.  -/
StrongDual.toWeakDual : {𝕜 : Type u_2} →
  {E : Type u_4} →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → StrongDual 𝕜 E ≃ₗ[𝕜] WeakDual 𝕜 E
-- Mathlib.RingTheory.Finiteness.Defs
Submodule.fg_iff_exists_fin_generating_family : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, N.FG ↔ ∃ n s, Submodule.span R (Set.range s) = N
-- Init.Data.List.Basic
List.take_nil : ∀ {α : Type u} {i : ℕ}, List.take i [] = []
-- Mathlib.RingTheory.Congruence.Defs
RingCon.comap_ringHomComp : ∀ {R : Type u_5} {R' : Type u_6} {R'' : Type u_7} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring R']
  [inst_2 : NonAssocSemiring R''] (J : RingCon R) (g : R' →+* R) (f : R'' →+* R'),
  J.comap (g.comp f) = (J.comap g).comap f
-- Mathlib.Data.Fintype.Basic
Fin.image_succ_univ : ∀ (n : ℕ), Finset.image Fin.succ Finset.univ = {0}ᶜ
-- Mathlib.Order.WithBot
/-- The image of a binary function `f : α → β → γ` as a function
`WithBot α → WithBot β → WithBot γ`.

Mathematically this should be thought of as the image of the corresponding function `α × β → γ`.  -/
WithBot.map₂ : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β → γ) → WithBot α → WithBot β → WithBot γ
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_containsKey_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true →
    (List.map Sigma.fst toInsert).contains k = false → Std.Internal.List.containsKey k l = true
-- Mathlib.Algebra.GroupWithZero.Units.Basic
not_isUnit_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀], ¬IsUnit 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CtorInfo.usize : Lean.Compiler.LCNF.CtorInfo → ℕ
-- Mathlib.Topology.Algebra.Group.Basic
continuous_neg_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G]
  [inst_3 : TopologicalSpace α] {f : α → G}, Continuous (-f) ↔ Continuous f
-- Mathlib.CategoryTheory.Limits.Final.Type
/-- When `F : C ⥤ D` and `P : D ⥤ Type _`, this is the obvious map
`P.sections → (F ⋙ P).sections`.  -/
CategoryTheory.Functor.sectionsPrecomp : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → {P : CategoryTheory.Functor D (Type w)} → ↑P.sections → ↑(F.comp P).sections
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.norm_mapL_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →L[𝕜] F) (g : G →L[𝕜] H),
  ‖TensorProduct.mapL f g‖ ≤ ‖f‖ * ‖g‖
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).inv.hom₁ =
    CategoryTheory.CategoryStruct.id X₁
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The constructed fan is indeed a limit  -/
TopCat.piFanIsLimit : {ι : Type v} → (α : ι → TopCat) → CategoryTheory.Limits.IsLimit (TopCat.piFan α)
-- Mathlib.Order.SetAccumulate
Set.iUnion_accumulate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α], ⋃ x, Set.accumulate s x = ⋃ x, s x
-- Init.SimpLemmas
dite_true : ∀ {α : Sort u} {t : True → α} {e : ¬True → α}, dite True t e = t True.intro
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
AddOpposite.unop_finsuppProd : ∀ {ι : Type u_16} {M : Type u_17} {N : Type u_18} [inst : CommMonoid M] [inst_1 : Zero N] (f : ι →₀ N)
  (g : ι → N → Mᵐᵒᵖ), AddOpposite.unop (f.prod g) = f.prod fun i n => AddOpposite.unop (g i n)
-- Init.Control.State
/-- Replaces the mutable state with a new value.
 -/
StateT.set : {σ : Type u} → {m : Type u → Type v} → [Monad m] → σ → StateT σ m PUnit.{u + 1}
-- Mathlib.Algebra.GroupWithZero.Basic
one_div_ne_zero : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → 1 / a ≠ 0
-- Mathlib.Data.Set.Operations
/-- Given an index set `ι` and a family of sets `t : Π i, Set (α i)`, `pi s t`
is the set of dependent functions `f : Πa, π a` such that `f i` belongs to `t i`
whenever `i ∈ s`.  -/
Set.pi : {ι : Type u_1} → {α : ι → Type u_2} → Set ι → ((i : ι) → Set (α i)) → Set ((i : ι) → α i)
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_smul : ∀ {α : Type u_1} {F : Type u_3} {𝕜 : Type u_6} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_7} [inst_2 : NormedAddCommGroup E]
  [inst_3 : SMulZeroClass 𝕜 E] [inst_4 : NormedSpace ℝ E] [inst_5 : DistribSMul 𝕜 F] (T : Set α → E →L[ℝ] F),
  MeasureTheory.FinMeasAdditive μ T →
    (∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) →
      ∀ (c : 𝕜) {f : MeasureTheory.SimpleFunc α E},
        MeasureTheory.Integrable (⇑f) μ →
          MeasureTheory.SimpleFunc.setToSimpleFunc T (c • f) = c • MeasureTheory.SimpleFunc.setToSimpleFunc T f
-- Lean.Environment
Lean.Kernel.Exception.declTypeMismatch.sizeOf_spec : ∀ (env : Lean.Kernel.Environment) (decl : Lean.Declaration) (givenType : Lean.Expr),
  sizeOf (Lean.Kernel.Exception.declTypeMismatch env decl givenType) = 1 + sizeOf env + sizeOf decl + sizeOf givenType
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.of_le_of_exists_dvd : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (N : Submonoid R), M ≤ N → (∀ n ∈ N, ∃ m ∈ M, n ∣ m) → IsLocalization N S
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Oriented angle version of "angles in same segment are equal" and "opposite angles of a
cyclic quadrilateral add to π", for oriented angles mod π (for which those are the same result),
represented here as equality of twice the angles.  -/
EuclideanGeometry.Sphere.two_zsmul_oangle_eq : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ p₄ : P},
  p₁ ∈ s →
    p₂ ∈ s →
      p₃ ∈ s →
        p₄ ∈ s →
          p₂ ≠ p₁ →
            p₂ ≠ p₄ → p₃ ≠ p₁ → p₃ ≠ p₄ → 2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)},
  IsLowerSet ↑s →
    ∀ {x : σ →₀ ℕ} (f g : MvPowerSeries σ R),
      x ∈ s →
        MvPolynomial.coeff x ((MvPowerSeries.truncFinset R s) f * (MvPowerSeries.truncFinset R s) g) =
          (MvPowerSeries.coeff x) (f * g)
-- Mathlib.ModelTheory.Basic
/-- An equivalence of first-order structures is an equivalence that commutes with the
interpretations of functions and relations.  -/
FirstOrder.Language.Equiv : (L : FirstOrder.Language) → (M : Type w) → (N : Type w') → [L.Structure M] → [L.Structure N] → Type (max w w')
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- If the pushout comparison map for `G` at `(f,g)` is an isomorphism, then `G` preserves the
pushout of `(f,g)`.  -/
CategoryTheory.Limits.PreservesPushout.of_iso_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [inst_2 : CategoryTheory.Limits.HasPushout f g]
  [inst_3 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
  [i : CategoryTheory.IsIso (CategoryTheory.Limits.pushoutComparison G f g)],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G
-- Mathlib.Order.Filter.Prod
Filter.prod_le_prod : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} [f₁.NeBot] [g₁.NeBot],
  f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂ ↔ f₁ ≤ f₂ ∧ g₁ ≤ g₂
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsTrivialBlock.preimage : ∀ {M : Type u_3} {α : Type u_4} {N : Type u_5} {β : Type u_6} [inst : Monoid M] [inst_1 : MulAction M α]
  [inst_2 : Monoid N] [inst_3 : MulAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Injective ⇑f → ∀ {B : Set β}, MulAction.IsTrivialBlock B → MulAction.IsTrivialBlock (⇑f ⁻¹' B)
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.valuedCompletion_surjective_iff : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀],
  Function.Surjective ⇑Valued.v ↔ Function.Surjective ⇑Valued.v
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.subtypeL_comp_codRestrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂)
  (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p), p.subtypeL ∘SL f.codRestrict p h = f
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_neg : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.variance (-X) μ = ProbabilityTheory.variance X μ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceDvd : Lean.Meta.Simp.Simproc
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_isColoop_iff : ∀ {α : Type u_1} {e : α} (M : Matroid α) (D : Set α),
  (M.delete D).IsColoop e ↔ e ∉ M.closure ((M.E \ D) \ {e}) ∧ e ∈ M.E ∧ e ∉ D
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousWithinAt.zpow : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G} {x : α} {s : Set α},
  ContinuousWithinAt f s x → ∀ (z : ℤ), ContinuousWithinAt (f ^ z) s x
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.maxEntry.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (x_1 : x.isEmpty = false) →
          ((size : ℕ) →
              (k : α) →
                (v : β) →
                  (l : Std.DTreeMap.Internal.Impl α fun x => β) →
                    (x :
                        (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
                      motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (l : Std.DTreeMap.Internal.Impl α fun x => β) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β) →
                            (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                              (h :
                                  (Std.DTreeMap.Internal.Impl.inner size k v l
                                        (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
                                    false) →
                                motive
                                  (Std.DTreeMap.Internal.Impl.inner size k v l
                                    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
                                  h) →
              motive x x_1