mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Calculus
Differentiable.dist : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f g : G → E},
  Differentiable ℝ f → Differentiable ℝ g → (∀ (x : G), f x ≠ g x) → Differentiable ℝ fun y => dist (f y) (g y)
-- Mathlib.MeasureTheory.MeasurableSpace.Card
MeasurableSpace.generateMeasurableRec.eq_1 : ∀ {α : Type u} (s : Set (Set α)) (i : Ordinal.{u_1}),
  MeasurableSpace.generateMeasurableRec s i =
    (s ∪ {∅} ∪ compl '' ⋃ j, ⋃ (_ : j < i), MeasurableSpace.generateMeasurableRec s j) ∪ Set.range fun f => ⋃ n, ↑(f n)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- Since `Truncated.inclusion` is fully faithful, so is right Kan extension along it.  -/
SSet.Truncated.cosk.fullyFaithful : (n : ℕ) → (SSet.Truncated.cosk n).FullyFaithful
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_inter_add_sdiff' : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set α} (t : Set α),
  (s ∩ Function.support f).Finite →
    ∑ᶠ (i : α) (_ : i ∈ s ∩ t), f i + ∑ᶠ (i : α) (_ : i ∈ s \ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atom.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a b : ℤ),
  IsEllipticNet.atom W a b = W ((a + b).tdiv 2) * W ((a - b).tdiv 2)
-- Mathlib.Order.Monotone.Defs
StrictMono.comp_strictAntiOn : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α}, StrictMono g → StrictAntiOn f s → StrictAntiOn (g ∘ f) s
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
/-- In this version of the spectral mapping theorem, we assume the spectrum
is nonempty instead of assuming the degree of the polynomial is positive.  -/
spectrum.map_polynomial_aeval_of_nonempty : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A)
  (p : Polynomial 𝕜),
  (spectrum 𝕜 a).Nonempty → spectrum 𝕜 ((Polynomial.aeval a) p) = (fun k => Polynomial.eval k p) '' spectrum 𝕜 a
-- Mathlib.Order.CompleteLattice.Basic
isLUB_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α}, IsLUB (Set.range f) (⨆ j, f j)
-- Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.LintVerbosity.low.sizeOf_spec : sizeOf Batteries.Tactic.Lint.LintVerbosity.low = 1
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
/-- `(d/dx) lim_{n → ∞} f n x = lim_{n → ∞} f' n x` when the `f' n` converge
_uniformly_ to their limit.  -/
hasFDerivAt_of_tendstoUniformly : ∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3}
  [inst_1 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] {G : Type u_4}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] {f : ι → E → G} {g : E → G} {f' : ι → E → E →L[𝕜] G}
  {g' : E → E →L[𝕜] G} [l.NeBot],
  TendstoUniformly f' g' l →
    (∀ (n : ι) (x : E), HasFDerivAt (f n) (f' n x) x) →
      (∀ (x : E), Filter.Tendsto (fun n => f n x) l (nhds (g x))) → ∀ (x : E), HasFDerivAt g (g' x) x
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.FunInfoEnvCacheKey.mk : Lean.Name → List Lean.Level → Option ℕ → Lean.Meta.FunInfoEnvCacheKey✝
-- Mathlib.RingTheory.AdicCompletion.Basic
IsHausdorff.subsingleton : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsHausdorff ⊤ M → Subsingleton M
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.abs_pos_of_ne_zero : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a : α}, a ≠ 0 → 0 < |a|
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.injOn_support_of_isPath_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} {p : G.Walk u v} {f : G →g G'},
  (SimpleGraph.Walk.map f p).IsPath → Set.InjOn ⇑f {w | w ∈ p.support}
-- Mathlib.Logic.Equiv.Prod
Equiv.prodShear_apply : ∀ {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂),
  ⇑(e₁.prodShear e₂) = fun x => (e₁ x.1, (e₂ x.1) x.2)
-- Mathlib.LinearAlgebra.Dual.Defs
/-- The bijection between a reflexive module and its double dual, bundled as a `LinearEquiv`.  -/
Module.evalEquiv : (R : Type u_3) →
  (M : Type u_4) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [Module.IsReflexive R M] → M ≃ₗ[R] Module.Dual R (Module.Dual R M)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Returns `true` if `e` is already associated with a cutsat variable.  -/
Lean.Meta.Grind.Arith.Cutsat.hasVar : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The equivalence `(ComposableArrows C n)ᵒᵖ ≌ ComposableArrows Cᵒᵖ n` obtained
by reversing the arrows.  -/
CategoryTheory.ComposableArrows.opEquivalence : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (n : ℕ) → (CategoryTheory.ComposableArrows C n)ᵒᵖ ≌ CategoryTheory.ComposableArrows Cᵒᵖ n
-- Mathlib.Data.Num.Bitwise
SNum.nz : NzsNum → SNum
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toArray_roo_eq_fallback : ∀ {m n fallback : ℤ} {i : ℕ}, (n - (m + 1)).toNat ≤ i → (m<...n).toArray.getD i fallback = fallback
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α} {h : k ∈ Std.TreeMap.filterMap f t},
  (Std.TreeMap.filterMap f t)[k] = (f (t.getKey k ⋯) t[k]).get ⋯
-- Mathlib.Control.Functor
/-- The `<*>` operation for the composition of applicative functors.  -/
Functor.Comp.seq : {F : Type u → Type w} →
  {G : Type v → Type u} →
    [Applicative F] →
      [Applicative G] → {α β : Type v} → Functor.Comp F G (α → β) → (Unit → Functor.Comp F G α) → Functor.Comp F G β
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.normalizer.eq_1 : ∀ {G : Type u_1} [inst : Group G] (S : Set G),
  Subgroup.normalizer S =
    { carrier := {g | ∀ (n : G), n ∈ S ↔ g * n * g⁻¹ ∈ S}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.GroupTheory.OrderOfElement
mod_card_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] (a : G) (n : ℕ), (n % Fintype.card G) • a = n • a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.alter.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → ∀ (a : α) (f f_1 : Option (β a) → Option (β a)), f = f_1 → t.alter a f = t_1.alter a f_1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey?_eq_getKey?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β), l.getKey? k = l.getKey?ₘ k
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getD_eq_getDₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] (k : α)
  (l : Std.DTreeMap.Internal.Impl α β) (fallback : β k),
  l.getD k fallback = Std.DTreeMap.Internal.Impl.getDₘ k l fallback
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
ExteriorAlgebra.GradedAlgebra.liftι.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ExteriorAlgebra.GradedAlgebra.liftι R M = (ExteriorAlgebra.lift R) ⟨ExteriorAlgebra.GradedAlgebra.ι R M, ⋯⟩
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getEntry!ₘ_eq_getEntry! : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} [inst_4 : Inhabited ((a : α) × β a)],
      m.getEntry!ₘ a = Std.Internal.List.getEntry! a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfLEArgs.le_total : ∀ {α : Type u} (self : Std.Packages.LinearPreorderOfLEArgs α) (a b : α), a ≤ b ∨ b ≤ a
-- Std.Tactic.BVDecide.LRAT.Actions
/-- `β` is for the type of a clause, `α` is for the type of variables  -/
Std.Tactic.BVDecide.LRAT.Action : Type u → Type v → Type (max u v)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.snd_op_opIso_hom_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op P ⊞ Opposite.op Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd.op
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  m.getKey? k = some k' →
    Std.DHashMap.Const.get! (Std.DHashMap.filterMap f m) k = ((Std.DHashMap.Const.get? m k).bind (f k')).get!
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.subtypeVal.match_1.splitter : (motive : (x : ℕ) → (x_1 : TypeVec.{u_1} x) → x_1.Arrow (TypeVec.repeat x Prop) → Fin2 x → Sort u_2) →
  (x : ℕ) →
    (x_1 : TypeVec.{u_1} x) →
      (x_2 : x_1.Arrow (TypeVec.repeat x Prop)) →
        (x_3 : Fin2 x) →
          ((n : ℕ) →
              (x : TypeVec.{u_1} n.succ) →
                (x_4 : x.Arrow (TypeVec.repeat n.succ Prop)) → (i : Fin2 n) → motive n.succ x x_4 i.fs) →
            ((n : ℕ) →
                (x : TypeVec.{u_1} n.succ) →
                  (x_4 : x.Arrow (TypeVec.repeat n.succ Prop)) → motive n.succ x x_4 Fin2.fz) →
              motive x x_1 x_2 x_3
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β}, k ∉ m₂ → Std.DHashMap.Const.getD (m₁.inter m₂) k fallback = fallback
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β k}, k ∉ t₂ → (t₁ ∩ t₂).getD k fallback = fallback
-- Init.Data.SInt.Lemmas
Int8.toUInt8_sub : ∀ (a b : Int8), (a - b).toUInt8 = a.toUInt8 - b.toUInt8
-- Init.Data.Fin.Lemmas
Fin.subNat_mk : ∀ {n m i : ℕ} (h₁ : i < n + m) (h₂ : m ≤ i), Fin.subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, ⋯⟩
-- Init.Prelude
/-- Decides whether two 64-bit unsigned integers are equal. Usually accessed via the
`DecidableEq UInt64` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `UInt64.decEq 123 123 = .isTrue rfl`
 * `(if (6 : UInt64) = 7 then "yes" else "no") = "no"`
 * `show (7 : UInt64) = 7 by decide`
 -/
UInt64.decEq : (a b : UInt64) → Decidable (a = b)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_diff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂).getKey k h_mem = m₁.getKey k ⋯
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.NormalExpr.zero.inj : ∀ {e e_1 : Lean.Expr}, Mathlib.Tactic.Abel.NormalExpr.zero e = Mathlib.Tactic.Abel.NormalExpr.zero e_1 → e = e_1
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.highestWeight_apply : ∀ {μ : YoungDiagram} {i j : ℕ}, (SemistandardYoungTableau.highestWeight μ) i j = if (i, j) ∈ μ then i else 0
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.Small.bind : ∀ {α : Type v} {β : Type w} (P : α → Prop) (Q : α → β → Prop),
  Std.Internal.Small { a // P a } →
    (∀ (a : α), Std.Internal.Small { b // Q a b }) → Std.Internal.Small { b // ∃ a, P a ∧ Q a b }
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.minimalPeriod_le : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, 0 < n → Function.IsPeriodicPt f n x → Function.minimalPeriod f x ≤ n
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.colorable_chromaticNumber : ∀ {V : Type u} {G : SimpleGraph V} {m : ℕ}, G.Colorable m → G.Colorable G.chromaticNumber.toNat
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.ofMul_eq_bot : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderBot α] {a : α}, Additive.ofMul a = ⊥ ↔ a = ⊥
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  (F : CategoryTheory.Functor Cᵒᵖ GrpCat) (α : (F.comp (CategoryTheory.forget GrpCat)).RepresentableBy X),
  (CategoryTheory.yonedaGrpObjIsoOfRepresentableBy X F α).inv =
    { app := fun X_1 => GrpCat.ofHom ↑{ toEquiv := α.homEquiv.symm, map_mul' := ⋯ }, naturality := ⋯ }
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isSyntheticTacticCompletion.isAtExpectedTacticIndentation : Lean.FileMap → String.Pos.Raw → Option String.Pos.Raw → Bool
-- Mathlib.Data.Finsupp.Single
Finsupp.card_support_eq_one : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M}, f.support.card = 1 ↔ ∃ a, f a ≠ 0 ∧ f = fun₀ | a => f a
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.isLoop_iff_mem_and_ncard_one : ∀ {α : Type u_1} {e : Set α} {H : Hypergraph α}, H.IsLoop e ↔ e ∈ H.edgeSet ∧ e.ncard = 1
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_one' : ∀ {α : Type u_1} (M : Type u_3) [inst : One M] {s : Set α}, s.mulIndicator 1 = 1
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roc.Internal.toList_eq_toList_iter : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roc α},
  r.toList = (Std.Roc.Internal.iter r).toList
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instUniqueSubtypeMemBot : {G : Type u_1} → [inst : Group G] → Unique ↥⊥
-- Mathlib.CategoryTheory.GuitartExact.Basic
/-- Given `w : TwoSquare T L R B` and a morphism `g : R.obj X₂ ⟶ B.obj X₃`, this is the
category `CostructuredArrow (w.structuredArrowDownwards X₂) (StructuredArrow.mk g)`,
see the constructor `CostructuredArrowDownwards.mk` for the data that is involved.  -/
CategoryTheory.TwoSquare.CostructuredArrowDownwards : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        CategoryTheory.TwoSquare T L R B →
                          {X₂ : C₂} → {X₃ : C₃} → (R.obj X₂ ⟶ B.obj X₃) → Type (max (max u₁ v₂) v₃)
-- Init.Core
Sum.inr.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β] (val : β), sizeOf (Sum.inr val) = 1 + sizeOf val
-- Mathlib.CategoryTheory.Adjunction.Comma
CategoryTheory.isLeftAdjoint_iff_hasTerminal_costructuredArrow : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  F.IsLeftAdjoint ↔ ∀ (A : D), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow F A)
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The coassociativity axiom associated to a coalgebra.  -/
CategoryTheory.Comonad.Coalgebra.coassoc_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra) {Z : C}
  (h : G.obj (G.obj self.A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.a (CategoryTheory.CategoryStruct.comp (G.δ.app self.A) h) =
    CategoryTheory.CategoryStruct.comp self.a (CategoryTheory.CategoryStruct.comp (G.map self.a) h)
-- Mathlib.Logic.Equiv.Set
Equiv.sigmaPreimageEquiv_symm_apply_fst : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (x : α), ((Equiv.sigmaPreimageEquiv f).symm x).fst = f x
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toArray_rco' : ∀ {m n k : ℕ}, Array.map (fun x => k + x) (m...n).toArray = ((k + m)...k + n).toArray
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.filter_mono : ∀ {α : Type u} {β : Type v} {l l' : Filter α} {f g : α → β}, f =ᶠ[l] g → l' ≤ l → f =ᶠ[l'] g
-- Mathlib.Analysis.Complex.Exponential
Real.exp_neg : ∀ (x : ℝ), Real.exp (-x) = (Real.exp x)⁻¹
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_mul_ofReal : ∀ {K : Type u_1} [inst : RCLike K] (z : K) (r : ℝ), RCLike.re (z * ↑r) = RCLike.re z * r
-- Mathlib.CategoryTheory.Localization.Predicate
/-- Via the equivalence of categories `equivalenceFromModel L W : W.Localization ≌ D`,
one may identify the functors `W.Q` and `L`.  -/
CategoryTheory.Localization.qCompEquivalenceFromModelFunctorIso : {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) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : L.IsLocalization W] → W.Q.comp (CategoryTheory.Localization.equivalenceFromModel L W).functor ≅ L
-- Mathlib.RingTheory.Idempotents
instCommRingCorner : {R : Type u_1} → (e : R) → [inst : NonUnitalCommRing R] → (idem : IsIdempotentElem e) → CommRing idem.Corner
-- Lean.Parser.Term
Lean.Parser.Term.fun.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Do not use this. Use `_root_.mul_le_mul_of_nonneg_left` instead.  -/
PosMulMono.mul_le_mul_of_nonneg_left : ∀ {α : Type u_1} {inst : Mul α} {inst_1 : Zero α} {inst_2 : Preorder α} [self : PosMulMono α] ⦃a : α⦄,
  0 ≤ a → ∀ ⦃b c : α⦄, b ≤ c → a * b ≤ a * c
-- Lean.Parser.Basic
Lean.Parser.strLitNoAntiquot : Lean.Parser.Parser
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.encode : ∀ {n : ℕ}, Nat.Primrec' Encodable.encode
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.brecOn_3.eq : ∀ {α : Type u} {β : Type v} {motive_1 : Lean.PersistentHashMap.Node α β → Sort u_1}
  {motive_2 : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1}
  {motive_3 : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1}
  {motive_4 : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_1}
  (t : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))
  (F_1 : (t : Lean.PersistentHashMap.Node α β) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      Lean.PersistentHashMap.Node.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      Lean.PersistentHashMap.Node.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
      Lean.PersistentHashMap.Node.below_3 t → motive_4 t),
  Lean.PersistentHashMap.Node.brecOn_3 t F_1 F_2 F_3 F_4 =
    F_4 t (Lean.PersistentHashMap.Node.brecOn_3.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Analysis.Convex.Between
wbtw_or_wbtw_smul_vadd_of_nonneg : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x : P) (v : V) {r₁ r₂ : R},
  0 ≤ r₁ → 0 ≤ r₂ → Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
-- Std.Data.DHashMap.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.DHashMap.Const.modify : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} → {β : Type v} → (Std.DHashMap α fun x => β) → α → (β → β) → Std.DHashMap α fun x => β
-- Mathlib.MeasureTheory.Integral.TorusIntegral
torusIntegral.eq_1 : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : (Fin n → ℂ) → E) (c : Fin n → ℂ)
  (R : Fin n → ℝ),
  torusIntegral f c R =
    ∫ (θ : Fin n → ℝ) in Set.Icc 0 fun x => 2 * Real.pi,
      (∏ i, ↑(R i) * Complex.exp (↑(θ i) * Complex.I) * Complex.I) • f (torusMap c R θ)
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.space_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E], ⊥.space = ∅
-- Mathlib.Algebra.Order.Sub.WithTop
WithTop.coe_sub : ∀ {α : Type u_1} [inst : Sub α] [inst_1 : Bot α] {a b : α}, ↑(a - b) = ↑a - ↑b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_erase : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k a : α},
  Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl a =
    if compare k a = Ordering.eq then none else Std.DTreeMap.Internal.Impl.Const.get? t a
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
DenseRange.exists_dist_lt : ∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_3} {f : β → α},
  DenseRange f → ∀ (x : α) {ε : ℝ}, 0 < ε → ∃ y, dist x (f y) < ε
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.eq_C_of_isEmpty : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [IsEmpty σ] (p : MvPolynomial σ R),
  p = MvPolynomial.C (MvPolynomial.coeff 0 p)
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
/-- **Alias** of `MeasureTheory.Measure.absolutelyContinuous_of_eq`. -/
Eq.absolutelyContinuous : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ = ν → μ.AbsolutelyContinuous ν
-- Mathlib.Data.Nat.Digits.Lemmas
/-- If `L` is a list in `List.fixedLengthDigits b l` and `d` is an integer `< b`, then
`d :: L` is a list in `List.fixedLengthDigits b (l + 1).`
 -/
List.cons_mem_fixedLengthDigits_succ : ∀ {b : ℕ} (hb : 1 < b) (l d : ℕ),
  d < b → ∀ {L : List ℕ}, L ∈ List.fixedLengthDigits hb l → d :: L ∈ List.fixedLengthDigits hb (l + 1)
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_finset_symmDiff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  {s t : Finset β} {a : α}, a ≠ 0 → a • symmDiff s t = symmDiff (a • s) (a • t)
-- Lean.Compiler.LCNF.Basic
/-- A projection from a pure LCNF value.
 -/
Lean.Compiler.LCNF.LetValue.proj : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Name →
    ℕ →
      Lean.FVarId →
        autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.LetValue._auto_1 →
          Lean.Compiler.LCNF.LetValue pu
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.generate_pushforward : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (R : CategoryTheory.Presieve X),
  CategoryTheory.Sieve.generate (CategoryTheory.Presieve.pushforward f R) =
    CategoryTheory.Sieve.pushforward f (CategoryTheory.Sieve.generate R)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_mul_const' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal),
  r ≠ ⊤ → ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPPrepend.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (t acc : List α) (h_1 : (acc : List α) → motive [] acc)
  (h_2 : (a : α) → (t acc : List α) → motive (a :: t) acc),
  (match a :: t, acc with
    | [], acc => h_1 acc
    | a :: t, acc => h_2 a t acc) =
    h_2 a t acc