mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOn.div_const : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {s : Set E}
  {f : E → 𝕝}, AnalyticOn 𝕜 f s → ∀ {c : 𝕝}, AnalyticOn 𝕜 (fun x => f x / c) s
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau.mk.injEq : ∀ {matType : ℕ → ℕ → Type} [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType]
  (basic free : Array ℕ) (mat : matType basic.size free.size) (basic_1 free_1 : Array ℕ)
  (mat_1 : matType basic_1.size free_1.size),
  ({ basic := basic, free := free, mat := mat } = { basic := basic_1, free := free_1, mat := mat_1 }) =
    (basic = basic_1 ∧ free = free_1 ∧ mat ≍ mat_1)
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of the forward direction of `wellFounded_lift₂_iff`.

---

A relation is well founded iff its lift to a quotient is.  -/
WellFounded.of_quotient_lift₂ : ∀ {α : Type u_1} {x : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂},
  WellFounded (Quotient.lift₂ r H) → WellFounded r
-- Mathlib.NumberTheory.AbelSummation
tendsto_sum_mul_atTop_nhds_one_sub_integral : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜},
  (∀ t ∈ Set.Ici 0, DifferentiableAt ℝ f t) →
    MeasureTheory.LocallyIntegrableOn (deriv f) (Set.Ici 0) MeasureTheory.volume →
      ∀ {l : 𝕜},
        Filter.Tendsto (fun n => f ↑n * ∑ k ∈ Finset.Icc 0 n, c k) Filter.atTop (nhds l) →
          ∀ {g : ℝ → 𝕜},
            (fun t => deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k) =O[Filter.atTop] g →
              MeasureTheory.IntegrableAtFilter g Filter.atTop MeasureTheory.volume →
                Filter.Tendsto (fun n => ∑ k ∈ Finset.Icc 0 n, f ↑k * c k) Filter.atTop
                  (nhds (l - ∫ (t : ℝ) in Set.Ioi 0, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k))
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.algHom_ext'_iff : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommSemiring S] [inst_2 : Semiring T]
  [inst_3 : Algebra S R] [inst_4 : Algebra S T] {p : Polynomial R} {f g : AdjoinRoot p →ₐ[S] T},
  f = g ↔
    f.comp (AdjoinRoot.ofAlgHom S p) = g.comp (AdjoinRoot.ofAlgHom S p) ∧ f (AdjoinRoot.root p) = g (AdjoinRoot.root p)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.one? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.Data.Opposite
Opposite.instNonempty : ∀ {α : Sort u} [Nonempty α], Nonempty αᵒᵖ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k fallback : α},
  (Std.ExtDTreeMap.filterMap f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome).getD fallback
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_add_const_Ici : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x + a) ⁻¹' Set.Ici b = Set.Ici (b - a)
-- Mathlib.Tactic.Algebra.Basic
/-- Collect all scalar rings from scalar multiplications using a state monad for performance.

Note: The match in this definition should be kept up to date with the `Common.eval` function.
 -/
Mathlib.Tactic.Algebra.collectScalarRingsAux : Lean.Expr → StateT (List Lean.Expr) Lean.MetaM Unit
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.BinaryInput_invert_lhs : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} (input : aig.BinaryInput)
  (linv rinv : Bool),
  (input.invert linv rinv).lhs = { gate := input.lhs.gate, invert := linv ^^ input.lhs.invert, hgate := ⋯ }
-- Mathlib.NumberTheory.LSeries.Deriv
/-- The L-series of `f` is complex differentiable in its open half-plane of absolute
convergence.  -/
LSeries_differentiableOn : ∀ (f : ℕ → ℂ), DifferentiableOn ℂ (LSeries f) {s | LSeries.abscissaOfAbsConv f < ↑s.re}
-- Mathlib.Algebra.Order.Group.Synonym
toDual_eq_zero : ∀ {α : Type u_1} [inst : Zero α] {a : α}, OrderDual.toDual a = 0 ↔ a = 0
-- Mathlib.Tactic.CategoryTheory.Monoidal.Basic
/-- Normalize the both sides of an equality.  -/
Mathlib.Tactic.Monoidal.monoidalNf : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Algebra.Order.Group.End
RelIso.one_def : ∀ {α : Type u_1} {r : α → α → Prop}, 1 = RelIso.refl r
-- Mathlib.Algebra.Order.Interval.Basic
Interval.pure_zero : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Zero α], Interval.pure 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Complex.betaIntegral_symm : ∀ (u v : ℂ), v.betaIntegral u = u.betaIntegral v
-- Lean.Elab.DeclModifiers
/-- Filters attributes using `p`  -/
Lean.Elab.Modifiers.filterAttrs : Lean.Elab.Modifiers → (Lean.Elab.Attribute → Bool) → Lean.Elab.Modifiers
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `BitVec.toInt`.  -/
BitVec.reduceToInt : Lean.Meta.Simp.DSimproc
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde : ∀ {R : CommRingCat} (M : ModuleCat ↑R), SheafOfModules.IsQuasicoherent (AlgebraicGeometry.tilde M)
-- Mathlib.Data.ZMod.Basic
/-- The map from `ZMod n` induced by `f : ℤ →+ A` that maps `n` to `0`.  -/
ZMod.lift : (n : ℕ) → {A : Type u_2} → [inst : AddGroup A] → { f // f ↑n = 0 } ≃ (ZMod n →+ A)
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder : ∀ {σ : Type u_1} (w : σ → ℕ) {R : Type u_4} {ι : Type u_5} [inst : CommRing R] (d : σ →₀ ℕ) (s : Finset ι)
  (f : MvPowerSeries σ R) (g : ι → MvPowerSeries σ R),
  (∀ i ∈ s, ↑((Finsupp.weight w) d) < MvPowerSeries.weightedOrder w (g i)) →
    (MvPowerSeries.coeff d) (f * ∏ i ∈ s, (1 - g i)) = (MvPowerSeries.coeff d) f
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.mapPower_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β : Type t}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] [inst_2 : CategoryTheory.Limits.HasProductsOfShape β C]
  (f : α → β), (U.mapPower f).f = fun i => i ∘ f
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.pellZd_succ : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.pellZd a1 (n + 1) = Pell.pellZd a1 n * { re := ↑a, im := 1 }
-- Mathlib.Order.Filter.Pointwise
Filter.div.instNeBot : ∀ {α : Type u_2} [inst : Div α] {f g : Filter α} [f.NeBot] [g.NeBot], (f / g).NeBot
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_inv_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (n : SimplexCategoryᵒᵖ) (i : CategoryTheory.ToType (Opposite.unop n)),
  CategoryTheory.CategoryStruct.comp (U.cechIsoCechNerveApp hT n).inv (U.powerπ i) =
    CategoryTheory.Limits.WidePullback.π (fun x => (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U) i
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.changeDiag_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.LimitPresentation J X) {F : CategoryTheory.Functor J C} (e : F ≅ P.diag),
  (P.changeDiag e).π = CategoryTheory.CategoryStruct.comp P.π e.inv
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The limit of `autGaloisSystem`.  -/
CategoryTheory.PreGaloisCategory.AutGalois : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [CategoryTheory.GaloisCategory C] → CategoryTheory.Functor C FintypeCat → Type (max u₁ u₂)
-- Mathlib.Topology.Algebra.Constructions
Topology.IsEmbedding.addUnits_map : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : TopologicalSpace N]
  [inst_3 : AddMonoid N] {f : M →+ N}, Topology.IsEmbedding ⇑f → Topology.IsEmbedding ⇑(AddUnits.map f)
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.expand_smul : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (a : R) (φ : PowerSeries R),
  (PowerSeries.expand p hp) (a • φ) = a • (PowerSeries.expand p hp) φ
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.mem_nhds_zero : ∀ {R : Type u} [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀]
  {s : Set R}, s ∈ nhds 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
-- Lean.Elab.Match
/-- Helper function for "saving" the user name associated with `mvarId` (if it is not "anonymous") before visiting `x`
The auto generalization feature will uses synthetic holes to preserve the name of the free variable included during generalization.
For example, if we are generalizing a free variable `bla`, we add the synthetic hole `?bla` for the pattern. We use synthetic hole
because we don't know whether `?bla` will become an inaccessible pattern or not.
The `withMVar` method makes sure we don't "lose" this name when `isDefEq` perform assignments of the form `?bla := ?m` where `?m` has no user name.
This can happen, for example, when the user provides a `_` pattern, or for implicit fields.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.withMVar : {α : Type} → Lean.MVarId → Lean.Elab.Term.ToDepElimPattern.M α → Lean.Elab.Term.ToDepElimPattern.M α
-- Mathlib.Algebra.RingQuot
RingQuot.liftAlgHom_def : ∀ (S : Type u_1) [inst : CommSemiring S] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra S A] {B : Type u_3}
  [inst_3 : Semiring B] [inst_4 : Algebra S B] {s : A → A → Prop},
  RingQuot.liftAlgHom S =
    { toFun := fun f' => RingQuot.preLiftAlgHom S ⋯, invFun := fun F => ⟨F.comp (RingQuot.mkAlgHom S s), ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.fold_filter : ∀ {α β δ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {f : β → Bool} {g : δ → β → δ}
  {init : δ} {it : Std.IterM m β},
  Std.IterM.fold g init (Std.IterM.filter f it) = Std.IterM.fold (fun d b => if f b = true then g d b else d) init it
-- Mathlib.Computability.TuringMachine.Computable
/-- A TM2 machine has finitely many stacks.  -/
Turing.FinTM2.kFin : (self : Turing.FinTM2) → Fintype self.K
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- Given a family of homogeneous elements `f` of positive degree that spans the irrelevant ideal,
`Spec (A_f)₀ ⟶ Proj A` forms an affine open cover of `Proj A`.  -/
AlgebraicGeometry.Proj.affineOpenCoverOfIrrelevantLESpan : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              {ι : Type u_2} →
                (f : ι → A) →
                  {m : ι → ℕ} →
                    (∀ (i : ι), f i ∈ 𝒜 (m i)) →
                      (∀ (i : ι), 0 < m i) →
                        (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f) →
                          (AlgebraicGeometry.Proj 𝒜).AffineOpenCover
-- Mathlib.Logic.Equiv.Defs
Equiv.permCongr_trans : ∀ {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p p' : Equiv.Perm α'),
  Equiv.trans (e.permCongr p) (e.permCongr p') = e.permCongr (Equiv.trans p p')
-- Init.Grind.Norm
Lean.Grind.false_imp_eq : ∀ (p : Prop), (False → p) = True
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the third quadrant. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open third quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp (B * ‖z‖ ^ c)` on the open third quadrant
  for some `c < 2`;
* `‖f z‖` is bounded from above by a constant `C` on the boundary of the third quadrant.

Then `‖f z‖` is bounded from above by the same constant on the closed third quadrant.  -/
PhragmenLindelof.quadrant_III : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
  DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Iio 0) →
    (∃ c < 2,
        ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Iio 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
      (∀ x ≤ 0, ‖f ↑x‖ ≤ C) → (∀ x ≤ 0, ‖f (↑x * Complex.I)‖ ≤ C) → z.re ≤ 0 → z.im ≤ 0 → ‖f z‖ ≤ C
-- Init.Data.Option.Lemmas
Option.some_eq_dite_none_left : ∀ {β : Type u_1} {a : β} {p : Prop} {x : Decidable p} {b : ¬p → Option β},
  (some a = if h : p then none else b h) ↔ ∃ (h : ¬p), some a = b h
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addPrehaar.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (K₀ U : Set G) (K : TopologicalSpace.Compacts G),
  MeasureTheory.Measure.haar.addPrehaar K₀ U K =
    ↑(MeasureTheory.Measure.haar.addIndex (↑K) U) / ↑(MeasureTheory.Measure.haar.addIndex K₀ U)
-- Mathlib.CategoryTheory.Localization.Trifunctor
CategoryTheory.Localization.natTrans₃_ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13}
  [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} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃]
  [inst_6 : CategoryTheory.Category.{v_13, u_13} E] (L₁ : CategoryTheory.Functor C₁ D₁)
  (L₂ : CategoryTheory.Functor C₂ D₂) (L₃ : CategoryTheory.Functor C₃ D₃) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) (W₃ : CategoryTheory.MorphismProperty C₃) [L₁.IsLocalization W₁]
  [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities]
  {F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))} {τ τ' : F₁' ⟶ F₂'},
  (∀ (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
      ((τ.app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃) = ((τ'.app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃)) →
    τ = τ'
-- Mathlib.NumberTheory.LSeries.Convolution
/-- Dirichlet convolution of two sequences.

We define this in terms of the already existing definition for arithmetic functions.  -/
LSeries.convolution : {R : Type u_1} → [Semiring R] → (ℕ → R) → (ℕ → R) → ℕ → R
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.dSmooth_id' : ∀ {X : Type u_1} [inst : DiffeologicalSpace X], Diffeology.DSmooth fun x => x
-- Mathlib.ModelTheory.Syntax
/-- The universal quantifier over bounded formulas.  -/
FirstOrder.Language.BoundedFormula.all : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α (n + 1) → L.BoundedFormula α n
-- Mathlib.Algebra.Opposites
AddOpposite.opEquiv_apply : ∀ {α : Type u_1}, ⇑AddOpposite.opEquiv = AddOpposite.op
-- Lean.Meta.ACLt
/-- An AC-compatible ordering.

Recall that an AC-compatible ordering if it is monotonic, well-founded, and total.
Both KBO and LPO are AC-compatible. KBO is faster, but we do not cache the weight of
each expression in Lean 4. Even if we did, we would need to have a weight where implicit instance arguments are ignored.
So, we use a LPO-like term ordering.

Remark: this method is used to implement ordered rewriting. We ignore implicit instance
arguments to address an issue reported at issue #972.

Remark: the order is not really total on terms since
 - We instance implicit arguments.
 - We ignore metadata.
 - We ignore universe parameters at constants.
 -/
Lean.Meta.acLt : Lean.Expr → Lean.Expr → optParam Lean.Meta.ACLt.ReduceMode Lean.Meta.ACLt.ReduceMode.none → Lean.MetaM Bool
-- Init.Data.Option.Lemmas
/-- We simplify away `isEqSome` in terms of `==`.  -/
Option.isEqSome_eq_beq_some : ∀ {α : Type u_1} [inst : BEq α] {y : α} {o : Option α}, o.isEqSome y = (o == some y)
-- Mathlib.CategoryTheory.Action.Continuous
/-- The "restriction" functor along a monoid homomorphism `f : G →* H`,
taking actions of `H` to actions of `G`. This is the analogue of
`Action.res` in the continuous setting.  -/
ContAction.res : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
              {G : Type u_4} →
                [inst_4 : Monoid G] →
                  [inst_5 : TopologicalSpace G] →
                    {H : Type u_5} →
                      [inst_6 : Monoid H] →
                        [inst_7 : TopologicalSpace H] →
                          (G →ₜ* H) → CategoryTheory.Functor (ContAction V H) (ContAction V G)
-- Lean.Data.NameTrie
_private.Lean.Data.NameTrie.0.Lean.toKey.loop : Lean.Name → List Lean.NamePart → List Lean.NamePart
-- Mathlib.Analysis.Matrix.Order
/-- **Alias** of the forward direction of `Matrix.nonneg_iff_posSemidef`. -/
Matrix.LE.le.posSemidef : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] {A : Matrix n n 𝕜}, 0 ≤ A → A.PosSemidef
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeGPFree_singleton : ∀ {α : Type u_2} [inst : Monoid α] (a : α), ThreeGPFree {a}
-- Std.Do.PostCond
Std.Do.ExceptConds.and.eq_def : ∀ {ps : Std.Do.PostShape} (x y : Std.Do.ExceptConds ps),
  (x ∧ₑ y) =
    match ps, x, y with
    | Std.Do.PostShape.pure, x, y => PUnit.unit
    | Std.Do.PostShape.arg σ ps, x, y => x ∧ₑ y
    | Std.Do.PostShape.except ε a, x, y => (fun e => spred(x.1 e ∧ y.1 e), x.2 ∧ₑ y.2)
-- Mathlib.Logic.Function.FromTypes
Function.FromTypes.const_succ : ∀ {n : ℕ} (p : Fin (n + 1) → Type u) {τ : Type u} (t : τ),
  Function.FromTypes.const p t = fun x => Function.FromTypes.const (Matrix.vecTail p) t
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.zero' : Turing.ToPartrec.Code
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.invtSubmodule_reflection_of_invtSubmodule_coreflection : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  ∀ q ∈ Module.End.invtSubmodule ↑(P.coreflection i),
    Submodule.map (↑P.toPerfPair.symm) q.dualAnnihilator ∈ Module.End.invtSubmodule ↑(P.reflection i)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.mapZeroObject_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroObject D]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.PreservesZeroMorphisms], F.mapZeroObject.hom = 0
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.toGermAddMonoidHom_apply : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : AddMonoid γ] [inst_3 : ContinuousAdd γ] (f : α →ₘ[μ] γ),
  MeasureTheory.AEEqFun.toGermAddMonoidHom f = f.toGerm
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.some_getEntryGT_eq_getEntryGT? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (t : Std.DTreeMap.Internal.Impl α β)
  {ho : t.Ordered} {he : ∃ a ∈ t, compare a k = Ordering.gt},
  some (Std.DTreeMap.Internal.Impl.getEntryGT k t ho he) = Std.DTreeMap.Internal.Impl.getEntryGT? k t
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_sup : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N N₂ : LieSubmodule R L M},
  LieSubmodule.map f (N ⊔ N₂) = LieSubmodule.map f N ⊔ LieSubmodule.map f N₂
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
/-- `HasFibers` instance for `∫ᶜ F`, where the fiber over `S` is `F.obj ⟨op S⟩`.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.instHasFibersForget : {𝒮 : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒮] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) →
      HasFibers (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F)
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.instWEqualsLocallyBijectiveAffineEtaleTopology : ∀ {S : AlgebraicGeometry.Scheme} {A : Type u'} [inst : CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1}
  {CD : A → Type u} [inst_1 : (X Y : A) → FunLike (FA X Y) (CD X) (CD Y)]
  [inst_2 : CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
  [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A]
  [(CategoryTheory.forget A).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)],
  (AlgebraicGeometry.Scheme.AffineEtale.topology S).WEqualsLocallyBijective A
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.coe_set_mk : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Subsemigroup M} (h_one : 1 ∈ s.carrier),
  ↑{ toSubsemigroup := s, one_mem' := h_one } = ↑s
-- Mathlib.Data.Set.Card
Set.finite_of_ncard_ne_zero : ∀ {α : Type u_1} {s : Set α}, s.ncard ≠ 0 → s.Finite
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `Stained` is the type of the stained locations: it can be
* a `Name` (typically of associated to the `FVarId` of a local declaration);
* the goal (`⊢`);
* the "wildcard" -- all the declaration in context (`*`).
 -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.Stained : Type
-- Mathlib.Analysis.Normed.Group.Constructions
Multiplicative.normedCommGroup : {E : Type u_2} → [NormedAddCommGroup E] → NormedCommGroup (Multiplicative E)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The composition of morphisms of short complexes.  -/
CategoryTheory.ShortComplex.Hom.comp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} → S₁.Hom S₂ → S₂.Hom S₃ → S₁.Hom S₃
-- Mathlib.Topology.Homotopy.HSpaces
IsTopologicalGroup.hSpace.eq_1 : ∀ (G : Type u) [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G],
  IsTopologicalGroup.hSpace G = IsTopologicalGroup.toHSpace G
-- Mathlib.Combinatorics.Digraph.Basic
/-- We define `Gᶜ` to be the `Digraph V` such that no two adjacent vertices in `G`
are adjacent in the complement, and every nonadjacent pair of vertices is adjacent.  -/
Digraph.instCompl : {V : Type u_2} → Compl (Digraph V)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_eq_get!_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {a : α}, t.get! a = (t.get? a).get!
-- Mathlib.MeasureTheory.Integral.Marginal
/-- Peel off a single integral from a `lmarginal` integral at the beginning (compare with
`lmarginal_erase'`, which peels off an integral at the end).  -/
MeasureTheory.lmarginal_erase : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] {s : Finset δ} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] (f : ((i : δ) → X i) → ENNReal),
  Measurable f →
    ∀ {i : δ},
      i ∈ s →
        ∀ (x : (i : δ) → X i), (∫⋯∫⁻_s, f ∂μ) x = ∫⁻ (xᵢ : X i), (∫⋯∫⁻_s.erase i, f ∂μ) (Function.update x i xᵢ) ∂μ i