mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Defs
NonAssocSemiring.toNonUnitalNonAssocSemiring : {α : Type u} → [self : NonAssocSemiring α] → NonUnitalNonAssocSemiring α
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `𝔖 : Set (Set α)` is nonempty and directed and `𝓑` is a filter basis of `𝓤 β`, then the
uniformity of `α →ᵤ[𝔖] β` admits the family `{(f, g) | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and
`V ∈ 𝓑` as a filter basis.  -/
UniformOnFun.hasBasis_uniformity_of_basis : ∀ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [inst : UniformSpace β] (𝔖 : Set (Set α)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      ∀ {p : ι → Prop} {s : ι → Set (β × β)},
        (uniformity β).HasBasis p s →
          (uniformity (UniformOnFun α β 𝔖)).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
            UniformOnFun.gen 𝔖 Si.1 (s Si.2)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
Seminorm.isBounded_const : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [inst : SeminormedRing 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : SeminormedRing 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] (ι' : Type u_11) [Nonempty ι']
  {p : ι → Seminorm 𝕜 E} {q : Seminorm 𝕜₂ F} (f : E →ₛₗ[σ₁₂] F),
  Seminorm.IsBounded p (fun x => q) f ↔ ∃ s C, q.comp f ≤ C • s.sup p
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (self : F.DescentDataAsCoalgebra f) (i : ι),
  CategoryTheory.CategoryStruct.comp (self.hom i i) ((F.map (f i).op.toLoc).adj.counit.toNatTrans.app (self.obj i)) =
    CategoryTheory.CategoryStruct.id (self.obj i)
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.sound : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp},
  t₁.Equiv t₂ → Std.ExtDTreeMap.mk t₁ = Std.ExtDTreeMap.mk t₂
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_div_cancel_left' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a b : G₀}, a ≠ 0 → a / b / a = b⁻¹
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_comap_eq_self : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {H : Subgroup N},
  H ≤ f.range → Subgroup.map f (Subgroup.comap f H) = H
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.neg_Ioo : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  -Set.Ioo a b = Set.Ioo (-b) (-a)
-- Mathlib.Data.Real.Embedding
Archimedean.embedRealFun_zero : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M]
  [ZeroLEOneClass M] [NeZero 1] [Archimedean M], Archimedean.embedRealFun 0 = 0
-- Mathlib.LinearAlgebra.Matrix.WithConv
/-- All matrices are intrinsically self-adjoint if they are convolutively idempotent.  -/
Matrix.WithConv.IsIdempotentElem.isSelfAdjoint : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Semiring α] [IsLeftCancelMulZero α] [inst_2 : StarRing α]
  {f : WithConv (Matrix m n α)}, IsIdempotentElem f → IsSelfAdjoint f
-- Mathlib.Algebra.MvPolynomial.Eval
/-- Evaluate a polynomial `p` given a valuation `f` of all the variables  -/
MvPolynomial.eval : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → (σ → R) → MvPolynomial σ R →+* R
-- Mathlib.Order.RelIso.Basic
isEmptyElim.congr_simp : ∀ {α : Sort u} [inst : IsEmpty α] {p : α → Sort v} (a : α), isEmptyElim a = isEmptyElim a
-- Mathlib.Data.Finite.Sum
Finite.psum_right : ∀ {α : Sort u_3} {β : Sort u_4} [Finite (α ⊕' β)], Finite β
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α}, (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).size ≤ m.size + l.length
-- Mathlib.Algebra.Ring.Equiv
/-- The opposite of a direct product is isomorphic to the direct product of the opposites
as rings.  -/
RingEquiv.piMulOpposite : {ι : Type u_7} →
  (S : ι → Type u_8) → [inst : (i : ι) → NonUnitalNonAssocSemiring (S i)] → ((i : ι) → S i)ᵐᵒᵖ ≃+* ((i : ι) → (S i)ᵐᵒᵖ)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Ico_eq_integral_Ioc : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x y : X} [MeasureTheory.NullSingletonClass μ],
  ∫ (t : X) in Set.Ico x y, f t ∂μ = ∫ (t : X) in Set.Ioc x y, f t ∂μ
-- Lean.Parser.Syntax
Lean.Parser.Command.syntax.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Tactic.Algebra.Basic
/-- A Field instance on `A`, if available.  -/
Mathlib.Tactic.Algebra.Cache.field : {u : Lean.Level} →
  {A : Q(Type u)} → {sA : Q(CommSemiring «$A»)} → Mathlib.Tactic.Algebra.Cache sA → Option Q(Field «$A»)
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
intervalIntegral.continuousWithinAt_primitive : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b₀ b₁ b₂ : ℝ} {μ : MeasureTheory.Measure ℝ}
  {f : ℝ → E},
  μ {b₀} = 0 →
    IntervalIntegrable f μ (min a b₁) (max a b₂) →
      ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Set.Icc b₁ b₂) b₀
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.instRespectsIsoStrongAnodyneExtensions : SSet.strongAnodyneExtensions.RespectsIso
-- Batteries.Data.List.Lemmas
List.idxOfNth_le_length : ∀ {α : Type u_1} {x : α} {n : ℕ} [inst : BEq α] {xs : List α}, List.idxOfNth x xs n ≤ xs.length
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.map_normalClosure_le : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (s : Set G) (f : G →+ N),
  AddSubgroup.map f (AddSubgroup.normalClosure s) ≤ AddSubgroup.normalClosure (⇑f '' s)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.isLoopAt_eqOn : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H ≤ G → Set.EqOn H.IsLoopAt G.IsLoopAt H.edgeSet
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprRaw_mathlib.toExpr : String.Pos.Raw → Lean.Expr
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableLocallyUniformly.hasSumLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β], SummableLocallyUniformly f → HasSumLocallyUniformly f fun x => ∑' (i : ι), f i x
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncLTAppTruncLTι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (X : C) (n : ℤ),
  CategoryTheory.IsIso ((t.truncLT n).map ((t.truncLTι n).app X))
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.periods.congr_simp : ∀ {ι : Type u_3} {s s_1 : Set (ι → ℕ)} (e_s : s = s_1) (hs : IsProperLinearSet s) (a a_1 : ι → ℕ),
  a = a_1 → IsProperLinearSet.periods✝ hs a = IsProperLinearSet.periods✝ ⋯ a_1
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.coe_symm_toEquiv : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  ⇑h.symm = ⇑h.symm
-- Mathlib.Data.Int.Init
/-- **Alias** of `Int.natAbs_pow_two`. -/
Int.natAbs_sq : ∀ (a : ℤ), ↑a.natAbs ^ 2 = a ^ 2
-- Mathlib.Topology.Compactness.Compact
/-- A filter is disjoint from the cocompact filter if and only if it contains a compact set.  -/
Filter.disjoint_cocompact_left : ∀ {X : Type u} [inst : TopologicalSpace X] (f : Filter X), Disjoint (Filter.cocompact X) f ↔ ∃ K ∈ f, IsCompact K
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.coeff_modMonomial_of_not_le : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s' s : σ →₀ ℕ} (x : MvPolynomial σ R),
  ¬s ≤ s' → MvPolynomial.coeff s' (x.modMonomial s) = MvPolynomial.coeff s' x
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- `G.neighborFinset v` is the `Finset` version of `G.neighborSet v` in case `G` is
locally finite at `v`.  -/
SimpleGraph.neighborFinset : {V : Type u_1} → (G : SimpleGraph V) → (v : V) → [Fintype ↑(G.neighborSet v)] → Finset V
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.coe_sup' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : SemilatticeSup β]
  [inst_3 : ContinuousSup β] {ι : Type u_3} {s : Finset ι} (H : s.Nonempty) (f : ι → C(α, β)),
  ⇑(s.sup' H f) = s.sup' H fun i => ⇑(f i)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
LipschitzWith.memLp_comp_iff_of_antilipschitz : ∀ {p : ENNReal} {α : Type u_6} {E : Type u_7} {F : Type u_8} {K K' : NNReal} [inst : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] {f : α → E} {g : E → F},
  LipschitzWith K g → AntilipschitzWith K' g → g 0 = 0 → (MeasureTheory.MemLp (g ∘ f) p μ ↔ MeasureTheory.MemLp f p μ)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLE_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} {f : A ⟶ B} [inst_1 : CategoryTheory.Mono f]
  {X : CategoryTheory.Subobject B} (h : CategoryTheory.Subobject.mk f ≤ X),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h) X.arrow = f
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.instReprRCasesPatt.repr : Lean.Elab.Tactic.RCases.RCasesPatt → ℕ → Std.Format
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.of_mem_of_add_mem_left : ∀ {R : Type u_1} {M : Type u_2} [inst : DivisionRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M},
  F ≤ C → (∀ {x y : M}, x ∈ C → y ∈ C → x + y ∈ F → x ∈ F) → F.IsFaceOf C
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α} {v : β},
  a ∈ t.insertIfNew k v ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Define a `StrongNormalizedGCDMonoid` structure on a monoid just from
the existence of a `gcd`.  -/
strongNormalizedGCDMonoidOfExistsGCD : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [StrongNormalizationMonoid α] →
        [DecidableEq α] → (∀ (a b : α), ∃ c, ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c) → StrongNormalizedGCDMonoid α
-- Aesop.Script.GoalWithMVars
Aesop.instInhabitedGoalWithMVars.default : Aesop.GoalWithMVars
-- Init.Data.Array.Basic
/-- Swaps two elements of an array, returning the array unchanged if either index is out of bounds. The
modification is performed in-place when the reference to the array is unique.

Examples:
* `#["red", "green", "blue", "brown"].swapIfInBounds 0 3 = #["brown", "green", "blue", "red"]`
* `#["red", "green", "blue", "brown"].swapIfInBounds 0 2 = #["blue", "green", "red", "brown"]`
* `#["red", "green", "blue", "brown"].swapIfInBounds 1 2 = #["red", "blue", "green", "brown"]`
* `#["red", "green", "blue", "brown"].swapIfInBounds 0 4 = #["red", "green", "blue", "brown"]`
* `#["red", "green", "blue", "brown"].swapIfInBounds 9 2 = #["red", "green", "blue", "brown"]`
 -/
Array.swapIfInBounds : {α : Type u} → Array α → ℕ → ℕ → Array α
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.coe_vadd : ∀ {α : Type u_4} {M : Type u_5} [inst : AddZeroClass M] [inst_1 : VAdd α M] [inst_2 : VAddAssocClass α M M]
  (c : AddCon M) (a : α) (x : M), ↑(a +ᵥ x) = a +ᵥ ↑x
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.toSlice : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String}, p.Splits t₁ t₂ → p.toSlice.Splits t₁ t₂
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- A copy of a type with metric given by `dist x y = (dist x.val y.val) ^ α`.

This is defined as a one-field structure.  -/
Metric.Snowflaking : Type u_1 → (α : ℝ) → 0 < α → α ≤ 1 → Type u_1
-- Lean.MetavarContext
/-- Similar to `localDeclDependsOn`, but `x` can be a free variable or an unassigned metavariable.  -/
Lean.localDeclDependsOn' : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.LocalDecl → Lean.Expr → optParam Bool true → m Bool
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.VAddInvariantMeasure.measure_preimage_vadd : ∀ {M : Type u_1} {α : Type u_2} {inst : VAdd M α} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [self : MeasureTheory.VAddInvariantMeasure M α μ] (c : M) ⦃s : Set α⦄,
  MeasurableSet s → μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s
-- Mathlib.Topology.MetricSpace.DilationEquiv
/-- Reinterpret a `DilationEquiv` as a homeomorphism.  -/
DilationEquiv.toHomeomorph : {X : Type u_1} → {Y : Type u_2} → [inst : PseudoEMetricSpace X] → [inst_1 : PseudoEMetricSpace Y] → X ≃ᵈ Y → X ≃ₜ Y
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is any function and `g` is analytic without zero at `z₀`, then `f` is meromorphic in
normal form at `z₀` iff `g • f` is meromorphic in normal form at `z₀`.  -/
meromorphicNFAt_smul_iff_right_of_analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {g : 𝕜 → 𝕜} {x : 𝕜},
  AnalyticAt 𝕜 g x → g x ≠ 0 → (MeromorphicNFAt (g • f) x ↔ MeromorphicNFAt f x)
-- Mathlib.Geometry.Manifold.Immersion
/-- The identity map is an immersion.  -/
Manifold.IsImmersion.id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_7} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_11}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M],
  Manifold.IsImmersion I I n id
-- Mathlib.Order.Hom.Bounded
BotHom.coe_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : SemilatticeSup β] [inst_2 : OrderBot β] (f g : BotHom α β),
  ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
-- Init.Data.Iterators.Lemmas.Combinators.Take
Std.Iter.toTake.congr_simp : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] (it it_1 : Std.Iter β),
  it = it_1 → it.toTake = it_1.toTake
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Prototile.mk : {G : Type u_1} →
  {X : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        (carrier : Set X) → Subgroup ↥(MulAction.stabilizer G carrier) → DiscreteTiling.Prototile G X
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.norm_qParam : ∀ (h : ℝ) (z : ℂ), ‖Function.Periodic.qParam h z‖ = Real.exp (-2 * Real.pi * z.im / h)
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.find? : Lean.Meta.FVarSubst → Lean.FVarId → Option Lean.Expr
-- Mathlib.Data.TypeVec
/-- projection for a repeat vector  -/
TypeVec.ofRepeat : {α : Type u_1} → {n : ℕ} → {i : Fin2 n} → TypeVec.repeat n α i → α
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
exists_dist_le_le : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {x z : E} {δ ε : ℝ},
  0 ≤ δ → 0 ≤ ε → dist x z ≤ ε + δ → ∃ y, dist x y ≤ δ ∧ dist y z ≤ ε
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_image_isBase_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {M : Matroid α} {hf : Set.InjOn f M.E} {B : Set α},
  B ⊆ M.E → ((M.map f hf).IsBase (f '' B) ↔ M.IsBase B)
-- Mathlib.Data.Sigma.Lex
Sigma.instTrichotomousLex : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [Std.Trichotomous r]
  [∀ (i : ι), Std.Trichotomous (s i)], Std.Trichotomous (Sigma.Lex r s)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.coeff_mapRingHom : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (f : R →+* S) (x : MonoidAlgebra R M) (m : M), ((MonoidAlgebra.mapRingHom M f) x).coeff m = f (x.coeff m)
-- Init.Data.SInt.Bitwise
Int8.toBitVec_shiftRight : ∀ (a b : Int8), (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 8)
-- Std.Data.HashMap.Lemmas
/-- Simpler variant of `getElem?_filterMap` when `LawfulBEq` is available.  -/
Std.HashMap.getElem?_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α]
  {f : α → β → Option γ} {k : α}, (Std.HashMap.filterMap f m)[k]? = m[k]?.bind fun x => f k x
-- Mathlib.Data.QPF.Univariate.Basic
_private.Mathlib.Data.QPF.Univariate.Basic.0.QPF.Cofix.bisim_aux : ∀ {F : Type u → Type u} [q : QPF F] (r : QPF.Cofix F → QPF.Cofix F → Prop),
  (∀ (x : QPF.Cofix F), r x x) →
    (∀ (x y : QPF.Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest) → ∀ (x y : QPF.Cofix F), r x y → x = y
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.opNNNorm_flip : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G), ‖f.flip‖₊ = ‖f‖₊
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam.eq_1 : ∀ {X : Type u_2} [inst : PseudoEMetricSpace X] (s : Set X), Metric.ediam s = ⨆ x ∈ s, ⨆ y ∈ s, edist x y
-- Mathlib.CategoryTheory.Grothendieck
/-- Auxiliary definition for `grothendieckTypeToCat`, to speed up elaboration.  -/
CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (G : CategoryTheory.Functor C (Type w)) →
      CategoryTheory.Functor (CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) G.Elements
-- Mathlib.Algebra.Homology.Localization
instQFactorsThroughHomotopyIntUp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasBinaryBiproducts C] [inst_3 : CategoryTheory.CategoryWithHomology C],
  (ComplexShape.up ℤ).QFactorsThroughHomotopy C
-- Mathlib.Topology.MetricSpace.Gluing
Metric.glueDist.eq_4 : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
  (x_2 : Y) (y : X), Metric.glueDist Φ Ψ ε (Sum.inr x_2) (Sum.inl y) = (⨅ p, dist y (Φ p) + dist x_2 (Ψ p)) + ε
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.nonunits_le_nonunits : ∀ {K : Type u} [inst : Field K] {A B : ValuationSubring K}, B.nonunits ≤ A.nonunits ↔ A ≤ B
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_le_csSup' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s t : Set α}, BddAbove t → s ⊆ t → sSup s ≤ sSup t
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp_id : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (f : α →ₘ[μ] β), MeasureTheory.AEEqFun.comp id ⋯ f = f
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.instCoeTypeForall_1 : {α : Type u} → Coe (Type v) (α → Type v)
-- Mathlib.Order.Interval.Set.ProjIcc
StrictMono.strictMonoOn_IicExtend : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {b : α} {f : ↑(Set.Iic b) → β},
  StrictMono f → StrictMonoOn (Set.IicExtend f) (Set.Iic b)
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.alternatingWord.eq_1 : ∀ {B : Type u_1} (i i' : B), CoxeterSystem.alternatingWord i i' 0 = []
-- Mathlib.Algebra.Quaternion
/-- The additive equivalence between a quaternion algebra over `R` and `Fin 4 → R`.  -/
QuaternionAlgebra.addEquivTuple : {R : Type u_3} → [inst : Add R] → (c₁ c₂ c₃ : R) → QuaternionAlgebra R c₁ c₂ c₃ ≃+ (Fin 4 → R)
-- Init.Data.Vector.Lex
/-- `xs` is lexicographically less than `ys` if
there exists an index `i` such that
- for all `j < i`, `l₁[j] == l₂[j]` and
- `l₁[i] < l₂[i]`
 -/
Vector.lex_eq_true_iff_exists : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] (lt : α → α → Bool) {xs ys : Vector α n},
  xs.lex ys lt = true ↔ ∃ i, ∃ (h : i < n), (∀ (j : ℕ) (hj : j < i), (xs[j] == ys[j]) = true) ∧ lt xs[i] ys[i] = true
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
/-- The torsion tensor of an unbundled covariant derivative on `TM`.  -/
IsCovariantDerivativeOn.torsion : {𝕜 : 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] →
                    [inst_5 : ChartedSpace H M] →
                      [inst_6 : IsManifold I 2 M] →
                        [CompleteSpace E] →
                          {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x} →
                            [CompleteSpace 𝕜] →
                              [FiniteDimensional 𝕜 E] →
                                IsCovariantDerivativeOn E cov →
                                  (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] TangentSpace I x
-- Mathlib.GroupTheory.CosetCover
AddSubgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {s : Finset ι} {H : AddSubgroup G} {g : ι → G},
  ⋃ i ∈ s, g i +ᵥ ↑H = Set.univ → H.index = s.card → (↑s).PairwiseDisjoint fun x => g x +ᵥ ↑H
-- Mathlib.Data.List.Nodup
Function.Injective.nodup : ∀ {α : Type u} {l : List α}, Function.Injective l.get → l.Nodup
-- Lean.Data.Json.Basic
Lean.Json.Structured.obj.sizeOf_spec : ∀ (kvPairs : Std.TreeMap.Raw String Lean.Json compare), sizeOf (Lean.Json.Structured.obj kvPairs) = 1 + sizeOf kvPairs
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.HasDetPlusMinusOne.mk : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R]
  {Γ : Subgroup (GL n R)},
  (∀ {g : GL n R}, g ∈ Γ → Matrix.GeneralLinearGroup.det g = 1 ∨ Matrix.GeneralLinearGroup.det g = -1) →
    Γ.HasDetPlusMinusOne
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.copy_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)) (f' : X → Y)
  (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.mk : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              Algebra.Presentation R S ι σ →
                (map : σ → ι) → Function.Injective map → Algebra.PreSubmersivePresentation R S ι σ
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.lintegral_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal}
  {μ : MeasureTheory.Measure β} {a : α}, ∫⁻ (x : β), f x ∂(ProbabilityTheory.Kernel.const α μ) a = ∫⁻ (x : β), f x ∂μ
-- Init.Data.List.Count
List.count_cons : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {l : List α},
  List.count a (b :: l) = List.count a l + if (b == a) = true then 1 else 0