mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.toList_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
  {l : Std.DHashMap.Internal.AssocList α β},
  (Std.DHashMap.Internal.AssocList.alter a f l).toList.Perm (Std.Internal.List.alterKey a f l.toList)
-- Mathlib.CategoryTheory.Limits.Fubini
/-- `coneOfConeUncurry Q c` is a limit cone when `c` is a limit cone.
 -/
CategoryTheory.Limits.coneOfConeUncurryIsLimit : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              {D : CategoryTheory.Limits.DiagramOfCones F} →
                (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j)) →
                  {c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.uncurry.obj F)} →
                    CategoryTheory.Limits.IsLimit c →
                      CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfConeUncurry Q c)
-- Mathlib.RingTheory.Etale.StandardEtale
Algebra.IsStandardEtale.nonempty_standardEtalePresentation : ∀ {R : Type u_4} {S : Type u_5} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  [self : Algebra.IsStandardEtale R S], Nonempty (StandardEtalePresentation R S)
-- Std.Time.Date.Unit.Day
Std.Time.Day.instLEOffset : LE Std.Time.Day.Offset
-- Mathlib.Data.List.Pi
List.Pi.forall_rel_cons_ext : ∀ {ι : Type u_1} [inst : DecidableEq ι] {α : ι → Sort u_2} {i : ι} {l : List ι} {r : ⦃i : ι⦄ → α i → α i → Prop}
  {a₁ a₂ : α i} {f₁ f₂ : (j : ι) → j ∈ l → α j},
  r a₁ a₂ →
    (∀ (i : ι) (hi : i ∈ l), r (f₁ i hi) (f₂ i hi)) →
      ∀ (j : ι) (hj : j ∈ i :: l), r (List.Pi.cons i l a₁ f₁ j hj) (List.Pi.cons i l a₂ f₂ j hj)
-- Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
CategoryTheory.MonoidalCategory.Limits.HasColimit.isoOfNatIso_ι_hom_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {J : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {F G : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] [inst_4 : CategoryTheory.Limits.HasColimit G] (w : F ≅ G) (j : J)
  {Q Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Limits.colimit G) Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.colimit.ι F j) Q)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.HasColimit.isoOfNatIso w).hom Q) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (w.hom.app j) Q)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.colimit.ι G j) Q) h)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.NormalExpr.nil.injEq : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (α : Mathlib.Tactic.BicategoryLike.Structural)
  (e_1 : Mathlib.Tactic.BicategoryLike.Mor₂) (α_1 : Mathlib.Tactic.BicategoryLike.Structural),
  (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α = Mathlib.Tactic.BicategoryLike.NormalExpr.nil e_1 α_1) =
    (e = e_1 ∧ α = α_1)
-- Mathlib.Logic.Function.Iterate
/-- **Alias** of the forward direction of `Function.iterate_add_eq_iterate`. -/
Function.iterate_cancel_of_add : ∀ {α : Type u} {f : α → α} {m n : ℕ} {a : α}, Function.Injective f → f^[m + n] a = f^[n] a → f^[m] a = a
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.LocallyRingedSpace.comp_ring_hom_ext : ∀ {X : AlgebraicGeometry.LocallyRingedSpace} {R : CommRingCat}
  {f : R ⟶ AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)}
  {β : X ⟶ AlgebraicGeometry.Spec.locallyRingedSpaceObj R},
  CategoryTheory.CategoryStruct.comp X.toΓSpec.base (AlgebraicGeometry.Spec.locallyRingedSpaceMap f).base = β.base →
    (∀ (r : ↑R),
        CategoryTheory.CategoryStruct.comp f (X.presheaf.map (CategoryTheory.homOfLE ⋯).op) =
          CategoryTheory.CategoryStruct.comp
            (CommRingCat.ofHom
              (algebraMap (↑R)
                ((AlgebraicGeometry.structureSheafInType ↑R ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen r)))))
            (β.c.app (Opposite.op (PrimeSpectrum.basicOpen r)))) →
      CategoryTheory.CategoryStruct.comp X.toΓSpec (AlgebraicGeometry.Spec.locallyRingedSpaceMap f) = β
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.mk_eq_zero : ∀ {R : Type u_1} {M : Type u_2} {x : M} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (p : Submodule R M), Submodule.Quotient.mk x = 0 ↔ x ∈ p
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
PiTensorProduct.dualSeminorms_bounded : ∀ {ι : Type uι} [inst : Fintype ι] {𝕜 : Type u𝕜} [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type uE}
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)],
  BddAbove
    {p |
      ∃ G x x_1,
        p =
          (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp
            (PiTensorProduct.toDualContinuousMultilinearMap G)}
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.evenOdd_comap_reverse : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (n : ZMod 2),
  Submodule.comap CliffordAlgebra.reverse (CliffordAlgebra.evenOdd Q n) = CliffordAlgebra.evenOdd Q n
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.gc_map_comap : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'),
  GaloisConnection (LieIdeal.map f) (LieIdeal.comap f)
-- Mathlib.FieldTheory.Laurent
RatFunc.laurent_div : ∀ {R : Type u} [inst : CommRing R] (r : R) (p q : Polynomial R) [inst_1 : IsDomain R],
  (RatFunc.laurent r) ((algebraMap (Polynomial R) (RatFunc R)) p / (algebraMap (Polynomial R) (RatFunc R)) q) =
    (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p) /
      (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) q)
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Reversal of a `GenLoop` along the `i`th coordinate.  -/
GenLoop.symmAt : {N : Type u_1} →
  {X : Type u_2} → [inst : TopologicalSpace X] → {x : X} → [DecidableEq N] → N → ↑(GenLoop N X x) → ↑(GenLoop N X x)
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basis_pair_left : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {v : ι → F} {i j : ι},
  i ≠ j → Lagrange.basis {i, j} v i = Lagrange.basisDivisor (v i) (v j)
-- Std.Http.Data.Method
/-- Remove a URI binding from a resource.
Source: https://www.rfc-editor.org/rfc/rfc5842#section-5
 -/
Std.Http.Method.unbind : Std.Http.Method
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.w₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp h.p₃ f₃ = h.p
-- Mathlib.MeasureTheory.OuterMeasure.Operations
/-- The pushforward of `m` along `f`. The outer measure on `s` is defined to be `m (f ⁻¹' s)`.  -/
MeasureTheory.OuterMeasure.map : {α : Type u_1} → {β : Type u_3} → (α → β) → MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β
-- Mathlib.RingTheory.Ideal.Operations
/-- `3 : Ideal R` is *not* the ideal generated by 3 (which would be spelt
`Ideal.span {3}`), it is simply `1 + 1 + 1 = ⊤`.  -/
Ideal.ofNat_eq_top : ∀ {R : Type u} [inst : Semiring R] {n : ℕ} [inst_1 : n.AtLeastTwo], OfNat.ofNat n = ⊤
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.comp_inv_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X},
  CategoryTheory.CategoryStruct.comp f α.inv = g ↔ f = CategoryTheory.CategoryStruct.comp g α.hom
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.RefIdentJsonRepr.f.inj : ∀ {m i m_1 i_1 : String},
  Lean.Lsp.RefIdent.RefIdentJsonRepr.f m i = Lean.Lsp.RefIdent.RefIdentJsonRepr.f m_1 i_1 → m = m_1 ∧ i = i_1
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- Let `M` act continuously on an R₁ topological space `X`.
Let `μ` be a finite inner regular measure on `X` which is ergodic with respect to this action.
If a null measurable set `s` is a.e. equal
to its preimages under the action of a dense set of elements of `M`,
then it is either null or conull.  -/
aeconst_of_dense_setOfPred_preimage_vadd_ae : ∀ {M : Type u_1} [inst : TopologicalSpace M] {X : Type u_2} [inst_1 : TopologicalSpace X] [R1Space X]
  [inst_3 : MeasurableSpace X] [BorelSpace X] [inst_5 : VAdd M X] [ContinuousVAdd M X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ] {s : Set X},
  MeasureTheory.NullMeasurableSet s μ →
    Dense {g | (fun x => g +ᵥ x) ⁻¹' s =ᵐ[μ] s} → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Init.Data.String.Lemmas.Iterate
String.Model.revPositionsFrom_eq_cons : ∀ {s : String} {p : s.Pos} (hp : p ≠ s.startPos),
  String.Model.revPositionsFrom p = ⟨p.prev hp, ⋯⟩ :: String.Model.revPositionsFrom (p.prev hp)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
/-- The simplicial morphism on the simplicial object `Γ₀.obj K` induced by
a morphism `Δ' → Δ` in `SimplexCategory` is defined on each summand
associated to an `A : Splitting.IndexSet Δ` in terms of the epi-mono factorisation
of `θ ≫ A.e`.  -/
AlgebraicTopology.DoldKan.Γ₀.Obj.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        (K : ChainComplex C ℕ) →
          {Δ' Δ : SimplexCategoryᵒᵖ} →
            (Δ ⟶ Δ') → (AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ ⟶ AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ')
-- Lean.Data.SMap
Lean.SMap.fold : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → {σ : Type w} → (σ → α → β → σ) → σ → Lean.SMap α β → σ
-- Mathlib.Order.BourbakiWitt
CompleteLattice.ωScottContinuous.top : ∀ {α : Type u_1} {β : Type u_2} [inst : OmegaCompletePartialOrder α] [inst_1 : CompleteLattice β],
  OmegaCompletePartialOrder.ωScottContinuous ⊤
-- Mathlib.AlgebraicGeometry.Cover.Directed
/-- The canonical diagram induced by a locally directed cover.  -/
AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
      [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] →
        [𝒰.LocallyDirected] → CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Types.instFullForgetTypeFun : (CategoryTheory.forget (Type u)).Full
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.inv_absolutelyContinuous : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant], μ.inv.AbsolutelyContinuous μ
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.addCongrTable.isEqCongrSymm : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Topology.ClusterPt
/-- `x` is an accumulation point of a set `C` iff it is a cluster point of `C ∖ {x}`.  -/
accPt_principal_iff_clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {C : Set X},
  AccPt x (Filter.principal C) ↔ ClusterPt x (Filter.principal (C \ {x}))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.beq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.TreeMap α β cmp} [inst : BEq β] [Std.TransCmp cmp]
  [ReflBEq β], m₁.Equiv m₂ → (m₁ == m₂) = true
-- Lean.Message
/-- Strip the `` `nested`` prefix components added to tags by `throwNestedTacticEx`.  -/
Lean.MessageData.stripNestedTags : Lean.MessageData → Lean.MessageData
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- **Alias** of `CategoryTheory.Precoverage.IsStableUnderSup.sup_mem_coverings`. -/
CategoryTheory.Precoverage.sup_mem_coverings : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.IsStableUnderSup]
  {X : C} {R S : CategoryTheory.Presieve X}, R ∈ J.coverings X → S ∈ J.coverings X → R ⊔ S ∈ J.coverings X
-- Mathlib.Algebra.Field.Basic
div_add_one : ∀ {K : Type u_1} [inst : DivisionSemiring K] {a b : K}, b ≠ 0 → a / b + 1 = (a + b) / b
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.completeSpace : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], CompleteSpace ℤ_[p]
-- Lean.Parser.Extra
Lean.ppRealGroup.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toFinset_toMultiset : ∀ {α : Type u_1} [inst : DecidableEq α] (f : α →₀ ℕ), (Finsupp.toMultiset f).toFinset = f.support
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.op_smul_finset_smul_eq_smul_smul_finset : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq β] [inst_1 : DecidableEq γ] [inst_2 : SMul αᵐᵒᵖ β]
  [inst_3 : SMul β γ] [inst_4 : SMul α γ] (a : α) (s : Finset β) (t : Finset γ),
  (∀ (a : α) (b : β) (c : γ), (MulOpposite.op a • b) • c = b • a • c) → (MulOpposite.op a • s) • t = s • a • t
-- Batteries.Data.Nat.Lemmas
Nat.recDiag.eq_1 : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 n → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive m n → motive (m + 1) (n + 1))
  (m n : ℕ),
  Nat.recDiag zero_zero zero_succ succ_zero succ_succ m n =
    Nat.recDiagAux (Nat.recDiag.left zero_zero zero_succ) (Nat.recDiag.right zero_zero succ_zero) succ_succ m n
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.one_le_mulConst_self : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G}, A.Nonempty → 1 ≤ A.mulConst A
-- Mathlib.Data.Set.Image
Set.range_image : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Set.range (Set.image f) = 𝒫 Set.range f
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
vectorSpan.eq_1 : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P), vectorSpan k s = Submodule.span k (s -ᵥ s)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.prodMkRight γ κ)
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.testBit.match_1.eq_1 : ∀ (motive : PosNum → ℕ → Sort u_1) (h_1 : Unit → motive PosNum.one 0) (h_2 : (x : ℕ) → motive PosNum.one x)
  (h_3 : (a : PosNum) → motive a.bit0 0) (h_4 : (p : PosNum) → (n : ℕ) → motive p.bit0 n.succ)
  (h_5 : (a : PosNum) → motive a.bit1 0) (h_6 : (p : PosNum) → (n : ℕ) → motive p.bit1 n.succ),
  (match PosNum.one, 0 with
    | PosNum.one, 0 => h_1 ()
    | PosNum.one, x => h_2 x
    | a.bit0, 0 => h_3 a
    | p.bit0, n.succ => h_4 p n
    | a.bit1, 0 => h_5 a
    | p.bit1, n.succ => h_6 p n) =
    h_1 ()
-- Mathlib.RingTheory.Derivation.Basic
Derivation.map_natCast : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M)
  (n : ℕ), D ↑n = 0
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.clm_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {X : Type u_5} [inst_7 : NormedAddCommGroup X]
  [inst_8 : NormedSpace 𝕜 X] {n : WithTop ℕ∞} {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F},
  ContDiff 𝕜 n g → ContDiff 𝕜 n f → ContDiff 𝕜 n fun x => g x ∘SL f x
-- Mathlib.Analysis.Convex.GaugeRescale
gaugeRescale_def : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (s t : Set E) (x : E),
  gaugeRescale s t x = (gauge s x / gauge t x) • x
-- Aesop.Util.Basic
Aesop.forEachExprInLCtxCore : {ω : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] →
      [MonadLiftT (ST ω) m] →
        [Monad m] → Lean.LocalContext → (Lean.Expr → m Bool) → Lean.MonadCacheT Lean.Expr Unit m Unit
-- Init.System.IO
/-- Write the provided bytes to a binary file at the specified path.
 -/
IO.FS.writeBinFile : System.FilePath → ByteArray → IO Unit
-- Mathlib.AlgebraicTopology.CechNerve
/-- A helper function used in defining the Čech adjunction.  -/
CategoryTheory.SimplicialObject.cechNerveEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 :
        ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
          CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
      (X : CategoryTheory.SimplicialObject.Augmented C) →
        (F : CategoryTheory.Arrow C) →
          (CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) ≃ (X ⟶ F.augmentedCechNerve)
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_anti : ∀ {V : Type u_1} {G : SimpleGraph V} {s₁ s₂ : Set (Sym2 V)}, s₁ ⊆ s₂ → G.deleteEdges s₂ ≤ G.deleteEdges s₁
-- Mathlib.GroupTheory.Index
AddSubgroup.index_ne_zero_iff_finite : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index ≠ 0 ↔ Finite (G ⧸ H)
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.lift_single : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u_4} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k] (F : G →* A) (a : G) (b : k),
  ((SkewMonoidAlgebra.lift k G A) F) (SkewMonoidAlgebra.single a b) = b • F a
-- Mathlib.Data.Fintype.BigOperators
Finset.sum_toFinset_eq_subtype : ∀ {α : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Fintype α] (p : α → Prop) [inst_2 : DecidablePred p]
  (f : α → M), ∑ a ∈ {x | p x}.toFinset, f a = ∑ a, f ↑a
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Quiver.FreeGroupoid.congr_reverse_comp : ∀ {V : Type u} [inst : Quiver V] {X Y : CategoryTheory.Paths (Quiver.Symmetrify V)} (p : X ⟶ Y),
  Quot.mk (CategoryTheory.HomRel.CompClosure Quiver.FreeGroupoid.redStep)
      (CategoryTheory.CategoryStruct.comp (Quiver.Path.reverse p) p) =
    Quot.mk (CategoryTheory.HomRel.CompClosure Quiver.FreeGroupoid.redStep) (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_prodCongr : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7}
  {V₃ : Type u_8} {V₄ : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : AddCommGroup V₄] [inst_5 : Module k V₁] [inst_6 : Module k V₂]
  [inst_7 : Module k V₃] [inst_8 : Module k V₄] [inst_9 : AddTorsor V₁ P₁] [inst_10 : AddTorsor V₂ P₂]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₃ ≃ᵃ[k] P₄),
  ↑(e₁.prodCongr e₂) = (↑e₁).prodMap ↑e₂
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mk_out : ∀ (x : ZFSet.{u_1}), ZFSet.mk (Quotient.out x) = x
-- Mathlib.Order.Heyting.Basic
BiheytingAlgebra.toSDiff : {α : Type u_4} → [self : BiheytingAlgebra α] → SDiff α
-- Mathlib.Analysis.Calculus.DSlope
dslope_eventuallyEq_slope_nhdsNE : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {a : 𝕜} (f : 𝕜 → E), dslope f a =ᶠ[nhdsWithin a {a}ᶜ] slope f a
-- Lean.Meta.Canonicalizer
_private.Lean.Meta.Canonicalizer.0.Lean.Meta.Canonicalizer.mkKey.unsafe_8 : Lean.Expr → UInt64 → Lean.Meta.CanonM PUnit.{1}
-- Mathlib.Order.Interval.Basic
NonemptyInterval.mem_mk : ∀ {α : Type u_1} [inst : Preorder α] {x : α × α} {a : α} {hx : x.1 ≤ x.2},
  a ∈ { toProd := x, fst_le_snd := hx } ↔ x.1 ≤ a ∧ a ≤ x.2
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
IsUniformAddGroup.comap : ∀ {G : Type u_1} {H : Type u_2} {hom : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup H] {u : UniformSpace H}
  [IsUniformAddGroup H] [inst_3 : FunLike hom G H] [AddMonoidHomClass hom G H] (f : hom), IsUniformAddGroup G
-- Mathlib.Algebra.Algebra.RestrictScalars
/-- Tautological ring isomorphism `RestrictScalars R S A ≃+* A`.  -/
RestrictScalars.ringEquiv : (R : Type u_1) → (S : Type u_2) → (A : Type u_4) → [inst : Semiring A] → RestrictScalars R S A ≃+* A
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- Centralizer of a cycle is a power of that cycle on the cycle  -/
Equiv.Perm.IsCycle.commute_iff' : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] {g c : Equiv.Perm α},
  c.IsCycle →
    (Commute g c ↔
      ∃ (hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.productIsProduct.eq_1 : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : β → C)
  [inst_1 : CategoryTheory.Limits.HasProduct f],
  CategoryTheory.Limits.productIsProduct f =
    (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor f)).ofIsoLimit
      (CategoryTheory.Limits.Cone.ext
        (CategoryTheory.Iso.refl (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor f)).pt) ⋯)
-- Mathlib.LinearAlgebra.Finsupp.LSum
Submodule.mulRightMap_apply : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : SMulCommClass R R S] [inst_4 : IsScalarTower R S S] {M N : Submodule R S} {ι : Type u_5} (n : ι → ↥N)
  (m : ι →₀ ↥M), (M.mulRightMap n) m = m.sum fun i m => ↑m * ↑(n i)
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_neg_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.covariance (fun ω => -X ω) Y μ = -ProbabilityTheory.covariance X Y μ
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- Given a prepartition `π` of a box `I` and a collection of prepartitions `πi J` of all boxes
`J ∈ π`, returns the prepartition of `I` into the union of the boxes of all `πi J`.

Though we only use the values of `πi` on the boxes of `π`, we require `πi` to be a globally defined
function.  -/
BoxIntegral.Prepartition.biUnion : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    BoxIntegral.Prepartition I → ((J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) → BoxIntegral.Prepartition I
-- Init.Data.Int.DivMod.Bootstrap
Int.zero_dvd : ∀ {n : ℤ}, 0 ∣ n ↔ n = 0
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- The maximum degree in the graph is at least the degree of any particular vertex.  -/
SimpleGraph.degree_le_maxDegree : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (v : V), G.degree v ≤ G.maxDegree
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion_one : ∀ (h : ℝ), UpperHalfPlane.qExpansion h 1 = 1
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_congr' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] [inst_1 : NormedAddCommGroup γ] {f : α → β} {g : α → γ},
  (∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) → (MeasureTheory.HasFiniteIntegral f μ ↔ MeasureTheory.HasFiniteIntegral g μ)