mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.FreeModule.PID
Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {n : ℕ} {N : Submodule R M} (snf : Module.Basis.SmithNormalForm N ι n) (m : ↥N) {i : ι},
  i ∉ Set.range ⇑snf.f → (snf.bM.repr ↑m) i = 0
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.StrongCore.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η : F ⟶ G}
  (naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (η.app a) (G.map f) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (η.app b))
  (naturality_hom :
    autoParam (∀ {a b : B} (f : a ⟶ b), (naturality f).hom = η.naturality f)
      CategoryTheory.Lax.LaxTrans.StrongCore.naturality_hom._autoParam)
  (naturality_1 :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (η.app a) (G.map f) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (η.app b))
  (naturality_hom_1 :
    autoParam (∀ {a b : B} (f : a ⟶ b), (naturality_1 f).hom = η.naturality f)
      CategoryTheory.Lax.LaxTrans.StrongCore.naturality_hom._autoParam),
  ({ naturality := naturality, naturality_hom := naturality_hom } =
      { naturality := naturality_1, naturality_hom := naturality_hom_1 }) =
    (naturality = naturality_1)
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.nat : ℕ → Mathlib.Deriving.Encodable.S✝
-- Mathlib.Data.Finsupp.Defs
/-- The underlying function of a bundled finitely supported function (aka `Finsupp`).  -/
Finsupp.toFun : {α : Type u_9} → {M : Type u_10} → [inst : Zero M] → (α →₀ M) → α → M
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- A closed ball centred at the origin in a valued ring is clopen.  -/
Valued.isClopen_closedBall : ∀ (R : Type u) [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀]
  {r : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀}, r ≠ 0 → IsClopen {x | Valued.v.restrict x ≤ r}
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insert.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (l l_1 : Std.ExtTreeMap α β cmp),
  l = l_1 → ∀ (a a_1 : α), a = a_1 → ∀ (b b_1 : β), b = b_1 → l.insert a b = l_1.insert a_1 b_1
-- Mathlib.Order.DirectedInverseSystem
/-- Extend a family of bijections to `piLT` by one step.  -/
InverseSystem.piEquivSucc : {ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      {i : ι} →
        [inst : LinearOrder ι] →
          [inst_1 : SuccOrder ι] →
            ((j : ↑(Set.Iic i)) → F ↑j ≃ InverseSystem.piLT X ↑j) →
              F (Order.succ i) ≃ F i × X i → ¬IsMax i → (j : ↑(Set.Iic (Order.succ i))) → F ↑j ≃ InverseSystem.piLT X ↑j
-- Mathlib.Order.KrullDimension
/-- In a maximally long series, i.e one as long as the coheight of the first element, the coheight of
each element is its reverse index in the series.
 -/
Order.coheight_eq_index_of_length_eq_head_coheight : ∀ {α : Type u_1} [inst : Preorder α] {p : LTSeries α},
  ↑p.length = Order.coheight (RelSeries.head p) → ∀ (i : Fin (p.length + 1)), Order.coheight (p.toFun i) = ↑↑i.rev
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with the provided status.
 -/
Std.Http.Response.withStatus : Std.Http.Status → Std.Http.Response.Builder
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
AlternatingMap.domCoprod_apply : ∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
  {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
  [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂)
  (v : ιa ⊕ ιb → Mᵢ), (a.domCoprod b) v = (∑ σ, AlternatingMap.domCoprod.summand a b σ) v
-- Mathlib.Analysis.Analytic.Constructions
/-- **Alias** of `AnalyticAt.curry_right`.

---

Analytic functions on products are analytic in the second coordinate  -/
AnalyticAt.along_snd : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {p : E × F},
  AnalyticAt 𝕜 f p → AnalyticAt 𝕜 (fun y => f (p.1, y)) p.2
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.lt_iff : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {f : α → β},
  LeftOrdContinuous f → Function.Injective f → ∀ {x y : α}, f x < f y ↔ x < y
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.isDiameter_iff_left_mem_and_midpoint_eq_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ midpoint ℝ p₁ p₂ = s.center
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.leftAdjointUniq_inv_app : ∀ {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] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C), (adj1.leftAdjointUniq adj2).inv.app x = (adj2.leftAdjointUniq adj1).hom.app x
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instAlgebraSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                Algebra R ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)
-- Mathlib.Analysis.Seminorm
/-- Alternative constructor for a `Seminorm` over a normed field `𝕜` that only assumes `f 0 = 0`
and an inequality for the scalar multiplication.  -/
Seminorm.ofSMulLE : {𝕜 : Type u_3} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          (f : E → ℝ) →
            f 0 = 0 → (∀ (x y : E), f (x + y) ≤ f x + f y) → (∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x) → Seminorm 𝕜 E
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_range_add_div_prod_range : ∀ {G : Type u_3} [inst : CommGroup G] (f : ℕ → G) (n m : ℕ),
  (∏ k ∈ Finset.range (n + m), f k) / ∏ k ∈ Finset.range n, f k = ∏ k ∈ Finset.range m, f (n + k)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
fderivWithin_cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x →
    UniqueDiffWithinAt ℝ s x → fderivWithin ℝ (fun x => Real.cos (f x)) s x = -Real.sin (f x) • fderivWithin ℝ f s x
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- `CompHausLike.LocallyConstant.functor` is naturally isomorphic to the restriction of
`topCatToSheafCompHausLike` to discrete topological spaces.
 -/
CompHausLike.LocallyConstant.functorIso : (P : TopCat → Prop) →
  [inst : CompHausLike.HasExplicitFiniteCoproducts P] →
    [inst_1 : CompHausLike.HasExplicitPullbacks P] →
      (hs :
          ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
            CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
        CompHausLike.LocallyConstant.functor P hs ≅ TopCat.discrete.comp (topCatToSheafCompHausLike P hs)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivAt.lineDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f' : F}
  {x v : E}, HasLineDerivAt 𝕜 f f' x v → lineDeriv 𝕜 f x v = f'
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.inclusion.congr_simp : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I₁ I₂ : LieIdeal R L}
  (h : I₁ ≤ I₂), LieIdeal.inclusion h = LieIdeal.inclusion h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  {f : (a : α) → β a → Option (γ a)} {k : α},
  t.WF →
    Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap! f t) = true →
      Std.DTreeMap.Internal.Impl.contains k t = true
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.mem_eventualRange_iff : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {j : J}
  {x : F.obj j},
  x ∈ F.eventualRange j ↔ ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))
-- Lean.Elab.Term.TermElabM
/-- List of errors associated to a metavariable that are shown to the user if the metavariable could not be fully instantiated  -/
Lean.Elab.Term.State.mvarErrorInfos : Lean.Elab.Term.State → List Lean.Elab.Term.MVarErrorInfo
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_surjective_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Surjective ⇑f → Function.Surjective (Subsemigroup.map f)
-- Mathlib.Data.Sym.Sym2
Set.sym2_inter : ∀ {α : Type u_1} (s t : Set α), (s ∩ t).sym2 = s.sym2 ∩ t.sym2
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `t` is in the upper shadow of `𝒜` iff `t` is exactly `k` elements less than something from `𝒜`.

See also `Finset.mem_upShadow_iff_exists_mem_card_add`.  -/
Finset.mem_upShadow_iterate_iff_exists_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ},
  t ∈ Finset.upShadow^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s).card = k
-- Mathlib.Order.Radical
Order.radical_nongenerating : ∀ {α : Type u_1} [inst : CompleteLattice α] [IsCoatomic α] {a : α}, a ⊔ Order.radical α = ⊤ → a = ⊤
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.TextDocumentClientCapabilities : Type
-- Init.Prelude
/-- Retrieves the local value.

Use `readThe` to explicitly specify a type when more than one value is available.
 -/
MonadReader.read : {ρ : outParam (Type u)} → {m : Type u → Type v} → [self : MonadReader ρ m] → m ρ
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_assoc : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l},
  Lean.Order.meet (Lean.Order.meet P Q) R = Lean.Order.meet P (Lean.Order.meet Q R)
-- Init.Data.Order.Ord
Std.instLawfulBEqCmpOfLawfulEqCmpOfLawfulBEq : ∀ {α : Type u} [inst : BEq α] {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [LawfulBEq α], Std.LawfulBEqCmp cmp
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instLattice : {G : Type u_1} → [inst : AddGroup G] → Lattice (FiniteIndexNormalAddSubgroup G)
-- Lean.Server.Completion.CompletionCollectors
Lean.Server.Completion.endSectionCompletion : Lean.Lsp.DocumentUri →
  Lean.Lsp.Position → ℕ → Option Lean.Name → Bool → List String → IO (Array Lean.Lsp.ResolvableCompletionItem)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.instBEqMatcherKey.beq : Lean.Meta.Match.MatcherKey✝ → Lean.Meta.Match.MatcherKey✝ → Bool
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj ⊤ = AlgebraicGeometry.Scheme.Hom.opensRange f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k : α}, k ∉ m₁ → (m₁ \ m₂).getKey! k = default
-- Mathlib.RingTheory.Ideal.Over
Ideal.smul_under : ∀ (A : Type u_2) [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B)
  {G : Type u_5} [inst_3 : Group G] [inst_4 : MulSemiringAction G B] (g : G) [inst_5 : MulSemiringAction G A]
  [SMulDistribClass G A B], g • Ideal.under A P = Ideal.under A (g • P)
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
CompleteLattice.MulticoequalizerDiagram.multispanIndex.congr_simp : ∀ {T : Type u} [inst : CompleteLattice T] {ι : Type u_1} {x x_1 : T} (e_x : x = x_1) {u u_1 : ι → T} (e_u : u = u_1)
  {v v_1 : ι → ι → T} (e_v : v = v_1) (d : CompleteLattice.MulticoequalizerDiagram x u v),
  d.multispanIndex = ⋯.multispanIndex
-- Mathlib.Topology.Order
instDiscreteTopologyPUnit : DiscreteTopology PUnit.{u_1 + 1}
-- Mathlib.MeasureTheory.Covering.Besicovitch
HasBesicovitchCovering.no_satelliteConfig : ∀ {α : Type u_1} {inst : MetricSpace α} [self : HasBesicovitchCovering α],
  ∃ N τ, 1 < τ ∧ IsEmpty (Besicovitch.SatelliteConfig α N τ)
-- Mathlib.Analysis.Normed.Module.Connected
Metric.contractibleSpace_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ},
  0 < r → ContractibleSpace ↑(Metric.ball x r)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_mul_left_singleton : ∀ {α : Type u_2} [inst : Group α] {a b : α}, {b}.preimage (fun x => a * x) ⋯ = {a⁻¹ * b}
-- Init.Data.Float.Float
instHomogeneousPowFloat : HomogeneousPow Float
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_mul : ∀ {x y : ℝ}, x ≠ 0 → y ≠ 0 → Real.log (x * y) = Real.log x + Real.log y
-- Init.Data.Ord.Basic
Ordering.isLE_of_eq_lt : ∀ {o : Ordering}, o = Ordering.lt → o.isLE = true
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_sSup_of_directedOn : ∀ {R : Type u} [inst : NonAssocRing R] {S : Set (Subring R)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ∀ {x : R}, x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.instIsWellOrderContinuousFunctor : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι) [SuccOrder ι]
  [OrderBot ι], ⋯.functor.IsWellOrderContinuous
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The induced map `∏ᶜ I.left ⟶ ∏ᶜ I.right` via `I.snd`.  -/
CategoryTheory.Limits.MulticospanIndex.sndPiMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasProduct I.left] →
          [inst_2 : CategoryTheory.Limits.HasProduct I.right] → ∏ᶜ I.left ⟶ ∏ᶜ I.right
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
quadraticCharFun_one : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F], quadraticCharFun F 1 = 1
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.homologyData'_right_ι : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hk : c.next j = k) (h : (K.sc' i j k).HomologyData),
  (HomologicalComplex.extend.homologyData' K e hj' hi hk h).right.ι = h.right.ι
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.leftRelDecidable : {α : Type u_1} →
  [inst : AddGroup α] →
    (s : AddSubgroup α) → [DecidablePred fun x => x ∈ s] → DecidableRel ⇑(QuotientAddGroup.leftRel s)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {I₁ I₂ : S.Arrow} [inst_1 : SizeOf C] (Z : C) (g₁ : Z ⟶ I₁.Y) (g₂ : Z ⟶ I₂.Y)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp g₁ I₁.f = CategoryTheory.CategoryStruct.comp g₂ I₂.f)
      CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w._autoParam),
  sizeOf { Z := Z, g₁ := g₁, g₂ := g₂, w := w } = 1 + sizeOf Z + sizeOf g₁ + sizeOf g₂ + sizeOf w
-- Mathlib.MeasureTheory.Group.Measure
/-- A convenience wrapper for `MeasureTheory.Measure.isHaarMeasure_map`.  -/
MulEquiv.isHaarMeasure_map : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [BorelSpace G] [ContinuousMul G] {H : Type u_3} [inst_6 : Group H]
  [inst_7 : TopologicalSpace H] [inst_8 : MeasurableSpace H] [BorelSpace H] [IsTopologicalGroup H] (e : G ≃* H),
  Continuous ⇑e → Continuous ⇑e.symm → (MeasureTheory.Measure.map (⇑e) μ).IsHaarMeasure
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv'_assoc : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z)
  [inst_4 : CategoryTheory.IsIso f] {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x (CategoryTheory.inv f)) h) =
    h
-- Mathlib.Algebra.Polynomial.Monic
/-- Alternate phrasing of `Polynomial.Monic.irreducible_iff_natDegree'` where we only have to check
one divisor at a time.  -/
Polynomial.Monic.irreducible_iff_lt_natDegree_lt : ∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] {p : Polynomial R},
  p.Monic →
    p ≠ 1 → (Irreducible p ↔ ∀ (q : Polynomial R), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.inv_hom_whiskerRight_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) {Z : a ⟶ c}
  (h_1 : CategoryTheory.CategoryStruct.comp g h ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.inv h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.hom h) h_1) =
    h_1
-- Init.Data.Vector.DecidableEq
Vector.isEqv_self_beq : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [ReflBEq α] (xs : Vector α n), (xs.isEqv xs fun x1 x2 => x1 == x2) = true
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.e.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) (i : I),
  Profinite.NobelingProof.e C i = { toFun := fun f => if ↑f i = true then 1 else 0, isLocallyConstant := ⋯ }
-- Mathlib.Algebra.Homology.Embedding.Extend
_private.Mathlib.Algebra.Homology.Embedding.Extend.0.HomologicalComplex.extend.d.match_1.eq_2 : ∀ {ι : Type u_1} (motive : Option ι → Option ι → Sort u_2) (i j : ι) (h_1 : (x : Option ι) → motive none x)
  (h_2 : (i j : ι) → motive (some i) (some j)) (h_3 : (val : ι) → motive (some val) none),
  (match some i, some j with
    | none, x => h_1 x
    | some i, some j => h_2 i j
    | some val, none => h_3 val) =
    h_2 i j
-- Mathlib.Algebra.Symmetrized
SymAlg.instInhabited : {α : Type u_1} → [Inhabited α] → Inhabited αˢʸᵐ
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
UCompactlyGeneratedSpace.mk : ∀ {X : Type v} [t : TopologicalSpace X], t ≤ TopologicalSpace.compactlyGenerated X → UCompactlyGeneratedSpace X
-- Lean.Data.PPContext
/-- Saved context for pretty printing. See `Lean.ppExt`.  -/
Lean.PPContext : Type
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- The function `Real.exp` is real analytic.  -/
analyticAt_rexp : ∀ {x : ℝ}, AnalyticAt ℝ Real.exp x
-- Mathlib.Algebra.Ring.Shrink
/-- Shrink `α` to a smaller universe preserves ring structure.  -/
Shrink.ringEquiv : (α : Type u_1) → [inst : Small.{v, u_1} α] → [inst_1 : Add α] → [inst_2 : Mul α] → Shrink.{v, u_1} α ≃+* α
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The (finite!) set of machine states visited during the course of evaluation of a continuation
`k`, not including the initial state `ret k`.  -/
Turing.PartrecToTM2.contSupp : Turing.PartrecToTM2.Cont' → Finset Turing.PartrecToTM2.Λ'
-- Mathlib.Data.Sum.Interval
_private.Mathlib.Data.Sum.Interval.0.Finset.sumLift₂.match_1.eq_1 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (motive : α₁ ⊕ α₂ → β₁ ⊕ β₂ → Sort u_5) (a : α₁)
  (b : β₁) (h_1 : (a : α₁) → (b : β₁) → motive (Sum.inl a) (Sum.inl b))
  (h_2 : (val : α₁) → (val_1 : β₂) → motive (Sum.inl val) (Sum.inr val_1))
  (h_3 : (val : α₂) → (val_1 : β₁) → motive (Sum.inr val) (Sum.inl val_1))
  (h_4 : (a : α₂) → (b : β₂) → motive (Sum.inr a) (Sum.inr b)),
  (match Sum.inl a, Sum.inl b with
    | Sum.inl a, Sum.inl b => h_1 a b
    | Sum.inl val, Sum.inr val_1 => h_2 val val_1
    | Sum.inr val, Sum.inl val_1 => h_3 val val_1
    | Sum.inr a, Sum.inr b => h_4 a b) =
    h_1 a b
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.proj_lift : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] {T : Bundle.Trivialization F proj} {z : Z} {b : B},
  b ∈ T.baseSet → proj (T.lift z b) = b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula.0.WeierstrassCurve.Projective.toAffine_addX_of_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      ∀ {n d : F},
        d ≠ 0 →
          W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2) (n / d) =
            (n ^ 2 * P 2 * Q 2 + W.a₁ * n * P 2 * Q 2 * d - W.a₂ * P 2 * Q 2 * d ^ 2 - P 0 * Q 2 * d ^ 2 -
                    Q 0 * P 2 * d ^ 2) *
                  d /
                (P 2 * Q 2) ^ 2 /
              (d ^ 3 / (P 2 * Q 2))
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub_eq_toIocDiv_add' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b c : α), toIocDiv hp (a - c) b = toIocDiv hp a (b + c)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialRightAdjoint_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (Y : F.PartialRightAdjointSource),
  F.partialRightAdjoint.obj Y = F.partialRightAdjointObj Y
-- Mathlib.Data.Nat.GCD.BigOperators
Nat.coprime_list_prod_left_iff : ∀ {l : List ℕ} {k : ℕ}, l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.ext_from_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i) {A : C}
  {f g : HomologicalComplex.homotopyCofiber.X φ j ⟶ A},
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij) f =
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij) g →
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ j) f =
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ j) g →
      f = g
-- Mathlib.Tactic.Translate.Core
/-- Run `applyReplacementFun` on an expression `∀ x₁ .. xₙ, e`,
making sure not to translate type-classes on `xᵢ` if `i` is in `dontTranslate`.  -/
Mathlib.Tactic.Translate.applyReplacementForall : Mathlib.Tactic.Translate.TranslateData →
  List ℕ → Lean.Expr → Lean.MetaM (Lean.Expr × Option Mathlib.Tactic.Translate.RelevantArg)