mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.ConstantSpeed
hasConstantSpeedOnWith_of_subsingleton : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] (f : ℝ → E) {s : Set ℝ},
  s.Subsingleton → ∀ (l : NNReal), HasConstantSpeedOnWith f s l
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiff.sum_section : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {ι : Type u_7} {t : ι → (x : M) → V x} {s : Finset ι},
  (∀ i ∈ s, ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, t i x⟩) →
    ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, ∑ i ∈ s, t i x⟩
-- Lean.Parser.Extra
Lean.Parser.atomic.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.sectionsMap_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {M N P : SheafOfModules R} (f : M ⟶ N) (g : N ⟶ P) (s : M.sections),
  SheafOfModules.sectionsMap (CategoryTheory.CategoryStruct.comp f g) s =
    SheafOfModules.sectionsMap g (SheafOfModules.sectionsMap f s)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k a : α} [inst_1 : Inhabited (β a)] {v : β k},
  (t.insertIfNew k v).get! a = if h : cmp k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.get! a
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Real.hasDerivAt_exp : ∀ (x : ℝ), HasDerivAt Real.exp (Real.exp x) x
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.coe_forget₂_obj : ∀ (X : CommMonCat), ↑((CategoryTheory.forget₂ CommMonCat MonCat).obj X) = ↑X
-- Mathlib.Logic.Equiv.PartialEquiv
Set.BijOn.toPartialEquiv_target : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : α → β) (s : Set α) (t : Set β) (hf : Set.BijOn f s t),
  (Set.BijOn.toPartialEquiv f s t hf).target = t
-- Mathlib.Data.Finsupp.BigOperators
Finset.mem_sup_support_iff : ∀ {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst_1 : Zero M] {s : Finset (ι →₀ M)} {x : ι},
  x ∈ s.sup Finsupp.support ↔ ∃ f ∈ s, x ∈ f.support
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.freeAddMonoidCongr_of : ∀ {α : Type u_6} {β : Type u_7} (e : α ≃ β) (a : α),
  (FreeAddMonoid.freeAddMonoidCongr e) (FreeAddMonoid.of a) = FreeAddMonoid.of (e a)
-- Init.Data.Vector.Basic
/-- The underlying array.  -/
Vector.toArray : {α : Type u} → {n : ℕ} → Vector α n → Array α
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Balanced.brecOn : ∀ {c₀ : RBTree.RBColor} {n₀ : ℕ} {α : Type u_1}
  {motive :
    (a : RBTree.RBNode.Path α) →
      (a_1 : RBTree.RBColor) → (a_2 : ℕ) → RBTree.RBNode.Path.Balanced c₀ n₀ a a_1 a_2 → Prop}
  {a : RBTree.RBNode.Path α} {a_1 : RBTree.RBColor} {a_2 : ℕ} (t : RBTree.RBNode.Path.Balanced c₀ n₀ a a_1 a_2),
  (∀ (a : RBTree.RBNode.Path α) (a_3 : RBTree.RBColor) (a_4 : ℕ) (t : RBTree.RBNode.Path.Balanced c₀ n₀ a a_3 a_4),
      RBTree.RBNode.Path.Balanced.below t → motive a a_3 a_4 t) →
    motive a a_1 a_2 t
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofTermInfo.sizeOf_spec : ∀ (i : Lean.Elab.TermInfo), sizeOf (Lean.Elab.Info.ofTermInfo i) = 1 + sizeOf i
-- Lean.Expr
Lean.PersistentExprStructMap : Type → Type
-- Mathlib.Order.Filter.Prod
/-- Characterization of the `Filter.map` of the coproduct of two principal filters `𝓟 {a}` and
`𝓟 {i}`, under the `Prod.map` of two functions, respectively the constant function `fun a => b` and
the identity function.  Together with the previous lemma,
`map_const_principal_coprod_map_id_principal`, this provides an example showing that the inequality
in the lemma `map_prodMap_coprod_le` can be strict.  -/
Filter.map_prodMap_const_id_principal_coprod_principal : ∀ {α : Type u_6} {β : Type u_7} {ι : Type u_8} (a : α) (b : β) (i : ι),
  Filter.map (Prod.map (fun x => b) id) ((Filter.principal {a}).coprod (Filter.principal {i})) =
    Filter.principal ({b} ×ˢ Set.univ)
-- Std.Data.ByteSlice
instSliceableByteSliceNat_2 : Std.Rci.Sliceable ByteSlice ℕ ByteSlice
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.toList_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ},
  (Std.ExtTreeMap.filterMap f t).toList = List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) t.toList
-- Mathlib.Data.NNReal.Defs
NNReal.orderIsoIccZeroCoe_symm_apply_coe : ∀ (a : NNReal) (b : ↑(Set.Iic a)), ↑(a.orderIsoIccZeroCoe.symm b) = ↑↑b
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_ofList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)}, List.Pairwise (fun a b => (a.1 == b.1) = false) l → (Std.ExtHashMap.ofList l).size = l.length
-- Lean.Environment
/-- Information to be exported to other modules.  -/
Lean.Environment.Visibility.public : Lean.Environment.Visibility
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelIso.eq_1 : ∀ {X Y : SemiNormedGrp} (f : X ⟶ Y),
  SemiNormedGrp.explicitCokernelIso f =
    (SemiNormedGrp.isColimitCokernelCocone f).coconePointUniqueUpToIso
      (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair f 0))
-- Mathlib.Algebra.Order.Floor.Extended
ENat.lt_floor : ∀ {r : ENNReal} {n : ℕ∞}, n ≠ ⊤ → (n < ⌊r⌋ₑ ↔ ↑n + 1 ≤ r)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.instCoePreconnectedPreconnectedElemVertsCoe : {V : Type u} → {G : SimpleGraph V} → {H : G.Subgraph} → Coe H.Preconnected H.coe.Preconnected
-- Mathlib.Data.Finset.Empty
/-- **Alias** of the reverse direction of `Finset.coe_nonempty`. -/
Finset.Nonempty.to_set : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → (↑s).Nonempty
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.norm_of_pow : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (n : ℕ), (FreeGroup.of a ^ n).norm = n
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
iSup_ne_of_notMem : ∀ {α : Type u_5} [inst : CompleteLinearOrder α] {ι : Sort u_6} [Finite ι] {f : ι → α} {a : α},
  a ≠ ⊥ → (∀ (x : ι), f x ≠ a) → iSup f ≠ a
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.ext : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R}, (∀ (x : R), x ∈ I ↔ x ∈ J) → I = J
-- Mathlib.Analysis.Normed.Group.Uniform
AddMonoidHomClass.antilipschitz_of_bound : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) {K : NNReal},
  (∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖) → AntilipschitzWith K ⇑f
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.rightCosetEquivalence_equiv_snd : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G} (hHT : Subgroup.IsComplement (↑H) T) (g : G),
  RightCosetEquivalence (↑H) g ↑(hHT.equiv g).2
-- Mathlib.Order.RelIso.Basic
/-- A relation embedding is also a relation homomorphism  -/
RelEmbedding.toRelHom : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → r →r s
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- Transitivity of cyclotomic extensions.  -/
IsCyclotomicExtension.trans : ∀ (S T : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (C : Type w)
  [inst_3 : CommRing C] [inst_4 : Algebra A C] [inst_5 : Algebra B C] [IsScalarTower A B C]
  [hS : IsCyclotomicExtension S A B] [hT : IsCyclotomicExtension T B C],
  Function.Injective ⇑(algebraMap B C) → IsCyclotomicExtension (S ∪ T) A C
-- Std.Data.HashMap.RawLemmas
/-- Variant of `getD_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.HashMap.Raw.getD_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → γ} {k : α} {fallback : γ} (h : m.WF),
  (Std.HashMap.Raw.map f m).getD k fallback = (Option.pmap (fun v h => f (m.getKey k h) v) m[k]? ⋯).getD fallback
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigOWith.const_smul_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} {R : Type u_13} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : SeminormedRing R] {c : ℝ} {g : α → F} {f' : α → E'} {l : Filter α} [inst_3 : Module R E']
  [IsBoundedSMul R E'],
  Asymptotics.IsBigOWith c l f' g → ∀ (c' : R), Asymptotics.IsBigOWith (‖c'‖ * c) l (fun x => c' • f' x) g
-- Mathlib.Order.Filter.Defs
Filter.univ_mem' : ∀ {α : Type u_1} {f : Filter α} {s : Set α}, (∀ (a : α), a ∈ s) → s ∈ f
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.innerRegular_inv_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G], μ.inv.InnerRegular ↔ μ.InnerRegular
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- The inverse of a structomorphism is a structomorphism.  -/
Structomorph.symm : {H : Type u} →
  {M : Type u_2} →
    {M' : Type u_3} →
      [inst : TopologicalSpace H] →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : ChartedSpace H M] →
            [inst_3 : TopologicalSpace M'] →
              {G : StructureGroupoid H} → [inst_4 : ChartedSpace H M'] → Structomorph G M M' → Structomorph G M' M
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.eval_monoidalComp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g h i : C} {η η' : f ⟶ g} {α : g ≅ h} {θ θ' : h ⟶ i}
  {αθ : g ⟶ i} {ηαθ : f ⟶ i},
  η = η' →
    θ = θ' →
      CategoryTheory.CategoryStruct.comp α.hom θ' = αθ →
        CategoryTheory.CategoryStruct.comp η' αθ = ηαθ →
          CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp α.hom θ) = ηαθ
-- Mathlib.Control.Traversable.Instances
Option.mapM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Applicative m] (f : α → m β),
  Option.mapM f none = pure none
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Arrow.hasColimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  [CategoryTheory.Limits.HasColimitsOfShape J T], CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Arrow T)
-- Mathlib.Algebra.CharP.LocalRing
/-- In a local ring the characteristic is either zero or a prime power.  -/
charP_zero_or_prime_power : ∀ (R : Type u_1) [inst : CommRing R] [IsLocalRing R] (q : ℕ) [char_R_q : CharP R q], q = 0 ∨ IsPrimePow q
-- Lean.Meta.Tactic.Grind.CollectParams
/-- Given a `grind` tactic sequence, extracts parameters and builds a `grind only` tactics.
It returns at most two. The first tactic uses anchors to restrict the search if applicable.
The second does not restrict the search using anchors. The second option is included only if there
are anchors.

The `extraParams` are additional parameters (e.g., term arguments from the original `grind?` call)
that should always be included in the suggestion.
 -/
Lean.Meta.Grind.mkGrindOnlyTactics : Lean.TSyntax `Lean.Parser.Tactic.optConfig →
  List Lean.Meta.Grind.TGrind → optParam (Array Lean.Meta.Grind.TParam) #[] → Lean.CoreM (Array (Lean.TSyntax `tactic))
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.topEquiv_symm_apply_coe : ∀ {M : Type u_5} [inst : MulOneClass M] (x : M), ↑(Submonoid.topEquiv.symm x) = x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqMon.beq_spec_3 : ∀ (x x_1 : Lean.Grind.CommRing.Mon),
  (x = Lean.Grind.CommRing.Mon.unit → x_1 = Lean.Grind.CommRing.Mon.unit → False) →
    (∀ (a : Lean.Grind.CommRing.Power) (a_1 : Lean.Grind.CommRing.Mon) (b : Lean.Grind.CommRing.Power)
        (b_1 : Lean.Grind.CommRing.Mon),
        x = Lean.Grind.CommRing.Mon.mult a a_1 → x_1 = Lean.Grind.CommRing.Mon.mult b b_1 → False) →
      (x == x_1) = false
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {l : List α} {k : α} {h : k ∈ Std.DHashMap.Const.unitOfList l},
  Std.DHashMap.Const.get (Std.DHashMap.Const.unitOfList l) k h = ()
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.inv_rev : ∀ {α : Type u_1} {𝕜 : Type u_15} {𝕜' : Type u_16} [inst : NormedDivisionRing 𝕜] [inst_1 : NormedDivisionRing 𝕜']
  {l : Filter α} {f : α → 𝕜} {g : α → 𝕜'},
  f =o[l] g → (∀ᶠ (x : α) in l, f x = 0 → g x = 0) → (fun x => (g x)⁻¹) =o[l] fun x => (f x)⁻¹
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
/-- Suppose we have a commutative square of functors

```
      Q
    A → B
  U ↓   ↓ V
    C → D
      R
```

where `U` has a left adjoint, `A` has reflexive coequalizers and `V` has a left adjoint such that
each component of the counit is a regular epi.
Then `Q` has a left adjoint if `R` has a left adjoint.

See https://ncatlab.org/nlab/show/adjoint+lifting+theorem
 -/
CategoryTheory.isRightAdjoint_square_lift : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (Q : CategoryTheory.Functor A B) (V : CategoryTheory.Functor B D)
  (U : CategoryTheory.Functor A C) (R : CategoryTheory.Functor C D) (comm : U.comp R ≅ Q.comp V) [U.IsRightAdjoint]
  [inst_5 : V.IsRightAdjoint] [R.IsRightAdjoint]
  (h : (X : B) → CategoryTheory.RegularEpi ((CategoryTheory.Adjunction.ofIsRightAdjoint V).counit.app X))
  [CategoryTheory.Limits.HasReflexiveCoequalizers A], Q.IsRightAdjoint
-- Mathlib.Analysis.LocallyConvex.Barrelled
Seminorm.continuous_of_lowerSemicontinuous : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddGroup E] [inst_1 : SMul 𝕜 E] [inst_2 : SeminormedRing 𝕜]
  [inst_3 : TopologicalSpace E] [BarrelledSpace 𝕜 E] (p : Seminorm 𝕜 E), LowerSemicontinuous ⇑p → Continuous ⇑p
-- Mathlib.Algebra.Order.Monoid.ToMulBot
WithZero.toMulBot_symm_bot : ∀ {α : Type u} [inst : Add α], WithZero.toMulBot.symm (Multiplicative.ofAdd ⊥) = 0
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.macroExpansion.sizeOf_spec : ∀ (macroName : Lean.Name) (stx stx' : Lean.Syntax) (nested : FBinopElab.Tree✝),
  sizeOf (FBinopElab.Tree.macroExpansion✝ macroName stx stx' nested) =
    1 + sizeOf macroName + sizeOf stx + sizeOf stx' + sizeOf nested
-- Mathlib.GroupTheory.Index
AddSubgroup.finiteIndex_toSubgroup_iff : ∀ {G : Type u_3} [inst : AddGroup G] (H : AddSubgroup G), (AddSubgroup.toSubgroup H).FiniteIndex ↔ H.FiniteIndex
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Coframe.mk : {α : Type u_1} →
  [toCompleteLattice : CompleteLattice α] →
    [toSDiff : SDiff α] →
      (∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c) → [toHNot : HNot α] → (∀ (a : α), ⊤ \ a = ￢a) → Order.Coframe α
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instSupSet : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → SupSet (CategoryTheory.Precoverage C)
-- Init.Data.SInt.Lemmas
Int64.toInt8_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt8 = OfNat.ofNat n
-- Init.Data.Nat.Order
Nat.instLawfulOrderMax : Std.LawfulOrderMax ℕ
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_eq_getValueD_default : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Inhabited β] {l : List ((_ : α) × β)} {a : α},
  Std.Internal.List.getValue! a l = Std.Internal.List.getValueD a l default
-- Mathlib.Topology.Algebra.InfiniteSum.Order
HasSum.nonpos : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {g : ι → α} {a : α} [L.NeBot],
  (∀ (i : ι), g i ≤ 0) → HasSum g a L → a ≤ 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue : Lean.Compiler.LCNF.Purity → Type
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.map_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} {P : Type u_6} [inst_1 : Group N] [inst_2 : Group P] (g : N →* P)
  (f : G →* N), Subgroup.map g f.range = (g.comp f).range
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lt_iSup_add_one : ∀ {ι : Type u_3} (f : ι → Ordinal.{u}) [Small.{u, u_3} ι] (i : ι), f i < ⨆ i, f i + 1
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).inv
        Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
        (CategoryTheory.MonoidalCategoryStruct.associator W X
            (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
-- Aesop.Tree.Data
Aesop.Goal.forwardRuleMatches : Aesop.Goal → Aesop.ForwardRuleMatches
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.range_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Set.range ⇑h = Set.univ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {kmi : α}, (t.insertIfNew k v).minKey?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Mathlib.RingTheory.Ideal.Operations
Ideal.add_eq_one_iff : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R}, I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
-- Mathlib.FieldTheory.Separable
Polynomial.separable_iff_derivative_ne_zero : ∀ {F : Type u} [inst : Field F] {f : Polynomial F}, Irreducible f → (f.Separable ↔ Polynomial.derivative f ≠ 0)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.rescaleAlgHom_one : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R], MvPowerSeries.rescaleAlgHom 1 = AlgHom.id R (MvPowerSeries σ R)
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.createsCountableLimits : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.CountableCategory J] → CategoryTheory.CreatesLimitsOfShape J lightToProfinite
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_apply_ite_of_true : ∀ {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [inst : CommMonoid M] {p : ι → Prop}
  [inst_1 : DecidablePred p] (f g : ι → γ) (k : γ → M),
  (∀ x ∈ s, p x) → ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (f x)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α}, k ∈ Std.DHashMap.map f m ↔ k ∈ m
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertListIfNew_perm_of_perm_first : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l1 l2 toInsert : List ((a : α) × β a)},
  l1.Perm l2 →
    Std.Internal.List.DistinctKeys l1 →
      (Std.Internal.List.insertListIfNew l1 toInsert).Perm (Std.Internal.List.insertListIfNew l2 toInsert)
-- Init.Grind.Ring.Basic
/-- The successor power law for exponentiation.  -/
Lean.Grind.Semiring.pow_succ : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a : α) (n : ℕ), a ^ (n + 1) = a ^ n * a
-- Mathlib.Data.Set.MulAntidiagonal
Set.mem_antidiagonal : ∀ {α : Type u_1} [inst : Add α] {s t : Set α} {a : α} {x : α × α},
  x ∈ s.antidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a
-- Mathlib.Algebra.Order.Module.Defs
IsOrderedRing.toIsOrderedModule : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α], IsOrderedModule α α
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.partition.loop.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α × List α → Sort u_2) →
    (x : List α) →
      (x_1 : List α × List α) →
        ((bs cs : List α) → motive [] (bs, cs)) →
          ((a : α) → (as bs cs : List α) → motive (a :: as) (bs, cs)) → motive x x_1
-- Mathlib.Combinatorics.Colex
Finset.Colex.instLinearOrder : {α : Type u_1} → [LinearOrder α] → LinearOrder (Colex (Finset α))
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.asIdeal_lt_asIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : PrimeSpectrum R), x.asIdeal < y.asIdeal ↔ x < y
-- Mathlib.LinearAlgebra.Pi
Submodule.iInf_comap_proj : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] {p : (i : ι) → Submodule R (φ i)},
  ⨅ i, Submodule.comap (LinearMap.proj i) (p i) = Submodule.pi Set.univ p
-- Mathlib.Order.Lattice.Congruence
/-- Alternative conditions for a lattice congruence.  -/
LatticeCon.mk' : {α : Type u_2} →
  [inst : Lattice α] →
    (r : α → α → Prop) →
      [h₁ : Std.Refl r] →
        (∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)) →
          (∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z) →
            (∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)) → LatticeCon α
-- Mathlib.Order.Cover
CovBy.le_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ⋖ b → c < b → c ≤ a
-- Mathlib.Logic.Encodable.Pi
/-- If `α` is countable, then so is `Vector α n`.  -/
Encodable.List.Vector.countable : ∀ {α : Type u_1} [Countable α] {n : ℕ}, Countable (List.Vector α n)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.eq_zero_of_mono_cokernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Mono (CategoryTheory.Limits.cokernel.π f)],
  f = 0
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceLErase.match_7.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size → Sort u_3)
  (rs : ℕ) (k : α) (v : β k) (l_1 r : Std.DTreeMap.Internal.Impl α β)
  (hrb : (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).size)
  (h_1 :
    (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hrb hlr)
  (h_2 :
    (rs : ℕ) →
      (k : α) →
        (v : β k) →
          (l_2 r : Std.DTreeMap.Internal.Impl α β) →
            (hrb : (Std.DTreeMap.Internal.Impl.inner rs k v l_2 r).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l_2 r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner rs k v l_2 r) hrb hlr),
  (match Std.DTreeMap.Internal.Impl.inner rs k v l_1 r, hrb, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hrb, hlr => h_1 hrb hlr
    | Std.DTreeMap.Internal.Impl.inner rs k v l_2 r, hrb, hlr => h_2 rs k v l_2 r hrb hlr) =
    h_2 rs k v l_1 r hrb hlr