mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.preservesKernel_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (X Y : C) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair 0 0) G
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_self_pos : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R]
  [AddLeftStrictMono R] [AddLeftReflectLT R] {a : R}, 0 < a * a ↔ a ≠ 0
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.isClosedMap_coe : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {H : Subgroup G},
  IsCompact ↑H → IsClosedMap QuotientGroup.mk
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
GromovHausdorff.instMetricSpaceOptimalGHCoupling : (X : Type u_1) →
  (Y : Type u_2) →
    [inst : MetricSpace X] →
      [inst_1 : CompactSpace X] →
        [inst_2 : Nonempty X] →
          [inst_3 : MetricSpace Y] →
            [inst_4 : CompactSpace Y] → [inst_5 : Nonempty Y] → MetricSpace (GromovHausdorff.OptimalGHCoupling X Y)
-- Init.Data.UInt.Bitwise
UInt64.toUInt32_xor : ∀ (a b : UInt64), (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32
-- Mathlib.Order.Category.Frm
Frm.ofHom_comp : ∀ {X Y Z : Type u} [inst : Order.Frame X] [inst_1 : Order.Frame Y] [inst_2 : Order.Frame Z] (f : FrameHom X Y)
  (g : FrameHom Y Z), Frm.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (Frm.ofHom f) (Frm.ofHom g)
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_aux.coe_fwdDiffₗ : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M),
  ⇑(fwdDiff_aux.fwdDiffₗ M G h) = fwdDiff h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.maxKeyD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {fallback : α}, t₁.maxKeyD fallback = t₂.maxKeyD fallback
-- Mathlib.Data.Finset.Image
Finset.image_eq_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α}, Finset.image f s = ∅ ↔ s = ∅
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.lift_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C),
  ((P.lift F hF).obj X).obj = F.obj X
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Result.elimApp : Lean.Elab.Tactic.ElimApp.Result → Lean.Expr
-- Lean.Parser.Basic
/-- Parses the whitespace after the `\` when there is a string gap.
Raises an error if the whitespace does not contain exactly one newline character.
 -/
Lean.Parser.stringGapFn : Bool → Lean.Parser.ParserFn
-- Batteries.Recycling.RBTree.Alter
/-- Descend into the right subtree of a red node.  -/
RBTree.RBNode.Path.Balanced.redR : ∀ {c₀ : RBTree.RBColor} {n₀ : ℕ} {α : Type u_1} {x : RBTree.RBNode α} {n : ℕ} {v : α} {parent : RBTree.RBNode.Path α},
  x.Balanced RBTree.RBColor.black n →
    RBTree.RBNode.Path.Balanced c₀ n₀ parent RBTree.RBColor.red n →
      RBTree.RBNode.Path.Balanced c₀ n₀ (RBTree.RBNode.Path.right RBTree.RBColor.red x v parent) RBTree.RBColor.black n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k}, (compare k ((Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKey ⋯)).isLE = true
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.coe_zpow : ∀ {K : Type u_1} [inst : Field K] (x : (NumberField.RingOfIntegers K)ˣ) (n : ℤ),
  (algebraMap (NumberField.RingOfIntegers K) K) ↑(x ^ n) = (algebraMap (NumberField.RingOfIntegers K) K) ↑x ^ n
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.sub_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄), (h.sub h').h₃ = h.h₃ - h'.h₃
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_compContinuous : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] (f : BoundedContinuousFunction α β) (g : C(δ, α)), ⇑(f.compContinuous g) = ⇑f ∘ ⇑g
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.all_iff : ∀ {α : Type u_1} {p : α → Bool} {t : RBTree.RBNode α},
  RBTree.RBNode.all p t = true ↔ RBTree.RBNode.All (fun x => p x = true) t
-- Mathlib.LinearAlgebra.Ray
exists_pos_right_iff_sameRay : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x y : M}, x ≠ 0 → y ≠ 0 → ((∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y)
-- Mathlib.Data.List.Sigma
List.dedupKeys.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α],
  List.dedupKeys = List.foldr (fun x => List.kinsert x.fst x.snd) []
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- `F : D ⥤ K ⥤ C` preserves all limits if it does for each `k : K`.  -/
CategoryTheory.Limits.preservesLimits_of_evaluation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor K C)),
  (∀ (k : K),
      CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v', v, u', u}
        (F.comp ((CategoryTheory.evaluation K C).obj k))) →
    CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v', max u₂ v, u', max (max (max u u₂) v) v₂} F
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Injective.State.mk.inj : ∀ {thms : Lean.Meta.Grind.InjectiveTheoremsArray}
  {fns : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.InjectiveInfo}
  {thms_1 : Lean.Meta.Grind.InjectiveTheoremsArray}
  {fns_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.InjectiveInfo},
  { thms := thms, fns := fns } = { thms := thms_1, fns := fns_1 } → thms = thms_1 ∧ fns = fns_1
-- Mathlib.Analysis.Normed.Module.Complemented
Submodule.coe_prodEquivOfClosedCompl : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {p q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed ↑p)
  (hq : IsClosed ↑q), ⇑(Submodule.prodEquivOfClosedCompl p q h hp hq) = ⇑(Submodule.prodEquivOfIsCompl p q h)
-- Mathlib.CategoryTheory.Preadditive.Opposite
_private.Mathlib.CategoryTheory.Preadditive.Opposite.0.CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite.match_1.eq_1 : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (G : C) (motive : (CategoryTheory.End G)ᵐᵒᵖ → Sort u_3)
  (f : CategoryTheory.End G) (h_1 : (f : CategoryTheory.End G) → motive { unop' := f }),
  (match { unop' := f } with
    | { unop' := f } => h_1 f) =
    h_1 f
-- Mathlib.GroupTheory.Coprod.Basic
/-- The natural embedding `N →+ AddMonoid.Coprod M N`.  -/
AddMonoid.Coprod.inr : {M : Type u_1} → {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → N →+ AddMonoid.Coprod M N
-- Mathlib.Algebra.BigOperators.Finprod
/-- See also `Finset.sum_bij`.  -/
finsum_mem_eq_of_bijOn : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {s : Set α} {t : Set β} {f : α → M} {g : β → M}
  (e : α → β), Set.BijOn e s t → (∀ x ∈ s, f x = g (e x)) → ∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ᶠ (j : β) (_ : j ∈ t), g j
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsCocartesian.fac : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCocartesian f φ] {b' : 𝒳}
  (φ' : a ⟶ b') [inst_3 : p.IsHomLift f φ'],
  CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Functor.IsCocartesian.map p f φ φ') = φ'
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selRightfAction_actionAssocIso_hom : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C),
  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x y z).hom =
    (CategoryTheory.MonoidalCategoryStruct.associator x y z).inv
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.compHom'_apply_apply : ∀ {M : Type uM} {N : Type uN} {P : Type uP} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : CommMonoid P]
  (f : M →* N) (y : N →* P) (x : M), (f.compHom' y) x = y (f x)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.abs_tprod : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommRing α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : ι → α}, Multipliable f → |∏' (i : ι), f i| = ∏' (i : ι), |f i|
-- Mathlib.FieldTheory.SeparableClosure
/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the image of `separableClosure F E`
under the map `i` is contained in `separableClosure F K`.  -/
separableClosure.map_le_of_algHom : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E →ₐ[F] K), IntermediateField.map i (separableClosure F E) ≤ separableClosure F K
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Real.borel_eq_generateFrom_Ici_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ a, {Set.Ici ↑a})
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.rel₁_of_memoizedLeft : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Std.Iterators.Finite α₁ m] [inst_3 : Std.Iterators.Productive α₂ m] {left : Std.IterM m β₁}
  {b' b : Option { out // ∃ it, it.IsPlausibleOutput out }} {right' right : Std.IterM m β₂},
  Option.lt emptyRelation b' b →
    Std.Iterators.Types.Zip.Rel₁ m { internalState := { left := left, memoizedLeft := b', right := right' } }
      { internalState := { left := left, memoizedLeft := b, right := right } }
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_f : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfRight 𝒰 f g).f i =
    CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp (𝒰.f i) g) f g
      (CategoryTheory.CategoryStruct.id X) (𝒰.f i) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_sub_fun_sub : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y Z T : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      MeasureTheory.MemLp Z 2 μ →
        MeasureTheory.MemLp T 2 μ →
          ProbabilityTheory.covariance (fun ω => X ω - Y ω) (fun ω => Z ω - T ω) μ =
            ProbabilityTheory.covariance X Z μ - ProbabilityTheory.covariance X T μ -
                ProbabilityTheory.covariance Y Z μ +
              ProbabilityTheory.covariance Y T μ
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_exp_mul_complex_Iic : ∀ {a : ℂ}, 0 < a.re → ∀ (c : ℝ), ∫ (x : ℝ) in Set.Iic c, Complex.exp (a * ↑x) = Complex.exp (a * ↑c) / a
-- Mathlib.Order.CompleteLattice.Basic
Monotone.iInf_comp_eq : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] [inst_1 : Preorder β] {f : β → α},
  Monotone f → ∀ {s : ι → β}, (∀ (x : β), ∃ i, s i ≤ x) → ⨅ x, f (s x) = ⨅ y, f y
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_cos_add_sin_mul_I_sub : ∀ (θ : ℝ), (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I).arg - θ = 2 * Real.pi * ↑⌊(Real.pi - θ) / (2 * Real.pi)⌋
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
Subsemigroup.closureCommSemigroupOfComm.eq_1 : ∀ (M : Type u_1) [inst : Semigroup M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a),
  Subsemigroup.closureCommSemigroupOfComm M hcomm = inferInstance
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_whiskerLeft_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.LaxFunctor B C} (η : x ⟶ x_1) (x_3 x_4 : x_1 ⟶ x_2) (Γ : x_3 ⟶ x_4) (a : B),
  (CategoryTheory.Bicategory.whiskerLeft η Γ).as.app a = CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.as.app a)
-- Mathlib.LinearAlgebra.Dual.BaseChange
IsBaseChange.dual : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] {A : Type u_4} [inst_5 : CommSemiring A] [inst_6 : Algebra R A]
  [inst_7 : Module A W] [inst_8 : IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j) [Module.Free R V]
  [Module.Finite R V], IsBaseChange A ibc.toDual
-- Mathlib.GroupTheory.GroupAction.Basic
/-- If the stabilizer of `a` is `S`, then the stabilizer of `g • a` is `gSg⁻¹`.  -/
MulAction.stabilizer_smul_eq_stabilizer_map_conj : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g : G) (a : α),
  MulAction.stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (MulAction.stabilizer G a)
-- Mathlib.RingTheory.IntegralDomain
Fintype.bijInv.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] {inst_1 : DecidableEq β} [inst_2 : DecidableEq β] {f f_1 : α → β}
  (e_f : f = f_1) (f_bij : Function.Bijective f) (b b_1 : β), b = b_1 → Fintype.bijInv f_bij b = Fintype.bijInv ⋯ b_1
-- Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
aemeasurable_withDensity_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E] [inst_3 : MeasurableSpace E] [BorelSpace E] {f : α → NNReal},
  Measurable f → ∀ {g : α → E}, AEMeasurable g (μ.withDensity fun x => ↑(f x)) ↔ AEMeasurable (fun x => ↑(f x) • g x) μ
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.injective : ∀ {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₂] (e : A₁ ≃ₐ[R] A₂), Function.Injective ⇑e
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The preimage of a subsemigroup along a semigroup homomorphism is a subsemigroup.  -/
Subsemigroup.comap : {M : Type u_1} → {N : Type u_2} → [inst : Mul M] → [inst_1 : Mul N] → (M →ₙ* N) → Subsemigroup N → Subsemigroup M
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.map_sub : ∀ {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : PartialOrder Γ] [inst_1 : AddGroup R] [inst_2 : AddGroup S]
  (f : R →+ S) {x y : HahnSeries Γ R}, (x - y).map f = x.map f - y.map f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.keys.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → t.keys = t_1.keys
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- We have `[0, W] = 0` for all vector fields `W`: this depends on the junk value 0
if `W` is not differentiable. Version within a set.  -/
VectorField.mlieBracketWithin_zero_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {W : (x : M) → TangentSpace I x},
  VectorField.mlieBracketWithin I 0 W s = 0
-- Mathlib.MeasureTheory.Constructions.Pi
/-- We intentionally restrict this only to the nondependent function space, since
type-class inference cannot find an instance for `ι → ℝ` when this is stated for dependent function
spaces.  -/
MeasureTheory.Pi.isAddLeftInvariant_volume : ∀ {ι : Type u_1} [inst : Fintype ι] {α : Type u_4} [inst_1 : AddGroup α] [inst_2 : MeasureTheory.MeasureSpace α]
  [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasurableAdd α] [MeasureTheory.volume.IsAddLeftInvariant],
  MeasureTheory.volume.IsAddLeftInvariant
-- Mathlib.Data.Sym.Card
/-- The *stars and bars* lemma: the cardinality of `Sym α k` is equal to
`Nat.choose (card α + k - 1) k`.  -/
Sym.card_sym_eq_choose : ∀ {α : Type u_2} [inst : Fintype α] (k : ℕ) [inst_1 : Fintype (Sym α k)],
  Fintype.card (Sym α k) = (Fintype.card α + k - 1).choose k
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_sq_eq_abs : ∀ (x : ℝ), √(x ^ 2) = |x|
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_inter_eq_size_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (∀ a ∈ m₂, a ∈ m₁) → (m₁ ∩ m₂).size = m₂.size
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.instMin.eq_1 : ∀ {M : Type u_1} [inst : Mul M], Subsemigroup.instMin = { min := fun S₁ S₂ => { carrier := ↑S₁ ∩ ↑S₂, mul_mem' := ⋯ } }
-- Mathlib.Logic.Equiv.Prod
Equiv.sigmaPUnit_symm_apply_fst : ∀ (α : Type u_9) (a : α), ((Equiv.sigmaPUnit α).symm a).fst = a
-- Init.Data.Nat.Basic
Nat.beq.eq_2 : ∀ (n : ℕ), Nat.zero.beq n.succ = false
-- Mathlib.CategoryTheory.Limits.FullSubcategory
CategoryTheory.Limits.hasColimit_of_closedUnderColimits : ∀ (J : Type w) [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderColimitsOfShape J]
  (F : CategoryTheory.Functor J P.FullSubcategory) [CategoryTheory.Limits.HasColimit (F.comp P.ι)],
  CategoryTheory.Limits.HasColimit F
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- Every semilinear map between two topological modules, where the source has the module
topology, is continuous.  -/
IsModuleTopology.continuous_of_distribMulActionHomₑ : ∀ {R : Type u_1} {S : Type u_2} [τR : TopologicalSpace R] [τS : TopologicalSpace S] [inst : Semiring R]
  [inst_1 : Semiring S] {A : Type u_3} [inst_2 : AddCommMonoid A] [inst_3 : Module R A] [aA : TopologicalSpace A]
  [IsModuleTopology R A] {B' : Type u_5} [inst_5 : AddCommMonoid B'] [inst_6 : Module S B'] [aB' : TopologicalSpace B']
  [ContinuousAdd B'] [ContinuousSMul S B'] {σ : R →* S}, Continuous ⇑σ → ∀ (φ : A →ₑ+[σ] B'), Continuous ⇑φ
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.sum_mult_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], ∑ w, w.mult = Module.finrank ℚ K
-- Mathlib.Data.Num.ZNum
ZNum.of_to_int' : ∀ (n : ZNum), ZNum.ofInt' ↑n = n
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The functor sending an arrow to its source.  -/
CategoryTheory.Arrow.leftFunc : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.Arrow C) C
-- Mathlib.Dynamics.Flow
/-- The composition of semiconjugacies is a semiconjugacy.  -/
Flow.IsSemiconjugacy.comp : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) {β : Type u_3} {γ : Type u_4} [inst_3 : TopologicalSpace β] [inst_4 : TopologicalSpace γ]
  (ψ : Flow τ β) (χ : Flow τ γ) {π : α → β} {ρ : β → γ},
  Flow.IsSemiconjugacy π ϕ ψ → Flow.IsSemiconjugacy ρ ψ χ → Flow.IsSemiconjugacy (ρ ∘ π) ϕ χ
-- Init.Data.Int.DivMod.Lemmas
Int.mul_add_ediv_right : ∀ (a c : ℤ) {b : ℤ}, b ≠ 0 → (a * b + c) / b = a + c / b
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.associatorImpl_inv_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C),
  (X.associatorImpl Y Z).inv.F =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst))
      (CategoryTheory.Limits.prod.lift
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd
          (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd))
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- The colimit cofork exhibiting the natural transformation
`toπ₀NatTrans : SSet.evaluation.obj (op ⦋0⦌) ⟶ π₀Functor`
as a coequalizer of the two face maps, considered as
natural transformations of functors `SSet.{u} ⥤ Type u`.  -/
SSet.coforkπ₀Functor : CategoryTheory.Limits.Cofork (SSet.evaluation.map (SimplexCategory.δ 1).op)
  (SSet.evaluation.map (SimplexCategory.δ 0).op)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.lift_f_snd_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cocycle K F 1) (β : CochainComplex.HomComplex.Cochain K G 0)
  (eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0) (p q : ℤ)
  (hpq : p + 0 = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.lift φ α β eq).f p)
      ((CochainComplex.mappingCone.snd φ).v p q hpq) =
    β.v p q hpq
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.mk'.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (f : M ≃ₜ N) (h : ∀ (x y : M), f (x + y) = f x + f y),
  ContinuousAddEquiv.mk' f h = { toEquiv := f.toEquiv, map_add' := h, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.WithConv
instNonUnitalNonAssocSemiringWithConvMatrix : {m : Type u_1} →
  {n : Type u_2} → {α : Type u_3} → [NonUnitalNonAssocSemiring α] → NonUnitalNonAssocSemiring (WithConv (Matrix m n α))
-- Lean.Elab.MutualDef
Lean.Elab.DefViewElabHeader.toDefView : Lean.Elab.DefViewElabHeader → Lean.Elab.DefView
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- A set is **3GP-free** if it does not contain any non-trivial geometric progression of length
three.  -/
ThreeGPFree : {α : Type u_2} → [Monoid α] → Set α → Prop
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
Commute.add_pow_dvd_pow_of_pow_eq_zero_left : ∀ {R : Type u_1} {x y : R} {n m p : ℕ} [inst : Ring R], n + m ≤ p + 1 → Commute x y → y ^ n = 0 → (x + y) ^ m ∣ x ^ p
-- Mathlib.Order.Interval.Set.Monotone
MonotoneOn.Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β} {s : Set α},
  MonotoneOn f s → AntitoneOn g s → AntitoneOn (fun x => Set.Ioo (f x) (g x)) s
-- Mathlib.Data.Sum.Order
Sum.Lex.not_inr_le_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a : α} {b : β}, ¬toLex (Sum.inr b) ≤ toLex (Sum.inl a)
-- Mathlib.Algebra.Category.ModuleCat.Abelian
/-- Add this instance to help Lean with universe levels.  -/
ModuleCat.instHasLimitsOfSize : ∀ {R : Type u} [inst : Ring R],
  CategoryTheory.Limits.HasLimitsOfSize.{v, v, max v w, max (max (v + 1) (w + 1)) u} (ModuleCat R)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.summandAction : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      [DecidableEq ι] → [(i : ι) → DecidableEq (M i)] → (i : ι) → MulAction (M i) (Monoid.CoprodI.Word M)