mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SavedState.mk.inj : ∀ {term : Lean.Elab.Term.SavedState} {tactic : Lean.Elab.Tactic.Grind.State} {term_1 : Lean.Elab.Term.SavedState}
  {tactic_1 : Lean.Elab.Tactic.Grind.State},
  { term := term, tactic := tactic } = { term := term_1, tactic := tactic_1 } → term = term_1 ∧ tactic = tactic_1
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_toLinearEquiv : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (f : M₁ ≃SL[σ₁₂] M₂), ⇑↑f = ⇑f
-- Lean.ErrorExplanation
/-- An environment extension that stores error explanations.   -/
Lean.errorExplanationExt : Lean.SimplePersistentEnvExtension (Lean.Name × Lean.ErrorExplanation) (Lean.NameMap Lean.ErrorExplanation)
-- Mathlib.Topology.UniformSpace.Equicontinuity
Filter.HasBasis.uniformEquicontinuousOn_iff_right : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {p : κ → Prop}
  {s : κ → Set (α × α)} {F : ι → β → α} {S : Set β},
  (uniformity α).HasBasis p s →
    (UniformEquicontinuousOn F S ↔
      ∀ (k : κ),
        p k → ∀ᶠ (xy : β × β) in uniformity β ⊓ Filter.principal (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_inf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {p p' : L.Substructure M} {x : M},
  x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_compAddMonoidHom : ∀ {A : Type u_1} {B : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : Monoid M]
  (φ : AddChar B M) (f : A →+ B), ⇑(φ.compAddMonoidHom f) = ⇑φ ∘ ⇑f
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (X_1 : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)),
  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso F U).inv.app X_1).hom =
    CategoryTheory.CategoryStruct.id X_1.pt
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesRightKanExtension F L] [inst_5 : L.HasRightKanExtension F]
  (a : A) {Z : D} (h : G.obj (F.obj a) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((G.rightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a))
      (CategoryTheory.CategoryStruct.comp (G.map ((L.rightKanExtensionCounit F).app a)) h) =
    CategoryTheory.CategoryStruct.comp ((L.rightKanExtensionCounit (F.comp G)).app a) h
-- Mathlib.Algebra.Group.Defs
IsAddCommutative.instDivisionAddCommMonoid.eq_1 : ∀ {M : Type u_2} [inst : SubtractionMonoid M] [inst_1 : IsAddCommutative M],
  IsAddCommutative.instDivisionAddCommMonoid = { toSubtractionMonoid := inst, add_comm := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.not_reachable_of_left_degree_zero : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : Fintype ↑(G.neighborSet u)],
  u ≠ v → G.degree u = 0 → ¬G.Reachable u v
-- Init.Data.Fin.Fold
Fin.foldr.loop.eq_2 : ∀ {α : Sort u_1} (n : ℕ) (f : Fin n → α → α) (a : α) (i_1 : ℕ) (h : i_1 + 1 ≤ n),
  Fin.foldr.loop n f i_1.succ h a = Fin.foldr.loop n f i_1 ⋯ (f ⟨i_1, h⟩ a)
-- Mathlib.Analysis.Convex.Integral
/-- **Jensen's inequality**: if a function `g : E → ℝ` is concave and continuous on a convex closed
set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending
`μ`-a.e. points of a set `t` to `s`, then the average value of `g ∘ f` over `t` is less than or
equal to the value of `g` at the average value of `f` over `t` provided that both `f` and `g ∘ f`
are integrable.  -/
ConcaveOn.le_map_set_average : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ},
  ConcaveOn ℝ s g →
    ContinuousOn g s →
      IsClosed s →
        μ t ≠ 0 →
          μ t ≠ ⊤ →
            (∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) →
              MeasureTheory.IntegrableOn f t μ →
                MeasureTheory.IntegrableOn (g ∘ f) t μ → ⨍ (x : α) in t, g (f x) ∂μ ≤ g (⨍ (x : α) in t, f x ∂μ)
-- Lean.Elab.Tactic.Induction
/-- Return the binder name at `fType`. This method assumes `fType` is a function type.  -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.getBindingName : Lean.Elab.Tactic.ElimApp.M✝ Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C} (α : X ⟶ Y),
  (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.functor.map α).hom =
    α.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- If `C(α, β)` is a complete space, then for any (possibly, discontinuous) function `f`
and any set `s`, the set of functions `g : C(α, β)` that are equal to `f` on `s`
is a complete set.

Note that this set does not have to be a closed set when `β` is not T0.
This lemma is useful to prove that, e.g., the space of paths between two points
and the space of homotopies between two continuous maps are complete spaces,
without assuming that the codomain is a Hausdorff space.  -/
ContinuousMap.isComplete_setOfPred_eqOn : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] [CompleteSpace C(α, β)] (f : α → β)
  (s : Set α), IsComplete {g | Set.EqOn (⇑g) f s}
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- More explicit constructor in case `Ω₀` is already known to be a terminal object.  -/
CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Ω₀ : C) →
      (t : CategoryTheory.Limits.IsTerminal Ω₀) →
        (Ω : C) →
          (truth : Ω₀ ⟶ Ω) →
            (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω) →
              (∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m],
                  CategoryTheory.IsPullback m (t.from U) (χ m) truth) →
                (∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] (χ' : X ⟶ Ω),
                    CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m) →
                  CategoryTheory.Subobject.Classifier C
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- Auxiliary definition for `MeasureTheory.Measure.condKernel` and
`ProbabilityTheory.Kernel.condKernel`.
A conditional kernel for `κ : Kernel Unit (α × ℝ)`.  -/
ProbabilityTheory.Kernel.condKernelUnitReal : {α : Type u_1} →
  {mα : MeasurableSpace α} →
    (κ : ProbabilityTheory.Kernel Unit (α × ℝ)) →
      [ProbabilityTheory.IsFiniteKernel κ] → ProbabilityTheory.Kernel (Unit × α) ℝ
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instNeg : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : AddGroup γ] → [IsTopologicalAddGroup γ] → Neg (α →ₘ[μ] γ)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The category of profinite groups. A term of this type consists of a profinite
set with a topological group structure.
 -/
ProfiniteGrp : Type (u + 1)
-- Mathlib.Data.Sym.Basic
instDecidableRelVectorEquivOfDecidableEq : {α : Type u_1} → {n : ℕ} → [DecidableEq α] → DecidableRel fun x1 x2 => x1 ≈ x2
-- Init.Data.SInt.Lemmas
Int64.toInt_zero : Int64.toInt 0 = 0
-- Mathlib.Computability.Partrec
Partrec₂.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable β]
  [inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : β → γ →. σ} {g : α → β} {h : α → γ},
  Partrec₂ f → Computable g → Computable h → Partrec fun a => f (g a) (h a)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.Hom.ext_iff : ∀ {A B : AddSemigrp} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Algebra.Ring.ULift
ULift.up_natCast : ∀ {R : Type u} [inst : NatCast R] (n : ℕ), { down := ↑n } = ↑n
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_toUInt64 : ∀ (n : USize) (h : System.Platform.numBits = 32), n.toUInt64.toBitVec = BitVec.setWidth 64 (n.toBitVec32 h)
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation.eq_4 : ∀ (x n : ℕ), hyperoperation n.succ.succ.succ x 0 = 1
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.not_continuousAt_inv_log_one : ¬ContinuousAt (fun x => (Real.log x)⁻¹) 1
-- Mathlib.Algebra.Order.Kleene
mul_kstar_le : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a b c : α}, b ≤ c → c * a ≤ c → b * KStar.kstar a ≤ c
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.brecOn.go : {motive : Lean.Grind.CommRing.Poly → Sort u} →
  (t : Lean.Grind.CommRing.Poly) →
    ((t : Lean.Grind.CommRing.Poly) → Lean.Grind.CommRing.Poly.below t → motive t) →
      motive t ×' Lean.Grind.CommRing.Poly.below t
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- Assuming the base ring has a discrete topology, the powers of a `MvPowerSeries` converge to 0
iff its constant coefficient is nilpotent.
[N. Bourbaki, *Algebra II*, Chapter 4, §4, n°2, corollary of prop. 3][bourbaki1981]

See also `MvPowerSeries.LinearTopology.isTopologicallyNilpotent_iff_constantCoeff`.  -/
MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : CommRing R] [DiscreteTopology R]
  (f : MvPowerSeries σ R), IsTopologicallyNilpotent f ↔ IsNilpotent (MvPowerSeries.constantCoeff f)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.leftHomotopy_congruence : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V],
  CategoryTheory.Congruence (CategoryTheory.Arrow.leftHomotopic V)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.toOver_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (X : T)
  (X_1 : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)),
  ((CategoryTheory.CostructuredArrow.toOver F X).obj X_1).hom = X_1.hom
-- Mathlib.Algebra.Category.ModuleCat.Images
ModuleCat.imageIsoRange_inv_image_ι_assoc : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H) {Z : ModuleCat R} (h : H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (ModuleCat.Hom.hom f).range.subtype) h
-- Batteries.Data.List.Basic
List.productTR.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β),
  l₁.productTR l₂ = (List.foldl (fun acc a => List.foldl (fun acc b => acc.push (a, b)) acc l₂) #[] l₁).toList
-- Mathlib.Topology.Closure
interior_iInter_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort v} (s : ι → Set X), interior (⋂ i, s i) ⊆ ⋂ i, interior (s i)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- `pointsWithCircumcenter`, applied to a `pointIndex` value,
equals `points` applied to that value.  -/
Affine.Simplex.pointsWithCircumcenter_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.pointsWithCircumcenter (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex i) = s.points i
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.smul_map_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) {U V : Cᵒᵖ} (f : U ⟶ V) (r : ↑(R.obj U)) {Z : AddCommGrpCat} (h : M.presheaf.obj V ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((M.obj U).smul r) (M.presheaf.map f)) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (M.presheaf.map f)
        ((M.obj V).smul ((CategoryTheory.ConcreteCategory.hom (R.map f)) r)))
      h
-- Mathlib.Data.List.GetD
List.getD_append : ∀ {α : Type u} (l l' : List α) (d : α), ∀ n < l.length, (l ++ l').getD n d = l.getD n d
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuous.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : TopologicalSpace β] {f : α → Set β} {g : γ → α},
  LowerHemicontinuous f → Continuous g → LowerHemicontinuous (f ∘ g)
-- Mathlib.Tactic.Ring.Common
/-- Embed an exponent (an `ExBase, ExProd` pair) as an `ExProd` by multiplying by 1.  -/
Mathlib.Tactic.Ring.Common.ExBase.toProd : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          {a : Q(«$α»)} →
            {b : Q(ℕ)} →
              Mathlib.Tactic.Ring.Common.ExBase bt sα a →
                Mathlib.Tactic.Ring.Common.ExProdNat b →
                  Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExProd bt sα)
                    q(«$a» ^ «$b» * Nat.rawCast 1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.of_toList_perm : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β},
  m₁.toList.Perm m₂.toList → m₁.Equiv m₂
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.tsnd_tfst : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] {F G : Type u → Type u} [inst_1 : Applicative F]
  [inst_2 : Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ α₁ β₀ β₁ : Type u}
  (f : α₀ → F α₁) (f' : β₀ → G β₁) (x : t α₀ β₀),
  Functor.Comp.mk (Bitraversable.tsnd f' <$> Bitraversable.tfst f x) =
    bitraverse (Functor.Comp.mk ∘ Functor.map pure ∘ f) (Functor.Comp.mk ∘ pure ∘ f') x
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
_private.Mathlib.RingTheory.Polynomial.Hermite.Basic.0.Polynomial.hermite.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- The sheafification-inclusion adjunction.  -/
CategoryTheory.sheafificationAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          [inst_2 : CategoryTheory.HasWeakSheafify J A] →
            CategoryTheory.presheafToSheaf J A ⊣ CategoryTheory.sheafToPresheaf J A
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_div_const_Iic : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x / a) ⁻¹' Set.Iic b = Set.Iic (b * a)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.esymm_zero : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ], MvPolynomial.esymm σ R 0 = 1
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatch.not_isRevMatch : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos → ∀ pos' < pos, ¬String.Slice.Pattern.Model.IsRevMatch pat pos'
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx.match_1.congr : ∀ {α : Sort u} {o o' : Ordering} {lt : o = Ordering.lt → α} {eq : o = Ordering.eq → α} {gt : o = Ordering.gt → α}
  {lt' : o' = Ordering.lt → α} {eq' : o' = Ordering.eq → α} {gt' : o' = Ordering.gt → α} (ho : o = o'),
  (∀ (h : o' = Ordering.lt), lt ⋯ = lt' h) →
    (∀ (h : o' = Ordering.eq), eq ⋯ = eq' h) →
      (∀ (h : o' = Ordering.gt), gt ⋯ = gt' h) →
        (match h : o with
          | Ordering.lt => lt h
          | Ordering.eq => eq h
          | Ordering.gt => gt h) =
          match h : o' with
          | Ordering.lt => lt' h
          | Ordering.eq => eq' h
          | Ordering.gt => gt' h
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instLawfulIdentityMeetTop : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l],
  Std.LawfulIdentity (fun x1 x2 => Lean.Order.meet x1 x2) Lean.Order.top
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1` and `*` is a monoid, if it admits an injective map that preserves `1`
and `*` to a monoid.  See note [reducible non-instances].  -/
Function.Injective.monoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : Monoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 1 = 1 → (∀ (x y : M₁), f (x * y) = f x * f y) → (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → Monoid M₁
-- Mathlib.RingTheory.Multiplicity
/-- `FiniteMultiplicity a b` indicates that the multiplicity of `a` in `b` is finite.  -/
FiniteMultiplicity : {α : Type u_1} → [Monoid α] → α → α → Prop
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.encodeCode.match_1.eq_7 : ∀ (motive : Nat.Partrec.Code → Sort u_1) (cf cg : Nat.Partrec.Code) (h_1 : Unit → motive Nat.Partrec.Code.zero)
  (h_2 : Unit → motive Nat.Partrec.Code.succ) (h_3 : Unit → motive Nat.Partrec.Code.left)
  (h_4 : Unit → motive Nat.Partrec.Code.right) (h_5 : (cf cg : Nat.Partrec.Code) → motive (cf.pair cg))
  (h_6 : (cf cg : Nat.Partrec.Code) → motive (cf.comp cg)) (h_7 : (cf cg : Nat.Partrec.Code) → motive (cf.prec cg))
  (h_8 : (cf : Nat.Partrec.Code) → motive cf.rfind'),
  (match cf.prec cg with
    | Nat.Partrec.Code.zero => h_1 ()
    | Nat.Partrec.Code.succ => h_2 ()
    | Nat.Partrec.Code.left => h_3 ()
    | Nat.Partrec.Code.right => h_4 ()
    | cf.pair cg => h_5 cf cg
    | cf.comp cg => h_6 cf cg
    | cf.prec cg => h_7 cf cg
    | cf.rfind' => h_8 cf) =
    h_7 cf cg
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.isNat.natElim : ∀ {p : ℕ → Prop} {n n' : ℕ}, Mathlib.Meta.NormNum.IsNat n n' → p n' → p n
-- Mathlib.Analysis.Analytic.Binomial
/-- **Binomial series**: the (scalar) formal multilinear series with coefficients given
by `Ring.choose a`. The sum of this series is `fun x ↦ (1 + x) ^ a` within the radius
of convergence.  -/
binomialSeries : {𝕂 : Type u} →
  [inst : Field 𝕂] →
    [CharZero 𝕂] →
      (𝔸 : Type v) →
        [inst_2 : Ring 𝔸] →
          [inst_3 : Algebra 𝕂 𝔸] →
            [inst_4 : TopologicalSpace 𝔸] → [inst_5 : IsTopologicalRing 𝔸] → 𝕂 → FormalMultilinearSeries 𝕂 𝔸 𝔸
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.merge.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (xs ys : List α) →
      ((ys : List α) → motive [] ys) →
        ((xs : List α) → (xs = [] → False) → motive xs []) →
          ((x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)) → motive xs ys
-- Mathlib.Algebra.Group.Prod
Prod.instIsRightCancelAdd : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] [IsRightCancelAdd G] [IsRightCancelAdd H],
  IsRightCancelAdd (G × H)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.top_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Subalgebra.toSubmodule ⊤ = ⊤
-- Mathlib.Data.Set.Function
Set.eqOn_of_leftInvOn_of_rightInvOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f₁' f₂' : β → α},
  Set.LeftInvOn f₁' f s → Set.RightInvOn f₂' f t → Set.MapsTo f₂' t s → Set.EqOn f₁' f₂' t
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance!.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (r : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          motive
            (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rr : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k : α) →
                (v : β k) →
                  (l r : Std.DTreeMap.Internal.Impl α β) →
                    rr = Std.DTreeMap.Internal.Impl.inner size_1 k v l r →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                          (Std.DTreeMap.Internal.Impl.inner size_1 k v l r)))
  (h_4 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (size_1 : ℕ) →
            (rlk : α) →
              (rlv : β rlk) →
                (l r : Std.DTreeMap.Internal.Impl α β) →
                  motive
                    (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                      Std.DTreeMap.Internal.Impl.leaf))
  (h_5 :
    (rs : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rls : ℕ) →
            (rlk : α) →
              (rlv : β rlk) →
                (rll rlr rr : Std.DTreeMap.Internal.Impl α β) →
                  (size : ℕ) →
                    (k : α) →
                      (v : β k) →
                        (l r : Std.DTreeMap.Internal.Impl α β) →
                          rr = Std.DTreeMap.Internal.Impl.inner size k v l r →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner rs rk rv
                                (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
                                (Std.DTreeMap.Internal.Impl.inner size k v l r))),
  r = Std.DTreeMap.Internal.Impl.leaf →
    (match r with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf =>
        h_2 size k v
      |
      Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
          rr@h:(Std.DTreeMap.Internal.Impl.inner size_1 k v l r) =>
        h_3 size rk rv rr size_1 k v l r h
      |
      Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
          Std.DTreeMap.Internal.Impl.leaf =>
        h_4 size rk rv size_1 rlk rlv l r
      |
      Std.DTreeMap.Internal.Impl.inner rs rk rv (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
          rr@h:(Std.DTreeMap.Internal.Impl.inner size k v l r) =>
        h_5 rs rk rv rls rlk rlv rll rlr rr size k v l r h) ≍
      h_1 ()
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.trivial_ρ_apply : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {V : Type w} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (g : G) (v : V), ((Rep.trivial k G V).ρ g) v = v
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_unitOfList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.HashMap.Raw.unitOfList l).getKey? k' = some k