mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order
nhds_nhdsAdjoint : ∀ {α : Type u} [inst : DecidableEq α] (a : α) (f : Filter α), nhds = Function.update pure a (pure a ⊔ f)
-- Init.Data.SInt.Lemmas
Int8.toInt_sub : ∀ (a b : Int8), (a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 8)
-- Mathlib.NumberTheory.NumberField.CMField
/-- The subgroup of `(𝓞 K)ˣ` generated by the units of `K⁺`. These units are exactly the units fixed
by the complex conjugation, see `IsCMField.unitsComplexConj_eq_self_iff`.
 -/
NumberField.IsCMField.realUnits : (K : Type u_1) → [inst : Field K] → Subgroup (NumberField.RingOfIntegers K)ˣ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.hasPullbackHorizPaste : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)],
  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g
-- Mathlib.GroupTheory.Nilpotent
/-- The lower central series of an additive subgroup `S` of `G`, computed in the ambient additive
group `G`.  -/
AddSubgroup.lowerCentralSeries : {G : Type u_2} → [inst : AddGroup G] → AddSubgroup G → ℕ → AddSubgroup G
-- Mathlib.Order.CompleteLattice.Basic
Equiv.iSup_congr : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : SupSet α] {f : ι → α} {g : ι' → α} (e : ι ≃ ι'),
  (∀ (x : ι), g (e x) = f x) → ⨆ x, f x = ⨆ y, g y
-- Mathlib.Algebra.Order.Group.PosPart
le_posPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] (a : α), a ≤ a⁺
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.priority? : Aesop.Frontend.RuleConfig → Option Aesop.Frontend.Priority
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.inclusion_comp_functorToCore : ∀ {G : Type u₂} [inst : CategoryTheory.Groupoid G],
  (CategoryTheory.Core.inclusion G).comp (CategoryTheory.Core.functorToCore (CategoryTheory.Functor.id G)) =
    CategoryTheory.Functor.id (CategoryTheory.Core G)
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The equivalence of quotients by powers of an integer induced by a group isomorphism.  -/
QuotientGroup.equivQuotientZPowOfEquiv : {A B : Type u} →
  [inst : CommGroup A] →
    [inst_1 : CommGroup B] → A ≃* B → (n : ℤ) → A ⧸ (zpowGroupHom n).range ≃* B ⧸ (zpowGroupHom n).range
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.deterministic.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f f_1 : α → β) (e_f : f = f_1)
  (hf : Measurable f), ProbabilityTheory.Kernel.deterministic f hf = ProbabilityTheory.Kernel.deterministic f_1 ⋯
-- Mathlib.Data.Int.Interval
Int.card_Ioo : ∀ (a b : ℤ), (Finset.Ioo a b).card = (b - a - 1).toNat
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.State.mk : Lean.Syntax.Traverser → String → Bool → Bool → Bool → Array Std.Format → Lean.PrettyPrinter.Formatter.State
-- Mathlib.Algebra.MvPolynomial.Comap
MvPolynomial.comap_comp : ∀ {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} [inst : CommSemiring R]
  (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R),
  MvPolynomial.comap (g.comp f) = MvPolynomial.comap f ∘ MvPolynomial.comap g
-- Init.Data.UInt.Bitwise
USize.toUInt16_and : ∀ (a b : USize), (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E}
  {f g : E → β}, StrictConvexOn 𝕜 s f → Set.EqOn f g s → StrictConvexOn 𝕜 s g
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.postcomp₂_naturality_hom_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) {a_1 b_1 : Bᵒᵖ} (g : a_1 ⟶ b_1)
  (X : ↑(CategoryTheory.Cat.of (Opposite.unop a_1 ⟶ a))),
  ((CategoryTheory.Bicategory.postcomp₂ f).naturality g).hom.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator g.unop X f).hom
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} [inst_2 : SizeOf C] [inst_3 : SizeOf J] (diag : CategoryTheory.Functor J C)
  (π : (CategoryTheory.Functor.const J).obj X ⟶ diag) (isLimit : CategoryTheory.Limits.IsLimit { pt := X, π := π }),
  sizeOf { diag := diag, π := π, isLimit := isLimit } = 1 + sizeOf diag + sizeOf π + sizeOf isLimit
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.mkIndFVar2Const : Array Lean.Elab.Command.InductiveView → Array Lean.Expr → List Lean.Name → Lean.ExprMap Lean.Expr
-- Init.Data.Int.LemmasAux
Int.instAssociativeMax : Std.Associative max
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
CategoryTheory.Limits.SequentialProduct.functorMap_commSq : ∀ {C : Type u_1} {M N : ℕ → C} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n)
  [inst_1 : CategoryTheory.Limits.HasCountableProducts C] {n m : ℕ} (h : ¬m < n),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.ofOpSequence (CategoryTheory.Limits.SequentialProduct.functorMap f)).map
        (CategoryTheory.homOfLE ⋯).op)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) m)
        (CategoryTheory.eqToHom ⋯)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => if x : i < m + 1 then M i else N i) m)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (f m))
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- A morphism of presheaves of modules is locally injective
if the underlying morphism of presheaves of abelian groups is.  -/
PresheafOfModules.IsLocallyInjective : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.GrothendieckTopology C →
      {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M₁ M₂ : PresheafOfModules R} → (M₁ ⟶ M₂) → Prop
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Strand.mk : ℕ →
  Mathlib.Tactic.Widget.StringDiagram.Node →
    Mathlib.Tactic.Widget.StringDiagram.Node →
      Mathlib.Tactic.BicategoryLike.Atom₁ → Mathlib.Tactic.Widget.StringDiagram.Strand
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.H1Cotangent.map_toExtendScalars_injective : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), Function.Injective ⇑(Algebra.Extension.H1Cotangent.map P.toExtendScalars)
-- Mathlib.Order.WithBot
WithBot.distribLattice : {α : Type u_1} → [DistribLattice α] → DistribLattice (WithBot α)
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.F_differentiableAt_of_ne : ∀ {N : ℕ} [inst : NeZero N] (B : DirichletCharacter.BadChar✝ N) {s : ℂ},
  s ≠ 1 → DifferentiableAt ℂ (DirichletCharacter.BadChar.F✝ B) s
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.coeFn_toL1 : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β} (hf : MeasureTheory.Integrable f μ), ↑↑(MeasureTheory.Integrable.toL1 f hf) =ᵐ[μ] f
-- Mathlib.Order.Hom.WithTopBot
SupHom.withTop'_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] [inst_2 : OrderTop β]
  (f : SupHom α β) (a : WithTop α), f.withTop' a = Option.elim a ⊤ ⇑f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α},
  t.contains a = true → t.getKey? a = some (t.getKeyD a fallback)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.unop_i₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Cᵒᵖ} (P : HomotopicalAlgebra.PrepathObject A),
  P.unop.i₀ = P.p₀.unop
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
/-- The braiding is symmetric.  -/
TensorProduct.gradedComm_symm : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)],
  (TensorProduct.gradedComm R 𝒜 ℬ).symm = TensorProduct.gradedComm R ℬ 𝒜
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signAux2.eq_2 : ∀ {α : Type u} [inst : DecidableEq α] (x : Equiv.Perm α) (x_2 : α) (l : List α),
  Equiv.Perm.signAux2 (x_2 :: l) x =
    if x_2 = x x_2 then Equiv.Perm.signAux2 l x else -Equiv.Perm.signAux2 l (Equiv.swap x_2 (x x_2) * x)
-- Init.Sym.Lemmas
Lean.Sym.or_eq_true_left : ∀ (a b : Prop), a = True → (a ∨ b) = True
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Ico_eq_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a < b → b < c → Set.Ioc a b ∪ Set.Ico b c = Set.Ioo a c
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
/-- An anti-equivalence between the categories of triangles in `C` and in `Cᵒᵖ`.
A triangle in `Cᵒᵖ` shall be distinguished iff it corresponds to a distinguished
triangle in `C` via this equivalence.  -/
CategoryTheory.Pretriangulated.triangleOpEquivalence : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ ≌ CategoryTheory.Pretriangulated.Triangle Cᵒᵖ
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- Characterization of differentiable sections of a vector bundle at a point within a set
in terms of the preferred trivialization at that point.  -/
mdifferentiableAt_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB)
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] (s : (b : B) → E b) {b₀ : B},
  MDiffAt (T% s) b₀ ↔ (MDiffAt fun b => (↑(trivializationAt F E b₀) ⟨b, s b⟩).2) b₀
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_le_cancel : ∀ {ctx : Nat.Internal.Linear.Context} {m₁ m₂ : Nat.Internal.Linear.Poly},
  Nat.Internal.Linear.Poly.denote_le ctx (m₁, m₂) → Nat.Internal.Linear.Poly.denote_le ctx (m₁.cancel m₂)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Iic : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : Preorder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {b : ι → α},
  Filter.Tendsto b l Filter.atTop → MeasureTheory.AECover μ l fun i => Set.Iic (b i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_filter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter! f t).getKey? k =
    (t.getKey? k).pfilter fun x h' => f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯)
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.IsMulRightInvariant.toSMulInvariantMeasure_op : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : Mul G] [μ.IsMulRightInvariant],
  MeasureTheory.SMulInvariantMeasure Gᵐᵒᵖ G μ
-- Lean.Parser.Term
Lean.Parser.Term.matchExprElseAlt.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.minKey!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minKey! = t₂.minKey!
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
/-- Precompose an open partial homeomorphism with a homeomorphism.
We modify the source and target to have better definitional behavior.  -/
Homeomorph.transOpenPartialHomeomorph : {X : Type u_1} →
  {Y : Type u_3} →
    {Z : Type u_5} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] → X ≃ₜ Y → OpenPartialHomeomorph Y Z → OpenPartialHomeomorph X Z
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.mk.injEq : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (var : relations.G → M)
  (linearCombination_var_relation : ∀ (r : relations.R), (Finsupp.linearCombination A var) (relations.relation r) = 0)
  (var_1 : relations.G → M)
  (linearCombination_var_relation_1 :
    ∀ (r : relations.R), (Finsupp.linearCombination A var_1) (relations.relation r) = 0),
  ({ var := var, linearCombination_var_relation := linearCombination_var_relation } =
      { var := var_1, linearCombination_var_relation := linearCombination_var_relation_1 }) =
    (var = var_1)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_symm_apply_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C)
  (t : CategoryTheory.Limits.FormalCoproduct C) (s : (i : 𝒜) → f i ⟶ t)
  (p : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt.I),
  ((CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv 𝒜 f t).symm s).φ p = (s p.fst).φ p.snd
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.filterMap_eq_empty_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ},
  Std.ExtHashMap.filterMap f m = ∅ ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) m[k] = none
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.hurwitzEvenFEPair_neg : ∀ (a : UnitAddCircle), HurwitzZeta.hurwitzEvenFEPair (-a) = HurwitzZeta.hurwitzEvenFEPair a
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instNeg : {ι : Type u_1} → {G : ι → Type u_4} → [(i : ι) → Neg (G i)] → Neg ((i : ι) → G i)
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Finset.insert_eq_cons : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α) (h : a ∉ s), insert a s = Finset.cons a s h
-- Init.Grind.Offset
Lean.Grind.Nat.lo_le : ∀ (u w v k : ℕ), u + k ≤ w → w ≤ v → u + k ≤ v
-- Init.Data.Int.Lemmas
Int.mul_ne_zero : ∀ {a b : ℤ}, a ≠ 0 → b ≠ 0 → a * b ≠ 0
-- Mathlib.Data.Rat.BigOperators
Rat.cast_multiset_prod : ∀ {α : Type u_2} [inst : Field α] [CharZero α] (s : Multiset ℚ), ↑s.prod = (Multiset.map Rat.cast s).prod
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (m.insertMany l).getKey? k' = some k
-- Lean.Util.ForEachExpr
/-- Apply `f` to each sub-expression of `e`. If `f t` returns false, then t's children are not visited.  -/
Lean.Expr.forEach' : {ω : Type} →
  {m : Type → Type} → [STWorld ω m] → [MonadLiftT (ST ω) m] → [Monad m] → Lean.Expr → (Lean.Expr → m Bool) → m Unit
-- Mathlib.FieldTheory.Fixed
FixedPoints.minpoly.ne_one : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [inst_3 : Fintype G]
  (x : F), FixedPoints.minpoly G F x ≠ 1
-- Mathlib.Algebra.Group.Defs
/-- An additive monoid is Dedekind-finite if every left inverse is also a right inverse.
Also called von Neumann-finite or directly finite.  -/
IsDedekindFiniteAddMonoid : (M : Type u_2) → [AddZero M] → Prop
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.mk.inj : ∀ {G : Type u_1} {H : Type u_2} {inst : Add G} {inst_1 : Add H} {a : G} {b : H} {toFun : G → H}
  {map_add_const' : ∀ (x : G), toFun (x + a) = toFun x + b} {toFun_1 : G → H}
  {map_add_const'_1 : ∀ (x : G), toFun_1 (x + a) = toFun_1 x + b},
  { toFun := toFun, map_add_const' := map_add_const' } = { toFun := toFun_1, map_add_const' := map_add_const'_1 } →
    toFun = toFun_1
-- Mathlib.Tactic.ClickSuggestions.FindPremises
Mathlib.Tactic.ClickSuggestions.Choice.mk : Bool → Bool → Bool → Bool → Mathlib.Tactic.ClickSuggestions.Choice
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.instInhabitedCode.default : Lean.Elab.Term.Do.Code
-- Mathlib.RepresentationTheory.Intertwining
/-- The product of two intertwining maps is an intertwining map.  -/
Representation.IntertwiningMap.prod : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        {U : Type u_5} →
          [inst : Semiring A] →
            [inst_1 : Monoid G] →
              [inst_2 : AddCommMonoid V] →
                [inst_3 : AddCommMonoid W] →
                  [inst_4 : AddCommMonoid U] →
                    [inst_5 : Module A V] →
                      [inst_6 : Module A W] →
                        [inst_7 : Module A U] →
                          {ρ : Representation A G V} →
                            {σ : Representation A G W} →
                              {τ : Representation A G U} →
                                ρ.IntertwiningMap σ → ρ.IntertwiningMap τ → ρ.IntertwiningMap (σ.prod τ)
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  matPolyEquiv =
    ((matrixEquivTensor n R (Polynomial R)).trans (Algebra.TensorProduct.comm R (Polynomial R) (Matrix n n R))).trans
      (polyEquivTensor R (Matrix n n R)).symm
-- Mathlib.Topology.Connected.Basic
Subtype.preconnectedSpace : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsPreconnected s → PreconnectedSpace ↑s
-- Mathlib.Algebra.MonoidAlgebra.Lift
AddMonoidAlgebra.liftNCRingHom_single : ∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : AddMonoid G] [inst_2 : Semiring R]
  (f : k →+* R) (g : Multiplicative G →* R) (h_comm : ∀ (x : k) (y : Multiplicative G), Commute (f x) (g y)) (a : G)
  (b : k), (AddMonoidAlgebra.liftNCRingHom f g h_comm) (AddMonoidAlgebra.single a b) = f b * g (Multiplicative.ofAdd a)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_add_measure : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {ν : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure ν] {f : α → E},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable f ν →
      ⨍ (x : α), f x ∂(μ + ν) =
        (μ.real Set.univ / (μ.real Set.univ + ν.real Set.univ)) • ⨍ (x : α), f x ∂μ +
          (ν.real Set.univ / (μ.real Set.univ + ν.real Set.univ)) • ⨍ (x : α), f x ∂ν
-- Mathlib.Algebra.Group.Defs
zpow_ofNat : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a : G) (n : ℕ), a ^ OfNat.ofNat n = a ^ OfNat.ofNat n
-- Std.Http.Data.Chunk
Std.Http.Chunk.ExtensionValue.instInhabited : Inhabited Std.Http.Chunk.ExtensionValue
-- Mathlib.Topology.EMetricSpace.Basic
Metric.eball.eq_1 : ∀ {α : Type u} [inst : EDist α] (x : α) (ε : ENNReal), Metric.eball x ε = {y | edist y x < ε}
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- Witness that the limit cone in `ModuleCat R` is a limit cone.
(Internal use only; use the limits API.)
 -/
ModuleCat.HasLimits.limitConeIsLimit : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          [inst_2 : Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] →
            CategoryTheory.Limits.IsLimit (ModuleCat.HasLimits.limitCone F)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_eq_aleph_natCast : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.lift.{v, u} c = Cardinal.aleph ↑n ↔ c = Cardinal.aleph ↑n
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.isCycle_cycleOf : ∀ {α : Type u_2} {x : α} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle], f x ≠ x → (f.cycleOf x).IsCycle
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- Suppose a set of vectors spans `V`.  Then a point `p`, together with those vectors added to `p`,
spans `P`.  -/
affineSpan_singleton_union_vadd_eq_top_of_span_eq_top : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set V} (p : P),
  Submodule.span k (Set.range Subtype.val) = ⊤ → affineSpan k ({p} ∪ (fun v => v +ᵥ p) '' s) = ⊤
-- Mathlib.Data.PNat.Defs
/-- `mod_div m k = (m % k, m / k)`.
We define `m % k` and `m / k` in the same way as for `ℕ`
except that when `m = n * k` we take `m % k = k` and
`m / k = n - 1`.  This ensures that `m % k` is always positive
and `m = (m % k) + k * (m / k)` in all cases.  Later we
define a function `div_exact` which gives the usual `m / k`
in the case where `k` divides `m`.
 -/
PNat.modDiv : ℕ+ → ℕ+ → ℕ+ × ℕ
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.isUnitTrinomial_iff' : ∀ {p : Polynomial ℤ},
  p.IsUnitTrinomial ↔ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3
-- Mathlib.Algebra.Group.Action.Sum
Sum.FaithfulVAddRight : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β] [FaithfulVAdd M β],
  FaithfulVAdd M (α ⊕ β)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.smul_domain : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {M : Type u_7}
  [inst_6 : Monoid M] [inst_7 : DistribMulAction M F] [inst_8 : SMulCommClass S M F] (a : M) (f : E →ₛₗ.[σ] F),
  (a • f).domain = f.domain
-- Mathlib.Data.Finset.Dedup
/-- `toFinset s` removes duplicates from the multiset `s` to produce a finset.  -/
Multiset.toFinset : {α : Type u_1} → [DecidableEq α] → Multiset α → Finset α
-- Batteries.Data.String.Matcher
/-- Returns the first substring of `s` that matches `pattern`,
or `none` if there is no such substring.
 -/
Substring.Raw.findSubstr? : Substring.Raw → Substring.Raw → Option Substring.Raw
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.isSFiniteKernel_prodMkRight_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [Nonempty γ] {κ : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.prodMkRight γ κ) ↔ ProbabilityTheory.IsSFiniteKernel κ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a fallback : α} {v : β k},
      (m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.ext'_iff : ∀ {α : Type u} [inst : Group α] {f g : GroupTopology α}, f = g ↔ TopologicalSpace.IsOpen = TopologicalSpace.IsOpen