mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The construction `precompose` respects functor composition.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A B) →
              (G : CategoryTheory.Functor C B) →
                {X : Type u₄} →
                  {Y : Type u₅} →
                    {Z : Type u₆} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} Y] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} Z] →
                            (U : CategoryTheory.Functor X Y) →
                              (V : CategoryTheory.Functor Y Z) →
                                (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj
                                    (U.comp V) ≅
                                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj V).comp
                                    ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.hasNoImplicitLambdaAnnotation : Lean.Expr → Bool
-- Mathlib.Data.Vector3
VectorAllP.imp : ∀ {α : Type u_1} {n : ℕ} {p q : α → Prop}, (∀ (x : α), p x → q x) → ∀ {v : Vector3 α n}, VectorAllP p v → VectorAllP q v
-- Mathlib.RingTheory.Smooth.Field
Algebra.FormallySmooth.adjoin_of_algebraicIndependent : ∀ {K : Type u_1} {L : Type u_2} {ι : Type u_3} [inst : Field L] [inst_1 : Field K] [inst_2 : Algebra K L] {v : ι → L},
  AlgebraicIndependent K v → Algebra.FormallySmooth K ↥(IntermediateField.adjoin K (Set.range v))
-- Mathlib.Probability.Kernel.Composition.CompNotation
MeasureTheory.Measure.swap_comp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure (α × β)},
  μ.bind ⇑(ProbabilityTheory.Kernel.swap α β) = MeasureTheory.Measure.map Prod.swap μ
-- Mathlib.Topology.Bornology.Basic
Bornology.ofBounded'_cobounded : ∀ {α : Type u_4} (B : Set (Set α)) (empty_mem : ∅ ∈ B) (subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B)
  (union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B) (sUnion_univ : ⋃₀ B = Set.univ),
  Bornology.cobounded α = Filter.comk (fun x => x ∈ B) empty_mem subset_mem union_mem
-- Init.Data.BitVec.Basic
/-- Every bitvector of length 0 is equal to `nil`, i.e., there is only one empty bitvector  -/
BitVec.eq_nil : ∀ (x : BitVec 0), x = BitVec.nil
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_const : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  (c : ε), p ≠ 0 → μ ≠ 0 → MeasureTheory.eLpNorm (fun x => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- The integral of an almost-everywhere strongly measurable function over `UnitAddCircle` is
equal to the integral over an interval $(t, t + 1]$ in `ℝ` of its lift to `ℝ`.  -/
UnitAddCircle.intervalIntegral_preimage : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (t : ℝ) (f : UnitAddCircle → E),
  ∫ (a : ℝ) in t..t + 1, f ↑a = ∫ (b : UnitAddCircle), f b
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.tensorFunc_map_app : ∀ (C : Type u) {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X ⟶ Y)
  (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C),
  ((CategoryTheory.FreeMonoidalCategory.tensorFunc C).map f).app n =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := n.as })
      f
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m₁ →
    Std.DHashMap.Internal.Raw.WFImp ↑m₂ →
      (Std.DHashMap.Internal.toListModel (↑(m₁.diff m₂)).buckets).Perm
        (List.filter (fun k => !(List.map Sigma.fst (Std.DHashMap.Internal.toListModel (↑m₂).buckets)).contains k.fst)
          (Std.DHashMap.Internal.toListModel (↑m₁).buckets))
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso X i).hom.right =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.right W)
-- Lean.Meta.Tactic.Grind.Attr
/-- Returns `true` is `declName` is a builtin split or has been tagged with `[grind]` attribute.  -/
Lean.Meta.Grind.isGlobalSplit : Lean.Name → Lean.CoreM Bool
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
/-- If two regular measures induce the same linear functional on `C_c(X, ℝ≥0)`, then they are
equal.  -/
NNRealRMK.integralLinearMap_inj : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [inst_3 : MeasurableSpace X]
  [inst_4 : BorelSpace X] {μ ν : MeasureTheory.Measure X} [inst_5 : μ.Regular] [inst_6 : ν.Regular],
  CompactlySupportedContinuousMap.integralLinearMap μ = CompactlySupportedContinuousMap.integralLinearMap ν ↔ μ = ν
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.exactly : {α : Type} → Std.Internal.Parsec.String.Parser α → ℕ → Std.Internal.Parsec.String.Parser (Array α)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.toList_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.toArray.toList = t.toList
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_mul_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G]
  {a : G}, ContMDiff I I n fun x => a * x
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.liftedLimitMapsToOriginal_inv_map_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} [inst_3 : CategoryTheory.CreatesLimit K F]
  {c : CategoryTheory.Limits.Cone (K.comp F)} (t : CategoryTheory.Limits.IsLimit c) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.liftedLimitMapsToOriginal t).inv.hom
      (F.map ((CategoryTheory.liftLimit t).π.app j)) =
    c.π.app j
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_iUnion_eq_sum_mk : ∀ {α ι : Type u} {f : ι → Set α},
  Pairwise (Function.onFun Disjoint f) → Cardinal.mk ↑(⋃ i, f i) = Cardinal.sum fun i => Cardinal.mk ↑(f i)
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.divLeft_eq_inv_trans_mulLeft : ∀ {G : Type u_5} [inst : Group G] (a : G), Equiv.divLeft a = Equiv.trans (Equiv.inv G) (Equiv.mulLeft a)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C}
  {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B),
  CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔
    Function.Bijective (CategoryTheory.Presieve.Arrows.toCompatible P π)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_filterMap_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filterMap f m)).isEmpty = true ↔
      ∀ (k : α) (h : m.contains k = true), f (m.getKey k h) (Std.DHashMap.Internal.Raw₀.Const.get m k h) = none)
-- Init.Data.SInt.Bitwise
instAssociativeISizeHOr : Std.Associative fun x1 x2 => x1 ||| x2
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.ringOfIntegersComplexConj.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K],
  NumberField.IsCMField.ringOfIntegersComplexConj K = NumberField.IsCMField.ringOfIntegersComplexConj K
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
isIntegral_of_submodule_noetherian : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] (S : Subalgebra R B),
  IsNoetherian R ↥(Subalgebra.toSubmodule S) → ∀ x ∈ S, IsIntegral R x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_insert_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β} {fallback : α}, (cmp ((t.insert k v).minKeyD fallback) k).isLE = true
-- Init.Data.SInt.Lemmas
Int16.lt_irrefl : ∀ {a : Int16}, ¬a < a
-- Mathlib.Analysis.Calculus.TangentCone.Basic
tangentConeAt_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : DivisionSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace 𝕜] [inst_4 : TopologicalSpace E] [ContinuousSMul 𝕜 E] {x : E} [(nhdsWithin 0 {0}ᶜ).NeBot],
  tangentConeAt 𝕜 Set.univ x = Set.univ
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.not : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsQF → φ.not.IsQF
-- Init.Data.Nat.ToString
Nat.ofDigitChars_cons_digitChar_of_lt_ten : ∀ {b n : ℕ},
  n < 10 → ∀ {cs : List Char} {init : ℕ}, b.ofDigitChars (n.digitChar :: cs) init = b.ofDigitChars cs (b * init + n)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_sum : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {ι' : Type u_8} (μ : ι → ι' → MeasureTheory.Measure α),
  (MeasureTheory.Measure.sum fun n => MeasureTheory.Measure.sum (μ n)) = MeasureTheory.Measure.sum fun p => μ p.1 p.2
-- Mathlib.Data.Ordmap.Invariants
Ordnode.eraseMin.eq_3 : ∀ {α : Type u_1} (size sz : ℕ) (l' : Ordnode α) (y : α) (r' : Ordnode α) (x_1 : α) (r : Ordnode α),
  (Ordnode.node size (Ordnode.node sz l' y r') x_1 r).eraseMin = (Ordnode.node sz l' y r').eraseMin.balanceR x_1 r
-- Lean.Expr
/-- Instantiates the loose bound variables in `e` using the `subst` array.
This is equivalent to `Lean.Expr.instantiate e subst.reverse`, but it avoids reversing the array.
In particular, rather than instantiating `Expr.bvar i` with `subst[i - d]` it instantiates with `subst[subst.size - 1 - (i - d)]`,
where `d` is the binding depth.

This function instantiates with the "forwards" indexing scheme.
For example, if `e` represents the expression `fun x y => x + y`,
then `instantiateRev e.bindingBody!.bindingBody! #[a, b]` yields `a + b`.
The `instantiate` function on the other hand would yield `b + a`, since de Bruijn indices count outwards.
  -/
Lean.Expr.instantiateRev : Lean.Expr → Array Lean.Expr → Lean.Expr
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.instPseudoEpimorphismClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β],
  PseudoEpimorphismClass (PseudoEpimorphism α β) α β
-- Mathlib.Data.Vector.Mem
List.Vector.get_mem : ∀ {α : Type u_1} {n : ℕ} (i : Fin n) (v : List.Vector α n), v.get i ∈ v.toList
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.Lifting.id : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            CategoryTheory.Localization.Lifting L W L (CategoryTheory.Functor.id D)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.prod_subgroupOf_prod_normal : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {H₁ K₁ : Subgroup G} {H₂ K₂ : Subgroup N}
  [h₁ : (H₁.subgroupOf K₁).Normal] [h₂ : (H₂.subgroupOf K₂).Normal], ((H₁.prod H₂).subgroupOf (K₁.prod K₂)).Normal
-- Mathlib.Data.Num.Prime
_private.Mathlib.Data.Num.Prime.0.PosNum.minFacAux.match_1.splitter : (motive : ℕ → PosNum → Sort u_1) →
  (x : ℕ) →
    (x_1 : PosNum) → ((x : PosNum) → motive 0 x) → ((fuel : ℕ) → (k : PosNum) → motive fuel.succ k) → motive x x_1
-- Mathlib.LinearAlgebra.Dimension.Localization
/-- A domain that is not (left) Ore is of infinite rank.
See [cohn_1995] Proposition 1.3.6  -/
aleph0_le_rank_of_isEmpty_oreSet : ∀ {R : Type u_1} [inst : Ring R] [IsDomain R],
  IsEmpty (OreLocalization.OreSet (nonZeroDivisors R)) → Cardinal.aleph0 ≤ Module.rank R R
-- Mathlib.Data.Finset.Image
Finset.image_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → β), Monotone (Finset.image f)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.π`.

---

`h.π m` is the first projection in the following pullback square:

```
U --h.π m--> (Ω₀ : C)
|                |
m             Ω₀.arrow
|                |
v                v
X -----h.χ m---> Ω
```
 -/
CategoryTheory.Classifier.SubobjectRepresentableBy.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} →
        (h : CategoryTheory.SubobjectRepresentableBy Ω) →
          {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → U ⟶ CategoryTheory.Subobject.underlying.obj h.Ω₀
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], k ∉ m₁ → (m₁ ∩ m₂).get! k = default
-- Mathlib.Topology.Separation.GDelta
/-- A `T₆` space is a `T₅` space.  -/
T6Space.toT5Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T6Space X], T5Space X
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.mul''_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (a : TensorProduct R A A), (LinearMap.mul'' R A) a = (TensorProduct.liftAux (LinearMap.mul R A)) a
-- Mathlib.Combinatorics.Graph.Basic
Graph.vertexSet_banana : ∀ {α : Type u_1} {β : Type u_2} (u v : α) (edgeSet : Set β), (Graph.banana u v edgeSet).vertexSet = {u, v}
-- Mathlib.Algebra.Free
/-- `FreeAddSemigroup` is traversable.  -/
FreeAddSemigroup.traverse : {m : Type u → Type u} → [Applicative m] → {α β : Type u} → (α → m β) → FreeAddSemigroup α → m (FreeAddSemigroup β)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ico_of_Ioc : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α} [MeasureTheory.NullSingletonClass μ],
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ico A B)) l fun i => Set.Ioc (a i) (b i)
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.toList_rci : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.toList_rci._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet.Raw α cmp},
  t.WF →
    ∀ {bound : α},
      Std.Slice.toList (Std.Rci.Sliceable.mkSlice t bound...*) = List.filter (fun e => (cmp e bound).isGE) t.toList
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_eq_zero_iff : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, addOrderOf x = 0 ↔ ¬IsOfFinAddOrder x
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.append_append_left_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} (L : List (α × Bool)), FreeGroup.Red (L ++ L₁) (L ++ L₂) ↔ FreeGroup.Red L₁ L₂
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biprod.ofComponents_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂),
  CategoryTheory.Biprod.ofComponents
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
        (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
        (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
        (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
        (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd)) =
    f
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.mulLeftCosetsCompSubtypeVal : {G : Type u} → [inst : Group G] → (H I : Subgroup G) → MulAction (↥I) (G ⧸ H)
-- Mathlib.Logic.Function.Basic
Function.extend_id : ∀ {α : Sort u_1} {γ : Sort u_3} (g e' : α → γ), Function.extend id g e' = g
-- Mathlib.Analysis.Normed.Lp.PiLp
_private.Mathlib.Analysis.Normed.Lp.PiLp.0.PiLp.antilipschitzWith_ofLp_aux : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : Fact (1 ≤ p)] [inst_1 : (i : ι) → PseudoEMetricSpace (β i)]
  [inst_2 : Fintype ι], AntilipschitzWith (↑(Fintype.card ι) ^ (1 / p).toReal) WithLp.ofLp
-- Mathlib.Algebra.Group.Action.Defs
/-- Pullback a multiplicative action along an injective map respecting `•`.
See note [reducible non-instances].  -/
Function.Injective.mulAction : {M : Type u_1} →
  {α : Type u_5} →
    {β : Type u_6} →
      [inst : Monoid M] →
        [inst_1 : MulAction M α] →
          [inst_2 : SMul M β] →
            (f : β → α) → Function.Injective f → (∀ (c : M) (x : β), f (c • x) = c • f x) → MulAction M β
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.lift_apply_apply : ∀ {R : Type u_2} {a b : R} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Ring A] [inst_2 : Algebra R A]
  (u : { u // u * u = a • 1 + b • u }) (z : QuadraticAlgebra R a b), (QuadraticAlgebra.lift u) z = z.re • 1 + z.im • ↑u
-- Mathlib.Algebra.Ring.Int.Defs
/-- Note this holds in marginally more generality than `Int.cast_mul`  -/
Int.cast_mul_eq_zsmul_cast : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (m n : ℤ), ↑(m * n) = m • ↑n
-- Mathlib.RingTheory.AdicCompletion.Functoriality
surjective_of_mkQ_comp_surjective : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsPrecomplete I M] [IsHausdorff I N] {f : M →ₗ[R] N},
  Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f) → Function.Surjective ⇑f
-- Mathlib.Order.RelClasses
instIsWellOrderOfIsEmpty : ∀ {α : Type u} [IsEmpty α] (r : α → α → Prop), IsWellOrder α r
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The inverse of distributivity isomorphism from the closed monoidal structure  -/
CategoryTheory.MonoidalClosed.leftDistrib_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.MonoidalClosed C] {X Y Z : C},
  (CategoryTheory.leftDistrib X Y Z).inv =
    CategoryTheory.MonoidalClosed.uncurry
      (CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalClosed.curry CategoryTheory.Limits.coprod.inl)
        (CategoryTheory.MonoidalClosed.curry CategoryTheory.Limits.coprod.inr))
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.isAlgebraic_sum : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsAlgebraic] [L'.IsAlgebraic], (L.sum L').IsAlgebraic
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- `-1` is a square in `ZMod p` iff `p` is not congruent to `3` mod `4`.  -/
ZMod.exists_sq_eq_neg_one_iff : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], IsSquare (-1) ↔ p % 4 ≠ 3
-- Mathlib.Order.Basic
/-- monotonicity of `≥` with respect to `→`  -/
ge_imp_ge_of_le_of_le : ∀ {α : Type u_2} [inst : Preorder α] {a b c d : α}, a ≤ c → d ≤ b → a ≥ b → c ≥ d
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.instSMul : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] → SMul R (PiTensorProduct R fun i => s i)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.diff : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {s' : Set X} {t' : Set Y},
  e.IsImage s t → e.IsImage s' t' → e.IsImage (s \ s') (t \ t')
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyOpIso_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ).op S₁.homologyOpIso.inv =
    CategoryTheory.CategoryStruct.comp S₂.homologyOpIso.inv
      (CategoryTheory.ShortComplex.homologyMap (CategoryTheory.ShortComplex.opMap φ))
-- Init.WF
PSigma.Lex.left : ∀ {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} {a₁ : α} (b₁ : β a₁) {a₂ : α}
  (b₂ : β a₂), r a₁ a₂ → PSigma.Lex r s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
-- Mathlib.Algebra.CharP.Lemmas
Nat.Prime.dvd_add_pow_sub_pow_of_dvd : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) {p : ℕ},
  Nat.Prime p → ∀ {r : R}, r ∣ x ^ p → r ∣ ↑p * x → r ∣ (x + y) ^ p - y ^ p
-- Init.Data.BitVec.Lemmas
/-- Equation theorem for `sdiv` in terms of `udiv`.  -/
BitVec.sdiv_eq : ∀ {w : ℕ} (x y : BitVec w),
  x.sdiv y =
    match x.msb, y.msb with
    | false, false => x.udiv y
    | false, true => -x.udiv (-y)
    | true, false => -(-x).udiv y
    | true, true => (-x).udiv (-y)
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.orbit.pairwiseDisjoint : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X],
  (Set.range fun x => AddAction.orbit G x).PairwiseDisjoint id
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.idx_trichotomy : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {start : ℕ} (aig : Std.Sat.AIG α)
  (hstart : start < aig.decls.size) {prop : Prop},
  (aig.decls[start] = Std.Sat.AIG.Decl.false → prop) →
    (∀ (a : α), aig.decls[start] = Std.Sat.AIG.Decl.atom a → prop) →
      (∀ (lhs rhs : Std.Sat.AIG.Fanin), aig.decls[start] = Std.Sat.AIG.Decl.gate lhs rhs → prop) → prop
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.chart_mem_maximalAtlas : ∀ {𝕜 : 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} {n : WithTop ℕ∞}
  {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I n M] (x : M),
  chartAt H x ∈ IsManifold.maximalAtlas I n M
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.toAddMonoidHom_linearMapOfLE : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : NormedRing 𝕜]
  [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] {p q : ENNReal} (h : p ≤ q),
  (lp.linearMapOfLE 𝕜 E h).toAddMonoidHom = AddSubgroup.inclusion ⋯
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castSucc_Icc : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc '' Set.Icc i j = Set.Icc i.castSucc j.castSucc