mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.NoncommPiCoprod
/-- `Finset.noncommSum` is “injective” in `f` if `f` maps into independent subgroups.
This generalizes (one direction of) `AddSubgroup.disjoint_iff_add_eq_zero`.  -/
AddSubgroup.eq_zero_of_noncommSum_eq_zero_of_iSupIndep : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} (s : Finset ι) (f : ι → G)
  (comm : (↑s).Pairwise (Function.onFun AddCommute f)) (K : ι → AddSubgroup G),
  iSupIndep K → (∀ x ∈ s, f x ∈ K x) → s.noncommSum f comm = 0 → ∀ i ∈ s, f i = 0
-- Mathlib.NumberTheory.Dioph
Dioph.diophPFun_vec : ∀ {n : ℕ} (f : Vector3 ℕ n →. ℕ), Dioph.DiophPFun f ↔ Dioph {v | (v ∘ Fin2.fs, v Fin2.fz) ∈ f.graph}
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instIsSubApply : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞}, IsSubApply (TestFunction Ω F n) E F
-- Init.Data.UInt.Lemmas
UInt32.toFin.ofNat : ∀ {n : ℕ}, (UInt32.ofNat n).toFin = Fin.ofNat UInt32.size n
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestRevMatch_iff_isLongestRevMatchAt_ofSliceTo : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {base : s.Pos}
  (startPos : (s.sliceTo base).Pos),
  String.Slice.Pattern.Model.IsLongestRevMatch pat startPos ↔
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat (String.Slice.Pos.ofSliceTo startPos) base
-- Lean.Compiler.InitAttr
/-- Run the initializer for `decl` and store its value for global access. Should only be used while importing.  -/
Lean.runInit : Lean.Environment → Lean.Options → Lean.Name → Lean.Name → IO Unit
-- Mathlib.RingTheory.ClassGroup.Basic
instInhabitedClassGroup : (R : Type u_1) → [inst : CommRing R] → [inst_1 : IsDomain R] → Inhabited (ClassGroup R)
-- Mathlib.MeasureTheory.Integral.ExpDecay
/-- If `f` is continuous on `[a, ∞)`, and is `O (exp (-b * x))` at `∞` for some `b > 0`, then
`f` is integrable on `(a, ∞)`.  -/
integrable_of_isBigO_exp_neg : ∀ {f : ℝ → ℝ} {a b : ℝ},
  0 < b →
    ContinuousOn f (Set.Ici a) →
      (f =O[Filter.atTop] fun x => Real.exp (-b * x)) → MeasureTheory.IntegrableOn f (Set.Ioi a) MeasureTheory.volume
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem_extract : ∀ {i : ℕ} {b : ByteArray} {start stop : ℕ} (h : i < (b.extract start stop).size),
  (b.extract start stop)[i] = b[start + i]
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e)
  {Z : a ⟶ e}
  (h_1 :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)
        i ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i) h_1)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalHorizontalCompAux'_of_whisker : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f f' g g' h : C}
  {η : g ⟶ h} {θ : f' ⟶ g'}
  {η₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj g f ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj h f}
  {ηθ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj g f) f' ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj h f) g'}
  {ηθ₁ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj g f) f' ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj h (CategoryTheory.MonoidalCategoryStruct.tensorObj f g')}
  {ηθ₂ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj g (CategoryTheory.MonoidalCategoryStruct.tensorObj f f') ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj h (CategoryTheory.MonoidalCategoryStruct.tensorObj f g')},
  CategoryTheory.MonoidalCategoryStruct.whiskerRight η f = η₁ →
    CategoryTheory.MonoidalCategoryStruct.tensorHom η₁
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl f').hom
            (CategoryTheory.CategoryStruct.comp θ (CategoryTheory.Iso.refl g').hom)) =
        ηθ →
      CategoryTheory.CategoryStruct.comp ηθ (CategoryTheory.MonoidalCategoryStruct.associator h f g').hom = ηθ₁ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator g f f').inv ηθ₁ = ηθ₂ →
          CategoryTheory.MonoidalCategoryStruct.tensorHom η (CategoryTheory.MonoidalCategoryStruct.whiskerLeft f θ) =
            ηθ₂
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.HasKernels.has_limit : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  [self : CategoryTheory.Limits.HasKernels C] {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasKernel f
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePullbackShapeOpEquiv_counitIso : ∀ (J : Type w),
  (CategoryTheory.Limits.widePullbackShapeOpEquiv J).counitIso = CategoryTheory.Limits.widePushoutShapeUnopOp J
-- Batteries.Data.List.Lemmas
List.inter_def : ∀ {α : Type u_1} [inst : BEq α] (l₁ l₂ : List α), l₁ ∩ l₂ = List.filter (fun x => List.elem x l₂) l₁
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.symmetry_symmetry_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [inst_2 : F.Full] [F.Faithful] {Z : C} (h : hf'.pullback g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (CategoryTheory.CategoryStruct.comp (hg.symmetry hf') h) = h
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.uniformSpace.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)),
  UniformOnFun.uniformSpace α β 𝔖 =
    ⨅ s ∈ 𝔖,
      UniformSpace.comap (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformFun.uniformSpace (↑s) β)
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log(m+n)). Build a tree from an element between two trees, without any
assumption on the relative sizes.

```
link {1, 2} 4 {5, 6} = {1, 2, 4, 5, 6}
link {1, 3} 2 {5} = precondition violation
```  -/
Ordnode.link : {α : Type u_1} → Ordnode α → α → Ordnode α → Ordnode α
-- Init.Grind.AC
Lean.Grind.AC.diseq_norm_a : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} (lhs rhs : Lean.Grind.AC.Expr)
  (lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_norm_a_cert lhs rhs lhs' rhs' = true →
    Lean.Grind.AC.Expr.denote ctx lhs ≠ Lean.Grind.AC.Expr.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs' ≠ Lean.Grind.AC.Seq.denote ctx rhs'
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- pullback preserves the identity (up to a natural isomorphism)  -/
CategoryTheory.MonoOver.pullbackId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
        CategoryTheory.MonoOver.pullback (CategoryTheory.CategoryStruct.id X) ≅
          CategoryTheory.Functor.id (CategoryTheory.MonoOver X)
-- Lean.Meta.Tactic.Util
Lean.Meta.TacticResultCNM.noChange : Lean.Meta.TacticResultCNM
-- Mathlib.MeasureTheory.Integral.CircleAverage
Real.circleAverage_def : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ},
  Real.circleAverage f c R = (2 * Real.pi)⁻¹ • ∫ (θ : ℝ) in 0..2 * Real.pi, f (circleMap c R θ)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_eq_some_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a fallback : α},
  a ∈ t → t.get? a = some (t.getD a fallback)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.incenter_mem_affineSpan_range : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n),
  s.incenter ∈ affineSpan ℝ (Set.range s.points)
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapRange.linearEquiv_toLinearMap : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ₁₂ : R →+* R₂}
  {σ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] N),
  ↑(Finsupp.mapRange.linearEquiv f) = Finsupp.mapRange.linearMap ↑f
-- Init.Data.UInt.Lemmas
UInt32.toUSize_ofNatClamp_of_le : ∀ {n : ℕ}, UInt32.size ≤ n → (UInt32.ofNatClamp n).toUSize = USize.ofNatLT (UInt32.size - 1) ⋯
-- Mathlib.RingTheory.Ideal.Defs
/-- A (left) ideal in a semiring `R` is an additive submonoid `s` such that
`a * b ∈ s` whenever `b ∈ s`. If `R` is a ring, then `s` is an additive subgroup.  -/
Ideal : (R : Type u) → [Semiring R] → Type u
-- Mathlib.RingTheory.OreLocalization.Cardinality
OreLocalization.cardinalMk : ∀ {R : Type u} [inst : Ring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S],
  S ≤ nonZeroDivisorsLeft R → Cardinal.mk (OreLocalization S R) = Cardinal.mk R
-- Mathlib.Algebra.CharP.Frobenius
/-- The iterated Frobenius endomorphism commutes with any ring homomorphism.  -/
RingHom.iterateFrobenius_comm : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (g : R →+* S) (p : ℕ)
  [inst_2 : ExpChar R p] [inst_3 : ExpChar S p] (n : ℕ),
  g.comp (iterateFrobenius R p n) = (iterateFrobenius S p n).comp g
-- Mathlib.Algebra.Module.Lattice
Submodule.IsLattice.fg : ∀ {R : Type u_1} {inst : CommRing R} {A : outParam (Type u_2)} {inst_1 : CommRing A} {inst_2 : Algebra R A}
  {V : Type u_3} {inst_3 : AddCommMonoid V} {inst_4 : Module R V} {inst_5 : Module A V}
  {inst_6 inst_7 : IsScalarTower R A V} {M : Submodule R V} [self : Submodule.IsLattice A M], M.FG
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.sum_C_index : ∀ {R : Type u} [inst : Semiring R] {a : R} {β : Type u_1} [inst_1 : AddCommMonoid β] {f : ℕ → R → β},
  f 0 0 = 0 → (Polynomial.C a).sum f = f 0 a
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeSubtypeEquivSubtypeExists_symm_apply_coe_coe : ∀ {α : Sort u_1} (p : α → Prop) (q : Subtype p → Prop) (a : { a // ∃ (h : p a), q ⟨a, h⟩ }),
  ↑↑((Equiv.subtypeSubtypeEquivSubtypeExists p q).symm a) = ↑a
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_erase_eq_iff_not_compare_eq_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).max? = t.max? ↔ ∀ {km : α}, t.max? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.Algebra.Lie.Weights.Cartan
/-- Given a nilpotent Lie subalgebra `H ⊆ L` together with `χ₁ χ₂ : H → R`, there is a natural
`R`-bilinear product of root vectors, compatible with the actions of `H`.  -/
LieAlgebra.rootSpaceProduct : (R : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (H : LieSubalgebra R L) →
            [inst_3 : LieRing.IsNilpotent ↥H] →
              (χ₁ χ₂ χ₃ : ↥H → R) →
                χ₁ + χ₂ = χ₃ →
                  TensorProduct R ↥(LieAlgebra.rootSpace H χ₁) ↥(LieAlgebra.rootSpace H χ₂) →ₗ⁅R,↥H⁆
                    ↥(LieAlgebra.rootSpace H χ₃)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
isGLB_inv' : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G},
  IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a
-- Mathlib.Control.Bifunctor
Prod.lawfulBifunctor : LawfulBifunctor Prod
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.toSubgroup_injective : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G], Function.Injective fun H => ↑H.toOpenSubgroup
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π_assoc : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)]
  {j : J} {k : K} {Z : C} (h : ((CategoryTheory.Functor.curry.obj G).obj j).obj k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) j)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).obj j) k) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G (j, k)) h
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.propSet_singleton`. -/
CategoryTheory.CardinalFilteredPoset.propSet_singleton : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J : CategoryTheory.CardinalDirectedPoset κ} (j : ↑J.obj), J.PropSet {j}
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly : Type
-- Mathlib.Algebra.Algebra.Unitization
Unitization.algHom_ext'' : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] {C : Type u_5} [inst_5 : Semiring C]
  [inst_6 : Algebra R C] {F : Type u_6} [inst_7 : FunLike F (Unitization R A) C] [AlgHomClass F R (Unitization R A) C]
  {φ ψ : F}, (∀ (a : A), φ ↑a = ψ ↑a) → φ = ψ
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.ext : ∀ {X Y : Semigrp} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.Integrable.comp_add_right : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : AddGroup G] [MeasurableAdd G] {f : G → F} [μ.IsAddRightInvariant],
  MeasureTheory.Integrable f μ → ∀ (g : G), MeasureTheory.Integrable (fun t => f (t + g)) μ
-- Mathlib.Topology.Algebra.Monoid
AddSubsemigroup.topologicalClosure.eq_1 : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddSemigroup M] [inst_2 : SeparatelyContinuousAdd M]
  (s : AddSubsemigroup M), s.topologicalClosure = { carrier := closure ↑s, add_mem' := ⋯ }
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.continuousMapEquiv_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  [inst_3 : CompactSpace α] (f : C(α, β)) (a : α), (CompactlySupportedContinuousMap.continuousMapEquiv f) a = f a
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.ins.match_3.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (Unit → motive RBTree.RBNode.nil) →
        ((a : RBTree.RBNode α) →
            (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a y b)) →
          ((a : RBTree.RBNode α) →
              (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b)) →
            motive x
-- Mathlib.CategoryTheory.Shift.SingleFunctorsLift
_private.Mathlib.CategoryTheory.Shift.SingleFunctorsLift.0.CategoryTheory.SingleFunctors.lift.map_shiftIso_hom_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{u_7, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_6, u_2} D] [inst_2 : CategoryTheory.Category.{u_5, u_3} E] {A : Type u_4}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  {F : CategoryTheory.SingleFunctors C E A} {G : CategoryTheory.Functor D E} [inst_6 : G.CommShift A] [inst_7 : G.Full]
  [inst_8 : G.Faithful] {Φ : A → CategoryTheory.Functor C D} (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (n a a' : A)
  (h : n + a = a') (X : C),
  G.map ((CategoryTheory.SingleFunctors.lift.shiftIso hΦ n a a' h).hom.app X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso G n).hom.app ((Φ a').obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor E n).map ((hΦ a').hom.app X))
        (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' h).hom.app X) ((hΦ a).inv.app X)))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.fold_eq_foldl_toArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w}
  {f : δ → (a : α) → β a → δ} {init : δ},
  Std.DHashMap.fold f init m = Array.foldl (fun a b => f a b.fst b.snd) init m.toArray
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.total_le : ∀ {α : Type u_1} [inst : LinearOrder α], Std.Total fun x1 x2 => x1 ≤ x2
-- Init.Data.Array.Basic
/-- Returns `true` if `p` returns `true` for every element of `as`.

Short-circuits upon encountering the first `false`.

The optional parameters `start` and `stop` control the region of the array to be checked. Only the
elements with indices from `start` (inclusive) to `stop` (exclusive) are checked. By default, the
entire array is checked.

Examples:
* `#[a, b, c].all p = (p a && (p b && p c))`
* `#[2, 4, 6].all (· % 2 = 0) = true`
* `#[2, 4, 5, 6].all (· % 2 = 0) = false`
 -/
Array.all : {α : Type u} → (as : Array α) → (α → Bool) → optParam ℕ 0 → optParam ℕ as.size → Bool
-- Lean.Data.Lsp.TextSync
Lean.Lsp.SaveOptions.mk.sizeOf_spec : ∀ (includeText : Bool), sizeOf { includeText := includeText } = 1 + sizeOf includeText
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get!_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∈ t₂ → (t₁ ∩ t₂).get! k = t₁.get! k
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.wordProd_append : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω ω' : List B),
  cs.wordProd (ω ++ ω') = cs.wordProd ω * cs.wordProd ω'
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.obj.ι_def_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] {G : C} [inst_5 : CategoryTheory.GrpObj G] {Z : D}
  (h : F.obj G ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv h =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.GrpObj.inv) h
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.IsComm.mk : ∀ {R : Type u_1} [inst : CommRing R] {F : FormalGroup R},
  F.toPowerSeries = MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 0] F.toPowerSeries → F.IsComm
-- Mathlib.RingTheory.Coalgebra.GroupLike
GroupLike.val_injective : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A], Function.Injective GroupLike.val
-- Mathlib.Data.FunLike.Group
FunLike.coeMulHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : Mul β]
  [inst_3 : IsMulApply F α β] (f : F), (FunLike.coeMulHom F α β) f = ⇑f
-- Mathlib.Order.Fin.Basic
/-- `Fin.addNat` as an `OrderEmbedding`.

`addNatOrderEmb m i` adds `m` to `i`, generalizes `Fin.succ`.  -/
Fin.addNatOrderEmb : {n : ℕ} → (m : ℕ) → Fin n ↪o Fin (n + m)
-- Mathlib.Combinatorics.Enumerative.Composition
_private.Mathlib.Combinatorics.Enumerative.Composition.0.Composition.recOnSingleAppend.match_1.eq_3 : ∀ (motive : (blocks : List ℕ) → (∀ {i : ℕ}, i ∈ blocks → 0 < i) → Sort u_1) (k : ℕ) (l : List ℕ)
  (blocks_pos : ∀ {i : ℕ}, i ∈ (k + 1) :: l → 0 < i)
  (h_1 : (blocks_pos : ∀ {i : ℕ}, i ∈ [] → 0 < i) → motive [] blocks_pos)
  (h_2 : (tail : List ℕ) → (blocks_pos : ∀ {i : ℕ}, i ∈ 0 :: tail → 0 < i) → motive (0 :: tail) blocks_pos)
  (h_3 : (k : ℕ) → (l : List ℕ) → (blocks_pos : ∀ {i : ℕ}, i ∈ (k + 1) :: l → 0 < i) → motive (k.succ :: l) blocks_pos),
  (match k.succ :: l, blocks_pos with
    | [], blocks_pos => h_1 blocks_pos
    | 0 :: tail, blocks_pos => h_2 tail blocks_pos
    | k.succ :: l, blocks_pos => h_3 k l blocks_pos) =
    h_3 k l blocks_pos
-- Lean.ProjFns
Lean.AuxParentProjectionInfo.mk.injEq : ∀ (numParams : ℕ) (fromClass : Bool) (numParams_1 : ℕ) (fromClass_1 : Bool),
  ({ numParams := numParams, fromClass := fromClass } = { numParams := numParams_1, fromClass := fromClass_1 }) =
    (numParams = numParams_1 ∧ fromClass = fromClass_1)
-- Lean.Elab.PatternVar
/-- State for the pattern variable collector monad.  -/
Lean.Elab.Term.CollectPatternVars.State : Type
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleResult.empty : LeanSearchClient.LoogleResult
-- Aesop.Forward.State
/-- Get the slot with the given index. Panic if the index is invalid.  -/
Aesop.ClusterState.slot! : Aesop.ClusterState → Aesop.SlotIndex → Aesop.Slot
-- Mathlib.RingTheory.Congruence.Basic
RingCon.comap.congr_simp : ∀ {R : Type u_2} {R' : Type u_3} {F : Type u_4} [inst : Add R] [inst_1 : Add R'] [inst_2 : FunLike F R R']
  [inst_3 : AddHomClass F R R'] [inst_4 : Mul R] [inst_5 : Mul R'] [inst_6 : MulHomClass F R R'] (J J_1 : RingCon R'),
  J = J_1 → ∀ (f f_1 : F), f = f_1 → J.comap f = J_1.comap f_1
-- Mathlib.Algebra.Category.CommHopfAlgCat
commHopfAlgCatEquivCogrpCommAlgCat_unitIso_inv_app : ∀ (R : Type u) [inst : CommRing R] (X : CommHopfAlgCat R),
  (commHopfAlgCatEquivCogrpCommAlgCat R).unitIso.inv.app X =
    CategoryTheory.CategoryStruct.id
      { X := ↑X, commRing := CommAlgCat.instCommRingObjForgetAlgHomCarrier,
        hopfAlgebra :=
          instHopfAlgebraCarrierUnopCommAlgCatOfGrpObjOpposite
            (Opposite.unop (Opposite.op { X := Opposite.op (CommAlgCat.of R ↑X), grp := CommAlgCat.grpObjOpOf })).X }
-- Mathlib.Analysis.Convex.Topology
Convex.nhdsWithin_inter_Iio_eq_nhdsLT : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜},
  Convex 𝕜 s →
    ∀ {a : 𝕜}, a ∈ closure s → (s ∩ Set.Iio a).Nonempty → nhdsWithin a (s ∩ Set.Iio a) = nhdsWithin a (Set.Iio a)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_iff_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {k : α}, t.contains k = true ↔ k ∈ t
-- Mathlib.Combinatorics.Matroid.Map
Matroid.restrictSubtype_indep_iff : ∀ {α : Type u_1} {X : Set α} {M : Matroid α} {I : Set ↑X}, (M.restrictSubtype X).Indep I ↔ M.Indep (Subtype.val '' I)
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.instConcreteCategoryMulHomCarrier.eq_1 : Semigrp.instConcreteCategoryMulHomCarrier =
  { hom := fun {X Y} => Semigrp.Hom.hom', ofHom := fun {X Y} => Semigrp.Hom.mk✝,
    hom_ofHom := @Semigrp.instConcreteCategoryMulHomCarrier._proof_1,
    ofHom_hom := @Semigrp.instConcreteCategoryMulHomCarrier._proof_2,
    id_apply := @Semigrp.instConcreteCategoryMulHomCarrier._proof_3,
    comp_apply := @Semigrp.instConcreteCategoryMulHomCarrier._proof_4 }