mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAdd.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [inst_2 : ContinuousAdd M],
  SeparationQuotient.instAdd = { add := Quotient.map₂ (fun x1 x2 => x1 + x2) ⋯ }
-- Mathlib.Analysis.Normed.Module.Complemented
Submodule.coe_prodEquivOfClosedCompl_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {p q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed ↑p)
  (hq : IsClosed ↑q), ⇑(Submodule.prodEquivOfClosedCompl p q h hp hq).symm = ⇑(Submodule.prodEquivOfIsCompl p q h).symm
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instInvOneClass : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [InvOneClass G] → InvOneClass (l.Germ G)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- The class of cofibrations in a category with cofibrations.  -/
HomotopicalAlgebra.cofibrations : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithCofibrations C] → CategoryTheory.MorphismProperty C
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.edgeSet_singletonSubgraph : ∀ {V : Type u} {G : SimpleGraph V} (v : V), (G.singletonSubgraph v).edgeSet = ∅
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- The point of `Y`.  -/
AlgebraicGeometry.Scheme.Pullback.Triplet.y : {X Y S : AlgebraicGeometry.Scheme} → {f : X ⟶ S} → {g : Y ⟶ S} → AlgebraicGeometry.Scheme.Pullback.Triplet f g → ↥Y
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.hasFiniteCoproducts_of_hasCountableCoproducts : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCountableCoproducts C],
  CategoryTheory.Limits.HasFiniteCoproducts C
-- Mathlib.Data.Multiset.Functor
Multiset.instLawfulMonad : LawfulMonad Multiset
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.valuation_pow : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) (n : ℕ), (x ^ n).valuation = ↑n * x.valuation
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubseqResult.middle.sizeOf_spec : ∀ (p s : Lean.Grind.AC.Seq), sizeOf (Lean.Grind.AC.SubseqResult.middle p s) = 1 + sizeOf p + sizeOf s
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A preadditive category has a coequalizer for `f` and `g` if it has a cokernel for `f - g`.  -/
CategoryTheory.Preadditive.hasCoequalizer_of_hasCokernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (f g : X ⟶ Y)
  [CategoryTheory.Limits.HasCokernel (f - g)], CategoryTheory.Limits.HasCoequalizer f g
-- Init.Data.UInt.Lemmas
UInt16.sub_def : ∀ (a b : UInt16), a - b = { toBitVec := a.toBitVec - b.toBitVec }
-- Mathlib.Data.Matrix.Basis
Matrix.smul_single : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : Zero α] [inst_3 : SMulZeroClass R α] (r : R) (i : m) (j : n) (a : α),
  r • Matrix.single i j a = Matrix.single i j (r • a)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.zero_lt_getElem!_toList_rio_iff : ∀ {n i : ℕ}, 0 < (*...n).toList[i]! ↔ i < n ∧ 0 < i
-- Mathlib.RingTheory.Length
Module.length_eq_coheight : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.length R M = Order.coheight ⊥
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.coeff_X_sub_C_mul : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {r : R} {a : ℕ},
  ((Polynomial.X - Polynomial.C r) * p).coeff (a + 1) = p.coeff a - r * p.coeff (a + 1)
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftableCocone.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cocone (K.comp F)}
  (liftedCocone : CategoryTheory.Limits.Cocone K) (validLift : F.mapCocone liftedCocone ≅ c)
  (liftedCocone_1 : CategoryTheory.Limits.Cocone K) (validLift_1 : F.mapCocone liftedCocone_1 ≅ c),
  ({ liftedCocone := liftedCocone, validLift := validLift } =
      { liftedCocone := liftedCocone_1, validLift := validLift_1 }) =
    (liftedCocone = liftedCocone_1 ∧ validLift ≍ validLift_1)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivAt.mul' : ∀ {𝕜 : 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] {z : M} {F' : Type u_21} [inst_6 : NormedRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'} {p' q' : TangentSpace I z →L[𝕜] F'},
  HasMFDerivAt% p z p' → HasMFDerivAt% q z q' → HasMFDerivAt% (p * q) z (p z • q' + MulOpposite.op (q z) • p')
-- Mathlib.LinearAlgebra.Projection
Submodule.projection.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p p_1 : Submodule R E)
  (e_p : p = p_1) (q q_1 : Submodule R E) (e_q : q = q_1) (hpq : IsCompl p q), p.projection q hpq = p_1.projection q_1 ⋯
-- Init.Data.Nat.Coprime
Nat.Coprime.dvd_of_dvd_mul_left : ∀ {k m n : ℕ}, k.Coprime m → k ∣ m * n → k ∣ n
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_closure : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {x : R} {s : Set R},
  x ∈ NonUnitalSubring.closure s ↔ ∀ (S : NonUnitalSubring R), s ⊆ ↑S → x ∈ S
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.of_ringEquiv : ∀ (k : Type u) [inst : Field k] (k' : Type u) [inst_1 : Field k'] (e : k ≃+* k') [IsAlgClosed k], IsAlgClosed k'
-- Qq.Simp
/-- A copy of `Meta.Simp.Step` with explicit types.  -/
Lean.Meta.Simp.StepQ : {u : Lean.Level} → {α : Q(Sort u)} → Q(«$α») → Type
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.homCategory.ext_iff : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {m n : η ⟶ θ}, m = n ↔ ∀ (b : B), m.as.app b = n.as.app b
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.G₂.eq_1 : CartanMatrix.G₂ = !![2, -3; -1, 2]
-- Aesop.Tree.Data
Aesop.instDecidableEqGoalId : DecidableEq Aesop.GoalId
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.NonnegCoeffs : Lean.Grind.CommRing.Poly → Prop
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.id_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C),
  (CategoryTheory.CategoryStruct.id A).hom = CategoryTheory.CategoryStruct.id A.toGrp
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.norm_smul_const : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] {R : Type u_4} {β : Type u_5}
  [inst_2 : SeminormedAddCommGroup β] [inst_3 : SeminormedRing R] [inst_4 : Module R β] [inst_5 : NormSMulClass R β]
  (f : C(α, R)) (b : β), ‖f • ContinuousMap.const α b‖ = ‖f‖ * ‖b‖
-- Mathlib.RingTheory.DedekindDomain.Instances
_private.Mathlib.RingTheory.DedekindDomain.Instances.0.termP' : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_insert_self : ∀ {𝕜 : 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'} {x : M} {s : Set M},
  MDiffAt[insert x s] f x ↔ MDiffAt[s] f x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.freeCofan_inj : ∀ {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] {I : Type u} (i : I),
  (SheafOfModules.freeCofan I).inj i = SheafOfModules.ιFree i
-- Lean.Level
Lean.Level.hasParamEx : Lean.Level → Bool
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → k ∉ t₁ ∩ t₂
-- Mathlib.Lean.Expr.ExtraRecognizers
/-- If `e` is a coercion of a set to a type, return the set.
Succeeds either for `Set.Elem s` terms or `{x // x ∈ s}` subtype terms.  -/
Lean.Expr.coeTypeSet? : Lean.Expr → Option Lean.Expr
-- Mathlib.SetTheory.ZFC.Class
/-- The intersection of a class is the class of all members of ZFC sets in the class .
Uses `⋂₀` notation, scoped under the `Class` namespace.  -/
Class.sInter : Class.{u_1} → Class.{u_1}
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- Construct a bundled `ReflQuiv` from the underlying type and the typeclass.  -/
CategoryTheory.ReflQuiv.of : (C : Type u) → [CategoryTheory.ReflQuiver C] → CategoryTheory.ReflQuiv
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.sigma' : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousMul α] [RegularSpace α]
  {γ : β → Type u_4} {f : (b : β) × γ b → α},
  Multipliable f → (∀ (b : β), Multipliable fun c => f ⟨b, c⟩) → Multipliable fun b => ∏' (c : γ b), f ⟨b, c⟩
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.natCard_algEquiv_extension : ∀ (k : Type u_1) [inst : Field k] [inst_1 : Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [inst_4 : NeZero n], Nat.card Gal(FiniteField.Extension k p n/k) = n
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.map_det : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S) (g : GL n R),
  Matrix.GeneralLinearGroup.det ((Matrix.GeneralLinearGroup.map f) g) = (Units.map ↑f) (Matrix.GeneralLinearGroup.det g)
-- Mathlib.Topology.Clopen
IsClopen.prod : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
  IsClopen s → IsClopen t → IsClopen (s ×ˢ t)
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.mem_of_append : ∀ {A : Type u_1} {T : ↥(Descriptive.tree A)} {x y : List A}, x ++ y ∈ T → x ∈ T
-- Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
/-- A presheaf of types is a sheaf for the `P`-qc topology if and only if it is a sheaf
for the Zariski topology and satisfies the sheaf property for all single object coverings
`{ f : Spec S ⟶ Spec R }` where `f` satisfies `P`.  -/
AlgebraicGeometry.isSheaf_type_propQCTopology_iff : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative]
  (F : CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ (Type u_1)) [AlgebraicGeometry.IsZariskiLocalAtSource P],
  CategoryTheory.Presieve.IsSheaf (AlgebraicGeometry.Scheme.propQCTopology P) F ↔
    CategoryTheory.Presieve.IsSheaf AlgebraicGeometry.Scheme.zariskiTopology F ∧
      ∀ {R S : CommRingCat} (f : R ⟶ S),
        P (AlgebraicGeometry.Spec.map f) →
          AlgebraicGeometry.Surjective (AlgebraicGeometry.Spec.map f) →
            CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton (AlgebraicGeometry.Spec.map f))
-- Lean.Parser.Command
Lean.Parser.Command.openDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_exp_neg_Ioi_zero : ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-x) = 1
-- Mathlib.Data.Set.Finite.Basic
Finset.exists : ∀ {α : Type u} {p : Finset α → Prop}, (∃ s, p s) ↔ ∃ s, ∃ (hs : s.Finite), p hs.toFinset
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Variant of `prod_cons` not applied to a function.  -/
Finset.prod_cons' : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : CommMonoid M] (h : a ∉ s),
  (Finset.cons a s h).prod = fun f => f a * ∏ x ∈ s, f x
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (α : Type w)
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] {X Y : CategoryTheory.Functor (CategoryTheory.Discrete α) C}
  (β : X ⟶ Y) (x : (Finset (CategoryTheory.Discrete α))ᵒᵖ),
  ((CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).map β).app x =
    CategoryTheory.Limits.Pi.map fun x_1 => β.app ↑x_1
-- Init.Data.Array.Basic
/-- Returns the index of the first element equal to `a`, or `none` if no element is equal
to `a`. The index is returned as a `Fin`, which guarantees that it is in bounds.

Examples:
 * `#["carrot", "potato", "broccoli"].finIdxOf? "carrot" = some 0`
 * `#["carrot", "potato", "broccoli"].finIdxOf? "broccoli" = some 2`
 * `#["carrot", "potato", "broccoli"].finIdxOf? "tomato" = none`
 * `#["carrot", "potato", "broccoli"].finIdxOf? "anything else" = none`
 -/
Array.finIdxOf? : {α : Type u} → [BEq α] → (xs : Array α) → α → Option (Fin xs.size)
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetsExtEntry.global.sizeOf_spec : ∀ (n : Lean.Name), sizeOf (Lean.Widget.PanelWidgetsExtEntry.global n) = 1 + sizeOf n
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.restrictionLT.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J] {j : J}
  (F F_1 : CategoryTheory.Functor (↑(Set.Iic j)) C),
  F = F_1 →
    ∀ {i : J} (hi : i ≤ j),
      CategoryTheory.SmallObject.restrictionLT F hi = CategoryTheory.SmallObject.restrictionLT F_1 hi
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The functor used to define the equivalence `ofCommaSndEquivalence`.  -/
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor C T) →
              (G : CategoryTheory.Functor D T) →
                (c : C) →
                  CategoryTheory.Functor (CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G))
                    (CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G)
-- Lean.Meta.Sym.InstantiateS
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.instantiateRevBetaS'.visitAppDefault : Array Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Sym.M✝ Lean.Expr
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ext : ∀ {numVarsSucc : ℕ} {x y : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc}, x.clause = y.clause → x = y
-- Init.Data.Range.Polymorphic.Char
Char.least?_eq : Std.PRange.least? = some '\x00'
-- Mathlib.Algebra.Algebra.Pi
AlgHom.compLeft_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (ι : Type u_4) (h : ι → A) (a : ι),
  (f.compLeft ι) h a = (⇑f ∘ h) a
-- Init.Data.BitVec.Lemmas
BitVec.cons_append : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (a : Bool), BitVec.cons a x ++ y = BitVec.cast ⋯ (BitVec.cons a (x ++ y))
-- Mathlib.Order.Monotone.Monovary
MonovaryOn.comp_antitone_on_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {s : Set ι},
  MonovaryOn f g s → Antitone f' → AntivaryOn (f' ∘ f) g s
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.mul' : ∀ {𝕜 : 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] {s : Set M} {z : M} {F' : Type u_21}
  [inst_6 : NormedRing F'] [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'} {p' q' : TangentSpace I z →L[𝕜] F'},
  HasMFDerivAt[s] p z p' → HasMFDerivAt[s] q z q' → HasMFDerivAt[s] (p * q) z (p z • q' + MulOpposite.op (q z) • p')
-- Aesop.Script.CtorNames
Aesop.CtorNames.toAltVarNames : Aesop.CtorNames → Lean.Meta.AltVarNames
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.isHaarMeasure : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → Group (α i)] [inst_4 : (i : ι) → TopologicalSpace (α i)] [∀ (i : ι), (μ i).IsHaarMeasure]
  [∀ (i : ι), MeasurableMul (α i)], (MeasureTheory.Measure.pi μ).IsHaarMeasure
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- An additive semigroup homomorphism `f : M →+ N` with a left-inverse
`g : N → M` defines an additive equivalence between `M` and `f.srange`.
This is a bidirectional version of `AddHom.srangeRestrict`.  -/
AddEquiv.ofLeftInverse : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Add M] → [inst_1 : Add N] → (f : M →ₙ+ N) → {g : N → M} → Function.LeftInverse g ⇑f → M ≃+ ↥f.srange
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.rename_esymm : ∀ {τ : Type u_2} (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : Fintype τ] (n : ℕ)
  (e : σ ≃ τ), (MvPolynomial.rename ⇑e) (MvPolynomial.esymm σ R n) = MvPolynomial.esymm τ R n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {a k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.get? a =
    if h : compare k a = Ordering.eq then some (cast ⋯ v) else t.get? a
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflQuiver.id_eq_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C),
  CategoryTheory.ReflQuiver.id X = CategoryTheory.CategoryStruct.id X
-- Lean.Declaration
Lean.RecursorVal.getFirstIndexIdx : Lean.RecursorVal → ℕ
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.Prepartition.splitCenter.eq_1 : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι),
  BoxIntegral.Prepartition.splitCenter I =
    { boxes := Finset.map I.splitCenterBoxEmb Finset.univ, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSheafFor_iff_of_nat_equiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P₁ : CategoryTheory.Functor Cᵒᵖ (Type w)}
  {P₂ : CategoryTheory.Functor Cᵒᵖ (Type w')} (e : ⦃X : C⦄ → P₁.obj (Opposite.op X) ≃ P₂.obj (Opposite.op X)),
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (Opposite.op Y)),
      e ((CategoryTheory.ConcreteCategory.hom (P₁.map f.op)) x) =
        (CategoryTheory.ConcreteCategory.hom (P₂.map f.op)) (e x)) →
    ∀ {X : C} {R : CategoryTheory.Presieve X},
      CategoryTheory.Presieve.IsSheafFor P₁ R ↔ CategoryTheory.Presieve.IsSheafFor P₂ R
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- Given `f` a linear map into multilinear maps, then the derivative
of `x ↦ f (a x) (b₁ x, ..., bₙ x)` at `x` applied to a vector `v` is given by
`f (a' v) (b₁ x, ...., bₙ x) + ∑ i, f a (b₁ x, ..., b'ᵢ v, ..., bₙ x)`. Version inside a set.  -/
HasFDerivWithinAt.linear_multilinear_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {ι : Type u_2}
  {G : ι → Type u_3} [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)]
  [inst_7 : Fintype ι] {H : Type u_4} [inst_8 : NormedAddCommGroup H] [inst_9 : NormedSpace 𝕜 H]
  [inst_10 : DecidableEq ι] {a : H → E} {a' : H →L[𝕜] E} {b : (i : ι) → H → G i} {b' : (i : ι) → H →L[𝕜] G i}
  {s : Set H} {x : H},
  HasFDerivWithinAt a a' s x →
    (∀ (i : ι), HasFDerivWithinAt (b i) (b' i) s x) →
      ∀ (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F),
        HasFDerivWithinAt (fun y => (f (a y)) fun i => b i y)
          ((f.flipMultilinear fun i => b i x) ∘SL a' + ∑ i, (f (a x)).toContinuousLinearMap (fun j => b j x) i ∘SL b' i)
          s x
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- In a space with the Besicovitch property, any set `s` can be covered with balls whose measures
add up to at most `μ s + ε`, for any positive `ε`. This works even if one restricts the set of
allowed radii around a point `x` to a set `f x` which accumulates at `0`.  -/
Besicovitch.exists_closedBall_covering_tsum_measure_le : ∀ {α : Type u_1} [inst : MetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α]
  [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ]
  [μ.OuterRegular] {ε : ENNReal},
  ε ≠ 0 →
    ∀ (f : α → Set ℝ) (s : Set α),
      (∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) →
        ∃ t r,
          t.Countable ∧
            t ⊆ s ∧
              (∀ x ∈ t, r x ∈ f x) ∧
                s ⊆ ⋃ x ∈ t, Metric.closedBall x (r x) ∧ ∑' (x : ↑t), μ (Metric.closedBall (↑x) (r ↑x)) ≤ μ s + ε
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.reverse_involutive : ∀ {T : Type u_1}, Function.Involutive ContextFreeGrammar.reverse
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_eq_empty : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s : Set X}, (Convexity.convexHull R) s = ∅ ↔ s = ∅
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_def : ∀ (R : Type u) [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M N : Submodule R A),
  M * N = Submodule.span R (↑M * ↑N)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → k ∉ t₁ ∩ t₂
-- Mathlib.Order.KrullDimension
/-- Another characterization of coheight, based on the supremum of the coheights of elements above.
 -/
Order.coheight_eq_iSup_gt_coheight : ∀ {α : Type u_1} [inst : Preorder α] (x : α), Order.coheight x = ⨆ y, ⨆ (_ : y > x), Order.coheight y + 1
-- Mathlib.Order.Filter.AtTopBot.Finite
Filter.Tendsto.eventually_forall_le_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {l : Filter α} {p : β → Prop} {f : α → β},
  Filter.Tendsto f l Filter.atBot → (∀ᶠ (x : β) in Filter.atBot, p x) → ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insert!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF → ∀ {k : α} {v : β}, Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.insert! k v t) k = v
-- Mathlib.Control.Traversable.Equiv
/-- The fact that `t` is a lawful traversable functor carries over the
equivalences to `t'`, with the traversable functor structure given by
`Equiv.traversable`.  -/
Equiv.isLawfulTraversable : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] [LawfulTraversable t],
  LawfulTraversable t'
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.instFiniteObjOppositeSimplexCategoryOfFinite : ∀ (X : SSet) [X.Finite] (n : SimplexCategoryᵒᵖ), Finite (X.obj n)
-- Mathlib.RingTheory.Valuation.Discrete.RankOne
Valuation.IsRankOneDiscrete.generator'.eq_1 : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [inst_2 : v.IsRankOneDiscrete],
  Valuation.IsRankOneDiscrete.generator' v = ⟨Valuation.IsRankOneDiscrete.generator v, ⋯⟩