mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Basic
/-- Returns the number of mappings present in the map.  -/
Std.TreeMap.size : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → ℕ
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- For all `m ≤ n`, `truncation m` factors through `Truncated n`.  -/
CategoryTheory.SimplicialObject.truncationCompTrunc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n m : ℕ} →
      (h : m ≤ n) →
        (CategoryTheory.SimplicialObject.truncation n).comp (CategoryTheory.SimplicialObject.Truncated.trunc C n m ⋯) ≅
          CategoryTheory.SimplicialObject.truncation m
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.ext_iff : ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : Turing.ListBlank Γ}, L₁ = L₂ ↔ ∀ (i_1 : ℕ), L₁.nth i_1 = L₂.nth i_1
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.preOmega_of_omega0_sq_le : ∀ {o : Ordinal.{u_1}}, Ordinal.omega0 ^ 2 ≤ o → Ordinal.preOmega o = Ordinal.omega o
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
/-- A variant of `RootPairing.pairing` for root pairings which are valued in a smaller set of
coefficients.

Note that it is uniquely-defined only when the map `S → R` is injective, i.e., when we have
`[FaithfulSMul S R]`.  -/
RootPairing.pairingIn : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (P : RootPairing ι R M N) →
                    (S : Type u_6) → [inst_5 : CommRing S] → [inst_6 : Algebra S R] → [P.IsValuedIn S] → ι → ι → S
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- The underlying object in the ambient monoidal category  -/
CategoryTheory.CommGrp.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.CommGrp C → C
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instPretriangulated : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.Pretriangulated (DerivedCategory C)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Two simplices are equal if and only if they have the same points.  -/
Affine.Simplex.ext_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} {s1 s2 : Affine.Simplex k P n},
  s1 = s2 ↔ ∀ (i : Fin (n + 1)), s1.points i = s2.points i
-- Mathlib.Tactic.Linarith.Preprocessing
/-- **Alias** of `Mathlib.Tactic.Linarith.removeNeAux`.

---

`removeNeAux` case splits on any proof `h : a ≠ b` in the input,
turning it into `a < b ∨ a > b`, provided the type has a `LinearOrder` instance.
This produces `2^n` branches when there are `n` such hypotheses in the input.
 -/
Mathlib.Tactic.Linarith.removeNe_aux : Lean.MVarId → List Lean.Expr → Lean.MetaM (List Mathlib.Tactic.Linarith.Branch)
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.instInhabitedResult : Inhabited Lean.Meta.MonadSimp.Result
-- Mathlib.Order.BooleanAlgebra.Set
Set.ssubset_iff_sdiff_singleton : ∀ {α : Type u_1} {s t : Set α}, s ⊂ t ↔ ∃ a ∈ t, s ⊆ t \ {a}
-- Std.Time.Date.Unit.Weekday
Std.Time.instInhabitedWeekday : Inhabited Std.Time.Weekday
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.mk : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : Module R A] →
            [inst_3 : AddCommMonoid B] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] →
                  [inst_6 : CoalgebraStruct R B] →
                    (toLinearMap : A →ₗ[R] B) →
                      CoalgebraStruct.counit ∘ₗ toLinearMap = CoalgebraStruct.counit →
                        TensorProduct.map toLinearMap toLinearMap ∘ₗ CoalgebraStruct.comul =
                            CoalgebraStruct.comul ∘ₗ toLinearMap →
                          A →ₗc[R] B
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_iff_nat_mul_le_aux : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  ((∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖) → (f =o[l] g ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instDivisionAddCommMonoid : {α : Type u_1} → [SubtractionCommMonoid α] → SubtractionCommMonoid (Lex α)
-- Mathlib.CategoryTheory.Equivalence
/-- The inverse of the counit of an equivalence of categories.  -/
CategoryTheory.Equivalence.counitInv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) → CategoryTheory.Functor.id D ⟶ e.inverse.comp e.functor
-- Mathlib.Topology.Maps.Proper.Basic
/-- Any product of proper maps is proper.  -/
IsProperMap.pi_map : ∀ {ι : Type u_5} {X : ι → Type u_6} {Y : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (Y i)] {f : (i : ι) → X i → Y i},
  (∀ (i : ι), IsProperMap (f i)) → IsProperMap fun x i => f i (x i)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_sup_distrib_right : ∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderTop α] (s : Finset ι) (f : ι → α) (a : α),
  s.inf f ⊔ a = s.inf fun i => f i ⊔ a
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.smeval_add : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : Module R S] [inst_3 : Monoid S]
  (f g : LaurentPolynomial R) (x : Sˣ), (f + g).smeval x = f.smeval x + g.smeval x
-- Mathlib.Algebra.Order.Group.End
OrderHom.instOne : {α : Type u_1} → [inst : Preorder α] → One (α →o α)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.sumLexMap_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  {u : δ → δ → Prop} (f : r ↪r s) (g : t ↪r u) (a : α ⊕ γ), (f.sumLexMap g) a = Sum.map (⇑f) (⇑g) a
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.mk.sizeOf_spec : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : SizeOf K] [inst_4 : SizeOf V] (carrier : Set (Projectivization K V))
  (mem_add' :
    ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
      Projectivization.mk K v hv ∈ carrier →
        Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier),
  sizeOf { carrier := carrier, mem_add' := mem_add' } = 1
-- Batteries.Data.Fin.Coding
Fin.encodePi.eq_1 : ∀ (x_2 : Fin 0 → ℕ) (x_3 : (i : Fin 0) → Fin (x_2 i)), Fin.encodePi x_2 x_3 = ⟨0, ⋯⟩
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.mem_invariants : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V] {π : ContRepresentation R G V}
  (v : V), v ∈ π.invariants ↔ ∀ (g : G), (π g) v = v
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- If `M` is commutative, we only need to check the left condition `x ∈ s`.  -/
Submonoid.MulSaturated.of_left : ∀ {M : Type u_2} [inst : CommMonoid M] {s : Submonoid M}, (∀ ⦃x y : M⦄, x * y ∈ s → x ∈ s) → s.MulSaturated
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Nat.iterate.match_1.eq_1 : ∀ {α : Sort u_2} (motive : ℕ → α → Sort u_1) (a : α) (h_1 : (a : α) → motive 0 a)
  (h_2 : (k : ℕ) → (a : α) → motive k.succ a),
  (match 0, a with
    | 0, a => h_1 a
    | k.succ, a => h_2 k a) =
    h_1 a
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_monotone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), Monotone (CategoryTheory.Sieve.functorPushforward F)
-- Mathlib.Combinatorics.Additive.CauchyDavenport
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.DevosMulRel.congr_simp : ∀ {α : Type u_2} [inst : Group α] {inst_1 : DecidableEq α} [inst_2 : DecidableEq α] (a a_1 : Finset α × Finset α),
  a = a_1 → ∀ (a_2 a_3 : Finset α × Finset α), a_2 = a_3 → DevosMulRel✝ a a_2 = DevosMulRel✝ a_1 a_3
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getEntry?_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α},
  Std.DHashMap.Internal.AssocList.getEntry? a l = Std.Internal.List.getEntry? a l.toList
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.symm_Λ₀_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) (s : ℂ),
  P.symm.Λ₀ s = P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / (↑P.k - s)) • P.f₀
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.size_glue : ∀ {α : Type u} {β : α → Type v} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced} {hr : r.Balanced}
  {hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size}, (l.glue r hl hr hlr).size = l.size + r.size
-- Init.Data.Array.Lemmas
Array.foldr_flatten' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {b : β} {xss : Array (Array α)} {start : ℕ},
  start = xss.flatten.size → Array.foldr f b xss.flatten start = Array.foldr (fun xs b => Array.foldr f b xs) b xss
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeReachable.reachable : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u v : V}, k ≠ 0 → G.IsEdgeReachable k u v → G.Reachable u v
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- Extension for the `positivity` tactic: `UpperHalfPlane.coe`.  -/
Mathlib.Meta.Positivity.evalUpperHalfPlaneCoe : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Order.Atoms
Set.instIsCoatomistic : ∀ {α : Type u_2}, IsCoatomistic (Set α)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_app : ∀ {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) (a b : ℤ) (h : a ≤ b) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.truncGEδLT a).app X)
      ((CategoryTheory.shiftFunctor C 1).map ((t.natTransTruncLTOfLE a b h).app X)) =
    CategoryTheory.CategoryStruct.comp ((t.natTransTruncGEOfLE a b h).app X) ((t.truncGEδLT b).app X)
-- Std.Http.Data.Response
Std.Http.Response.mk.sizeOf_spec : ∀ {t : Type} [inst : SizeOf t] (line : Std.Http.Response.Head) (body : t) (extensions : Std.Http.Extensions),
  sizeOf { line := line, body := body, extensions := extensions } = 1 + sizeOf line + sizeOf body + sizeOf extensions
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A variant of `lift_unique` with `Z` an initial object.  -/
CategoryTheory.WithInitial.liftToInitialUnique : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          (F : CategoryTheory.Functor C D) →
            (hZ : CategoryTheory.Limits.IsInitial Z) →
              (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) →
                (CategoryTheory.WithInitial.incl.comp G ≅ F) →
                  (G.obj CategoryTheory.WithInitial.star ≅ Z) → (G ≅ CategoryTheory.WithInitial.liftToInitial F hZ)
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- The subcollection of all the finite sequences of `uIoc` intervals consisting of
`uIoc (a i) (b i)`, `i < n` where `a i`, `b i` are all in `uIcc a b` for `i < n` and
`uIoc (a i) (b i)` are mutually disjoint for `i < n`. Technically the finite sequence
`uIoc (a i) (b i)`, `i < n` is represented by any `E : ℕ × (ℕ → ℝ × ℝ)` which satisfies
`E.1 = n` and `E.2 i = (a i, b i)` for `i < n`.  -/
AbsolutelyContinuousOnInterval.disjWithin : ℝ → ℝ → Set (ℕ × (ℕ → ℝ × ℝ))
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_id : ∀ {N : Type u_5} [inst : Group N] (K : Subgroup N), Subgroup.comap (MonoidHom.id N) K = K
-- Std.Time.Format.Basic
Std.Time.instInhabitedGenericFormat : {a : Std.Time.Awareness} → Inhabited (Std.Time.GenericFormat a)
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Enriched.Functor.natTransEquiv_symm_app_app_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F G : CategoryTheory.Functor C D) (f : F ⟶ G) {X : C}
  {a : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C (Type (max v' v u)))).obj X} (Y : C)
  {φ : X ⟶ Y},
  ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.natTransEquiv.symm f).app X)) a).app Y φ = f.app Y
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.map'_id : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : α → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g]
  (p : (b : α) → f b ⟶ g b), CategoryTheory.Limits.Sigma.map' id p = CategoryTheory.Limits.Sigma.map p
-- Init.Data.Order.PackageFactories
/-- This class entails `LE α`, `LT α`, `BEq α`, `Ord α`, `Min α` and `Max α` instances as well as proofs
that these operations represent the same linear order structure on `α`.
 -/
Std.LinearOrderPackage : Type u → Type u
-- Batteries.Recycling.MonadSatisfying.Array
Array.SatisfiesM_anyM_iff_exists : ∀ {m : Type → Type u_1} {α : Type u_2} {start stop : ℕ} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α}
  {q : Fin as.size → Prop},
  (∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])) →
    SatisfiesM (fun res => res = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i) (Array.anyM p as start stop)
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- A proof that `f` is equal, up to modification over a discrete set, to a product of `g` and
canonical factors prescribed by the divisor of `f`.
 -/
Complex.CanonicalDecomp.eventuallyEq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {R : ℝ},
  Complex.CanonicalDecomp f g R →
    f =ᶠ[Filter.codiscreteWithin (Metric.closedBall 0 R)]
      (∏ᶠ (u : ℂ), Complex.canonicalFactor R u ^ (-(MeromorphicOn.divisor f (Metric.ball 0 R)) u)) • g
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.normedAddGroup.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → NormedAddGroup (G i)],
  Pi.normedAddGroup =
    { toNorm := Pi.seminormedAddGroup.toNorm, toAddGroup := Pi.seminormedAddGroup.toAddGroup,
      toPseudoMetricSpace := Pi.seminormedAddGroup.toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counitInv_functor_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X : C),
  CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (e.functor.map (e.unitInv.app X)) =
    CategoryTheory.CategoryStruct.id (e.functor.obj X)
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.mulIsInitial_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C]
  {I : C} (X : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct X I] (hI : CategoryTheory.Limits.IsInitial I),
  (CategoryTheory.Limits.mulIsInitial X hI).inv = hI.to (X ⨯ I)
-- Init.Data.Int.DivMod.Lemmas
Int.negSucc_emod : ∀ (m : ℕ) {b : ℤ}, 0 < b → Int.negSucc m % b = b - 1 - ↑m % b
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNonAssocSemiringOfRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → NonAssocSemiring (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] → NonAssocSemiring (DirectLimit G f)
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- Two `R`-linear maps from `PolynomialModule R M` which are equal
after pre-composition with every `lsingle R a` are equal.  -/
PolynomialModule.hom_ext : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_7}
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] {f g : PolynomialModule R M →ₗ[R] M'},
  (∀ (a : ℕ), f ∘ₗ PolynomialModule.lsingle R a = g ∘ₗ PolynomialModule.lsingle R a) → f = g
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- The family of 2-morphisms out of a left Kan extension.  -/
CategoryTheory.Bicategory.LeftExtension.IsKan.desc : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          {t : CategoryTheory.Bicategory.LeftExtension f g} →
            t.IsKan → (s : CategoryTheory.Bicategory.LeftExtension f g) → t.extension ⟶ s.extension
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertMany.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {β : Type v} {ρ : Type w}
  [inst_2 : ForIn Id ρ (α × β)] (m m_1 : Std.ExtDHashMap α fun x => β),
  m = m_1 → ∀ (l l_1 : ρ), l = l_1 → Std.ExtDHashMap.Const.insertMany m l = Std.ExtDHashMap.Const.insertMany m_1 l_1
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.eraseKey.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k k_1 : α) (v : β k_1) (l : List ((a : α) × β a)),
  Std.Internal.List.eraseKey k (⟨k_1, v⟩ :: l) = bif k_1 == k then l else ⟨k_1, v⟩ :: Std.Internal.List.eraseKey k l
-- Mathlib.Analysis.Distribution.Support
Distribution.TemperedDistribution.dsupport_smulLeftCLM_subset : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℂ F] {f : TemperedDistribution E F} {g : E → ℂ},
  Function.HasTemperateGrowth g →
    Distribution.dsupport ⇑((TemperedDistribution.smulLeftCLM F g) f) ⊆ Distribution.dsupport ⇑f
-- Mathlib.Algebra.BigOperators.NatAntidiagonal
Finset.Nat.sum_antidiagonal_subst : ∀ {M : Type u_1} [inst : AddCommMonoid M] {n : ℕ} {f : ℕ × ℕ → ℕ → M},
  ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, f p n = ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, f p (p.1 + p.2)
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidalFunctor.eq_1 : ∀ {M : Type u} [inst : AddMonoid M] {N : Type u'} [inst_1 : AddMonoid N] (F : M →+ N),
  CategoryTheory.Discrete.addMonoidalFunctor F = CategoryTheory.Discrete.functor fun X => { as := F X }
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso],
  P.map (CategoryTheory.Functor.id C) = P
-- Mathlib.ModelTheory.Skolem
/-- Any `L.sum L.skolem₁`-substructure is an elementary `L`-substructure.  -/
FirstOrder.Language.Substructure.elementarySkolem₁Reduct : {L : FirstOrder.Language} →
  {M : Type w} →
    [inst : Nonempty M] → [inst_1 : L.Structure M] → (L.sum L.skolem₁).Substructure M → L.ElementarySubstructure M
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_submatrix_equiv : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (A : Matrix m m α) (e₁ e₂ : n ≃ m),
  (A.submatrix ⇑e₁ ⇑e₂)⁻¹ = A⁻¹.submatrix ⇑e₂ ⇑e₁
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k : α}
  {h' : k ∈ Std.DHashMap.Raw.filterMap f m} (h : m.WF), (Std.DHashMap.Raw.filterMap f m).getKey k h' = m.getKey k ⋯
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.cons.sizeOf_spec : ∀ {V : Type u} {G : SimpleGraph V} [inst : SizeOf V] {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  sizeOf (SimpleGraph.Walk.cons h p) = 1 + sizeOf u + sizeOf v + sizeOf w + sizeOf h + sizeOf p
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_eq_get!_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {a : α},
  t.get! a = (t.get? a).get!
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- A bilinear map is right-separating if and only if its flip has a trivial kernel.  -/
LinearMap.separatingRight_iff_flip_ker_eq_bot : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M}, B.SeparatingRight ↔ B.flip.ker = ⊥
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**: if `f : ℝ → E` is integrable on `a..b` and `f` is
continuous at `a` and `b`, then `(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u •
ca` at `(a, b)`.  -/
intervalIntegral.integral_hasFDerivAt : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
      StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
        ContinuousAt f a →
          ContinuousAt f b →
            HasFDerivAt (fun p => ∫ (x : ℝ) in p.1..p.2, f x)
              ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a)) (a, b)
-- Init.Data.String.Iterator
/-- Moves the iterator's position to the end of the string, just past the last character.
 -/
String.Legacy.Iterator.toEnd : String.Legacy.Iterator → String.Legacy.Iterator
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.exportIREntries : Lean.Environment → Array (Lean.Name × Array Lean.EnvExtensionEntry)
-- Init.Data.Int.Linear
Int.Internal.Linear.cdiv_eq_div_of_divides : ∀ {a b : ℤ}, a % b = 0 → a / b = Int.Internal.Linear.cdiv a b
-- Lean.Environment
_private.Lean.Environment.0.Lean.Kernel.Environment.mk.sizeOf_spec : ∀ (constants : Lean.ConstMap) (quotInit : Bool) (diagnostics : Lean.Kernel.Diagnostics)
  (const2ModIdx : Std.HashMap Lean.Name Lean.ModuleIdx) (extensions irBaseExts : Array Lean.EnvExtensionState)
  (header : Lean.EnvironmentHeader),
  sizeOf
      { constants := constants, quotInit := quotInit, diagnostics := diagnostics, const2ModIdx := const2ModIdx,
        extensions := extensions, irBaseExts := irBaseExts, header := header } =
    1 + sizeOf constants + sizeOf quotInit + sizeOf diagnostics + sizeOf const2ModIdx + sizeOf extensions +
        sizeOf irBaseExts +
      sizeOf header
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndepOn_sUnion_of_directed : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {s : Set (Set ι)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) s → (∀ a ∈ s, LinearIndepOn R v a) → LinearIndepOn R v (⋃₀ s)
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.instHasNoLoopIntUp : (ComplexShape.up ℤ).HasNoLoop