mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.mul : Lean.Grind.Linarith.Poly → ℤ → Lean.Grind.Linarith.Poly
-- Mathlib.Logic.Equiv.Finset
Denumerable.lower'.eq_def : ∀ (x : List ℕ) (x_1 : ℕ),
  Denumerable.lower' x x_1 =
    match x, x_1 with
    | [], x => []
    | m :: l, n => (m - n) :: Denumerable.lower' l (m + 1)
-- Mathlib.Data.Int.Fib.Lemmas
/-- Auxiliary for `Int.fib_succ_mul_fib_pred_sub_fib_sq`  -/
_private.Mathlib.Data.Int.Fib.Lemmas.0.Int.fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq : ∀ (n : ℕ), Int.fib (↑n + 1) * Int.fib (↑n - 1) - Int.fib ↑n ^ 2 = (-1) ^ n
-- Mathlib.Computability.Primrec.List
/-- If `R a b` is decidable, then for any fixed `n` and `y`, `g n y ↔ ∀ x < n, R x y` is a
primitive recursive relation.  -/
PrimrecRel.forall_lt : ∀ {R : ℕ → ℕ → Prop}, PrimrecRel R → PrimrecRel fun n y => ∀ x < n, R x y
-- Lean.Data.NameTrie
Lean.NamePart.str.inj : ∀ {s s_1 : String}, Lean.NamePart.str s = Lean.NamePart.str s_1 → s = s_1
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  T ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C ↔
    Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Algebra.Group.Defs
/-- Auxiliary typeclass for types with an involutive `Neg`.  -/
InvolutiveNeg : Type u_2 → Type u_2
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.gfpApprox_mem_fixedPoints_of_eq : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a b c : Ordinal.{u}},
  f x ≤ x →
    a < b →
      a ≤ c →
        OrdinalApprox.gfpApprox f x a = OrdinalApprox.gfpApprox f x b →
          OrdinalApprox.gfpApprox f x c ∈ Function.fixedPoints ⇑f
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Kind.monoidal : Mathlib.Tactic.Widget.StringDiagram.Kind
-- Mathlib.Data.Set.Basic
Equiv.setSubtypeComm_apply : ∀ {α : Type u_1} (p : α → Prop) (s : Set { a // p a }), (Equiv.setSubtypeComm p) s = ⟨{a | ∃ (h : p a), ⟨a, h⟩ ∈ s}, ⋯⟩
-- Mathlib.Data.NNReal.Defs
NNReal.coe_nnqsmul : ∀ (q : ℚ≥0) (x : NNReal), ↑(q • x) = q • ↑x
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.cpolynomialOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {x : E},
  HasFiniteFPowerSeriesOnBall f p x n r → CPolynomialOn 𝕜 f (Metric.eball x r)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.IsRegular.mk : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} [toIsProper : P.IsProper], WellFounded P.AncestralRel → P.IsRegular
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.add_lt_of_neg_of_le : ∀ {α : Type u} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {a b c : α},
  a < 0 → b ≤ c → a + b < c
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAtChain_iff : ∀ {pat s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAtChain pat pos₁ pos₂ ↔
    ∃ (h : pos₁ ≤ pos₂), ∃ n, (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat.copy)
-- Mathlib.Order.RelIso.Set
Subrel.instReflSubtype : ∀ {α : Type u_1} (r : α → α → Prop) [Std.Refl r] (p : α → Prop), Std.Refl (Subrel r p)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.left : {J : CategoryTheory.Limits.MulticospanShape} → J.L → CategoryTheory.Limits.WalkingMulticospan J
-- Mathlib.NumberTheory.FrobeniusNumber
/-- The gcd of a set of natural numbers is defined to be the nonnegative generator
of the ideal of `ℤ` generated by them.  -/
Nat.setGcd : Set ℕ → ℕ
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.Arrows.secondMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type t}
  [inst_1 : Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B)
  [inst_2 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks],
  CategoryTheory.Equalizer.Presieve.Arrows.secondMap P X π =
    CategoryTheory.Limits.Pi.lift fun x =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => P.obj (Opposite.op (X i))) x.2)
        (P.map (CategoryTheory.Limits.pullback.snd (π x.1) (π x.2)).op)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofChoiceInfo.sizeOf_spec : ∀ (i : Lean.Elab.ChoiceInfo), sizeOf (Lean.Elab.Info.ofChoiceInfo i) = 1 + sizeOf i
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Induct using `tprodCoeff`  -/
PiTensorProduct.induction_on' : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {motive : (PiTensorProduct R fun i => s i) → Prop}
  (z : PiTensorProduct R fun i => s i),
  (∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R r f)) →
    (∀ (x y : PiTensorProduct R fun i => s i), motive x → motive y → motive (x + y)) → motive z
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.IsPartition.eq_of_boxes_subset : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I},
  π₁.IsPartition → π₁.boxes ⊆ π₂.boxes → π₁ = π₂
-- Init.Data.String.Lemmas.Splits
String.Slice.copy_slice_eq_append_of_lt : ∀ {s : String.Slice} {p q : s.Pos} (h : p < q),
  (s.slice p q ⋯).copy = String.singleton (p.get ⋯) ++ (s.slice (p.next ⋯) q ⋯).copy
-- Mathlib.Algebra.Group.Even
IsSquare.pow : ∀ {α : Type u_2} [inst : Monoid α] {a : α} (n : ℕ), IsSquare a → IsSquare (a ^ n)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.Indep.fundCircuit_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {e : α},
  M.Indep I → e ∈ M.closure I → e ∉ I → M.IsCircuit (M.fundCircuit e I)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.hP : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  (self : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ), self.P.HasCardinalLT κ
-- Mathlib.Geometry.Euclidean.Inversion.Basic
/-- Distance from the center of an inversion to the image of a point under the inversion. This
formula accidentally works for `x = c`.  -/
EuclideanGeometry.dist_center_inversion : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c x : P) (R : ℝ), dist c (EuclideanGeometry.inversion c R x) = R ^ 2 / dist c x
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.Quotient.addGroup : {G : Type u_1} → [inst : AddGroup G] → (N : AddSubgroup G) → [nN : N.Normal] → AddGroup (G ⧸ N)
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- A morphism from the "infimum" of two objects in `MonoOver A` to the second object.  -/
CategoryTheory.MonoOver.infLERight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {A : C} → (f g : CategoryTheory.MonoOver A) → (CategoryTheory.MonoOver.inf.obj f).obj g ⟶ g
-- Mathlib.Analysis.Calculus.Deriv.Linear
LinearMap.derivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} (e : 𝕜 →ₗ[𝕜] F), UniqueDiffWithinAt 𝕜 s x → derivWithin (⇑e) s x = e 1
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.mem_finset_iff : ∀ {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) (i : Fin (n + 2)),
  i ∈ SimplexCategory.II.finset f x ↔
    i = Fin.last (n + 1) ∨ ∃ (h : i ≠ Fin.last (n + 1)), x ≤ (f (i.castPred h)).castSucc
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.instBEqMon.beq.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (a : Lean.Grind.CommRing.Power)
  (a_1 : Lean.Grind.CommRing.Mon) (b : Lean.Grind.CommRing.Power) (b_1 : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit)
  (h_2 :
    (a : Lean.Grind.CommRing.Power) →
      (a_2 : Lean.Grind.CommRing.Mon) →
        (b : Lean.Grind.CommRing.Power) →
          (b_2 : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult a a_2) (Lean.Grind.CommRing.Mon.mult b b_2))
  (h_3 : (x x_1 : Lean.Grind.CommRing.Mon) → motive x x_1),
  (match Lean.Grind.CommRing.Mon.mult a a_1, Lean.Grind.CommRing.Mon.mult b b_1 with
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => h_1 ()
    | Lean.Grind.CommRing.Mon.mult a a_2, Lean.Grind.CommRing.Mon.mult b b_2 => h_2 a a_2 b b_2
    | x, x_1 => h_3 x x_1) =
    h_2 a a_1 b b_1
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.IsDetpBalanced.refl : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (A : Matrix n n R)
  (a : R), A.IsDetpBalanced a a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k fallback : α}, (List.map Prod.fst l).contains k = false → (Std.HashMap.ofList l).getKeyD k fallback = fallback
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.comp_continuous_iff' : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {γ : Type u_3}
  [inst_2 : TopologicalSpace γ] (h : α ≃ᵢ β) {f : β → γ}, Continuous (f ∘ ⇑h) ↔ Continuous f
-- Mathlib.Data.Vector.MapLemmas
/-- If an accumulation function `f`, produces the same output bits regardless of accumulation state,
then the state is redundant and can be optimized out.
 -/
List.Vector.mapAccumr₂_eq_map₂_of_unused_state : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {xs : List.Vector α n} {ys : List.Vector β n}
  (f : α → β → σ → σ × γ) (f' : α → β → γ) (s : σ),
  (∀ (a : α) (b : β) (s : σ), (f a b s).2 = f' a b) →
    (List.Vector.mapAccumr₂ f xs ys s).2 = List.Vector.map₂ (fun x y => (f x y s).2) xs ys
-- Mathlib.Data.Multiset.Fold
Multiset.fold_distrib : ∀ {α : Type u_1} {β : Type u_2} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] {f g : β → α}
  (u₁ u₂ : α) (s : Multiset β),
  Multiset.fold op (op u₁ u₂) (Multiset.map (fun x => op (f x) (g x)) s) =
    op (Multiset.fold op u₁ (Multiset.map f s)) (Multiset.fold op u₂ (Multiset.map g s))
-- Plausible.Testable
/-- Enable tracing of values that fulfilled the property and were thus discarded.
 -/
Plausible.Configuration.traceSuccesses : Plausible.Configuration → Bool
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.skipSuffix?_char_eq_some_iff : ∀ {c : Char} {s : String} {pos : s.Pos},
  s.skipSuffix? c = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ (s.endPos.prev h).get ⋯ = c
-- Mathlib.Logic.Encodable.Basic
Encodable.mem_decode₂' : ∀ {α : Type u_1} [inst : Encodable α] {n : ℕ} {a : α},
  a ∈ Encodable.decode₂ α n ↔ a ∈ Encodable.decode n ∧ Encodable.encode a = n
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.iterate_derivative_T_eval_one_eq_div : ∀ {𝔽 : Type u_3} [inst : Field 𝔽] [CharZero 𝔽] (n : ℤ) (k : ℕ),
  Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T 𝔽 n)) =
    ↑(∏ l ∈ Finset.range k, (n ^ 2 - ↑l ^ 2)) / ↑(∏ l ∈ Finset.range k, (2 * l + 1))
-- Std.Data.ExtHashMap.Basic
/-- Hash maps.

This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
and an array of buckets, where each bucket is a linked list of key-value pairs. The number of buckets
is always a power of two. The hash map doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.

The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
avoid expensive copies.

The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.

In contrast to regular hash maps, `Std.ExtHashMap` offers several extensionality lemmas
and therefore has more lemmas about equality of hash maps. This however also makes it lose the
ability to iterate freely over hash maps.

These hash maps contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, `Std.HashMap.Raw` and
`Std.HashMap.Raw.WF` unbundle the invariant from the hash map. When in doubt, prefer
`HashMap` or `ExtHashMap` over `HashMap.Raw`.

Dependent hash maps, in which keys may occur in their values' types, are available as
`Std.ExtDHashMap` in the module `Std.Data.ExtDHashMap`.
 -/
Std.ExtHashMap : (α : Type u) → Type v → [BEq α] → [Hashable α] → Type (max u v)
-- Init.Data.SInt.Basic
/-- Signed 32-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 32-bit value.
 -/
Int32 : Type
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isLimitConeOfCoconeLeftOp_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.leftOp}
  (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.isLimitConeOfCoconeLeftOp F hc).lift s =
    (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry?.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.leaf.maxEntry? = none
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to negative infinity along a nontrivial filter `l`,
then `fun x ↦ f x / r` tends to infinity if and only if `r < 0`.  -/
Filter.tendsto_div_const_atTop_iff_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto f l Filter.atBot → (Filter.Tendsto (fun x => f x / r) l Filter.atTop ↔ r < 0)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.NormalExpr.nterm.inj : ∀ {e : Lean.Expr} {n : Lean.Expr × ℤ} {x : ℕ × Lean.Expr} {a : Mathlib.Tactic.Abel.NormalExpr} {e_1 : Lean.Expr}
  {n_1 : Lean.Expr × ℤ} {x_1 : ℕ × Lean.Expr} {a_1 : Mathlib.Tactic.Abel.NormalExpr},
  Mathlib.Tactic.Abel.NormalExpr.nterm e n x a = Mathlib.Tactic.Abel.NormalExpr.nterm e_1 n_1 x_1 a_1 →
    e = e_1 ∧ n = n_1 ∧ x = x_1 ∧ a = a_1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- A left homology data for a short complex `S` consists of morphisms `i : K ⟶ S.X₂` and
`π : K ⟶ H` such that `i` identifies `K` to the kernel of `g : S.X₂ ⟶ S.X₃`,
and that `π` identifies `H` to the cokernel of the induced map `f' : S.X₁ ⟶ K`  -/
CategoryTheory.ShortComplex.LeftHomologyData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → Type (max u_1 v_1)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.rightOp_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ D} (α : F ⟶ G) (x : C),
  (CategoryTheory.NatTrans.rightOp α).app x = (α.app (Opposite.op x)).op
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.reverse_involutive : ∀ {n : ℕ}, Function.Involutive Composition.reverse
-- Mathlib.MeasureTheory.Group.Convolution
/-- To get commutativity, we need the underlying multiplication to be commutative.  -/
MeasureTheory.Measure.mconv_comm : ∀ {M : Type u_2} [inst : CommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] (μ ν : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν], μ.mconv ν = ν.mconv μ
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instT0SpaceCarrierCarrierCommRingCat : ∀ (X : AlgebraicGeometry.Scheme), T0Space ↥X
-- Mathlib.RingTheory.Ideal.Over
/-- `R / p` has a canonical map to `S / pS`.  -/
Ideal.Quotient.algebraQuotientMapQuotient : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Type u_2} →
      [inst_1 : CommRing S] →
        {p : Ideal R} → [inst_2 : Algebra R S] → Algebra (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
-- Mathlib.GroupTheory.EckmannHilton
/-- If a type carries an additive group structure that distributes over a unital binary
operation, then the additive group is commutative.  -/
EckmannHilton.addCommGroup : {X : Type u} →
  {m₁ : X → X → X} →
    {e₁ : X} →
      EckmannHilton.IsUnital m₁ e₁ →
        [G : AddGroup X] → (∀ (a b c d : X), m₁ (a + b) (c + d) = m₁ a c + m₁ b d) → AddCommGroup X
-- Mathlib.Computability.NFA
DFA.toNFA_step : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (a : α), M.toNFA.step s a = {M.step s a}
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- An element is in `pinGroup Q` if and only if `star x` is in `pinGroup Q`.
See `star_mem` for only one direction.  -/
pinGroup.star_mem_iff : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, star x ∈ pinGroup Q ↔ x ∈ pinGroup Q
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.riemannianEDist_def : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_5} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_6} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] (x y : M),
  Manifold.riemannianEDist I x y =
    ⨅ γ,
      ⨅ (_ : ContMDiff (modelWithCornersEuclideanHalfSpace 1) I 1 ⇑γ), ∫⁻ (x_2 : ↑unitInterval), ‖(mfderiv% ⇑γ x_2) 1‖ₑ
-- Mathlib.Order.Interval.Multiset
/-- The multiset of elements `x` such that `a < x`. Basically `Set.Ioi a` as a multiset.  -/
Multiset.Ioi : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderTop α] → α → Multiset α
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_sum_eq_sum_toLeft_add_sum_toRight : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] (s : Finset (ι ⊕ κ)) (f : ι ⊕ κ → M),
  ∑ x ∈ s, f x = ∑ x ∈ s.toLeft, f (Sum.inl x) + ∑ x ∈ s.toRight, f (Sum.inr x)
-- Mathlib.Data.Finset.Sym
Finset.Nonempty.sym : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α], s.Nonempty → ∀ (n : ℕ), (s.sym n).Nonempty
-- Init.Data.List.Lemmas
List.map_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} {α_1 : Type u_2} {f : α → α_1},
  List.map f (List.replicate n a) = List.replicate n (f a)
-- Mathlib.Data.List.Sigma
/-- Replaces the first value with key `a` by `b`.  -/
List.kreplace : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → β a → List (Sigma β) → List (Sigma β)
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- Let `A : ι' × ι → K`, which we can interpret as a linear map from `ι → K` to `ι' → K`.
Let `x : ι → K` be a tuple. Then the multiplicative height of `A x` is bounded by
`#ι ^ totalWeight K * mulHeight A * mulHeight x` (if `ι` is nonempty).

Note: We use the uncurried form of `A` so that we can write `mulHeight A`.  -/
Height.mulHeight_linearMap_apply_le : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_2} {ι' : Type u_3} [inst_1 : Fintype ι] [Finite ι']
  [inst_3 : Height.AdmissibleAbsValues K] [Nonempty ι] (A : ι' × ι → K) (x : ι → K),
  (Height.mulHeight fun j => ∑ i, A (j, i) * x i) ≤
    ↑(Nat.card ι) ^ Height.totalWeight K * Height.mulHeight A * Height.mulHeight x
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.coe_support : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R} [inst_1 : P.HasIdealSupport], ↑P.support = ↑P ∩ -↑P
-- Std.Do.Triple.SpecLemmas
liftM.eq_1 : @liftM = @monadLift
-- Qq.Match
_private.Qq.Match.0.Qq.Impl.getPatVars.isPatVar : Lean.Syntax → Bool
-- Mathlib.MeasureTheory.Integral.IntervalAverage
/-- Interval averages are invariant when functions change along discrete sets.  -/
intervalAverage_congr_codiscreteWithin : ∀ {a b : ℝ} {f₁ f₂ : ℝ → ℝ},
  f₁ =ᶠ[Filter.codiscreteWithin (Set.uIoc a b)] f₂ → ⨍ (x : ℝ) in a..b, f₁ x = ⨍ (x : ℝ) in a..b, f₂ x
-- Mathlib.Analysis.Normed.Module.Bases
/-- Coercion from a `GeneralSchauderBasis` to the underlying basis function.  -/
instCoeFunGeneralSchauderBasisForall : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} →
      [inst_1 : NormedAddCommGroup X] →
        [inst_2 : NormedSpace 𝕜 X] →
          {β : Type u_3} → {L : SummationFilter β} → CoeFun (GeneralSchauderBasis β 𝕜 X L) fun x => β → X
-- Mathlib.Analysis.Normed.Order.UpperLower
IsClopen.upperClosure_pi : ∀ {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)}, IsClopen s → BddBelow s → IsClopen ↑(upperClosure s)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddEquiv.addSubmonoidMap_symm_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M)
  (g : ↥(AddSubmonoid.map (↑e) S)), (e.addSubmonoidMap S).symm g = ⟨e.symm ↑g, ⋯⟩
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.closed : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (S : L.Substructure M),
  ↑S ∈ (FirstOrder.Language.Substructure.closure L).closed
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.AbelianStruct.imageι_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {f : X ⟶ Y} (self : CategoryTheory.Abelian.AbelianStruct f) {Z : C} (h : self.cokernelCofork.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.imageι
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π self.cokernelCofork) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instReflectsLimitsOfSizeModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w, w, w, max (max u v) (w + 1), max u (w + 1)}
    (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k))
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Continuity from above: the measure of the intersection of a sequence of measurable
sets such that one has finite measure is the limit of the measures of the partial intersections.  -/
MeasureTheory.tendsto_measure_iInter_le : ∀ {α : Type u_8} {ι : Type u_9} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] [inst : Preorder ι]
  {f : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ) →
    (∃ i, μ (f i) ≠ ⊤) → Filter.Tendsto (fun i => μ (⋂ j, ⋂ (_ : j ≤ i), f j)) Filter.atTop (nhds (μ (⋂ i, f i)))
-- Aesop.Rule.Forward
/-- Compare two rule priorities. Less means higher priority ('better').
Norm/safe rules have higher priority than unsafe rules. Among norm/safe rules,
lower penalty is better. Among unsafe rules, higher percentage is better.  -/
Aesop.ForwardRulePriority.compare : Aesop.ForwardRulePriority → Aesop.ForwardRulePriority → Ordering
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsG2.mk : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [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}
  [toIsValuedIn : P.IsValuedIn ℤ] [toIsReduced : P.IsReduced] [toIsIrreducible : P.IsIrreducible],
  (∃ i j, P.pairingIn ℤ i j = -3) → P.IsG2