mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} [inst_3 : SizeOf C] (f : X.src ⟶ Y.src)
  (F : X.src ⨯ Y.tgt ⟶ X.tgt)
  (le :
    (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst F)).obj X.rel ≤
      (CategoryTheory.Subobject.pullback
            (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id Y.tgt))).obj
        Y.rel),
  sizeOf { f := f, F := F, le := le } = 1 + sizeOf f + sizeOf F + sizeOf le
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.ofGradedObject_d_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂)
  (X : CategoryTheory.GradedObject (I₁ × I₂) C) (d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂))
  (d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂'))
  (shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0)
  (shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0)
  (d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₁ i₁' i₁'' i₂) = 0)
  (d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₂ i₁ i₂' i₂'') = 0)
  (comm :
    ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂),
      CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₂ i₁' i₂ i₂') =
        CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₁ i₁ i₁' i₂'))
  (i₁ i₁' : I₁) (i₂ : I₂),
  ((HomologicalComplex₂.ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).d i₁ i₁').f i₂ =
    d₁ i₁ i₁' i₂
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.mk.inj : ∀ {G : Type u} {inst : TopologicalSpace G} {H : Type v} {inst_1 : TopologicalSpace H} {inst_2 : Add G} {inst_3 : Add H}
  {toAddEquiv : G ≃+ H}
  {continuous_toFun : autoParam (Continuous toAddEquiv.toFun) Homeomorph.continuous_toFun._autoParam}
  {continuous_invFun : autoParam (Continuous toAddEquiv.invFun) Homeomorph.continuous_invFun._autoParam}
  {toAddEquiv_1 : G ≃+ H}
  {continuous_toFun_1 : autoParam (Continuous toAddEquiv_1.toFun) Homeomorph.continuous_toFun._autoParam}
  {continuous_invFun_1 : autoParam (Continuous toAddEquiv_1.invFun) Homeomorph.continuous_invFun._autoParam},
  { toAddEquiv := toAddEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toAddEquiv := toAddEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 } →
    toAddEquiv = toAddEquiv_1
-- Mathlib.Data.Int.Fib.Basic
Int.fib_two_mul : ∀ (n : ℤ), Int.fib (2 * n) = Int.fib n * (2 * Int.fib (n + 1) - Int.fib n)
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instEssSurjArrowPlusMapArrowQh : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Plus.Qh.mapArrow.EssSurj
-- Mathlib.RingTheory.Flat.Basic
/-- If `M₁` and `N₂` are flat `R`-modules, `i₁ : M₁ →ₗ[R] N₁` and `i₂ : M₂ →ₗ[R] N₂` are injective
linear maps, then the linear map `i : M ≅ M₁ ⊗[R] M₂ →ₗ[R] N₁ ⊗[R] N₂ ≅ N` induced by `i₁`
and `i₂` is injective.
See `IsTensorProduct.map_injective_of_flat` for different flatness conditions.  -/
IsTensorProduct.map_injective_of_flat_left_right : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {M₁ : Type u_5} {M₂ : Type u_6} {N₁ : Type u_7}
  {N₂ : Type u_8} [inst_5 : AddCommMonoid M₁] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₁] [inst_8 : Module R M₂]
  [inst_9 : AddCommMonoid N₁] [inst_10 : AddCommMonoid N₂] [inst_11 : Module R N₁] [inst_12 : Module R N₂]
  {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g)
  (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂),
  Function.Injective ⇑i₁ →
    Function.Injective ⇑i₂ → ∀ [Module.Flat R M₁] [Module.Flat R N₂], Function.Injective ⇑(hf.map hg i₁ i₂)
-- Init.Data.List.MinMaxOn
List.maxOn_mem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {xs : List α} {f : α → β} {h : xs ≠ []},
  List.maxOn f xs h ∈ xs
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- A natural isomorphism gives a natural isomorphism between the pushforward functors.  -/
SheafOfModules.pushforwardNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F G : CategoryTheory.Functor C D} →
              {T : CategoryTheory.Sheaf J RingCat} →
                {S : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    [inst_3 : G.IsContinuous J K] →
                      (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S) →
                        (α : F ≅ G) →
                          SheafOfModules.pushforward φ ≅
                            SheafOfModules.pushforward
                              (CategoryTheory.CategoryStruct.comp φ
                                ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S))
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mem_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} {x : M},
  x ∈ AddSubmonoid.comap f S ↔ f x ∈ S
-- Init.Data.SInt.Bitwise
Int8.shiftRight_and : ∀ {a b c : Int8}, (a &&& b) >>> c = a >>> c &&& b >>> c
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.instAdditiveTypeSigmaConst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasCoproducts C], CategoryTheory.Limits.sigmaConst.Additive
-- Mathlib.Tactic.Algebra.Basic
Mathlib.Tactic.Algebra.BaseType.mk.inj : ∀ {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)}
  {sAlg : Q(Algebra «$R» «$A»)} {r : Q(«$R»)} {x x_1 : Mathlib.Tactic.Ring.ExSum q(«$sR») r},
  Mathlib.Tactic.Algebra.BaseType.mk r x = Mathlib.Tactic.Algebra.BaseType.mk r x_1 → x = x_1
-- Mathlib.Analysis.Normed.Group.InfiniteSum
/-- If a function `f` is summable in norm, and along some sequence of finsets exhausting the space
its sum is converging to a limit `a`, then this holds along all finsets, i.e., `f` is summable
with sum `a`.  -/
hasSum_of_subseq_of_summable : ∀ {ι : Type u_1} {α : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E},
  (Summable fun a => ‖f a‖) →
    ∀ {s : α → Finset ι} {p : Filter α} [p.NeBot],
      Filter.Tendsto s p Filter.atTop → ∀ {a : E}, Filter.Tendsto (fun b => ∑ i ∈ s b, f i) p (nhds a) → HasSum f a
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.mem_box_iff_index : ∀ {ι : Type u_1} {n : ℕ} [inst : NeZero n] {x : ι → ℝ} {ν : ι → ℤ},
  x ∈ BoxIntegral.unitPartition.box n ν ↔ BoxIntegral.unitPartition.index n x = ν
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- `PreservesColimitsOfSize_shrink.{w w'} F` tries to obtain `PreservesColimitsOfSize.{w w'} F`
from some other `PreservesColimitsOfSize F`.
 -/
CategoryTheory.Limits.preservesColimitsOfSize_shrink : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.GroupTheory.Subgroup.Simple
IsSimpleAddGroup.toNontrivial : ∀ {A : Type u_2} {inst : AddGroup A} [self : IsSimpleAddGroup A], Nontrivial A
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_eq_some_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.max? = some (t.maxD fallback)
-- Batteries.Tactic.PermuteGoals
/-- `pick_goal n` will move the `n`-th goal to the front.

`pick_goal -n` will move the `n`-th goal (counting from the bottom) to the front.

See also `Tactic.rotate_goals`, which moves goals from the front to the back and vice-versa.
 -/
Batteries.Tactic.«tacticPick_goal-_» : Lean.ParserDescr
-- Batteries.Lean.EStateM
EStateM.run'_modify : ∀ {σ ε : Type u_1} (f : σ → σ) (s : σ), (modify f).run' s = some PUnit.unit
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.IsNontrivial.condition : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : ValuativeRel R} [self : ValuativeRel.IsNontrivial R], ∃ γ, γ ≠ 0 ∧ γ ≠ 1
-- Mathlib.Data.List.Dedup
List.dedup.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α], List.dedup = List.pwFilter fun x1 x2 => x1 ≠ x2
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 2nd object in the complex of inhomogeneous chains of `A : Rep k G` is isomorphic
to `G² →₀ A` as a `k`-module.  -/
groupHomology.chainsIso₂ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → (groupHomology.inhomogeneousChains A).X 2 ≅ ModuleCat.of k (G × G →₀ ↑A)
-- Mathlib.SetTheory.Ordinal.Univ
Ordinal.univ_umax : Ordinal.univ.{u, max (u + 1) v} = Ordinal.univ.{u, v}
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.hom_ext_iff : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] {P : Type u_4} [inst_3 : AddCommMonoid P]
  {g₁ g₂ : AddCommGroup.DirectLimit G f →+ P},
  g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (AddCommGroup.DirectLimit.of G f i) = g₂.comp (AddCommGroup.DirectLimit.of G f i)
-- Mathlib.Probability.Process.Stopping
/-- The associated σ-algebra with a stopping time.  -/
MeasureTheory.IsStoppingTime.measurableSpace : {Ω : Type u_1} →
  {ι : Type u_3} →
    {m : MeasurableSpace Ω} →
      [inst : Preorder ι] →
        {f : MeasureTheory.Filtration ι m} → {τ : Ω → WithTop ι} → MeasureTheory.IsStoppingTime f τ → MeasurableSpace Ω
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- Given an orthogonal basis with respect to a bilinear map, the bilinear map is nondegenerate
if the basis has no elements which are self-orthogonal.  -/
LinearMap.IsOrthoᵢ.nondegenerate_of_not_isOrtho_basis_self : ∀ {n : Type u_19} {R : Type u_20} {M : Type u_21} {M₁ : Type u_22} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R M] [inst_4 : Module R M₁] [IsDomain R] [Module.IsTorsionFree R M₁]
  {B : M →ₗ[R] M →ₗ[R] M₁} (v : Module.Basis n R M), B.IsOrthoᵢ ⇑v → (∀ (i : n), (B (v i)) (v i) ≠ 0) → B.Nondegenerate
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndependent.group_smul_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {G : Type u_6} [hG : Group G] [inst_3 : MulAction G R] [inst_4 : MulAction G M] [IsScalarTower G R M]
  [SMulCommClass G R M] (v : ι → M) (w : ι → G), LinearIndependent R (w • v) ↔ LinearIndependent R v
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_gcd_mul_iff_dvd_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {m n k : α}, k ∣ gcd k m * n ↔ k ∣ m * n
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_smul : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  {𝕜 : Type u_5} [inst_2 : SMul 𝕜 γ] [inst_3 : ContinuousConstSMul 𝕜 γ] (c : 𝕜) (f : α →ₘ[μ] γ), ↑(c • f) =ᵐ[μ] c • ↑f
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.AndKind.eq : Mathlib.Tactic.ITauto.AndKind
-- Aesop.Search.Main
Aesop.checkGoalLimit : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q (Option Lean.MessageData)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
/-- `ℝ`-linear map from `ℂ` to itself, which we shall show is the real derivative of the
`GL(2, ℝ)`-action on `ℍ`.  -/
UpperHalfPlane.smulFDeriv : GL (Fin 2) ℝ → ℂ → ℂ →L[ℝ] ℂ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.eq_d₃₂_comp_inv_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin 2 → G) →₀ ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₃ A).inv
      (CategoryTheory.CategoryStruct.comp
        (ChainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) →₀ ↑A))
          (fun n => groupHomology.inhomogeneousChains.d A n) 3 2)
        h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.d₃₂ A)
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₂ A).inv h)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Orientation.oangle.eq_1 : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), o.oangle x y = ↑((o.kahler x) y).arg
-- Mathlib.SetTheory.Cardinal.Free
nonempty_commRing_iff : ∀ (α : Type u), Nonempty (CommRing α) ↔ Nonempty α
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.instSingleton : {α : Type u_1} → Singleton α (Ordnode α)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F' : Type u_21} [inst_6 : NormedDivisionRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'}, MDiff p → MDiff q → (∀ (z : M), q z ≠ 0) → MDiff (p / q)
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.ref : Lean.Elab.PreDefinition → Lean.Syntax
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.isPath_iff_isChain : ∀ {V : Type u_1} {G : SimpleGraph V},
  G.IsAcyclic → ∀ {v w : V} (p : G.Walk v w), p.IsPath ↔ List.IsChain (fun x1 x2 => x1 ≠ x2) p.edges
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netMaxcard_zero : ∀ {X : Type u_1} {F : Set X} (T : X → X), F.Nonempty → ∀ (U : SetRel X X), Dynamics.netMaxcard T F U 0 = 1
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smulCommClass_set'' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α γ] [inst_1 : SMul β γ] [SMulCommClass α β γ],
  SMulCommClass (Set α) β (Set γ)
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
MeasureTheory.innerRegularWRT_isCompact_isClosed : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure P], P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) IsClosed
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.card_pos_of_affineSpan_eq_top : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_5} [inst_3 : Fintype ι] {p : ι → P},
  affineSpan k (Set.range p) = ⊤ → 0 < Fintype.card ι
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C) (T : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.OplaxMonoidal.δ F X Y))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.LaxMonoidal.μ F X Y)) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj T (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)))
-- Mathlib.Topology.Category.LightProfinite.Basic
LightDiagram.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} LightDiagram
-- Mathlib.RingTheory.TensorProduct.Pi
Algebra.TensorProduct.piRightHom_mul : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] {ι : Type u_4}
  {B : ι → Type u_5} [inst_7 : (i : ι) → Semiring (B i)] [inst_8 : (i : ι) → Algebra R (B i)]
  (x y : TensorProduct R A ((i : ι) → B i)),
  (TensorProduct.piRightHom R S A B) (x * y) =
    (TensorProduct.piRightHom R S A B) x * (TensorProduct.piRightHom R S A B) y
-- Mathlib.RingTheory.Regular.RegularSequence
IsLocalRing.isRegular_of_perm : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsLocalRing R]
  [IsNoetherian R M] {rs rs' : List R},
  RingTheory.Sequence.IsRegular M rs → rs.Perm rs' → RingTheory.Sequence.IsRegular M rs'
-- Mathlib.Topology.ContinuousMap.Basic
/-- A family `F s` of continuous maps `C(s, β)`, where (1) the domains `s` are taken from a set `A`
of sets in `α` which contain a neighbourhood of each point in `α` and (2) the functions `F s` agree
pairwise on intersections, can be glued to construct a continuous map in `C(α, β)`.  -/
ContinuousMap.liftCover' : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        (A : Set (Set α)) →
          (F : (s : Set α) → s ∈ A → C(↑s, β)) →
            (∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
                (F s hs) ⟨x, hxi⟩ = (F t ht) ⟨x, hxj⟩) →
              (∀ (x : α), ∃ i ∈ A, i ∈ nhds x) → C(α, β)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.of_ne_one : ∀ {α : Type u_1} (a : α), FreeGroup.of a ≠ 1
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.wbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ → Wbtw ℝ p₁ s.center p₂
-- Mathlib.CategoryTheory.Limits.Preorder
/-- An initial object in a preorder `C` is bottom element for `C`.  -/
CategoryTheory.Limits.IsInitial.orderBot : {C : Type u} → [inst : Preorder C] → {X : C} → CategoryTheory.Limits.IsInitial X → OrderBot C
-- Init.Data.Array.Count
Array.count_empty : ∀ {α : Type u_1} [inst : BEq α] {a : α}, Array.count a #[] = 0
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (a : α) (b : β) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? ⟨{ size := size, buckets := buckets }, hm⟩ a b =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ =>
      let bkt := buckets[i];
      match Std.DHashMap.Internal.AssocList.get? a bkt with
      | none =>
        have size' := size + 1;
        let buckets' := buckets.uset i (Std.DHashMap.Internal.AssocList.cons a b bkt) h;
        (none, Std.DHashMap.Internal.Raw₀.expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩)
      | some v => (some v, ⟨{ size := size, buckets := buckets }, hm⟩)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.isLoop_iff_mem_edgeSet_and_singleton : ∀ {α : Type u_1} {e : Set α} {H : Hypergraph α}, H.IsLoop e ↔ e ∈ H.edgeSet ∧ ∃ x, e = {x}
-- Mathlib.Data.EReal.Basic
/-- The set of numbers in `EReal` that are not equal to `±∞` is equivalent to `ℝ`.  -/
EReal.neTopBotEquivReal : ↑{⊥, ⊤}ᶜ ≃ ℝ
-- Mathlib.Data.Nat.Choose.Factorization
Nat.factorization_factorial_eq_zero_of_lt : ∀ {p n : ℕ}, n < p → n.factorial.factorization p = 0
-- Mathlib.Algebra.Order.Group.OrderIso
/-- **Alias** of the forward direction of `inv_le'`. -/
inv_le_of_inv_le' : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] [MulRightMono α] {a b : α}, a⁻¹ ≤ b → b⁻¹ ≤ a
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f g : X ⟶ Y) (hfg : f = g) (x : ↑X.toTopCat),
  AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap g x)
-- Mathlib.FieldTheory.Perfect
Polynomial.rootsExpandPowEquivRoots_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (p : ℕ) [inst_2 : ExpChar R p] (f : Polynomial R)
  [inst_3 : DecidableEq R] [inst_4 : PerfectRing R p] (n : ℕ) (x : ↥((Polynomial.expand R (p ^ n)) f).roots.toFinset),
  ↑((Polynomial.rootsExpandPowEquivRoots p f n) x) = ↑x ^ p ^ n
-- Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots
AdjoinPthRoots.algebraMap_root_symm : ∀ {k : Type u_1} [inst : Field k] (p : ℕ) [ExpChar k p] (x : AdjoinPthRoots k),
  (algebraMap k (AdjoinPthRoots k)) ((AdjoinPthRoots.root k).symm x) = x ^ p
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.ComposableArrows.Precomp.obj.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (X : C)
  (isLt : 0 < n + 1 + 1), CategoryTheory.ComposableArrows.Precomp.obj F X ⟨0, isLt⟩ = X
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.centralizer_univ : ∀ {R : Type u_1} [inst : Semiring R], Subsemiring.centralizer Set.univ = Subsemiring.center R
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.instEpiTopCatPullbackComparisonForgetToTop : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S),
  CategoryTheory.Epi (CategoryTheory.Limits.pullbackComparison AlgebraicGeometry.Scheme.forgetToTop f g)
-- Lean.Meta.Tactic.Simp.Rewrite
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.rewrite?.diagnoseWhenNoIndex : Lean.Expr → Lean.Meta.SimpTheoremTree → Lean.Meta.SimpTheorem → Lean.Meta.SimpM Unit
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.mul_lt_one_of_lt_of_le`.  -/
Left.mul_lt_one_of_lt_of_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b : α}, a < 1 → b ≤ 1 → a * b < 1
-- Mathlib.Data.EReal.Inv
EReal.mul_div_cancel : ∀ {a b : EReal}, b ≠ ⊥ → b ≠ ⊤ → b ≠ 0 → b * (a / b) = a
-- Mathlib.Data.Fintype.Prod
/-- Non-dependent version of `Pi.infinite_of_left`.  -/
Function.infinite_of_left : ∀ {ι : Sort u_4} {π : Type u_5} [Nontrivial π] [Infinite ι], Infinite (ι → π)
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.CasesTypes.eraseDecl : Lean.Meta.Grind.CasesTypes → Lean.Name → Lean.CoreM Lean.Meta.Grind.CasesTypes
-- Mathlib.Geometry.Convex.Cone.Basic
Submodule.toConvexCone_top : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], ⊤.toConvexCone = ⊤
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isIdempotentElemEquivClopens_symm_top : ∀ {R : Type u} [inst : CommRing R], PrimeSpectrum.isIdempotentElemEquivClopens.symm ⊤ = ⟨1, ⋯⟩
-- Lean.Data.Iterators.Producers.PersistentHashMap
/-- Counts the total number of entries reachable from a node, including nested children.  -/
Lean.PersistentHashMap.Node.measure : {α : Type u_1} → {β : Type u_2} → Lean.PersistentHashMap.Node α β → ℕ