mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Adjunction
CategoryTheory.Adjunction.localization_counit_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) (L₁ : CategoryTheory.Functor C₁ D₁) (W₁ : CategoryTheory.MorphismProperty C₁)
  [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (W₂ : CategoryTheory.MorphismProperty C₂)
  [inst_5 : L₂.IsLocalization W₂] (G' : CategoryTheory.Functor D₁ D₂) (F' : CategoryTheory.Functor D₂ D₁)
  [inst_6 : CategoryTheory.CatCommSq G L₁ L₂ G'] [inst_7 : CategoryTheory.CatCommSq F L₂ L₁ F'] (X₂ : C₂),
  (adj.localization L₁ W₁ L₂ W₂ G' F').counit.app (L₂.obj X₂) =
    CategoryTheory.CategoryStruct.comp (G'.map ((CategoryTheory.CatCommSq.iso F L₂ L₁ F').inv.app X₂))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂))
        (L₂.map (adj.counit.app X₂)))
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.sourceHomeomorphBaseSetProd_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) (p : ↑e.source),
  e.sourceHomeomorphBaseSetProd p = (⟨proj ↑p, ⋯⟩, (↑e ↑p).2)
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Extend a `SimpleFunc` along a measurable embedding: `f₁.extend g hg f₂` is the function
`F : β →ₛ γ` such that `F ∘ g = f₁` and `F y = f₂ y` whenever `y ∉ range g`.  -/
MeasureTheory.SimpleFunc.extend : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        [inst_1 : MeasurableSpace β] →
          MeasureTheory.SimpleFunc α γ →
            (g : α → β) → MeasurableEmbedding g → MeasureTheory.SimpleFunc β γ → MeasureTheory.SimpleFunc β γ
-- Mathlib.Order.Filter.Extr
/-- If `f` is monotone on `Icc a b` and antitone on `Ico b c`, then the maximum of `f` on
`Ico a c` is attained at `b`.  -/
isMaxOn_Ico_of_mono_anti : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b c : α} {f : α → β},
  MonotoneOn f (Set.Icc a b) → AntitoneOn f (Set.Ico b c) → IsMaxOn f (Set.Ico a c) b
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.measure_preimage_equiv : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α ≃ᵐ β},
  MeasureTheory.MeasurePreserving (⇑f) μa μb → ∀ (s : Set β), μa (⇑f ⁻¹' s) = μb s
-- Init.Data.BitVec.Lemmas
BitVec.msb_reverse : ∀ {w : ℕ} {x : BitVec w}, x.reverse.msb = x.getLsbD 0
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.seq.eq_2 : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A) (k : ℕ),
  H.seq f k.succ =
    H.seq f k +
      (PowerSeries.mk fun i =>
          (PowerSeries.coeff (i + ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat)) (f - g * H.seq f k)) *
        ↑⋯.unit⁻¹
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ιTotalOrZero_map_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K L : HomologicalComplex₂ C c₁ c₂)
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) {Z : C}
  (h : (L.total c₁₂).X i₁₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂)
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) h) =
    CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂)
      (CategoryTheory.CategoryStruct.comp (L.ιTotalOrZero c₁₂ i₁ i₂ i₁₂) h)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_succ_succ : ∀ {m n : ℤ}, ((m + 1)<...n + 1).toList = List.map (fun x => x + 1) (m<...n).toList
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- The *measurable atom* of `x` is the intersection of all the measurable sets containing `x`.
It is measurable when the space is countable (or more generally when the measurable space is
countably generated).  -/
measurableAtom : {β : Type u_2} → [MeasurableSpace β] → β → Set β
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.map₂ : ∀ {x y : ℝ*} {r s : ℝ},
  x.IsSt r →
    y.IsSt s →
      ∀ {f : ℝ → ℝ → ℝ}, ContinuousAt (Function.uncurry f) (r, s) → Hyperreal.IsSt (Filter.Germ.map₂ f x y) (f r s)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.isOpen : ∀ {α : Type u_2} [inst : TopologicalSpace α] (U : TopologicalSpace.Opens α), IsOpen ↑U
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.ofIsReflexivePair_hasColimit_of_hasCoequalizer : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B}
  [inst_1 : CategoryTheory.IsReflexivePair f g] [h : CategoryTheory.Limits.HasCoequalizer f g],
  CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.ofIsReflexivePair f g)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral norm is a `K`-algebra norm on `L`.  -/
spectralAlgNorm : (K : Type u_2) →
  [inst : NormedField K] →
    (L : Type u_3) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → [IsUltrametricDist K] → [h_alg : Algebra.IsAlgebraic K L] → AlgebraNorm K L
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.sumOfNonempty.congr_simp : ∀ {H : Type u} {M : Type u_2} {M' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] [inst_3 : Nonempty H],
  ChartedSpace.sumOfNonempty = ChartedSpace.sumOfNonempty
-- Mathlib.Control.Fold
Traversable.foldr.ofFreeMonoid_comp_of : ∀ {α β : Type u} (f : β → α → α), ⇑(Monoid.Foldr.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.Foldr.mk ∘ f
-- Mathlib.MeasureTheory.Measure.Prod
Measurable.map_prodMk_left : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν], Measurable fun x => MeasureTheory.Measure.map (Prod.mk x) ν
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- Isomorphism between the bar resolution and standard resolution, with `n`th map
`(Gⁿ →₀ k[G]) → k[Gⁿ⁺¹]` sending `(g₁, ..., gₙ) ↦ (1, g₁, g₁g₂, ..., g₁...gₙ)`.  -/
Rep.barComplex.isoStandardComplex : (k G : Type u) → [inst : CommRing k] → [inst_1 : Group G] → Rep.barComplex k G ≅ Rep.standardComplex k G
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesMap_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : M.HasHomology i] {Z : C} (h : M.opcycles i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap (CategoryTheory.CategoryStruct.comp φ ψ) i) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ψ i) h)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
left_sub_midpoint : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  (v₁ v₂ : V), v₁ - midpoint R v₁ v₂ = ⅟2 • (v₁ - v₂)
-- Init.Grind.Ring.Basic
Lean.Grind.CommSemiring.mul_left_comm : ∀ {α : Type u} [inst : Lean.Grind.CommSemiring α] (a b c : α), a * (b * c) = b * (a * c)
-- Mathlib.Algebra.Polynomial.Taylor
/-- `Polynomial.taylor` as an `AlgEquiv` for commutative rings.  -/
Polynomial.taylorEquiv : {R : Type u_1} → [inst : CommRing R] → R → Polynomial R ≃ₐ[R] Polynomial R
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.sinKernel_neg : ∀ (a : UnitAddCircle) (x : ℝ), HurwitzZeta.sinKernel (-a) x = -HurwitzZeta.sinKernel a x
-- Mathlib.Order.Basic
/-- A version of `ne_iff_lt_or_gt` with LHS and RHS reversed.  -/
lt_or_lt_iff_ne : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, a < b ∨ b < a ↔ a ≠ b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : β → β},
      (t.modify k f).isEmpty = false →
        ∀ {fallback : α},
          (t.modify k f).maxKeyD fallback = if cmp (t.maxKeyD fallback) k = Ordering.eq then k else t.maxKeyD fallback
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.mergeWith : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] (f : (a : α) → β a → β a → β a),
  t₁.Equiv t₂ → t₃.Equiv t₄ → (Std.DTreeMap.mergeWith f t₁ t₃).Equiv (Std.DTreeMap.mergeWith f t₂ t₄)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.w_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {j j' : J} (f : j' ⟶ j) {F' : C → C → Type uF}
  {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F' X Y) (carrier X) (carrier Y)}
  [inst_2 : CategoryTheory.ConcreteCategory C F'] (x : carrier (F.obj j')),
  (CategoryTheory.ConcreteCategory.hom (c.ι.app j)) ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (c.ι.app j')) x
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.unop_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ≅ Y), f.unop.op = f
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.lift_obj_mk : ∀ {V : SSet.Truncated 2} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  (obj : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 }) → D)
  (map :
    {x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })} →
      SSet.Truncated.Edge x y → (obj x ⟶ obj y))
  (map_id :
    ∀ (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })),
      map (SSet.Truncated.Edge.id x) = CategoryTheory.CategoryStruct.id (obj x))
  (map_comp :
    ∀ {x₀ x₁ x₂ : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
      {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
      (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂)
  (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })),
  (SSet.Truncated.HomotopyCategory.lift obj (fun {x y} => map) map_id ⋯).obj (SSet.Truncated.HomotopyCategory.mk x) =
    obj x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.mk.inj : ∀ {val : Lean.Expr} {ival? : Option ℤ} {val_1 : Lean.Expr} {ival?_1 : Option ℤ},
  { val := val, ival? := ival? } = { val := val_1, ival? := ival?_1 } → val = val_1 ∧ ival? = ival?_1
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- The extension of a functor to under categories behaves well with compositions.  -/
CategoryTheory.WithInitial.liftFromUnderComp : {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] →
            {X : C} →
              {K : CategoryTheory.Functor J (CategoryTheory.Under X)} →
                {F : CategoryTheory.Functor C D} →
                  CategoryTheory.WithInitial.liftFromUnder.obj (K.comp (CategoryTheory.Under.post F)) ≅
                    (CategoryTheory.WithInitial.liftFromUnder.obj K).comp F
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
Measurable.sup_of_left : ∀ {α : Type u_1} {β : Type u_2} {mα mα' : MeasurableSpace α} {x : MeasurableSpace β} {f : α → β},
  Measurable f → Measurable f
-- Mathlib.Data.Set.Lattice.Image
Set.biInter_range : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → Set β}, ⋂ x ∈ Set.range f, g x = ⋂ y, g (f y)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNonUnitalRingQuotient : {R : Type u_1} → [inst : NonUnitalRing R] → (c : RingCon R) → NonUnitalRing c.Quotient
-- Mathlib.Algebra.Category.BoolRing
BoolRing.Iso.mk_inv_hom' : ∀ {α β : BoolRing} (e : ↑α ≃+* ↑β), (BoolRing.Iso.mk e).inv.hom' = ↑e.symm
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.nonsingular_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [Nontrivial R], W'.Nonsingular ![0, 1, 0]
-- Mathlib.Data.EReal.Basic
EReal.zero_ne_top : 0 ≠ ⊤
-- Mathlib.Topology.Bases
TopologicalSpace.SeparableSpace.mk : ∀ {α : Type u} [t : TopologicalSpace α], (∃ s, s.Countable ∧ Dense s) → TopologicalSpace.SeparableSpace α
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero : CategoryTheory.CategoryStruct.comp
    (SimplexCategory.Truncated.δ₂ 2 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1
      SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2)
    (SimplexCategory.Truncated.σ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2
      SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1) =
  CategoryTheory.CategoryStruct.comp
    (SimplexCategory.Truncated.σ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3
      SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4)
    (SimplexCategory.Truncated.δ₂ 1 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4
      SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.ExtHashMap.ofList l).getKeyD k' fallback = k
-- Init.Data.Array.Zip
Array.zip_replicate : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {m n : ℕ},
  (Array.replicate m a).zip (Array.replicate n b) = Array.replicate (min m n) (a, b)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.toPrenex.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u'} (x l : ℕ) (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin x)),
  (FirstOrder.Language.BoundedFormula.rel R ts).toPrenex = FirstOrder.Language.BoundedFormula.rel R ts
-- Init.Data.Int.Order
Int.sign.eq_1 : ∀ (n : ℕ), (Int.ofNat n.succ).sign = 1
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.leadingCoeff = 0 ↔ p = 0
-- Mathlib.Algebra.MonoidAlgebra.Division
_private.Mathlib.Algebra.MonoidAlgebra.Division.0.AddMonoidAlgebra.«term_%ᵒᶠ_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Convex.Extreme
extremePoints_prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] (s : Set E) (t : Set F),
  Set.extremePoints 𝕜 (s ×ˢ t) = Set.extremePoints 𝕜 s ×ˢ Set.extremePoints 𝕜 t
-- Mathlib.NumberTheory.ModularForms.Basic
CuspFormClass.zero_at_infty_slash : ∀ {k : ℤ} {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : FunLike F UpperHalfPlane ℂ] (f : F) [Γ.IsArithmetic]
  (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) [CuspFormClass F Γ k],
  UpperHalfPlane.IsZeroAtImInfty (SlashAction.map k g ⇑f)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
/-- Selects the variable in the given linear polynomial whose coefficient has the smallest absolute value.
 -/
Lean.Grind.Linarith.Poly.pickVarToElim? : Lean.Grind.Linarith.Poly → Option (ℤ × Lean.Grind.Linarith.Var)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings
SheafOfModules.restrictScalars_map_val : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R R' : CategoryTheory.Sheaf J RingCat} (α : R ⟶ R') {X Y : SheafOfModules R'} (φ : X ⟶ Y),
  ((SheafOfModules.restrictScalars α).map φ).val = (PresheafOfModules.restrictScalars α.hom).map φ.val
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.tryCatch_Option : ∀ {α : Type} {post : α → Prop} {epost : Prop} (x : Option α) (h : PUnit.{1} → Option α),
  ⦃ Std.Internal.Do.wp x post (Std.Internal.Do.wp (h PUnit.unit) post epost) ⦄ MonadExceptOf.tryCatch x h ⦃ post;
    epost ⦄
-- Init.Data.String.Lemmas.TakeDrop
String.Slice.take_eq_sliceTo : ∀ {s : String.Slice} {n : ℕ}, s.take n = s.sliceTo (s.startPos.nextn n)
-- Mathlib.Data.ENNReal.Basic
ENNReal.range_coe' : Set.range ENNReal.ofNNReal = Set.Iio ⊤
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.le_opENorm₂ : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F),
  ‖(f x) y‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ * ‖y‖ₑ
-- Init.Data.BitVec.Bitblast
/-- One round of the division algorithm. It tries to perform a subtract shift.

This should only be called when `r.msb = false`, so it will not overflow.
 -/
BitVec.divSubtractShift : {w : ℕ} → BitVec.DivModArgs w → BitVec.DivModState w → BitVec.DivModState w
-- Mathlib.Logic.Equiv.Defs
Equiv.Perm.congr_fun : ∀ {α : Sort u} {f g : Equiv.Perm α}, f = g → ∀ (x : α), f x = g x
-- Mathlib.Algebra.BrauerGroup.Defs
/-- `CSA` equipped with Brauer Equivalence is indeed a setoid.  -/
Brauer.CSA_Setoid : (K : Type u) → [inst : Field K] → Setoid (CSA K)
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.ins.eq_2 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : α) (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α),
  RBTree.RBNode.ins cmp x (RBTree.RBNode.node RBTree.RBColor.red a y b) =
    match cmp x y with
    | Ordering.lt => RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.ins cmp x a) y b
    | Ordering.gt => RBTree.RBNode.node RBTree.RBColor.red a y (RBTree.RBNode.ins cmp x b)
    | Ordering.eq => RBTree.RBNode.node RBTree.RBColor.red a x b
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.toFun_eq_coe : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (f : P →ᴬ[R] Q), (↑f).toFun = ⇑f
-- Mathlib.Probability.Independence.InfinitePi
/-- If random variables are independent then their joint distribution is the product measure.  -/
ProbabilityTheory.iIndepFun.map_fun_eq_infinitePi_map : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : ι → Type u_3}
  {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i},
  (∀ (i : ι), Measurable (X i)) →
    ProbabilityTheory.iIndepFun X P →
      MeasureTheory.Measure.map (fun ω i => X i ω) P =
        MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.map (X i) P
-- Mathlib.Order.Monotone.Monovary
Antivary.comp_antitone_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β}, Antivary f g → Antitone f' → Monovary (f' ∘ f) g
-- Init.Prelude
/-- Auxiliary declaration used to implement named patterns like `x@h:p`.  -/
namedPattern : {α : Sort u} → (x a : α) → x = a → α
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.eval_one_cyclotomic_prime_pow : ∀ {R : Type u_1} [inst : CommRing R] {p : ℕ} (k : ℕ) [hn : Fact (Nat.Prime p)],
  Polynomial.eval 1 (Polynomial.cyclotomic (p ^ (k + 1)) R) = ↑p
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_map_map : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G') (H K : AddSubgroup G),
  (AddSubgroup.map f H).relIndex (AddSubgroup.map f K) = (H ⊔ f.ker).relIndex (K ⊔ f.ker)
-- Mathlib.Tactic.CongrExclamation
Congr!.Config.mk : Bool →
  Bool →
    Lean.Meta.TransparencyMode →
      Lean.Meta.TransparencyMode →
        Lean.Meta.TransparencyMode → Bool → Bool → Bool → Option ℕ → Bool → Bool → Bool → Bool → Congr!.Config
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.isIso_fromOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [CategoryTheory.Balanced C],
  S.Exact → ∀ [CategoryTheory.Epi S.g] [inst_4 : S.HasRightHomology], CategoryTheory.IsIso S.fromOpcycles
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.isSaveInfoAnnotation? : Lean.Expr → Option Lean.Expr
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_eq_neg_one_iff : ∀ (n : ℤ), n.negOnePow = -1 ↔ Odd n
-- Mathlib.Order.Lex
/-- `toLex` is the identity function to the `Lex` of a type.  -/
toLex : {α : Type u_1} → α ≃ Lex α
-- Init.Data.String.Slice
/-- Checks whether a slice has a match of the pattern `pat` anywhere.

This function is generic over all currently supported patterns.

Examples:

* `"coffee tea water".toSlice.contains Char.isWhitespace = true`

* `"tea".toSlice.contains (fun (c : Char) => c == 'X') = false`

* `"coffee tea water".toSlice.contains "tea" = true`
 -/
String.Slice.any : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        String.Slice → (pat : ρ) → [String.Slice.Pattern.ToForwardSearcher pat σ] → Bool
-- Mathlib.Algebra.BigOperators.Finprod
finprod_curry₃ : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {γ : Type u_7} (f : α × β × γ → M),
  Function.HasFiniteMulSupport f → ∏ᶠ (abc : α × β × γ), f abc = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_mul_eq_prod_mul_of_exists : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {s : Finset ι} {f : ι → M} {b₁ b₂ : M},
  ∀ a ∈ s, f a * b₁ = f a * b₂ → (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂
-- Mathlib.Order.CountableSupClosed
mem_countableInfClosure_iff_iInf : ∀ {α : Type u_2} {s : Set α} {a : α} [inst : CompleteLattice α],
  a ∈ countableInfClosure s ↔ ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨅ n, t n = a
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The composition of homology map data.  -/
CategoryTheory.ShortComplex.HomologyMapData.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {φ' : S₂ ⟶ S₃} →
            {h₁ : S₁.HomologyData} →
              {h₂ : S₂.HomologyData} →
                {h₃ : S₃.HomologyData} →
                  CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂ →
                    CategoryTheory.ShortComplex.HomologyMapData φ' h₂ h₃ →
                      CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.CategoryStruct.comp φ φ') h₁ h₃
-- 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 => x = a) f = fun₀ | a => f a