mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Discriminant
/-- Mapping a family of vectors along an `AlgEquiv` preserves the discriminant.  -/
Algebra.discr_eq_discr_of_algEquiv : ∀ {A : Type u} {B : Type v} {C : Type z} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [inst_4 : CommRing C] [inst_5 : Algebra A C] [inst_6 : Fintype ι] (b : ι → B) (f : B ≃ₐ[A] C),
  Algebra.discr A b = Algebra.discr A (⇑f ∘ b)
-- Lean.Parser.Term
Lean.Parser.Term.matchExprPat.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Holor
Holor.slice_sum : ∀ {α : Type} {d : ℕ} {ds : List ℕ} [inst : AddCommMonoid α] {β : Type} (i : ℕ) (hid : i < d) (s : Finset β)
  (f : β → Holor α (d :: ds)), ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on `R`, the closed unit ball
around zero `{x | v x ≤ 1}` is closed in the valuative topology.  -/
Valuation.isClosed_integer : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible], IsClosed ↑v.integer
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.Order.InitialSeg
RelEmbedding.codRestrict.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f f_1 : r ↪r s) (e_f : f = f_1)
  (H : ∀ (a : α), f a ∈ p), RelEmbedding.codRestrict p f H = RelEmbedding.codRestrict p f_1 ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformlyOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] (f : ι → β → α) (g : β → α) (s : Set β)
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasProdLocallyUniformlyOn f g s = TendstoLocallyUniformlyOn (fun x1 x2 => ∏ i ∈ x1, f i x2) g Filter.atTop s
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.registerMVarArgName : Lean.MVarId → Lean.Name → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.map_π_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G],
  CategoryTheory.Epi (G.map (CategoryTheory.Limits.coequalizer.π f g))
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'}
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') {Z : C}
  (h : CategoryTheory.Limits.kernel f' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map f f' sq.left sq.right ⋯) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f').hom h)
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.normBound_spec : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {L : Submodule ℤ E} [inst_3 : DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (i : ι),
  ZLattice.normBound b * ↑|(b.repr x) i| ≤ ‖x‖
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_quotient : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Setoid α} {t : Set (Quotient s)},
  MeasurableSet t ↔ MeasurableSet (Quotient.mk'' ⁻¹' t)
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.centralizer_eq_top_iff_subset : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G}, AddSubgroup.centralizer s = ⊤ ↔ s ⊆ ↑(AddSubgroup.center G)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).getKey! k =
        if (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true then k else default
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Nat.Iio_succ_eq_of_Icc_zero_eq : ∀ {n : ℕ} {s : Finset ℕ}, Finset.Icc 0 n = s → Finset.Iio (n + 1) = s
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine.go : ℕ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Std.Data.DTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.DTreeMap.Const.entryAtIdxD : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → ℕ → α × β → α × β
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousSMul.toMeasurableSMul : ∀ {M : Type u_7} {α : Type u_8} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace α] [inst_2 : MeasurableSpace M]
  [inst_3 : MeasurableSpace α] [OpensMeasurableSpace M] [BorelSpace α] [inst_6 : SMul M α] [ContinuousSMul M α],
  MeasurableSMul M α
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyπ_comp_asIsoHomologyπ_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [inst_2 : S.HasHomology] {Z : C} (h : S.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.homologyπ (CategoryTheory.CategoryStruct.comp (S.asIsoHomologyπ hf).inv h) = h
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α},
  m.WF →
    (k ∈ Std.DHashMap.Raw.filterMap f m ↔
      ∃ (h : k ∈ m), (f (m.getKey k h) (Std.DHashMap.Raw.Const.get m k h)).isSome = true)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ran.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F],
  L.ran =
    { obj := fun F => L.rightKanExtension F,
      map := fun {F₁ F₂} φ =>
        (L.rightKanExtension F₂).liftOfIsRightKanExtension (L.rightKanExtensionCounit F₂) (L.rightKanExtension F₁)
          (CategoryTheory.CategoryStruct.comp (L.rightKanExtensionCounit F₁) φ),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Bundle.Trivialization.localFrame.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {M : Type u_4} [inst_1 : TopologicalSpace M] {F : Type u_5}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {V : M → Type u_6}
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_5 : (x : M) → AddCommGroup (V x)]
  [inst_6 : (x : M) → Module 𝕜 (V x)] [inst_7 : (x : M) → TopologicalSpace (V x)] [inst_8 : FiberBundle F V]
  [inst_9 : VectorBundle 𝕜 F V] {ι : Type u_7} (e e_1 : Bundle.Trivialization F Bundle.TotalSpace.proj) (e_e : e = e_1)
  [inst_10 : MemTrivializationAtlas e] (b b_1 : Module.Basis ι 𝕜 F),
  b = b_1 → ∀ (a a_1 : ι), a = a_1 → ∀ (x : M), e.localFrame b a x = e_1.localFrame b_1 a_1 x
-- Aesop.Search.Expansion.Norm
Aesop.normUnfold : Lean.MVarId → Aesop.NormM (Option Aesop.NormRuleResult)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.FixPoint.markModified : Lean.Elab.Term.MutualClosure.FixPoint.M Unit
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_one : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), ↑1 = 1
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldr_reverse : ∀ {α : Type u_1} {β : Type u_2} {t : RBTree.RBNode α} {f : α → β → β} {init : β},
  RBTree.RBNode.foldr f t.reverse init = RBTree.RBNode.foldl (flip f) init t
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.algebraOverBot : {F : Type u_1} → [inst : Field F] → {E : Type u_2} → [inst_1 : Field E] → [inst_2 : Algebra F E] → Algebra (↥⊥) F
-- Mathlib.Control.Monad.Cont
MonadCont.Label.mk : {α : Type w} → {m : Type u → Type v} → {β : Type u} → (α → m β) → MonadCont.Label α m β
-- Mathlib.Algebra.Order.Module.Archimedean
ArchimedeanClass.mk_smul : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {K : Type u_2}
  [inst_3 : Ring K] [inst_4 : LinearOrder K] [IsOrderedRing K] [Archimedean K] [inst_7 : Module K M] [PosSMulMono K M]
  (a : M) {k : K}, k ≠ 0 → ArchimedeanClass.mk (k • a) = ArchimedeanClass.mk a
-- Mathlib.RepresentationTheory.Induced
Rep.coinvariantsTensorIndIso_inv : ∀ {k : Type u} [inst : CommRing k] {G H : Type u} [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  (A : Rep.{u, u, u} k G) (B : Rep.{u, u, u} k H),
  (Rep.coinvariantsTensorIndIso φ A B).inv = Rep.coinvariantsTensorIndInv φ A B
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.stopPos : ∀ {l m r : List Char} {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s → s.stopPos = { byteIdx := String.utf8Len l + String.utf8Len m }
-- Init.System.ST
instSTWorldST : {σ : Type} → STWorld σ (ST σ)
-- Aesop.Search.Queue
Aesop.LIFOQueue.init : Aesop.LIFOQueue
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ioo_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b : α) {c : α},
  c < 0 → (fun x => c * x) ⁻¹' Set.Ioo a b = Set.Ioo (b / c) (a / c)
-- Mathlib.Algebra.Module.BigOperators
Finset.sum_smul_sum : ∀ {α : Type u_3} {β : Type u_4} {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (s : Finset α) (t : Finset β) {f : α → R} {g : β → M},
  (∑ i ∈ s, f i) • ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i • g j
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.AndKind.ofNat : ℕ → Mathlib.Tactic.ITauto.AndKind
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.trailingWhitespace.sizeOf_spec : sizeOf Mathlib.Linter.TextBased.StyleError.trailingWhitespace✝ = 1
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddZeroClass : {α : Type u_2} → [inst : Small.{v, u_2} α] → [AddZeroClass α] → AddZeroClass (Shrink.{v, u_2} α)
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.mapsTo_closedEBall : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ENNReal), Set.MapsTo f (Metric.closedEBall x r) (Metric.closedEBall (f x) r)
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.divRight_apply : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul Gᵐᵒᵖ G] (c b : G),
  (IsometryEquiv.divRight c) b = b / c
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.continuous_fst : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  Continuous WithLp.fst
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- Sum of elements in an `AddSubmonoid` of an `AddCommMonoid` indexed by a `Finset`
is in the `AddSubmonoid`.  -/
AddSubmonoid.sum_mem : ∀ {M : Type u_4} [inst : AddCommMonoid M] (S : AddSubmonoid M) {ι : Type u_5} {t : Finset ι} {f : ι → M},
  (∀ c ∈ t, f c ∈ S) → ∑ c ∈ t, f c ∈ S
-- Mathlib.Algebra.Notation.Prod
Prod.swap_add : ∀ {M : Type u_8} {N : Type u_9} [inst : Add M] [inst_1 : Add N] (p q : M × N), (p + q).swap = p.swap + q.swap
-- Lean.CoreM
Lean.Core.State.mk.injEq : ∀ (env : Lean.Environment) (nextMacroScope : Lean.MacroScope) (ngen : Lean.NameGenerator)
  (auxDeclNGen : Lean.DeclNameGenerator) (traceState : Lean.TraceState) (cache : Lean.Core.Cache)
  (messages : Lean.MessageLog) (infoState : Lean.Elab.InfoState)
  (snapshotTasks : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) (env_1 : Lean.Environment)
  (nextMacroScope_1 : Lean.MacroScope) (ngen_1 : Lean.NameGenerator) (auxDeclNGen_1 : Lean.DeclNameGenerator)
  (traceState_1 : Lean.TraceState) (cache_1 : Lean.Core.Cache) (messages_1 : Lean.MessageLog)
  (infoState_1 : Lean.Elab.InfoState) (snapshotTasks_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  ({ env := env, nextMacroScope := nextMacroScope, ngen := ngen, auxDeclNGen := auxDeclNGen, traceState := traceState,
        cache := cache, messages := messages, infoState := infoState, snapshotTasks := snapshotTasks } =
      { env := env_1, nextMacroScope := nextMacroScope_1, ngen := ngen_1, auxDeclNGen := auxDeclNGen_1,
        traceState := traceState_1, cache := cache_1, messages := messages_1, infoState := infoState_1,
        snapshotTasks := snapshotTasks_1 }) =
    (env = env_1 ∧
      nextMacroScope = nextMacroScope_1 ∧
        ngen = ngen_1 ∧
          auxDeclNGen = auxDeclNGen_1 ∧
            traceState = traceState_1 ∧
              cache = cache_1 ∧ messages = messages_1 ∧ infoState = infoState_1 ∧ snapshotTasks = snapshotTasks_1)
-- Mathlib.RingTheory.PicardGroup
/-- If `M` is an invertible `R`-module, `(· ⊗[R] M)` is an auto-equivalence of the category
of `R`-modules.  -/
Module.Invertible.rTensorEquiv : {R : Type u} →
  {M : Type v} →
    {N : Type u_1} →
      (P : Type u_2) →
        (Q : Type u_3) →
          [inst : CommSemiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid N] →
                [inst_3 : AddCommMonoid P] →
                  [inst_4 : AddCommMonoid Q] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R N] →
                        [inst_7 : Module R P] →
                          [inst_8 : Module R Q] →
                            (TensorProduct R M N ≃ₗ[R] R) →
                              (P →ₗ[R] Q) ≃ₗ[R] TensorProduct R P M →ₗ[R] TensorProduct R Q M
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.comm_ring_aux₂ : (p : ℕ) → (R : Type u_1) → [Fact (Nat.Prime p)] → CommRing (WittVector p (MvPolynomial R ℤ))
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets.of_precomp : ∀ {Ω : Type u_1} {ι : Type u_2} {π : ι → Set (Set Ω)} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ι' : Type u_6} {g : ι' → ι},
  Function.Surjective g → ProbabilityTheory.iIndepSets (π ∘ g) μ → ProbabilityTheory.iIndepSets π μ
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.add.sizeOf_spec : ∀ (a b : Int.Internal.Linear.Expr), sizeOf (a.add b) = 1 + sizeOf a + sizeOf b
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.injective_codRestrict : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S),
  Function.Injective ⇑(NonUnitalAlgHom.codRestrict f S hf) ↔ Function.Injective ⇑f
-- Mathlib.Tactic.Sat.FromLRAT
/-- Asserts that `¬⟦c⟧_v` implies `p`.  -/
Sat.Clause.reify : Sat.Valuation → Sat.Clause → Prop → Prop
-- Mathlib.Algebra.Homology.ImageToKernel
instMonoImageToKernel : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [inst_3 : CategoryTheory.Limits.HasKernel g]
  (w : CategoryTheory.CategoryStruct.comp f g = 0), CategoryTheory.Mono (imageToKernel f g w)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.linearIndependent : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  AlgebraicIndependent R x → LinearIndependent R x
-- Mathlib.FieldTheory.Fixed
instIsInvariantSubringOfIsInvariantSubfield : ∀ (M : Type u) [inst : Monoid M] {F : Type v} [inst_1 : Field F] [inst_2 : MulSemiringAction M F] (S : Subfield F)
  [IsInvariantSubfield M S], IsInvariantSubring M S.toSubring
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformContinuousOn.comp_tendstoUniformly_eventually : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : UniformSpace β] [inst_1 : UniformSpace γ]
  {p : Filter ι} {s : Set β} {F : ι → α → β} {f : α → β} {g : β → γ},
  (∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s) →
    (∀ (x : α), f x ∈ s) →
      UniformContinuousOn g s → TendstoUniformly F f p → TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_eq_coe_iff_of_mem_Ico : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)]
  {a : 𝕜} [Archimedean 𝕜] {x y : 𝕜}, x ∈ Set.Ico a (a + p) → y ∈ Set.Ico a (a + p) → (↑x = ↑y ↔ x = y)
-- Mathlib.Algebra.Ring.GeomSum
Commute.mul_geom_sum₂ : ∀ {R : Type u_1} [inst : Ring R] {x y : R},
  Commute x y → ∀ (n : ℕ), (x - y) * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n
-- Mathlib.Order.CompleteBooleanAlgebra
sInf_codisjoint_iff : ∀ {α : Type u} [inst : Order.Coframe α] {a : α} {s : Set α}, Codisjoint (sInf s) a ↔ ∀ b ∈ s, Codisjoint b a
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
isSimplyConnected_smul_set_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {G : Type u_3} [inst_1 : Group G] [inst_2 : MulAction G X]
  [ContinuousConstSMul G X] {c : G} {s : Set X}, IsSimplyConnected (c • s) ↔ IsSimplyConnected s
-- Lean.Meta.Match.Basic
/-- Apply the free variable substitution `s` to the given pattern  -/
Lean.Meta.Match.Pattern.applyFVarSubst : Lean.Meta.FVarSubst → Lean.Meta.Match.Pattern → Lean.Meta.Match.Pattern
-- Mathlib.MeasureTheory.Group.Arithmetic
Finset.aemeasurable_sum : ∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} [inst : AddCommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, AEMeasurable (f i) μ) → AEMeasurable (∑ i ∈ s, f i) μ
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.WeakEquivalence.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.weakEquivalences C f → HomotopicalAlgebra.WeakEquivalence f
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.computeSize : {α : Type u} → {β : α → Type v} → Array (Std.DHashMap.Internal.AssocList α β) → ℕ
-- Init.Data.Float.Float
/-- Computes the hyperbolic arc tangent (inverse tangent) of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`atanh`.
 -/
Float.atanh : Float → Float
-- Lean.Meta.Basic
Lean.Meta.instInhabitedConfigWithKey : Inhabited Lean.Meta.ConfigWithKey
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I} (h : π₂.iUnion = ↑I \ π₁.iUnion),
  (π₁.disjUnion π₂ ⋯).IsPartition
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.conj_smul_le_of_le : ∀ {G : Type u_2} [inst : Group G] {P H : Subgroup G}, P ≤ H → ∀ (h : ↥H), MulAut.conj ↑h • P ≤ H
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasStrictDerivAt_iff_hasStrictFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [inst_4 : ContinuousSMul 𝕜 F],
  HasStrictDerivAt f f' x ↔ HasStrictFDerivAt f (ContinuousLinearMap.toSpanSingleton 𝕜 f') x
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.instUnique : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        {d : F.WellOrderInductionData} →
          [inst_2 : OrderBot J] →
            {val₀ : F.obj (Opposite.op ⊥)} → [WellFoundedLT J] → (j : J) → Unique (d.Extension val₀ j)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_eq_coe_nat : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (n : ℕ), MvPolynomial.C ↑n = ↑n
-- Std.Time.DateTime.Timestamp
Std.Time.instOrdTimestamp : Ord Std.Time.Timestamp
-- Mathlib.GroupTheory.Commensurable
Subgroup.Commensurable.eq : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  H.Commensurable K → Subgroup.Commensurable.commensurator H = Subgroup.Commensurable.commensurator K
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Adj.ne : ∀ {V : Type u} {G : SimpleGraph V} {a b : V}, G.Adj a b → a ≠ b
-- Lean.Expr
Lean.instHashableMVarId : Hashable Lean.MVarId
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_vadd_right_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P} {v : V}, v ∈ s.direction → (s.WOppSide x (v +ᵥ y) ↔ s.WOppSide x y)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.pairing_reflectionPerm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j k : ι),
  P.pairing j ((P.reflectionPerm i) k) = P.pairing ((P.reflectionPerm i) j) k
-- Mathlib.Algebra.Order.Group.Lattice
inf_add_sup : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b : α), a ⊓ b + a ⊔ b = a + b
-- Mathlib.Order.WithBot
WithBot.lt_unbotD_iff : ∀ {α : Type u_1} {a b : α} [inst : LT α] {x : WithBot α}, x ≠ ⊥ → (b < WithBot.unbotD a x ↔ ↑b < x)
-- Mathlib.Order.Types.Defs
OrderType.lift_type_le_iff : ∀ {α β : Type u} [inst : LinearOrder α] [inst_1 : LinearOrder β],
  OrderType.lift.{u_1, u} (OrderType.type α) ≤ OrderType.lift.{u_1, u} (OrderType.type β) ↔ Nonempty (α ↪o β)
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.instInhabited : Inhabited FintypeCat
-- Mathlib.Data.Multiset.Filter
Multiset.filter_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (b : α),
  Multiset.filter (Eq b) s = Multiset.replicate (Multiset.count b s) b
-- Mathlib.Analysis.Convex.Extreme
/-- **Alias** of `Convex.mem_extremePoints_iff_convex_sdiff`. -/
Convex.mem_extremePoints_iff_convex_diff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [DenselyOrdered 𝕜] [Module.IsTorsionFree 𝕜 E] {A : Set E} {x : E},
  Convex 𝕜 A → (x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ Convex 𝕜 (A \ {x}))
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- Multiplication of the dihedral group.
 -/
_private.Mathlib.GroupTheory.SpecificGroups.Dihedral.0.DihedralGroup.mul : {n : ℕ} → DihedralGroup n → DihedralGroup n → DihedralGroup n
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- Theorem 23 of [grinberg_clifford_2016]  -/
CliffordAlgebra.changeForm_contractLeft : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
  (d : Module.Dual R M) (x : CliffordAlgebra Q),
  (CliffordAlgebra.changeForm h) ((CliffordAlgebra.contractLeft d) x) =
    (CliffordAlgebra.contractLeft d) ((CliffordAlgebra.changeForm h) x)