mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.Defs
vadd_eq_add : ∀ {α : Type u_9} [inst : Add α] (a b : α), a +ᵥ b = a + b
-- Mathlib.Order.Lattice
inf_right_le_sup_left : ∀ {α : Type u} [inst : Lattice α] {a b c : α}, b ⊓ c ≤ a ⊔ b
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBySet_le_torsionBySet_pow : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (i j : ℕ),
  i ≤ j → ∀ (I : Ideal R), Submodule.torsionBySet R M ↑(I ^ i) ≤ Submodule.torsionBySet R M ↑(I ^ j)
-- Init.Meta.Defs
/-- Finds the trailing whitespace substring of the first `SourceInfo` from the back of `stx`.
If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains
no trailing whitespace, the result is `none`.
 -/
Lean.Syntax.getTrailing? : Lean.Syntax → Option Substring.Raw
-- Mathlib.Analysis.SpecificLimits.Basic
/-- The sum of `2⁻¹ ^ i` for `n ≤ i` equals `2 * 2⁻¹ ^ n`.  -/
tsum_geometric_inv_two_ge : ∀ (n : ℕ), (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientMapOfLE.congr_simp : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (h : s ≤ t) (a a_1 : α ⧸ s),
  a = a_1 → Subgroup.quotientMapOfLE h a = Subgroup.quotientMapOfLE h a_1
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (toPreZeroHypercover : CategoryTheory.PreZeroHypercover S) →
        (I₁ : toPreZeroHypercover.I₀ → toPreZeroHypercover.I₀ → Type w) →
          (Y : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → I₁ i₁ i₂ → C) →
            (p₁ : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ toPreZeroHypercover.X i₁) →
              (p₂ : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ toPreZeroHypercover.X i₂) →
                (∀ ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ (j : I₁ i₁ i₂),
                    CategoryTheory.CategoryStruct.comp (p₁ j) (toPreZeroHypercover.f i₁) =
                      CategoryTheory.CategoryStruct.comp (p₂ j) (toPreZeroHypercover.f i₂)) →
                  CategoryTheory.PreOneHypercover S
-- Mathlib.NumberTheory.FermatPsp
_private.Mathlib.NumberTheory.FermatPsp.0.Nat.a_id_helper : ∀ {a b : ℕ}, 2 ≤ a → 2 < b → b < (a ^ b - 1) / (a - 1)
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_subset_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₂ ≤ a₁ → b₁ ≤ b₂ → Set.Ioo a₁ b₁ ⊆ Set.Ioo a₂ b₂
-- Mathlib.RingTheory.AlgebraTower
/-- `Basis.smulTower (b : Basis ι R S) (c : Basis ι S A)` is the `R`-basis on `A`
where the `(i, j)`th basis vector is `b j • c i`.  -/
Module.Basis.smulTower' : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : AddCommMonoid A] →
            [inst_3 : Module R S] →
              [inst_4 : Module S A] →
                [inst_5 : Module R A] →
                  [IsScalarTower R S A] →
                    {ι : Type u_5} →
                      {ι' : Type u_6} → Module.Basis ι R S → Module.Basis ι' S A → Module.Basis (ι' × ι) R A
-- Mathlib.MeasureTheory.Group.LIntegral
/-- The Lebesgue integral of a function with respect to an inverse invariant measure is
invariant under the change of variables x ↦ -x.  -/
MeasureTheory.lintegral_neg_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : InvolutiveNeg G] [MeasurableNeg G]
  [μ.IsNegInvariant] (f : G → ENNReal), ∫⁻ (x : G), f (-x) ∂μ = ∫⁻ (x : G), f x ∂μ
-- Mathlib.Algebra.Group.Prod
/-- Combine two `MonoidHom`s `f : M →ₙ* N`, `g : M →ₙ* P` into
`f.prod g : M →ₙ* (N × P)` given by `(f.prod g) x = (f x, g x)`.  -/
MulHom.prod : {M : Type u_3} →
  {N : Type u_4} →
    {P : Type u_5} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.oreDiv_pow : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r : R) (s : ↥S) (n : ℕ),
  Commute r ↑s → (r /ₒ s) ^ n = r ^ n /ₒ s ^ n
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.smul_def : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] (a : M) (x : (i : ι) × α i),
  a • x = Sigma.map id (fun x x_1 => a • x_1) x
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- Forgetting the reflexion yields an equivalence between cocones over a bundled reflexive pair and
coforks on the underlying parallel pair.  -/
CategoryTheory.Limits.reflexiveCoforkEquivCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) →
      CategoryTheory.Limits.ReflexiveCofork F ≌
        CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
          (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_id : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] (A : Rep.{w, u, v} k G),
  Rep.Hom.hom (CategoryTheory.CategoryStruct.id A) = Representation.IntertwiningMap.id A.ρ
-- Mathlib.Data.Sum.Order
Sum.Lex.inl_lt_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] (a : α) (b : β), toLex (Sum.inl a) < toLex (Sum.inr b)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.hole.inj : ∀ {name name_1 : Lean.TSyntax `Lean.binderIdent},
  Lean.Parser.Tactic.MRefinePat.hole name = Lean.Parser.Tactic.MRefinePat.hole name_1 → name = name_1
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddMonoidOfAddOpposite : {M : Type u_1} → [AddMonoid Mᵃᵒᵖ] → AddMonoid Mᵈᵃᵃ
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- A *cylinder set* is the set of all configurations that agree with a given
reference configuration `x` on a fixed finite subset `U` of the index set `G`.

The set `U` is called the *support* of the cylinder.

Intuitively, cylinders specify the "letters" on finitely many coordinates, while
leaving all other coordinates free. For example, in the full shift `{0, 1}^ℤ`,
the cylinder determined by `U = {0, 1}` and `x 0 = 1, x 1 = 0` consists of all
bi-infinite sequences of `0`s and `1`s whose entries on positions `0` and `1`
respectively are `1` and `0`.

When `A` has the discrete topology, cylinder sets form a basis of clopen sets
for the product topology on `G → A`.  -/
SymbolicDynamics.FullShift.cylinder : {A : Type u_1} → {G : Type u_2} → Finset G → (G → A) → Set (G → A)
-- Lean.Elab.MutualDef
/-- Return `some [b, c]` if the given `views` are representing a declaration of the form
```
opaque a b c : Nat
```
 -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.isMultiConstant? : Array Lean.Elab.DefView → Option (List Lean.Name)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_lipschitz : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  LipschitzWith C.toNNReal ⇑(MeasureTheory.L1.setToL1 hT)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_mk' : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (h : ∀ (c : R) (x : A), f (c • x) = c • f x), ⇑(GradedAlgHom.mk' f h) = ⇑f
-- Batteries.Data.UnionFind.Basic
/-- Rank of union-find node  -/
Batteries.UnionFind.rank : Batteries.UnionFind → ℕ → ℕ
-- Mathlib.Analysis.Normed.Field.WithAbs
/-- The completion of a field with respect to a real absolute value.  -/
AbsoluteValue.Completion : {K : Type u_1} → [inst : Field K] → AbsoluteValue K ℝ → Type u_1
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableOn_iff_of_mem_maximalAtlas : ∀ {𝕜 : 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'} {s : Set M}
  {e : OpenPartialHomeomorph M H} {e' : OpenPartialHomeomorph M' H'},
  e ∈ IsManifold.maximalAtlas I 1 M →
    e' ∈ IsManifold.maximalAtlas I' 1 M' →
      s ⊆ e.source →
        Set.MapsTo f s e'.source →
          (MDiff[s] f ↔
            ContinuousOn f s ∧ DifferentiableOn 𝕜 (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s))
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.braidedCategoryCenter : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.BraidedCategory (CategoryTheory.Center C)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.IsModHom.map_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] {Y : C}
  [inst_4 : CategoryTheory.ModObj M Y] (f : X ⟶ Y) [CategoryTheory.IsModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X),
  CategoryTheory.CategoryStruct.comp (m • x) f = m • CategoryTheory.CategoryStruct.comp x f
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.ofNat_add_continuum : ∀ {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n + Cardinal.continuum = Cardinal.continuum
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_apply_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : C} {B : D} (f : F.obj A ⟶ B)
  (g : A ⟶ G.obj B), (adj.homEquiv A B) f = g ↔ f = (adj.homEquiv A B).symm g
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_π_app : ∀ {α : Type u} {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J]
  [inst_2 : SemilatticeInf α] [inst_3 : OrderTop α] (F : CategoryTheory.Functor J α) (x : J),
  (CategoryTheory.Limits.CompleteLattice.finiteLimitCone F).cone.π.app x = CategoryTheory.homOfLE ⋯
-- Init.System.IO
BaseIO.map : {α β : Type} → (α → β) → BaseIO α → BaseIO β
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- This map sends a point `P` on a Weierstrass curve `W'` in affine coordinates
to a representative of its image on ℙ¹ under the x-coordinate map.
We take `![1, 0]` for the point at infinity and `![x, 1]`,
where `x` is the x-coordinate of `P`, for an affine point.

We define it in the general setting of a commutative base ring, even though the definition
of points in this setting is not really correct. For Weierstrass curves over fields, this
gives the correct notion.  -/
WeierstrassCurve.Affine.Point.xRep : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Affine R} → W'.Point → Fin 2 → R
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.mk.inj : ∀ {carrier : Type u} {str : AddCommMonoid carrier} {carrier_1 : Type u} {str_1 : AddCommMonoid carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_principalUnitGroup_iff : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : Kˣ), x ∈ A.principalUnitGroup ↔ A.valuation (↑x - 1) < 1
-- Mathlib.Order.Interval.Set.SuccOrder
Set.Ici.coe_pred_of_not_isMin : ∀ {J : Type u_1} [inst : PartialOrder J] [inst_1 : PredOrder J] {j : J} {i : ↑(Set.Ici j)},
  ¬IsMin i → ↑(Order.pred i) = Order.pred ↑i
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.Hom.iso_comm_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) (X : TopCat),
  CategoryTheory.CategoryStruct.comp ((HP.iso i).hom.app X) ((f.homₚ i).app (TopPair.ofTopCat X)) =
    CategoryTheory.CategoryStruct.comp ((f.hom i).app X) ((HP'.iso i).hom.app X)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_mul_antidiagonal_finsum : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : SMulZeroClass G k]
  (f g : SkewMonoidAlgebra k G) (x : G),
  (f * g).coeff x = ∑ᶠ (p : G × G) (_ : p ∈ {p | p.1 * p.2 = x}), f.coeff p.1 * p.1 • g.coeff p.2
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.maxInsts.injEq : ∀ (n n_1 : ℕ),
  (Lean.Meta.Grind.EMatchTheoremConstraint.maxInsts n = Lean.Meta.Grind.EMatchTheoremConstraint.maxInsts n_1) =
    (n = n_1)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.dvd_of_toWithBotNat_le_toWithBotNat : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (x y : R),
  x ≠ 0 → IsDiscreteValuationRing.toWithBotNat x ≤ IsDiscreteValuationRing.toWithBotNat y → x ∣ y
-- Mathlib.Data.List.Cycle
Cycle.notMem_nil : ∀ {α : Type u_1} (a : α), a ∉ Cycle.nil
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.RightAdjointCommShift.iso.eq_1 : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a : A) [inst_5 : F.CommShift A],
  CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a =
    CategoryTheory.Adjunction.RightAdjointCommShift.iso' adj a (-a) ⋯
-- Mathlib.GroupTheory.Finiteness
/-- An equivalent expression of `AddGroup.fg` in terms of `Set.Finite` instead of `Finset`.  -/
AddGroup.fg_iff : ∀ {G : Type u_3} [inst : AddGroup G], AddGroup.FG G ↔ ∃ S, AddSubgroup.closure S = ⊤ ∧ S.Finite
-- Mathlib.Algebra.DirectSum.Ring
/-- Optional field to allow definitional control of natural powers  -/
DirectSum.GSemiring.gnpow : {ι : Type u_1} →
  {A : ι → Type u_2} →
    {inst : AddMonoid ι} →
      {inst_1 : (i : ι) → AddCommMonoid (A i)} → [self : DirectSum.GSemiring A] → (n : ℕ) → {i : ι} → A i → A (n • i)
-- Mathlib.Algebra.Homology.Embedding.Restriction
ComplexShape.Embedding.restrictionFunctor.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e e_1 : c.Embedding c') (e_e : e = e_1)
  (C : Type u_3) [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : e.IsRelIff]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C], e.restrictionFunctor C = e_1.restrictionFunctor C
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- Eta-expanded form of `iteratedDeriv_sub` -/
iteratedDeriv_fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f g : 𝕜 → F},
  ContDiffAt 𝕜 (↑n) f x →
    ContDiffAt 𝕜 (↑n) g x → iteratedDeriv n (fun i => f i - g i) x = iteratedDeriv n f x - iteratedDeriv n g x
-- Mathlib.Order.Filter.CardinalInter
Filter.mem_ofCardinalUnion : ∀ {α : Type u} {c : Cardinal.{u}} {l : Set (Set α)} (hc : 2 < c)
  {hunion : ∀ (S : Set (Set α)), Cardinal.mk ↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l} {hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l}
  {s : Set α}, s ∈ Filter.ofCardinalUnion l hc hunion hmono ↔ l sᶜ
-- Mathlib.Order.WithBot
IsMax.withBot : ∀ {α : Type u_1} {a : α} [inst : LE α], IsMax a → IsMax ↑a
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  (K : TopologicalSpace.CompactOpens α) (L : TopologicalSpace.CompactOpens β), ↑(K ×ˢ L) = ↑K ×ˢ ↑L
-- Mathlib.Logic.Small.Set
small_pair : ∀ {α : Type u1} (x y : α), Small.{u, u1} ↑{x, y}
-- Mathlib.Topology.UniformSpace.Defs
IsUniformEmbedding.toIsUniformInducing : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformEmbedding f → IsUniformInducing f
-- Mathlib.Data.List.Permutation
_private.Mathlib.Data.List.Permutation.0.Nat.factorial.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.r'.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M),
  AddLocalization.r' S = { r := fun a b => ∃ c, ↑c + (↑b.2 + a.1) = ↑c + (↑a.2 + b.1), iseqv := ⋯, add' := ⋯ }
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiff.sumMap : ∀ {𝕜 : 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] {M' : Type u_16} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {n : WithTop ℕ∞} {E' : Type u_17} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_18} [inst_10 : TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'}
  {N : Type u_20} {N' : Type u_21} [inst_11 : TopologicalSpace N] [inst_12 : TopologicalSpace N']
  [inst_13 : ChartedSpace H' N] [inst_14 : ChartedSpace H' N'] {f : M → N} {g : M' → N'},
  ContMDiff I J n f → ContMDiff I J n g → ContMDiff I J n (Sum.map f g)
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.isUnit_toMatrix_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) {f : M₁ →ₗ[R] M₁},
  IsUnit ((LinearMap.toMatrix v₁ v₁) f) ↔ IsUnit f
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isIso_stalkMap_coprodSpec : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S]
  (x : ↥(AlgebraicGeometry.Spec (CommRingCat.of R) ⨿ AlgebraicGeometry.Spec (CommRingCat.of S))),
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.coprodSpec R S) x)
-- Mathlib.Order.Filter.Map
Filter.map_bot : ∀ {α : Type u_1} {β : Type u_2} {m : α → β}, Filter.map m ⊥ = ⊥
-- Init.Data.Rat.Lemmas
Rat.num_nonneg : ∀ {q : ℚ}, 0 ≤ q.num ↔ 0 ≤ q
-- Mathlib.Data.Ineq
/-- `max R1 R2` computes the strength of the sum of two inequalities. If `t1 R1 0` and `t2 R2 0`,
then `t1 + t2 (max R1 R2) 0`.
 -/
Mathlib.Ineq.max : Mathlib.Ineq → Mathlib.Ineq → Mathlib.Ineq
-- Mathlib.Order.Defs.LinearOrder
compare_le_iff_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, compare a b ≠ Ordering.gt ↔ a ≤ b
-- Aesop.Stats.Basic
Aesop.Stats.ruleStats : Aesop.Stats → Array Aesop.RuleStats
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.IsClosedUnderSubobjects.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f], P Y → P X) → P.IsClosedUnderSubobjects
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.congr_arg : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (f : α →ᵈ β) {x y : α},
  x = y → f x = f y
-- Init.Data.String.Basic
String.Pos.Raw.byteIdx_lt_byteIdx_next : ∀ (s : String) (i : String.Pos.Raw), i.byteIdx < (String.Pos.Raw.next s i).byteIdx
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_pos_of_exists : ∀ {G : Type u} [inst : Monoid G] (n : ℕ), 0 < n → (∀ (g : G), g ^ n = 1) → 0 < Monoid.exponent G
-- Lean.Data.Lsp.Extra
/-- This import is imported twice; once with `meta`, once without.  -/
Lean.Lsp.LeanImportMetaKind.full : Lean.Lsp.LeanImportMetaKind
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.index_union_le : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  (K₁ K₂ : TopologicalSpace.Compacts G) {V : Set G},
  (interior V).Nonempty →
    MeasureTheory.Measure.haar.index (K₁.carrier ∪ K₂.carrier) V ≤
      MeasureTheory.Measure.haar.index K₁.carrier V + MeasureTheory.Measure.haar.index K₂.carrier V
-- Mathlib.Topology.Convenient.HomSpace
Topology.ContinuousMapGeneratedBy.continuousGeneratedBy_dom_prod_iff : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] {T : Type v''} [inst_3 : TopologicalSpace T]
  [∀ (i j : ι), Topology.IsGeneratedBy X (X i × X j)] (g : Y × Z → T),
  Topology.ContinuousGeneratedBy X g ↔
    ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
      Continuous fun x =>
        match x with
        | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
-- Mathlib.Order.LiminfLimsup
Filter.liminf_piecewise : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {u : β → α} {s : Set β}
  [inst_1 : DecidablePred fun x => x ∈ s] {v : β → α},
  Filter.liminf (s.piecewise u v) f = (Filter.bliminf u f fun x => x ∈ s) ⊓ Filter.bliminf v f fun x => x ∉ s
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.symm_ofStarAlgHom : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] [inst_5 : Star A₁] [inst_6 : Star A₂] (f : A₁ →⋆ₐ[R] A₂)
  (g : A₂ →⋆ₐ[R] A₁) (h₁ : g.comp f = StarAlgHom.id R A₁) (h₂ : f.comp g = StarAlgHom.id R A₂),
  (StarAlgEquiv.ofStarAlgHom f g h₁ h₂).symm = StarAlgEquiv.ofStarAlgHom g f h₂ h₁
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.basis.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) [inst_3 : Nontrivial S],
  Algebra.Generators.PresentationOfFreeCotangent.Aux.basis✝ D =
    ((Algebra.Generators.PresentationOfFreeCotangent.Aux.basisRight✝ D).prod
          (Algebra.Generators.PresentationOfFreeCotangent.Aux.basisLeft✝ D)).map
      (Algebra.Generators.PresentationOfFreeCotangent.Aux.cotangentEquivProd✝ D).symm
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- If `χ` and `φ` are multiplicative characters on a finite field `F` with values
in another field `F'` and such that `χφ` is nontrivial, then `J(χ,φ) = g(χ) * g(φ) / g(χφ)`.  -/
jacobiSum_eq_gaussSum_mul_gaussSum_div_gaussSum : ∀ {F : Type u_1} {F' : Type u_2} [inst : Fintype F] [inst_1 : Field F] [inst_2 : Field F'],
  ↑(Fintype.card F) ≠ 0 →
    ∀ {χ φ : MulChar F F'},
      χ * φ ≠ 1 → ∀ {ψ : AddChar F F'}, ψ.IsPrimitive → jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ / gaussSum (χ * φ) ψ
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.relation_mul_id_pow_six_eventuallyEq : ∀ (L : PeriodPair),
  PeriodPair.relation✝ L * id ^ 6 =ᶠ[nhds 0] fun z =>
    (L.derivWeierstrassPExcept 0 z * z ^ 3 - 2) ^ 2 - 4 * (L.weierstrassPExcept 0 z * z ^ 2 + 1) ^ 3 +
        L.g₂ * (L.weierstrassPExcept 0 z * z ^ 6 + z ^ 4) +
      L.g₃ * z ^ 6
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.denumerable_iff : ∀ {α : Type u}, Nonempty (Denumerable α) ↔ Cardinal.mk α = Cardinal.aleph0
-- Mathlib.SetTheory.Ordinal.Topology
/-- **Alias** of the forward direction of `Ordinal.isClosedBelow_iff`. -/
Ordinal.IsClosedBelow.forall_lt : ∀ {S : Set Ordinal.{u_1}} {o : Ordinal.{u_1}}, Ordinal.IsClosedBelow S o → ∀ p < o, p.IsAcc S → p ∈ S