mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.ring.inj : ∀ {c : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr} {lhs : Lean.Meta.Grind.Arith.Linear.LinExpr}
  {c_1 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr} {lhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.ring c lhs =
      Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.ring c_1 lhs_1 →
    c = c_1 ∧ lhs = lhs_1
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Restriction of partial equivs respects equivalence.  -/
PartialEquiv.EqOnSource.restr : ∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β}, e ≈ e' → ∀ (s : Set α), e.restr s ≈ e'.restr s
-- Mathlib.Algebra.Algebra.Hom
/-- Each element of the monoid defines an algebra homomorphism.

This is a stronger version of `MulSemiringAction.toRingHom` and
`DistribSMul.toLinearMap`.  -/
MulSemiringAction.toAlgHom : {M : Type u_1} →
  (R : Type u_3) →
    (A : Type u_4) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Monoid M] → [inst_4 : MulSemiringAction M A] → [SMulCommClass M R A] → M → A →ₐ[R] A
-- Init.Data.UInt.Lemmas
USize.toUInt16_mul : ∀ (a b : USize), (a * b).toUInt16 = a.toUInt16 * b.toUInt16
-- Lean.ToExpr
Lean.ToExpr.mk : {α : Type u} → (α → Lean.Expr) → Lean.Expr → Lean.ToExpr α
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          (diag : CategoryTheory.Functor J C) →
            (ι : diag ⟶ (CategoryTheory.Functor.const J).obj X) →
              CategoryTheory.Limits.IsColimit { pt := X, ι := ι } → CategoryTheory.Limits.ColimitPresentation J X
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.isUnit_sqrt_iff : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A),
  autoParam (0 ≤ a) CFC.isUnit_sqrt_iff._auto_1 → (IsUnit (CFC.sqrt a) ↔ IsUnit a)
-- Mathlib.Algebra.Group.Units.Defs
Units.mk.sizeOf_spec : ∀ {α : Type u} [inst : Monoid α] [inst_1 : SizeOf α] (val inv : α) (val_inv : val * inv = 1) (inv_val : inv * val = 1),
  sizeOf { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val } =
    1 + sizeOf val + sizeOf inv + sizeOf val_inv + sizeOf inv_val
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_eq_zero_iff : ∀ {θ : Real.Angle}, θ.sign = 0 ↔ θ = 0 ∨ θ = ↑Real.pi
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.succ : Nat.Partrec.Code
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.B₁_inv : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R}, IsCHSHTuple A₀ A₁ B₀ B₁ → B₁ ^ 2 = 1
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.isPath_takeUntil : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} [inst : DecidableEq V] {c : G.Walk v v},
  c.IsCycle → ∀ (h : w ∈ c.support), (c.takeUntil w h).IsPath
-- Mathlib.Analysis.Convex.Strong
UniformConcaveOn.add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {φ ψ : ℝ → ℝ} {s : Set E} {f g : E → ℝ},
  UniformConcaveOn s φ f → UniformConcaveOn s ψ g → UniformConcaveOn s (φ + ψ) (f + g)
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.mulEquivHaarChar_smul_eq_comap : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure]
  [μ.Regular] (φ : G ≃ₜ* G), MeasureTheory.mulEquivHaarChar φ • μ = MeasureTheory.Measure.comap (⇑φ) μ
-- Mathlib.Algebra.Category.Grp.Yoneda
/-- The Hom bifunctor sending a type `X` and a commutative group `G` to the commutative group
`X → G` with pointwise operations.

This is also the coyoneda embedding of `Type` into `CommGrpCat`-valued presheaves of commutative
groups.  -/
CommGrpCat.coyonedaType : CategoryTheory.Functor Type uᵒᵖ (CategoryTheory.Functor CommGrpCat CommGrpCat)
-- Lean.Elab.MutualInductive
/-- Solves for level metavariables in constructor argument types that are completely determined by the resulting type.
The `simplifyResultingUniverse` of the resulting universe level `u` must be of the form `r+k`, where `r` is a parameter or zero,
otherwise inference is ambiguous.
Ambiguity example: `?v ≤ max a b` could be satisfied by either constraint `?v ≤ a` or `?v ≤ b`.
Possibly `r` is a metavariable -- in that case, since it will eventually be turned into a parameter
in `levelMVarToParamAtInductives`, we work with it as if it is a parameter here.

This only assigns if there is a *unique* solution, though we will take a non-constant solution over
a constant one. This function does not throw errors. For underconstrained metavariables it simply
doesn't assign to them. Even constraint issues are ignored, since these will be reported later.
We also assume that `imax` is effectively `max`.

The rules imply that the only assignments we will ever consider are `?v = 0` or `?v = r`.
From each universe constraint, we get simple constraints of the form `?v ≤ r + k'`,
with `k' : Int` like in `inferResultingUniverse`.
Consider the cases:
- if `r=0`, then we must have `k'≥0` to have a solution, and `k'≤0` to have a unique solution.
- if `r` is a parameter, then if `k'>0` there are multiple non-constant solutions, and if
  `k'<0` then there are no solutions that work for all values of `r`. We must have `k'=0`.
Thus, the solution to such simple constraints is always `?v = r` if `k' = 0`.

One wrinkle to this is that we wish to avoid assigning `?u = 0` in some cases due examples like the following
that lead to counterintuitive behavior:
```
inductive Bar : Type
| foobar {Foo} : Foo → Bar
```
Since `Foo : Sort ?u : Type ?u`, propagation causes `?u = 0`, and so `Foo : Prop`.
We avoid assigning level metavariables to `0` if it could cause a field to become a `Prop`.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.propagateUniversesToConstructors : ℕ → List Lean.InductiveType → Lean.Elab.Command.ResultingUniverseResult✝ → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.isConnected_iff_of_equivalence : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  (e : J ≌ K), CategoryTheory.IsConnected J ↔ CategoryTheory.IsConnected K
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Complex.sinh` is complex analytic.  -/
Complex.analyticOn_sinh : ∀ {s : Set ℂ}, AnalyticOn ℂ Complex.sinh s
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
CategoryTheory.ObjectProperty.tStructure_isGE_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : P.IsTriangulated]
  [h : P.HasInducedTStructure t] (X : P.FullSubcategory) (n : ℤ), (P.tStructure t).IsGE X n ↔ t.IsGE X.obj n
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.toList_flatMapAfter : ∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α m]
  [Std.Iterators.Finite α₂ m] {f : β → Std.IterM m γ} {it₁ : Std.IterM m β} {it₂ : Option (Std.IterM m γ)},
  (Std.IterM.flatMapAfter f it₁ it₂).toList =
    match it₂ with
    | none => List.flatten <$> (Std.IterM.mapM (fun b => (f b).toList) it₁).toList
    | some it₂ => do
      let __do_lift ← it₂.toList
      let __do_lift_1 ← List.flatten <$> (Std.IterM.mapM (fun b => (f b).toList) it₁).toList
      pure (__do_lift ++ __do_lift_1)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.IsSheafFor.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w))
  (R : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.IsSheafFor P R =
    ∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃! t, x.IsAmalgamation t
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdFstIsoProd_inv_snd_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Z] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
  [inst_3 : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h)) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_nonunits_iff : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) {x : K}, x ∈ A.nonunits ↔ A.valuation x < 1
-- Mathlib.Algebra.FreeAlgebra
/-- An induction principle for the free algebra.

If `C` holds for the `algebraMap` of `r : R` into `FreeAlgebra R X`, the `ι` of `x : X`, and is
preserved under addition and multiplication, then it holds for all of `FreeAlgebra R X`.
 -/
FreeAlgebra.induction : ∀ (R : Type u_1) (X : Type u_2) [inst : CommSemiring R] {motive : FreeAlgebra R X → Prop},
  (∀ (r : R), motive ((algebraMap R (FreeAlgebra R X)) r)) →
    (∀ (x : X), motive (FreeAlgebra.ι R x)) →
      (∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a * b)) →
        (∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a + b)) → ∀ (a : FreeAlgebra R X), motive a
-- Lean.Meta.Tactic.CasesOnStuckLHS
_private.Lean.Meta.Tactic.CasesOnStuckLHS.0.Lean.Meta.casesOnStuckLHS.findFVar? : Lean.Expr → Lean.MetaM (Option Lean.FVarId)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
/-- Given a morphism `φ : R ⟶ R'` of presheaves of types and `r' : R'.obj X`,
this is the family of elements of `R` defined over the sieve `Presheaf.imageSieve φ r'`
which sends a map in this sieve to an arbitrary choice of a preimage of the
restriction of `r'`.  -/
CategoryTheory.Presieve.FamilyOfElements.localPreimage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R R' : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      (φ : R ⟶ R') →
        {X : Cᵒᵖ} →
          (r' : R'.obj X) → CategoryTheory.Presieve.FamilyOfElements R (CategoryTheory.Presheaf.imageSieve φ r').arrows
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansionRingHom_apply : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [inst : Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (k : ℤ)
  (f : ModularForm Γ k),
  (ModularForm.qExpansionRingHom h hh hΓ) ((DirectSum.of (ModularForm Γ) k) f) = UpperHalfPlane.qExpansion h ⇑f
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
Subsemigroup.center_le_centralizer : ∀ {M : Type u_1} [inst : Semigroup M] (S : Set M), Subsemigroup.center M ≤ Subsemigroup.centralizer S
-- Mathlib.Data.Rat.Cast.CharZero
NNRat.cast_inv : ∀ {α : Type u_3} [inst : DivisionSemiring α] [CharZero α] (p : ℚ≥0), ↑p⁻¹ = (↑p)⁻¹
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- Auxiliary definition for `pullFunctor`.  -/
CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {S' : C} →
                {p : S' ⟶ S} →
                  {ι' : Type t'} →
                    {X' : ι' → C} →
                      {f' : (j : ι') → X' j ⟶ S'} →
                        {α : ι' → ι} →
                          {p' : (j : ι') → X' j ⟶ X (α j)} →
                            (∀ (j : ι'),
                                CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) =
                                  CategoryTheory.CategoryStruct.comp (f' j) p) →
                              (D : F.DescentData f) →
                                ⦃Y : C⦄ →
                                  (q : Y ⟶ S') →
                                    ⦃j₁ j₂ : ι'⦄ →
                                      (f₁ : Y ⟶ X' j₁) →
                                        (f₂ : Y ⟶ X' j₂) →
                                          autoParam (CategoryTheory.CategoryStruct.comp f₁ (f' j₁) = q)
                                              CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom._auto_1 →
                                            autoParam (CategoryTheory.CategoryStruct.comp f₂ (f' j₂) = q)
                                                CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom._auto_3 →
                                              ((F.map f₁.op.toLoc).toFunctor.obj
                                                  ((F.map (p' j₁).op.toLoc).toFunctor.obj (D.obj (α j₁))) ⟶
                                                (F.map f₂.op.toLoc).toFunctor.obj
                                                  ((F.map (p' j₂).op.toLoc).toFunctor.obj (D.obj (α j₂))))
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- A zero object is in particular initial.  -/
CategoryTheory.Limits.HasZeroObject.hasInitial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Limits.HasInitial C
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
HomologicalComplex.XIsoOfEq.eq_1 : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p q : ι}
  (h : p = q), K.XIsoOfEq h = CategoryTheory.eqToIso ⋯
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isSyntheticTacticCompletion.getTacticsNode? : Lean.Syntax → Option Lean.Syntax
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
_private.Mathlib.Analysis.InnerProductSpace.ExteriorPower.0.exteriorPower.innerProductForm_symm : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (x y : ↥(⋀[ℝ]^n E)),
  (exteriorPower.innerProductForm✝ y) x = (exteriorPower.innerProductForm✝ x) y
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.IterM.toList_toIter : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.IterM Id β},
  it.toIter.toList = it.toList.run
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
/-- A monoidal structural isomorphism between two objects.  -/
CategoryTheory.MonoidalCoherence.iso : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} → {X Y : C} → [self : CategoryTheory.MonoidalCoherence X Y] → X ≅ Y
-- Mathlib.CategoryTheory.Galois.Topology
/-- The image of `Aut F` in `∀ X, Aut (F.obj X)` are precisely the compatible families of
automorphisms.  -/
CategoryTheory.PreGaloisCategory.autEmbedding_range : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat),
  Set.range ⇑(CategoryTheory.PreGaloisCategory.autEmbedding F) =
    ⋂ f,
      {a |
        CategoryTheory.CategoryStruct.comp (F.map f.hom) (a f.right).hom =
          CategoryTheory.CategoryStruct.comp (a f.left).hom (F.map f.hom)}
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.le_pointwise_smul_iff : ∀ {G : Type u_2} {A : Type u_4} [inst : Group G] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G A]
  {S T : AddSubgroup A} {a : G}, S ≤ a • T ↔ a⁻¹ • S ≤ T
-- Mathlib.Order.DirSupClosed
dirSupInaccOn_univ : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], DirSupInaccOn Set.univ s ↔ DirSupInacc s
-- Mathlib.Data.Prod.Basic
/-- When true, then `Prod.fst x` and `Prod.snd x` pretty print as `x.1` and `x.2`
rather than as `x.fst` and `x.snd`.
 -/
Prod.PrettyPrinting.pp.numericProj.prod : Lean.Option Bool
-- Mathlib.Order.Filter.SmallSets
Filter.Tendsto.smallSets_mono : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {s t : α → Set β},
  Filter.Tendsto t la lb.smallSets → (∀ᶠ (x : α) in la, s x ⊆ t x) → Filter.Tendsto s la lb.smallSets
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.brecOn.eq : ∀ {motive_1 : Aesop.Frontend.RuleExpr → Sort u} {motive_2 : Array Aesop.Frontend.RuleExpr → Sort u}
  {motive_3 : List Aesop.Frontend.RuleExpr → Sort u} (t : Aesop.Frontend.RuleExpr)
  (F_1 : (t : Aesop.Frontend.RuleExpr) → t.below → motive_1 t)
  (F_2 : (t : Array Aesop.Frontend.RuleExpr) → Aesop.Frontend.RuleExpr.below_1 t → motive_2 t)
  (F_3 : (t : List Aesop.Frontend.RuleExpr) → Aesop.Frontend.RuleExpr.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Aesop.Frontend.RuleExpr.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffAt_one_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, ContDiffAt 𝕜 1 f x ↔ ∃ f', ∃ u ∈ nhds x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterStep.successor.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : Std.IterStep α β → Sort u_3)
  (h_1 : (it : α) → (out : β) → motive (Std.IterStep.yield it out)) (h_2 : (it : α) → motive (Std.IterStep.skip it))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it out => h_1 it out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.inv_right : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (a : N ⋊[φ] G),
  a⁻¹.right = a.right⁻¹
-- Mathlib.Topology.Algebra.Group.Basic
topologicalGroup_sInf : ∀ {G : Type w} [inst : Group G] {ts : Set (TopologicalSpace G)}, (∀ t ∈ ts, IsTopologicalGroup G) → IsTopologicalGroup G
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.sub_mem_Ioo_iff_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a - b ∈ Set.Ioo c d ↔ a ∈ Set.Ioo (c + b) (d + b)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldl_reverse : ∀ {α : Type u_1} {β : Type u_2} {t : RBTree.RBNode α} {f : β → α → β} {init : β},
  RBTree.RBNode.foldl f init t.reverse = RBTree.RBNode.foldr (flip f) t init
-- ProofWidgets.Component.MakeEditLink
ProofWidgets.MakeEditLinkProps.mk.sizeOf_spec : ∀ (edit : Lean.Lsp.TextDocumentEdit) (newSelection? : Option Lean.Lsp.Range) (title? : Option String),
  sizeOf { edit := edit, newSelection? := newSelection?, title? := title? } =
    1 + sizeOf edit + sizeOf newSelection? + sizeOf title?
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.mem_inf_iff : ∀ {α : Type u_1} [inst : LE α] {s t : LowerSet α} {a : α}, a ∈ s ⊓ t ↔ a ∈ s ∧ a ∈ t
-- Mathlib.Data.Set.Sigma
Set.range_sigmaMk : ∀ {ι : Type u_1} {α : ι → Type u_3} (i : ι), Set.range (Sigma.mk i) = Sigma.fst ⁻¹' {i}
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairOfIsCoreflexivePairOfPreservesLimitOfIsCoreflexivePair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {A B : C} (f g : A ⟶ B) [CategoryTheory.IsCoreflexivePair f g]
  [CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair F],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) F
-- Mathlib.Data.Sign.Defs
SignType.cast.eq_1 : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Neg α], ↑SignType.zero = 0
-- Mathlib.Util.LongNames
/-- Lists all instances with a long name beginning with `inst`,
gathered according to the module they are defined in.
This is useful for finding automatically named instances with absurd names.

Use as `#long_names` or `#long_names 100` to specify the length.
 -/
«command#long_instances_» : Lean.ParserDescr
-- Mathlib.RingTheory.Polynomial.Basic
/-- **Alias** of `Polynomial.not_isField`.

---

`R[X]` is never a field for any ring `R`.  -/
Ideal.polynomial_not_isField : ∀ (R : Type u) [inst : Ring R], ¬IsField (Polynomial R)
-- Mathlib.Algebra.Group.Pi.Lemmas
MonoidHom.mulSingle_apply : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → MulOneClass (f i)] (i : I) (x : f i),
  (MonoidHom.mulSingle f i) x = Pi.mulSingle i x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.TheoremGuard.e : Lean.Meta.Grind.TheoremGuard → Lean.Expr
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
/-- This is the functor sending a sheaf `X : Sheaf J A` to the sheafification
of `X.val ⋙ F`.  -/
CategoryTheory.Sheaf.composeAndSheafify : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {A : Type u_1} →
        {B : Type u_2} →
          [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} B] →
              CategoryTheory.Functor A B →
                [CategoryTheory.HasWeakSheafify J B] →
                  CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf J B)
-- Init.Data.Char.Ordinal
/-- Computes the next `Char`, skipping over surrogate code points \(which are not valid
`Char`s\) as necessary.

This function is specified by its interaction with `Char.ordinal`, see
`Char.succ?_eq`.
 -/
Char.succ? : Char → Option Char
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.alter.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp]
  (t t_1 : Std.ExtDTreeMap α (fun x => β) cmp),
  t = t_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (f f_1 : Option β → Option β),
          f = f_1 → Std.ExtDTreeMap.Const.alter t a f = Std.ExtDTreeMap.Const.alter t_1 a_1 f_1
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instPowNat : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : Monoid γ] → [ContinuousMul γ] → Pow (α →ₘ[μ] γ) ℕ
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.preimage_coe_Ioo_top : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some ⁻¹' Set.Ioo ↑a ⊤ = Set.Ioi a
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.instCoeSortType : CoeSort MagmaCat (Type u)
-- Mathlib.Logic.Equiv.Sum
Equiv.emptySum_apply_inr : ∀ {α : Type u_9} {β : Type u_10} [inst : IsEmpty α] (b : β), (Equiv.emptySum α β) (Sum.inr b) = b
-- Mathlib.Tactic.NormNum.NatFactorial
Mathlib.Meta.NormNum.isNat_descFactorial : ∀ {n x l y : ℕ} (z : ℕ),
  Mathlib.Meta.NormNum.IsNat n x →
    Mathlib.Meta.NormNum.IsNat l y →
      x = z + y → ∀ (a : ℕ), (z + 1).ascFactorial y = a → Mathlib.Meta.NormNum.IsNat (n.descFactorial l) a
-- Mathlib.Algebra.Order.BigOperators.Expect
Fintype.expect_eq_zero_iff_of_nonneg : ∀ {ι : Type u_1} {α : Type u_2} [inst : Fintype ι] [inst_1 : AddCommMonoid α] [inst_2 : PartialOrder α]
  [IsOrderedAddMonoid α] [inst_4 : Module ℚ≥0 α] {f : ι → α}, 0 ≤ f → ((Finset.univ.expect fun i => f i) = 0 ↔ f = 0)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Add to the `todo` stack the match with `key`.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.matchKey : Lean.Meta.RefinedDiscrTree.Key →
  Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex →
    Lean.Meta.RefinedDiscrTree.PartialMatch✝ →
      Array Lean.Meta.RefinedDiscrTree.PartialMatch✝ → Array Lean.Meta.RefinedDiscrTree.PartialMatch✝