mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.StrictPositivity
Units.isStrictlyPositive_iff : ∀ {A : Type u_1} [inst : LE A] [inst_1 : Monoid A] [inst_2 : Zero A] {a : Aˣ}, IsStrictlyPositive ↑a ↔ 0 ≤ ↑a
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_char_add : ∀ {c : Char} {p : String.Pos.Raw}, (c + p).byteIdx = c.utf8Size + p.byteIdx
-- Mathlib.Logic.Basic
Exists₃.imp : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {p q : (a : α) → (b : β a) → γ a b → Prop},
  (∀ (a : α) (b : β a) (c : γ a b), p a b c → q a b c) → (∃ a b c, p a b c) → ∃ a b c, q a b c
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.transport_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c), (x.transport t).fiber = (F.map t).toFunctor.obj x.fiber
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.liftCochain_v_snd_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m)
  (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂) {Z : C} (h_1 : G.X p₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v p₂ p₂ ⋯) h_1) =
    CategoryTheory.CategoryStruct.comp (β.v p₁ p₂ h₁₂) h_1
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- Constructor for functor composition  -/
MvPFunctor.comp.mk : {n m : ℕ} →
  {P : MvPFunctor.{u} n} →
    {Q : Fin2 n → MvPFunctor.{u} m} → {α : TypeVec.{u} m} → (↑P fun i => ↑(Q i) α) → ↑(P.comp Q) α
-- Mathlib.CategoryTheory.Action.Limits
Action.functorCategoryEquivalence_preservesZeroMorphisms : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V],
  (Action.functorCategoryEquivalence V G).functor.PreservesZeroMorphisms
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
BirdDet.birdDet_zero : ∀ {R : Type u_1} [inst : CommRing R] (A : Array R), BirdDet.birdDet 0 A = 1
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.pglMk_smul : ∀ (g : GL (Fin 2) ℝ) (z : UpperHalfPlane), Matrix.ProjGenLinGroup.mk g • z = g • z
-- Mathlib.Data.Finset.Union
Finset.disjiUnion_disjiUnion : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Finset α) (f : α → Finset β) (g : β → Finset γ)
  (h1 : (↑s).PairwiseDisjoint f) (h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g),
  (s.disjiUnion f h1).disjiUnion g h2 = s.attach.disjiUnion (fun a => (f ↑a).disjiUnion g ⋯) ⋯
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (preimage : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y))
  (map_preimage :
    autoParam (∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage f) = f)
      CategoryTheory.Functor.FullyFaithful.map_preimage._autoParam)
  (preimage_map :
    autoParam (∀ {X Y : C} (f : X ⟶ Y), preimage (F.map f) = f)
      CategoryTheory.Functor.FullyFaithful.preimage_map._autoParam)
  (preimage_1 : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y))
  (map_preimage_1 :
    autoParam (∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage_1 f) = f)
      CategoryTheory.Functor.FullyFaithful.map_preimage._autoParam)
  (preimage_map_1 :
    autoParam (∀ {X Y : C} (f : X ⟶ Y), preimage_1 (F.map f) = f)
      CategoryTheory.Functor.FullyFaithful.preimage_map._autoParam),
  ({ preimage := preimage, map_preimage := map_preimage, preimage_map := preimage_map } =
      { preimage := preimage_1, map_preimage := map_preimage_1, preimage_map := preimage_map_1 }) =
    (preimage = preimage_1)
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_ne_one : ∀ {a : ENNReal}, a.toNNReal ≠ 1 ↔ a ≠ 1
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.nonempty_uIoo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} [DenselyOrdered α], (Set.uIoo a b).Nonempty ↔ a ≠ b
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getElimNameInfo.throwMissingEliminator : Bool → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
/-- A triangle in `Cᵒᵖ` shall be distinguished iff it corresponds to a distinguished
triangle in `C` via the equivalence `triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ`.  -/
CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [CategoryTheory.Pretriangulated C] → Set (CategoryTheory.Pretriangulated.Triangle Cᵒᵖ)
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.comp_val : ∀ {M : Type u_1} [inst : Monoid M] {X : Type u} [inst_1 : MulAction M X] {x y z : CategoryTheory.ActionCategory M X}
  (f : x ⟶ y) (g : y ⟶ z), ↑(CategoryTheory.CategoryStruct.comp f g) = ↑g * ↑f
-- Lean.Level
Lean.Level.PP.Result.offset.injEq : ∀ (a : Lean.Level.PP.Result) (a_1 : ℕ) (a_2 : Lean.Level.PP.Result) (a_3 : ℕ),
  (a.offset a_1 = a_2.offset a_3) = (a = a_2 ∧ a_1 = a_3)
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.refl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} (m : Std.HashSet α), m.Equiv m
-- Lean.Declaration
Lean.instInhabitedInductiveType : Inhabited Lean.InductiveType
-- Mathlib.LinearAlgebra.Semisimple
Module.End.isFinitelySemisimple_iff_isSemisimple : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  [Module.Finite R M], f.IsFinitelySemisimple ↔ f.IsSemisimple
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ico_castAdd : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n),
  ∏ i ∈ Finset.Ico (Fin.castAdd m a) (Fin.castAdd m b), f i = ∏ i ∈ Finset.Ico a b, f (Fin.castAdd m i)
-- Mathlib.Tactic.NormNum.Irrational
Mathlib.Meta.NormNum.irrational_rpow_rat_rat_of_num : ∀ {x y : ℝ} {x_num x_den y_num y_den k_num : ℕ},
  Mathlib.Meta.NormNum.IsNNRat x x_num x_den →
    Mathlib.Meta.NormNum.IsNNRat y y_num y_den →
      x_num.Coprime x_den →
        y_num.Coprime y_den → k_num ^ y_den < x_num → x_num < (k_num + 1) ^ y_den → Irrational (x ^ y)
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.inf_mem_closed_subalgebra : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)),
  IsClosed ↑A → ∀ (f g : ↥A), ↑f ⊓ ↑g ∈ A
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.const_smul : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {s : Set M} {f : M → E'} (a : 𝕜), MDiff[s] f → MDiff[s] (a • f)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_lt_iff_lt_sin' : ∀ {x y : ℝ}, y ∈ Set.Ioc (-(Real.pi / 2)) (Real.pi / 2) → (Real.arcsin x < y ↔ x < Real.sin y)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instInfOpenNormalAddSubgroup.eq_1 : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenNormalAddSubgroup.instInfOpenNormalAddSubgroup =
    { min := fun U V => { toOpenAddSubgroup := U.toOpenAddSubgroup ⊓ V.toOpenAddSubgroup, isNormal' := ⋯ } }
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome.success : Lean.TSyntax `tactic → Mathlib.TacticAnalysis.TerminalReplacementOutcome✝
-- Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Subgroup.properlyDiscontinuousSMul_of_le : ∀ {Γ : Type u_1} {α : Type u_2} [inst : Group Γ] [inst_1 : TopologicalSpace α] [inst_2 : SMul Γ α] {G H : Subgroup Γ},
  ProperlyDiscontinuousSMul (↥G) α → H ≤ G → ProperlyDiscontinuousSMul (↥H) α
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.inv_right_hom_right_assoc : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (e : f ≅ g) {Z : T}
  (h : g.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right e.inv)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right e.hom) h) =
    h
-- Mathlib.AlgebraicGeometry.ResidueField
/-- The residue map from the stalk to the residue field.  -/
AlgebraicGeometry.Scheme.residue : (X : AlgebraicGeometry.Scheme) → (x : ↥X) → X.presheaf.stalk x ⟶ X.residueField x
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_coe_eq_top_iff : ∀ {α : Type u} [inst : Add α] {x : WithTop α} {b : α}, x + ↑b = ⊤ ↔ x = ⊤
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the induced map from the short complex
`Fun(H, A) --d₁₂--> Fun(H × H, A) --d₂₃--> Fun(H × H × H, A)` to
`Fun(G, B) --d₁₂--> Fun(G × G, B) --d₂₃--> Fun(G × G × G, B)`.  -/
groupCohomology.mapShortComplexH2 : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u_1, u, u} k H} →
          {B : Rep.{u_1, u, u} k G} →
            (f : G →* H) → (Rep.res f A ⟶ B) → (groupCohomology.shortComplexH2 A ⟶ groupCohomology.shortComplexH2 B)
-- Mathlib.Order.Interval.Finset.Fin
Fin.card_Iio : ∀ {n : ℕ} (b : Fin n), (Finset.Iio b).card = ↑b
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.indepFun_zero_left : ∀ {α : Type u_1} {Ω : Type u_2} {γ : Type u_6} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} {β : Type u_10} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] {f : Ω → β}
  {g : Ω → γ}, ProbabilityTheory.Kernel.IndepFun f g 0 μ
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.univ : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X], Convexity.IsConvexSet R Set.univ
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, panicking if the map is
empty.
 -/
Std.DTreeMap.Const.minEntry! : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap α (fun x => β) cmp → α × β
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_finCongr_Ici : ∀ {n m : ℕ} (h : n = m) (i : Fin n), Finset.map (finCongr h).toEmbedding (Finset.Ici i) = Finset.Ici (Fin.cast h i)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.map₂_const : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (l : Filter α) (b : β) (c : γ) (f : β → γ → δ),
  Filter.Germ.map₂ f ↑b ↑c = ↑(f b c)
-- Mathlib.Logic.Function.Basic
/-- Uncurrying operator. The most generic use is to recursively uncurry. For instance
`f : α → β → γ → δ` will be turned into `↿f : α × β × γ → δ`. One can also add instances
for bundled maps.  -/
Function.HasUncurry.uncurry : {α : Type u_5} → {β : outParam (Type u_6)} → {γ : outParam (Type u_7)} → [self : Function.HasUncurry α β γ] → α → β → γ
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_iSup_Iio : ∀ {a : Ordinal.{u_1}} {f : ↑(Set.Iio a) → Ordinal.{u_1}}, StrictMono f → Order.IsSuccPrelimit a → (⨆ i, f i).cof = a.cof
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.sub_self : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] (a : M), a - a = 0
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_mono : ∀ {X : Type u_2} [inst : EMetricSpace X] {s t : Set X}, s ⊆ t → dimH s ≤ dimH t
-- Init.Data.List.Basic
List.prod_eq_foldr : ∀ {α : Type u} [inst : Mul α] [inst_1 : One α] {l : List α}, l.prod = List.foldr (fun x1 x2 => x1 * x2) 1 l
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.instSMulSubtypeMem : {R : Type u_1} → [inst : Ring R] → (I : TwoSidedIdeal R) → SMul R ↥I
-- Mathlib.Data.Finset.Basic
Equiv.Finset.union_inl : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (h : Disjoint s t) (x : ↥s),
  (Equiv.Finset.union s t h) (Sum.inl x) = ⟨↑x, ⋯⟩
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.State.cache : Lean.MetavarContext.LevelMVarToParam.State → Std.HashMap Lean.ExprStructEq Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.orthogonalFamily_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E), OrthogonalFamily 𝕜 (fun b => ↥(bif b then K else Kᗮ)) fun b => (bif b then K else Kᗮ).subtypeₗᵢ
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Given a `TransvectionStruct` on `n`, define the corresponding `TransvectionStruct` on `n ⊕ p`
using the identity on `p`.  -/
Matrix.TransvectionStruct.sumInl : {n : Type u_1} → (p : Type u_2) → {R : Type u₂} → Matrix.TransvectionStruct n R → Matrix.TransvectionStruct (n ⊕ p) R
-- Mathlib.Logic.Equiv.Basic
Eq.mpr.congr_simp : ∀ {α β : Sort u} (h : α = β) (b b_1 : β), b = b_1 → h.mpr b = h.mpr b_1
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.tensor : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {W X Y Z : CategoryTheory.FreeMonoidalCategory C} {f f' : W.Hom X} {g g' : Y.Hom Z}
  (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f f') (a_1 : CategoryTheory.FreeMonoidalCategory.HomEquiv g g'),
  CategoryTheory.FreeMonoidalCategory.HomEquiv.below a →
    motive f f' a →
      CategoryTheory.FreeMonoidalCategory.HomEquiv.below a_1 →
        motive g g' a_1 → CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.Tactic.Linter.Whitespace
/-- The distance to the end of the formatted string, as number of characters  -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.FormatError.fmtPos : Mathlib.Linter.FormatError✝ → ℕ
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.cocycle : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i)
        (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j)) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
-- Mathlib.Order.Filter.AtTopBot.Finset
Filter.tendsto_toLeft_atTop : ∀ {α : Type u_3} {β : Type u_4}, Filter.Tendsto Finset.toLeft Filter.atTop Filter.atTop
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.Map.instIterator_eq_filterMapInstIterator : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad n] [inst_1 : Std.Iterator α m β]
  {lift : ⦃α : Type w⦄ → m α → n α} {f : β → Std.Iterators.PostconditionT n γ},
  Std.Iterators.Types.Map.instIterator = Std.Iterators.Types.FilterMap.instIterator
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.lsingle_apply : ∀ {R : Type u_3} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] {α : Type u_6} (a : α)
  [inst_2 : Module R M] (m : M), (SkewMonoidAlgebra.lsingle R a) m = SkewMonoidAlgebra.single a m
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.instGroup : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → Group (N ⋊[φ] G)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_nhds_one_swapped : ∀ (Gᵣ : Type u_3) [inst : UniformSpace Gᵣ] [inst_1 : Group Gᵣ] [IsRightUniformGroup Gᵣ],
  uniformity Gᵣ = Filter.comap (fun x => x.1 / x.2) (nhds 1)
-- Mathlib.Order.Sublocale
_private.Mathlib.Order.Sublocale.0.Sublocale.le_restrictAux : ∀ {X : Type u_1} [inst : Order.Frame X] {S : Sublocale X} {a : X}, a ≤ ↑(Sublocale.restrictAux✝ S a)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insert.induct : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k)
  (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Prop),
  (∀ (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced), motive Std.DTreeMap.Internal.Impl.leaf hr) →
    (∀ (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
        (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
        compare k k' = Ordering.lt →
          ∀ (d : Std.DTreeMap.Internal.Impl α β) (hd : d.Balanced) (hd₁ : l'.size ≤ d.size)
            (hd₂ : d.size ≤ l'.size + 1),
            Std.DTreeMap.Internal.Impl.insert k v l' ⋯ =
                { impl := d, balanced_impl := hd, lb_le_size_impl := hd₁, size_impl_le_ub := hd₂ } →
              motive l' ⋯ → motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr) →
      (∀ (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
          (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
          compare k k' = Ordering.gt →
            ∀ (d : Std.DTreeMap.Internal.Impl α β) (hd : d.Balanced) (hd₁ : r'.size ≤ d.size)
              (hd₂ : d.size ≤ r'.size + 1),
              Std.DTreeMap.Internal.Impl.insert k v r' ⋯ =
                  { impl := d, balanced_impl := hd, lb_le_size_impl := hd₁, size_impl_le_ub := hd₂ } →
                motive r' ⋯ → motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr) →
        (∀ (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
            (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
            compare k k' = Ordering.eq → motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr) →
          ∀ (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced), motive t hl
-- Mathlib.Logic.Relation
Relation.reflGen_le_reflTransGen : ∀ {α : Type u_1} {r : α → α → Prop}, Relation.ReflGen r ≤ Relation.ReflTransGen r
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffAt.of_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {m n : WithTop ℕ∞}, ContDiffAt 𝕜 n f x → m ≤ n → ContDiffAt 𝕜 m f x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasFDerivWithinAt.csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E}
  {s : Set E}, HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Complex.sin (f x)) (Complex.cos (f x) • f') s x
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.exp_one_pow : ∀ (n : ℕ), Real.exp 1 ^ n = Real.exp ↑n
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
/-- The pointwise scalar multiplication of sets `s • t` is defined as `{x • y | x ∈ s, y ∈ t}` in
scope `Pointwise`.  -/
Set.smul : {α : Type u_2} → {β : Type u_3} → [SMul α β] → SMul (Set α) (Set β)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.app_left_eq_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (a : J.L),
  K.π.app (CategoryTheory.Limits.WalkingMulticospan.left a) = K.ι a
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.norm_integral_le_abs_integral_norm : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ}, ‖∫ (x : ℝ) in a..b, f x ∂μ‖ ≤ |∫ (x : ℝ) in a..b, ‖f x‖ ∂μ|
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- (Implementation) Transition maps in the glue data for `𝒪ₓ/I`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.glueDataT : {X : AlgebraicGeometry.Scheme} →
  (I : X.IdealSheafData) → (U V : ↑X.affineOpens) → I.glueDataObjPullback U V ⟶ I.glueDataObjPullback V U
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} (π : ι → Set (Set Ω)) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndepSets π μ =
    ProbabilityTheory.Kernel.iIndepSets π (ProbabilityTheory.Kernel.const Unit μ) (MeasureTheory.Measure.dirac ())
-- Mathlib.Order.InitialSeg
InitialSeg.image_Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : PartialOrder α] (f : α ≤i β) (a : α),
  ⇑f '' Set.Iio a = Set.Iio (f a)
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
/-- Let `M, N` be `R`-modules, `n ≤ N` be an `R`-submodule. Then we have a linear isomorphism between
tensor products of the quotient and the quotient of the tensor product:
`M ⊗[R] (N ⧸ n) ≃ₗ[R] (M ⊗[R] N) ⧸ (M ⊗ n)`.
 -/
TensorProduct.tensorQuotientEquiv : {R : Type u_1} →
  (M : Type u_2) →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] →
                (n : Submodule R N) →
                  TensorProduct R M (N ⧸ n) ≃ₗ[R] TensorProduct R M N ⧸ (TensorProduct.map LinearMap.id n.subtype).range
-- Mathlib.Topology.Algebra.Star.Unitary
isClosed_unitary : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : TopologicalSpace R] [T1Space R] [ContinuousStar R]
  [ContinuousMul R], IsClosed ↑(unitary R)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  k ∉ m₂ → (m₁ \ m₂).get? k = m₁.get? k
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.comap_normalizer_eq_of_le_range : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {N : Type u_5} [inst_1 : AddGroup N] {f : N →+ G},
  H ≤ f.range → AddSubgroup.comap f (AddSubgroup.normalizer ↑H) = AddSubgroup.normalizer ↑(AddSubgroup.comap f H)
-- Lean.Data.Trie
/-- Find the longest _key_ in the trie that is contained in the given string `s` at position `i`,
and return the associated value.  -/
Lean.Data.Trie.matchPrefix : {α : Type} →
  (s : String) →
    Lean.Data.Trie α →
      String.Pos.Raw →
        (endByte : optParam ℕ s.utf8ByteSize) →
          autoParam (endByte ≤ s.utf8ByteSize) Lean.Data.Trie.matchPrefix._auto_1 → Option α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β k}, (t.insertIfNew k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.sum_sum_index : ∀ {α : Type u_3} {β : Type u_4} {M : Type u_5} {N : Type u_6} {P : Type u_7} [inst : AddCommMonoid M]
  [inst_1 : AddCommMonoid N] [inst_2 : AddCommMonoid P] {f : SkewMonoidAlgebra M α} {g : α → M → SkewMonoidAlgebra N β}
  {h : β → N → P},
  (∀ (a : β), h a 0 = 0) →
    (∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂) → (f.sum g).sum h = f.sum fun a b => (g a b).sum h
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipping_functor_map_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  {F₁ F₂ : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (φ : F₁ ⟶ F₂) (Y : D) (X : C),
  ((CategoryTheory.Functor.flipping.functor.map φ).app Y).app X = (φ.app X).app Y