mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.SizedBalancedTree.mk.inj : ∀ {α : Type u} {β : α → Type v} {lb ub : ℕ} {impl : Std.DTreeMap.Internal.Impl α β} {balanced_impl : impl.Balanced}
  {lb_le_size_impl : lb ≤ impl.size} {size_impl_le_ub : impl.size ≤ ub} {impl_1 : Std.DTreeMap.Internal.Impl α β}
  {balanced_impl_1 : impl_1.Balanced} {lb_le_size_impl_1 : lb ≤ impl_1.size} {size_impl_le_ub_1 : impl_1.size ≤ ub},
  { impl := impl, balanced_impl := balanced_impl, lb_le_size_impl := lb_le_size_impl,
        size_impl_le_ub := size_impl_le_ub } =
      { impl := impl_1, balanced_impl := balanced_impl_1, lb_le_size_impl := lb_le_size_impl_1,
        size_impl_le_ub := size_impl_le_ub_1 } →
    impl = impl_1
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.iff_le_inverseImage_isomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (W : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D),
  W.IsInvertedBy F ↔ W ≤ (CategoryTheory.MorphismProperty.isomorphisms D).inverseImage F
-- Init.Data.Array.Attach
Array.unattach_push : ∀ {α : Type u_1} {p : α → Prop} {a : { x // p x }} {xs : Array { x // p x }}, (xs.push a).unattach = xs.unattach.push ↑a
-- Init.Data.Array.OfFn
Array.ofFn_succ : ∀ {n : ℕ} {α : Type u_1} {f : Fin (n + 1) → α}, Array.ofFn f = (Array.ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)
-- Aesop.Script.UScript
Aesop.Script.UScript.renderTacticSeq : Aesop.Script.UScript → Lean.Meta.SavedState → Lean.MVarId → Lean.MetaM (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)
-- Init.Data.ByteArray.Basic
ByteArray.copySlice.eq_1 : ∀ (src : ByteArray) (srcOff : ℕ) (dest : ByteArray) (destOff len : ℕ) (exact : Bool),
  src.copySlice srcOff dest destOff len exact =
    {
      data :=
        dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len) ++
          dest.data.extract (destOff + min len (src.data.size - srcOff)) }
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- If a scalar is central, then its right action is measurable when its left action is.  -/
MulOpposite.instMeasurableConstSMul : ∀ {M : Type u_2} {α : Type u_4} {m : MeasurableSpace α} [inst : SMul M α] [inst_1 : SMul Mᵐᵒᵖ α] [IsCentralScalar M α]
  [MeasurableConstSMul M α], MeasurableConstSMul Mᵐᵒᵖ α
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colim.congr_simp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C], CategoryTheory.Limits.colim = CategoryTheory.Limits.colim
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.prodPrimes_ne_zero : ∀ {s : BoundingSieve}, s.prodPrimes ≠ 0
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.sup_support_coeff_mul_le`. -/
AddMonoidAlgebra.sup_support_mul_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : SemilatticeSup B] [inst_1 : OrderBot B] [inst_2 : Semiring R]
  [inst_3 : Add A] [inst_4 : Add B] [AddLeftMono B] [AddRightMono B] {degb : A → B},
  (∀ (a b : A), degb (a + b) ≤ degb a + degb b) →
    ∀ (f g : AddMonoidAlgebra R A), (f * g).coeff.support.sup degb ≤ f.coeff.support.sup degb + g.coeff.support.sup degb
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_leftUnitor : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  (U : CategoryTheory.Functor X Y),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map U.leftUnitor.hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G (CategoryTheory.Functor.id X)
          U).hom
      (CategoryTheory.CategoryStruct.comp
        (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).whiskerLeft
          (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G X).hom)
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).rightUnitor.hom)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Construct a bundled `AddCommGrpCat` from the underlying type and typeclass.  -/
AddCommGrpCat.of : (M : Type u) → [AddCommGroup M] → AddCommGrpCat
-- Mathlib.Data.Finset.Insert
Finset.insert_idem : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), insert a (insert a s) = insert a s
-- Init.Data.Nat.Basic
Nat.le_of_mul_le_mul_right : ∀ {a b c : ℕ}, a * c ≤ b * c → 0 < c → a ≤ b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_eq_some_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {a : α} (h : a ∈ m), Std.DHashMap.Raw.Const.get? m a = some (Std.DHashMap.Raw.Const.get m a h)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∉ m₁ → (m₁ ∩ m₂).get? k = none
-- Init.Data.UInt.Lemmas
USize.toNat_ofNatClamp_of_le : ∀ {n : ℕ}, USize.size ≤ n → (USize.ofNatClamp n).toNat = USize.size - 1
-- Init.Data.UInt.Bitwise
UInt64.and_self : ∀ {a : UInt64}, a &&& a = a
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.liftpPreservation_iff_uniform : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F], MvQPF.LiftPPreservation ↔ MvQPF.IsUniform
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a right invariant measure under a left action is right invariant, assuming that
the action preserves multiplication.  -/
MeasureTheory.isMulRightInvariant_map_smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G}
  {α : Type u_3} [inst_3 : SMul α G] [SMulCommClass α Gᵐᵒᵖ G] [MeasurableConstSMul α G] [μ.IsMulRightInvariant] (a : α),
  (MeasureTheory.Measure.map (fun x => a • x) μ).IsMulRightInvariant
-- Init.Data.List.Zip
List.zip_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {l₁' l₂' : List (α × β)} {l₁ : List α} {l₂ : List β},
  l₁.zip l₂ = l₁' ++ l₂' ↔
    ∃ ws xs ys zs, ws.length = ys.length ∧ l₁ = ws ++ xs ∧ l₂ = ys ++ zs ∧ l₁' = ws.zip ys ∧ l₂' = xs.zip zs
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.uniformContinuous_compareEquiv : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α),
  UniformContinuous ⇑(pkg.compareEquiv pkg')
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.restrictScalars_bot_eq_self : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E),
  IntermediateField.restrictScalars F ⊥ = K
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_eq_ofNat : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo] (m : α),
  ↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g : G) (a : ↑A),
  ((fun₀ | g => (A.ρ g) a) + fun₀ | g⁻¹ => a) ∈ groupHomology.boundaries₁ A
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.ComposableArrows.twoδ₂Toδ₁.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g g_1 : j ⟶ k) (e_g : g = g_1)
  (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg),
  CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h = CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g_1 fg ⋯
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.coe_toMonoidHom : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) [inst_3 : IsDomain S] [inst_4 : Nontrivial R], ⇑abv.toMonoidHom = ⇑abv
-- Lean.DocString.Markdown
Lean.Doc.instToMarkdownBlockOfMarkdownInlineOfMarkdownBlock : {i : Type u_1} →
  {b : Type u_2} → [Lean.Doc.MarkdownInline i] → [Lean.Doc.MarkdownBlock i b] → Lean.Doc.ToMarkdown (Lean.Doc.Block i b)
-- Mathlib.RingTheory.TensorProduct.Basic
/-- If `M` is a representation of two different `R`-algebras `A` and `B` whose actions commute,
then it is a representation the `R`-algebra `A ⊗[R] B`.

An important example arises from a semiring `S`; allowing `S` to act on itself via left and right
multiplication, the roles of `R`, `A`, `B`, `M` are played by `ℕ`, `S`, `Sᵐᵒᵖ`, `S`. This example
is important because a submodule of `S` as a `Module` over `S ⊗[ℕ] Sᵐᵒᵖ` is a two-sided ideal.

NB: This is not an instance because in the case `B = A` and `M = A ⊗[R] A` we would have a diamond
of `smul` actions. Furthermore, this would not be a mere definitional diamond but a true
mathematical diamond in which `A ⊗[R] A` had two distinct scalar actions on itself: one from its
multiplication, and one from this would-be instance. Arguably we could live with this but in any
case the real fix is to address the ambiguity in notation, probably along the lines outlined here:
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234773.20base.20change/near/240929258
 -/
TensorProduct.Algebra.module : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {M : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : Semiring A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Module A M] →
                    [inst_6 : Module B M] →
                      [inst_7 : Algebra R A] →
                        [inst_8 : Algebra R B] →
                          [IsScalarTower R A M] →
                            [IsScalarTower R B M] → [SMulCommClass A B M] → Module (TensorProduct R A B) M
-- Mathlib.Analysis.CStarAlgebra.Unitization
ContinuousLinearMap.opNorm_mul_flip_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing E]
  [inst_2 : StarRing E] [NormedStarGroup E] [inst_4 : NormedSpace 𝕜 E] [inst_5 : IsScalarTower 𝕜 E E]
  [inst_6 : SMulCommClass 𝕜 E E] [RegularNormedAlgebra 𝕜 E] (a : E), ‖(ContinuousLinearMap.mul 𝕜 E).flip a‖ = ‖a‖
-- Mathlib.Analysis.Normed.Ring.Units
Units.add.eq_1 : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : HasSummableGeomSeries R] (x : Rˣ) (t : R) (h : ‖t‖ < ‖↑x⁻¹‖⁻¹),
  x.add t h = (x * Units.oneSub (-(↑x⁻¹ * t)) ⋯).copy (↑x + t) ⋯ ↑(x * Units.oneSub (-(↑x⁻¹ * t)) ⋯)⁻¹ ⋯
-- Mathlib.Order.SymmDiff
Disjoint.symmDiff_eq_sup : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → symmDiff a b = a ⊔ b
-- Mathlib.Algebra.Lie.Weights.IsSimple
/-- A Killing Lie algebra is simple if and only if its root system is irreducible.  -/
LieAlgebra.IsKilling.isSimple_iff_isIrreducible : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : FiniteDimensional K L] [inst_5 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L],
  (LieAlgebra.IsKilling.rootSystem H).IsIrreducible ↔ LieAlgebra.IsSimple K L
-- Mathlib.Data.Multiset.Replicate
Multiset.count_replicate_self : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (n : ℕ), Multiset.count a (Multiset.replicate n a) = n
-- Mathlib.Algebra.CharZero.Quotient
/-- `z • r` is a multiple of `p` iff `r` is `k * (p / z)` above a multiple of `p`, where
`0 ≤ k < |z|`.  -/
AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div : ∀ {R : Type u_1} [inst : DivisionRing R] [CharZero R] {p r : R} {z : ℤ},
  z ≠ 0 → (z • r ∈ AddSubgroup.zmultiples p ↔ ∃ k, r - ↑k • (p / ↑z) ∈ AddSubgroup.zmultiples p)
-- Mathlib.Topology.Maps.Strict.Module
/-- The product (in the sense of `LinearMap.prodMap`) of linear maps is strict if and only if both
maps are strict.  -/
LinearMap.isStrictMap_prodMap_iff : ∀ {R : Type u_1} {M : Type u_3} {Nₗ : Type u_5} {M' : Type u_6} {Nₗ' : Type u_7} [inst : Ring R]
  [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup Nₗ] [inst_3 : AddCommGroup M'] [inst_4 : AddCommGroup Nₗ']
  [inst_5 : Module R M] [inst_6 : Module R Nₗ] [inst_7 : Module R M'] [inst_8 : Module R Nₗ'] {fₗ : M →ₗ[R] Nₗ}
  {gₗ : M' →ₗ[R] Nₗ'} [inst_9 : TopologicalSpace M] [inst_10 : TopologicalSpace Nₗ] [IsTopologicalAddGroup M]
  [inst_12 : TopologicalSpace M'] [IsTopologicalAddGroup M'] [inst_14 : TopologicalSpace Nₗ'],
  Topology.IsStrictMap ⇑(fₗ.prodMap gₗ) ↔ Topology.IsStrictMap ⇑fₗ ∧ Topology.IsStrictMap ⇑gₗ
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_maxKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : Std.Internal.List.containsKey (Std.Internal.List.maxKey! l) l = true},
      Std.Internal.List.getKey (Std.Internal.List.maxKey! l) l he = Std.Internal.List.maxKey! l
-- Init.Data.Fin.Lemmas
/-- For rewriting in the reverse direction, see `Fin.cast_natAdd_right`.  -/
Fin.natAdd_cast : ∀ {n n' : ℕ} (m : ℕ) (i : Fin n') (h : n' = n), Fin.natAdd m (Fin.cast h i) = Fin.cast ⋯ (Fin.natAdd m i)
-- Mathlib.Order.Cofinal
isCofinal_iff_top_mem : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {s : Set α}, IsCofinal s ↔ ⊤ ∈ s
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  (Ideal.span {hζ.toInteger - 1}).LiesOver (Ideal.span {↑p})
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_nonpos : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
  [ClosedIciTopology E] {f : α → E}, f ≤ 0 → ∫ (x : α), f x ∂μ ≤ 0
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.smul_subset_of_set_mem_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {s t : Set α} {g : G},
  t ⊆ s → s ∈ MulAction.fixedBy (Set α) g → g • t ⊆ s
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.whisker_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.Cone.whisker E c).pt = c.pt
-- Lean.Environment
Lean.instInhabitedEnvExtension : {a : Type} → Inhabited (Lean.EnvExtension a)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.elabSimpConfigCore : Lean.Syntax →
  optParam Lean.Meta.Simp.Config { } →
    optParam Lean.Options ∅ → Lean.Elab.Tactic.TacticM Lean.Meta.Simp.ConfigWithOptions
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the forward direction of the isomorphism
`PreservesLimit₂.isoObjConePointsOfIsLimit` w.r.t. the canonical maps to the limit.  -/
CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit_hom_comp_π_assoc : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cone K₁}
  (hc₁ : CategoryTheory.Limits.IsLimit c₁) {c₂ : CategoryTheory.Limits.Cone K₂} (hc₂ : CategoryTheory.Limits.IsLimit c₂)
  {c₃ :
    CategoryTheory.Limits.Cone
      (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
  (hc₃ : CategoryTheory.Limits.IsLimit c₃) (j : J₁ × J₂) {Z : C}
  (h :
    (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)).obj j ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃).hom
      (CategoryTheory.CategoryStruct.comp (c₃.π.app j) h) =
    CategoryTheory.CategoryStruct.comp ((G.map (c₁.π.app j.1)).app c₂.pt)
      (CategoryTheory.CategoryStruct.comp ((G.obj (K₁.obj j.1)).map (c₂.π.app j.2)) h)
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.covariance_eval_multivariateGaussian : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ},
  S.PosSemidef →
    ∀ (i j : ι),
      ProbabilityTheory.covariance (fun x => x.ofLp i) (fun x => x.ofLp j)
          (ProbabilityTheory.multivariateGaussian μ S) =
        S i j
-- Init.Data.List.Range
List.range'_sublist_right : ∀ {step s m n : ℕ}, (List.range' s m step).Sublist (List.range' s n step) ↔ m ≤ n
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.restrictSupport.eq_1 : ∀ {σ : Type u} (R : Type v) [inst : CommSemiring R] (s : Set (σ →₀ ℕ)),
  MvPolynomial.restrictSupport R s = AddMonoidAlgebra.supported R R s
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.mk.inj : ∀ {toLocallyRingedSpace : AlgebraicGeometry.LocallyRingedSpace}
  {local_affine :
    ∀ (x : ↑toLocallyRingedSpace.toTopCat),
      ∃ U R,
        Nonempty (toLocallyRingedSpace.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))}
  {toLocallyRingedSpace_1 : AlgebraicGeometry.LocallyRingedSpace}
  {local_affine_1 :
    ∀ (x : ↑toLocallyRingedSpace_1.toTopCat),
      ∃ U R,
        Nonempty (toLocallyRingedSpace_1.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))},
  { toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine } =
      { toLocallyRingedSpace := toLocallyRingedSpace_1, local_affine := local_affine_1 } →
    toLocallyRingedSpace = toLocallyRingedSpace_1
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.isLinear : ∀ {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (fₗ : M →ₗ[R] M₂), IsLinearMap R ⇑fₗ
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_left_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.LaxLeftLinear C] {c c' : C} (f : c ⟶ c')
  (d : D) {Z : D'} (h : F.obj (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxLeftLinear.μₗ F c' d) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d)
      (CategoryTheory.CategoryStruct.comp
        (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d)) h)
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_neg : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R}, IsUnit A.det → ∀ (n : ℤ), A ^ (-n) = (A ^ n)⁻¹
-- Mathlib.Order.Ideal
Order.Ideal.le_toIdeal : ∀ {P : Type u_1} [inst : LE P] {I : Set P} (h : Order.IsIdeal I) {J : Order.Ideal P}, J ≤ h.toIdeal ↔ ↑J ⊆ I
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_inj : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {x y : AddMonoid.Coprod M N},
  (AddMonoid.Coprod.swap M N) x = (AddMonoid.Coprod.swap M N) y ↔ x = y
-- Mathlib.Data.Analysis.Topology
LocallyFinite.Realizer.mk.injEq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {F : Ctop.Realizer α} {f : β → Set α}
  (bas : (a : α) → { s // a ∈ F.F.f s }) (sets : (x : α) → Fintype ↑{i | (f i ∩ F.F.f ↑(bas x)).Nonempty})
  (bas_1 : (a : α) → { s // a ∈ F.F.f s }) (sets_1 : (x : α) → Fintype ↑{i | (f i ∩ F.F.f ↑(bas_1 x)).Nonempty}),
  ({ bas := bas, sets := sets } = { bas := bas_1, sets := sets_1 }) = (bas = bas_1 ∧ sets ≍ sets_1)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- `Rel` as a ring congruence, used to build the quotient.  -/
CliffordAlgebra.ringCon : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → RingCon (TensorAlgebra R M)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.trivial_mon_one : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.mk : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            (val : ι → S) →
              (σ' : S → MvPolynomial ι R) →
                (∀ (s : S), (MvPolynomial.aeval val) (σ' s) = s) →
                  (algebra : Algebra (MvPolynomial ι R) S) →
                    autoParam (algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval val))
                        Algebra.Generators.algebraMap_eq._autoParam →
                      Algebra.Generators R S ι
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A morphism which is a coequalizer for its kernel pair is a regular epi.  -/
CategoryTheory.regularEpiOfKernelPair : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B X : C} →
      (f : X ⟶ B) →
        [inst_1 : CategoryTheory.Limits.HasPullback f f] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯) → CategoryTheory.RegularEpi f
-- Mathlib.Tactic.Order.Preprocessing
/-- Preprocesses facts for linear orders. Replaces `x < y`, `¬ (x ≤ y)`, `¬ (x < y)`, and `x = y`
with equivalent facts involving only `≤` and `≠`. For each fact `x = y ⊔ z` adds `y ≤ x`
and `z ≤ x` facts, and similarly for `⊓`.  -/
Mathlib.Tactic.Order.preprocessFactsLinear : Array Mathlib.Tactic.Order.AtomicFact → Mathlib.Tactic.AtomM (Array Mathlib.Tactic.Order.AtomicFact)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : Option β → Option β},
  t.alter k f ≠ ∅ → ((t.alter k f).maxKey! = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true)
-- Mathlib.Algebra.Category.FGModuleCat.Limits
FGModuleCat.instCreatesLimitsOfShapeModuleCatForget₂LinearMapIdCarrierObjIsFG : {J : Type} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] →
      {k : Type u} →
        [inst_2 : Ring k] →
          [IsNoetherianRing k] →
            CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.invEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {X Y : C} (a : Y ⟶ X),
  CategoryTheory.Groupoid.invEquiv.symm a = CategoryTheory.Groupoid.inv a