mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.OfFn
_private.Init.Data.Array.OfFn.0.Array.ofFn.go.match_1.eq_1 : ∀ {n : ℕ} (motive : (x : ℕ) → x ≤ n → Sort u_1) (i : ℕ) (h : i + 1 ≤ n)
  (h_1 : (i : ℕ) → (h : i + 1 ≤ n) → motive i.succ h) (h_2 : (x : 0 ≤ n) → motive 0 x),
  (match i.succ, h with
    | i.succ, h => h_1 i h
    | 0, x => h_2 x) =
    h_1 i h
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.map_eq_zero_iff : ∀ {β : Type v} {α : Type u_1} {f : α → β} {v : WithTop α} [inst : Zero β], WithTop.map f v = 0 ↔ ∃ x, v = ↑x ∧ f x = 0
-- Mathlib.FieldTheory.Galois.Basic
/-- If `K / E / k` is a field extension tower with `E / k` and `K / k` normal,
`L` is an intermediate field of `E / k`, then the index of the fixing subgroup of `L` viewed as an
intermediate field of `K / k` is equal to the index of the fixing subgroup of `L` viewed as an
intermediate field of `E / k`.  -/
IntermediateField.map_fixingSubgroup_index : ∀ {F : Type u_1} {E : Type u_2} (E' : Type u_3) [inst : Field F] [inst_1 : Field E] [inst_2 : Field E']
  [inst_3 : Algebra F E] [inst_4 : Algebra F E'] [inst_5 : Algebra E E'] [inst_6 : IsScalarTower F E E']
  (L : IntermediateField F E) [Normal F E] [Normal F E'],
  (IntermediateField.map (IsScalarTower.toAlgHom F E E') L).fixingSubgroup.index = L.fixingSubgroup.index
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropy_biUnion_finset : ∀ {X : Type u_1} {ι : Type u_2} [inst : UniformSpace X] {T : X → X} {F : ι → Set X} {s : Finset ι},
  Dynamics.coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, Dynamics.coverEntropy T (F i)
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftRight_eq : ∀ (n : ℤ) (s : ℕ), n >>> s = n.shiftRight s
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.nestedBC : Lean.Elab.Term.Do.ToTerm.Kind
-- Mathlib.Algebra.Ring.Ext
NonUnitalRing.toNonUnitalSemiring_injective : ∀ {R : Type u}, Function.Injective (@NonUnitalRing.toNonUnitalSemiring R)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.isIso_iff_coyoneda_map_bijective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsIso f ↔ ∀ (T : C), Function.Bijective fun x => CategoryTheory.CategoryStruct.comp f x
-- Mathlib.LinearAlgebra.Projection
/-- `range f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = T ∘ₗ f`,
for idempotent `f`.  -/
LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff : ∀ {E : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T f : E →ₗ[R] E},
  IsIdempotentElem f → (f.range ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.ExtTreeSet.ofList l cmp).getD k' fallback = k
-- Lean.Parser.Extension
Lean.Parser.getUnaryAlias : {α : Type} → IO.Ref (Lean.Parser.AliasTable α) → Lean.Name → IO (α → α)
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.condCDF.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α),
  ProbabilityTheory.condCDF ρ a =
    ProbabilityTheory.stieltjesOfMeasurableRat (fun a r => (ProbabilityTheory.preCDF ρ r a).toReal) ⋯ a
-- Mathlib.RingTheory.Smooth.Basic
/-- Being smooth is transported via algebra isomorphisms.  -/
Algebra.Smooth.of_equiv : ∀ {R : Type u_4} [inst : CommRing R] {A : Type u_5} {B : Type u_6} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.Smooth R A] (e : A ≃ₐ[R] B), Algebra.Smooth R B
-- Std.Async.IO
Std.Async.IO.AsyncWrite.mk : {α β : Type} →
  (α → β → Std.Async.Async Unit) →
    (α → Array β → Std.Async.Async Unit) → (α → Std.Async.Async Unit) → Std.Async.IO.AsyncWrite α β
-- Mathlib.Order.WellQuasiOrder
/-- A typeclass for an order with a well-quasi-ordered `≤` relation.

Note that this is unlike `WellFoundedLT`, which instead takes a `<` relation.  -/
WellQuasiOrderedLE : (α : Type u_3) → [LE α] → Prop
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.prod_rightr : ∀ {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : SeminormedAddCommGroup F'] {f : α → E} (f' : α → E') {g' : α → F'} {l : Filter α},
  f =o[l] g' → f =o[l] fun x => (f' x, g' x)
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.instIntCastHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier : (X : TopCat) → (R : TopCommRingCat) → IntCast (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Mathlib.Algebra.Order.Chebyshev
/-- **Chebyshev's Sum Inequality**: When `f` and `g` antivary together (e.g. one is monotone, the
other is antitone), the product of their sum is less than the size of the set times their scalar
product.  -/
Antivary.card_mul_sum_le_sum_mul_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {f g : ι → α} [inst_4 : Fintype ι], Antivary f g → ↑(Fintype.card ι) * ∑ i, f i * g i ≤ (∑ i, f i) * ∑ i, g i
-- Std.Data.HashSet.RawLemmas
/-- This is a restatement of `contains_insert` that is written to exactly match the proof
obligation in the statement of `get_insert`.  -/
Std.HashSet.Raw.contains_of_contains_insert' : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a : α}, (m.insert k).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_associator_inv'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y Z : C) {Z_1 : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
                (F.obj Z))
              h))))
-- Mathlib.RingTheory.Ideal.Prime
Ideal.isPrime_iff : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I.IsPrime ↔ I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I
-- Aesop.Rule
Aesop.instToStringSafeRule : ToString Aesop.SafeRule
-- Mathlib.Data.Finset.Sups
Finset.sups_subset_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t u : Finset α},
  s ⊻ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊔ b ∈ u
-- Mathlib.Topology.Algebra.MulAction
Inseparable.smul : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : SMul M X]
  [ContinuousSMul M X] {a b : M} {x y : X}, Inseparable a b → Inseparable x y → Inseparable (a • x) (b • y)
-- Mathlib.CategoryTheory.Limits.Cones
/-- An object of `C`  -/
CategoryTheory.Limits.Cocone.pt : {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.Cocone F → C
-- Init.Data.String.Lemmas.FindPos
String.posLE_eq_pos : ∀ {s : String} {p : String.Pos.Raw} (h : String.Pos.Raw.IsValid s p), s.posLE p = s.pos p h
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_reindex_right : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {l' : Type u_15}
  {m' : Type u_16} {n' : Type u_17} (f : α → β → γ) (em : m ≃ m') (en : n ≃ n') (M : Matrix l l' α) (N : Matrix m n β),
  Matrix.kroneckerMap f M ((Matrix.reindex em en) N) =
    (Matrix.reindex ((Equiv.refl l).prodCongr em) ((Equiv.refl l').prodCongr en)) (Matrix.kroneckerMap f M N)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.cons : Turing.ToPartrec.Code → Turing.ToPartrec.Code → Turing.ToPartrec.Code
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.theory_model_iff : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.ElementarySubstructure M) (T : L.Theory),
  ↥S ⊨ T ↔ M ⊨ T
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- A map in the opposite direction to `f` and `g`  -/
CategoryTheory.IsSplitEqualizer.rightRetraction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f g : X ⟶ Y} → {W : C} → {ι : W ⟶ X} → CategoryTheory.IsSplitEqualizer f g ι → (Y ⟶ X)
-- Init.Data.Float.Model.Float
/-- Compute the difference of two `Float.Model`.
 -/
Float.Model.sub : Float.Model → Float.Model → Float.Model
-- Mathlib.Topology.Subpath
/-- **Alias** of `Set.Icc.convexComb_one`. -/
Path.subpathAux_one : ∀ {a b : ℝ} (x y : ↑(Set.Icc a b)), Set.Icc.convexComb x y 1 = y
-- Mathlib.Topology.Category.LightProfinite.AsLimit
/-- The functor `ℕᵒᵖ ⥤ FintypeCat` whose limit is isomorphic to `S`.  -/
LightProfinite.fintypeDiagram : LightProfinite → CategoryTheory.Functor ℕᵒᵖ FintypeCat
-- Mathlib.Topology.ContinuousMap.Algebra
/-- The constant map `x ↦ y ↦ x` as a `ContinuousLinearMap`.  -/
ContinuousLinearMap.const : (R : Type u_3) →
  {M : Type u_5} →
    [inst : TopologicalSpace M] →
      [inst_1 : Semiring R] →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : ContinuousAdd M] →
            [inst_4 : Module R M] →
              [inst_5 : ContinuousConstSMul R M] → (α : Type u_7) → [inst_6 : TopologicalSpace α] → M →L[R] C(α, M)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M}
  {V W V₁ W₁ : (x : M) → TangentSpace I x},
  V₁ =ᶠ[nhds x] V →
    W₁ =ᶠ[nhds x] W → VectorField.mlieBracketWithin I V₁ W₁ s x = VectorField.mlieBracketWithin I V W s x
-- Mathlib.Data.Stream.Init
Stream'.any_def : ∀ {α : Type u} (p : α → Prop) (s : Stream' α), Stream'.Any p s = ∃ n, p (s.get n)
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csSup_add : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M]
  {s t : Set M}, s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sSup (s + t) = sSup s + sSup t
-- Std.Time.Format.Modifier
Std.Time.Modifier.L.injEq : ∀ (presentation presentation_1 : Std.Time.Number ⊕ Std.Time.Text),
  (Std.Time.Modifier.L presentation = Std.Time.Modifier.L presentation_1) = (presentation = presentation_1)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix'_mul : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (B : LinearMap.BilinForm R₁ (n → R₁)) (M : Matrix n n R₁),
  LinearMap.BilinForm.toMatrix' B * M = LinearMap.BilinForm.toMatrix' (B.compRight (Matrix.toLin' M))
-- Mathlib.LinearAlgebra.Prod
LinearMap.coprodEquiv_symm_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module S M₃] [inst_9 : SMulCommClass R S M₃]
  (f : M × M₂ →ₗ[R] M₃), (LinearMap.coprodEquiv S).symm f = (f ∘ₗ LinearMap.inl R M M₂, f ∘ₗ LinearMap.inr R M M₂)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_of_singleton.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] (a : α),
  SubAddAction.ofFixingAddSubgroup_of_singleton M a = { toFun := fun x => ⟨↑x, ⋯⟩, map_vadd' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonIdIso_hom_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon C), (CategoryTheory.Functor.mapMonIdIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Data.Int.WithZero
/-- `toNNReal` sends nonzero elements to nonzero elements.  -/
WithZeroMulInt.toNNReal_ne_zero : ∀ {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : e ≠ 0), m ≠ 0 → (WithZeroMulInt.toNNReal he) m ≠ 0
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual_injective : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M), Function.Injective ⇑b.toDual
-- Mathlib.NumberTheory.Padics.Complex
/-- We define `𝓞_ℂ_[p]` as the valuation subring of `ℂ_[p]`, consisting of those elements with
valuation `≤ 1`.  -/
PadicComplexInt : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ValuationSubring ℂ_[p]
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Splitting.rightHom_splitting : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} (s : S.Splitting) (g : G), S.rightHom (s g) = g
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₃.eq_1 : ∀ (w x y : UInt8),
  ByteArray.utf8DecodeChar?.assemble₃ w x y =
    if
        (ByteArray.utf8DecodeChar?.isInvalidContinuationByte x ||
            ByteArray.utf8DecodeChar?.isInvalidContinuationByte y) =
          true then
      none
    else
      let r := ByteArray.utf8DecodeChar?.assemble₃Unchecked w x y;
      if r < 2048 then none else if hr : 55296 ≤ r ∧ r ≤ 57343 then none else some { val := r, valid := ⋯ }
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.ratio_trans : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y]
  [inst_2 : PseudoEMetricSpace Z] (e : X ≃ᵈ Y) (e' : Y ≃ᵈ Z),
  Dilation.ratio (e.trans e') = Dilation.ratio e * Dilation.ratio e'
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_add_omega0_opow`. -/
Ordinal.principal_add_omega0_opow : ∀ (o : Ordinal.{u_1}), Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) (Ordinal.omega0 ^ o)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.alter.match_3.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.Balanced → Sort u_3) →
      (t : Std.DTreeMap.Internal.Impl α fun x => β) →
        (hl : t.Balanced) →
          ((hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hl) →
            ((sz : ℕ) →
                (k' : α) →
                  (v' : β) →
                    (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) →
                      (hl : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
                        motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hl) →
              motive t hl
-- Init.Sym.Lemmas
Lean.Sym.Char.le_eq_true : ∀ (a b : Char), decide (a ≤ b) = true → (a ≤ b) = True
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- If two ring homomorphisms from `R[M]` are equal on all `single m 1` and `single 0 r`,
then they are equal.  -/
AddMonoidAlgebra.ringHom_ext : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M] [inst_2 : Semiring S]
  {f g : AddMonoidAlgebra R M →+* S},
  (∀ (r : R), f (AddMonoidAlgebra.single 0 r) = g (AddMonoidAlgebra.single 0 r)) →
    (∀ (m : M), f (AddMonoidAlgebra.single m 1) = g (AddMonoidAlgebra.single m 1)) → f = g
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {fallback v : β},
  (m.insertIfNew k v).getD a fallback = if (k == a) = true ∧ k ∉ m then v else m.getD a fallback
-- Mathlib.Data.Finset.Prod
Finset.prodMap_map_product : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α ↪ β) (g : γ ↪ δ) (s : Finset α) (t : Finset γ),
  Finset.map (f.prodMap g) (s ×ˢ t) = Finset.map f s ×ˢ Finset.map g t
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_zero : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α}, (MeasureTheory.Measure.sum fun x => 0) = 0
-- Mathlib.Analysis.InnerProductSpace.Basic
real_inner_self_abs : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F), |inner ℝ x x| = inner ℝ x x
-- Mathlib.Algebra.Notation.Lemmas
dite_le_one : ∀ {α : Type u_1} [inst : One α] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α} [inst_2 : LE α],
  (∀ (h : p), a h ≤ 1) → (∀ (h : ¬p), b h ≤ 1) → dite p a b ≤ 1
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.mk.inj : ∀ {K : Type u_1} {inst : Field K} {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  {toSolution' : FermatLastTheoremForThreeGen.Solution'✝ hζ}
  {hab :
    (hζ.toInteger - 1) ^ 2 ∣
      FermatLastTheoremForThreeGen.Solution'.a✝ toSolution' + FermatLastTheoremForThreeGen.Solution'.b✝ toSolution'}
  {toSolution'_1 : FermatLastTheoremForThreeGen.Solution'✝ hζ}
  {hab_1 :
    (hζ.toInteger - 1) ^ 2 ∣
      FermatLastTheoremForThreeGen.Solution'.a✝ toSolution'_1 +
        FermatLastTheoremForThreeGen.Solution'.b✝ toSolution'_1},
  { toSolution' := toSolution', hab := hab } = { toSolution' := toSolution'_1, hab := hab_1 } →
    toSolution' = toSolution'_1
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.FiniteAdeleRing.ext_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {a₁ a₂ : IsDedekindDomain.FiniteAdeleRing R K},
  a₁ = a₂ ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), a₁ v = a₂ v
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.instFaithfulExactFunctorWhiskeringLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] (E : Type u'') [inst_4 : CategoryTheory.Category.{v'', u''} E]
  [inst_5 : CategoryTheory.Abelian E] [inst_6 : L.IsLocalization P.isoModSerre] [inst_7 : CategoryTheory.Preadditive D]
  [inst_8 : L.Additive], (CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft L P E).Faithful
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.mk.inj : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} {inst : AddCommGroup V} {inst_1 : AddTorsor V P}
  {inst_2 : Ring k} {inst_3 : Module k V} {toFun : ι → P} {ind' : AffineIndependent k toFun}
  {tot' : affineSpan k (Set.range toFun) = ⊤} {toFun_1 : ι → P} {ind'_1 : AffineIndependent k toFun_1}
  {tot'_1 : affineSpan k (Set.range toFun_1) = ⊤},
  { toFun := toFun, ind' := ind', tot' := tot' } = { toFun := toFun_1, ind' := ind'_1, tot' := tot'_1 } →
    toFun = toFun_1
-- Lean.Elab.ConfigEval.Util
/-- Returns a list of types that are are missing `cls` instances such that
implementing them would ensure a `cls type` instance. If there are no conditional
instances to support this, returns `#[type]`. If there's already a `cls type` instance,
returns `#[]`.

Only supports one-parameter classes.

For example, `planDerivation C t` where `t` is `Array t₁ × Option t₂` might return `#[t₁, t₂]`
if there are instances for `Array`, `Option`, and `Prod`, but not for `t₁` and `t₂`.

The `extraDeps` function is called whenever a type cannot be satisfied by existing instances.
It should return an array of types that need an instance to be implemented for the implementation
of the instance to succeed. For example, a `structure` might report the list of the types of all
its fields.
 -/
_private.Lean.Elab.ConfigEval.Util.0.Lean.Elab.ConfigEval.planDerivation : Lean.Name → Lean.Expr → (Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)) → Lean.Elab.TermElabM (Array Lean.Expr)
-- Mathlib.Control.Applicative
Comp.seq_mk : ∀ {α β : Type w} {f : Type u → Type v} {g : Type w → Type u} [inst : Applicative f] [inst_1 : Applicative g]
  (h : f (g (α → β))) (x : f (g α)),
  Functor.Comp.mk h <*> Functor.Comp.mk x = Functor.Comp.mk ((fun x1 x2 => x1 <*> x2) <$> h <*> x)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.instIsLocallyFreeDataLocalGeneratorsDataGeneratingSections : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_3 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_4 : CategoryTheory.Limits.HasBinaryProducts C]
  [inst_5 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (I : Type u),
  (SheafOfModules.free.generatingSections I).localGeneratorsData.IsLocallyFreeData
-- Mathlib.Order.SuccPred.Archimedean
PredOrder.forall_ne_top_iff : ∀ {α : Type u_1} [Nontrivial α] [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α]
  [IsPredArchimedean α] (P : α → Prop), (∀ (i : α), i ≠ ⊤ → P i) ↔ ∀ (i : α), P (PredOrder.pred i)
-- Mathlib.NumberTheory.NumberField.Basic
/-- The ring of integers of `L` is isomorphic to any integral closure of `𝓞 K` in `L`  -/
NumberField.RingOfIntegers.algEquiv : (K : Type u_4) →
  (L : Type u_5) →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          (R : Type u_6) →
            [inst_3 : CommRing R] →
              [inst_4 : Algebra (NumberField.RingOfIntegers K) R] →
                [inst_5 : Algebra R L] →
                  [IsScalarTower (NumberField.RingOfIntegers K) R L] →
                    [IsIntegralClosure R (NumberField.RingOfIntegers K) L] →
                      NumberField.RingOfIntegers L ≃ₐ[NumberField.RingOfIntegers K] R
-- Lean.Meta.Basic
Lean.Meta.shouldReduceReducibleOnly : Lean.MetaM Bool
-- Std.Http.Data.Body.Stream
/-- A zero-buffer rendezvous body channel that supports both sending and receiving chunks.
 -/
Std.Http.Body.Stream : Type
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.coe_transEquiv_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : PartialEquiv α β} {g : β ≃ γ},
  ↑(f.transEquiv g).symm = ↑f.symm ∘ ⇑g.symm
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- The measurable superset `toMeasurable μ t` of `t` (which has the same measure as `t`)
satisfies, for any measurable set `s`, the equality `μ (toMeasurable μ t ∩ s) = μ (t ∩ s)`.
This only holds when `μ` is s-finite -- for example for σ-finite measures. For a version without
this assumption (but requiring that `t` has finite measure), see `measure_toMeasurable_inter`.  -/
MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {s : Set α},
  MeasurableSet s → ∀ (t : Set α), μ (MeasureTheory.toMeasurable μ t ∩ s) = μ (t ∩ s)
-- Init.Data.List.Sublist
List.sublist_of_cons_sublist : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Sublist l₂ → l₁.Sublist l₂