mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousSubmodule_fg : ∀ (σ : Type u_1) (R : Type u_3) [inst : CommSemiring R] [Finite σ] (n : ℕ), (MvPolynomial.homogeneousSubmodule σ R n).FG
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (L₁ L₂ : IntermediateField k K) [IsGalois k ↥L₁] [IsGalois k ↥L₂], IsGalois k ↥(L₁ ⊓ L₂)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0.step.match_1.splitter : {Γ : Type u_1} →
  (motive : Turing.TM0.Stmt Γ → Sort u_2) →
    (a : Turing.TM0.Stmt Γ) →
      ((d : Turing.Dir) → motive (Turing.TM0.Stmt.move d)) → ((a : Γ) → motive (Turing.TM0.Stmt.write a)) → motive a
-- Mathlib.Topology.Algebra.Indicator
continuous_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  [inst_2 : Zero β], (∀ a ∈ frontier s, f a = 0) → ContinuousOn f (closure s) → Continuous (s.indicator f)
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.comp.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} {a b c : M} (f : CategoryTheory.ShiftedHom X Y a)
  (g : CategoryTheory.ShiftedHom Y Z b) (h : b + a = c),
  f.comp g h =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map g)
        ((CategoryTheory.shiftFunctorAdd' C b a c h).inv.app Z))
-- Mathlib.Algebra.Star.Basic
MulOpposite.instStarRing : {R : Type u} → [inst : NonUnitalSemiring R] → [StarRing R] → StarRing Rᵐᵒᵖ
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- Fractions which differ by a factor of the numerator can be proven equal if
those factors expand to equal elements of `R`.  -/
OreLocalization.eq_of_num_factor_eq : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {r r' r₁ r₂ : R} {s t : ↥S},
  ↑t * r = ↑t * r' → r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_maxKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false},
      Std.Internal.List.getKey! (Std.Internal.List.maxKey l he) l = Std.Internal.List.maxKey l he
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.realSize.match_1.eq_1 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.Heap α → Sort u_2)
  (h_1 : Unit → motive Batteries.BinomialHeap.Imp.Heap.nil)
  (h_2 :
    (rank : ℕ) →
      (val : α) →
        (c : Batteries.BinomialHeap.Imp.HeapNode α) →
          (s : Batteries.BinomialHeap.Imp.Heap α) → motive (Batteries.BinomialHeap.Imp.Heap.cons rank val c s)),
  (match Batteries.BinomialHeap.Imp.Heap.nil with
    | Batteries.BinomialHeap.Imp.Heap.nil => h_1 ()
    | Batteries.BinomialHeap.Imp.Heap.cons rank val c s => h_2 rank val c s) =
    h_1 ()
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom.comp.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  (g : CategoryTheory.FreeBicategory.Hom b c),
  sizeOf (f.comp g) = 1 + sizeOf a + sizeOf b + sizeOf c + sizeOf f + sizeOf g
-- Batteries.Data.List.Lemmas
List.findIdxNth.go.eq_3 : ∀ {α : Type u_1} (p : α → Bool) (s : ℕ) (a : α) (xs_1 : List α) (n_1 : ℕ),
  List.findIdxNth.go p (a :: xs_1) n_1.succ s =
    bif !p a then List.findIdxNth.go p xs_1 (n_1 + 1) (s + 1) else List.findIdxNth.go p xs_1 n_1 (s + 1)
-- Mathlib.Order.Defs.PartialOrder
/-- A version of `le_refl` where the argument is implicit  -/
le_rfl : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, a ≤ a
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The map `pr₀*` of the Stacks entry.  -/
CategoryTheory.Equalizer.Presieve.firstMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) →
      {X : C} →
        (R : CategoryTheory.Presieve X) →
          [inst_1 : R.HasPairwisePullbacks] →
            CategoryTheory.Equalizer.FirstObj P R ⟶ CategoryTheory.Equalizer.Presieve.SecondObj P R
-- Mathlib.Analysis.Matrix.LDL
/-- Inverse statement of **LDL decomposition**: we can conjugate a positive definite matrix
by some lower triangular matrix and get a diagonal matrix.  -/
LDL.diag_eq_lowerInv_conj : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n] [inst_2 : WellFoundedLT n]
  [inst_3 : LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [inst_4 : Fintype n] (hS : S.PosDef),
  LDL.diag hS = LDL.lowerInv hS * S * (LDL.lowerInv hS).conjTranspose
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- If a set `s` spans the module `M`, then the set of all elements of the form `x₁ ∧ ⋯ ∧ xₙ`
where `xᵢ ∈ s` spans `⋀ⁿ M`.  -/
exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s : Set M},
  Submodule.span R s = ⊤ → Submodule.span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | Set.range a ⊆ s}) = ⋀[R]^n M
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : DecidableEq γ] [inst_3 : Fintype α] [inst_4 : Fintype β] [inst_5 : Fintype γ]
  [SimpleGraph.TripartiteFromTriangles.NoAccidental t],
  (SimpleGraph.TripartiteFromTriangles.graph t).cliqueFinset 3 =
    Finset.map SimpleGraph.TripartiteFromTriangles.toTriangle t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_eq_some_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.minKey? = some t.minKey!
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.anyM.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Order.Bounds.Basic
IsGreatest.isLUB : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsGreatest s a → IsLUB s a
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- a class of triangle which are called `distinguished`  -/
CategoryTheory.Pretriangulated.distinguishedTriangles : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.Limits.HasZeroObject C} →
      {inst_2 : CategoryTheory.HasShift C ℤ} →
        {inst_3 : CategoryTheory.Preadditive C} →
          {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} →
            [self : CategoryTheory.Pretriangulated C] → Set (CategoryTheory.Pretriangulated.Triangle C)
-- Mathlib.Tactic.Translate.Core
/-- `Config` is the type of the arguments that can be provided to `to_additive`.  -/
Mathlib.Tactic.Translate.Config : Type
-- Mathlib.Data.Set.Pairwise.Lattice
/-- Equivalence between a disjoint bounded union and a dependent sum.  -/
Set.biUnionEqSigmaOfDisjoint : {α : Type u_1} →
  {ι : Type u_2} → {s : Set ι} → {f : ι → Set α} → s.PairwiseDisjoint f → ↑(⋃ i ∈ s, f i) ≃ (i : ↑s) × ↑(f ↑i)
-- Mathlib.Topology.EMetricSpace.Basic
/-- A variation of the emetric characterization of Cauchy sequences that deals with
`ℝ≥0` upper bounds.  -/
EMetric.cauchySeq_iff_NNReal : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {u : β → α},
  CauchySeq u ↔ ∀ (ε : NNReal), 0 < ε → ∃ N, ∀ (n : β), N ≤ n → edist (u n) (u N) < ↑ε
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.leftInverseUnitor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.prod.leftInverseUnitor C).map f =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id { as := PUnit.unit }) f
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.toHom_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  Function.Injective fun x => x.toHom
-- Mathlib.Topology.Order.Monotone
IsClosed.isLeast_csInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {s : Set α}, IsClosed s → s.Nonempty → BddBelow s → IsLeast s (sInf s)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_eq_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {a : α} {fallback : β} {h' : a ∈ t}, Std.DTreeMap.Raw.Const.get t a h' = Std.DTreeMap.Raw.Const.getD t a fallback
-- Lean.Parser.Term
Lean.Parser.Term.debugAssert.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.map : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v v' : Valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀) (hf : Monotone ⇑f),
  Function.Injective ⇑f → v.IsEquiv v' → (Valuation.map f hf v).IsEquiv (Valuation.map f hf v')
-- Init.Data.String.Basic
String.Pos.Raw.isValid_iff_isValidUTF8_extract_utf8ByteSize : ∀ {s : String} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid s p ↔ p ≤ s.rawEndPos ∧ (s.toByteArray.extract p.byteIdx s.utf8ByteSize).IsValidUTF8
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
Submodule.coe_closure : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] [inst_4 : ContinuousAdd M] [inst_5 : ContinuousConstSMul R M] (s : Submodule R M),
  ↑s.closure = closure ↑s
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.isPlausibleOutput_iff : ∀ {α : Type u} {a : α} [inst : Std.PRange.UpwardEnumerable α] {it : Std.Iter α},
  it.IsPlausibleOutput a ↔ it.internalState.next = some a
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.mem_nhds_iff : ∀ {α : Type ua} [inst : UniformSpace α] {x : α} {s : Set α}, s ∈ nhds x ↔ ∃ V ∈ uniformity α, UniformSpace.ball x V ⊆ s
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hom_ext_iff : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] {A B : TopRep k G}
  {f g : A ⟶ B}, f = g ↔ TopRep.Hom.hom f = TopRep.Hom.hom g
-- Init.Data.SInt.Lemmas
ISize.toInt_ofNat_of_lt : ∀ {n : ℕ}, n < 2 ^ 31 → (ISize.ofNat n).toInt = ↑n
-- Init.Data.List.ToArray
List.eq_toArray_iff : ∀ {α : Type u_1} {as : Array α} {bs : List α}, as = bs.toArray ↔ as.toList = bs
-- ProofWidgets.Cancellable
ProofWidgets.CancellableTask.mk : Task (Except Lean.Server.RequestError (ProofWidgets.LazyEncodable Lean.Json)) → IO Unit → ProofWidgets.CancellableTask
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_le_exp_iff : ∀ {a b : EReal}, a.exp ≤ b.exp ↔ a ≤ b
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.norm_star_mul_self' : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E] {x : E},
  ‖star x * x‖ = ‖star x‖ * ‖x‖
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.val_injective : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K],
  Function.Injective FiniteGaloisIntermediateField.toIntermediateField
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- A binary operation on two `BVExpr`.
 -/
Std.Tactic.BVDecide.BVExpr.bin : {w : ℕ} →
  Std.Tactic.BVDecide.BVExpr w →
    Std.Tactic.BVDecide.BVBinOp → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr w
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.pointwise_smul_toSubring : ∀ {K : Type u} [inst : Field K] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G K] (g : G)
  (S : ValuationSubring K), (g • S).toSubring = g • S.toSubring
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_neg_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, (f =o[l] fun x => -g' x) ↔ f =o[l] g'
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.card_mono : ∀ (k : Type u_1) [inst : Field k] (K : Type u_2) [inst_1 : Field K] [Algebra k K] [inst_3 : NumberField k]
  [inst_4 : NumberField K], Fintype.card (NumberField.InfinitePlace k) ≤ Fintype.card (NumberField.InfinitePlace K)
-- Mathlib.Order.RelIso.Basic
RelIso.relEmbeddingCongr_apply_apply : ∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ ↪r s₁) (a : α₂),
  ((e₁.relEmbeddingCongr e₂) f₁) a = e₂ (f₁ (e₁.symm a))
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.card_Iic : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  [inst_2 : (i : ι) → AddCommMonoid (α i)] [inst_3 : (i : ι) → PartialOrder (α i)]
  [inst_4 : ∀ (i : ι), IsBotZeroClass (α i)] [inst_5 : (i : ι) → OrderBot (α i)]
  [inst_6 : (i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i),
  (Finset.Iic f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instInhabitedAltParamInfo : Inhabited Lean.Meta.Match.AltParamInfo
-- Mathlib.Tactic.NormNum.Result
/-- The result is `z : ℤ` and `proof : isNat x z`.  -/
Mathlib.Meta.NormNum.Result.isInt : {u : Lean.Level} →
  {α : Q(Type u)} →
    {x : Q(«$α»)} →
      (inst : autoParam Q(Ring «$α») Mathlib.Meta.NormNum.Result.isInt._auto_1) →
        (z : Q(ℤ)) → ℤ → Q(Mathlib.Meta.NormNum.IsInt «$x» «$z») → Mathlib.Meta.NormNum.Result x
-- Lean.Meta.Tactic.Simp.Types
/-- Number of indices in the local context when starting `simp`.
We use this information to decide which assumptions we can use without
invalidating the cache.
 -/
Lean.Meta.Simp.Context.lctxInitIndices : Lean.Meta.Simp.Context → ℕ
-- Mathlib.Logic.Basic
exists_or_forall_not : ∀ {α : Sort u_1} (P : α → Prop), (∃ a, P a) ∨ ∀ (a : α), ¬P a
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.liftFromProjective.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) {P : C} (f f_1 : P ⟶ S.X₂) (e_f : f = f_1)
  [inst_2 : CategoryTheory.Projective P] (hf : CategoryTheory.CategoryStruct.comp f S.g = 0),
  hS.liftFromProjective f hf = hS.liftFromProjective f_1 ⋯
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.elabGrindConfigCore.evalConfigItem : (Lean.Term → Lean.Elab.TermElabM Lean.Grind.Config) → Lean.Elab.ConfigEval.EvalConfigItem Lean.Grind.Config
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is positive, then
`f` is a strictly monotone function.
Note that we don't require differentiability explicitly as it already implied by the derivative
being strictly positive.  -/
strictMono_of_deriv_pos : ∀ {f : ℝ → ℝ}, (∀ (x : ℝ), 0 < deriv f x) → StrictMono f
-- Mathlib.Data.Tree.Basic
/-- **Alias** of `BinaryTree`.

---

A binary tree with values stored in non-leaf nodes.  -/
Tree : Type u → Type u
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.Rel : {α β : Type w} →
  (m : Type w → Type w') →
    [Monad m] → [inst : Std.Iterator α m β] → [Std.Iterators.Productive α m] → Std.IterM m β → Std.IterM m β → Prop
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a fallback : α}, m.contains a = false → m.getD a fallback = fallback
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.HashMap.unitOfList l).getKey? k' = some k
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.flag : Lean.Name → Bool → Lean.Doc.ArgSpec✝
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The product of almost everywhere measurable functions is measurable.  -/
AEMeasurable.tprod' : ∀ {X : Type u_6} {E : Type u_7} {ι : Type u_8} [inst : MeasurableSpace X] [inst_1 : CommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [inst_4 : MeasurableSpace E] [BorelSpace E]
  [MeasurableMul₂ E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] {μ : MeasureTheory.Measure X}
  {f : ι → X → E}, (∀ (i : ι), AEMeasurable (f i) μ) → AEMeasurable (∏'[L] (i : ι), f i) μ
-- Init.Data.Float.Float32
instMulFloat32 : Mul Float32
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- A Hadamard matrix with constant column sum `s` has order `s * star s`, provided the order
is regular in `R`.

The row-sum form is `IsHadamard.card_eq_star_mul_of_const_row_sum`; over a ring with trivial
star the conclusion becomes `(Fintype.card n : R) = s ^ 2`, a slightly stronger form of
[Theorem 2.3.7][deLauneyFlannery2011]: only a constant sum hypothesis on one side is needed
under the two-sided orthogonality condition.  -/
Matrix.IsHadamard.card_eq_mul_star_of_const_col_sum : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] [inst_3 : StarRing R]
  {A : Matrix n n R} {s : R},
  A.IsHadamard → IsRegular ↑(Fintype.card n) → (∀ (j : n), ∑ i, A i j = s) → ↑(Fintype.card n) = s * star s
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.eraseManyEntries_eq_foldl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {l : List ((a : α) × β a)} {t : Std.DTreeMap.Internal.Impl α β}
  (h : t.Balanced),
  ↑(t.eraseManyEntries l h) =
    List.foldl
      (fun acc x_1 =>
        match x_1 with
        | ⟨k, snd⟩ => Std.DTreeMap.Internal.Impl.erase! k acc)
      t l
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.matchAt?_eq : ∀ {s : String.Slice} {pos : s.Pos} {c : Char},
  String.Slice.Pattern.Model.matchAt? c pos =
    if h₀ : ∃ (h : pos ≠ s.endPos), pos.get h = c then some (pos.next ⋯) else none
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.IsUnitTrinomial.ne_zero : ∀ {p : Polynomial ℤ}, p.IsUnitTrinomial → p ≠ 0
-- Mathlib.Topology.Order.Basic
pi_Ioi_mem_nhds : ∀ {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [inst : (i : ι) → LinearOrder (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a x : (i : ι) → X i} [Nonempty ι],
  (∀ (i : ι), a i < x i) → Set.Ioi a ∈ nhds x
-- Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
AddChar.wInner_cWeight_eq_zero_iff_ne : ∀ {G : Type u_1} {R : Type u_3} [inst : AddCommGroup G] [inst_1 : RCLike R] {ψ₁ ψ₂ : AddChar G R} [inst_2 : Fintype G],
  ⟪⇑ψ₁, ⇑ψ₂⟫ₙ_[R] = 0 ↔ ψ₁ ≠ ψ₂
-- Mathlib.Algebra.Group.Even
Even.nsmul_left : ∀ {α : Type u_2} [inst : AddMonoid α] {n : ℕ}, Even n → ∀ (a : α), Even (n • a)
-- Init.PropLemmas
exists_apply_eq_apply : ∀ {α : Sort u_2} {β : Sort u_1} (f : α → β) (a' : α), ∃ a, f a = f a'
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceₘ.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (r : Std.DTreeMap.Internal.Impl α β) →
      (motive :
          (l : Std.DTreeMap.Internal.Impl α β) →
            ¬r.size > Std.DTreeMap.Internal.delta * l.size → l.size > Std.DTreeMap.Internal.delta * r.size → Sort u_3) →
        (l : Std.DTreeMap.Internal.Impl α β) →
          (h : ¬r.size > Std.DTreeMap.Internal.delta * l.size) →
            (h_1 : l.size > Std.DTreeMap.Internal.delta * r.size) →
              ((h : ¬r.size > Std.DTreeMap.Internal.delta * Std.DTreeMap.Internal.Impl.leaf.size) →
                  (h_2 : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * r.size) →
                    motive Std.DTreeMap.Internal.Impl.leaf h h_2) →
                ((size : ℕ) →
                    (lk : α) →
                      (lv : β lk) →
                        (ll lr : Std.DTreeMap.Internal.Impl α β) →
                          (h :
                              ¬r.size >
                                  Std.DTreeMap.Internal.delta *
                                    (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size) →
                            (h_2 :
                                (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size >
                                  Std.DTreeMap.Internal.delta * r.size) →
                              motive (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr) h h_2) →
                  motive l h h_1
-- Mathlib.ModelTheory.Arithmetic.Presburger.Definability
IsLinearSet.definable : ∀ {α : Type u_1} {s : Set (α → ℕ)} {A : Set ℕ} [Finite α], IsLinearSet s → A.Definable FirstOrder.Language.presburger s
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
isUniformAddGroup_sInf : ∀ {G : Type u_1} [inst : AddGroup G] {us : Set (UniformSpace G)}, (∀ u ∈ us, IsUniformAddGroup G) → IsUniformAddGroup G
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_sub_nhds_zero_iff_eq : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {α : Type u_1} {l : Filter α}
  [l.NeBot] [T2Space G] {f g : α → G} {a b : G},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto g l (nhds b) → (Filter.Tendsto (fun x => f x - g x) l (nhds 0) ↔ a = b)
-- Mathlib.Algebra.Exact.Basic
LinearMap.injective_iff_eq_zero_of_exact : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P}, Function.Exact ⇑f ⇑g → (Function.Injective ⇑g ↔ f = 0)
-- Lean.Compiler.ExternAttr
Lean.instHashableExternAttrData : Hashable Lean.ExternAttrData
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (t : CategoryTheory.Limits.PushoutCocone f g),
  CategoryTheory.CategoryStruct.comp f t.inl = CategoryTheory.CategoryStruct.comp g t.inr
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- Left whiskering for morphisms of bimodule objects.  -/
Bimod.whiskerLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        [inst_3 :
            ∀ (X : C),
              CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                (CategoryTheory.MonoidalCategory.tensorLeft X)] →
          [inst_4 :
              ∀ (X : C),
                CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                  (CategoryTheory.MonoidalCategory.tensorRight X)] →
            {X Y Z : CategoryTheory.Mon C} →
              (M : Bimod X Y) → {N₁ N₂ : Bimod Y Z} → (N₁ ⟶ N₂) → (M.tensorBimod N₁ ⟶ M.tensorBimod N₂)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Subsemirings of a semiring form a complete lattice.  -/
Subsemiring.instCompleteLattice : {R : Type u} → [inst : NonAssocSemiring R] → CompleteLattice (Subsemiring R)
-- Lean.Meta.Instances
Lean.Meta.DefaultInstances.mk.sizeOf_spec : ∀ (defaultInstances : Lean.NameMap (List (Lean.Name × ℕ))) (priorities : Lean.Meta.PrioritySet),
  sizeOf { defaultInstances := defaultInstances, priorities := priorities } =
    1 + sizeOf defaultInstances + sizeOf priorities
-- Init.Control.Except
/-- Use a monadic action that may throw an exception by providing explicit success and failure
continuations.
 -/
ExceptT.runK : {m : Type u_1 → Type u_2} → {ε α β : Type u_1} → [Monad m] → ExceptT ε m α → (α → m β) → (ε → m β) → m β
-- Aesop.Tree.ExtractScript
Aesop.MVarClusterRef.extractSafePrefixScriptCore : Aesop.MVarClusterRef → Aesop.ExtractScriptM Unit