mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiableWithinAt_add_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x}
  {u : Set B} {x₀ : B}, MDiffAt[u] (T% s) x₀ → MDiffAt[u] (T% t) x₀ → (MDiffAt[u] fun x => ⟨x, (s + t) x⟩) x₀
-- Mathlib.NumberTheory.Cyclotomic.Gal
PowerBasis.equivOfMinpoly.congr_simp : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb pb_1 : PowerBasis A S) (e_pb : pb = pb_1) (pb' pb'_1 : PowerBasis A S')
  (e_pb' : pb' = pb'_1) (h : minpoly A pb.gen = minpoly A pb'.gen),
  pb.equivOfMinpoly pb' h = pb_1.equivOfMinpoly pb'_1 ⋯
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.exists_finpartition_sdiff : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α}, MeasureTheory.IsSetSemiring C → s ∈ C → t ∈ C → ∃ P, ↑P.parts ⊆ C
-- Mathlib.Analysis.Normed.Module.Ball.Action
isScalarTower_sphere_ball_ball : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'],
  IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.ball 0 1) ↑(Metric.ball 0 1)
-- Std.Time.Date.Unit.Month
/-- Size in days of each month if the year is not a leap year.
 -/
_private.Std.Time.Date.Unit.Month.0.Std.Time.Month.Ordinal.monthSizesNonLeap : { val // val.size = 12 }
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toHomeomorph_refl : ∀ {X : Type u_1} [inst : TopologicalSpace X], (Equiv.refl X).toHomeomorph ⋯ = Homeomorph.refl X
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A `C^n` local diffeomorphism on `s` is `C^n` on `s`.  -/
IsLocalDiffeomorphOn.contMDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {s : Set M},
  IsLocalDiffeomorphOn I J n f s → ContMDiffOn I J n f s
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Composition of inverse and coercion from the subtype of the target.  -/
Bundle.Pretrivialization.setSymm : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] → {proj : Z → B} → (e : Bundle.Pretrivialization F proj) → ↑e.target → Z
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_toDual : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α),
  Set.uIoo (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.uIoo a b
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivAt.hasMFDerivWithinAt : ∀ {𝕜 : 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'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt% f x f' → HasMFDerivAt[s] f x f'
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.inf_addSubgroupOf_inf_normal_of_left : ∀ {G : Type u_1} [inst : AddGroup G] {A' A : AddSubgroup G} (B : AddSubgroup G) [hN : (A'.addSubgroupOf A).Normal],
  ((A' ⊓ B).addSubgroupOf (A ⊓ B)).Normal
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.trunc_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (n : σ →₀ ℕ),
  n ≠ 0 → ∀ (a : R), (MvPowerSeries.trunc R n) (MvPowerSeries.C a) = MvPolynomial.C a
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.split : {α : Type u_1} → Lean.PArray α → (α → ℤ) → Lean.PArray α × Array (ℤ × α)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a b : α}, (a == b) = true → m[a]? = m[b]?
-- Mathlib.CategoryTheory.Sites.Hypercover.One
_private.Mathlib.CategoryTheory.Sites.Hypercover.One.0.CategoryTheory.PreOneHypercover.Hom.mapMulticospan.match_3.eq_2 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  (motive : (X Y : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape) → (X ⟶ Y) → Sort u_4)
  (i : E.multicospanShape.R)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape) →
      motive x x (CategoryTheory.Limits.WalkingMulticospan.Hom.id x))
  (h_2 :
    (i : E.multicospanShape.R) →
      motive (CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.fst i))
        (CategoryTheory.Limits.WalkingMulticospan.right i) (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i))
  (h_3 :
    (i : E.multicospanShape.R) →
      motive (CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.snd i))
        (CategoryTheory.Limits.WalkingMulticospan.right i) (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i)),
  (match CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.fst i),
      CategoryTheory.Limits.WalkingMulticospan.right i, CategoryTheory.Limits.WalkingMulticospan.Hom.fst i with
    | x, .(x), CategoryTheory.Limits.WalkingMulticospan.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.fst i)),
      .(CategoryTheory.Limits.WalkingMulticospan.right i), CategoryTheory.Limits.WalkingMulticospan.Hom.fst i => h_2 i
    | .(CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.snd i)),
      .(CategoryTheory.Limits.WalkingMulticospan.right i), CategoryTheory.Limits.WalkingMulticospan.Hom.snd i =>
      h_3 i) =
    h_2 i
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.rid_comp_map_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid M'] [inst_8 : Module R M'] (f : M →ₗ[R] M')
  (g : N →ₗ[R] R) (h : P →ₗ[R] TensorProduct R M N),
  ↑(TensorProduct.rid R M') ∘ₗ TensorProduct.map f g ∘ₗ h =
    f ∘ₗ ↑(TensorProduct.rid R M) ∘ₗ TensorProduct.map LinearMap.id g ∘ₗ h
-- Mathlib.Topology.DiscreteSubset
/-- The union of finitely many discrete closed subsets is discrete.  -/
discreteTopology_union : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S T : Set X},
  DiscreteTopology ↑S → DiscreteTopology ↑T → IsClosed S → IsClosed T → DiscreteTopology ↑(S ∪ T)
-- Mathlib.Data.Set.Image
Subtype.preimage_coe_inter_self : ∀ {α : Type u_1} (s t : Set α), Subtype.val ⁻¹' (t ∩ s) = Subtype.val ⁻¹' t
-- Lean.Expr
_private.Lean.Expr.0.Lean.propEq : Lean.Expr
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
hfdifferential.congr_simp : ∀ {𝕜 : 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'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f_1 : ContMDiffMap I I' M M' ↑⊤}
  (e_f : f = f_1) {x : M} {y : M'} (h : f x = y), hfdifferential h = hfdifferential ⋯
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.Hom.ext : ∀ {X : UniformSpaceCat} {Y : UniformSpaceCat} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Functor.mapTriangleIdIso C).hom.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃
-- Mathlib.GroupTheory.Congruence.Hom
/-- A monoid homomorphism `f` induces an injective homomorphism on the quotient by `f`'s kernel.  -/
Con.kerLift_injective : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (f : M →* P),
  Function.Injective ⇑(Con.kerLift f)
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR.run.match_1.eq_1 : ∀ {α : Type u_1} (n : ℕ) (motive : { l // l.length = (n + 2 + 1) / 2 } × { l // l.length = (n + 2) / 2 } → Sort u_2)
  (l : { l // l.length = (n + 2 + 1) / 2 }) (r : { l // l.length = (n + 2) / 2 })
  (h_1 : (l : { l // l.length = (n + 2 + 1) / 2 }) → (r : { l // l.length = (n + 2) / 2 }) → motive (l, r)),
  (match (l, r) with
    | (l, r) => h_1 l r) =
    h_1 l r
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_ofInt : ∀ {d : ℤ} (n : ℤ), (Zsqrtd.ofInt n).im = 0
-- Mathlib.RingTheory.Noetherian.Defs
isNoetherian_iff_fg_wellFounded : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsNoetherian R M ↔ WellFoundedGT { N // N.FG }
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_eq_integral_probChar : ∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [inst : SeminormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] (t : E), MeasureTheory.charFun μ t = ∫ (x : E), ↑(Real.probChar (inner ℝ x t)) ∂μ
-- Mathlib.Order.Basic
Pi.instHNot.eq_1 : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → HNot (π i)], Pi.instHNot = { hnot := fun x i => ￢x i }
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.toMonoidHom_symm_extendScalarsHomOfSurjective : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A]
  (h : Function.Surjective ⇑(algebraMap R S)),
  ↑(AlgEquiv.extendScalarsHomOfSurjective h).symm = AlgEquiv.restrictScalarsHom R
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.tendsto_zero_iff : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {f'' : α → E''} {g'' : α → F''} {l : Filter α},
  f'' =Θ[l] g'' → (Filter.Tendsto f'' l (nhds 0) ↔ Filter.Tendsto g'' l (nhds 0))
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.monadMap_trans : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {o : Type u → Type u_1} {n : Type u → Type u_2} {α : Type u}
  {f : {β : Type u} → m β → m β} {x : o α} {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP o ps]
  [inst_1 : MonadFunctor n o] [inst_2 : MonadFunctorT m n],
  ⦃(Std.Do.wp (MonadFunctor.monadMap (fun {β} => monadMap fun {β} => f) x)).apply Q⦄ monadMap f x ⦃Q⦄
-- Mathlib.GroupTheory.Goursat
AddSubgroup.mem_goursatFst : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {I : AddSubgroup (G × H)} {g : G},
  g ∈ I.goursatFst ↔ (g, 0) ∈ I
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact
IsBaseChange.of_right_exact : ∀ {R : Type u_1} [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S] {M₁ : Type u_3}
  {M₂ : Type u_4} {M₃ : Type u_5} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} [inst_3 : AddCommGroup M₁]
  [inst_4 : AddCommGroup M₂] [inst_5 : AddCommGroup M₃] [inst_6 : AddCommGroup N₁] [inst_7 : AddCommGroup N₂]
  [inst_8 : AddCommGroup N₃] [inst_9 : Module R M₁] [inst_10 : Module R M₂] [inst_11 : Module R M₃]
  [inst_12 : Module R N₁] [inst_13 : Module R N₂] [inst_14 : Module R N₃] [inst_15 : Module S N₁]
  [inst_16 : Module S N₂] [inst_17 : Module S N₃] [inst_18 : IsScalarTower R S N₁] [inst_19 : IsScalarTower R S N₂]
  [inst_20 : IsScalarTower R S N₃] (h₁ : M₁ →ₗ[R] N₁) (h₂ : M₂ →ₗ[R] N₂) (h₃ : M₃ →ₗ[R] N₃) {f : M₁ →ₗ[R] M₂}
  {g : M₂ →ₗ[R] M₃} {f' : N₁ →ₗ[S] N₂} {g' : N₂ →ₗ[S] N₃},
  h₂ ∘ₗ f = ↑R f' ∘ₗ h₁ →
    h₃ ∘ₗ g = ↑R g' ∘ₗ h₂ →
      IsBaseChange S h₁ →
        IsBaseChange S h₂ →
          Function.Exact ⇑f ⇑g →
            Function.Surjective ⇑g → Function.Exact ⇑f' ⇑g' → Function.Surjective ⇑g' → IsBaseChange S h₃
-- Mathlib.Data.Set.Function
Set.InvOn.mono : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} {f : α → β} {f' : β → α},
  Set.InvOn f' f s t → s₁ ⊆ s → t₁ ⊆ t → Set.InvOn f' f s₁ t₁
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' : ∀ {E : Type u_1} {X : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : TopologicalSpace X]
  {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {f : X → ℝ → E}, Continuous (Function.uncurry f) → ∀ (a₀ b₀ : ℝ), Continuous fun x => ∫ (t : ℝ) in a₀..b₀, f x t ∂μ
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
/-- Implementation: This is a construction which will be used in the proof that
the sieve generated by a single arrow is effective epimorphic if and only if
the arrow is an effective epi.
 -/
CategoryTheory.isColimitOfEffectiveEpiStruct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : Y ⟶ X) →
        CategoryTheory.EffectiveEpiStruct f →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Sieve.generateSingleton f).arrows.cocone
-- Mathlib.Data.Int.Lemmas
Int.div2_bit : ∀ (b : Bool) (n : ℤ), (Int.bit b n).div2 = n
-- Mathlib.Data.Multiset.Count
Multiset.ext'_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s = t ↔ ∀ (a : α), Multiset.count a s = Multiset.count a t
-- Std.Data.HashMap.Lemmas
Std.HashMap.forM_eq_forM_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → m' PUnit.{w + 1}}, (forM m fun a => f a.1) = m.keys.forM f
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.Indep.isBase_of_cRank_le : ∀ {α : Type u} {M : Matroid α} {I : Set α} [M.RankFinite], M.Indep I → M.cRank ≤ Cardinal.mk ↑I → M.IsBase I
-- Batteries.Data.List.Basic
List.tails.eq_def : ∀ {α : Type u_1} (x : List α),
  x.tails =
    match x with
    | [] => [[]]
    | a :: l => (a :: l) :: l.tails
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instT2Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T2Space M], T2Space Mᵈᵃᵃ
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.diagramObj.eq_2 : ∀ {ι : Type v} {α : Type u} (U : ι → α) [inst : SemilatticeInf α] (a a_1 : ι),
  CategoryTheory.Pairwise.diagramObj U (CategoryTheory.Pairwise.pair a a_1) = U a ⊓ U a_1
-- Mathlib.Topology.Algebra.GroupWithZero
/-- Eta-expanded form of `ContinuousOn.inv₀` -/
ContinuousOn.fun_inv₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  {f : α → G₀} {s : Set α} [inst_4 : TopologicalSpace α],
  ContinuousOn f s → (∀ x ∈ s, f x ≠ 0) → ContinuousOn (fun i => (f i)⁻¹) s
-- Init.System.ST
/-- Replaces the value of a mutable reference.
 -/
ST.Ref.set : {σ : Type} → {m : Type → Type} → [MonadLiftT (ST σ) m] → {α : Type} → ST.Ref σ α → α → m Unit
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.transport : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D)
  (G : CategoryTheory.Functor D C) {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [G.IsCoverDense J]
  [G.Full] [inst_5 : G.IsContinuous K J] [(G.sheafPushforwardContinuous A K J).EssSurj] [G.IsCocontinuous K J]
  {FA : A → A → Type u_1} {CA : A → Type u_2} [inst_8 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_9 : CategoryTheory.ConcreteCategory A FA] [K.WEqualsLocallyBijective A],
  CategoryTheory.CoverPreserving K J G → J.WEqualsLocallyBijective A
-- Batteries.Data.Array.Basic
/-- Find the first maximal element of an array. If the array is empty, `d` is
returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered.
 -/
Array.rangeMaxD : {α : Type u_1} → [ord : Ord α] → (xs : Array α) → α → optParam ℕ 0 → optParam ℕ xs.size → α
-- Lean.Data.Lsp.CodeActions
/-- Code actions were explicitly requested by the user or by an extension.  -/
Lean.Lsp.CodeActionTriggerKind.invoked : Lean.Lsp.CodeActionTriggerKind
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_int_mul_two_pi_sub : ∀ (x : ℂ) (n : ℤ), Complex.sin (↑n * (2 * ↑Real.pi) - x) = -Complex.sin x
-- Mathlib.Data.Matrix.Basis
Matrix.sum_single_intCast : ∀ {m : Type u_2} {α : Type u_7} [inst : DecidableEq m] [inst_1 : AddCommGroupWithOne α] [inst_2 : Fintype m] (z : ℤ),
  ∑ i, Matrix.single i i ↑z = ↑z
-- Mathlib.RingTheory.LocalRing.Pullback
RingHom.pullback_comm_sq : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Semiring T] (f : R →+* T)
  (g : S →+* T), f.comp (f.pullbackFst g) = g.comp (f.pullbackSnd g)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.denoteInt_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (k : ℤ), Lean.Grind.CommRing.denoteInt k = ↑k
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.numerator_isUnit : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (s : ↥S),
  IsUnit (OreLocalization.numeratorHom ↑s)
-- Mathlib.Topology.PartialHomeomorph.Basic
/-- The identity on the whole space as a partial homeomorphism.  -/
PartialHomeomorph.refl : (X : Type u_7) → [inst : TopologicalSpace X] → PartialHomeomorph X X
-- Mathlib.Topology.Connected.Clopen
IsClopen.isPreconnected_iff : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  IsClopen s →
    (IsPreconnected s ↔ ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b)
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.iteratedLineDerivOp_one : ∀ {V : Type u_11} {E : Type u_12} [inst : LineDeriv V E E] (m : Fin 1 → V) (f : E),
  LineDeriv.iteratedLineDerivOp m f = LineDeriv.lineDerivOp (m 0) f
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.localTrivAt_def : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (b : B),
  Z.localTriv (Z.indexAt b) = Z.localTrivAt b
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.support_truncLT : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : PartialOrder Γ] [inst_2 : DecidableLT Γ] (c : Γ)
  (x : HahnSeries Γ R), ((HahnSeries.truncLT c) x).support = {y | y ∈ x.support ∧ y < c}
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
/-- Sections of `F.op ⋙ yoneda.obj X` identify to natural
transformations `F ⟶ (const J).obj X`.  -/
CategoryTheory.Limits.opCompYonedaSectionsEquiv : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        (F : CategoryTheory.Functor J C) →
          (X : C) → ↑(F.op.comp (CategoryTheory.yoneda.obj X)).sections ≃ (F ⟶ (CategoryTheory.Functor.const J).obj X)
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.Compl.adjDecidable : (V : Type u_2) → (G : Digraph V) → [DecidableRel G.Adj] → DecidableRel Gᶜ.Adj
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- Hecke coset module data compose. Not an instance, since the middle subgroup cannot be
inferred from the goal.  -/
IsHeckeTriple.trans : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₁ H₂ H₃ : Subgroup G} [IsHeckeTriple Δ H₁ H₂]
  [IsHeckeTriple Δ H₂ H₃], IsHeckeTriple Δ H₁ H₃
-- Std.Data.DHashMap.Raw
/-- Inserts multiple mappings into the hash map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insertMany` function on `HashSet` and `HashSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.DHashMap.Raw.insertMany : {α : Type u} →
  {β : α → Type v} →
    [BEq α] →
      [Hashable α] → {ρ : Type w} → [ForIn Id ρ ((a : α) × β a)] → Std.DHashMap.Raw α β → ρ → Std.DHashMap.Raw α β
-- Mathlib.MeasureTheory.Measure.Decomposition.Hahn
MeasureTheory.exists_isHahnDecomposition : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν], ∃ s, MeasureTheory.IsHahnDecomposition μ ν s
-- Mathlib.Algebra.Polynomial.Laurent
/-- The map which substitutes `T ↦ T⁻¹` into a Laurent polynomial.  -/
LaurentPolynomial.invert : {R : Type u_3} → [inst : CommSemiring R] → LaurentPolynomial R ≃ₐ[R] LaurentPolynomial R
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.equivHom_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (F G : CochainComplex C ℤ) (z : CochainComplex.HomComplex.Cocycle F G 0),
  (CochainComplex.HomComplex.Cocycle.equivHom F G).symm z = z.homOf
-- Mathlib.Order.UpperLower.Closure
/-- The least lower set containing a given set.  -/
lowerClosure : {α : Type u_1} → [inst : Preorder α] → Set α → LowerSet α
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Subtracting two points in the affine span produces a vector in the spanning submodule.  -/
vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p₁ p₂ : P},
  p₁ ∈ affineSpan k s → p₂ ∈ affineSpan k s → p₁ -ᵥ p₂ ∈ vectorSpan k s
-- Mathlib.Data.Nat.Bits
Nat.shiftLeft'.eq_def : ∀ (b : Bool) (m x : ℕ),
  Nat.shiftLeft' b m x =
    match x with
    | 0 => m
    | n.succ => Nat.bit b (Nat.shiftLeft' b m n)
-- Mathlib.CategoryTheory.Monoidal.Arrow
/-- The monoidal category instance induced by the pushout-product.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.instMonoidalCategoryStructArrowOfHasPushoutsOfHasInitialOfMonoidalClosedOfBraidedCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasPushouts C] →
      [CategoryTheory.Limits.HasInitial C] →
        [inst_3 : CategoryTheory.CartesianMonoidalCategory C] →
          [CategoryTheory.MonoidalClosed C] →
            [CategoryTheory.BraidedCategory C] → CategoryTheory.MonoidalCategoryStruct (CategoryTheory.Arrow C)
-- Mathlib.Combinatorics.SimpleGraph.Partition
/-- Create a coloring using the parts themselves as the colors.
Each vertex is colored by the part it's contained in.  -/
SimpleGraph.Partition.toColoring : {V : Type u} → {G : SimpleGraph V} → (P : G.Partition) → G.Coloring ↑P.parts
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Constructs a morphism from `star` to `of X`.  -/
CategoryTheory.WithInitial.homTo : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) → CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.incl.obj X
-- Mathlib.Data.List.Sigma
List.mem_keys_kinsert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {b' : β a'} {l : List (Sigma β)},
  a ∈ (List.kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys