mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.StructuredArrow
CategoryTheory.Localization.induction_structuredArrow : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] {X : C}
  (P : CategoryTheory.StructuredArrow (L.obj X) L → Prop),
  P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X))) →
    (∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁),
        P (CategoryTheory.StructuredArrow.mk φ) →
          P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp φ (L.map f)))) →
      (∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
          P (CategoryTheory.StructuredArrow.mk φ) →
            P
              (CategoryTheory.StructuredArrow.mk
                (CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Localization.isoOfHom L W w hw).inv))) →
        ∀ (g : CategoryTheory.StructuredArrow (L.obj X) L), P g
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.pow_mulLeft` for matrix multiplication.  -/
pow_mulLeftLinearMap : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} {A : Type u_6} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : Semiring R] [inst_3 : Semiring A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A] (a : Matrix m m A)
  (k : ℕ), mulLeftLinearMap n R a ^ k = mulLeftLinearMap n R (a ^ k)
-- Mathlib.GroupTheory.Commutator.Basic
addCommutator_centralizer_addCommutator_le_center : ∀ (G : Type u_1) [inst : AddGroup G],
  ⁅AddSubgroup.centralizer ↑(addCommutator G), AddSubgroup.centralizer ↑(addCommutator G)⁆ ≤ AddSubgroup.center G
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofBijective_symm_apply_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective ⇑f) (x : A₁),
  (AlgEquiv.ofBijective f hf).symm (f x) = x
-- Qq.Simp
/-- A copy of `Lean.Meta.Simproc` with explicit types.

See `Simproc.ofQ` to construct terms of this type.  -/
Lean.Meta.Simp.SimprocQ : Type
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Ring.hom_ext : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonAssocSemiring (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)]
  [inst_6 : Nonempty ι] (P : Type u_7) [inst_7 : NonAssocSemiring P] {g₁ g₂ : DirectLimit G f →+* P},
  (∀ (i : ι), g₁.comp (DirectLimit.Ring.of G f i) = g₂.comp (DirectLimit.Ring.of G f i)) → g₁ = g₂
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.tensorEquiv_symm_single_eq_tmul_single_one : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] (mn : M × N) (r : R),
  (MonoidAlgebra.tensorEquiv R).symm (MonoidAlgebra.single mn r) =
    MonoidAlgebra.single mn.1 r ⊗ₜ[R] MonoidAlgebra.single mn.2 1
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.pow : ∀ {α : Type u_2} [inst : Monoid α] {s : Set α}, s.Nonempty → ∀ {n : ℕ}, (s ^ n).Nonempty
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.Submartingale.stoppedAbove : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ → ∀ (r : ℝ), MeasureTheory.Submartingale (MeasureTheory.stoppedAbove f r) ℱ μ
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.HasPullbacksAlong.hasPullback : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y}
  [self : P.HasPullbacksAlong f] {W : C} (g : W ⟶ Y), P g → CategoryTheory.Limits.HasPullback g f
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.addMonoidHom_apply : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (f : M →+ N)
  (g : ι →₀ M), (Finsupp.mapRange.addMonoidHom f) g = Finsupp.mapRange ⇑f ⋯ g
-- Mathlib.CategoryTheory.Filtered.FinallySmall
CategoryTheory.InitiallySmall.instCategoryCofilteredInitialModel : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofiltered C] →
      [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] →
        [inst_3 : CategoryTheory.InitiallySmall C] →
          CategoryTheory.Category.{w, w} (CategoryTheory.InitiallySmall.CofilteredInitialModel C)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toList_rcc' : ∀ {m n k : ℤ}, List.map (fun x => k + x) (m...=n).toList = ((k + m)...=k + n).toList
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring : {α : Type u} → [self : NonUnitalNonAssocCommSemiring α] → NonUnitalNonAssocSemiring α
-- Lean.Elab.DefView
Lean.Elab.DefKind.example.sizeOf_spec : sizeOf Lean.Elab.DefKind.example = 1
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trList.match_1.eq_2 : ∀ (motive : List ℕ → Sort u_1) (n : ℕ) (ns : List ℕ) (h_1 : Unit → motive [])
  (h_2 : (n : ℕ) → (ns : List ℕ) → motive (n :: ns)),
  (match n :: ns with
    | [] => h_1 ()
    | n :: ns => h_2 n ns) =
    h_2 n ns
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.pos_intCast_of_pos : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R] (a : ℤ), 0 < a → 0 < ↑a
-- Mathlib.Algebra.GCDMonoid.PUnit
PUnit.lcm_eq : ∀ {x y : PUnit.{u_1 + 1}}, lcm x y = PUnit.unit
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_symm_coe_below : ∀ {n : ℕ} {i : Fin (n + 1)} {m : Fin n}, m.castSucc < i → (finSuccEquiv' i).symm (some m) = m.castSucc
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_subset_cthickening_of_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ₁ δ₂ : ℝ},
  δ₁ ≤ δ₂ → ∀ (E : Set α), Metric.thickening δ₁ E ⊆ Metric.cthickening δ₂ E
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.sameCycle : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.IsCycle → f x ≠ x → f y ≠ y → f.SameCycle x y
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instRing : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Ring β] → Ring (MeasureTheory.SimpleFunc α β)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
/-- The connecting homomorphism in the Jacobi-Zariski sequence for given presentations.
Given representations `0 → I → R[X] → S → 0` and `0 → K → S[Y] → T → 0`,
we may consider the induced representation `0 → J → R[X, Y] → T → 0`,
and this map is obtained by applying snake lemma to the following diagram
```
    T ⊗[S] Ω[S/R]    →          Ω[T/R]        →   Ω[T/S]  → 0
        ↑                         ↑                 ↑
0 → T ⊗[S] (⨁ₓ S dx) → (⨁ₓ T dx) ⊕ (⨁ᵧ T dy) →  ⨁ᵧ T dy → 0
        ↑                         ↑                 ↑
    T ⊗[S] (I/I²)    →           J/J²         →    K/K²   → 0
                                  ↑                 ↑
                             H¹(L_{T/R})      → H¹(L_{T/S})

```
This is independent from the presentations chosen. See `H1Cotangent.δ_comp_equiv`.
 -/
Algebra.Generators.H1Cotangent.δ : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {T : Type u₃} →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  [IsScalarTower R S T] →
                    {ι : Type w₁} →
                      {σ : Type w₂} →
                        (Q : Algebra.Generators S T ι) →
                          Algebra.Generators R S σ → Q.toExtension.H1Cotangent →ₗ[T] TensorProduct S T Ω[S⁄R]
-- Init.Data.Option.Lemmas
Option.map_min : ∀ {α : Type u_1} {β : Type u_2} [inst : Min α] [inst_1 : Min β] {o o' : Option α} {f : α → β},
  (∀ (x y : α), f (x ⊓ y) = f x ⊓ f y) → Option.map f (o ⊓ o') = Option.map f o ⊓ Option.map f o'
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientMap.eq_1 : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] {I : Ideal R} (J : Ideal S) [inst_2 : I.IsTwoSided]
  [inst_3 : J.IsTwoSided] (f : R →+* S) (hIJ : I ≤ Ideal.comap f J),
  Ideal.quotientMap J f hIJ = Ideal.Quotient.lift I ((Ideal.Quotient.mk J).comp f) ⋯
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_ne_zero_iff : ∀ {α : Type u_1} [inst : Zero α] (a : αˢʸᵐ), SymAlg.unsym a ≠ 0 ↔ a ≠ 0
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.coe_symm_measurableEquivPiIoc_apply : ∀ {ι : Type u_2} (b : ι → ℝ) (y : { x // ∀ (i : ι), x i ∈ Set.Ioc (b i) (b i + 1) }),
  (UnitAddTorus.measurableEquivPiIoc b).symm y = fun i => ↑(↑y i)
-- Mathlib.Topology.Homotopy.Lifting
/-- The monodromy of a covering map `p : E → X`, which sends a lift of the starting point of a
path in `X` to the endpoint of the lifted path in `E`. It only depends on the homotopy class
of the path.  -/
IsCoveringMap.monodromy : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {p : E → X} → IsCoveringMap p → {x y : X} → Path.Homotopic.Quotient x y → ↑(p ⁻¹' {x}) → ↑(p ⁻¹' {y})
-- Std.Data.Iterators.Producers.Monadic.Empty
/-- Returns an iterator that terminates immediately.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always

 -/
Std.IterM.empty : (m : Type w → Type w') → (β : Type w) → Std.IterM m β
-- Mathlib.Order.Hom.Bounded
/-- The function preserves the top element. The preferred spelling is `map_top`.  -/
TopHom.map_top' : ∀ {α : Type u_6} {β : Type u_7} [inst : Top α] [inst_1 : Top β] (self : TopHom α β), self.toFun ⊤ = ⊤
-- Mathlib.Order.Lattice
inf_lt_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b < b ↔ ¬b ≤ a
-- Mathlib.CategoryTheory.Action.Monoidal
Action.forget_ε : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V],
  CategoryTheory.Functor.LaxMonoidal.ε (Action.forget V G) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)
-- Init.Data.BitVec.Bitblast
BitVec.getMsbD_srem : ∀ {w i : ℕ} {x y : BitVec w},
  (x.srem y).getMsbD i =
    match x.msb, y.msb with
    | false, false => (x % y).getMsbD i
    | false, true => (x % -y).getMsbD i
    | true, false => (-(-x % y)).getMsbD i
    | true, true => (-(-x % -y)).getMsbD i
-- Mathlib.LinearAlgebra.Pi
LinearMap.proj_surjective : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] (i : ι), Function.Surjective ⇑(LinearMap.proj i)
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.comp_apply : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.Structure P] (g : L.ElementaryEmbedding N P) (f : L.ElementaryEmbedding M N) (x : M),
  (g.comp f) x = g (f x)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.ne_one : ∀ {x : ℝ}, Irrational x → x ≠ 1
-- Init.SizeOf
sizeOf_default : ∀ {α : Sort u_1} (n : α), sizeOf n = 0
-- Mathlib.Logic.Basic
forall_imp_iff_exists_imp : ∀ {α : Sort u_3} {p : α → Prop} {b : Prop} [ha : Nonempty α], (∀ (x : α), p x) → b ↔ ∃ x, p x → b
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minView.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l' r' : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl.View α β (l'.size + r'.size) → Sort u_3) (dk : α) (dv : β dk)
  (dt : Std.DTreeMap.Internal.Impl α β) (hdt : dt.Balanced) (hdt' : dt.size = l'.size + r'.size)
  (h_1 :
    (dk : α) →
      (dv : β dk) →
        (dt : Std.DTreeMap.Internal.Impl α β) →
          (hdt : dt.Balanced) →
            (hdt' : dt.size = l'.size + r'.size) →
              motive { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } }),
  (match { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } } with
    | { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } } => h_1 dk dv dt hdt hdt') =
    h_1 dk dv dt hdt hdt'
-- Mathlib.Probability.Distributions.Uniform
PMF.support_uniformOfFintype : ∀ (α : Type u_2) [inst : Fintype α] [inst_1 : Nonempty α], (PMF.uniformOfFintype α).support = ⊤
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.Forget₂.createsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat),
  CommGrpCat.Forget₂.createsLimit F =
    CategoryTheory.createsLimitOfReflectsIso fun c hc =>
      have this := ⋯;
      have this := ⋯;
      have this_1 := this;
      have this_2 := this_1;
      {
        liftedCone :=
          {
            pt :=
              CommGrpCat.of
                (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommGrpCat))).pt,
            π :=
              {
                app := fun j =>
                  CommGrpCat.ofHom
                    (MonCat.limitπMonoidHom
                      (F.comp ((CategoryTheory.forget₂ CommGrpCat GrpCat).comp (CategoryTheory.forget₂ GrpCat MonCat)))
                      j),
                naturality := ⋯ } },
        validLift := (GrpCat.limitConeIsLimit (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat))).uniqueUpToIso hc,
        makesLimit :=
          CategoryTheory.Limits.IsLimit.ofFaithful
            ((CategoryTheory.forget₂ CommGrpCat GrpCat).comp (CategoryTheory.forget₂ GrpCat MonCat))
            (MonCat.HasLimits.limitConeIsLimit
              (F.comp ((CategoryTheory.forget₂ CommGrpCat GrpCat).comp (CategoryTheory.forget₂ GrpCat MonCat))))
            (fun s =>
              {
                hom' :=
                  {
                    toFun := fun v =>
                      EquivLike.coe
                        (equivShrink
                          ↑((F.comp
                                    ((CategoryTheory.forget₂ CommGrpCat GrpCat).comp
                                      (CategoryTheory.forget₂ GrpCat MonCat))).comp
                                (CategoryTheory.forget MonCat)).sections)
                        ⟨fun j =>
                          (CategoryTheory.ConcreteCategory.hom
                              (((CategoryTheory.forget MonCat).mapCone
                                      (((CategoryTheory.forget₂ CommGrpCat GrpCat).comp
                                            (CategoryTheory.forget₂ GrpCat MonCat)).mapCone
                                        s)).π.app
                                j))
                            v,
                          ⋯⟩,
                    map_one' := ⋯, map_mul' := ⋯ } })
            ⋯ }
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.NatTrans.PullbackShift.natIsoId.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B),
  CategoryTheory.NatTrans.PullbackShift.natIsoId C φ =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.PullbackShift C φ))
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.brecOn_3.eq : ∀ {motive_1 : Lean.Widget.MsgEmbed → Sort u} {motive_2 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Sort u}
  {motive_3 :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
        (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
      Sort u}
  {motive_4 : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u}
  {motive_5 : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u}
  (t : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) (F_1 : (t : Lean.Widget.MsgEmbed) → t.below → motive_1 t)
  (F_2 : (t : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Lean.Widget.MsgEmbed.below_1 t → motive_2 t)
  (F_3 :
    (t :
        Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
          (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
      Lean.Widget.MsgEmbed.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) → Lean.Widget.MsgEmbed.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) → Lean.Widget.MsgEmbed.below_4 t → motive_5 t),
  Lean.Widget.MsgEmbed.brecOn_3 t F_1 F_2 F_3 F_4 F_5 = F_4 t (Lean.Widget.MsgEmbed.brecOn_3.go t F_1 F_2 F_3 F_4 F_5).2
-- Mathlib.Analysis.Normed.Group.Hom
/-- The norm of the identity is at most `1`. It is in fact `1`, except when the norm of every
element vanishes, where it is `0`. (Since we are working with seminorms this can happen even if the
space is non-trivial.) It means that one cannot do better than an inequality in general.  -/
NormedAddGroupHom.norm_id_le : ∀ (V : Type u_1) [inst : SeminormedAddCommGroup V], ‖NormedAddGroupHom.id V‖ ≤ 1
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
/-- The horizontal composition of 2-squares. (Variant where we allow the replacement of
the horizontal compositions by isomorphic functors.)  -/
CategoryTheory.TwoSquare.hComp' : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_4} →
        {D₂ : Type u_5} →
          {D₃ : Type u_6} →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] →
                        {V₁ : CategoryTheory.Functor C₁ D₁} →
                          {T₁ : CategoryTheory.Functor C₁ C₂} →
                            {B₁ : CategoryTheory.Functor D₁ D₂} →
                              {V₂ : CategoryTheory.Functor C₂ D₂} →
                                CategoryTheory.TwoSquare T₁ V₁ V₂ B₁ →
                                  {T₂ : CategoryTheory.Functor C₂ C₃} →
                                    {B₂ : CategoryTheory.Functor D₂ D₃} →
                                      {V₃ : CategoryTheory.Functor C₃ D₃} →
                                        CategoryTheory.TwoSquare T₂ V₂ V₃ B₂ →
                                          {T₁₂ : CategoryTheory.Functor C₁ C₃} →
                                            {B₁₂ : CategoryTheory.Functor D₁ D₃} →
                                              (T₁.comp T₂ ≅ T₁₂) →
                                                (B₁.comp B₂ ≅ B₁₂) → CategoryTheory.TwoSquare T₁₂ V₁ V₃ B₁₂
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.instIsFiniteKernelWithDensityRnDeriv : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [hκ : ProbabilityTheory.IsFiniteKernel κ]
  [inst : ProbabilityTheory.IsFiniteKernel η], ProbabilityTheory.IsFiniteKernel (η.withDensity (κ.rnDeriv η))
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.not_isDiag_of_mem_edgeSet : ∀ {V : Type u} (G : SimpleGraph V) {e : Sym2 V}, e ∈ G.edgeSet → ¬e.IsDiag
-- Init.Data.Array.Lemmas
Array.append_inj_left : ∀ {α : Type u_1} {xs₁ xs₂ ys₁ ys₂ : Array α}, xs₁ ++ ys₁ = xs₂ ++ ys₂ → xs₁.size = xs₂.size → xs₁ = xs₂
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
/-- Let `C` be the supremum of `ν s` over all measurable sets `s` such that `μ.restrict s` is
sigma-finite. `C` is finite since `ν` is a finite measure. Then there exists a measurable set `t`
with `μ.restrict t` sigma-finite such that `ν t ≥ C - 1/n`.  -/
MeasureTheory.exists_isSigmaFiniteSet_measure_ge : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν] (n : ℕ),
  ∃ t,
    MeasurableSet t ∧
      MeasureTheory.SigmaFinite (μ.restrict t) ∧
        (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : MeasureTheory.SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t
-- Init.Data.List.Nat.Modify
List.take_modify : ∀ {α : Type u_1} (f : α → α) (i j : ℕ) (l : List α), List.take j (l.modify i f) = (List.take j l).modify i f
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Eta-expanded form of `contDiffAt_id` -/
contDiffAt_fun_id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {x : E}, ContDiffAt 𝕜 n (fun x => x) x
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.prod_top : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (s : Subring R),
  s.prod ⊤ = Subring.comap (RingHom.fst R S) s
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf.eq_1 : ∀ {G : Type u_1} [inst : AddMonoid G] (x : G), addOrderOf x = Function.minimalPeriod (fun x_1 => x + x_1) 0
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of `AffineSubspace.setOfPred_sSameSide_eq_image2`. -/
AffineSubspace.setOf_sSameSide_eq_image2 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x p : P},
  x ∉ s → p ∈ s → {y | s.SSameSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s
-- Lean.Server.Rpc.Basic
Lean.Server.instRpcEncodableOption : {α : Type} → [Lean.Server.RpcEncodable α] → Lean.Server.RpcEncodable (Option α)
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp
/-- Converting a group object in `Type u` into a group.  -/
GrpTypeEquivalenceGrp.functor : CategoryTheory.Functor (CategoryTheory.Grp (Type u)) GrpCat
-- Aesop.RuleTac.Basic
Aesop.RuleTac.ofTacticSyntax : (Aesop.RuleTacInput → Lean.MetaM Lean.Syntax.Tactic) → Aesop.RuleTac
-- Mathlib.Data.ZMod.Basic
ZMod.val.eq_2 : ∀ (n : ℕ), ZMod.val = Fin.val
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.transvection_coeff_zero : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i j : ι}
  (hij : i ≠ j), Matrix.SpecialLinearGroup.transvection hij 0 = 1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
MeasureTheory.Integrable.aefinStronglyMeasurable : ∀ {α : Type u_1} {G : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup G]
  {f : α → G}, MeasureTheory.Integrable f μ → MeasureTheory.AEFinStronglyMeasurable f μ
-- Mathlib.Topology.Algebra.Algebra
/-- Under a continuous algebra map, the image of the `TopologicalClosure` of a subalgebra is
contained in the `TopologicalClosure` of its image.  -/
Subalgebra.map_topologicalClosure_le : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : IsSemitopologicalSemiring B] (f : A →A[R] B) (s : Subalgebra R A),
  Subalgebra.map (↑f) s.topologicalClosure ≤ (Subalgebra.map (↑f) s).topologicalClosure
-- Mathlib.Algebra.GroupWithZero.Opposite
MulOpposite.instIsCancelMulZero : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [IsCancelMulZero α], IsCancelMulZero αᵐᵒᵖ
-- Init.Data.SInt.Basic
instInhabitedInt32 : Inhabited Int32
-- Init.Data.Int.Gcd
Int.gcd_dvd_gcd_mul_right_right : ∀ (a b c : ℤ), a.gcd b ∣ a.gcd (b * c)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.instSMul : {α : Type u_1} → [inst : MeasurableSpace α] → SMul NNReal (MeasureTheory.JordanDecomposition α)