mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized'_inf : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] (M' M'' : Submodule R M),
  Submodule.localized' S p f (M' ⊓ M'') = Submodule.localized' S p f M' ⊓ Submodule.localized' S p f M''
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.elim_update_aux : ∀ {a b c d c' : List Turing.PartrecToTM2.Γ'},
  Function.update (Turing.PartrecToTM2.K'.elim a b c d) Turing.PartrecToTM2.K'.aux c' =
    Turing.PartrecToTM2.K'.elim a b c' d
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
PolynormableSpace.withSeminorms : ∀ (𝕜 : Type u_2) (E : Type u_6) [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [PolynormableSpace 𝕜 E], WithSeminorms fun p => ↑p
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.exp_llr : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
  (fun x => Real.exp (MeasureTheory.llr μ ν x)) =ᵐ[ν] fun x => if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_sum_of_identDistrib₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {s : Finset ι}
  {j : ι},
  (∀ (i : ι), AEMeasurable (X i) μ) →
    ProbabilityTheory.iIndepFun X μ →
      (∀ i ∈ s, ∀ j ∈ s, ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) →
        j ∈ s → ∀ (t : ℝ), ProbabilityTheory.mgf (∑ i ∈ s, X i) μ t = ProbabilityTheory.mgf (X j) μ t ^ s.card
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `hasFDerivAt_sub_const_iff`. -/
HasFDerivAt.sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (c : F), HasFDerivAt f f' x → HasFDerivAt (fun x => f x - c) f' x
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Overlaps.mk.sizeOf_spec : ∀ (map : Std.HashMap ℕ (Std.TreeSet ℕ compare)), sizeOf { map := map } = 1 + sizeOf map
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.inlCokernelCofork_π : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y), CategoryTheory.Limits.Cofork.π c.inlCokernelCofork = c.snd
-- Mathlib.Tactic.NormNum.Abs
Mathlib.Meta.NormNum.isNat_abs_nonneg : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : Lattice α] [IsOrderedRing α] {a : α} {na : ℕ},
  Mathlib.Meta.NormNum.IsNat a na → Mathlib.Meta.NormNum.IsNat |a| na
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.IsSheaf.amalgamate_map_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A}
  (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (x : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y))
  (hx :
    ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂),
      CategoryTheory.CategoryStruct.comp (x I₁) (P.map r.g₁.op) =
        CategoryTheory.CategoryStruct.comp (x I₂) (P.map r.g₂.op))
  (I : S.Arrow) {Z : A} (h : P.obj (Opposite.op I.Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hP.amalgamate S x hx) (CategoryTheory.CategoryStruct.comp (P.map I.f.op) h) =
    CategoryTheory.CategoryStruct.comp (x I) h
-- Mathlib.Algebra.GroupWithZero.Pi
Pi.single_mul_left_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MulZeroClass (α i)] [inst_1 : DecidableEq ι] (i j : ι) (a : α i)
  (f : (i : ι) → α i), Pi.single i (a * f i) j = Pi.single i a j * f j
-- Aesop.Rule.Name
Aesop.BuilderName.forward : Aesop.BuilderName
-- Mathlib.Tactic.ClickSuggestions.Util
/-- A free variable.  -/
Mathlib.Tactic.ClickSuggestions.Premise.fvar : Lean.FVarId → Mathlib.Tactic.ClickSuggestions.Premise
-- Mathlib.Condensed.Light.Limits
instHasCountableLimitsLightCondMod : ∀ (R : Type u) [inst : Ring R], CategoryTheory.Limits.HasCountableLimits (LightCondMod R)
-- Lean.Parser.Do
/-- `continue` skips to the next iteration of the surrounding `for` loop.  -/
Lean.Parser.Term.doContinue : Lean.Parser.Parser
-- Mathlib.Data.Int.Cast.Defs
AddCommGroupWithOne.toNatCast : {R : Type u} → [self : AddCommGroupWithOne R] → NatCast R
-- Lean.Elab.Term.TermElabM
/-- Return normalized expected type if it is of the form `{a : α} → β` or `[a : α] → β` and
`blockImplicitLambda stx` is not true, else return `none`.

Remark: implicit lambdas are not triggered by the strict implicit binder annotation `{{a : α}} → β`
 -/
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.useImplicitLambda : Lean.Syntax → Option Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Term.UseImplicitLambdaResult
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.centroid_reindex : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {m n : ℕ} (s : Affine.Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)),
  (s.reindex e).centroid = s.centroid
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_lt_top : ∀ {x y : ENNReal}, x ≠ ⊤ → y ≠ 0 → x / y < ⊤
-- Init.Data.List.Range
List.length_range : ∀ {n : ℕ}, (List.range n).length = n
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_union_eq_left_of_forall : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {s t : Set X} {μ : MeasureTheory.Measure X} {f : X → E},
  MeasurableSet t → (∀ x ∈ t, f x = 0) → ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.embDomain_of_notMem_range : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) {b : β}, b ∉ Set.range ⇑f → (s.embDomain f) b = 0
-- Mathlib.Algebra.Prime.Lemmas
prime_mul_isUnit : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {x y : M}, IsUnit x → (Prime (y * x) ↔ Prime y)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiffWithinAt.sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E}
  {n : WithTop ℕ∞}, ContDiffWithinAt ℝ n f s x → ContDiffWithinAt ℝ n (fun x => Real.sinh (f x)) s x
-- Init.Data.Array.Attach
Array.all_subtype : ∀ {α : Type u_1} {stop : ℕ} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → stop = xs.size → xs.all f 0 stop = xs.unattach.all g
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_comm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α), gcd a b = gcd b a
-- Lean.Meta.LitValues
/-- Recognize a non-negated `Float32` literal: an `OfScientific` or `OfNat` application.  -/
_private.Lean.Meta.LitValues.0.Lean.Meta.getFloat32Lit? : Lean.Expr → Lean.MetaM (Option Float32)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshotInner.mk.injEq : ∀ {α : Type} (toSnapshot : Lean.Language.Snapshot) (stx : Lean.Syntax) (inner? : Option (Lean.Language.SnapshotTask α))
  (finished : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticFinishedSnapshot)
  (toSnapshot_1 : Lean.Language.Snapshot) (stx_1 : Lean.Syntax) (inner?_1 : Option (Lean.Language.SnapshotTask α))
  (finished_1 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticFinishedSnapshot),
  ({ toSnapshot := toSnapshot, stx := stx, inner? := inner?, finished := finished } =
      { toSnapshot := toSnapshot_1, stx := stx_1, inner? := inner?_1, finished := finished_1 }) =
    (toSnapshot = toSnapshot_1 ∧ stx = stx_1 ∧ inner? = inner?_1 ∧ finished = finished_1)
-- Mathlib.Data.Finset.Fold
Finset.fold_const : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {b : β}
  {s : Finset α} [hd : Decidable (s = ∅)] (c : β),
  op c (op b c) = op b c → Finset.fold op b (fun x => c) s = if s = ∅ then b else op b c
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hom_ext_iff : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} {f g : M ⟶ N},
  f = g ↔ SemimoduleCat.Hom.hom f = SemimoduleCat.Hom.hom g
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- One can bound `‖w‖^n * ‖D^k (𝓕 f) w‖` in terms of integrals of the derivatives of `f` (or order
at most `n`) multiplied by powers of `v` (of order at most `k`).  -/
Real.pow_mul_norm_iteratedFDeriv_fourier_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {f : V → E} {K N : ℕ∞},
  ContDiff ℝ (↑N) f →
    (∀ (k n : ℕ),
        ↑k ≤ K → ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) MeasureTheory.volume) →
      ∀ {k n : ℕ},
        ↑k ≤ K →
          ↑n ≤ N →
            ∀ (w : V),
              ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (FourierTransform.fourier f) w‖ ≤
                (2 * Real.pi) ^ k * (2 * ↑k + 2) ^ n *
                  ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H0π_comp_H0Iso_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (Rep.coinvariantsFunctor k G).obj A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.H0π A)
      (CategoryTheory.CategoryStruct.comp (groupHomology.H0Iso A).hom h) =
    CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) h
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
SzemerediRegularity.increment.congr_simp : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P P_1 : Finpartition Finset.univ} (e_P : P = P_1)
  (hP : P.IsEquipartition) (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ {inst_2 : DecidableRel G.Adj} [inst_3 : DecidableRel G_1.Adj] (ε ε_1 : ℝ),
      ε = ε_1 → SzemerediRegularity.increment hP G ε = SzemerediRegularity.increment ⋯ G_1 ε_1
-- Mathlib.Data.Finsupp.Indicator
Finsupp.support_indicator_subset : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α),
  (Finsupp.indicator s f).support ⊆ s
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.data_drop : ∀ {s : Substring.Raw}, s.Valid → ∀ (n : ℕ), (s.drop n).toString.toList = List.drop n s.toString.toList
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_roo_eq_none : ∀ {m n : ℤ} {i : ℕ}, (n - (m + 1)).toNat ≤ i → (m<...n).toArray[i]? = none
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.mk_le_mk : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α]
  [inst_3 : Lean.Grind.OrderedAdd α] {a₁ a₂ b₁ b₂ : α},
  Lean.Grind.IntModule.OfNatModule.Q.mk (a₁, a₂) ≤ Lean.Grind.IntModule.OfNatModule.Q.mk (b₁, b₂) ↔ a₁ + b₂ ≤ a₂ + b₁
-- Mathlib.Algebra.Category.ModuleCat.Semi
_private.Mathlib.Algebra.Category.ModuleCat.Semi.0.SemimoduleCat.mk : {R : Type u} →
  [inst : Semiring R] →
    (carrier : Type v) → [isAddCommMonoid : AddCommMonoid carrier] → [isModule : Module R carrier] → SemimoduleCat R
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- In the model space, the identity is in any maximal atlas.  -/
StructureGroupoid.id_mem_maximalAtlas : ∀ {H : Type u} [inst : TopologicalSpace H] (G : StructureGroupoid H),
  OpenPartialHomeomorph.refl H ∈ StructureGroupoid.maximalAtlas H G
-- Init.Data.Array.MapIdx
Array.mapIdx_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {f : ℕ → α → β} {g : ℕ → β → γ},
  Array.mapIdx g (Array.mapIdx f xs) = Array.mapIdx (fun i => g i ∘ f i) xs
-- Mathlib.Analysis.Convex.Quasiconvex
QuasiconcaveOn.dual : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LE β] [inst_4 : SMul 𝕜 E] {s : Set E} {f : E → β},
  QuasiconcaveOn 𝕜 s f → QuasiconvexOn 𝕜 s (⇑OrderDual.toDual ∘ f)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.alter_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  Std.ExtDTreeMap.Const.alter t k f = ∅ ↔ (t = ∅ ∨ t.size = 1 ∧ k ∈ t) ∧ f (Std.ExtDTreeMap.Const.get? t k) = none
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] [CategoryTheory.Limits.HasFiniteLimits D],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.sheafToPresheaf J D)
-- Mathlib.GroupTheory.QuotientGroup.Defs
AddCon.addSubgroup_quotientAddGroupCon : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : H.Normal], (QuotientAddGroup.con H).addSubgroup = H
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.uniformContinuous_restrictScalars : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : UniformSpace F]
  [inst_7 : IsUniformAddGroup F] (𝕜' : Type u_5) [inst_8 : NontriviallyNormedField 𝕜'] [inst_9 : NormedAlgebra 𝕜' 𝕜]
  [inst_10 : (i : ι) → Module 𝕜' (E i)] [inst_11 : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [inst_12 : Module 𝕜' F]
  [inst_13 : IsScalarTower 𝕜' 𝕜 F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)],
  UniformContinuous (ContinuousMultilinearMap.restrictScalars 𝕜')
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.prepartition_isHenstock : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] (B : BoxIntegral.Box ι),
  (BoxIntegral.unitPartition.prepartition n B).IsHenstock
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_congr : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s₁ s₂ : Finset β}
  {f g : β → α}, s₁ = s₂ → (∀ a ∈ s₂, f a = g a) → s₁.gcd f = s₂.gcd g
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.constGet_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (hk : k ∈ m₁) (h : m₁.Equiv m₂),
  Std.DHashMap.Const.get m₁ k hk = Std.DHashMap.Const.get m₂ k ⋯
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Valuation.mem_nhds_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_3 : TopologicalSpace R] (v : Valuation R Γ₀) [v.Compatible] [IsValuativeTopology R] {s : Set R} {x : R},
  s ∈ nhds x ↔ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α}
  {b : β}, (t.insert a b).getKeyD a fallback = a
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.toOrderHom_comp : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : AddCommMonoid E₃]
  [inst_6 : PartialOrder E₃] [inst_7 : Module R E₁] [inst_8 : Module R E₂] [inst_9 : Module R E₃] (g : E₂ →ₚ[R] E₃)
  (f : E₁ →ₚ[R] E₂), (g.comp f).toOrderHom = g.toOrderHom.comp f.toOrderHom
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit'.eq_def : ∀ (e : Lean.Expr) (omitTopForall : Bool),
  Lean.Elab.Command.NameGen.mkBaseNameCore.visit'✝ e omitTopForall =
    match e with
    | Lean.Expr.const name us => do
      modify fun st =>
          { seen := Lean.Elab.Command.NameGen.MkNameState.seen✝ st,
            consts := (Lean.Elab.Command.NameGen.MkNameState.consts✝ st).insert name }
      pure
          (match name.eraseMacroScopes with
          | pre.str str => str.capitalize
          | x => "")
    | f.app x =>
      (fun x1 x2 => x1 ++ x2) <$> Lean.Elab.Command.NameGen.mkBaseNameCore.visit✝ f <*>
        Lean.Elab.Command.NameGen.mkBaseNameCore.visit✝ x
    | Lean.Expr.forallE binderName ty body binderInfo => do
      let sty ← Lean.Elab.Command.NameGen.mkBaseNameCore.visit✝ ty
      if (omitTopForall && sty == "") = true then Lean.Elab.Command.NameGen.mkBaseNameCore.visit✝ body true
        else (fun x => "Forall" ++ sty ++ x) <$> Lean.Elab.Command.NameGen.mkBaseNameCore.visit✝ body
    | Lean.Expr.sort Lean.Level.zero => pure "Prop"
    | Lean.Expr.sort a.succ => pure "Type"
    | Lean.Expr.sort u => pure "Sort"
    | x => pure ""
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₁_fst_assoc : ∀ (X : TopCat) {Z : TopCat} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp TopCat.ι₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X TopCat.I) h) =
    h
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Right-exactness, as a property of objects in `C ⥤ D`.  -/
CategoryTheory.rightExactFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.ObjectProperty (CategoryTheory.Functor C D)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.coe_one : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X], ⇑1 = id
-- Mathlib.Order.Types.Arithmetic
OrderType.instOfNat : (n : ℕ) → OfNat OrderType.{0} n
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∈ t₂ → (t₁ \ t₂).getD k fallback = fallback
-- Init.Data.List.MapIdx
List.length_mapFinIdx : ∀ {α : Type u_1} {β : Type u_2} {as : List α} {f : (i : ℕ) → α → i < as.length → β}, (as.mapFinIdx f).length = as.length
-- Mathlib.Order.RelSeries
RelSeries.head_fromListIsChain : ∀ {α : Type u_1} {r : SetRel α α} (l : List α) (l_ne_nil : l ≠ []) (hl : List.IsChain (fun x1 x2 => (x1, x2) ∈ r) l),
  (RelSeries.fromListIsChain l l_ne_nil hl).head = l.head l_ne_nil
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsLoopAt.mono : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β}, H ≤ G → H.IsLoopAt e x → G.IsLoopAt e x
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.take.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → Stream'.Seq α → Sort u_2) →
    (x : ℕ) →
      (x_1 : Stream'.Seq α) →
        ((x : Stream'.Seq α) → motive 0 x) → ((n : ℕ) → (s : Stream'.Seq α) → motive n.succ s) → motive x x_1
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots : ∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
  {ζ : B} {n : ℕ} [NeZero n],
  IsPrimitiveRoot ζ n →
    Algebra.adjoin A ((Polynomial.cyclotomic n A).rootSet B) = Algebra.adjoin A {b | ∃ a ∈ {n}, a ≠ 0 ∧ b ^ a = 1}
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.leftOpWhiskerRight_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C Dᵒᵖ} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor E C} (α : F ⟶ G) {Z : CategoryTheory.Functor Eᵒᵖ D} (h : (H.comp F).leftOp ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftOp (H.whiskerLeft α)) h =
    CategoryTheory.CategoryStruct.comp (H.leftOpComp G).hom
      (CategoryTheory.CategoryStruct.comp (H.op.whiskerLeft (CategoryTheory.NatTrans.leftOp α))
        (CategoryTheory.CategoryStruct.comp (H.leftOpComp F).inv h))
-- Mathlib.NumberTheory.NumberField.CMField
/-- An element of `K` is fixed by the complex conjugation iff it lies in `K⁺`.
 -/
NumberField.IsCMField.complexConj_eq_self_iff : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (x : K),
  (NumberField.IsCMField.complexConj K) x = x ↔ x ∈ NumberField.maximalRealSubfield K
-- Mathlib.Topology.Algebra.Ring.Basic
/-- A semitopological semiring is a semiring `R` where addition is jointly continuous and
multiplication is continuous in each variable separately.
We allow for non-unital and non-associative semirings as well.

The `IsSemitopologicalSemiring` class should *only* be instantiated in the presence of a
`NonUnitalNonAssocSemiring` instance; if there is an instance of `NonUnitalNonAssocRing`,
then `IsSemitopologicalRing` should be used. Note: in the presence of `NonAssocRing`, these classes
are mathematically equivalent (see `IsTopologicalSemiring.continuousNeg_of_mul` or
`IsSemitopologicalSemiring.toIsTopologicalRing`).  -/
IsSemitopologicalSemiring : (R : Type u_2) → [TopologicalSpace R] → [NonUnitalNonAssocSemiring R] → Prop
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L]
  [LieModule.IsTriangularizable K (↥H) L] [inst_7 : CharZero K] (α : LieModule.Weight K (↥H) L),
  Disjoint LieModule.Weight.ker (LieIdeal.toLieSubalgebra K (↥H) (LieAlgebra.corootSpace ⇑α)).toSubmodule
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Express `edist` in terms of `nndist`  -/
edist_nndist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), edist x y = ↑(nndist x y)
-- Init.Data.List.Control
List.forM_nil : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] {f : α → m PUnit.{u_1 + 1}}, forM [] f = pure PUnit.unit
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.mk.sizeOf_spec : ∀ (wp x y zp ap bp : ℕ),
  sizeOf { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } =
    1 + sizeOf wp + sizeOf x + sizeOf y + sizeOf zp + sizeOf ap + sizeOf bp
-- Mathlib.Order.SymmDiff
bihimp_comm : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), bihimp a b = bihimp b a
-- Mathlib.NumberTheory.Real.Irrational
/-- This can be used as
```lean
unseal Nat.sqrt.iter in
example : Irrational √24 := by decide
```
 -/
instDecidableIrrationalSqrtOfNatReal : {n : ℕ} → [inst : n.AtLeastTwo] → Decidable (Irrational √(OfNat.ofNat n))
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_le_mul_of_nonpos_of_nonneg' : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b c d : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
  [AddRightMono R] [AddRightReflectLE R], c ≤ a → b ≤ d → 0 ≤ a → d ≤ 0 → a * b ≤ c * d
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.ShortComplex.Exact.isIso_imageToKernel : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C), S.Exact → CategoryTheory.IsIso (imageToKernel S.f S.g ⋯)
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.ExtensionState.declNames : {γ : Type} → Lean.KeyedDeclsAttribute.ExtensionState γ → Lean.PHashSet Lean.Name
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.closure_insert_one : ∀ {M : Type u_1} [inst : MulOneClass M] (s : Set M), Submonoid.closure (insert 1 s) = Submonoid.closure s
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.isFinite : Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval → Bool