mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- `smul` can be moved from one side of the product to the other .  -/
TensorProduct.smul_tmul : ∀ {R : Type u_1} {R' : Type u_4} [inst : CommSemiring R] [inst_1 : Monoid R'] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : DistribMulAction R' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : DistribMulAction R' N] [TensorProduct.CompatibleSMul R R' M N] (r : R') (m : M)
  (n : N), (r • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • n)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.IsCut.lt_trans : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} [RBTree.RBNode.IsCut cmp cut]
  [Std.TransCmp cmp], cmp x y = Ordering.lt → cut x = Ordering.lt → cut y = Ordering.lt
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome.success.sizeOf_spec : ∀ (stx : Lean.TSyntax `tactic), sizeOf (Mathlib.TacticAnalysis.TerminalReplacementOutcome.success✝ stx) = 1 + sizeOf stx
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- **Alias** of the reverse direction of `measurable_mem`. -/
MeasurableSet.mem : ∀ {α : Type u_1} {s : Set α} [inst : MeasurableSpace α], MeasurableSet s → Measurable fun x => x ∈ s
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
dist_pi_const_le : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : Fintype β] (a b : α),
  (dist (fun x => a) fun x => b) ≤ dist a b
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
/-- If the pre-`0`-hypercover `E` has pairwise pullbacks, the sections over the multifork
associated to a presheaf of types are equivalent to the compatible families on `E`.  -/
CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} →
      (E : CategoryTheory.PreZeroHypercover S) →
        [inst_1 : E.HasPullbacks] →
          (F : CategoryTheory.Functor Cᵒᵖ (Type u_2)) →
            (E.toPreOneHypercover.multicospanIndex F).sections ≃
              Subtype (CategoryTheory.Presieve.Arrows.Compatible F E.f)
-- Lean.Meta.Sym.AlphaShareCommon
/-- Returns `true` if `declName` is the name of a grind helper declaration that
should not be unfolded by `unfoldReducible`. `Grind.EqMatch` and `Grind.MatchCond`
are `abbrev`s, but they are gadgets that must survive until the corresponding
propagators consume them.
 -/
Lean.Meta.Sym.isGrindGadget : Lean.Name → Bool
-- Mathlib.Topology.Compactness.Lindelof
LindelofSpace.mk : ∀ {X : Type u_2} [inst : TopologicalSpace X], IsLindelof Set.univ → LindelofSpace X
-- Mathlib.Order.WellFoundedSet
Set.Finite.wellFoundedOn : ∀ {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α}, s.Finite → s.WellFoundedOn r
-- Mathlib.Topology.Separation.Basic
minimal_nonempty_open_eq_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X},
  IsOpen s → s.Nonempty → (∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) → ∃ x, s = {x}
-- Init.PropLemmas
left_iff_dite_iff : ∀ {p : Prop} [inst : Decidable p] {x : Prop} {y : ¬p → Prop}, (x ↔ if h : p then x else y h) ↔ ∀ (h : ¬p), x ↔ y h
-- Mathlib.Algebra.GradedMonoid
/-- A variant of `GradedMonoid.mk_list_dProd` for rewriting in the other direction.  -/
GradedMonoid.list_prod_map_eq_dProd : ∀ {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMonoid A] (l : List α)
  (f : α → GradedMonoid A),
  (List.map f l).prod =
    GradedMonoid.mk (l.dProdIndex fun i => (f i).fst) (l.dProd (fun i => (f i).fst) fun i => (f i).snd)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- The pullback provided by `HasPullback f g` fits into an `IsPullback`.  -/
CategoryTheory.IsPullback.of_hasPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g) f g
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.IndepFun.comp : ∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {γ : Type u_6} {γ' : Type u_7} {mα : MeasurableSpace α}
  {mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ω → β} {g : Ω → β'}
  {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {mγ : MeasurableSpace γ} {mγ' : MeasurableSpace γ'} {φ : β → γ}
  {ψ : β' → γ'},
  ProbabilityTheory.Kernel.IndepFun f g κ μ →
    Measurable φ → Measurable ψ → ProbabilityTheory.Kernel.IndepFun (φ ∘ f) (ψ ∘ g) κ μ
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  AddSubgroup.addCommutator = { bracket := fun H₁ H₂ => AddSubgroup.closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g} }
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.pushout_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushoutsAlong f] (x : CategoryTheory.Under X),
  (CategoryTheory.Under.pushout f).obj x = CategoryTheory.Under.mk (CategoryTheory.Limits.pushout.inr x.hom f)
-- Mathlib.Order.Minimal
maximal_subset_iff : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α}, Maximal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → s ⊆ t → s = t
-- Mathlib.Order.KrullDimension
Order.height_toDual : ∀ {α : Type u_1} [inst : Preorder α] (x : α), Order.height (OrderDual.toDual x) = Order.coheight x
-- Std.Time.Format.Modifier
/-- `v`: Generic time zone name, without DST distinction (e.g., Pacific Time, PT).
 -/
Std.Time.Modifier.v : Std.Time.ZoneName → Std.Time.Modifier
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.ind : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → Prop},
  (∀ (y : M × ↥S), p (AddLocalization.mk y.1 y.2)) → ∀ (x : AddLocalization S), p x
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- Given the trajectory up to time `a`, `partialTraj κ a b` gives the distribution of
the trajectory up to time `b`. Then plugging this into `partialTraj κ b c` gives
the distribution of the trajectory up to time `c`.  -/
ProbabilityTheory.Kernel.partialTraj_comp_partialTraj : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a b c : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))},
  a ≤ b →
    b ≤ c →
      (ProbabilityTheory.Kernel.partialTraj κ b c).comp (ProbabilityTheory.Kernel.partialTraj κ a b) =
        ProbabilityTheory.Kernel.partialTraj κ a c
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_le : ∀ {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}} {a : Ordinal.{max u v}},
  (∀ (i : Ordinal.{u}) (h : i < o), f i h ≤ a) → o.bsup f ≤ a
-- Lean.Elab.InfoTree.Types
Lean.Elab.TacticInfo.goalsBefore : Lean.Elab.TacticInfo → List Lean.MVarId
-- Mathlib.RingTheory.Unramified.LocalRing
Localization.exists_awayMap_bijective_of_localRingHom_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  [inst_3 : p.IsPrime] {q : Ideal S} [inst_4 : q.IsPrime],
  p.primesOver S = {q} →
    ∀ [Module.Finite R S] [inst_6 : q.LiesOver p],
      (RingHom.ker (algebraMap R S)).FG →
        Function.Bijective ⇑(Localization.localRingHom p q (algebraMap R S) ⋯) →
          ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Bijective ⇑(Localization.awayMap (algebraMap R S) r')
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
/-- The smallest positive integer `d` contained in the conductor of `θ`. It is the smallest integer
such that `d • 𝓞 K ⊆ ℤ[θ]`, see `exponent_eq_sInf`. It is set to `0` if `d` does not exists.
 -/
RingOfIntegers.exponent : {K : Type u_1} → [inst : Field K] → NumberField.RingOfIntegers K → ℕ
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- A commutative monoid object is a monoid object.  -/
CategoryTheory.CommMon.toMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.CommMon C → CategoryTheory.Mon C
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.comp_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [W.IsStableUnderComposition] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  W f → W g → W (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- Given two `C^n` functions `f` and `g` which coincide locally around the frontier of a set `s`,
then the piecewise function defined using `f` on `s` and `g` elsewhere is `C^n`.  -/
ContMDiff.piecewise : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  {f g : M → M'} {s : Set M} [inst_11 : DecidablePred fun x => x ∈ s],
  ContMDiff I I' n f → ContMDiff I I' n g → (∀ x ∈ frontier s, f =ᶠ[nhds x] g) → ContMDiff I I' n (s.piecewise f g)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.mk.injEq : ∀ (Functions : ℕ → Type u) (Relations : ℕ → Type v) (Functions_1 : ℕ → Type u) (Relations_1 : ℕ → Type v),
  ({ Functions := Functions, Relations := Relations } = { Functions := Functions_1, Relations := Relations_1 }) =
    (Functions = Functions_1 ∧ Relations = Relations_1)
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- Define the second primitive quadratic character on `ZMod 8`, `χ₈'`.
It corresponds to the extension `ℚ(√-2)/ℚ`.  -/
ZMod.χ₈' : MulChar (ZMod 8) ℤ
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.pushforward_def : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : AddGroup A] [inst_1 : AddGroup B]
  [inst_2 : AddGroup C] [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C]
  {φ : A →+ B} {ψ : B →+ C} (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A]
  [inst_7 : IsTopologicalAddGroup B] [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A]
  [inst_10 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [inst_11 : NormedSpace ℝ E]
  [inst_12 : IsTopologicalAddGroup C] [inst_13 : LocallyCompactSpace B] (f : CompactlySupportedContinuousMap B E)
  (c : C), ((H.pushforward μA) f) c = ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA
-- Lean.Data.OpenDecl
Lean.removeRoot : Lean.Name → Lean.Name
-- Std.Http.Data.Status
/-- Converts a `UInt16` to `Status`.
 -/
Std.Http.Status.ofCode : Option { x // Std.Http.IsValidReasonPhrase x } → UInt16 → Option Std.Http.Status
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.Const.alter.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_pi_sub : ∀ (x : ℝ), Real.sin (Real.pi - x) = Real.sin x
-- Mathlib.Order.Types.Arithmetic
OrderType.card_monotone : Monotone OrderType.card
-- Mathlib.CategoryTheory.ConnectedComponents
/-- The inclusion of each component into the decomposed category. This is just `sigma.incl` but having
this abbreviation helps guide typeclass search to get the right category instance on `decomposed J`.
 -/
CategoryTheory.inclusion : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    (j : CategoryTheory.ConnectedComponents J) → CategoryTheory.Functor j.Component (CategoryTheory.Decomposed J)
-- Mathlib.Algebra.RingQuot
RingQuot.instSemiring : {R : Type uR} → [inst : Semiring R] → (r : R → R → Prop) → Semiring (RingQuot r)
-- Mathlib.RingTheory.Localization.Away.Basic
/-- If `S₁` is the localization of `R` away from `f` and `S₂` is the localization away from `g`,
then any localization `T` of `S₂` away from `f` is also a localization of `S₁` away from `g`.  -/
IsLocalization.Away.commutes : ∀ {R : Type u_5} [inst : CommSemiring R] (S₁ : Type u_6) (S₂ : Type u_7) (T : Type u_8) [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] [inst_3 : CommSemiring T] [inst_4 : Algebra R S₁] [inst_5 : Algebra R S₂]
  [inst_6 : Algebra R T] [inst_7 : Algebra S₁ T] [inst_8 : Algebra S₂ T] [IsScalarTower R S₁ T] [IsScalarTower R S₂ T]
  (x y : R) [IsLocalization.Away x S₁] [IsLocalization.Away y S₂] [IsLocalization.Away ((algebraMap R S₂) x) T],
  IsLocalization.Away ((algebraMap R S₁) y) T
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.instOne : {ι : Type u_1} →
  {A : Type u_2} → {σ : Type u_6} → [inst : Semiring A] → [inst_1 : SetLike σ A] → {𝒜 : ι → σ} → One (𝒜 →+*ᵍ 𝒜)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.lift_symm_apply : ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (a : ExteriorAlgebra R M →ₐ[R] A),
  (ExteriorAlgebra.lift R).symm a = ⟨a.toLinearMap ∘ₗ CliffordAlgebra.ι 0, ⋯⟩
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Sum of a list of elements in a subring is in the subring.  -/
Subring.list_sum_mem : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) {l : List R}, (∀ x ∈ l, x ∈ s) → l.sum ∈ s
-- Mathlib.Algebra.Homology.BifunctorShift
/-- Auxiliary definition for `mapBifunctorShift₁Iso`.  -/
CochainComplex.mapBifunctorHomologicalComplexShift₁Iso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            [inst_3 : CategoryTheory.Preadditive C₁] →
              [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                [inst_5 : CategoryTheory.Preadditive D] →
                  (K₁ : CochainComplex C₁ ℤ) →
                    (K₂ : CochainComplex C₂ ℤ) →
                      (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                        [inst_6 : F.Additive] →
                          [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                            (x : ℤ) →
                              ((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj
                                      ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).obj
                                        K₁)).obj
                                  K₂ ≅
                                (HomologicalComplex₂.shiftFunctor₁ D x).obj
                                  (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj
                                        K₁).obj
                                    K₂)
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.coe_toGenContFract : ∀ {α : Type u_1} {β : Type u_2} [inst : Coe α β] {g : GenContFract α},
  ↑g = { h := Coe.coe g.h, s := Stream'.Seq.map GenContFract.Pair.coeFn g.s }
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.right_distrib : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x y z : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F ((x.add y).mul z) ((x.mul z).add (y.mul z))
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- **Alias** of `neg_apply`. -/
UniformConvergenceCLM.neg_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Neg β}
  {inst_2 : Neg F} [self : IsNegApply F α β] (f : F) (x : α), (-f) x = -f x
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort'_k : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.Analysis.Complex.Norm
Complex.lim_re : ∀ (f : CauSeq ℂ fun x => ‖x‖), (Complex.cauSeqRe f).lim = f.lim.re
-- Mathlib.MeasureTheory.Measure.Doubling
/-- A measure `μ` is said to be a uniformly locally doubling measure if there exists a constant `C`
such that for all sufficiently small radii `ε`, and for any centre, the measure of a ball of radius
`2 * ε` is bounded by `C` times the measure of the concentric ball of radius `ε`.

Note: it is important that this definition makes a demand only for sufficiently small `ε`. For
example we want hyperbolic space to carry the instance `IsUnifLocDoublingMeasure volume` but
volumes grow exponentially in hyperbolic space. To be really explicit, consider the hyperbolic plane
of curvature -1, the area of a disc of radius `ε` is `A(ε) = 2π(cosh(ε) - 1)` so
`A(2ε)/A(ε) ~ exp(ε)`.  -/
IsUnifLocDoublingMeasure : {α : Type u_1} → [PseudoMetricSpace α] → [inst : MeasurableSpace α] → MeasureTheory.Measure α → Prop
-- Mathlib.Analysis.Normed.Group.Basic
enorm_prod_le_of_le : ∀ {ι : Type u_3} {ε : Type u_8} [inst : TopologicalSpace ε] [inst_1 : ESeminormedCommMonoid ε] (s : Finset ι)
  {f : ι → ε} {n : ι → ENNReal}, (∀ b ∈ s, ‖f b‖ₑ ≤ n b) → ‖∏ b ∈ s, f b‖ₑ ≤ ∑ b ∈ s, n b
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CStarAlgebra.instNegPart : {A : Type u_1} →
  [inst : NonUnitalRing A] →
    [inst_1 : Module ℝ A] →
      [inst_2 : SMulCommClass ℝ A A] →
        [inst_3 : IsScalarTower ℝ A A] →
          [inst_4 : StarRing A] →
            [inst_5 : TopologicalSpace A] → [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] → NegPart A
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.State : Type
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
MonoidHom.CompTriple.IsId.eq_id : ∀ {M : Type u_1} {inst : Monoid M} {σ : M →* M} [self : MonoidHom.CompTriple.IsId σ], σ = MonoidHom.id M
-- Mathlib.Logic.Equiv.Prod
Equiv.prodPiEquivSumPi_apply : ∀ {ι : Type u_9} {ι' : Type u_10} (π : ι → Type u) (π' : ι' → Type u)
  (a : ((i : ι) → Sum.elim π π' (Sum.inl i)) × ((i' : ι') → Sum.elim π π' (Sum.inr i'))) (i : ι ⊕ ι'),
  (Equiv.prodPiEquivSumPi π π') a i = (Equiv.sumPiEquivProdPi (Sum.elim π π')).symm a i
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H) (β : F ⟶ L.comp G) (X : C),
  CategoryTheory.CategoryStruct.comp (α.app X) ((F'.descOfIsLeftKanExtension α G β).app (L.obj X)) = β.app X
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insert.go.induct_unfolding : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k_1 : ℤ),
      motive (Lean.Grind.CommRing.Poly.num k_1) (Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.num k_1))) →
    (∀ (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        m.grevlex m_1 = Ordering.eq →
          have k := k + k_1;
          (k == 0) = true → motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p) p) →
      (∀ (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
          m.grevlex m_1 = Ordering.eq →
            have k := k + k_1;
            (k == 0) = false → motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p) (Lean.Grind.CommRing.Poly.add k m p)) →
        (∀ (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
            m.grevlex m_1 = Ordering.gt →
              motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p)
                (Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.add k_1 m_1 p))) →
          (∀ (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
              m.grevlex m_1 = Ordering.lt →
                motive p (Lean.Grind.CommRing.Poly.insert.go k m p) →
                  motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p)
                    (Lean.Grind.CommRing.Poly.add k_1 m_1 (Lean.Grind.CommRing.Poly.insert.go k m p))) →
            ∀ (a : Lean.Grind.CommRing.Poly), motive a (Lean.Grind.CommRing.Poly.insert.go k m a)
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.addGroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst_1 : Zero M₂] [inst_2 : SMul ℕ M₂] [inst_3 : Neg M₂]
  [inst_4 : Sub M₂] [inst_5 : SMul ℤ M₂] [inst_6 : AddGroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f)
  (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x)
  (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
  (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x),
  Function.Surjective.addGroup f hf one mul inv div npow zpow =
    { toSubNegMonoid := Function.Surjective.subNegMonoid f hf one mul inv div npow zpow, neg_add_cancel := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_eq_back?_keysArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.maxKey? = t.keysArray.back?
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.exp_neg_llr : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν → (fun x => Real.exp (-MeasureTheory.llr μ ν x)) =ᵐ[μ] fun x => (ν.rnDeriv μ x).toReal
-- Aesop.RuleTac.GoalDiff
Aesop.instInhabitedGoalDiff.default : Aesop.GoalDiff
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
ContDiff.fourierPowSMulRight : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} {k : WithTop ℕ∞},
  ContDiff ℝ k f → ∀ (n : ℕ), ContDiff ℝ k fun v => VectorFourier.fourierPowSMulRight L f v n
-- Mathlib.GroupTheory.OrderOfElement
orderOf_one : ∀ {G : Type u_1} [inst : Monoid G], orderOf 1 = 1
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.triangle_obj₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C],
  (CochainComplex.mappingCocone.triangle φ).obj₂ = K
-- Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
CategoryTheory.Limits.sigmaConstCokernelCofork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (R : C)
  {α : Type u_1} {β : Type u_2} (f : α → β) [inst_2 : CategoryTheory.Limits.HasCoproduct fun x => R]
  [inst_3 : CategoryTheory.Limits.HasCoproduct fun x => R] [inst_4 : CategoryTheory.Limits.HasCoproduct fun x => R],
  (CategoryTheory.Limits.sigmaConstCokernelCofork R f).pt = ∐ fun x => R
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_congr : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
  {g₁ g₂ : α → F}, f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → (f₁ =O[l] g₁ ↔ f₂ =O[l] g₂)
-- Std.Time.Format.Modifier
Std.Time.Modifier.x.injEq : ∀ (presentation presentation_1 : Std.Time.OffsetX),
  (Std.Time.Modifier.x presentation = Std.Time.Modifier.x presentation_1) = (presentation = presentation_1)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The category of topological modules.  -/
TopModuleCat : (R : Type u) → [Ring R] → [TopologicalSpace R] → Type (max u (v + 1))
-- Mathlib.Analysis.Normed.Ring.Basic
SeminormedCommRing.mk : {α : Type u_5} → [toSeminormedRing : SeminormedRing α] → (∀ (a b : α), a * b = b * a) → SeminormedCommRing α