mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- The inclusion map from a component of the coproduct induced by `f` into `S`.  -/
CompHausLike.LocallyConstant.sigmaIncl : {P : TopCat → Prop} →
  [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    {Q : CompHausLike P} →
      {Z : Type (max u w)} →
        (r : LocallyConstant (↑Q.toTop) Z) → (a : Function.Fiber ⇑r) → CompHausLike.LocallyConstant.fiber r a ⟶ Q
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_eq_zero_iff : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {p : α → Prop} {f : α →₀ M},
  (∀ x ∈ f.support, p x) → (Finsupp.subtypeDomain p f = 0 ↔ f = 0)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF →
    (Std.DHashMap.Raw.Const.alter m k f).getKey? k' =
      if (k == k') = true then if (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true then some k else none
      else m.getKey? k'
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.isIso_iff_yoneda_map_bijective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsIso f ↔ ∀ (T : C), Function.Bijective fun x => CategoryTheory.CategoryStruct.comp x f
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- The `PowerBasis` given by `η - 1`.  -/
IsPrimitiveRoot.subOnePowerBasis : {n : ℕ} →
  [NeZero n] →
    (K : Type u) →
      {L : Type v} →
        [inst : Field K] →
          [inst_1 : CommRing L] →
            [IsDomain L] →
              [inst_3 : Algebra K L] → [IsCyclotomicExtension {n} K L] → {ζ : L} → IsPrimitiveRoot ζ n → PowerBasis K L
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.lift_f' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} [inst_3 : F.IsWellOrderContinuous] {j : J} (hj : Order.IsSuccLimit j)
  (s : ↑(⋯.functor.op.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g)).sections),
  (CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.lift hj s).f' =
    CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom hj s
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.curry_mul : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : (a : α) → (b : β a) → Mul (γ a b)]
  (x y : (i : (a : α) × β a) → γ i.fst i.snd), Sigma.curry (x * y) = Sigma.curry x * Sigma.curry y
-- Mathlib.Order.DirectedInverseSystem
/-- It is compatible with a family of bijections relating `F i⁺` to `F i`.  -/
InverseSystem.PEquivOn.compat : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [inst : LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  [inst_1 : SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s : Set ι}
  (self : InverseSystem.PEquivOn f equivSucc s) {i : ι} (hsi : Order.succ i ∈ s) (hi : ¬IsMax i)
  (x : F ↑⟨Order.succ i, hsi⟩), (self.equiv ⟨Order.succ i, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
-- Mathlib.Order.Filter.AtTopBot.Finset
/-- If `f` is a monotone sequence of `Finset`s and each `x` belongs to one of `f n`, then
`Tendsto f atTop atTop`.  -/
Filter.tendsto_atTop_finset_of_monotone : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {f : β → Finset α},
  Monotone f → (∀ (x : α), ∃ n, x ∈ f n) → Filter.Tendsto f Filter.atTop Filter.atTop
-- Std.Http.Data.URI.Basic
Std.Http.URI.instReprPath.repr : Std.Http.URI.Path → ℕ → Std.Format
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.hom_ext : ∀ {X Y : UniformSpaceCat} {f g : X ⟶ Y},
  ⇑(CategoryTheory.ConcreteCategory.hom f) = ⇑(CategoryTheory.ConcreteCategory.hom g) → f = g
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable,
then $[K:F]_s = [K:E]_s$.
It is a special case of `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`, and is an
intermediate result used to prove it.  -/
Field.sepDegree_eq_of_isPurelyInseparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F E],
  Field.sepDegree F K = Field.sepDegree E K
-- Mathlib.AlgebraicGeometry.Stalk
/-- A morphism from `Spec(O_x)` to `X`, which is defined with the help of an affine open
neighborhood `U` of `x`.
 -/
AlgebraicGeometry.IsAffineOpen.fromSpecStalk : {X : AlgebraicGeometry.Scheme} →
  {U : X.Opens} →
    AlgebraicGeometry.IsAffineOpen U → {x : ↥X} → x ∈ U → (AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ X)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- Two measures which are finite on closed-open intervals are equal if they agree on all
open-closed intervals.  -/
MeasureTheory.Measure.ext_of_Ioc' : ∀ {α : Type u_5} [inst : TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α]
  [inst_2 : LinearOrder α] [OrderTopology α] [BorelSpace α] [NoMinOrder α] (μ ν : MeasureTheory.Measure α),
  (∀ ⦃a b : α⦄, a < b → μ (Set.Ioc a b) ≠ ⊤) → (∀ ⦃a b : α⦄, a < b → μ (Set.Ioc a b) = ν (Set.Ioc a b)) → μ = ν
-- Mathlib.Order.Bounded
Set.unbounded_le_Ioi : ∀ {α : Type u_1} [inst : SemilatticeSup α] [NoMaxOrder α] (a : α), Set.Unbounded (fun x1 x2 => x1 ≤ x2) (Set.Ioi a)
-- Batteries.Data.List.Basic
List.zipWithLeftTR.go.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : List β) (a_1 : Array γ),
  List.zipWithLeftTR.go f [] a a_1 = a_1.toList
-- Mathlib.Topology.UniformSpace.Closeds
Filter.HasBasis.uniformity_closeds : ∀ {α : Type u_1} [inst : UniformSpace α] {ι : Sort u_4} {p : ι → Prop} {s : ι → Set (α × α)},
  (uniformity α).HasBasis p s →
    (uniformity (TopologicalSpace.Closeds α)).HasBasis p fun i =>
      Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (s i)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- The component of `expMap` at the place `w`.
 -/
NumberField.mixedEmbedding.fundamentalCone.expMap_single : {K : Type u_1} → [inst : Field K] → NumberField.InfinitePlace K → OpenPartialHomeomorph ℝ ℝ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k fallback : α}, (t.erase k).getKeyD k fallback = fallback
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minEntryD.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3)
  (fallback : (a : α) × β a) (h_1 : (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : (a : α) × β a) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : (a : α) × β a) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) =
    h_1 fallback
-- Mathlib.Order.Hom.Lattice
SupHom.coe_top : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] [inst_2 : Top β], ⇑⊤ = ⊤
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.hasBasis_uniformity : ∀ (R : Type u) [inst : Ring R] (Γ₀ : Type v) [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀],
  (uniformity R).HasBasis (fun x => True) fun γ => {p | Valued.v.restrict (p.2 - p.1) < ↑γ}
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsFibrantResolutionObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C)
  [HomotopicalAlgebra.IsFibrant X],
  HomotopicalAlgebra.IsFibrant (HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj X)
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_addChar_eq : ∀ {M : Type u_3} {R : Type u_4} [inst : AddCommMonoid M] [inst_1 : Ring R] (φ : AddChar M R) (x h : M) (n : ℕ),
  (fwdDiff h)^[n] (⇑φ) x = (φ h - 1) ^ n * φ x
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso_mop_mop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c c' : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso { unmop := c } { unmop := c' } d =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c' c
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.processAtom : Lean.Syntax → Lean.Elab.Term.ToParserDescrM (Lean.Term × ℕ)
-- Mathlib.Analysis.Normed.Lp.SmoothApprox
MeasureTheory.Lp.dense_hasCompactSupport_contDiff : ∀ {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  [inst_6 : NormedSpace ℝ F] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {p : ENNReal},
  p ≠ ⊤ → ∀ [hp₂ : Fact (1 ≤ p)], Dense {f | ∃ g, ↑↑f =ᵐ[μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g}
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets_smul_right : ∀ {R : Type u_1} {E : Type u_6} {ι : Type u_9} [inst : SeminormedRing R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p : SeminormFamily R E ι) (v : E), ∀ U ∈ p.basisSets, ∀ᶠ (x : R) in nhds 0, x • v ∈ U
-- Init.Data.BitVec.Lemmas
BitVec.msb_eq_true_iff_two_mul_ge : ∀ {w : ℕ} {x : BitVec w}, x.msb = true ↔ 2 * x.toNat ≥ 2 ^ w
-- Mathlib.Algebra.Ring.InjSurj
/-- A type endowed with `0`, `1` and `+` is an additive commutative monoid with one, if it admits an
injective map that preserves `0`, `1` and `+` to an additive commutative monoid with one.
See note [reducible non-instances].  -/
Function.Injective.addCommMonoidWithOne : {R : Type u_1} →
  {S : Type u_3} →
    [inst : Zero S] →
      [inst_1 : One S] →
        [inst_2 : Add S] →
          [inst_3 : SMul ℕ S] →
            [inst_4 : NatCast S] →
              [inst_5 : AddCommMonoidWithOne R] →
                (f : S → R) →
                  Function.Injective f →
                    f 0 = 0 →
                      f 1 = 1 →
                        (∀ (x y : S), f (x + y) = f x + f y) →
                          (∀ (n : ℕ) (x : S), f (n • x) = n • f x) → (∀ (n : ℕ), f ↑n = ↑n) → AddCommMonoidWithOne S
-- Mathlib.Data.Multiset.Powerset
Multiset.revzip_powersetAux_perm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → (Multiset.powersetAux l₁).revzip.Perm (Multiset.powersetAux l₂).revzip
-- Mathlib.Data.FinEnum
FinEnum.Quotient.enum : {α : Type u} → [FinEnum α] → (s : Setoid α) → [DecidableRel fun x1 x2 => x1 ≈ x2] → FinEnum (Quotient s)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.subset_vanishingIdeal_zeroLocus : ∀ {R : Type u} [inst : CommSemiring R] (s : Set R), s ⊆ ↑(PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus s))
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).hom
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.instCommRing : {R : Type u_1} →
  [inst : CommRing R] → {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → CommRing (OreLocalization S R)
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingFieldAux.algebra : (n : ℕ) → {K : Type u} → [inst : Field K] → (f : Polynomial K) → Algebra K (Polynomial.SplittingFieldAux n f)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.revMatchAt?_eq : ∀ {s : String.Slice} {pos : s.Pos} {p : Char → Bool},
  String.Slice.Pattern.Model.revMatchAt? p pos =
    if h₀ : ∃ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯) = true then some (pos.prev ⋯) else none
-- Aesop.Options.Public
Aesop.instInhabitedOptions.default : Aesop.Options
-- Lean.Util.Heartbeats
/-- Returns the current `maxHeartbeats`.  -/
Lean.getMaxHeartbeats : Lean.CoreM ℕ
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.epi_iff_range_eq_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (p : F' ⟶ F),
  CategoryTheory.Epi p ↔ CategoryTheory.Subfunctor.range p = ⊤
-- Mathlib.Logic.Basic
Not.imp_symm : ∀ {a b : Prop}, (¬a → b) → ¬b → a
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.id_base : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C),
  (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id ↑X
-- Mathlib.Data.Fintype.Prod
Pi.infinite_of_left : ∀ {ι : Sort u_4} {π : ι → Type u_5} [∀ (i : ι), Nontrivial (π i)] [Infinite ι], Infinite ((i : ι) → π i)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.ComplexEmbedding.lift.congr_simp : ∀ (K : Type u_1) [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K]
  [inst_3 : Algebra.IsAlgebraic k K] (φ φ_1 : k →+* ℂ),
  φ = φ_1 → NumberField.ComplexEmbedding.lift K φ = NumberField.ComplexEmbedding.lift K φ_1
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
RingHom.IsIntegralElem.of_mul_unit : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (x y : S) (r : R),
  f r * y = 1 → f.IsIntegralElem (x * y) → f.IsIntegralElem x
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_neg : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
  [inst_2 : SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (g : ι → G), ⇑f ∘ (-g) = -⇑f ∘ g
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
_private.Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds.0.HurwitzKernelBounds.exp_lt_aux : ∀ {t : ℝ}, 0 < t → Real.exp (-Real.pi * t) < 1
-- Lean.Data.Json.Parser
Lean.Json.Parser.num : Std.Internal.Parsec.String.Parser Lean.JsonNumber
-- Mathlib.Data.Part
Part.mod_def : ∀ {α : Type u_1} [inst : Mod α] (a b : Part α),
  a % b = do
    let y ← a
    Part.map (fun x => y % x) b
-- Lean.Parser.Term
Lean.Parser.Term.letRecDecls.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Util.Notation3
/-- A matcher is a delaboration function that transforms `MatchState`s.  -/
Mathlib.Notation3.Matcher : Type
-- Aesop.Tree.AddRapp
Aesop.AddRapp.mk.inj : ∀ {toRuleApplication : Aesop.RuleApplication} {parent : Aesop.GoalRef} {appliedRule : Aesop.RegularRule}
  {successProbability : Aesop.Percent} {toRuleApplication_1 : Aesop.RuleApplication} {parent_1 : Aesop.GoalRef}
  {appliedRule_1 : Aesop.RegularRule} {successProbability_1 : Aesop.Percent},
  { toRuleApplication := toRuleApplication, parent := parent, appliedRule := appliedRule,
        successProbability := successProbability } =
      { toRuleApplication := toRuleApplication_1, parent := parent_1, appliedRule := appliedRule_1,
        successProbability := successProbability_1 } →
    toRuleApplication = toRuleApplication_1 ∧
      parent = parent_1 ∧ appliedRule = appliedRule_1 ∧ successProbability = successProbability_1
-- Mathlib.Tactic.Linarith.Frontend
/-- An extension of `linarith` with some preprocessing to allow it to solve some nonlinear arithmetic
problems. (Based on Coq's `nra` tactic.) See `linarith` for the available syntax of options,
which are inherited by `nlinarith`; that is, `nlinarith!` and `nlinarith only [h1, h2]` all work as
in `linarith`. The preprocessing is as follows:

* For every subterm `a ^ 2` or `a * a` in a hypothesis or the goal,
  the assumption `0 ≤ a ^ 2` or `0 ≤ a * a` is added to the context.
* For every pair of hypotheses `a1 R1 b1`, `a2 R2 b2` in the context, `R1, R2 ∈ {<, ≤, =}`,
  the assumption `0 R' (b1 - a1) * (b2 - a2)` is added to the context (non-recursively),
  where `R ∈ {<, ≤, =}` is the appropriate comparison derived from `R1, R2`.
 -/
Mathlib.Tactic.nlinarith : Lean.ParserDescr
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_id_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : TensorProduct R N M),
  (LinearMap.rTensor M LinearMap.id) x = x
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.ιMapObjOrZero_mapMap_assoc : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (p : I → J) [inst_1 : X.HasMap p] [inst_2 : Y.HasMap p]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : DecidableEq J] (i : I) (j : J) {Z : C}
  (h : Y.mapObj p j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ιMapObjOrZero p i j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap φ p j) h) =
    CategoryTheory.CategoryStruct.comp (φ i) (CategoryTheory.CategoryStruct.comp (Y.ιMapObjOrZero p i j) h)
-- Mathlib.RingTheory.RootsOfUnity.Minpoly
/-- Let `P` be the minimal polynomial of a root of unity `μ` and `Q` be the minimal polynomial of
`μ ^ p`, where `p` is a prime that does not divide `n`. Then `P` divides `Q ^ p` modulo `p`.  -/
IsPrimitiveRoot.minpoly_dvd_pow_mod : ∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n →
    ∀ [IsDomain K] [CharZero K] {p : ℕ} [hprime : Fact (Nat.Prime p)],
      ¬p ∣ n →
        Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣
          Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) ^ p
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_eq_mod_256_iff : ∀ (a : UInt8) (b : UInt16), a.toUInt16 = b % 256 ↔ a = b.toUInt8
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_succ_right_eq_push : ∀ {m n : ℕ}, m ≤ n → (m...n + 1).toArray = (m...n).toArray.push n
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instFullMonForget₂Mon : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.Grp.forget₂Mon C).Full
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.eqToHom_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} (hF : X = Y),
  CategoryTheory.eqToHom hF = { base := CategoryTheory.eqToHom ⋯, fiber := CategoryTheory.eqToHom ⋯ }
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.mono_num : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {s : Set E} {c c' : NNReal}, c ≤ c' → ApproximatesLinearOn f f' s c → ApproximatesLinearOn f f' s c'
-- Mathlib.Data.Tree.Basic
/-- **Alias** of `BinaryTree.numNodes`.  -/
Tree.numNodes : {α : Type u_1} → Tree α → ℕ
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.forget_mapComp_inv : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {a b c : CategoryTheory.Bicategory.InducedBicategory C F} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.Bicategory.InducedBicategory.forget.mapComp f g).inv =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.hom g.hom)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorLeftTensor_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (CategoryTheory.MonoidalCategory.tensorLeftTensor X Y).hom.app Z =
    (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
sigmaAntidiagonalEquivProd.eq_1 : sigmaAntidiagonalEquivProd =
  { toFun := fun x => divisorsAntidiagonalFactors x.fst x.snd, invFun := fun x => ⟨⟨↑x.1 * ↑x.2, ⋯⟩, ⟨(↑x.1, ↑x.2), ⋯⟩⟩,
    left_inv := sigmaAntidiagonalEquivProd._proof_4, right_inv := sigmaAntidiagonalEquivProd._proof_3 }
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.φ_four : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R),
  W.φ 4 =
    Polynomial.C Polynomial.X * Polynomial.C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 -
        Polynomial.C W.preΨ₄ * W.ψ₂ ^ 4 * Polynomial.C W.Ψ₃ +
      Polynomial.C W.Ψ₃ ^ 4
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
/-- A sequence converges if every subsequence has a convergent subsequence.  -/
Filter.tendsto_of_subseq_tendsto : ∀ {α : Type u_1} {ι : Type u_3} {x : ι → α} {f : Filter α} {l : Filter ι} [l.IsCountablyGenerated],
  (∀ (ns : ℕ → ι), Filter.Tendsto ns Filter.atTop l → ∃ ms, Filter.Tendsto (fun n => x (ns (ms n))) Filter.atTop f) →
    Filter.Tendsto x l f
-- Mathlib.Logic.Relation
Relation.reflexive_reflGen : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Refl (Relation.ReflGen r)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- A measurable equivalence is a measurable embedding.  -/
MeasurableEquiv.measurableEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β),
  MeasurableEmbedding ⇑e
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharType.separator : Lean.FuzzyMatching.CharType
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Turn an element of a type `F` satisfying `OrderHomClass F α β` and `AddMonoidHomClass F α β`
into an actual `OrderAddMonoidHom`.
This is declared as the default coercion from `F` to `α →+o β`.  -/
OrderMonoidHomClass.toOrderAddMonoidHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : AddZeroClass α] →
            [inst_3 : AddZeroClass β] →
              [inst_4 : FunLike F α β] → [OrderHomClass F α β] → [AddMonoidHomClass F α β] → F → α →+o β
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_left_cancel : ∀ {M : Type u_1} [inst : Monoid M] {a b c : M}, IsUnit a → a * b = a * c → b = c
-- Mathlib.Algebra.Category.Grp.Shrink
GrpCat.shrinkFunctorMap_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C GrpCat} (τ : F ⟶ G)
  [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)] [inst_2 : ∀ (X : C), Small.{w, w'} ↑(G.obj X)] (X : C),
  (GrpCat.shrinkFunctorMap τ).app X =
    GrpCat.ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (GrpCat.Hom.hom (τ.app X))).comp Shrink.mulEquiv.toMonoidHom)