mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.CostructuredArrow.hasFiniteColimits : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.HasFiniteColimits A]
  [CategoryTheory.Limits.PreservesFiniteColimits G],
  CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.CostructuredArrow G X)
-- Mathlib.Algebra.Group.Units.Basic
instUniqueAddUnitsOfSubsingleton.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : Subsingleton M],
  instUniqueAddUnitsOfSubsingleton = { toInhabited := AddUnits.instInhabited, uniq := ⋯ }
-- Lean.CoreM
_private.Lean.CoreM.0.Lean.Core.mkFreshNameImp : Lean.Name → Lean.CoreM Lean.Name
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates the limit of `K` and `K ⋙ F` has a limit, then `K` has a limit.  -/
CategoryTheory.hasColimit_of_created : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasColimit (K.comp F)] [CategoryTheory.CreatesColimit K F],
  CategoryTheory.Limits.HasColimit K
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.equivOfIsClopen.congr_simp : ∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {U : ι → Set α} (hclopen : ∀ (i : ι), IsClopen (U i))
  (hdisj : Pairwise (Function.onFun Disjoint U)) (hunion : ⋃ i, U i = Set.univ),
  ConnectedComponents.equivOfIsClopen hclopen hdisj hunion = ConnectedComponents.equivOfIsClopen hclopen hdisj hunion
-- Mathlib.Order.Hom.WithTopBot
SupHom.withTop'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] [inst_2 : OrderTop β]
  (f : SupHom α β), f.withTop' = { toFun := fun a => Option.elim a ⊤ ⇑f, map_sup' := ⋯ }
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.truth_comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C},
  CategoryTheory.CategoryStruct.comp 𝒞₁.truth (𝒞₁.hom 𝒞₂) = CategoryTheory.CategoryStruct.comp (𝒞₂.χ₀ 𝒞₁.Ω₀) 𝒞₂.truth
-- Batteries.Data.List.Lemmas
List.findIdxs_map : ∀ {α : Type u_1} {xs : List α} {α_1 : Type u_2} {f : α → α_1} {p : α_1 → Bool} {s : ℕ},
  List.findIdxs p (List.map f xs) s = List.findIdxs (p ∘ f) xs s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.forM_eq_forM_toList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : (a : α) × β a → m' PUnit.{w + 1}}, forM m f = forM m.toList f
-- Std.Sync.Channel
Std.CloseableChannel.instMonadLiftEIOErrorIO : MonadLift (EIO Std.CloseableChannel.Error) IO
-- Mathlib.Algebra.Ring.Defs
CommSemiring.toSemiring : {R : Type u} → [self : CommSemiring R] → Semiring R
-- Init.Data.UInt.Lemmas
USize.ofNatLT_uInt64ToNat : ∀ (n : UInt64) (h : n.toNat < USize.size), USize.ofNatLT n.toNat h = n.toUSize
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.inc.injEq : ∀ (x : Lean.IR.VarId) (n : ℕ) (c persistent : Bool) (b : Lean.IR.FnBody) (x_1 : Lean.IR.VarId) (n_1 : ℕ)
  (c_1 persistent_1 : Bool) (b_1 : Lean.IR.FnBody),
  (Lean.IR.FnBody.inc x n c persistent b = Lean.IR.FnBody.inc x_1 n_1 c_1 persistent_1 b_1) =
    (x = x_1 ∧ n = n_1 ∧ c = c_1 ∧ persistent = persistent_1 ∧ b = b_1)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- Every finite measure is σ-finite.  -/
MeasureTheory.IsFiniteMeasure.toSigmaFinite : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.SigmaFinite μ
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.instIsIsoIntιTruncLEOfIsStrictlyLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) [K.IsStrictlyLE n],
  CategoryTheory.IsIso (K.ιTruncLE n)
-- Mathlib.ModelTheory.Syntax
/-- The biimplication between two bounded formulas.  -/
FirstOrder.Language.BoundedFormula.iff : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instNonemptySavedState : Nonempty Lean.Elab.Do.SavedState
-- Lean.Language.Basic
Lean.Language.instInhabitedSnapshot : Inhabited Lean.Language.Snapshot
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- **Alias** of `AlgebraicGeometry.tilde.toOpen_res`. -/
ModuleCat.Tilde.toOpen_res : ∀ {R : CommRingCat} (M : ModuleCat ↑R) (U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑R))
  (i : V ⟶ U),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.toOpen M U)
      ((AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M)).presheaf.map i.op) =
    AlgebraicGeometry.tilde.toOpen M V
-- Mathlib.Algebra.CharP.Basic
/-- If two integers from `{0, 1, -1}` result in equal elements in a ring `R`
that is nontrivial and of characteristic not `2`, then they are equal.  -/
Int.cast_injOn_of_ringChar_ne_two : ∀ {R : Type u_2} [inst : NonAssocRing R] [Nontrivial R], ringChar R ≠ 2 → Set.InjOn Int.cast {0, 1, -1}
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.mem_iInf : ∀ {R : Type u} [inst : Semiring R] {ι : Sort u_1} {I : ι → Ideal R} {x : R}, x ∈ iInf I ↔ ∀ (i : ι), x ∈ I i
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integrableOn_rpow_mul_exp_neg_mul_sq : ∀ {b : ℝ},
  0 < b →
    ∀ {s : ℝ},
      -1 < s → MeasureTheory.IntegrableOn (fun x => x ^ s * Real.exp (-b * x ^ 2)) (Set.Ioi 0) MeasureTheory.volume
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.instPatternModelChar : {c : Char} → String.Slice.Pattern.Model.PatternModel c
-- Mathlib.Data.ENNReal.Operations
/-- Weaker version of `ENNReal.sub_eq_of_eq_add` assuming that `a = c + b` itself is finite rather
han `b`.  -/
ENNReal.sub_eq_of_eq_add' : ∀ {a b c : ENNReal}, a ≠ ⊤ → a = c + b → a - b = c
-- Mathlib.RingTheory.WittVector.Basic
/-- An auxiliary tactic for proving that `ghostFun` respects the ring operations.  -/
WittVector.«tacticGhost_fun_tac_,_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
CategoryTheory.ShiftedHom.opEquiv'_symm_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y : C}
  {n a : ℤ}
  (f : Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj (Opposite.op X))
  (a' : ℤ) (h : n + a = a'),
  (CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm f =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ShiftedHom.opEquiv n).symm f)
      ((CategoryTheory.shiftFunctorAdd' C a n a' ⋯).inv.app Y)
-- Lean.Declaration
Lean.ConstantInfo.type : Lean.ConstantInfo → Lean.Expr
-- Lean.Elab.DeclNameGen
/-- Converts a module name into a suffix. Includes a leading `_`,
so for example `Lean.Elab.DefView` becomes `_lean_elab_defView`.
 -/
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.moduleToSuffix : Lean.Name → String
-- Lean.Meta.BinderNameHint
/-- Does `e` have a binder name hint? (quick check)  -/
Lean.Expr.hasBinderNameHint : Lean.Expr → Bool
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.excenterWeights_eq_excenterWeights_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n}
  {signs₁ signs₂ : Finset (Fin (n + 1))},
  s.ExcenterExists signs₁ →
    s.ExcenterExists signs₂ → (s.excenterWeights signs₁ = s.excenterWeights signs₂ ↔ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.blocks_eq_nil : ∀ {n : ℕ} (c : Composition n), c.blocks = [] ↔ n = 0
-- Aesop.Tree.Data
Aesop.GoalData.unsafeRulesSelected : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Bool
-- Init.Data.Random
/-- Generates a random natural number in the interval [lo, hi].  -/
randNat : {gen : Type u} → [RandomGen gen] → gen → ℕ → ℕ → ℕ × gen
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.eq_1 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1)
  (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))),
  (match none with
    | none => h_1 ()
    | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
    | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) =
    h_1 ()
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- The field of fractions of a valuative commutative square.  -/
AlgebraicGeometry.ValuativeCommSq.K : {X Y : AlgebraicGeometry.Scheme} → {f : X ⟶ Y} → AlgebraicGeometry.ValuativeCommSq f → Type u
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- The composition of `Ext`.  -/
CategoryTheory.Abelian.Ext.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y Z : C} →
          {a b : ℕ} →
            CategoryTheory.Abelian.Ext X Y a →
              CategoryTheory.Abelian.Ext Y Z b → {c : ℕ} → a + b = c → CategoryTheory.Abelian.Ext X Z c
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.Scheme.germToFunctionField_injective : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsIntegral X] (U : X.Opens) [inst_1 : Nonempty ↥↑U],
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U))
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₄_def : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution.u₄✝ S =
    ⋯.unit * FermatLastTheoremForThreeGen.Solution.u₃✝ S * (FermatLastTheoremForThreeGen.Solution.u₂✝ S)⁻¹
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.liftAddHom_apply_single : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (f : α → M →+ N)
  (a : α) (b : M), ((Finsupp.liftAddHom f) fun₀ | a => b) = (f a) b
-- Mathlib.RingTheory.Frobenius
/-- Suppose `S` is a domain, and `φ : S →ₐ[R] S` is a Frobenius at `Q : Ideal S`.
Let `ζ` be a `m`-th root of unity with `Q ∤ m`, then `φ` sends `ζ` to `ζ ^ q`.  -/
AlgHom.IsArithFrobAt.apply_of_pow_eq_one : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S},
  φ.IsArithFrobAt Q → ∀ [IsDomain S] {ζ : S} {m : ℕ}, ζ ^ m = 1 → ↑m ∉ Q → φ ζ = ζ ^ Nat.card (R ⧸ Ideal.under R Q)
-- Mathlib.Order.Filter.Pointwise
Filter.one_mem_one : ∀ {α : Type u_2} [inst : One α], 1 ∈ 1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.isSorted : Lean.Grind.CommRing.Poly → Bool
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singleton_zpow : ∀ {α : Type u_2} [inst : DivisionMonoid α] (a : α) (n : ℤ), {a} ^ n = {a ^ n}
-- Mathlib.Algebra.Algebra.Hom
AlgHom.id_toRingHom : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  ↑(AlgHom.id R A) = RingHom.id A
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.empty_equiv_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  ∅.Equiv m ↔ m.isEmpty = true
-- Init.Data.Range.Polymorphic.PRange
Std.Rio.LawfulRcoIntersection.mk : ∀ {α : Type w} [inst : LT α] [inst_1 : LE α] [inst_2 : Std.Rio.HasRcoIntersection α],
  (∀ {a : α} {r : Std.Rio α} {s : Std.Rco α}, a ∈ Std.Rio.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s) →
    Std.Rio.LawfulRcoIntersection α
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.Braided.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F : CategoryTheory.Functor C D} →
                  [toMonoidal : F.Monoidal] →
                    autoParam
                        (∀ (X Y : C),
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
                              (F.map (β_ X Y).hom) =
                            CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom
                              (CategoryTheory.Functor.LaxMonoidal.μ F Y X))
                        CategoryTheory.Functor.LaxBraided.braided._autoParam →
                      F.Braided
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.coe_evalMonoidHom : ∀ {I : Type u} (f : I → Type v) [inst : (i : I) → MulOneClass (f i)] (i : I), ⇑(Pi.evalMonoidHom f i) = Function.eval i
-- Mathlib.Data.ENat.Lattice
ENat.natCast_sSup : ∀ {s : Set ℕ}, BddAbove s → ↑(sSup s) = ⨆ a ∈ s, ↑a
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHoms.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p),
  CochainComplex.HomComplex.Cochain.ofHoms ψ =
    CochainComplex.HomComplex.Cochain.mk fun p q hpq =>
      CategoryTheory.CategoryStruct.comp (ψ p) (CategoryTheory.eqToHom ⋯)
-- Mathlib.Geometry.Manifold.Notation
/-- Utility for sections in a fibre bundle: if an expression `e` is a section
`s : Π x : M, V x` as a dependent function, convert it to a non-dependent function into the total
space. This handles the cases of
- sections of a trivial bundle
- vector fields on a manifold (i.e., sections of the tangent bundle)
- sections of an explicit fibre bundle
- turning a bare function `E → E'` into a section of the trivial bundle `Bundle.Trivial E E'`

This searches the local context for suitable hypotheses for the above cases by matching
on the expression structure, avoiding `isDefEq`. Therefore, it should be fast enough to always run.
This process can be traced with `set_option Elab.DiffGeo.TotalSpaceMk true`.

All applications of `e` in the resulting expression are beta-reduced.
If none of the handled cases apply, we simply return `e` (after beta-reducing).

This function is used for implementing the `T%` elaborator.
 -/
Manifold.Elab.totalSpaceMk : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.rank_eq_two : ∀ {R : Type u_1} (a b : R) [inst : Semiring R] [StrongRankCondition R], Module.rank R (QuadraticAlgebra R a b) = 2
-- Mathlib.Order.Interval.Multiset
Multiset.Icc_eq_zero_of_lt : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, b < a → Multiset.Icc a b = 0
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.induction_on : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {β : LocalizedModule S M → Prop}, (∀ (m : M) (s : ↥S), β (LocalizedModule.mk m s)) → ∀ (x : LocalizedModule S M), β x
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
forall_le_add_iff_le_right : ∀ {α : Type u_1} [inst : LinearOrder α] {P : α → Prop} {b c : α} [inst_1 : AddCommMagma α] [CanonicallyOrderedAdd α]
  [AddLeftMono α] [IsLeftCancelAdd α], (∀ a ≤ b + c, P a) ↔ (∀ a < c, P a) ∧ ∀ d ≤ b, P (d + c)
-- Mathlib.LinearAlgebra.Prod
LinearMap.coe_prodMap : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄),
  ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.lintegral_eq_zero_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α →ₘ[μ] ENNReal}, f.lintegral = 0 ↔ f = 0
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- `rightSection` splits `π`  -/
CategoryTheory.IsSplitCoequalizer.rightSection_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
  (self : CategoryTheory.IsSplitCoequalizer f g π),
  CategoryTheory.CategoryStruct.comp self.rightSection π = CategoryTheory.CategoryStruct.id Z
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_eq_getD : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {fallback : β} {h' : a ∈ m}, m[a] = m.getD a fallback
-- Mathlib.Computability.Primrec.List
Primrec.list_getI : ∀ {α : Type u_1} [inst : Primcodable α] [inst_1 : Inhabited α], Primrec₂ List.getI
-- Mathlib.Order.Hom.Lattice
InfHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Min α] [inst_1 : Min β] [inst_2 : SizeOf α] [inst_3 : SizeOf β] (toFun : α → β)
  (map_inf' : ∀ (a b : α), toFun (a ⊓ b) = toFun a ⊓ toFun b), sizeOf { toFun := toFun, map_inf' := map_inf' } = 1
-- Lean.Elab.App
Lean.Elab.Term.instReprElabElimInfo : Repr Lean.Elab.Term.ElabElimInfo
-- Lean.Elab.DeclNameGen
/-- Uses heuristics to generate an informative but terse base name for a term of the given type, using `mkBaseName`.
Makes use of the current namespace.
It tries to make these names relatively unique ecosystem-wide,
and it adds suffixes using the current module if the resulting name doesn't refer to anything defined in this module.

If any constant in `type` has a name with macro scopes, then the result will be a name with fresh macro scopes.
While in this case we could skip the naming heuristics, we still want informative names for debugging purposes.
 -/
Lean.Elab.Command.NameGen.mkBaseNameWithSuffix : String → Lean.Expr → Lean.MetaM Lean.Name
-- Mathlib.MeasureTheory.Measure.Haar.DistribChar
MeasureTheory.distribHaarChar.congr_simp : ∀ {G : Type u_1} (A : Type u_2) [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : TopologicalSpace A] [inst_4 : IsTopologicalAddGroup A] [inst_5 : LocallyCompactSpace A]
  [inst_6 : ContinuousConstSMul G A], MeasureTheory.distribHaarChar A = MeasureTheory.distribHaarChar A
-- Init.Core
optParam_eq : ∀ (α : Sort u) (default : α), optParam α default = α
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂), z₁.comp (-z₂) h = -z₁.comp z₂ h
-- Mathlib.GroupTheory.IsSubnormal
/-- If `g : Γ` is an element of a group acting on `G` and `H` is subnormal, then `g • H` is subnormal.
 -/
Subgroup.IsSubnormal.smul : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {Γ : Type u_2} [inst_1 : Group Γ] [inst_2 : MulDistribMulAction Γ G],
  H.IsSubnormal → ∀ (g : Γ), (g • H).IsSubnormal
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
/-- The connecting homomorphism (as a natural transformation) for the spectral
objects attached to the objects of a triangulated equipped with a t-structure.  -/
CategoryTheory.Triangulated.TStructure.ω₁δ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                [CategoryTheory.IsTriangulated C] →
                  (a b c : EInt) →
                    (hab : a ≤ b) →
                      (hbc : b ≤ c) →
                        t.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hbc)) ⟶
                          (t.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hab))).comp
                            (CategoryTheory.shiftFunctor C 1)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.isAdmissible_cons_cons_iff : ∀ {m a b : ℕ} {L : List ℕ},
  SimplexCategoryGenRel.IsAdmissible m (a :: b :: L) ↔
    a < b ∧ SimplexCategoryGenRel.IsAdmissible (m + 1) (b :: L) ∧ a ≤ m
-- Mathlib.Analysis.Complex.Norm
Complex.nnnorm_real : ∀ (r : ℝ), ‖↑r‖₊ = ‖r‖₊
-- Mathlib.Algebra.Homology.CochainComplexPlus
CochainComplex.instIsClosedUnderIsomorphismsIntPlus : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (CochainComplex.plus C).IsClosedUnderIsomorphisms
-- Init.Data.BitVec.Lemmas
BitVec.mul_assoc : ∀ {w : ℕ} (x y z : BitVec w), x * y * z = x * (y * z)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.lt_def : ∀ {M : Type u_1} [inst : Group M] [inst_1 : Lattice M] {a b : MulArchimedeanOrder M},
  a < b ↔ ∀ (n : ℕ), |MulArchimedeanOrder.val b|ₘ ^ n < |MulArchimedeanOrder.val a|ₘ
-- Mathlib.Algebra.Star.Module
/-- The skew-adjoint elements of a star module, as a submodule.  -/
skewAdjoint.submodule : (R : Type u_1) →
  (A : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : StarMul R] →
        [TrivialStar R] →
          [inst_3 : AddCommGroup A] →
            [inst_4 : Module R A] → [inst_5 : StarAddMonoid A] → [StarModule R A] → Submodule R A
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeIso.eq_1 : ∀ {B : Type u} [inst : Quiver B] {a : B} (x x_1 : B) (x_2 : Quiver.Path a x) (f : x ⟶ x_1),
  CategoryTheory.FreeBicategory.normalizeIso x_2 (CategoryTheory.FreeBicategory.Hom.of f) =
    CategoryTheory.Iso.refl
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.FreeBicategory.preinclusion B).map { as := x_2 })
        (CategoryTheory.FreeBicategory.Hom.of f))
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply : ∀ {R : Type u} [inst : CommRing R] {x x_1 : CategoryTheory.Mon (ModuleCat R)} (f : x ⟶ x_1) (a : ↑x.X),
  (AlgCat.Hom.hom (ModuleCat.MonModuleEquivalenceAlgebra.functor.map f)) a =
    (CategoryTheory.ConcreteCategory.hom f.hom) a
-- Mathlib.Data.Finset.Fold
Finset.fold_union_inter : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β}
  [inst : DecidableEq α] {s₁ s₂ : Finset α} {b₁ b₂ : β},
  op (Finset.fold op b₁ f (s₁ ∪ s₂)) (Finset.fold op b₂ f (s₁ ∩ s₂)) =
    op (Finset.fold op b₂ f s₁) (Finset.fold op b₁ f s₂)
-- Mathlib.Data.Countable.Defs
Uncountable.mk : ∀ {α : Sort u_1}, ¬Countable α → Uncountable α