mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Context.mk.inj : ∀ {simp : Lean.Meta.Simp.Context} {simpMethods : Lean.Meta.Simp.Methods} {config : Lean.Grind.Config}
  {anchorRefs? : Option (Array Lean.Meta.Grind.AnchorRef)} {cheapCases reportMVarIssue : Bool}
  {splitSource : Lean.Meta.Grind.SplitSource} {ematchDiagSource : Lean.Meta.Grind.EMatchDiagSource}
  {symPrios : Lean.Meta.Grind.SymbolPriorities} {extensions : Lean.Meta.Grind.ExtensionStateArray}
  {debug ematchDiag : Bool} {simp_1 : Lean.Meta.Simp.Context} {simpMethods_1 : Lean.Meta.Simp.Methods}
  {config_1 : Lean.Grind.Config} {anchorRefs?_1 : Option (Array Lean.Meta.Grind.AnchorRef)}
  {cheapCases_1 reportMVarIssue_1 : Bool} {splitSource_1 : Lean.Meta.Grind.SplitSource}
  {ematchDiagSource_1 : Lean.Meta.Grind.EMatchDiagSource} {symPrios_1 : Lean.Meta.Grind.SymbolPriorities}
  {extensions_1 : Lean.Meta.Grind.ExtensionStateArray} {debug_1 ematchDiag_1 : Bool},
  { simp := simp, simpMethods := simpMethods, config := config, anchorRefs? := anchorRefs?, cheapCases := cheapCases,
        reportMVarIssue := reportMVarIssue, splitSource := splitSource, ematchDiagSource := ematchDiagSource,
        symPrios := symPrios, extensions := extensions, debug := debug, ematchDiag := ematchDiag } =
      { simp := simp_1, simpMethods := simpMethods_1, config := config_1, anchorRefs? := anchorRefs?_1,
        cheapCases := cheapCases_1, reportMVarIssue := reportMVarIssue_1, splitSource := splitSource_1,
        ematchDiagSource := ematchDiagSource_1, symPrios := symPrios_1, extensions := extensions_1, debug := debug_1,
        ematchDiag := ematchDiag_1 } →
    simp = simp_1 ∧
      simpMethods = simpMethods_1 ∧
        config = config_1 ∧
          anchorRefs? = anchorRefs?_1 ∧
            cheapCases = cheapCases_1 ∧
              reportMVarIssue = reportMVarIssue_1 ∧
                splitSource = splitSource_1 ∧
                  ematchDiagSource = ematchDiagSource_1 ∧
                    symPrios = symPrios_1 ∧ extensions = extensions_1 ∧ debug = debug_1 ∧ ematchDiag = ematchDiag_1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
/-- Returns `true` if the linarith state is inconsistent.  -/
Lean.Meta.Grind.Arith.Linear.inconsistent : Lean.Meta.Grind.Arith.Linear.LinearM Bool
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULift.downFunctor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : ULift.{u₂, u₁} C} (f : X ⟶ Y),
  CategoryTheory.ULift.downFunctor.map f = f
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.instIsCancelAddLocalization : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} [IsCancelAdd M], IsCancelAdd (AddLocalization S)
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.Martingale.martingalePart_eq : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0} [CompleteSpace E],
  MeasureTheory.Martingale f ℱ μ → ∀ (n : ℕ), MeasureTheory.martingalePart f ℱ μ n =ᵐ[μ] f n
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.rightCont_eq_of_nhdsGT_eq_bot : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : PartialOrder ι] [inst_1 : TopologicalSpace ι]
  [OrderTopology ι] (𝓕 : MeasureTheory.Filtration ι m) {i : ι}, nhdsWithin i (Set.Ioi i) = ⊥ → ↑𝓕.rightCont i = ↑𝓕 i
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.ofTop_toLinearEquiv : ∀ (E : Type u_5) [inst : SeminormedAddCommGroup E] {R : Type u_12} [inst_1 : Ring R] [inst_2 : Module R E]
  (p : Submodule R E) (hp : p = ⊤), (LinearIsometryEquiv.ofTop E p hp).toLinearEquiv = LinearEquiv.ofTop p hp
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : β → β} {h : k' ∈ Std.DHashMap.Const.modify m k f},
  Std.DHashMap.Const.get (Std.DHashMap.Const.modify m k f) k' h =
    if heq : (k == k') = true then f (Std.DHashMap.Const.get m k ⋯) else Std.DHashMap.Const.get m k' ⋯
-- Lean.Parser.Term
Lean.Parser.Term.tuple.formatter : Lean.PrettyPrinter.Formatter
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.trailingNode.formatter : Lean.SyntaxNodeKind → ℕ → ℕ → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_isLoopAt : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {F : Set β},
  (G.restrict F).IsLoopAt e x ↔ G.IsLoopAt e x ∧ e ∈ F
-- Lean.Elab.Tactic.Basic
/-- Execute an action and return any new messages it generates.
Restores the original message log afterward.
Useful for inspecting messages produced by a tactic without committing them.  -/
Lean.Elab.Tactic.withCapturedMessages : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM (α × List Lean.Message)
-- Mathlib.Algebra.Group.Action.Units
Units.instIsScalarTower : ∀ {M : Type u_3} {N : Type u_4} {α : Type u_5} [inst : Monoid M] [inst_1 : SMul M N] [inst_2 : SMul M α]
  [inst_3 : SMul N α] [IsScalarTower M N α], IsScalarTower Mˣ N α
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
/-- The equivalence between a field and the residue field of its prime ideal,
induced by the algebra map.  -/
Ideal.algEquivResidueFieldOfField : {k : Type u_5} → [inst : Field k] → (p : Ideal k) → [inst_1 : p.IsPrime] → k ≃ₐ[k] p.ResidueField
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.M : Type → Type
-- Mathlib.Topology.LocallyFinsupp
/-- On a T1 space, the support of a function with locally finite support within `U` is discrete.
 -/
Function.locallyFinsuppWithin.discreteSupport : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] [T1Space X]
  (D : Function.locallyFinsuppWithin U Y), IsDiscrete D.support
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.forget₂CommMon_comp_forget : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.CommGrp.forget₂CommMon C).comp (CategoryTheory.CommMon.forget C) = CategoryTheory.CommGrp.forget C
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instCommMonoid : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : CommMonoid γ] → [ContinuousMul γ] → CommMonoid (α →ₘ[μ] γ)
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedCtorInfo.default : Lean.IR.CtorInfo
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.associator_inv_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H I : CategoryTheory.Grp C),
  (CategoryTheory.MonoidalCategoryStruct.associator G H I).inv.hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.associator G.X H.X I.X).inv
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Nonsingular P → W.Nonsingular Q → P 2 = 0 → Q 2 = 0 → W.add P Q = P 1 ^ 4 • ![0, 1, 0]
-- Init.Sym.Lemmas
Lean.Sym.UInt32.le_eq_false : ∀ (a b : UInt32), decide (a ≤ b) = false → (a ≤ b) = False
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeffEquiv.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R],
  AddMonoidAlgebra.coeffEquiv =
    { toFun := AddMonoidAlgebra.coeff, invFun := AddMonoidAlgebra.ofCoeff, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Data.QPF.Multivariate.Basic
/-- does `abs` preserve `liftp`?  -/
MvQPF.LiftPPreservation : {n : ℕ} → {F : TypeVec.{u} n → Type u_1} → [q : MvQPF F] → Prop
-- Init.Data.SInt.Lemmas
Int64.eq_iff_ofBitVec_eq : ∀ {a b : BitVec 64}, a = b ↔ Int64.ofBitVec a = Int64.ofBitVec b
-- Mathlib.RingTheory.Radical.Basic
EuclideanDomain.divRadical_mul : ∀ {E : Type u_1} [inst : EuclideanDomain E] [inst_1 : NormalizationMonoid E] [inst_2 : UniqueFactorizationMonoid E]
  {a b : E},
  IsCoprime a b → EuclideanDomain.divRadical (a * b) = EuclideanDomain.divRadical a * EuclideanDomain.divRadical b
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_ne_nil : ∀ {n : ℕ}, (*...=n).toList ≠ []
-- Mathlib.GroupTheory.OrderOfElement
isOfFinOrder_iff_zpow_eq_one : ∀ {G : Type u_6} [inst : DivisionMonoid G] {x : G}, IsOfFinOrder x ↔ ∃ n, n ≠ 0 ∧ x ^ n = 1
-- Init.Data.Sum.Basic
/-- `inr b₁` and `inr b₂` are related via `Lex r s` if `b₁` and `b₂` are related via `s`.  -/
Sum.Lex.inr : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {b₁ b₂ : β},
  s b₁ b₂ → Sum.Lex r s (Sum.inr b₁) (Sum.inr b₂)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getEntryD_eq_getEntryD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [instBEq : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β} {fallback : (a : α) × β a},
  t.Ordered → t.getEntryD k fallback = Std.Internal.List.getEntryD k fallback t.toListModel
-- Lean.Elab.Tactic.Try
/-- `evalSuggest` for `attempt_all_par` tactic (parallel version).  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestAttemptAllPar : Array (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Mathlib.CategoryTheory.Presentable.Basic
/-- A functor is accessible relative to a universe `w` if
it is `κ`-accessible for some regular `κ : Cardinal.{w}`.  -/
CategoryTheory.Functor.IsAccessible : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.ColimitType.AddGroupWithOne : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) → AddGroupWithOne (CommRingCat.Colimits.ColimitType F)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonNatIso_inv_app_hom : ∀ {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 F' : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [inst_5 : F'.LaxMonoidal] (e : F ≅ F')
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal e.hom] (X : CategoryTheory.AddMon C),
  ((CategoryTheory.Functor.mapAddMonNatIso e).inv.app X).hom = e.inv.app X.X
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatch.isLongestMatchAt_ofSliceFrom : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {p₀ : s.Pos}
  {pos : (s.sliceFrom p₀).Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos →
    String.Slice.Pattern.Model.IsLongestMatchAt pat p₀ (String.Slice.Pos.ofSliceFrom pos)
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBySet.mk_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (b : R) (x : ↥(Submodule.torsionBySet R M ↑I)), (Ideal.Quotient.mk I) b • x = b • x
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso_inv_homologyπ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) {Z : C} (h : ((HomologicalComplex.single C c j).obj A).homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).inv
      (CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).homologyπ j) h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).inv h
-- Init.Data.Ord.Basic
Ordering.eq_beq_lt : (Ordering.eq == Ordering.lt) = false
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comap_apply₀ : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β)
  (μ : MeasureTheory.Measure β),
  Function.Injective f →
    (∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ) →
      MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.comap f μ) →
        (MeasureTheory.Measure.comap f μ) s = μ (f '' s)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.Sheaf K (Type v)}
  (α α_1 : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj),
  α = α_1 →
    ∀ {X : D} (x x_1 : ℱ.obj (Opposite.op X)),
      x = x_1 →
        ∀ ⦃Y : D⦄ (f f_1 : Y ⟶ X) (e_f : f = f_1) (a : CategoryTheory.Presieve.coverByImage G X f),
          CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x f a =
            CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α_1 x_1 f_1 ⋯
-- Mathlib.Order.Sublocale
Sublocale.coe_iInf : ∀ {X : Type u_1} [inst : Order.Frame X] {ι : Sort u_2} {S : Sublocale X} (f : ι → ↥S), ↑(⨅ i, f i) = ⨅ i, ↑(f i)
-- Init.Data.SInt.Lemmas
ISize.toInt_sub : ∀ (a b : ISize), (a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ System.Platform.numBits)
-- Mathlib.Algebra.Algebra.Pi
AlgHom.pi_apply : ∀ {ι : Type u_1} {R : Type u_2} {A : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] {B : Type u_4} [inst_3 : Semiring B] [inst_4 : Algebra R B]
  (g : (i : ι) → B →ₐ[R] A i) (x : B) (b : ι), (AlgHom.pi g) x b = (g b) x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.verts_top : ∀ {V : Type u} {G : SimpleGraph V}, ⊤.verts = Set.univ
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Ring
/-- Applying the recurrence formula repeatedly, we get

$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) =
\left(\sum_{k=0}^{j} (-1)^k \left(x^{k(3k+1)/2} - x^{(k+1)(3k+2)/2}\right) \right) +
(-1)^{j+1}x^{(j+1)(3j+4)/2}A_j $$  -/
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.Ring.0.Pentagonal.tprod_one_sub_pow_eq_powMulProdOneSubPow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [T2Space R] (j : ℕ) {x : R},
  IsTopologicallyNilpotent x →
    (∀ (k : ℕ), Summable fun x_1 => Pentagonal.powMulProdOneSubPow✝ k x_1 x) →
      (∀ (k : ℕ), Multipliable fun n => 1 - x ^ (n + k + 1)) →
        ∏' (n : ℕ), (1 - x ^ (n + 1)) =
          ∑ k ∈ Finset.range (j + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
            (-1) ^ (j + 1) * x ^ ((j + 1) * (3 * j + 4) / 2) * ∑' (n : ℕ), Pentagonal.powMulProdOneSubPow✝ j n x
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBaseNat.brecOn.eq : ∀ {motive_1 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExBaseNat e → Sort u}
  {motive_2 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExProdNat e → Sort u}
  {motive_3 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExSumNat e → Sort u} {e : Q(ℕ)}
  (t : Mathlib.Tactic.Ring.Common.ExBaseNat e)
  (F_1 : (e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExBaseNat e) → t.below → motive_1 e t)
  (F_2 : (e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExProdNat e) → t.below → motive_2 e t)
  (F_3 : (e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExSumNat e) → t.below → motive_3 e t),
  t.brecOn F_1 F_2 F_3 = F_1 e t (Mathlib.Tactic.Ring.Common.ExBaseNat.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.sumNodes_le_sumNodes_T : ∀ {n : ℕ} {c : ℕ → ℝ},
  (∀ i ≤ n, 0 ≤ (-1) ^ i * c i) →
    ∀ {P : Polynomial ℝ},
      (∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ 1) →
        Polynomial.Chebyshev.sumNodes n c P ≤ Polynomial.Chebyshev.sumNodes n c (Polynomial.Chebyshev.T ℝ ↑n)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : SizeOf C] (hom : X ⟶ Y) (inv : Y ⟶ X)
  (hom_inv_id :
    autoParam (CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.Iso.hom_inv_id._autoParam)
  (inv_hom_id :
    autoParam (CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.Iso.inv_hom_id._autoParam),
  sizeOf { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id } =
    1 + sizeOf hom + sizeOf inv + sizeOf hom_inv_id + sizeOf inv_hom_id
-- Mathlib.Algebra.Order.Group.Finset
Multiset.toFinset_eq_singleton_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (a : α), s.toFinset = {a} ↔ s.card ≠ 0 ∧ s = s.card • {a}
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.length_add : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α]
  (s t : NonemptyInterval α), (s + t).length = s.length + t.length
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instBot.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  AddSubgroup.instBot =
    {
      bot :=
        let __src := ⊥;
        { toAddSubmonoid := __src, neg_mem' := ⋯ } }
-- Init.Data.Int.DivMod.Lemmas
Int.emod_sub_cancel_left : ∀ {m n k : ℤ} (i : ℤ), (i - m) % n = (i - k) % n ↔ m % n = k % n
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Section.mk : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] →
          [inst_2 : AddGroup G] →
            {S : AddGroupExtension N E G} → (toFun : G → E) → Function.RightInverse toFun ⇑S.rightHom → S.Section
-- Mathlib.Topology.Separation.Regular
/-- In a compact T₂ space, the connected component of a point equals the intersection of all
its clopen neighbourhoods.  -/
connectedComponent_eq_iInter_isClopen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [CompactSpace X] (x : X), connectedComponent x = ⋂ s, ↑s
-- Mathlib.RingTheory.Localization.Finiteness
/-- If there exists a set `{ r }` of `R` that generates the unit ideal and such that `Mᵣ` is
`Rᵣ`-finite for each `r`, then `M` is a finite `R`-module.  -/
Module.Finite.of_localizationSpan : ∀ {R : Type u} [inst : CommSemiring R] {M : Type w} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (t : Set R),
  Ideal.span t = ⊤ →
    (∀ (g : ↑t), Module.Finite (Localization.Away ↑g) (LocalizedModule.Away (↑g) M)) → Module.Finite R M
-- ProofWidgets.Data.Html
ProofWidgets.Html.brecOn_2.eq : ∀ {motive_1 : ProofWidgets.Html → Sort u} {motive_2 : Array ProofWidgets.Html → Sort u}
  {motive_3 : List ProofWidgets.Html → Sort u} (t : List ProofWidgets.Html)
  (F_1 : (t : ProofWidgets.Html) → t.below → motive_1 t)
  (F_2 : (t : Array ProofWidgets.Html) → ProofWidgets.Html.below_1 t → motive_2 t)
  (F_3 : (t : List ProofWidgets.Html) → ProofWidgets.Html.below_2 t → motive_3 t),
  ProofWidgets.Html.brecOn_2 t F_1 F_2 F_3 = F_3 t (ProofWidgets.Html.brecOn_2.go t F_1 F_2 F_3).2
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.withConstants_funMap_sumInl : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] {α : Type w'} [inst_1 : (L.withConstants α).Structure M]
  [(L.lhomWithConstants α).IsExpansionOn M] {n : ℕ} {f : L.Functions n} {x : Fin n → M},
  FirstOrder.Language.Structure.funMap (Sum.inl f) x = FirstOrder.Language.Structure.funMap f x
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.Λ₀.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E), P.Λ₀ = mellin P.f_modif
-- Lean.Meta.AppBuilder
_private.Lean.Meta.AppBuilder.0.Lean.Meta.withAppBuilderTrace : {α β : Type} → [Lean.ToMessageData α] → [Lean.ToMessageData β] → α → β → Lean.MetaM Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Functor.Trifunctor
/-- Auxiliary definition for `bifunctorComp₂₃`.  -/
CategoryTheory.bifunctorComp₂₃Obj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₂₃ : Type u_6} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] →
                    CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄) →
                      CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃) →
                        C₁ → CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)
-- Aesop.Options.Public
/-- Best-first search. This is the default strategy.
 -/
Aesop.Strategy.bestFirst : Aesop.Strategy
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.mk_le_mk : ∀ {K : Type u} [inst : DivisionRing K] {S S' : Subring K} (h : ∀ x ∈ S.carrier, x⁻¹ ∈ S.carrier)
  (h' : ∀ x ∈ S'.carrier, x⁻¹ ∈ S'.carrier),
  { toSubring := S, inv_mem' := h } ≤ { toSubring := S', inv_mem' := h' } ↔ S ≤ S'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.hasPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z}, CategoryTheory.IsPullback fst snd f g → CategoryTheory.Limits.HasPullback f g
-- Aesop.Rule
Aesop.RegularRule.indexingMode : Aesop.RegularRule → Aesop.IndexingMode
-- Mathlib.Tactic.ClickSuggestions.TryPremises
/-- Spawn tasks for the given candidate premises and
return an HTML that shows the incoming results  -/
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.runSuggestions : Mathlib.Tactic.ClickSuggestions.SectionKind →
  Mathlib.Tactic.ClickSuggestions.Candidates✝ → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM ProofWidgets.Html
-- Mathlib.Analysis.InnerProductSpace.Continuous
ContinuousWithinAt.inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {α : Type u_4} [inst_3 : TopologicalSpace α] {f g : α → E} {x : α} {s : Set α},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun t => inner 𝕜 (f t) (g t)) s x
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_eq_on_Ico' : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  (n : ℕ), ∀ a ∈ Set.Ico (↑n) (↑n + 1), ↑⌊a⌋₊ = ↑n
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_le_iff_le_add' : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, a - b ≤ c ↔ a ≤ b + c
-- Mathlib.Topology.Sets.BaseChangeNhds
/-- The evidence that `⊥` is initial among the compact open neighbourhoods of `⊥`  -/
TopologicalSpace.Compacts.isInitialBotOpensOpenNhdsBot : {α : Type u_1} → [inst : TopologicalSpace α] → CategoryTheory.Limits.IsInitial ⊥
-- Std.Tactic.BVDecide.Syntax
/-- The number of seconds that the SAT solver is run before aborting.  -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.timeout : Lean.Elab.Tactic.BVDecide.BVDecideConfig → ℕ
-- Mathlib.CategoryTheory.Functor.CurryingThree
/-- Flip the first and third arguments in a trifunctor, as a functor.
 -/
CategoryTheory.Functor.flip₁₃Functor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_4} →
      {E : Type u_9} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] →
              [inst_3 : CategoryTheory.Category.{v_9, u_9} E] →
                CategoryTheory.Functor
                  (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)))
                  (CategoryTheory.Functor C₃ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₁ E)))
-- Mathlib.Tactic.Order.Graph.Basic
/-- `visited.contains v` if and only if the algorithm has already entered vertex `v`.  -/
Mathlib.Tactic.Order.Graph.DFSState.visited : Mathlib.Tactic.Order.Graph.DFSState → Std.HashSet ℕ