mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.self_lt_sinh_iff : ∀ {x : ℝ}, x < Real.sinh x ↔ 0 < x
-- Mathlib.Algebra.Group.Basic
mul_div_assoc' : ∀ {G : Type u_3} [inst : DivInvMonoid G] (a b c : G), a * (b / c) = a * b / c
-- Mathlib.Logic.ExistsUnique
/-- `∃! x ∈ s, p x` means `∃! x, x ∈ s ∧ p x`, which is to say that there exists a unique `x ∈ s`
such that `p x`.
Similarly, notations such as `∃! x ≤ n, p n` are supported,
using any relation defined using the `binder_predicate` command.
 -/
Mathlib.Notation.«term∃!__,_» : Lean.ParserDescr
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_rci_eq_toArray_mkSlice_rco : ∀ {α : Type u_1} {xs : List α} {lo : ℕ},
  Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) =
    Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...xs.length)
-- Std.Data.TreeSet.Basic
/-- Tree sets.

A tree set stores elements of a certain type in a certain order. It depends on a comparator function
that defines an ordering on the keys and provides efficient order-dependent queries, such as
retrieval of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function `cmp` should satisfy
certain laws that ensure a consistent ordering:

* If `a` is less than (or equal) to `b`, then `b` is greater than (or equal) to `a`
and vice versa (see the `OrientedCmp` typeclass).
* If `a` is less than or equal to `b` and `b` is, in turn, less than or equal to `c`, then `a`
is less than or equal to `c` (see the `TransCmp` typeclass).

Keys for which `cmp a b = Ordering.eq` are considered the same, i.e., there can be only one of them
be contained in a single tree set at the same time.

To avoid expensive copies, users should make sure that the tree set is used linearly.

Internally, the tree sets are represented as size-bounded trees, a type of self-balancing binary
search tree with efficient order statistic lookups.

For use in proofs, the type `Std.ExtTreeSet` of extensional tree sets should be preferred. This
type comes with several extensionality lemmas and provides the same functions but requires a
`TransCmp` instance to work with.

These tree sets contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, `Std.TreeSet.Raw` and
`Std.TreeSet.Raw.WF` unbundle the invariant from the tree set. When in doubt, prefer
`TreeSet` over `TreeSet.Raw`.
 -/
Std.TreeSet : (α : Type u) → autoParam (α → α → Ordering) Std.TreeSet._auto_1 → Type u
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The first projection within a domain at a point in a product is `C^∞`.  -/
contDiffWithinAt_fst : ∀ {𝕜 : 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] {n : WithTop ℕ∞}
  {s : Set (E × F)} {p : E × F}, ContDiffWithinAt 𝕜 n Prod.fst s p
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.EvalTacticFailure.mk.sizeOf_spec : ∀ (exception : Lean.Exception) (state : Lean.Elab.Tactic.SavedState),
  sizeOf { exception := exception, state := state } = 1 + sizeOf exception + sizeOf state
-- Mathlib.Data.Fintype.BigOperators
Fintype.sum_congr : ∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : AddCommMonoid M] (f g : α → M),
  (∀ (a : α), f a = g a) → ∑ a, f a = ∑ a, g a
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.map_add : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B) (x y : A), f (x + y) = f x + f y
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.haar_singleton : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [ContinuousMul G] [BorelSpace G] (g : G), μ {g} = μ {1}
-- Mathlib.Tactic.Linter.FindDeprecations
/-- The main structure containing the information a deprecated declaration.
* `module` is the name of the module containing the deprecated declaration;
* `decl` is the name of the deprecated declaration;
* `rgStart` is the `Position` where the deprecated declaration starts;
* `rgStop` is the `Position` where the deprecated declaration ends;
* `since` is the date when the declaration was deprecated.
 -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.DeprecationInfo : Type
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.IsIrreducible.eq_top_of_invtSubmodule_reflection : ∀ {ι : 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}
  [self : P.IsIrreducible] (q : Submodule R M),
  (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.πTruncGE.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C], K.πTruncGE e = e.liftExtend (K.restrictionToTruncGE' e) ⋯
-- Lean.Elab.Tactic.Simp
/-- The elaborated simp arguments with syntax  -/
Lean.Elab.Tactic.MkSimpContextResult.simpArgs : Lean.Elab.Tactic.MkSimpContextResult → Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult)
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_add'_hom_app : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n m mn : M) (hnm : m + n = mn) (a a' a'' : M)
  (ha' : n + a = a') (ha'' : m + a' = a'') (X : C),
  (F.shiftIso mn a a'' ⋯).hom.app X =
    CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).hom.app X))
      (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X))
        ((F.shiftIso m a' a'' ha'').hom.app X))
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.image_mem_toOpenPartialHomeomorph_target : ∀ {𝕜 : 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} {a : E} [inst_5 : CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a),
  f a ∈ (HasStrictFDerivAt.toOpenPartialHomeomorph f hf).target
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} (s : CategoryTheory.Limits.CokernelCofork f) {Z : C} (h : s.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π s) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Init.Data.List.Nat.Range
List.find?_range'_eq_some : ∀ {s n i : ℕ} {p : ℕ → Bool},
  List.find? p (List.range' s n) = some i ↔ p i = true ∧ i ∈ List.range' s n ∧ ∀ (j : ℕ), s ≤ j → j < i → (!p j) = true
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
/-- A slight variant of `hasFDerivAt_of_tendstoLocallyUniformlyOn` with the assumption stated
in terms of `DifferentiableOn` rather than `HasFDerivAt`. This makes a few proofs nicer in
complex analysis where holomorphicity is assumed but the derivative is not known a priori.  -/
hasFDerivAt_of_tendsto_locally_uniformly_on' : ∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3}
  [inst_1 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] {G : Type u_4}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] {f : ι → E → G} {g : E → G} {g' : E → E →L[𝕜] G} {x : E}
  [l.NeBot] {s : Set E},
  IsOpen s →
    TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s →
      (∀ (n : ι), DifferentiableOn 𝕜 (f n) s) →
        (∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) → x ∈ s → HasFDerivAt g (g' x) x
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Transfer `CompleteDistribLattice` across an `Equiv`.  -/
Equiv.completeDistribLattice : {α : Type u} → {β : Type v} → α ≃ β → [CompleteDistribLattice β] → CompleteDistribLattice α
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_le_iff : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α},
  BddAbove s → s.Nonempty → (sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.proj : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup F]
  [inst_2 : TopologicalSpace F] [inst_3 : Module 𝕜 F] {l : Filter α} {g : α → F} {ι : Type u_7} {E : ι → Type u_8}
  [inst_4 : (i : ι) → AddCommGroup (E i)] [inst_5 : (i : ι) → Module 𝕜 (E i)]
  [inst_6 : (i : ι) → TopologicalSpace (E i)] {f : α → (i : ι) → E i},
  f =o[𝕜; l] g → ∀ (i : ι), (fun x => f x i) =o[𝕜; l] g
-- Init.Data.Vector.Lemmas
Vector.prod_singleton : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] [Std.LawfulRightIdentity (fun x1 x2 => x1 * x2) 1] {x : α},
  #v[x].prod = x
-- Mathlib.Analysis.Normed.Ring.Lemmas
Int.instNormOneClass : NormOneClass ℤ
-- Mathlib.RingTheory.Smooth.Kaehler
derivationQuotKerSq_mk : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S] (x : P),
  (derivationQuotKerSq R P S) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) x) =
    1 ⊗ₜ[P] (KaehlerDifferential.D R P) x
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- The natural isomorphism
`F.mapShortComplex ⋙ leftHomologyFunctor D ≅ leftHomologyFunctor C ⋙ F`
for a functor `F : C ⥤ D` which preserves homology.  -/
CategoryTheory.ShortComplex.leftHomologyFunctorIso : {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] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.PreservesZeroMorphisms] →
                [inst_5 : CategoryTheory.Limits.HasKernels C] →
                  [inst_6 : CategoryTheory.Limits.HasCokernels C] →
                    [inst_7 : CategoryTheory.Limits.HasKernels D] →
                      [inst_8 : CategoryTheory.Limits.HasCokernels D] →
                        [F.PreservesHomology] →
                          F.mapShortComplex.comp (CategoryTheory.ShortComplex.leftHomologyFunctor D) ≅
                            (CategoryTheory.ShortComplex.leftHomologyFunctor C).comp F
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.IsExtension.ker_eq_bot : ∀ {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} {inst : CommRing R} {inst_1 : LieRing L}
  {inst_2 : LieAlgebra R L} {inst_3 : LieRing N} {inst_4 : LieAlgebra R N} {inst_5 : LieRing M}
  {inst_6 : LieAlgebra R M} {i : N →ₗ⁅R⁆ L} (p : L →ₗ⁅R⁆ M) [self : LieAlgebra.IsExtension i p], i.ker = ⊥
-- Mathlib.Computability.EpsilonNFA
εNFA.step_zero : ∀ {α : Type u} {σ : Type v} (s : σ) (a : Option α), εNFA.step 0 s a = ∅
-- Init.Data.List.Perm
_private.Init.Data.List.Perm.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- If `v` and `w` are infinite places of `K` and `v = w ^ t` for some `t` then `t = 1`.  -/
NumberField.InfinitePlace.eq_one_of_rpow_eq : ∀ {K : Type u_1} [inst : Field K] {v w : NumberField.InfinitePlace K} {t : ℝ}, (fun x => w x) ^ t = ⇑v → t = 1
-- Mathlib.Data.Sym.Sym2
Function.Embedding.sym2Map_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a : Sym2 α), f.sym2Map a = Sym2.map (⇑f) a
-- Init.Data.Array.DecidableEq
Array.instDecidableEqEmpImpl : {α : Type u_1} → (xs : Array α) → Decidable (xs = #[])
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.minKey_modify_eq_minKey : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {he : (Std.DTreeMap.Const.modify t k f).isEmpty = false},
  (Std.DTreeMap.Const.modify t k f).minKey he = t.minKey ⋯
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- The p-adic valuation of `n` is equal to the logarithm w.r.t. `p` iff
`n` is less than `p` raised to one plus the p-adic valuation of `n`.  -/
nat_log_eq_padicValNat_iff : ∀ {p n : ℕ} [hp : Fact (Nat.Prime p)], n ≠ 0 → (Nat.log p n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addY_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2 →
            W.addY P Q / WeierstrassCurve.Jacobian.addZ P Q ^ 3 =
              W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3)
                (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3))
-- Mathlib.Algebra.Order.Group.Equiv
toLexAddEquiv.eq_1 : ∀ (α : Type u_1) [inst : Add α], toLexAddEquiv α = { toEquiv := toLex, map_add' := ⋯ }
-- Mathlib.Algebra.Colimit.Module
/-- The direct limit of a directed system is the modules glued together along the maps.  -/
Module.DirectLimit : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        (G : ι → Type u_3) →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              ((i j : ι) → i ≤ j → G i →ₗ[R] G j) → [DecidableEq ι] → Type (max u_2 u_3)
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal_update_of_mem : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] (μ : (i : δ) → MeasureTheory.Measure (X i))
  [inst_1 : DecidableEq δ] {s : Finset δ} {i : δ},
  i ∈ s →
    ∀ (f : ((i : δ) → X i) → ENNReal) (x : (i : δ) → X i) (y : X i),
      (∫⋯∫⁻_s, f ∂μ) (Function.update x i y) = (∫⋯∫⁻_s, f ∂μ) x
-- Mathlib.Data.Finset.Max
/-- Induction principle for `Finset`s in a linearly ordered type: a predicate is true on all
`s : Finset α` provided that:

* it is true on the empty `Finset`,
* for every `s : Finset α` and an element `a` strictly less than all elements of `s`, `p s`
  implies `p (insert a s)`.  -/
Finset.induction_on_min : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : DecidableEq α] {motive : Finset α → Prop} (s : Finset α),
  motive ∅ → (∀ (a : α) (s : Finset α), (∀ x ∈ s, a < x) → motive s → motive (insert a s)) → motive s
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.PropagatorMap.insert : Lean.Meta.Grind.PropagatorMap → Lean.Name → Lean.Meta.Grind.Propagator → Lean.Meta.Grind.PropagatorMap
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.resetBody : Lean.IR.FnBody → Lean.IR.FnBody
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.mk_lift : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_1}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra.FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I)
  (g : A →ₐ[R] B ⧸ I) (x : A), (Ideal.Quotient.mk I) ((Algebra.FormallySmooth.lift I hI g) x) = g x
-- Init.Data.Vector.Zip
Vector.zip_map' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β} {g : α → γ} {xs : Vector α n},
  (Vector.map f xs).zip (Vector.map g xs) = Vector.map (fun a => (f a, g a)) xs
-- Lean.Data.Trie
Lean.Data.Trie.node.injEq : ∀ {α : Type} (a : Option α) (a_1 : ByteArray) (a_2 : Array (Lean.Data.Trie α)) (a_3 : Option α) (a_4 : ByteArray)
  (a_5 : Array (Lean.Data.Trie α)),
  (Lean.Data.Trie.node a a_1 a_2 = Lean.Data.Trie.node a_3 a_4 a_5) = (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.Order.Lattice
inf_sup_right : ∀ {α : Type u} [inst : DistribLattice α] (a b c : α), (a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c
-- Mathlib.CategoryTheory.Shift.InducedShiftSequence
CategoryTheory.Functor.ShiftSequence.induced_shiftMap_assoc : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D A} {G : CategoryTheory.Functor C A} (e : L.comp F ≅ G)
  (M : Type u_4) [inst_3 : AddMonoid M] [inst_4 : CategoryTheory.HasShift C M] [inst_5 : G.ShiftSequence M]
  (F' : M → CategoryTheory.Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m)
  [inst_6 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Full]
  [inst_7 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Faithful] [inst_8 : CategoryTheory.HasShift D M]
  [inst_9 : L.CommShift M] {n : M} {X Y : C} (f : X ⟶ (CategoryTheory.shiftFunctor C n).obj Y) (a a' : M)
  (h : n + a = a') {Z : A} (h_1 : (F.shift a').obj (L.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (F.shiftMap (CategoryTheory.CategoryStruct.comp (L.map f) ((CategoryTheory.Functor.commShiftIso L n).hom.app Y)) a
        a' h)
      h_1 =
    CategoryTheory.CategoryStruct.comp ((e' a).hom.app X)
      (CategoryTheory.CategoryStruct.comp (G.shiftMap f a a' h)
        (CategoryTheory.CategoryStruct.comp ((e' a').inv.app Y) h_1))
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered additive monoids M, N, the natural inclusion
ordered homomorphism from N to M × N.  -/
OrderAddMonoidHom.inr : (α : Type u_1) →
  (β : Type u_2) →
    [inst : AddMonoid α] → [inst_1 : PartialOrder α] → [inst_2 : AddMonoid β] → [inst_3 : Preorder β] → β →+o α × β
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Unsigned modulo.
 -/
Std.Tactic.BVDecide.BVBinOp.umod : Std.Tactic.BVDecide.BVBinOp
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_eq_headD_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {fallback : α}, t.minKeyD fallback = t.keys.headD fallback
-- Mathlib.MeasureTheory.Measure.FiniteMeasurePi
MeasureTheory.ProbabilityMeasure.pi_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.ProbabilityMeasure (α i)) (s : (i : ι) → Set (α i)),
  (MeasureTheory.ProbabilityMeasure.pi μ) (Set.univ.pi s) = ∏ i, (μ i) (s i)
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.sq_add_sq_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a b : R},
  IsCoprime a b → a ^ 2 + b ^ 2 ≠ 0
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mk'.eq_1 : ∀ {ι : Type u_1} (l u : ι → ℝ),
  BoxIntegral.Box.mk' l u = if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : LawfulBEq α] {a : α}, ∅.get? a = none
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyRel.trans_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ f₂ : C(X, Y)} {S : Set X}
  (F : f₀.HomotopyRel f₁ S) (G : f₁.HomotopyRel f₂ S) (x : ↑unitInterval × X),
  (F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)
-- Mathlib.Order.Heyting.Basic
ofDual_himp : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a b : αᵒᵈ),
  OrderDual.ofDual (b ⇨ a) = OrderDual.ofDual a \ OrderDual.ofDual b
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- The induced functor from `Fib p S` to the standard fiber.  -/
HasFibers.inducedFunctor : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        (p : CategoryTheory.Functor 𝒳 𝒮) →
          [inst_2 : HasFibers p] → (S : 𝒮) → CategoryTheory.Functor (HasFibers.Fib p S) (p.Fiber S)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
normEDS_one : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), normEDS b c d 1 = 1
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
le_ciSup₂ : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {κ : ι → Sort u_5} {f : (i : ι) → κ i → α},
  BddAbove (⋃ i, Set.range (f i)) → ∀ (i : ι) (j : κ i), f i j ≤ ⨆ i, ⨆ j, f i j
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.snd X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) h
-- Lean.Parser.Command
Lean.Parser.Command.nonrec : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategoryι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [inst_6 : P.IsTriangulated], P.ι.IsTriangulated
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.prodCongr_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7}
  {V₃ : Type u_8} {V₄ : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂]
  [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : TopologicalSpace P₃] [inst_13 : AddCommGroup V₄] [inst_14 : Module k V₄]
  [inst_15 : AddTorsor V₄ P₄] [inst_16 : TopologicalSpace P₄] (e₁ : P₁ ≃ᴬ[k] P₂) (e₂ : P₃ ≃ᴬ[k] P₄) (p : P₁ × P₃),
  (e₁.prodCongr e₂) p = (e₁ p.1, e₂ p.2)
-- Init.Core
dif_pos : ∀ {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : c → α} {e : ¬c → α}, dite c t e = t hc
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- The natural transformation presenting `f`.  -/
CategoryTheory.IndParallelPairPresentation.φ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} → (self : CategoryTheory.IndParallelPairPresentation f g) → self.F₁ ⟶ self.F₂
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.le_of_isLE : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ) [t.IsLE X n], t.le n X
-- Init.Grind.Interactive
/-- `by_contra` applies proof by contradiction, negating the target and making it `False`.
Only available in `sym =>` mode.  -/
Lean.Parser.Tactic.Grind.symByContra : Lean.ParserDescr