mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swap.match_1.eq_4 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Sort u_2) (a : α) (xs : List α) (i : ℕ)
  (h_1 : (x x_1 : ℕ) → motive [] x x_1) (h_2 : (a : α) → (xs : List α) → motive (a :: xs) 0 0)
  (h_3 : (a : α) → (xs : List α) → (i : ℕ) → motive (a :: xs) 0 i.succ)
  (h_4 : (a : α) → (xs : List α) → (i : ℕ) → motive (a :: xs) i.succ 0)
  (h_5 : (a : α) → (xs : List α) → (i j : ℕ) → motive (a :: xs) i.succ j.succ),
  (match a :: xs, i.succ, 0 with
    | [], x, x_1 => h_1 x x_1
    | a :: xs, 0, 0 => h_2 a xs
    | a :: xs, 0, i.succ => h_3 a xs i
    | a :: xs, i.succ, 0 => h_4 a xs i
    | a :: xs, i.succ, j.succ => h_5 a xs i j) =
    h_4 a xs i
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.trans_isLittleOTVS : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G}, f =O[𝕜; l] g → g =o[𝕜; l] k → f =o[𝕜; l] k
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.of_equiv_equiv : ∀ {F : Type u_1} {E : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {M : Type u_5} {N : Type u_6}
  [inst_3 : Field N] [inst_4 : Field M] [inst_5 : Algebra M N] [h : IsGalois F E] {f : F ≃+* M} {g : E ≃+* N},
  (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E) → IsGalois M N
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift_word_prod_nontrivial_of_other_i : ∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] {H : ι → Type u_5} [inst_1 : (i : ι) → Group (H i)]
  (f : (i : ι) → H i →* G) {α : Type u_6} [inst_2 : MulAction G α] (X : ι → Set α),
  (∀ (i : ι), (X i).Nonempty) →
    Pairwise (Function.onFun Disjoint X) →
      (Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i) →
        ∀ {i j k : ι} (w : Monoid.CoprodI.NeWord H i j), k ≠ i → k ≠ j → (Monoid.CoprodI.lift f) w.prod ≠ 1
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X],
  CategoryTheory.CategoryStruct.comp X.toSpecΓ X.isoSpec.inv = CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The underlying morphism  -/
CategoryTheory.CommRingObjCat.Hom.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {R₁ R₂ : CategoryTheory.CommRingObjCat C} → R₁.Hom R₂ → (R₁.X ⟶ R₂.X)
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.le_enumOrd_self : ∀ {s : Set Ordinal.{u}}, ¬BddAbove s → ∀ {a : Ordinal.{u}}, a ≤ Ordinal.enumOrd s a
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.bind : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] {α β : Type u} {x : m α}
  {f : α → m β} {Q : Std.Do.PostCond β ps},
  ⦃(Std.Do.wp x).apply (fun a => (Std.Do.wp (f a)).apply Q, Q.2)⦄ (x >>= f) ⦃Q⦄
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.rightCont_self : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : PartialOrder ι] (𝓕 : MeasureTheory.Filtration ι m),
  𝓕.rightCont.rightCont = 𝓕.rightCont
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.oreDiv_mul_oreDiv_comm : ∀ {R : Type u_1} [inst : CommMonoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {r₁ r₂ : R} {s₁ s₂ : ↥S},
  r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.isAdmissible_iff : ∀ (m : ℕ) (L : List ℕ),
  SimplexCategoryGenRel.IsAdmissible m L ↔
    L = [] ∨
      (∃ a ≤ m, L = [a]) ∨
        ∃ a b L', a < b ∧ SimplexCategoryGenRel.IsAdmissible (m + 1) (b :: L') ∧ a ≤ m ∧ L = a :: b :: L'
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
MvQPF.Sigma.repr.eq_1 : ∀ {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [inst : (α : A) → MvQPF (F α)] ⦃α : TypeVec.{u} n⦄ (a : A)
  (x_1 : F a α), MvQPF.Sigma.repr F ⟨a, x_1⟩ = ⟨⟨a, (MvQPF.repr x_1).fst⟩, (MvQPF.repr x_1).snd⟩
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.sUnion_singleton : ∀ {x : ZFSet.{u}}, {x}.sUnion = x
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.linearMapLeftRightHom_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {P : Type u_5} [inst_7 : AddCommMonoid P] [inst_8 : Module R P] {Q : Type u_6} [inst_9 : AddCommMonoid Q]
  [inst_10 : Module R Q] [inst_11 : Module S P] [inst_12 : IsScalarTower R S P] [inst_13 : Module S Q]
  [inst_14 : IsScalarTower R S Q] {α : M →ₗ[R] P} (j : IsBaseChange S α) (β : N →ₗ[R] Q) (f : M →ₗ[R] N),
  ↑R ((j.linearMapLeftRightHom β) f) ∘ₗ α = β ∘ₗ f
-- Mathlib.Topology.UniformSpace.CompareReals
CompareReals.instCommRingQ : CommRing CompareReals.Q
-- Mathlib.RingTheory.Valuation.RankOne
instRankOneValueGroupWithZeroValuationOfIsNontrivialOfIsRankLeOne : {R : Type u_3} →
  [inst : Ring R] →
    [inst_1 : ValuativeRel R] →
      [ValuativeRel.IsNontrivial R] → [ValuativeRel.IsRankLeOne R] → (ValuativeRel.valuation R).RankOne
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.UnitLike.instInhabitedState : Inhabited Lean.Meta.Grind.UnitLike.State
-- Mathlib.Data.Finsupp.Single
/-- `erase a f` is the finitely supported function equal to `f` except at `a` where it is equal to `0`.
If `a` is not in the support of `f` then `erase a f = f`.
 -/
Finsupp.erase : {α : Type u_1} → {M : Type u_5} → [inst : Zero M] → α → (α →₀ M) → α →₀ M
-- Mathlib.Order.Hom.Basic
map_lt_map_iff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : EquivLike F α β]
  [OrderIsoClass F α β] (f : F) {a b : α}, f a < f b ↔ a < b
-- Mathlib.Algebra.Group.Conj
AddConjClasses.instZero : {α : Type u} → [inst : AddMonoid α] → Zero (AddConjClasses α)
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a `Cone F` into a `Cocone F.op`.  -/
CategoryTheory.Limits.Cone.op : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.Cone F → CategoryTheory.Limits.Cocone F.op
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `s` is a colimit cokernel cofork, then every `k : Y ⟶ W` satisfying `f ≫ k = 0` induces
`l : s.X ⟶ W` such that `cofork.π s ≫ l = k`.  -/
CategoryTheory.Limits.CokernelCofork.IsColimit.desc' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {s : CategoryTheory.Limits.CokernelCofork f} →
            CategoryTheory.Limits.IsColimit s →
              {W : C} →
                (k : Y ⟶ W) →
                  CategoryTheory.CategoryStruct.comp f k = 0 →
                    { l // CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π s) l = k }
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.enum_type : ∀ {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s]
  (f : PrincipalSeg s r) {h : Ordinal.type s < Ordinal.type r}, (Ordinal.enum r) ⟨Ordinal.type s, h⟩ = f.top
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionRight_mop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : C) {d d' : D} (f : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight { unmop := c } f =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.MonadMor₁.mk : {m : Type → Type} →
  (Mathlib.Tactic.BicategoryLike.Obj → m Mathlib.Tactic.BicategoryLike.Mor₁) →
    (Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₁) →
      Mathlib.Tactic.BicategoryLike.MonadMor₁ m
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
EReal.borelSpace : BorelSpace EReal
-- Mathlib.Order.Disjoint
bot_codisjoint : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {a : α}, Codisjoint ⊥ a ↔ a = ⊤
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3}
  {E : Type u_4} [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  {FD : D → D → Type u_5} {CD : D → Type u_6} {FE : E → E → Type u_7} {CE : E → Type u_8}
  [inst_9 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_10 : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)]
  [instCCD : CategoryTheory.ConcreteCategory D FD] [instCCE : CategoryTheory.ConcreteCategory E FE]
  [inst_11 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_12 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)]
  [inst_13 :
    CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (CategoryTheory.forget D)]
  [inst_14 :
    CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (CategoryTheory.forget E)]
  [inst_15 : (CategoryTheory.forget D).ReflectsIsomorphisms] [inst_16 : (CategoryTheory.forget E).ReflectsIsomorphisms]
  (P : CategoryTheory.Functor Cᵒᵖ D),
  (CategoryTheory.sheafToPresheaf J E).map
      ((CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D)
            (CategoryTheory.plusPlusAdjunction J E)).app
        P) =
    (J.sheafifyCompIso F P).inv
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.cos_arcsin_nonneg : ∀ (x : ℝ), 0 ≤ Real.cos (Real.arcsin x)
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LiftSourceTargetPropertyAt.mem_codChart_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop}
  (h : Manifold.LiftSourceTargetPropertyAt I J n f x P), f x ∈ h.codChart.source
-- Mathlib.Topology.Sheaves.Flasque
CategoryTheory.Functor.whiskerRight.hcongr_10 : ∀ (C C' : Type u₁),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v₁, u₁} C) (inst' : CategoryTheory.Category.{v₁, u₁} C'),
      inst ≍ inst' →
        ∀ (D D' : Type u₂),
          D = D' →
            ∀ (inst_1 : CategoryTheory.Category.{v₂, u₂} D) (inst'_1 : CategoryTheory.Category.{v₂, u₂} D'),
              inst_1 ≍ inst'_1 →
                ∀ (E E' : Type u₃),
                  E = E' →
                    ∀ (inst_2 : CategoryTheory.Category.{v₃, u₃} E) (inst'_2 : CategoryTheory.Category.{v₃, u₃} E'),
                      inst_2 ≍ inst'_2 →
                        ∀ (G : CategoryTheory.Functor C D) (G' : CategoryTheory.Functor C' D'),
                          G ≍ G' →
                            ∀ (H : CategoryTheory.Functor C D) (H' : CategoryTheory.Functor C' D'),
                              H ≍ H' →
                                ∀ (α : G ⟶ H) (α' : G' ⟶ H'),
                                  α ≍ α' →
                                    ∀ (F : CategoryTheory.Functor D E) (F' : CategoryTheory.Functor D' E'),
                                      F ≍ F' →
                                        CategoryTheory.Functor.whiskerRight α F ≍
                                          CategoryTheory.Functor.whiskerRight α' F'
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  l.contains k = false → (Std.TreeSet.ofList l cmp).get? k = none
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
/-- The set of measures of the set of measurable negative sets.  -/
MeasureTheory.SignedMeasure.measureOfNegatives : {α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.SignedMeasure α → Set ℝ
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φQ =
    CategoryTheory.Limits.Cofork.π c
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityInt8HAndNegOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 &&& x2) (-1)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- If `w : InfinitePlace L` lies above `v : InfinitePlace K`, then either `w.embedding`
extends `v.embedding` as complex embeddings, or `conjugate w.embedding` extends `v.embedding`.  -/
NumberField.InfinitePlace.LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eq : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) [w.LiesOver v],
  w.embedding.comp (algebraMap K L) = v.embedding ∨
    (NumberField.ComplexEmbedding.conjugate w.embedding).comp (algebraMap K L) = v.embedding
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.instIteratorLoop : {α β : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      {n : Type x → Type x'} →
        [Monad n] →
          {P : β → Prop} → [inst_2 : Std.Iterator α m β] → Std.IteratorLoop (Std.Iterators.Types.Attach α m P) m n
-- Mathlib.Combinatorics.Hindman
Ultrafilter.mul.eq_1 : ∀ {M : Type u_1} [inst : Mul M], Ultrafilter.mul = { mul := fun U V => (fun x1 x2 => x1 * x2) <$> U <*> V }
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_add : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E),
  Metric.ball x δ + s = x +ᵥ Metric.thickening δ s
-- Lean.Elab.Tactic.Doc
/-- Creates some `MessageData` for a parser name.

If the parser name maps to a description with an
identifiable leading token, then that token is shown. Otherwise, the underlying name is shown
without an `@`. The name includes metadata that makes infoview hovers and the like work. This
only works for global constants, as the local context is not included.
 -/
_private.Lean.Elab.Tactic.Doc.0.Lean.Elab.Tactic.Doc.showParserName : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.NameMap String → Lean.Name → m Lean.MessageData
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_iInf : ∀ {R : Type u} [inst : NonAssocRing R] {ι : Sort u_1} {S : ι → Subring R} {x : R}, x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise scalar multiplication of `f` and `g` is minimized when
`f` and `g` antivary together on `s`. Stated by permuting the entries of `f`.  -/
AntivaryOn.sum_smul_le_sum_comp_perm_smul : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
  AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g i ≤ ∑ i ∈ s, f (σ i) • g i
-- Lean.Elab.Tactic.BuiltinTactic
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.getCaseGoals : Lean.TSyntax `Lean.binderIdent → Lean.Elab.Tactic.TacticM (Lean.MVarId × List Lean.MVarId)
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
/-- The localization of the fiber `p.Fiber S` is isomorphic to a quotient of a localization.  -/
Ideal.Fiber.localizationAlgEquivQuotient : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : Ideal R) →
            [inst_3 : p.IsPrime] →
              (q : Ideal (p.Fiber S)) →
                [inst_4 : q.IsPrime] →
                  [inst_5 :
                      Algebra (Localization.AtPrime p)
                        (Localization.AtPrime (Ideal.comap Algebra.TensorProduct.includeRight q))] →
                    [Localization.AtPrime.IsLiesOverAlgebra p (Ideal.comap Algebra.TensorProduct.includeRight q)] →
                      Localization.AtPrime q ≃ₐ[Localization.AtPrime p]
                        Localization.AtPrime (Ideal.comap Algebra.TensorProduct.includeRight q) ⧸
                          Ideal.map
                            (algebraMap R (Localization.AtPrime (Ideal.comap Algebra.TensorProduct.includeRight q))) p
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.hasFiniteIntegral_prod_iff : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  ⦃f : α × β → E⦄,
  MeasureTheory.StronglyMeasurable f →
    (MeasureTheory.HasFiniteIntegral f (μ.prod ν) ↔
      (∀ᵐ (x : α) ∂μ, MeasureTheory.HasFiniteIntegral (fun y => f (x, y)) ν) ∧
        MeasureTheory.HasFiniteIntegral (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ)
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.topEquiv_apply : ∀ {G : Type u_1} [inst : Group G] (x : ↥⊤), Subgroup.topEquiv x = ↑x
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableOn.add_iff_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {s : Set E}, DifferentiableOn 𝕜 g s → (DifferentiableOn 𝕜 (f + g) s ↔ DifferentiableOn 𝕜 f s)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_mul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} {f : σ → R},
  (MvPolynomial.eval f) (p * q) = (MvPolynomial.eval f) p * (MvPolynomial.eval f) q
-- Init.Data.Vector.Lemmas
Vector.flatMap_id : ∀ {α : Type u_1} {m n : ℕ} {xss : Vector (Vector α m) n}, xss.flatMap id = xss.flatten
-- Mathlib.Order.PartialSups
partialSups_eq_sup_range : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (f : ℕ → α) (n : ℕ),
  (partialSups f) n = (Finset.range (n + 1)).sup f
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.insert k).min? = some (t.min?.elim k fun k' => if cmp k k' = Ordering.lt then k else k')
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateFunDeclCoreImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.FunDecl pu →
    Lean.Expr → Array (Lean.Compiler.LCNF.Param pu) → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.FunDecl pu
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.resolveLValAux : Lean.Expr → Lean.Expr → Lean.Elab.Term.LVal → Lean.Elab.TermElabM Lean.Elab.Term.LValResolution
-- Mathlib.Topology.Algebra.Monoid.Defs
/-- A type class encoding that addition is continuous in each argument. This is weaker than
`ContinuousAdd`.  -/
SeparatelyContinuousAdd : (M : Type u_1) → [TopologicalSpace M] → [Add M] → Prop
-- Init.Data.Dyadic.Basic
Dyadic.instSub : Sub Dyadic
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.zero_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) {Y Z : C} (n : ℕ) {m : ℕ} (β : CategoryTheory.Abelian.Ext Y Z m) (p : ℕ)
  (h : n + m = p), CategoryTheory.Abelian.Ext.comp 0 β h = 0
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.sSupFun.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R}
  {c : Set (HahnEmbedding.Partial seed)} (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c),
  HahnEmbedding.Partial.sSupFun hc = LinearPMap.sSup ((fun x => ↑x) '' c) ⋯
-- Mathlib.CategoryTheory.Abelian.FunctorCategory
CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type w} [inst_1 : CategoryTheory.Category.{z, w} D]
  [inst_2 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C),
  (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.map (CategoryTheory.Limits.kernel.ι (α.app X))
        ((CategoryTheory.Limits.kernel.ι α).app X)
        (CategoryTheory.Limits.PreservesKernel.iso ((CategoryTheory.evaluation C D).obj X) α).inv
        (CategoryTheory.CategoryStruct.id (F.obj X)) ⋯)
      (CategoryTheory.Limits.cokernelComparison (CategoryTheory.Limits.kernel.ι α)
        ((CategoryTheory.evaluation C D).obj X))
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.uncurryRight_norm : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : Ei i.castSucc [×n]→L[𝕜] Ei (Fin.last n) →L[𝕜] G),
  ‖f.uncurryRight‖ = ‖f‖
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMap.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (f : M → M') (p : TangentBundle I M),
  tangentMap I I' f p = ⟨f p.proj, (mfderiv% f p.proj) p.snd⟩