mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
/-- The inductive group (with parameters) of the argument's type  -/
Lean.Elab.Structural.RecArgInfo.indGroupInst : Lean.Elab.Structural.RecArgInfo → Lean.Elab.Structural.IndGroupInst
-- Init.Data.BitVec.Lemmas
BitVec.intMax.eq_1 : ∀ (w : ℕ), BitVec.intMax w = BitVec.twoPow w (w - 1) - 1
-- Mathlib.Topology.MetricSpace.Bilipschitz
/-- If `f : α → β` is bilipschitz, then the pullback of the bornology on `β` through `f` agrees
with the bornology on `α`.  -/
bornology_eq_of_bilipschitz : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K₁ K₂ : NNReal}
  {f : α → β}, AntilipschitzWith K₁ f → LipschitzWith K₂ f → Bornology.cobounded α = Bornology.cobounded α
-- Mathlib.Order.RelIso.Basic
RelIso.coe_ofOnFun : ∀ {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α ≃ β), ⇑(RelIso.ofOnFun r f) = ⇑f
-- Mathlib.Data.Ordmap.Invariants
Ordnode.findMax'_all : ∀ {α : Type u_1} {P : α → Prop} (x : α) (t : Ordnode α), P x → Ordnode.All P t → P (Ordnode.findMax' x t)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orImpL.inj : ∀ {p p_1 : Mathlib.Tactic.ITauto.Proof}, p.orImpL = p_1.orImpL → p = p_1
-- Mathlib.Order.CompactlyGenerated.Basic
/-- In an atomic lattice, every element `b` has a complement of the form `sSup s` relative to a
given element `c`, where each element of `s` is an atom.
See also `complementedLattice_of_sSup_atoms_eq_top`.  -/
exists_sSupIndep_disjoint_sSup_atoms : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (b c : α),
  b ≤ c →
    sSup {a | a ≤ c ∧ IsAtom a} = c →
      ∃ s, sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
-- Lean.ScopedEnvExtension
/-- Used to implement `end_local_scope` command, that disables delimiting local entries of ScopedEnvExtension
across `depth` scope levels.
 -/
Lean.setDelimitsLocal : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [MonadLiftT (ST IO.RealWorld) m] → ℕ → m Unit
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰)
  {i j : 𝒰.I₀} (hij : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (d.functor.map hij)
-- Mathlib.Analysis.Asymptotics.TVS
/-- We say that `f =Θ[𝕜; l] g` (`IsThetaTVS 𝕜 l f g`), if `f =O[𝕜; l] g` and `g =O[𝕜; l] f`.
It is a generalization of `f =Θ[l] g` that works in topological `𝕜`-vector spaces.  -/
Asymptotics.IsThetaTVS : (𝕜 : Type u_1) →
  {α : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        [ENorm 𝕜] →
          [TopologicalSpace E] →
            [TopologicalSpace F] → [Zero E] → [Zero F] → [SMul 𝕜 E] → [SMul 𝕜 F] → Filter α → (α → E) → (α → F) → Prop
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.commaFromUnder_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (K : CategoryTheory.Functor J (CategoryTheory.Under X)),
  (CategoryTheory.WithInitial.commaFromUnder.obj K).right = K.comp (CategoryTheory.Under.forget X)
-- Mathlib.CategoryTheory.Comma.Basic
/-- The right subobject  -/
CategoryTheory.Comma.right : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor A T} → {R : CategoryTheory.Functor B T} → CategoryTheory.Comma L R → B
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.lift₂Expand.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_3}
  [inst_2 : AddAction R X] {C : Sort u_2} (P : X → ↥S → X → ↥S → C)
  (hP :
    ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ + ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ + ↑s₂ ∈ S),
      P r₁ s₁ r₂ s₂ = P (t₁ +ᵥ r₁) ⟨t₁ + ↑s₁, ht₁⟩ (t₂ +ᵥ r₂) ⟨t₂ + ↑s₂, ht₂⟩),
  AddOreLocalization.lift₂Expand P hP =
    AddOreLocalization.liftExpand (fun r₁ s₁ => AddOreLocalization.liftExpand (P r₁ s₁) ⋯) ⋯
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientQuotientEquivQuotient.eq_1 : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M),
  QuotientGroup.quotientQuotientEquivQuotient N M h =
    (QuotientGroup.quotientQuotientEquivQuotientAux N M h).toMulEquiv
      (QuotientGroup.map M (Subgroup.map (QuotientGroup.mk' N) M) (QuotientGroup.mk' N) ⋯) ⋯ ⋯
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.TaggedPrepartition.unionComplToSubordinate.eq_1 : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I)
  (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → ↑(Set.Ioi 0)),
  π₁.unionComplToSubordinate π₂ hU r = π₁.disjUnion (π₂.toSubordinate r) ⋯
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- Given a family of Hilbert spaces `G : ι → Type*`, a Hilbert sum of `G` consists of a Hilbert
space `E` and an orthogonal family `V : Π i, G i →ₗᵢ[𝕜] E` such that the induced isometry
`Φ : lp G 2 → E` is surjective.

Keeping in mind that `lp G 2` is "the" external Hilbert sum of `G : ι → Type*`, this is analogous
to `DirectSum.IsInternal`, except that we don't express it in terms of actual submodules.  -/
IsHilbertSum : {ι : Type u_1} →
  (𝕜 : Type u_2) →
    [inst : RCLike 𝕜] →
      {E : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            (G : ι → Type u_4) →
              [inst_3 : (i : ι) → NormedAddCommGroup (G i)] →
                [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] → [CompleteSpace E] → ((i : ι) → G i →ₗᵢ[𝕜] E) → Prop
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- Create a `ConditionallyCompleteLattice` from a `PartialOrder` and `sup` function
that returns the least upper bound of a nonempty set which is bounded above. Usually this
constructor provides poor definitional equalities.  If other fields are known explicitly, they
should be provided; for example, if `inf` is known explicitly, construct the
`ConditionallyCompleteLattice` instance as
```
instance : ConditionallyCompleteLattice my_T where
  inf := better_inf
  le_inf := ...
  inf_le_right := ...
  inf_le_left := ...
  -- don't care to fix sup, sInf
  __ := conditionallyCompleteLatticeOfsSup my_T ...
```
 -/
conditionallyCompleteLatticeOfsSup : (α : Type u_5) →
  [H1 : PartialOrder α] →
    [H2 : SupSet α] →
      (∀ (a b : α), BddAbove {a, b}) →
        (∀ (a b : α), BddBelow {a, b}) →
          (∀ (s : Set α), BddAbove s → s.Nonempty → IsLUB s (sSup s)) → ConditionallyCompleteLattice α
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- Angles are translation invariant.  -/
EuclideanGeometry.angle_const_vsub : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p p₁ p₂ p₃ : P),
  EuclideanGeometry.angle (p -ᵥ p₁) (p -ᵥ p₂) (p -ᵥ p₃) = EuclideanGeometry.angle p₁ p₂ p₃
-- Init.Data.List.Lemmas
List.exists_mem_cons : ∀ {α : Type u_1} {p : α → Prop} {a : α} {l : List α}, (∃ x, ∃ (_ : x ∈ a :: l), p x) ↔ p a ∨ ∃ x, ∃ (_ : x ∈ l), p x
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.brecOn_1.eq : ∀ {motive_1 : Lean.Parser.Tactic.MRefinePat → Sort u} {motive_2 : List Lean.Parser.Tactic.MRefinePat → Sort u}
  (t : List Lean.Parser.Tactic.MRefinePat) (F_1 : (t : Lean.Parser.Tactic.MRefinePat) → t.below → motive_1 t)
  (F_2 : (t : List Lean.Parser.Tactic.MRefinePat) → Lean.Parser.Tactic.MRefinePat.below_1 t → motive_2 t),
  Lean.Parser.Tactic.MRefinePat.brecOn_1 t F_1 F_2 = F_2 t (Lean.Parser.Tactic.MRefinePat.brecOn_1.go t F_1 F_2).2
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivAevalXAddC.eq_1 : ∀ {R : Type u_3} [inst : CommRing R] (t : R),
  Polynomial.algEquivAevalXAddC t =
    (Polynomial.X + Polynomial.C t).algEquivOfCompEqX (Polynomial.X - Polynomial.C t) ⋯ ⋯
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
/-- Faithfulness follows because `G` is a separator, see
`isSeparator_iff_faithful_preadditiveCoyonedaObj`.  -/
CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.full : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] (G : C),
  CategoryTheory.IsSeparator G → (CategoryTheory.preadditiveCoyonedaObj G).Full
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_minKey?_modify_eq_isSome : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : β → β}, (t.modify k f).minKey?.isSome = t.minKey?.isSome
-- Mathlib.Data.Finset.Insert
/-- Combine a product with a pi type to pi of insert.  -/
Finset.prodPiInsert : {α : Type u_1} →
  [inst : DecidableEq α] →
    {s : Finset α} → (f : α → Type u_3) → {a : α} → f a × ((i : α) → i ∈ s → f i) → (i : α) → i ∈ insert a s → f i
-- Mathlib.Topology.PartitionOfUnity
/-- If `f` is a partition of unity on `s : Set X` and `g : X → E` is continuous at every point of
the topological support of some `f i`, then `fun x ↦ f i x • g x` is continuous on the whole space.
 -/
PartitionOfUnity.continuous_smul : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {E : Type u_1} [inst_1 : AddCommMonoid E]
  [inst_2 : SMulWithZero ℝ E] [inst_3 : TopologicalSpace E] [ContinuousSMul ℝ E] {s : Set X}
  (f : PartitionOfUnity ι X s) {g : X → E} {i : ι},
  (∀ x ∈ tsupport ⇑(f i), ContinuousAt g x) → Continuous fun x => (f i) x • g x
-- Init.Meta.Defs
/-- Creates an array of syntax, separated by `sep`.
 -/
Lean.mkSepArray : Array Lean.Syntax → Lean.Syntax → Array Lean.Syntax
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.sum_partition_boxes' : ∀ {ι : Type u_3} {M : Type u_4} [inst : AddCommMonoid M] {I : WithTop (BoxIntegral.Box ι)}
  (self : BoxIntegral.BoxAdditiveMap ι M I) (J : BoxIntegral.Box ι),
  ↑J ≤ I → ∀ (π : BoxIntegral.Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, self.toFun Ji = self.toFun J
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_diff_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∈ m₁ \ m₂ ↔ k ∈ m₁ ∧ k ∉ m₂
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instRing : (X : Type u_2) → {S : Type u_3} → [inst : CommRing S] → Ring (FreeAlgebra S X)
-- Mathlib.Data.FinEnum
/-- A type indexable by `Fin n` with positive `n` is inhabited and vice versa.  -/
FinEnum.card_pos_iff : ∀ {α : Type u} [inst : FinEnum α], 0 < FinEnum.card α ↔ Nonempty α
-- Lean.Parser.Basic
/-- Implements a variant of Pratt's algorithm. In Pratt's algorithms tokens have a right and left binding power.
In our implementation, parsers have precedence instead. This method selects a parser (or more, via
`longestMatchFn`) from `leadingTable` based on the current token. Note that the unindexed `leadingParsers` parsers
are also tried. We have the unindexed `leadingParsers` because some parsers do not have a "first token". Example:
```
syntax term:51 "≤" ident "<" term "|" term : index
```
Example, in principle, the set of first tokens for this parser is any token that can start a term, but this set
is always changing. Thus, this parsing rule is stored as an unindexed leading parser at `leadingParsers`.
After processing the leading parser, we chain with parsers from `trailingTable`/`trailingParsers` that have precedence
at least `c.prec` where `c` is the `ParsingContext`. Recall that `c.prec` is set by `categoryParser`.

Note that in the original Pratt's algorithm, precedences are only checked before calling trailing parsers. In our
implementation, leading *and* trailing parsers check the precedence. We claim our algorithm is more flexible,
modular and easier to understand.

`antiquotParser` should be a `mkAntiquot` parser (or always fail) and is tried before all other parsers.
It should not be added to the regular leading parsers because it would heavily
overlap with antiquotation parsers nested inside them.  -/
Lean.Parser.prattParser : Lean.Name →
  Lean.Parser.PrattParsingTables → Lean.Parser.LeadingIdentBehavior → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.integral_traj_partialTraj' : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] {a b : ℕ},
  a ≤ b →
    ∀ {x₀ : (i : ↥(Finset.Iic a)) → X ↑i} {f : ((i : ↥(Finset.Iic b)) → X ↑i) → ((n : ℕ) → X n) → E},
      MeasureTheory.Integrable (Function.uncurry f)
          (((ProbabilityTheory.Kernel.partialTraj κ a b) x₀).compProd (ProbabilityTheory.Kernel.traj κ b)) →
        ∫ (x : (i : ↥(Finset.Iic b)) → X ↑i),
            ∫ (y : (n : ℕ) → X n),
              f x y ∂(ProbabilityTheory.Kernel.traj κ b) x ∂(ProbabilityTheory.Kernel.partialTraj κ a b) x₀ =
          ∫ (x : (n : ℕ) → X n), f (Preorder.frestrictLe b x) x ∂(ProbabilityTheory.Kernel.traj κ a) x₀
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.CategoryStruct.comp F.toRightDerivedZero F.rightDerivedZeroIsoSelf.hom =
    CategoryTheory.CategoryStruct.id F
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.mk_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y),
  (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).pt = P
-- Mathlib.RingTheory.Algebraic.Basic
Subalgebra.isAlgebraic_of_isAlgebraic_bot : ∀ {R : Type u} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  IsAlgebraic (↥⊥) x → IsAlgebraic R x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.FinStronglyMeasurable.add : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → β}
  [inst : TopologicalSpace β] [inst_1 : AddZeroClass β] [ContinuousAdd β],
  MeasureTheory.FinStronglyMeasurable f μ →
    MeasureTheory.FinStronglyMeasurable g μ → MeasureTheory.FinStronglyMeasurable (f + g) μ
-- Mathlib.Order.Filter.Lift
Filter.prod_def : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, f ×ˢ g = f.lift fun s => g.lift' fun t => s ×ˢ t
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSymbolKind : Lean.FromJson Lean.Lsp.SymbolKind
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.regularizedGaussHGFunSeries.eq_1 : ∀ (a b c : ℂ), a.regularizedGaussHGFunSeries b c = Complex.regularizedHGFunSeries {a, b} {c}
-- Mathlib.Algebra.Group.Units.Basic
Units.inv_eq_of_mul_eq_one_right : ∀ {α : Type u} [inst : Monoid α] {u : αˣ} {a : α}, ↑u * a = 1 → ↑u⁻¹ = a
-- Mathlib.Data.Multiset.Pi
Multiset.Pi.empty.congr_simp : ∀ {α : Type u_1} (δ : α → Sort u_3) (a : α) (a_1 : a ∈ 0), Multiset.Pi.empty δ a a_1 = Multiset.Pi.empty δ a a_1
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks.0.CategoryTheory.Limits.WidePullbackShape.mkCone.match_1.splitter : {J : Type u_1} →
  (motive : CategoryTheory.Limits.WidePullbackShape J → Sort u_2) →
    (j : CategoryTheory.Limits.WidePullbackShape J) → (Unit → motive none) → ((j : J) → motive (some j)) → motive j
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.ofNat_add_aleph0 : ∀ {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n + Cardinal.aleph0 = Cardinal.aleph0
-- Mathlib.Combinatorics.Hall.Basic
/-- The set of matchings for `t` when restricted to a `Finset` of `ι`.  -/
hallMatchingsOn : {ι : Type u} → {α : Type v} → (ι → Finset α) → (ι' : Finset ι) → Set (↥ι' → α)
-- Mathlib.Analysis.Convex.Topology
Real.closedBall_eq_segment : ∀ {r ε : ℝ}, 0 ≤ ε → Metric.closedBall r ε = segment ℝ (r - ε) (r + ε)
-- Mathlib.Topology.Connected.LocallyConnected
/-- If a space is locally connected, the topology of its connected components is discrete.  -/
instDiscreteTopologyConnectedComponentsOfLocallyConnectedSpace : ∀ {α : Type u} [inst : TopologicalSpace α] [LocallyConnectedSpace α], DiscreteTopology (ConnectedComponents α)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardCongr.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] {φ ψ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R} (e : φ = ψ),
  SheafOfModules.pushforwardCongr e = SheafOfModules.pushforwardCongr e
-- Mathlib.Algebra.GCDMonoid.Basic
/-- The GCD is normalized to itself.  -/
NormalizedGCDMonoid.normalize_gcd : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : NormalizedGCDMonoid α] (a b : α), normalize (gcd a b) = gcd a b
-- Mathlib.NumberTheory.Padics.PadicNumbers
Rat.surjective_padicValuation : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], Function.Surjective ⇑(Rat.padicValuation p)
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.mono_iff_injective : ∀ {A B : NonemptyFinLinOrd} (f : A ⟶ B),
  CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.QuadraticDiscriminant
discrim_neg : ∀ {R : Type u_1} [inst : Ring R] (a b c : R), discrim (-a) (-b) (-c) = discrim a b c
-- Mathlib.Logic.Basic
/-- A two-argument function applied to two `ite`s is a `ite` of that two-argument function
applied to each of the branches.  -/
apply_ite₂ : ∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (f : α → β → γ) (P : Prop) [inst : Decidable P] (a b : α) (c d : β),
  f (if P then a else b) (if P then c else d) = if P then f a c else f b d
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.mk.sizeOf_spec : ∀ (toGlueData : CategoryTheory.GlueData AlgebraicGeometry.Scheme)
  (f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.IsOpenImmersion (toGlueData.f i j)),
  sizeOf { toGlueData := toGlueData, f_open := f_open } = 1 + sizeOf toGlueData
-- Mathlib.RingTheory.Coalgebra.GroupLike
/-- The underlying element of a group-like element.  -/
GroupLike.val : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [inst_3 : Coalgebra R A] → GroupLike R A → A
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeUnopOfCone_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.coconeUnopOfCone c).ι = CategoryTheory.NatTrans.unop c.π
-- Mathlib.Probability.Independence.Process.Basic
/-- Stochastic processes $((X^s_t)_{t \in T_s})_{s \in S}$ are mutually independent if
for all $s_1, ..., s_n$ and all $t^{s_i}_1, ..., t^{s_i}_{p_i}$ the families
$(X^{s_1}_{t^{s_1}_1}, ..., X^{s_1}_{t^{s_1}_{p_1}}), ...,
(X^{s_n}_{t^{s_n}_1}, ..., X^{s_n}_{t^{s_n}_{p_n}})$ are mutually independent.

This version only requires a.e.-measurability.  -/
ProbabilityTheory.Kernel.iIndepFun.iIndepFun_process₀ : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {T : S → Type u_5} {𝓧 : (i : S) → T i → Type u_6}
  [inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)] {X : (i : S) → (j : T i) → Ω → 𝓧 i j},
  (∀ (i : S) (j : T i), AEMeasurable (X i j) (P.bind ⇑κ)) →
    (∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)),
        ProbabilityTheory.Kernel.iIndepFun (fun i ω j => X (↑i) (↑j) ω) κ P) →
      ProbabilityTheory.Kernel.iIndepFun (fun i ω j => X i j ω) κ P
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- The interval of reals `t` for which `exp (t * X)` is integrable.  -/
ProbabilityTheory.integrableExpSet : {Ω : Type u_1} → {m : MeasurableSpace Ω} → (Ω → ℝ) → MeasureTheory.Measure Ω → Set ℝ
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.UnusedSimpArgsInfo.mk : Array Bool → Lean.Elab.Tactic.UnusedSimpArgsInfo
-- Mathlib.Order.RelSeries
RelSeries.length_le_length_longestOf : ∀ {α : Type u_1} (r : SetRel α α) [inst : r.FiniteDimensional] (x : RelSeries r),
  x.length ≤ (RelSeries.longestOf r).length
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonWorkDoneProgressOptions.toJson : Lean.Lsp.WorkDoneProgressOptions → Lean.Json
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
/-- When `f : A ⟶ B` is a morphism in the category `CommRingCat`, this is the
differential map `B → KaehlerDifferential f`.  -/
CommRingCat.KaehlerDifferential.d : {A B : CommRingCat} → {f : A ⟶ B} → ↑B → ↑(CommRingCat.KaehlerDifferential f)
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) {n m : ℕ}
  (i i_1 : ℕ) (e_i : i = i_1) (hi : n + i = m), X.σ₀Iter i hi = X.σ₀Iter i_1 ⋯
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.id_comp : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B] (f : A →⋆* B),
  (StarMonoidHom.id B).comp f = f
-- Mathlib.CategoryTheory.Opposites
/-- Given a natural transformation `α : F ⟶ G`, for `F G : Cᵒᵖ ⥤ D`,
taking `op` of each component gives a natural transformation `G.rightOp ⟶ F.rightOp`.
 -/
CategoryTheory.NatTrans.rightOp : {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} → (F ⟶ G) → (G.rightOp ⟶ F.rightOp)
-- Mathlib.Algebra.Ring.Invertible
AddUnits.val_neg_mulLeft : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R), ↑(-x.mulLeft y) = y * x.neg
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.congr_eq_4 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (x : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b)))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  x = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit →
    (match x with
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) => h_3 l b
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) ≍
      h_4 ()
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.liminf_const_mul_of_nonpos_of_ne_bot : ∀ {α : Type u_3} {f : Filter α} {u : α → EReal} [f.NeBot] {c : EReal},
  c ≤ 0 → c ≠ ⊥ → Filter.liminf (fun x => c * u x) f = c * Filter.limsup u f