mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.reflexivePair.match_3.splitter : (motive : (X Y : CategoryTheory.Limits.WalkingReflexivePair) → (X ⟶ Y) → Sort u_1) →
  (X Y : CategoryTheory.Limits.WalkingReflexivePair) →
    (h : X ⟶ Y) →
      ((x : CategoryTheory.Limits.WalkingReflexivePair) →
          motive x x (CategoryTheory.Limits.WalkingReflexivePair.Hom.id x)) →
        (Unit →
            motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
              CategoryTheory.Limits.WalkingReflexivePair.Hom.left) →
          (Unit →
              motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
                CategoryTheory.Limits.WalkingReflexivePair.Hom.right) →
            (Unit →
                motive CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Limits.WalkingReflexivePair.one
                  CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) →
              (Unit →
                  motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
                    CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion) →
                (Unit →
                    motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
                      CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion) →
                  motive X Y h
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k k' fallback : α} {f : β → β},
      (Std.DHashMap.Internal.Raw₀.Const.modify m k f).getKeyD k' fallback =
        if (k == k') = true then if m.contains k = true then k else fallback else m.getKeyD k' fallback
-- Mathlib.Data.Countable.Defs
Countable.of_equiv : ∀ {β : Sort v} (α : Sort u_1) [Countable α] (e : α ≃ β), Countable β
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerivedNatTrans.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (LF' LF : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α' α'_1 : L.comp LF' ⟶ F'),
  α' = α'_1 →
    ∀ (α α_1 : L.comp LF ⟶ F) (e_α : α = α_1) (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1)
      [inst_3 : L.IsLocalization W] [inst_4 : LF.IsLeftDerivedFunctor α W] (τ τ_1 : F' ⟶ F),
      τ = τ_1 → LF'.leftDerivedNatTrans LF α' α W τ = LF'.leftDerivedNatTrans LF α'_1 α_1 W_1 τ_1
-- Mathlib.Data.Rel
SetRel.isSymm_id : ∀ {α : Type u_1}, SetRel.id.IsSymm
-- Mathlib.Analysis.ODE.PicardLindelof
/-- `IsPicardLindelof` is preserved when enlarging the Lipschitz constant `K`.  -/
IsPicardLindelof.weaken_lipschitz : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E}
  {a r L K : NNReal}, IsPicardLindelof f t₀ x₀ a r L K → ∀ {K' : NNReal}, K ≤ K' → IsPicardLindelof f t₀ x₀ a r L K'
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.sInter : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set (Set α)},
  s.Countable → (∀ t ∈ s, MeasureTheory.NullMeasurableSet t μ) → MeasureTheory.NullMeasurableSet (⋂₀ s) μ
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.instAddCommGroup : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] → {X Y : C} → {n : ℕ} → AddCommGroup (CategoryTheory.Abelian.Ext X Y n)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.type? : Lean.Elab.Command.InductiveView → Option Lean.Syntax
-- Mathlib.Topology.CompactOpen
/-- If `X` has a single element, then `Y` is homeomorphic to `C(X, Y)`.  -/
Homeomorph.continuousMapOfUnique : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → [Unique X] → Y ≃ₜ C(X, Y)
-- Mathlib.Data.Set.Opposite
Set.unop_mem_unop : ∀ {α : Type u_1} {s : Set αᵒᵖ} {a : αᵒᵖ}, Opposite.unop a ∈ s.unop ↔ a ∈ s
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
/-- For any `K`-basis of `L`, and any `x : L`, we have `B.norm (-x) = B.norm x`.  -/
Module.Basis.norm_neg : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Ring L] [inst_2 : Algebra K L] {ι : Type u_3}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] (B : Module.Basis ι K L) (x : L), B.norm (-x) = B.norm x
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation on `R`.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDedekindDomain R] → IsDedekindDomain.HeightOneSpectrum R → Valuation R (WithZero (Multiplicative ℤ))
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_pushArg : ∀ {ps : Std.Do.PostShape} {α σ : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)}
  (f : σ → Std.Do.PredTrans ps (α × σ)),
  (Std.Do.PredTrans.pushArg f).apply Q = fun s =>
    (f s).apply
      (fun x =>
        match x with
        | (a, s) => Q.1 a s,
        Q.2)
-- Mathlib.SetTheory.Ordinal.Principal
/-- Principal ordinals under any operation are unbounded.  -/
Ordinal.not_bddAbove_setOfPred_isPrincipal : ∀ (op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}), ¬BddAbove {o | Ordinal.IsPrincipal op o}
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.IsAddModHom.addActionHom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {X : C} [inst_3 : CategoryTheory.AddModObj M X] {Y : C}
  [inst_4 : CategoryTheory.AddModObj M Y] (f : X ⟶ Y) [inst_5 : CategoryTheory.IsAddModHom M f] (Z : C),
  CategoryTheory.IsAddModHom.addActionHom f Z =
    { toFun := fun x => CategoryTheory.CategoryStruct.comp x f, map_vadd' := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_le_left_iff_le : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} {r : k}, 0 < r → ((AffineMap.lineMap a b) r ≤ a ↔ b ≤ a)
-- Init.Data.List.MinMax
List.foldl_min_eq_min : ∀ {α : Type u_1} [inst : Min α] [Std.IdempotentOp min] [Std.Associative min] {l : List α} (hl : l ≠ []) {a : α},
  List.foldl min a l = a ⊓ l.min hl
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (k : α)
  (hlk : Std.DTreeMap.Internal.Impl.contains k t = true),
  t.getKey k hlk =
    match t, hlk with
    | Std.DTreeMap.Internal.Impl.inner size k' v l r, hlk =>
      match h : compare k k' with
      | Ordering.lt => l.getKey k ⋯
      | Ordering.gt => r.getKey k ⋯
      | Ordering.eq => k'
-- Mathlib.Combinatorics.Enumerative.Stirling
_private.Mathlib.Combinatorics.Enumerative.Stirling.0.Nat.stirlingFirst.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) →
  (x x_1 : ℕ) →
    (Unit → motive 0 0) →
      ((n : ℕ) → motive 0 n.succ) → ((n : ℕ) → motive n.succ 0) → ((n k : ℕ) → motive n.succ k.succ) → motive x x_1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceBneDiff : Lean.Meta.Simp.Simproc
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.apply_linearCombination : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {M' : Type u_8} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') (v : α → M) (l : α →₀ R),
  f ((Finsupp.linearCombination R v) l) = (Finsupp.linearCombination R (⇑f ∘ v)) l
-- Mathlib.Algebra.Group.Hom.Instances
instIsLeftCancelMulMonoidHom : ∀ {M : Type uM} {N : Type uN} [inst : MulOneClass M] [inst_1 : CommMonoid N] [IsLeftCancelMul N],
  IsLeftCancelMul (M →* N)
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeriesBilinear_apply_one : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F),
  f.fpowerSeriesBilinear x 1 = (continuousMultilinearCurryFin1 𝕜 (E × F) G).symm (f.deriv₂ x)
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
/-- The bijection on nondegenerate simplices induced by an isomorphism
of simplicial sets.  -/
SSet.nonDegenerateEquivOfIso : {X Y : SSet} → (X ≅ Y) → {n : ℕ} → ↑(X.nonDegenerate n) ≃ ↑(Y.nonDegenerate n)
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- `X ×[X ⨿ Y] Y` is initial.  -/
CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjoint : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] →
        [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y] →
          [inst_3 :
              CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr] →
            CategoryTheory.Limits.IsInitial
              (CategoryTheory.Limits.pullback CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.exists_of_rankOne_eq_rankOne : ∀ {𝕜 : Type u_4} [inst : RCLike 𝕜] {F : Type u_8} {H : Type u_9} [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace 𝕜 F] [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H] {a c : F} {b d : H},
  a ≠ 0 →
    b ≠ 0 →
      ((InnerProductSpace.rankOne 𝕜) a) b = ((InnerProductSpace.rankOne 𝕜) c) d →
        ∃ α β, ∃ (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The canonical map `X ⟶ Spec Γ(X, ⊤)`. This is the unit of the `Γ-Spec` adjunction.  -/
AlgebraicGeometry.Scheme.toSpecΓ : (X : AlgebraicGeometry.Scheme) → X ⟶ AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op ⊤))
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compl₁₂_apply : ∀ {R₁ : Type u_3} {R₂ : Type u_4} [inst : Semiring R₁] [inst_1 : Semiring R₂] {Mₗ : Type u_6} {N : Type u_7}
  {Pₗ : Type u_9} {Qₗ : Type u_10} {Qₗ' : Type u_11} [inst_2 : AddCommMonoid Mₗ] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid Pₗ] [inst_5 : AddCommMonoid Qₗ] [inst_6 : AddCommMonoid Qₗ'] [inst_7 : Module R₁ Mₗ]
  [inst_8 : Module R₂ N] [inst_9 : Module R₂ Pₗ] [inst_10 : Module R₁ Pₗ] [inst_11 : Module R₁ Qₗ]
  [inst_12 : Module R₂ Qₗ'] [inst_13 : SMulCommClass R₂ R₁ Pₗ] (f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ) (g : Qₗ →ₗ[R₁] Mₗ)
  (g' : Qₗ' →ₗ[R₂] N) (x : Qₗ) (y : Qₗ'), ((f.compl₁₂ g g') x) y = (f (g x)) (g' y)
-- Mathlib.Algebra.Module.Equiv.Basic
AddHom.mk.congr_simp : ∀ {M : Type u_10} {N : Type u_11} [inst : Add M] [inst_1 : Add N] (toFun toFun_1 : M → N) (e_toFun : toFun = toFun_1)
  (map_add' : ∀ (x y : M), toFun (x + y) = toFun x + toFun y),
  { toFun := toFun, map_add' := map_add' } = { toFun := toFun_1, map_add' := ⋯ }
-- Mathlib.Probability.Independence.Conditional
/-- The σ-algebras generated by conditionally independent pi-systems are conditionally independent.
 -/
ProbabilityTheory.iCondIndepSets.iCondIndep : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] (m : ι → MeasurableSpace Ω),
  (∀ (i : ι), m i ≤ mΩ) →
    ∀ (π : ι → Set (Set Ω)),
      (∀ (n : ι), IsPiSystem (π n)) →
        (∀ (i : ι), m i = MeasurableSpace.generateFrom (π i)) →
          ProbabilityTheory.iCondIndepSets m' hm' π μ → ProbabilityTheory.iCondIndep m' hm' m μ
-- Init.Grind.Ring.Basic
/-- Natural number numerals in the semiring.
The field `ofNat_eq_natCast` ensures that these are (propositionally) equal to the values of `natCast`.
 -/
Lean.Grind.Semiring.ofNat : {α : Type u} → [self : Lean.Grind.Semiring α] → (n : ℕ) → OfNat α n
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_map_left : ∀ {α : Type u_3} {α' : Type u_4} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11}
  {p : Type u_12} (f : α' → β → γ) (g : α → α') (A : Matrix l m α) (B : Matrix n p β),
  Matrix.kroneckerMap f (A.map g) B = Matrix.kroneckerMap (fun a b => f (g a) b) A B
-- Init.Data.SInt.Lemmas
Int8.neg_mul_not_eq_add_mul : ∀ {a b : Int8}, -(a * ~~~b) = a + a * b
-- Mathlib.GroupTheory.Finiteness
/-- Finite product of finitely generated groups is finitely generated.  -/
Pi.instGroupFG : ∀ {ι : Type u_5} [Finite ι] {G : ι → Type u_6} [inst : (i : ι) → Group (G i)] [∀ (i : ι), Group.FG (G i)],
  Group.FG ((i : ι) → G i)
-- Mathlib.Data.Nat.ModEq
Nat.modEq_iff_eq_of_div_eq : ∀ {n a b : ℕ}, a / n = b / n → (a ≡ b [MOD n] ↔ a = b)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l → k ∈ List.map Prod.fst l → (Std.HashMap.ofList l).getKey! k' = k
-- Mathlib.Algebra.Module.SpanRank
Submodule.FG.finite_generators : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M},
  p.FG → p.generators.Finite
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.hasSheafifyEssentiallySmallSite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₃)
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.EssentiallySmall.{w, v₁, u₁} C]
  [CategoryTheory.HasSheafify ((CategoryTheory.equivSmallModel C).inverse.inducedTopology J) A],
  CategoryTheory.HasSheafify J A
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.mk.injEq : ∀ {n : ℕ} (blocks : List ℕ) (blocks_pos : ∀ {i : ℕ}, i ∈ blocks → 0 < i) (blocks_sum : blocks.sum = n)
  (blocks_1 : List ℕ) (blocks_pos_1 : ∀ {i : ℕ}, i ∈ blocks_1 → 0 < i) (blocks_sum_1 : blocks_1.sum = n),
  ({ blocks := blocks, blocks_pos := blocks_pos, blocks_sum := blocks_sum } =
      { blocks := blocks_1, blocks_pos := blocks_pos_1, blocks_sum := blocks_sum_1 }) =
    (blocks = blocks_1)
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_atTop_nsmul_tfae : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (x y : G),
  [MapClusterPt x Filter.atTop fun x => x • y, MapClusterPt x Filter.atTop fun x => x • y,
      x ∈ closure (Set.range fun x => x • y), x ∈ closure (Set.range fun x => x • y)].TFAE
-- Lean.Elab.AssertExists
/-- The name of the module where the assertion was made.  -/
Lean.Elab.Command.AssertExists.modName : Lean.Elab.Command.AssertExists → Lean.Name
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instZero : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → Zero (DoubleCentralizer 𝕜 A)
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.productEquiv_symm_apply_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max w v)}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  (F : J → C) [inst_3 : CategoryTheory.Limits.HasProduct F]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)]
  (x : (j : J) → CategoryTheory.ToType (F j)) (j : J),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j))
      ((CategoryTheory.Limits.Concrete.productEquiv F).symm x) =
    x j
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- A saturated additive submonoid is a submonoid `s` that satisfies `x + y ∈ s → x ∈ s ∧ y ∈ s`.  -/
SaturatedAddSubmonoid : (M : Type u_1) → [AddZeroClass M] → Type u_1
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- `AddSubmonoidClass S M` says `S` is a type of subsets `s ≤ M` that contain `0`
and are closed under `(+)`  -/
AddSubmonoidClass : (S : Type u_3) → (M : outParam (Type u_4)) → [AddZeroClass M] → [SetLike S M] → Prop
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Oplax.StrongTrans.Modification.id η).app a = CategoryTheory.CategoryStruct.id (η.app a)
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.bot_mul' : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (b : WithBot α), ⊥ * b = if b = 0 then 0 else ⊥
-- Aesop.RuleTac.Basic
Aesop.RuleTacInput.mk : Lean.MVarId →
  Aesop.UnorderedArraySet Lean.MVarId →
    Array Aesop.IndexMatchLocation → Option (Array Aesop.Substitution) → Aesop.Options' → Aesop.RuleTacInput
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum.congr_simp : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} {inst : DecidableEq ι} [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → Zero (β i)] {inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)}
  [inst_4 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_5 : AddCommMonoid γ] (f f_1 : Π₀ (i : ι), β i),
  f = f_1 → ∀ (g g_1 : (i : ι) → β i → γ), g = g_1 → f.sum g = f_1.sum g_1
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.comp_hom : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  {X Y Z : CategoryTheory.Abelian.SpectralObject C ι} (f : X.Hom Y) (g : Y.Hom Z) (n : ℤ),
  (CategoryTheory.CategoryStruct.comp f g).hom n = CategoryTheory.CategoryStruct.comp (f.hom n) (g.hom n)
-- Init.Data.SInt.Float32
/-- Obtains a `Float32` whose value is near the given `Int32`.

It will be exactly the value of the given `Int32` if such a `Float32` exists. If no such `Float32`
exists, the returned value will either be the smallest `Float32` that is larger than the given
value, or the largest `Float32` that is smaller than the given value.

This function does not reduce in the kernel.
 -/
Int32.toFloat32 : Int32 → Float32
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideEqualizer.lift_ι_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] [inst_2 : Nonempty J] {W : C} (k : W ⟶ X)
  (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)) {Z : C}
  (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.lift k h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.mul_dvd : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α} [DecompositionMonoid α], IsRelPrime x y → x ∣ z → y ∣ z → x * y ∣ z
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.toOpenₗ.eq_1 : ∀ (R M : Type u) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  AlgebraicGeometry.StructureSheaf.toOpenₗ R M U =
    { toFun := fun m => AlgebraicGeometry.StructureSheaf.const m 1 U ⋯, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The name length of a premise.  -/
Mathlib.Tactic.ClickSuggestions.Premise.length : Mathlib.Tactic.ClickSuggestions.Premise → ℕ
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α)
  [inst_1 : DecidableEq β] {b : β}, (insert b s).inf' ⋯ f = f b ⊓ s.inf' H f
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_add_one_le : ∀ {ι : Sort u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}}, (∀ (i : ι), f i < a) → ⨆ i, f i + 1 ≤ a
-- Mathlib.Data.List.Basic
List.head.hcongr_3 : ∀ (α α' : Type u),
  α = α' → ∀ (as : List α) (as' : List α'), as ≍ as' → ∀ (a : as ≠ []) (a' : as' ≠ []), a ≍ a' → as.head a ≍ as'.head a'
-- Mathlib.Data.Finset.Image
/-- The image of a nontrivial finset under a function injective on the finset is nontrivial.
For the version assuming `Function.Injective` see `Finset.map_nontrivial`, and for the combined
iff see `Finset.image_nontrivial_iff_of_injOn`.  -/
Finset.Nontrivial.image_of_injOn : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α},
  s.Nontrivial → Set.InjOn f ↑s → (Finset.image f s).Nontrivial
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.inv_simple : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B),
  (cs.simple i)⁻¹ = cs.simple i
-- Mathlib.Data.PNat.Prime
/-- The greatest common divisor (gcd) of two positive natural numbers,
viewed as positive natural number.  -/
PNat.gcd : ℕ+ → ℕ+ → ℕ+
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- The `ℕ∞`-valued rank function is submodular.  -/
Matroid.eRk_inter_add_eRk_union_le : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α), M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
-- Mathlib.Order.Restriction
Preorder.updateFinset_frestrictLe : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] [inst_2 : DecidableEq α]
  (a : α) (x : (a : α) → π a), Function.updateFinset x (Finset.Iic a) (Preorder.frestrictLe a x) = x
-- ProofWidgets.Component.Basic
ProofWidgets.Component.mk : {Props : Type} → Lean.Widget.Module → String → ProofWidgets.Component Props
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.instMonoFKernelSequenceE : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  CategoryTheory.Mono (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X}
  {c₁ c₂ : CategoryTheory.Limits.PullbackCone f g} (a : c₁ ⟶ c₂),
  (CategoryTheory.Limits.pullbackConeEquivBinaryFan.functor.map a).hom = CategoryTheory.Over.homMk a.hom ⋯
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_modify : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : β k → β k} (h : k' ∈ m.modify k f),
  (m.modify k f).get k' h = if heq : (k == k') = true then cast ⋯ (f (m.get k ⋯)) else m.get k' ⋯
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.L1.SimpleFunc.toLp_one_eq_toL1 : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Integrable (⇑f) μ),
  ↑(f.toLp ⋯) = MeasureTheory.Integrable.toL1 (⇑f) hf
-- Mathlib.Order.Cover
WCovBy.Icc_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b → Set.Icc a b = {a, b}
-- Init.Data.SInt.Lemmas
Int64.mul_zero : ∀ {a : Int64}, a * 0 = 0
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.isPrincipal_mul_ord : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) c.ord