mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Implicit
/-- Data used to apply the generic implicit function theorem to the case of a strictly
differentiable map such that its derivative is surjective and has a complemented kernel.  -/
HasStrictFDerivAt.implicitFunctionDataOfComplemented : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : CompleteSpace F] →
                    (f : E → F) →
                      (f' : E →L[𝕜] F) →
                        {a : E} →
                          HasStrictFDerivAt f f' a →
                            (↑f').range = ⊤ → (↑f').ker.ClosedComplemented → ImplicitFunctionData 𝕜 E F ↥(↑f').ker
-- Mathlib.Analysis.Normed.Lp.PiLp
Sigma.curry.eq_1 : ∀ {α : Type u_1} {β : α → Type u_4} {γ : (a : α) → β a → Type u_7} (f : (x : Sigma β) → γ x.fst x.snd) (x : α)
  (y : β x), Sigma.curry f x y = f ⟨x, y⟩
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCover_t : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x x_1 : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).t x x_1 = (CategoryTheory.Limits.pullbackSymmetry (𝒰.f x) (𝒰.f x_1)).hom
-- Mathlib.Tactic.Sat.FromLRAT
/-- Parse an integer  -/
Mathlib.Tactic.Sat.Parser.parseInt : Std.Internal.Parsec.String.Parser ℤ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β}, t.isEmpty = true → t.getD a fallback = fallback
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGT?.go.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option α),
  Std.DTreeMap.Internal.Impl.getKeyGT?.go k best Std.DTreeMap.Internal.Impl.leaf = best
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
/-- In a simply connected space, any two paths are homotopic  -/
SimplyConnectedSpace.paths_homotopic : ∀ {X : Type u_3} [inst : TopologicalSpace X] [SimplyConnectedSpace X] {x y : X} (p₁ p₂ : Path x y), p₁.Homotopic p₂
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_fin_zero : ∀ {α : Type w} [inst : CommRing α] (A : Matrix (Fin 0) (Fin 0) α), A.adjugate = 0
-- Init.Data.Int.Order
Int.le_iff_lt_add_one : ∀ {a b : ℤ}, a ≤ b ↔ a < b + 1
-- Mathlib.Order.Category.Frm
/-- The type of morphisms in `Frm R`.  -/
Frm.Hom : Frm → Frm → Type u
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a left invariant measure under right addition is left invariant.  -/
MeasureTheory.isMulLeftInvariant_map_add_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G}
  [μ.IsAddLeftInvariant] (g : G), (MeasureTheory.Measure.map (fun x => x + g) μ).IsAddLeftInvariant
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.mk.injEq : ∀ {α : Type u_5} {β : Type u_6} (toFun : α → β) (invFun : β → α) (source : Set α) (target : Set β)
  (map_source' : ∀ ⦃x : α⦄, x ∈ source → toFun x ∈ target) (map_target' : ∀ ⦃x : β⦄, x ∈ target → invFun x ∈ source)
  (left_inv' : ∀ ⦃x : α⦄, x ∈ source → invFun (toFun x) = x) (right_inv' : ∀ ⦃x : β⦄, x ∈ target → toFun (invFun x) = x)
  (toFun_1 : α → β) (invFun_1 : β → α) (source_1 : Set α) (target_1 : Set β)
  (map_source'_1 : ∀ ⦃x : α⦄, x ∈ source_1 → toFun_1 x ∈ target_1)
  (map_target'_1 : ∀ ⦃x : β⦄, x ∈ target_1 → invFun_1 x ∈ source_1)
  (left_inv'_1 : ∀ ⦃x : α⦄, x ∈ source_1 → invFun_1 (toFun_1 x) = x)
  (right_inv'_1 : ∀ ⦃x : β⦄, x ∈ target_1 → toFun_1 (invFun_1 x) = x),
  ({ toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
        map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' } =
      { toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1, map_source' := map_source'_1,
        map_target' := map_target'_1, left_inv' := left_inv'_1, right_inv' := right_inv'_1 }) =
    (toFun = toFun_1 ∧ invFun = invFun_1 ∧ source = source_1 ∧ target = target_1)
-- Mathlib.GroupTheory.NoncommPiCoprod
Subgroup.noncommPiCoprod_range : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} [inst_1 : Fintype ι]
  {hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y},
  (Subgroup.noncommPiCoprod hcomm).range = ⨆ i, H i
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
/-- Any independent set can be extended into a larger independent set.  -/
Matroid.Indep.augment : ∀ {α : Type u_1} {M : Matroid α} {I J : Set α},
  M.Indep I → M.Indep J → I.encard < J.encard → ∃ e ∈ J \ I, M.Indep (insert e I)
-- Batteries.Data.String.Lemmas
String.revFindAux_of_valid : ∀ (p : Char → Bool) (l r : List Char),
  String.Legacy.revFindAux (String.ofList (l.reverse ++ r)) p { byteIdx := String.utf8Len l } =
    Option.map (fun x => { byteIdx := String.utf8Len x }) (List.dropWhile (fun x => !p x) l).tail?
-- Mathlib.Combinatorics.Schnirelmann
/-- **Alias** of `schnirelmannDensity_setOfPred_even`. -/
schnirelmannDensity_setOf_even : schnirelmannDensity (Set.ofPred Even) = 0
-- Mathlib.Data.Set.Lattice
Set.sInter_singleton : ∀ {α : Type u_1} (s : Set α), ⋂₀ {s} = s
-- Mathlib.Data.ENNReal.Operations
ENNReal.image_coe_Iio : ∀ (x : NNReal), ENNReal.ofNNReal '' Set.Iio x = Set.Iio ↑x
-- Mathlib.RingTheory.Smooth.StandardSmoothOfFree
/-- An `R`-algebra `S` of finite presentation is standard smooth if and only if
`H¹(S/R) = 0` and `Ω[S⁄R]` is free on `{d sᵢ}ᵢ` for some `sᵢ : S`.  -/
Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FinitePresentation R S],
  Algebra.IsStandardSmooth R S ↔
    Subsingleton (Algebra.H1Cotangent R S) ∧ ∃ I b, Set.range ⇑b ⊆ Set.range ⇑(KaehlerDifferential.D R S)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.map_zero : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), e 0 = 0
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_eq : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : DecidableEq α] (f : α →₀ M) (a : α),
  Finsupp.filter (fun x => a = x) f = fun₀ | a => f a
-- Init.Data.SInt.Bitwise
Int8.ofBitVec_intMax : Int8.ofBitVec (BitVec.intMax 8) = Int8.maxValue
-- Mathlib.Data.FunLike.Graded
GradedFunLike.mk : ∀ {F : Type u_1} {A : outParam (Type u_2)} {B : outParam (Type u_3)} {σ : outParam (Type u_4)} {τ : outParam (Type u_5)}
  {ι : outParam (Type u_6)} [inst : SetLike σ A] [inst_1 : SetLike τ B] {𝒜 : outParam (ι → σ)} {ℬ : outParam (ι → τ)}
  [inst_2 : FunLike F A B], (∀ (f : F) {i : ι} {x : A}, x ∈ 𝒜 i → f x ∈ ℬ i) → GradedFunLike F 𝒜 ℬ
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.IsReduced.reduce_eq : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α], FreeAddGroup.IsReduced L → FreeAddGroup.reduce L = L
-- Std.Async.Basic
/-- Converts `Except` to `EAsync`.
 -/
Std.Async.EAsync.ofExcept : {ε α : Type} → Except ε α → Std.Async.EAsync ε α
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_map : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset γ)
  (f : γ ↪ β) (g : β → α), (Finset.map f s).sup g = s.sup (g ∘ ⇑f)
-- Mathlib.Logic.Pairwise
Function.Bijective.pairwise_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : β → α},
  Function.Bijective f → (Pairwise (Function.onFun r f) ↔ Pairwise r)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  [inst_2 : CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f}
  (i : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).inr =
    let c' := CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π c) ⋯;
    have i' := CategoryTheory.Limits.isCokernelEpiComp i (CategoryTheory.retraction f) ⋯;
    have i'' := CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork i';
    (CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C ⋯ i'').section_
-- Mathlib.Topology.ContinuousMap.Basic
Topology.IsQuotientMap.liftEquiv_symm_apply_coe : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : C(X, Y)} (hf : Topology.IsQuotientMap ⇑f) (g : C(Y, Z)),
  ↑(hf.liftEquiv.symm g) = g.comp f
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_const_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {d : 𝕜 → 𝔸} (c : 𝔸), DifferentiableAt 𝕜 d x → deriv (fun y => c * d y) x = c * deriv d x
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.iterationFunctor.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ Φ_1 : CategoryTheory.SmallObject.SuccStruct C),
  Φ = Φ_1 →
    ∀ (J : Type w) [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
      [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C], Φ.iterationFunctor J = Φ_1.iterationFunctor J
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instDiv.eq_1 : ∀ {α : Type u_1} [inst : Div α], OrderDual.instDiv = inst
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- A closed ball centred at the origin in a valued ring is closed.  -/
Valued.isClosed_closedBall : ∀ (R : Type u) [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀]
  (r : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀), IsClosed {x | Valued.v.restrict x ≤ r}
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndepOn_id_insert : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  {x : V}, x ∉ s → (LinearIndepOn K id (insert x s) ↔ LinearIndepOn K id s ∧ x ∉ Submodule.span K s)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- The canonical function `M → N → M ⊗ N`.  -/
TensorProduct.«term_⊗ₜ_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.Ring.Basic
/-- If `R` is a ring which is a semitopological semiring, then it is automatically a
semitopological ring. This exists so that one can place a topological ring structure on `R` without
explicitly proving `continuous_neg`.  -/
IsSemitopologicalSemiring.toIsSemitopologicalRing : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonAssocRing R],
  IsSemitopologicalSemiring R → IsSemitopologicalRing R
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent_one : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.toLaurent 1 = 1
-- Mathlib.FieldTheory.SeparableDegree
/-- A non-constant polynomial has non-zero separable degree.  -/
Polynomial.natSepDegree_ne_zero : ∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.natDegree ≠ 0 → f.natSepDegree ≠ 0
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.brecOn.eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : CommRingCat.Colimits.Prequotient F → Sort u} (t : CommRingCat.Colimits.Prequotient F)
  (F_1 : (t : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Prequotient.below t → motive t),
  CommRingCat.Colimits.Prequotient.brecOn t F_1 = F_1 t (CommRingCat.Colimits.Prequotient.brecOn.go t F_1).2
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mk.injEq : ∀ {X : AlgebraicGeometry.Scheme} (ideal : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U)))
  (map_ideal_basicOpen :
    ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal U) =
        ideal (X.affineBasicOpen f))
  (supportSet : Set ↥X)
  (supportSet_eq_iInter_zeroLocus :
    autoParam (supportSet = ⋂ U, X.zeroLocus ↑(ideal U))
      AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus._autoParam)
  (ideal_1 : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U)))
  (map_ideal_basicOpen_1 :
    ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal_1 U) =
        ideal_1 (X.affineBasicOpen f))
  (supportSet_1 : Set ↥X)
  (supportSet_eq_iInter_zeroLocus_1 :
    autoParam (supportSet_1 = ⋂ U, X.zeroLocus ↑(ideal_1 U))
      AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus._autoParam),
  ({ ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := supportSet,
        supportSet_eq_iInter_zeroLocus := supportSet_eq_iInter_zeroLocus } =
      { ideal := ideal_1, map_ideal_basicOpen := map_ideal_basicOpen_1, supportSet := supportSet_1,
        supportSet_eq_iInter_zeroLocus := supportSet_eq_iInter_zeroLocus_1 }) =
    (ideal = ideal_1 ∧ supportSet = supportSet_1)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.trans_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (hom : X ⟶ Y) (inv : Y ⟶ X)
  (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X)
  (inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y) (hom' : Y ⟶ Z)
  (inv' : Z ⟶ Y) (hom_inv_id' : CategoryTheory.CategoryStruct.comp hom' inv' = CategoryTheory.CategoryStruct.id Y)
  (inv_hom_id' : CategoryTheory.CategoryStruct.comp inv' hom' = CategoryTheory.CategoryStruct.id Z)
  (hom_inv_id'' :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp hom hom')
        (CategoryTheory.CategoryStruct.comp inv' inv) =
      CategoryTheory.CategoryStruct.id X)
  (inv_hom_id'' :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp inv' inv)
        (CategoryTheory.CategoryStruct.comp hom hom') =
      CategoryTheory.CategoryStruct.id Z),
  { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id } ≪≫
      { hom := hom', inv := inv', hom_inv_id := hom_inv_id', inv_hom_id := inv_hom_id' } =
    { hom := CategoryTheory.CategoryStruct.comp hom hom', inv := CategoryTheory.CategoryStruct.comp inv' inv,
      hom_inv_id := hom_inv_id'', inv_hom_id := inv_hom_id'' }
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- **Alias** of the forward direction of `affineIndependent_smul`. -/
AffineIndependent.of_smul : ∀ (k : Type u_1) {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_4}
  {G : Type u_5} [inst_3 : Group G] [inst_4 : DistribMulAction G V] [SMulCommClass G k V] {p : ι → V} {a : G},
  AffineIndependent k (a • p) → AffineIndependent k p
-- Mathlib.Algebra.Group.Hom.Defs
map_div' : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : DivInvMonoid G]
  [inst_2 : DivInvMonoid H] [MulHomClass F G H] (f : F),
  (∀ (a : G), f a⁻¹ = (f a)⁻¹) → ∀ (a b : G), f (a / b) = f a / f b
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.mk : ℕ →
  ℕ →
    Lean.Expr →
      Lean.Level →
        Lean.Expr →
          Option Lean.Expr →
            Option Lean.Expr →
              Option Lean.Expr →
                Option Lean.Expr →
                  Option Lean.Expr →
                    Option Lean.Expr →
                      Option Lean.Expr →
                        Lean.Expr →
                          Lean.Expr →
                            Lean.Expr →
                              Lean.Expr →
                                Lean.Expr →
                                  Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr) →
                                    Lean.Meta.Grind.Arith.Linear.NatStruct
-- Std.Internal.UV.Loop
/-- Configures the event loop with the specified options.
 -/
Std.Internal.UV.Loop.configure : Std.Internal.UV.Loop.Options → BaseIO Unit
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.sum_Icc_mu_right : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : PartialOrder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (a b : α),
  ∑ x ∈ Finset.Icc a b, (IncidenceAlgebra.mu 𝕜) a x = if a = b then 1 else 0
-- Init.Data.Nat.Fold
/-- Combines an initial value with each natural number from a range, in increasing order.

In particular, `(start, stop).foldI f init` applies `f`on all the numbers
from `start` (inclusive) to `stop` (exclusive) in increasing order:

Examples:
* `(5, 8).foldI (fun j _ _ xs => xs.push j) #[] = (#[] |>.push 5 |>.push 6 |>.push 7)`
* `(5, 8).foldI (fun j _ _ xs => xs.push j) #[] = #[5, 6, 7]`
* `(5, 8).foldI (fun j _ _ xs => toString j :: xs) [] = ["7", "6", "5"]`
 -/
Prod.foldI : {α : Type u} → (i : ℕ × ℕ) → ((j : ℕ) → i.1 ≤ j → j < i.2 → α → α) → α → α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : Cᵒᵖ} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P}, CategoryTheory.IsPushout f g inl inr → CategoryTheory.IsPullback inr.unop inl.unop g.unop f.unop
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp₂Measurable.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace β]
  [inst_5 : TopologicalSpace.PseudoMetrizableSpace β] [inst_6 : BorelSpace β] [inst_7 : MeasurableSpace γ]
  [inst_8 : TopologicalSpace.PseudoMetrizableSpace γ] [inst_9 : BorelSpace γ]
  [inst_10 : SecondCountableTopologyEither β γ] [inst_11 : MeasurableSpace δ]
  [inst_12 : TopologicalSpace.PseudoMetrizableSpace δ] [inst_13 : OpensMeasurableSpace δ]
  [inst_14 : SecondCountableTopology δ] (g g_1 : β → γ → δ) (e_g : g = g_1) (hg : Measurable (Function.uncurry g))
  (f₁ f₁_1 : α →ₘ[μ] β),
  f₁ = f₁_1 →
    ∀ (f₂ f₂_1 : α →ₘ[μ] γ),
      f₂ = f₂_1 →
        MeasureTheory.AEEqFun.comp₂Measurable g hg f₁ f₂ = MeasureTheory.AEEqFun.comp₂Measurable g_1 ⋯ f₁_1 f₂_1
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `η ▷ f` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.evalWhiskerRight : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.Mor₁ →
              Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableAdd₂.mk : ∀ {M : Type u_2} [inst : MeasurableSpace M] [inst_1 : Add M], (Measurable fun p => p.1 + p.2) → MeasurableAdd₂ M
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientGroup.instSeminormedCommGroup.eq_1 : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] (S : Subgroup M),
  QuotientGroup.instSeminormedCommGroup S =
    { toNorm := QuotientGroup.groupSeminorm.toSeminormedCommGroup.toNorm,
      toCommGroup := QuotientGroup.groupSeminorm.toSeminormedCommGroup.toCommGroup,
      toDist := QuotientGroup.groupSeminorm.toSeminormedCommGroup.toDist, dist_self := ⋯, dist_comm := ⋯,
      dist_triangle := ⋯, edist := PseudoMetricSpace.edist, edist_dist := ⋯,
      toUniformSpace := IsTopologicalGroup.leftUniformSpace (M ⧸ S), uniformity_dist := ⋯,
      toBornology := PseudoMetricSpace.toBornology, cobounded_sets := ⋯, dist_eq := ⋯ }
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_add_le' : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : α → E},
  MeasureTheory.MemLp g p μ →
    1 ≤ p → MeasureTheory.lpNorm (f + g) p μ ≤ MeasureTheory.lpNorm f p μ + MeasureTheory.lpNorm g p μ
-- Mathlib.Combinatorics.Matroid.Sum
/-- The sum of an indexed family `M : ι → Matroid α` of matroids on the same type,
as a matroid on the product type `ι × α`.  -/
Matroid.sum' : {α : Type u_1} → {ι : Type u_2} → (ι → Matroid α) → Matroid (ι × α)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instBraidedCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.AddGrp.instBraidedCategory =
    CategoryTheory.BraidedCategory.ofFaithful (CategoryTheory.AddGrp.forget₂Mon C)
      (fun G H => CategoryTheory.AddGrp.mkIso (β_ G.X H.X) ⋯ ⋯) ⋯
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.toFun_div : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Div β] (f g : UniformOnFun α β 𝔖),
  (UniformOnFun.toFun 𝔖) (f / g) = (UniformOnFun.toFun 𝔖) f / (UniformOnFun.toFun 𝔖) g
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAtChain_iff : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAtChain pat pos₁ pos₂ ↔
    ∃ (h : pos₁ ≤ pos₂), ∃ n, (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat)
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.refl_symm_apply : ∀ (X : Type u) [inst : TopologicalSpace X] (a : X), (ContinuousMap.HomotopyEquiv.refl X).symm.toFun a = a
-- Init.Data.UInt.Bitwise
UInt64.toUInt8_shiftLeft_mod : ∀ (a b : UInt64), (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)],
  (t₁ \ t₂).get! k = if k ∈ t₂ then default else t₁.get! k
-- Std.Data.ExtTreeMap.Basic
/-- Returns the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.ExtTreeMap.keyAtIdx! : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeMap α β cmp → ℕ → α
-- Mathlib.Analysis.Convex.Body
ConvexBody.instZero : {V : Type u_1} → [inst : TopologicalSpace V] → [inst_1 : AddCommGroup V] → [inst_2 : Module ℝ V] → Zero (ConvexBody V)
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.restrictPreimage_bijective`. -/
Function.Bijective.restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β},
  Function.Bijective f → Function.Bijective (t.restrictPreimage f)
-- Init.Data.Range.Polymorphic.Map
/-- Compatibility class for `Map` and `Rxc.HasSize`.  -/
Std.PRange.UpwardEnumerable.Map.PreservesRxcSize : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : Std.PRange.UpwardEnumerable β] →
        [Std.Rxc.HasSize α] → [Std.Rxc.HasSize β] → Std.PRange.UpwardEnumerable.Map α β → Prop
-- Mathlib.Algebra.Module.Injective
/-- **Baer's criterion** for injective module : a Baer module is an injective module, i.e. if every
linear map from an ideal can be extended, then the module is injective.  -/
Module.Baer.injective : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q],
  Module.Baer R Q → Module.Injective R Q