mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.core.injEq : ∀ (a b : Lean.Expr) (ra rb : Lean.Grind.CommRing.Expr) (a_1 b_1 : Lean.Expr) (ra_1 rb_1 : Lean.Grind.CommRing.Expr),
  (Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.core a b ra rb =
      Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.core a_1 b_1 ra_1 rb_1) =
    (a = a_1 ∧ b = b_1 ∧ ra = ra_1 ∧ rb = rb_1)
-- Mathlib.ModelTheory.Quotients
FirstOrder.Language.Prestructure.mk : {L : FirstOrder.Language} →
  {M : Type u_1} →
    {s : Setoid M} →
      (toStructure : L.Structure M) →
        (∀ {n : ℕ} {f : L.Functions n} (x y : Fin n → M),
            x ≈ y → FirstOrder.Language.Structure.funMap f x ≈ FirstOrder.Language.Structure.funMap f y) →
          (∀ {n : ℕ} {r : L.Relations n} (x y : Fin n → M),
              x ≈ y → FirstOrder.Language.Structure.RelMap r x = FirstOrder.Language.Structure.RelMap r y) →
            L.Prestructure s
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.Localization.essSurj_mapArrow : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions], L.mapArrow.EssSurj
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelIsoOfEq.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasKernel g] (h : f = g),
  CategoryTheory.Limits.kernelIsoOfEq h =
    CategoryTheory.Limits.HasLimit.isoOfNatIso
      (⋯.mpr (CategoryTheory.Iso.refl (CategoryTheory.Limits.parallelPair g 0)))
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Atom.mk : Lean.Expr → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Atom
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.flatMapAfter.eq_1 : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterator α₂ m γ] (f : β → Std.IterM m γ) (it₁ : Std.IterM m β) (it₂ : Option (Std.IterM m γ)),
  Std.IterM.flatMapAfter f it₁ it₂ = Std.IterM.flattenAfter✝ (Std.IterM.map f it₁) it₂
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.ground_finite : ∀ {α : Type u_1} (M : Matroid α) [M.Finite], M.E.Finite
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.foldM_filterMap : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad m] [LawfulMonad n]
  [inst_6 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n]
  {f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : Std.IterM m β},
  Std.IterM.foldM g init (Std.IterM.filterMap f it) =
    Std.IterM.foldM
      (fun d b =>
        match f b with
        | some c => g d c
        | x => pure d)
      init it
-- Init.Data.List.TakeDrop
List.takeWhile_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {p : β → Bool} {l : List α},
  List.takeWhile p (List.filterMap f l) = List.filterMap f (List.takeWhile (fun a => Option.all p (f a)) l)
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.ker_fundamentalGroupToMulOpposite : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x : X} (e : ↑(p ⁻¹' {x})),
  (hp.fundamentalGroupToMulOpposite e).ker = (⋯.monodromyPerm x).ker
-- Init.Data.BitVec.Lemmas
BitVec.msb_eq_getMsbD_zero : ∀ {w : ℕ} (x : BitVec w), x.msb = x.getMsbD 0
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_iff_forall : ∀ {α : Type u_1} {P : α → Prop} {t : Ordnode α}, Ordnode.All P t ↔ ∀ (x : α), Ordnode.Emem x t → P x
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.OptionT.bind.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) →
    (__do_lift : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive __do_lift
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M}
  {V : (x : M') → TangentSpace I' x}, VectorField.mpullback I I' f V x = (mfderiv% f x).inverse (V (f x))
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
/-- The functor `Γ` for the equivalence is `Γ₀`.  -/
CategoryTheory.Idempotents.DoldKan.Γ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.IsIdempotentComplete C] →
        [CategoryTheory.Limits.HasFiniteCoproducts C] →
          CategoryTheory.Functor (ChainComplex C ℕ) (CategoryTheory.SimplicialObject C)
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Adjunction.sheafPushforwardContinuous_counit_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K] [inst_4 : G.IsContinuous K J]
  (P : CategoryTheory.Sheaf J E) (X : Cᵒᵖ),
  ((adj.sheafPushforwardContinuous J K).counit.app P).hom.app X = P.obj.map (adj.unit.app (Opposite.unop X)).op
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometric_eq_tsum : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a b c : 𝕂),
  ₂F₁ a b c = fun x =>
    ∑' (n : ℕ),
      ((↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
          (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
        x ^ n
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.mulEquivAlgEquiv.congr_simp : ∀ (G : Type u_1) [inst : Group G] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : FaithfulSMul A B] [inst_6 : MulSemiringAction G B]
  [inst_7 : IsGaloisGroup G A B] [inst_8 : Finite G],
  IsGaloisGroup.mulEquivAlgEquiv G A B = IsGaloisGroup.mulEquivAlgEquiv G A B
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- Recurrent formula for `torusIntegral`, see also `torusIntegral_succAbove`.  -/
torusIntegral_succ : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : (Fin (n + 1) → ℂ) → E}
  {c : Fin (n + 1) → ℂ} {R : Fin (n + 1) → ℝ},
  TorusIntegrable f c R →
    (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
      ∮ (x : ℂ) in C(c 0, R 0), ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succ, R ∘ Fin.succ), f (Fin.cons x y)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_neg : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : NormedAddCommGroup V]
  (μ : MeasureTheory.VectorMeasure X V), (-μ).variation = μ.variation
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.reduceCyclically.eq_1 : ∀ {α : Type u} [inst : DecidableEq α] (l : List (α × Bool)),
  FreeGroup.reduceCyclically l =
    List.bidirectionalRec [] (fun x => [x]) (fun a L b rC => if b.1 = a.1 ∧ (!b.2) = a.2 then rC else a :: L ++ [b]) l
-- Mathlib.Data.Stream.Init
Stream'.get_const : ∀ {α : Type u} (n : ℕ) (a : α), (Stream'.const a).get n = a
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.Λ₀_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) (s : ℂ),
  P.Λ₀ s = P.Λ s + (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α},
  Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.Const.insertManyIfNewUnit m l) k = ()
-- Mathlib.Topology.KrullDimension
irreducibleSetEquivPoints.congr_simp : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSober α] [inst_2 : T0Space α],
  irreducibleSetEquivPoints = irreducibleSetEquivPoints
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β k}, (t₁ ∪ t₂).getD k fallback = t₂.getD k (t₁.getD k fallback)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurable_infNndist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α},
  Measurable fun x => Metric.infNndist x s
-- Init.Data.SInt.Lemmas
Int32.ofInt_le_iff_le : ∀ {a b : ℤ},
  Int32.minValue.toInt ≤ a →
    a ≤ Int32.maxValue.toInt →
      Int32.minValue.toInt ≤ b → b ≤ Int32.maxValue.toInt → (Int32.ofInt a ≤ Int32.ofInt b ↔ a ≤ b)
-- Mathlib.Topology.Order
isOpen_singleton_nhdsAdjoint : ∀ {α : Type u_1} {a b : α} (f : Filter α), b ≠ a → IsOpen {b}
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- A subsemigroup of a `CommSemigroup` is a `CommSemigroup`.  -/
MulMemClass.toCommSemigroup : {M : Type u_5} →
  [inst : CommSemigroup M] → {A : Type u_4} → [inst_1 : SetLike A M] → [MulMemClass A M] → (S : A) → CommSemigroup ↥S
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.mul_omega0_opow_opow : ∀ {a b : Ordinal.{u}},
  0 < a →
    a < Ordinal.omega0 ^ Ordinal.omega0 ^ b →
      a * Ordinal.omega0 ^ Ordinal.omega0 ^ b = Ordinal.omega0 ^ Ordinal.omega0 ^ b
-- Mathlib.Condensed.Light.Module
LightCondensed.forget_obj_obj_map_hom_apply : ∀ (R : Type u) [inst : Ring R] (X : LightCondMod R) {S T : LightProfiniteᵒᵖ} (f : S ⟶ T)
  (a :
    ↑(((CategoryTheory.sheafToPresheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)).obj X).obj S)),
  (CategoryTheory.ConcreteCategory.hom (((LightCondensed.forget R).obj X).obj.map f)) a =
    (CategoryTheory.ConcreteCategory.hom (X.obj.map f)) a
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.sheafifyComposeIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.HasWeakSheafify J A]
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [inst_5 : J.HasSheafCompose F] [inst_6 : J.PreservesSheafification F]
  (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.sheafifyComposeIso J F P = CategoryTheory.sheafifyComposeIso J F P
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] (X Y : C),
  CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv F X Y =
    CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv F X Y
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels
/-- A colimit cokernel cofork in the opposite category gives a limit kernel fork
in the original category  -/
CategoryTheory.Limits.CokernelCofork.IsColimit.ofπUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y Q : Cᵒᵖ} →
        (p : Y ⟶ Q) →
          {f : X ⟶ Y} →
            (w : CategoryTheory.CategoryStruct.comp f p = 0) →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p w) →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι p.unop ⋯)
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.exists_zpow_uniformizingPolynomial : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [inst_2 : v.IsNontrivial] [inst_3 : Valuation.IsTrivialOn K v] (hle : v RatFunc.X ≤ 1)
  {f : RatFunc K}, f ≠ 0 → ∃ z, v f = v ↑(RatFunc.uniformizingPolynomial hle) ^ z
-- Mathlib.Topology.Category.FinTopCat
FinTopCat.instCoeSortType : CoeSort FinTopCat (Type u)
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.Balanced.left : ∀ {α : Type u} {β : α → Type v} {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).Balanced → l.Balanced
-- Mathlib.Data.Set.Finite.Basic
/-- A `Fintype` instance for set intersection where the right set has a `Fintype` instance.  -/
Set.fintypeInterOfRight : {α : Type u} → (s t : Set α) → [Fintype ↑t] → [DecidablePred fun x => x ∈ s] → Fintype ↑(s ∩ t)
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.and_self_left : ∀ (a b : ℕ), a &&& (a &&& b) = a &&& b
-- Mathlib.Data.Setoid.Basic
/-- The complete lattice of equivalence relations on a type, with bottom element `=`
and top element the trivial equivalence relation.  -/
Setoid.completeLattice : {α : Type u_1} → CompleteLattice (Setoid α)
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
/-- If `R` is an additive monoid with one (e.g., a semiring), then `1 : AddSubmonoid R` is the range
of `Nat.cast : ℕ → R`.  -/
AddSubmonoid.one : {R : Type u_2} → [inst : AddMonoidWithOne R] → One (AddSubmonoid R)
-- Mathlib.Data.Finset.Sups
Finset.empty_infs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {t : Finset α}, ∅ ⊼ t = ∅
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Rep.FiniteCyclicGroup.resolution.π_f : ∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (g : G) (i : ℕ),
  (Rep.FiniteCyclicGroup.resolution.π k g).f i =
    if hi : i = 0 then
      CategoryTheory.CategoryStruct.comp
        ((HomologicalComplex.alternatingConst (Rep.leftRegular k G) ⋯ ⋯ ⋯).XIsoOfEq hi).hom
        (CategoryTheory.CategoryStruct.comp ((Rep.trivial k G k).leftRegularHom 1)
          (HomologicalComplex.singleObjXIsoOfEq (ComplexShape.down ℕ) 0 (Rep.trivial k G k) i hi).inv)
    else 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.get_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} {hk : k ∈ t₁}
  (h : t₁.Equiv t₂), t₁.get k hk = t₂.get k ⋯
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- When `S₁.f`, `S₁.g`, `S₂.f` and `S₂.g` are all zero, the action on right homology of a
morphism `φ : S₁ ⟶ S₂` is given by the action `φ.τ₂` on the middle objects.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (hf₁ : S₁.f = 0) →
            (hg₁ : S₁.g = 0) →
              (hf₂ : S₂.f = 0) →
                (hg₂ : S₂.g = 0) →
                  CategoryTheory.ShortComplex.RightHomologyMapData φ
                    (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S₁ hf₁ hg₁)
                    (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S₂ hf₂ hg₂)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- If `F` preserves the limit of every `Discrete.functor f`, it preserves all limits of shape
`Discrete J`.  -/
CategoryTheory.Limits.preservesLimitsOfShape_of_discrete : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} (F : CategoryTheory.Functor C D)
  [∀ (f : J → C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.Data.Finset.Lattice.Fold
Finset.apply_sup_eq_sup_comp_of_linearOrder : ∀ {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
  [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β] (g : α → β), Monotone g → g ⊥ = ⊥ → g (s.sup f) = s.sup (g ∘ f)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zpow_of_gcd_eq_one : ∀ {G : Type u_3} [inst : DivisionCommMonoid G] {k : ℕ} {ζ : G},
  IsPrimitiveRoot ζ k → ∀ (i : ℤ), i.gcd ↑k = 1 → IsPrimitiveRoot (ζ ^ i) k
-- Mathlib.Algebra.Module.DedekindDomain
/-- Over a Dedekind domain, an `I`-torsion module is the internal direct sum of its `p i ^ e i`-
torsion submodules, where `I = ∏ i, p i ^ e i` is its unique decomposition in prime ideals.  -/
Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {M : Type v} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {I : Ideal R},
  I ≠ ⊥ →
    Module.IsTorsionBySet R M ↑I →
      DirectSum.IsInternal fun p =>
        Submodule.torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors I))
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_rotateL : ∀ {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α},
  Ordnode.All P (l.rotateL x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r
-- Init.MetaTypes
/-- When merging is enabled, if true (default: true), make use of pre-existing local definitions in the local context.  -/
Lean.Meta.ExtractLetsConfig.useContext : Lean.Meta.ExtractLetsConfig → Bool
-- Mathlib.LinearAlgebra.Finsupp.Pi
LinearMap.exists_finsupp_nat_of_prod_injective : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid P] [inst_4 : Module R P] {f : P × M →ₗ[R] M},
  Function.Injective ⇑f → ∃ g, Function.Injective ⇑g
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The coproduct comparison morphism from `FA ⨿ F-` to `F(A ⨿ -)`, whose components are given by
`coprodComparison`.
 -/
CategoryTheory.Limits.coprodComparisonNatTrans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{w, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] →
          [inst_3 : CategoryTheory.Limits.HasBinaryCoproducts D] →
            (F : CategoryTheory.Functor C D) →
              (A : C) →
                F.comp (CategoryTheory.Limits.coprod.functor.obj (F.obj A)) ⟶
                  (CategoryTheory.Limits.coprod.functor.obj A).comp F
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.blocks_partial_sum : ∀ {n : ℕ} (c : CompositionAsSet n) {i : ℕ} (h : i < c.boundaries.card),
  (List.take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.symm_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂), e.symm.hom = e.inv
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.map_hsymm : ∀ {S : Type u_4} (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Fintype σ]
  [inst_3 : DecidableEq σ] (n : ℕ) (f : R →+* S),
  (MvPolynomial.map f) (MvPolynomial.hsymm σ R n) = MvPolynomial.hsymm σ S n
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.coe_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f : CauSeq β abv), ↑(-f) = -↑f
-- Mathlib.Algebra.Order.Quantale
add_sSup_distrib : ∀ {α : Type u_1} {x : α} {s : Set α} [inst : AddSemigroup α] [inst_1 : CompleteLattice α] [IsAddQuantale α],
  x + sSup s = ⨆ y ∈ s, x + y
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.dist_left_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ → dist p₁ p₂ = 2 * s.radius
-- Mathlib.CategoryTheory.Sites.Monoidal
CategoryTheory.Sheaf.instBraidedFunctorOppositePresheafToSheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₃) →
        [inst_1 : CategoryTheory.Category.{v₃, u₃} A] →
          [inst_2 : CategoryTheory.MonoidalCategory A] →
            [inst_3 : J.W.IsMonoidal] →
              [inst_4 : CategoryTheory.HasWeakSheafify J A] →
                [inst_5 : CategoryTheory.BraidedCategory A] → (CategoryTheory.presheafToSheaf J A).Braided
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_bind_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.maxKey?.bind t.getKey? = t.maxKey?
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_of_nonneg : ∀ {K : Type u_1} [inst : RCLike K] {r : ℝ}, 0 ≤ r → ‖↑r‖ = r
-- Mathlib.Computability.Encoding
/-- An encoding function of the binary numbers in `Bool`.  -/
Computability.encodeNum : Num → List Bool
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.ne_zero_of_not_isOrtho_self : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {B : LinearMap.BilinForm K V} (x : V), (B x) x ≠ 0 → x ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonian.map : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {β : Type u_2} [inst_1 : DecidableEq β] {H : SimpleGraph β}
  {a b : α} {p : G.Walk a b} (f : G →g H),
  Function.Bijective ⇑f → p.IsHamiltonian → (SimpleGraph.Walk.map f p).IsHamiltonian
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.postAdjunctionLeft_unit_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F : CategoryTheory.Functor T D} {G : CategoryTheory.Functor D T} (a : F ⊣ G)
  (A : CategoryTheory.Under ((CategoryTheory.Functor.id T).obj X)),
  (CategoryTheory.Under.postAdjunctionLeft a).unit.app A = CategoryTheory.Under.homMk (a.unit.app A.right) ⋯
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instAddOffset : Add Std.Time.Minute.Offset
-- Std.Data.DTreeMap.Raw.Lemmas
/-- Variant of `get!_map` that holds without `LawfulEqCmp`.  -/
Std.DTreeMap.Raw.Const.get!_map' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited γ] {f : α → β → γ} {k : α} (h : t.WF),
  Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.map f t) k =
    (Option.pmap (fun v h => f (t.getKey k h) v) (Std.DTreeMap.Raw.Const.get? t k) ⋯).get!
-- Init.Data.SInt.Lemmas
ISize.toInt64_div_of_ne_left : ∀ (a b : ISize), a ≠ ISize.minValue → (a / b).toInt64 = a.toInt64 / b.toInt64
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.instInhabited : Inhabited Turing.PartrecToTM2.Λ'
-- Mathlib.Topology.Constructions
Topology.IsEmbedding.piMap : ∀ {ι : Type u_5} {A : ι → Type u_6} {B : ι → Type u_7} [T : (i : ι) → TopologicalSpace (A i)]
  [inst : (i : ι) → TopologicalSpace (B i)] {f : (i : ι) → A i → B i},
  (∀ (i : ι), Topology.IsEmbedding (f i)) → Topology.IsEmbedding (Pi.map f)