mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.ext_of_isPullback : ∀ {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄},
  CategoryTheory.IsPullback t l r b →
    ∀ {x₁ y₁ : X₁},
      (CategoryTheory.ConcreteCategory.hom t) x₁ = (CategoryTheory.ConcreteCategory.hom t) y₁ →
        (CategoryTheory.ConcreteCategory.hom l) x₁ = (CategoryTheory.ConcreteCategory.hom l) y₁ → x₁ = y₁
-- Mathlib.Topology.Closure
closure_univ : ∀ {X : Type u} [inst : TopologicalSpace X], closure Set.univ = Set.univ
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- Any linear map `f : p →ₗ[K] V'` defined on a subspace `p` can be extended to the whole
space.  -/
LinearMap.exists_extend : ∀ {K : Type u_3} {V : Type u_4} {V' : Type u_5} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V'] [inst_3 : Module K V] [inst_4 : Module K V'] {p : Submodule K V} (f : ↥p →ₗ[K] V'),
  ∃ g, g ∘ₗ p.subtype = f
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAt.source_subset_preimage_source : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAt I J n f x), h.domChart.source ⊆ f ⁻¹' h.codChart.source
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its
`finrank`. This is a copy of `finrank_eq_rank _ _` which creates easier typeclass searches.  -/
Module.finrank_eq_rank' : ∀ (K : Type u) (V : Type v) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V], ↑(Module.finrank K V) = Module.rank K V
-- Mathlib.Order.BoundedOrder.Lattice
max_bot_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderBot α] (a : α), max a ⊥ = a
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- The choice of a preimage of a morphism under a full functor.  -/
CategoryTheory.Functor.preimage : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X Y : C} → (F : CategoryTheory.Functor C D) → [F.Full] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.tprod_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [T2Space β]
  [inst_3 : CommMonoid β] [inst_4 : ContinuousMul β] {γ : Type u_3} {f : γ → C(α, β)} {L : SummationFilter γ},
  Multipliable f L → ∀ [L.NeBot] (x : α), ∏'[L] (i : γ), (f i) x = (∏'[L] (i : γ), f i) x
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.fixupBlocks : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock) × Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty) →
  Lean.Doc.DocM
    (Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock) × Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty))
-- Aesop.Script.CtorNames
Aesop.CtorNames : Type
-- Mathlib.GroupTheory.Exponent
AddMonoid.nsmul_eq_mod_exponent : ∀ {G : Type u} [inst : AddMonoid G] {n : ℕ} (g : G), n • g = (n % AddMonoid.exponent G) • g
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.prod_base_smul : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (h : H) (w : Monoid.PushoutI.NormalWord d),
  (h • w).prod = (Monoid.PushoutI.base φ) h * w.prod
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.fin3_def_ext : ∀ {R : Type r} (a b c : R), ![a, b, c] 0 = a ∧ ![a, b, c] 1 = b ∧ ![a, b, c] 2 = c
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.faithfulSMul_tower_top : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] (A : Type u_3) [inst_1 : CommRing S] [NoZeroDivisors S]
  [inst_3 : Algebra R S] [alg : Algebra.IsAlgebraic R S] [inst_4 : Ring A] [inst_5 : Algebra R A] [inst_6 : Algebra S A]
  [IsScalarTower R S A] [FaithfulSMul R A], FaithfulSMul S A
-- Mathlib.Data.PFun
PFun.lawfulMonad : ∀ {α : Type u_1}, LawfulMonad (PFun α)
-- Init.Data.Iterators.Basic
Std.Iter.isPlausibleOutput_iff_exists : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {out : β},
  it.IsPlausibleOutput out ↔ ∃ it', it.IsPlausibleStep (Std.IterStep.yield it' out)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.singularPart_add : ∀ {α : Type u_1} {m : MeasurableSpace α} (s t : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [s.HaveLebesgueDecomposition μ] [t.HaveLebesgueDecomposition μ],
  (s + t).singularPart μ = s.singularPart μ + t.singularPart μ
-- Mathlib.Analysis.Seminorm
/-- Reinterpret a seminorm over a field `𝕜'` as a seminorm over a smaller field `𝕜`. This will
typically be used with `RCLike 𝕜'` and `𝕜 = ℝ`.  -/
Seminorm.restrictScalars : (𝕜 : Type u_3) →
  {E : Type u_7} →
    {𝕜' : Type u_12} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedRing 𝕜'] →
          [inst_2 : SMul 𝕜 𝕜'] →
            [NormSMulClass 𝕜 𝕜'] →
              [NormOneClass 𝕜'] →
                [inst_5 : AddCommGroup E] →
                  [inst_6 : Module 𝕜' E] → [inst_7 : SMul 𝕜 E] → [IsScalarTower 𝕜 𝕜' E] → Seminorm 𝕜' E → Seminorm 𝕜 E
-- Aesop.Stats.Basic
Aesop.Stats.ruleStatsTotals : Aesop.Stats →
  optParam (Std.HashMap Aesop.DisplayRuleName Aesop.RuleStatsTotals) ∅ →
    Std.HashMap Aesop.DisplayRuleName Aesop.RuleStatsTotals
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_indep_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {M : Matroid α} {hf : Set.InjOn f M.E} {I : Set β},
  (M.map f hf).Indep I ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instT4Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T4Space M], T4Space Mᵈᵃᵃ
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_map_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (S : CategoryTheory.Subgroupoid C) {c d : D}
  (f : c ⟶ d),
  f ∈ (CategoryTheory.Subgroupoid.map φ hφ S).arrows c d ↔
    ∃ a b g,
      ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
        f =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp (φ.map g) (CategoryTheory.eqToHom hb))
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- If all the elements of a set `s` commute, then `closure s` is a non-unital commutative
semiring.  -/
NonUnitalSubring.isMulCommutative_closure : ∀ {R : Type u_1} [inst : NonUnitalRing R] {s : Set R},
  (∀ x ∈ s, ∀ y ∈ s, x * y = y * x) → IsMulCommutative ↥(NonUnitalSubring.closure s)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ColorInformation.mk : Lean.Lsp.Range → Lean.Lsp.Color → Lean.Lsp.ColorInformation
-- Mathlib.Data.ENat.Basic
ENat.top_ne_zero : ⊤ ≠ 0
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (n a n' : ℤ) (hn' : n' + a = n)
  (γ : CochainComplex.HomComplex.Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'),
  (CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv n a n' hn').symm γ = γ.rightUnshift n hn'
-- Mathlib.Algebra.Group.Basic
nsmul_add_sub_nsmul : ∀ {M : Type u_4} [inst : AddMonoid M] {m n : ℕ} (a : M), m ≤ n → m • a + (n - m) • a = n • a
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.length_alterKey_eq_add_one : ∀ {α : Type u} [inst : BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)},
  Std.Internal.List.containsKey k l = false →
    (f (Std.Internal.List.getValue? k l)).isSome = true → (Std.Internal.List.Const.alterKey k f l).length = l.length + 1
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.tensorIso_inv : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (e : X₁ ≅ X₂)
  (e' : Y₁ ≅ Y₂) [inst_3 : X₁.HasTensor Y₁] [inst_4 : X₂.HasTensor Y₂] (i : I),
  (CategoryTheory.GradedObject.Monoidal.tensorIso e e').inv i =
    CategoryTheory.GradedObject.Monoidal.tensorHom e.inv e'.inv i
-- Init.Data.String.Termination
/-- Type alias for `String.Pos` representing that the given position is expected to decrease
in recursive calls.  -/
String.Pos.Down : String → Type
-- Mathlib.LinearAlgebra.PiTensorProduct.Generators
/-- The linear equivalence between `⨂[R] i, M i` and the tensor product of
the pi tensor product indexed by the complement of `{i₀}` and `M i₀`.  -/
PiTensorProduct.equivPiTensorComplSingletonTensor : (R : Type u_1) →
  {ι : Type u_2} →
    [DecidableEq ι] →
      (M : ι → Type u_3) →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              (i₀ : ι) → (PiTensorProduct R fun i => M i) ≃ₗ[R] TensorProduct R (PiTensorProduct R fun i => M ↑i) (M i₀)
-- Mathlib.Topology.Sheaves.Forget
/-- If `G : C ⥤ D` is a functor which reflects isomorphisms and preserves limits
(we assume all limits exist in `C`),
then checking the sheaf condition for a presheaf `F : Presheaf C X`
is equivalent to checking the sheaf condition for `F ⋙ G`.

The important special case is when
`C` is a concrete category with a forgetful functor
that preserves limits and reflects isomorphisms.
Then to check the sheaf condition it suffices to check it on the underlying sheaf of types.

Another useful example is the forgetful functor `TopCommRingCat ⥤ TopCat`.  -/
TopCat.Presheaf.isSheaf_iff_isSheaf_comp' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.Limits.HasLimitsOfSize.{v, v, v₁, u₁} C]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, v₁, v₂, u₁, u₂} G] {X : TopCat} (F : TopCat.Presheaf C X),
  F.IsSheaf ↔ TopCat.Presheaf.IsSheaf (CategoryTheory.Functor.comp F G)
-- Mathlib.Data.Fintype.Defs
/-- Delaborator for `Finset.filter`. The `pp.funBinderTypes` option controls whether
to show the domain type when the filter is over `Finset.univ`.  -/
Mathlib.Meta.delabFinsetFilter : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_eq_card_filter : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] (s t : Finset α),
  s.mulEnergy t = {x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}.card
-- Mathlib.Logic.Function.DependsOn
/-- A function which depends on the empty set is constant.  -/
DependsOn.empty : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β},
  DependsOn f ∅ → ∀ (x y : (i : ι) → α i), f x = f y
-- Init.Data.UInt.Bitwise
USize.ofFin_rev : ∀ (a : Fin USize.size), USize.ofFin a.rev = ~~~USize.ofFin a
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.stdAddChar_coe : ∀ {N : ℕ} [inst : NeZero N] (j : ℤ), ZMod.stdAddChar ↑j = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j / ↑N)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The negation in a group object  -/
CategoryTheory.AddGrpObj.neg : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.CartesianMonoidalCategory C} → {X : C} → [self : CategoryTheory.AddGrpObj X] → X ⟶ X
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_mul : ∀ {𝕜 : Type u_1} {E : Type u_2} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G] (f₁ f₂ : E →L[𝕜] E),
  ContinuousLinearMap.lTensor G (f₁ * f₂) = ContinuousLinearMap.lTensor G f₁ * ContinuousLinearMap.lTensor G f₂
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.liftAt.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {x : ℕ} (n' m : ℕ) (φ : L.BoundedFormula α x),
  FirstOrder.Language.BoundedFormula.liftAt n' m φ =
    FirstOrder.Language.BoundedFormula.mapTermRel (fun x t => FirstOrder.Language.Term.liftAt n' m t) (fun x => id)
      (fun x => FirstOrder.Language.BoundedFormula.castLE ⋯) φ
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.sInf_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (S : Set (CategoryTheory.Subfunctor F)) (U : C), (sInf S).obj U = sInf ((fun T => T.obj U) '' S)
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.inter_of_finite_sdiff : ∀ {α : Type u_1} {s t : Set α}, s.Infinite → (s \ t).Finite → (s ∩ t).Infinite
-- Mathlib.Analysis.Convex.Strict
/-- The image of a strictly convex set under an affine map is strictly convex.  -/
StrictConvex.affine_image : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : TopologicalSpace F] [inst_4 : AddCommGroup E] [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 F] {s : Set E}, StrictConvex 𝕜 s → ∀ {f : E →ᵃ[𝕜] F}, IsOpenMap ⇑f → StrictConvex 𝕜 (⇑f '' s)
-- Init.Data.List.ToArray
List.foldrM_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m β) (init : β) (l : List α),
  Array.foldrM f init l.toArray = List.foldrM f init l
-- Mathlib.Algebra.CharP.Quotient
/-- If an ideal does not contain any coercions of natural numbers other than zero, then its quotient
inherits the characteristic of the underlying ring.  -/
CharP.quotient' : ∀ {R : Type u_1} [inst : CommRing R] (p : ℕ) [CharP R p] (I : Ideal R), (∀ (x : ℕ), ↑x ∈ I → ↑x = 0) → CharP (R ⧸ I) p
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorialBinary.match_1.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1)
  (h_3 : (k n : ℕ) → k = n + 2 → motive n.succ.succ),
  k = 0 →
    (match k with
      | 0 => h_1 ()
      | 1 => h_2 ()
      | k@h:n.succ.succ => h_3 k n h) ≍
      h_1 ()
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.whiskerLeft_apply : ∀ {R : Type u} [inst : CommRing R] (L : ModuleCat R) {M N : ModuleCat R} (f : M ⟶ N) (l : ↑L) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f)) (l ⊗ₜ[R] m) =
    l ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom f) m
-- Mathlib.Data.Setoid.Basic
Quot.subsingleton_iff : ∀ {α : Type u_1} (r : α → α → Prop), Subsingleton (Quot r) ↔ Relation.EqvGen r = ⊤
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.coe_sum : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] (f : α →₀ M)
  (g : α → M → β →₀ N), ⇑(f.sum g) = f.sum fun a₁ b => ⇑(g a₁ b)
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.comp_smul_smul : ∀ {R : Type u_1} {V : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V]
  {f : Module.Dual R V} {v : V} {r s : R},
  LinearMap.transvection f (r • v) ∘ₗ LinearMap.transvection f (s • v) =
    LinearMap.transvection f ((r + s + s * f v * r) • v)
-- Init.Data.Int.DivMod.Basic
Int.fdiv.eq_4 : ∀ (a : ℕ), (Int.negSucc a).fdiv 0 = 0
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.sum_add_tsum_nat_add : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {f : ℕ → G}
  (k : ℕ), Summable f → ∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The homotopy group at `x` indexed by a singleton is in bijection with the fundamental group,
i.e. the loops based at `x` up to homotopy.  -/
homotopyGroupEquivFundamentalGroupOfUnique : {X : Type u_2} →
  [inst : TopologicalSpace X] → {x : X} → (N : Type u_3) → [Unique N] → HomotopyGroup N X x ≃ FundamentalGroup X x
-- Lean.Meta.Tactic.Grind.Types
/-- Returns all enodes in the goal  -/
Lean.Meta.Grind.getExprs : Lean.Meta.Grind.GoalM (Lean.PArray Lean.Expr)
-- Init.Data.List.Basic
List.mapTR.loop.eq_def : ∀ {α : Type u} {β : Type v} (f : α → β) (a : List α) (a_1 : List β),
  List.mapTR.loop f a a_1 =
    match a, a_1 with
    | [], bs => bs.reverse
    | a :: as, bs => List.mapTR.loop f as (f a :: bs)
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.algebraMap_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] (T : Type u_7) [inst_7 : CommRing T] [inst_8 : Algebra T S]
  [inst_9 : Algebra T R] [IsScalarTower T S R] [inst_11 : P.IsValuedIn T] [inst_12 : P.IsValuedIn S] [FaithfulSMul S R]
  (i j : ι), (algebraMap T S) (P.pairingIn T i j) = P.pairingIn S i j
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum'' : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g +ᵥ x) ∂μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Raw.filter f t).getKey? k = (t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)
-- Mathlib.Algebra.DualNumber
DualNumber.algHom_ext'_iff : ∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {f g : DualNumber A →ₐ[R] B},
  f = g ↔
    f.comp (TrivSqZeroExt.inlAlgHom R A A) = g.comp (TrivSqZeroExt.inlAlgHom R A A) ∧
      f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A (DualNumber A) DualNumber.eps) =
        g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A (DualNumber A) DualNumber.eps)
-- Init.Data.Nat.MinMax
Nat.add_max_add_left : ∀ (a b c : ℕ), max (a + b) (a + c) = a + max b c
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Reformulation of `hasSum_nat_sinZeta` using `LSeriesHasSum`.  -/
HurwitzZeta.LSeriesHasSum_sin : ∀ (a : ℝ) {s : ℂ}, 1 < s.re → LSeriesHasSum (fun x => ↑(Real.sin (2 * Real.pi * a * ↑x))) s (HurwitzZeta.sinZeta (↑a) s)
-- Mathlib.AlgebraicGeometry.ColimitsOver
/-- The glued cocone is colimiting.  -/
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isColimitGluedCocone : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    [inst_1 : P.IsMultiplicative] →
      {S : AlgebraicGeometry.Scheme} →
        {J : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
            {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
              {𝒰 : S.OpenCover} →
                [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                    (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) →
                      [inst_5 :
                          ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
                            CategoryTheory.Limits.PreservesColimitsOfShape J
                              (CategoryTheory.MorphismProperty.Over.pullback P ⊤
                                (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))] →
                        [inst_6 : Quiver.IsThin 𝒰.I₀] →
                          [inst_7 : Small.{u, u_2} 𝒰.I₀] →
                            [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P] →
                              CategoryTheory.Limits.IsColimit d.gluedCocone
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub_natCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIcoDiv hp a (b - ↑m * p) = toIcoDiv hp a b - ↑m
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- A functor that preserves terminal objects and pullbacks preserves binary products.  -/
preservesBinaryProducts_of_preservesTerminal_and_pullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
-- Lean.Meta.ArgsPacker
/-- Given type `(A ⊕' C) → R` (possibly dependent), return types
```
#[A → R, B → R]
```
 -/
Lean.Meta.ArgsPacker.Mutual.curryType : ℕ → Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.mem_mk : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : AddSubmonoid M}
  {x : M} (h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier),
  x ∈ { toAddSubmonoid := S, smul_mem' := h } ↔ x ∈ S
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.algebraMap_apply'' : ∀ {R : Type u_1} (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (f : PowerSeries R), (algebraMap (PowerSeries R) (PowerSeries A)) f = (PowerSeries.map (algebraMap R A)) f
-- Mathlib.Analysis.Normed.Group.AddTorsor
/-- The distance equals the norm of subtracting two points. In this
lemma, it is necessary to have `V` as an explicit argument; otherwise
`rw dist_eq_norm_vsub` sometimes doesn't work.  -/
dist_eq_norm_vsub : ∀ (V : Type u_2) {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (x y : P), dist x y = ‖x -ᵥ y‖
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.coe_toIntLinearEquiv : ∀ {M : Type u_5} {M₂ : Type u_7} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] {modM : Module ℤ M}
  {modM₂ : Module ℤ M₂} (e : M ≃+ M₂), ⇑e.toIntLinearEquiv = ⇑e
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.subtype_comp_inclusion : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S T : L.Substructure M} (h : S ≤ T),
  T.subtype.comp (FirstOrder.Language.Substructure.inclusion h) = S.subtype
-- Lean.Environment
/-- Finds constants including from other environment branches by recursively looking up longest
prefixes (which is sufficient by `AsyncContext.mayContain`).
 -/
_private.Lean.Environment.0.Lean.AsyncConsts.findRec? : Lean.AsyncConsts✝ → Lean.Name → Option Lean.AsyncConst✝
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sOppSide_excenter_singleton_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i : Fin (n + 1)), (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SOppSide (s.excenter {i}) (s.points i)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- Bypass repeated vertices like `Walk.bypass`, except the starting vertex.

This is intended to be used for closed walks, for which `Walk.bypass` unhelpfully returns the empty
walk.  -/
SimpleGraph.Walk.cycleBypass : {V : Type u} → {G : SimpleGraph V} → {v : V} → [DecidableEq V] → G.Walk v v → G.Walk v v