mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Finite.Basic
/-- Finite sets can be lifted to finsets.  -/
Set.instCanLiftFinsetCoeFinite : ∀ {α : Type u}, CanLift (Set α) (Finset α) SetLike.coe Set.Finite
-- Mathlib.CategoryTheory.Limits.Final
/-- See also the strictly more general `initial_iff_comp_initial_full_faithful` below.  -/
CategoryTheory.Functor.initial_iff_comp_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [G.IsEquivalence], F.Initial ↔ (F.comp G).Initial
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.single_mem_pi : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] [inst_1 : DecidableEq ι] {I : Set ι}
  {S : (i : ι) → AddSubmonoid (M i)} (i : ι) (x : M i), Pi.single i x ∈ AddSubmonoid.pi I S ↔ i ∈ I → x ∈ S i
-- Mathlib.Order.Filter.Pointwise
Filter.mul_add_subset : ∀ {α : Type u_2} [inst : Distrib α] {f g h : Filter α}, f * (g + h) ≤ f * g + f * h
-- Mathlib.Tactic.Simproc.ExistsAndEq
ExistsAndEq.instInhabitedGoTo : Inhabited ExistsAndEq.GoTo
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.instTop : {V : Type u} → {G : SimpleGraph V} → [Finite V] → Top G.Finsubgraph
-- Mathlib.Data.Set.Pairwise.Lattice
Set.pairwiseDisjoint_sUnion : ∀ {α : Type u_1} {ι : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {f : ι → α} {s : Set (Set ι)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) s → ((⋃₀ s).PairwiseDisjoint f ↔ ∀ ⦃a : Set ι⦄, a ∈ s → a.PairwiseDisjoint f)
-- Batteries.CodeAction.Attr
Batteries.CodeAction.TacticCodeActionEntry.mk.injEq : ∀ (declName : Lean.Name) (tacticKinds : Array Lean.Name) (declName_1 : Lean.Name) (tacticKinds_1 : Array Lean.Name),
  ({ declName := declName, tacticKinds := tacticKinds } = { declName := declName_1, tacticKinds := tacticKinds_1 }) =
    (declName = declName_1 ∧ tacticKinds = tacticKinds_1)
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.PreservesMonomorphisms.ofRetract : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (r : CategoryTheory.Retract G F) [F.PreservesMonomorphisms],
  G.PreservesMonomorphisms
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_id : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d (CategoryTheory.CategoryStruct.id c) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_lt_sqrt : ∀ {x y : NNReal}, NNReal.sqrt x < NNReal.sqrt y ↔ x < y
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.strictMono : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), StrictMono ⇑f
-- Mathlib.Topology.Order.Monotone
/-- In a second countable space, the set of points where a monotone function is not right-continuous
within a set is at most countable. Superseded by `MonotoneOn.countable_not_continuousWithinAt`
which gives the two-sided version.  -/
MonotoneOn.countable_not_continuousWithinAt_Ioi : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {s : Set α} {f : α → β} [inst_4 : TopologicalSpace β] [OrderTopology β]
  [SecondCountableTopology β], MonotoneOn f s → {x | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Set.Ioi x) x}.Countable
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
/-- The nerve of a category, as a functor `Cat ⥤ SSet`  -/
CategoryTheory.nerveFunctor : CategoryTheory.Functor CategoryTheory.Cat SSet
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.congrRightₗ_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} (R : Type u_7) [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid Y] [inst_3 : Module R Y] [inst_4 : AddCommMonoid Z] [inst_5 : Module R Z] (e : Y ≃ₗ[R] Z)
  (g : LocallyConstant X Y) (a : X), ((LocallyConstant.congrRightₗ R e) g) a = e (g a)
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.dvd : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Associated a b → a ∣ b
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.mk.injEq : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (toMonoidHom : R →* R')
  (map_nonunit' : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom).toFun a = 0) (toMonoidHom_1 : R →* R')
  (map_nonunit'_1 : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom_1).toFun a = 0),
  ({ toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' } =
      { toMonoidHom := toMonoidHom_1, map_nonunit' := map_nonunit'_1 }) =
    (toMonoidHom = toMonoidHom_1)
-- Mathlib.Data.Seq.Computation
Computation.eq_thinkN' : ∀ {α : Type u} (s : Computation α) [_h : s.Terminates], s = (Computation.pure s.get).thinkN s.length
-- Mathlib.Geometry.Convex.Hull
Convexity.subset_convexHull_iff : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s t : Set X},
  t ⊆ (Convexity.convexHull R) s ↔ ∀ (C : Set X), s ⊆ C → Convexity.IsConvexSet R C → t ⊆ C
-- Init.System.IOError
IO.Error.resourceVanished.sizeOf_spec : ∀ (osCode : UInt32) (details : String),
  sizeOf (IO.Error.resourceVanished osCode details) = 1 + sizeOf osCode + sizeOf details
-- Lean.Data.OpenDecl
Lean.OpenDecl.simple.sizeOf_spec : ∀ (ns : Lean.Name) (except : List Lean.Name), sizeOf (Lean.OpenDecl.simple ns except) = 1 + sizeOf ns + sizeOf except
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_subset_ball' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ},
  ε₁ + dist x y < ε₂ → Metric.closedBall x ε₁ ⊆ Metric.ball y ε₂
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_embDomain : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {v : α →₀ M}
  {f : α ↪ β} {g : β → M → N}, (Finsupp.embDomain f v).sum g = v.sum fun a b => g (f a) b
-- Mathlib.GroupTheory.SchurZassenhaus
Subgroup.instInhabitedQuotientDiff : {G : Type u_1} →
  [inst : Group G] →
    (H : Subgroup G) → [inst_1 : IsMulCommutative ↥H] → [inst_2 : H.FiniteIndex] → Inhabited H.QuotientDiff
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.linter.unusedSimpArgs : Lean.Option Bool
-- Init.Data.Vector.Lemmas
Vector.prod_append : ∀ {α : Type u_1} {n m : ℕ} [inst : One α] [inst_1 : Mul α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.LeftIdentity (fun x1 x2 => x1 * x2) 1] [Std.LawfulLeftIdentity (fun x1 x2 => x1 * x2) 1] {as₁ : Vector α n}
  {as₂ : Vector α m}, (as₁ ++ as₂).prod = as₁.prod * as₂.prod
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.finOrderIsoPairCompl_apply_val : ∀ {n : ℕ} (i j : Fin (n + 2)) (h : i < j) (k : Fin n),
  ↑((SSet.stdSimplex.finOrderIsoPairCompl i j h) k) = j.succAbove ((i.castPred ⋯).succAbove k)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.sset.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {i offset : ℕ} {y : Lean.FVarId} {ty : Lean.Expr}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_7} {fvarId_1 : Lean.FVarId}
  {i_1 offset_1 : ℕ} {y_1 : Lean.FVarId} {ty_1 : Lean.Expr}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_7},
  Lean.Compiler.LCNF.CodeDecl.sset fvarId i offset y ty h =
      Lean.Compiler.LCNF.CodeDecl.sset fvarId_1 i_1 offset_1 y_1 ty_1 h_1 →
    fvarId = fvarId_1 ∧ i = i_1 ∧ offset = offset_1 ∧ y = y_1 ∧ ty = ty_1
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.aestronglyMeasurable : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E} [OpensMeasurableSpace E]
  {μ : MeasureTheory.Measure E} (f : ContDiffMapSupportedIn E F n K), MeasureTheory.AEStronglyMeasurable (⇑f) μ
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instTransVltVeq : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : ValuativeRel R] → Trans ValuativeRel.vlt ValuativeRel.veq ValuativeRel.vlt
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.mem_ordConnectedComponent : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x y : α}, y ∈ s.ordConnectedComponent x ↔ Set.uIcc x y ⊆ s
-- Lean.Parser.Term
Lean.Parser.Term.structInstFieldEqns.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.arrowCongrₗ_apply : ∀ {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} {V₄ : Type u_9}
  [inst : AddCommGroup V₁] [inst_1 : AddCommGroup V₂] [inst_2 : AddCommGroup V₃] [inst_3 : AddCommGroup V₄]
  [inst_4 : AddTorsor V₁ P₁] [inst_5 : AddTorsor V₂ P₂] {R : Type u_10} [inst_6 : CommRing R] [inst_7 : Module R V₁]
  [inst_8 : Module R V₂] [inst_9 : Module R V₃] [inst_10 : Module R V₄] (e₁ : P₁ ≃ᵃ[R] P₂) (e₂ : V₃ ≃ₗ[R] V₄)
  (f : P₁ →ᵃ[R] V₃) (x : P₂), ((e₁.arrowCongrₗ e₂) f) x = e₂ (f (e₁.symm x))
-- Lean.Meta.Tactic.Simp.Arith.Util
Lean.Meta.Simp.Arith.isLinearPosCnstr : Lean.Expr → Bool
-- Mathlib.Topology.Order.NhdsSet
nhdsSet_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a : α},
  nhdsSet (Set.Iio a) = Filter.principal (Set.Iio a)
-- Init.Data.Int.Linear
Int.Internal.Linear.of_var_eq_mul : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (k : ℤ) (y : Int.Internal.Linear.Var)
  (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.of_var_eq_mul_cert x k y p = true →
    Int.Internal.Linear.Var.denote ctx x = k * Int.Internal.Linear.Var.denote ctx y →
      Int.Internal.Linear.Poly.denote' ctx p = 0
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
/-- If `f : ℂ → ℂ` is complex-analytic, then its complex conjugate is harmonic.
 -/
AnalyticAt.harmonicAt_conj : ∀ {x : ℂ} {f : ℂ → ℂ}, AnalyticAt ℂ f x → InnerProductSpace.HarmonicAt ((starRingEnd (ℂ → ℂ)) f) x
-- Mathlib.Order.Lattice
inf_inf_inf_comm : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c d : α), a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ (b ⊓ d)
-- Mathlib.GroupTheory.Commutator.Basic
commutatorElement_eq_one_iff_mul_comm : ∀ {G : Type u_1} [inst : Group G] {g₁ g₂ : G}, ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.pi : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → Monoid (α i)] {x : (i : ι) → α i} [Finite ι],
  (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- On topological spaces where indicators of closed sets have decreasing approximating sequences of
continuous functions (`HasOuterApproxClosed`), the topology of convergence in distribution of Borel
probability measures is Hausdorff (`T2Space`).  -/
MeasureTheory.ProbabilityMeasure.t2Space : ∀ (Ω : Type u_1) [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [HasOuterApproxClosed Ω]
  [inst_3 : BorelSpace Ω], T2Space (MeasureTheory.ProbabilityMeasure Ω)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_preimage_image : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.normLeOne K =
    NumberField.mixedEmbedding.normAtAllPlaces ⁻¹'
      NumberField.mixedEmbedding.normAtAllPlaces '' NumberField.mixedEmbedding.fundamentalCone.normLeOne K
-- Mathlib.Topology.Maps.Basic
/-- **Alias** of the reverse direction of `Topology.isCoinducing_iff`. -/
Topology.IsCoinducing.of_isOpen_preimage_iff_isOpen : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  (∀ (s : Set Y), IsOpen (f ⁻¹' s) ↔ IsOpen s) → Topology.IsCoinducing f
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- The Cartesian product of two alternating maps, as an alternating map.  -/
AlternatingMap.prod : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {P : Type u_4} →
                  [inst_5 : AddCommMonoid P] →
                    [inst_6 : Module R P] → {ι : Type u_7} → M [⋀^ι]→ₗ[R] N → M [⋀^ι]→ₗ[R] P → M [⋀^ι]→ₗ[R] (N × P)
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.ExtDTreeMap.entryAtIdx! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → [Inhabited ((a : α) × β a)] → Std.ExtDTreeMap α β cmp → ℕ → (a : α) × β a
-- Mathlib.Topology.MetricSpace.Algebra
AddOpposite.lipschitzAdd : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : AddMonoid β] [LipschitzAdd β], LipschitzAdd βᵃᵒᵖ
-- Mathlib.FieldTheory.IsSepClosed
SeparableClosure.isSepClosed : ∀ (F : Type u_1) [inst : Field F], IsSepClosed (SeparableClosure F)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [Std.LawfulEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false} {km : α},
      Std.Internal.List.minKey l he = km ↔
        Std.Internal.List.containsKey km l = true ∧
          ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare km k).isLE = true
-- Mathlib.Algebra.Group.Defs
/-- An `AddSemigroup` which `IsMulCommutative` is a `AddCommSemigroup`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsAddCommutative.instAddCommSemigroup : {M : Type u_2} → [inst : AddSemigroup M] → [IsAddCommutative M] → AddCommSemigroup M
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT : ∀ (N : Type u_2) [inst : Add N] [IsRightCancelAdd N] [inst_2 : PartialOrder N] [AddRightReflectLT N],
  AddRightReflectLE N
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.isEmptyEquiv_apply : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R] [inst_1 : IsEmpty σ] (a : MvPowerSeries σ R),
  (MvPowerSeries.isEmptyEquiv σ R) a = MvPowerSeries.constantCoeff a
-- Init.Data.Rat.Lemmas
Rat.add_le_iff_le_sub : ∀ {a b c : ℚ}, a + b ≤ c ↔ a ≤ c - b
-- Mathlib.GroupTheory.SchurZassenhaus
Subgroup.smul_diff' : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst_1 : IsMulCommutative ↥H] [inst_2 : H.FiniteIndex]
  (α β : H.LeftTransversal) [inst_3 : H.Normal] (h : ↥H),
  Subgroup.leftTransversals.diff (MonoidHom.id ↥H) α (MulOpposite.op ↑h • β) =
    Subgroup.leftTransversals.diff (MonoidHom.id ↥H) α β * h ^ H.index
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_I_of_ne_zero : ∀ {K : Type u_1} [inst : RCLike K], RCLike.I ≠ 0 → ‖RCLike.I‖ = 1
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.homAddEquiv_symm_apply_hom : ∀ {M N : AddCommGrpCat} (a : CategoryTheory.ToHom M N), AddCommGrpCat.Hom.hom (AddCommGrpCat.homAddEquiv.symm a) = a
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.right_unitality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (self : F.CoreMonoidal) (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) self.εIso.hom)
      (CategoryTheory.CategoryStruct.comp (self.μIso X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) h))
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- Construct an isomorphism of commutative group objects by giving a monoid isomorphism between the
underlying objects.  -/
CategoryTheory.CommGrp.mkIso' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {G H : C} →
          (e : G ≅ H) →
            [inst_3 : CategoryTheory.GrpObj G] →
              [inst_4 : CategoryTheory.IsCommMonObj G] →
                [inst_5 : CategoryTheory.GrpObj H] →
                  [inst_6 : CategoryTheory.IsCommMonObj H] →
                    [CategoryTheory.IsMonHom e.hom] →
                      { X := G, grp := inst_3, comm := inst_4 } ≅ { X := H, grp := inst_5, comm := inst_6 }
-- Lean.Expr
/-- Return `p ∨ q`  -/
Lean.mkOr : Lean.Expr → Lean.Expr → Lean.Expr
-- Init.Data.List.MinMaxIdx
List.get_maxIdxOn?_eq_maxIdxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α}
  (h : (List.maxIdxOn? f xs).isSome = true), (List.maxIdxOn? f xs).get h = List.maxIdxOn f xs ⋯
-- Mathlib.LinearAlgebra.Orientation
/-- Every basis vector from `adjust_to_orientation` is either that from the original basis or its
negation.  -/
Module.Basis.adjustToOrientation_apply_eq_or_eq_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  [inst_7 : Nonempty ι] (e : Module.Basis ι R M) (x : Orientation R M ι) (i : ι),
  (e.adjustToOrientation x) i = e i ∨ (e.adjustToOrientation x) i = -e i
-- Mathlib.Algebra.CubicDiscriminant
Cubic.eq_sum_three_roots : ∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K} {x y z : K},
  P.a ≠ 0 →
    (Cubic.map φ P).roots = {x, y, z} →
      Cubic.map φ P =
        { a := φ P.a, b := φ P.a * -(x + y + z), c := φ P.a * (x * y + x * z + y * z), d := φ P.a * -(x * y * z) }
-- Init.Conv
/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
that would be sufficient to close the goal. See the `simp?` tactic for more information.  -/
Lean.Parser.Tactic.Conv.simpTrace : Lean.ParserDescr
-- Mathlib.Order.Interval.Finset.Nat
Nat.Ico_image_const_sub_eq_Ico : ∀ {a b c : ℕ}, a ≤ c → Finset.image (fun x => c - x) (Finset.Ico a b) = Finset.Ico (c + 1 - b) (c + 1 - a)
-- Init.Grind.Ring.Basic
/-- Alternative constructor when `α` is a `Ring`.  -/
Lean.Grind.IsCharP.mk' : ∀ (p : ℕ) (α : Type u) [inst : Lean.Grind.Ring α], (∀ (x : ℕ), OfNat.ofNat x = 0 ↔ x % p = 0) → Lean.Grind.IsCharP α p