mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.pow : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {l : Filter α} {f : α → R} {g : α → S}, f =o[l] g → ∀ {n : ℕ}, 0 < n → (fun x => f x ^ n) =o[l] fun x => g x ^ n
-- Mathlib.Order.Partition.Basic
Partition.mk : {α : Type u_1} →
  [inst : CompleteLattice α] → {s : α} → (parts : Set α) → sSupIndep parts → ⊥ ∉ parts → sSup parts = s → Partition s
-- Lean.Parser.Command
Lean.Parser.Command.instance.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Order.Monotone
/-- If a function is antitone on a set in a second countable topological space, then there
are only countably many points that have several preimages.  -/
AntitoneOn.countable_setOfPred_two_preimages : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {s : Set α} {f : α → β} [SecondCountableTopology α],
  AntitoneOn f s → {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable
-- Mathlib.ModelTheory.Ultraproducts
FirstOrder.Language.Ultraproduct.realize_formula_cast : ∀ {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [inst : (a : α) → L.Structure (M a)]
  [∀ (a : α), Nonempty (M a)] {β : Type u_3} (φ : L.Formula β) (x : β → (a : α) → M a),
  (φ.Realize fun i => Quotient.mk' (x i)) ↔ ∀ᶠ (a : α) in ↑u, φ.Realize fun i => x i a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → (k ∈ t ↔ k' ∈ t)
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The center of isomorphic (not necessarily associative) rings are isomorphic.  -/
Subring.centerCongr : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocRing R] → [inst_1 : NonAssocRing S] → R ≃+* S → ↥(Subring.center R) ≃+* ↥(Subring.center S)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_map_piOptionEquivProd : ∀ {ι : Type u_1} [inst : Fintype ι] {β : Option ι → Type u_4} [inst_1 : (i : Option ι) → MeasurableSpace (β i)]
  (μ : (i : Option ι) → MeasureTheory.Measure (β i)) [∀ (i : Option ι), MeasureTheory.SigmaFinite (μ i)],
  MeasureTheory.Measure.map (⇑(MeasurableEquiv.piOptionEquivProd β).symm)
      ((MeasureTheory.Measure.pi fun i => μ (some i)).prod (μ none)) =
    MeasureTheory.Measure.pi μ
-- Mathlib.Combinatorics.HalesJewett
/-- Given a coloring `C` of `ι → α` and a combinatorial subspace `l` of `ι → α`, `l.IsMono C`
means that `l` is monochromatic with regard to `C`.  -/
Combinatorics.Subspace.IsMono : {η : Type u_5} → {α : Type u_6} → {ι : Type u_7} → {κ : Type u_8} → ((ι → α) → κ) → Combinatorics.Subspace η α ι → Prop
-- Mathlib.Order.SemiconjSup
IsOrderRightAdjoint.unique : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β} {g₁ g₂ : β → α},
  IsOrderRightAdjoint f g₁ → IsOrderRightAdjoint f g₂ → g₁ = g₂
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkspaceEdit.mk : Option (Std.TreeMap Lean.Lsp.DocumentUri Lean.Lsp.TextEditBatch compare) →
  Option (Array Lean.Lsp.DocumentChange) →
    Option (Std.TreeMap String Lean.Lsp.ChangeAnnotation compare) → Lean.Lsp.WorkspaceEdit
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_subset_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ∩ t ⊆ s ∪ t
-- Mathlib.Algebra.Lie.Weights.Killing
/-- Elements of the `α` root space which are Killing-orthogonal to the `-α` root space are
Killing-orthogonal to all of `L`.  -/
LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg : ∀ (K : Type u_2) (L : Type u_3) [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L] [FiniteDimensional K L]
  (H : LieSubalgebra K L) [inst_4 : H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {α : ↥H → K} {x : L},
  x ∈ LieAlgebra.rootSpace H α →
    (∀ y ∈ LieAlgebra.rootSpace H (-α), ((killingForm K L) x) y = 0) → x ∈ LinearMap.ker (killingForm K L)
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.quotientDiag_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (V : OpenSubgroup (CategoryTheory.Aut F)) {U : OpenSubgroup (CategoryTheory.Aut F)} (h : (↑U).Normal) {A : C}
  (u :
    (CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U)))
  (x : CategoryTheory.SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)),
  (CategoryTheory.PreGaloisCategory.quotientDiag✝ V h u).obj x = A
-- Mathlib.RingTheory.RingHom.Flat
/-- A ring homomorphism `f : R →+* S` is flat if `S` is flat as an `R` module.  -/
RingHom.Flat : {R : Type u} → {S : Type v} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f f_1 : A ⟶ X} (e_f : f = f_1)
  {i i_1 : A ⟶ B} (e_i : i = i_1) {p p_1 : X ⟶ Y} (e_p : p = p_1) {g g_1 : B ⟶ Y} (e_g : g = g_1)
  (sq : CategoryTheory.CommSq f i p g), sq.LiftStruct = ⋯.LiftStruct
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.instDecidableEqQuaternionGroup.decEq.match_1.eq_1 : ∀ {n : ℕ} (motive : QuaternionGroup n → QuaternionGroup n → Sort u_1) (a b : ZMod (2 * n))
  (h_1 : (a b : ZMod (2 * n)) → motive (QuaternionGroup.a a) (QuaternionGroup.a b))
  (h_2 : (a a_1 : ZMod (2 * n)) → motive (QuaternionGroup.a a) (QuaternionGroup.xa a_1))
  (h_3 : (a a_1 : ZMod (2 * n)) → motive (QuaternionGroup.xa a) (QuaternionGroup.a a_1))
  (h_4 : (a b : ZMod (2 * n)) → motive (QuaternionGroup.xa a) (QuaternionGroup.xa b)),
  (match QuaternionGroup.a a, QuaternionGroup.a b with
    | QuaternionGroup.a a, QuaternionGroup.a b => h_1 a b
    | QuaternionGroup.a a, QuaternionGroup.xa a_1 => h_2 a a_1
    | QuaternionGroup.xa a, QuaternionGroup.a a_1 => h_3 a a_1
    | QuaternionGroup.xa a, QuaternionGroup.xa b => h_4 a b) =
    h_1 a b
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isNNRat_lt_true : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α} {na nb da db : ℕ},
  Mathlib.Meta.NormNum.IsNNRat a na da →
    Mathlib.Meta.NormNum.IsNNRat b nb db → decide (na * db < nb * da) = true → a < b
-- Aesop.RuleTac.Cases
Aesop.CasesTarget'.decl : Lean.Name → Aesop.CasesTarget'
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.WF.containsThenInsert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α} {a : α},
  m.WF → (m.containsThenInsert a).2.WF
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α),
  QuotientAddGroup.quotientRightRelEquivQuotientLeftRel s =
    { toFun := Quotient.map' (fun g => -g) ⋯, invFun := Quotient.map' (fun g => -g) ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.GroupTheory.Nilpotent
/-- `upperCentralSeries G n` is the `n`th term in the upper central series of `G`.

This is the increasing chain of additive subgroups of `G` that starts with the trivial additive
subgroup `⊥` of `G` and then continues defining `upperCentralSeries G (n + 1)` to be all the
elements of `G` that, modulo `upperCentralSeries G n`, belong to the center of the additive quotient
`G ⧸ upperCentralSeries G n`.

In particular, the identities
* `upperCentralSeries G 0 = ⊥` (`upperCentralSeries_zero`);
* `upperCentralSeries G 1 = center G` (`upperCentralSeries_one`);

hold.
 -/
AddSubgroup.upperCentralSeries : (G : Type u_1) → [inst : AddGroup G] → ℕ → AddSubgroup G
-- Init.Data.Array.Lemmas
List.filterMap_toArray' : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} {stop : ℕ},
  stop = l.length → Array.filterMap f l.toArray 0 stop = (List.filterMap f l).toArray
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapCyclesIso_inv_naturality : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasLeftHomology]
  [inst_6 : S₂.HasLeftHomology] [inst_7 : F.PreservesLeftHomologyOf S₁] [inst_8 : F.PreservesLeftHomologyOf S₂],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.cyclesMap φ)) (S₂.mapCyclesIso F).inv =
    CategoryTheory.CategoryStruct.comp (S₁.mapCyclesIso F).inv
      (CategoryTheory.ShortComplex.cyclesMap (F.mapShortComplex.map φ))
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv_assoc : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension G] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape D H]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape C H]
  (X : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)) {Z : H}
  (h : CategoryTheory.Limits.colimit G ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G) X)
      (CategoryTheory.CategoryStruct.comp (L.colimitIsoColimitGrothendieck G).inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι G ((CategoryTheory.CostructuredArrow.proj L X.base).obj X.fiber)) h
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.balancedAtRoot_zero_iff : ∀ {n : ℕ}, Std.DTreeMap.Internal.Impl.BalancedAtRoot 0 n ↔ n ≤ 1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.updateFVar! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu → Lean.FVarId → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.RingTheory.Localization.AsSubring
Localization.subalgebra.instIsFractionRingSubtypeMemSubalgebra : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  (S : Subalgebra A K), IsFractionRing (↥S) K
-- Mathlib.Topology.Defs.Induced
/-- Given `f : X → Y` and a topology on `X`,
the coinduced topology on `Y` is defined such that
`s : Set Y` is open if the preimage of `s` is open.
This is the finest topology that makes `f` continuous.  -/
TopologicalSpace.coinduced : {X : Type u_1} → {Y : Type u_2} → (X → Y) → TopologicalSpace X → TopologicalSpace Y
-- Mathlib.Topology.Category.TopPair
/-- Construct a morphism in `TopPair` from its components.  -/
TopPair.ofHom : {X Y : TopPair} →
  (f : TopPair.fst ⟶ TopPair.fst) →
    (g : TopPair.snd ⟶ TopPair.snd) →
      autoParam (CategoryTheory.CategoryStruct.comp g TopPair.map = CategoryTheory.CategoryStruct.comp TopPair.map f)
          TopPair.ofHom._auto_1 →
        (X ⟶ Y)
-- Mathlib.Order.Fin.Basic
Fin.symm_castOrderIso : ∀ {m n : ℕ} (h : n = m), (Fin.castOrderIso h).symm = Fin.castOrderIso ⋯
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_subsingleton`.

---

The diameter of a subsingleton vanishes.  -/
EMetric.diam_subsingleton : ∀ {X : Type u_2} {s : Set X} [inst : PseudoEMetricSpace X], s.Subsingleton → Metric.ediam s = 0
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f)
    (AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.comp
      AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasProd.map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  {L : SummationFilter β} [inst_2 : CommMonoid γ] [inst_3 : TopologicalSpace γ],
  HasProd f a L →
    ∀ {G : Type u_4} [inst_4 : FunLike G α γ] [MonoidHomClass G α γ] (g : G), Continuous ⇑g → HasProd (⇑g ∘ f) (g a) L
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category `C` which has products is said to have `AB4Star` (in literature AB4\*)
provided that products are exact.  -/
CategoryTheory.AB4StarOfSize : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasProducts C] → Prop
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_isMaximal_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Ring R] [inst_1 : Ring S] [inst_2 : FunLike F R S]
  [inst_3 : RingHomClass F R S] (f : F),
  Function.Surjective ⇑f → ∀ {K : Ideal S} [H : K.IsMaximal], (Ideal.comap f K).IsMaximal
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_set_biUnion : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal]
  [inst_1 : MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set β},
  s.Countable → ∀ {t t' : β → Set α}, (∀ b ∈ s, t b =ᵐ[μ] t' b) → ⋃ b ∈ s, t b =ᵐ[μ] ⋃ b ∈ s, t' b
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoState.mk.injEq : ∀ (enabled : Bool) (assignment : Lean.PersistentHashMap Lean.MVarId Lean.Elab.InfoTree)
  (lazyAssignment : Lean.PersistentHashMap Lean.MVarId (Task Lean.Elab.InfoTree))
  (trees : Lean.PersistentArray Lean.Elab.InfoTree) (enabled_1 : Bool)
  (assignment_1 : Lean.PersistentHashMap Lean.MVarId Lean.Elab.InfoTree)
  (lazyAssignment_1 : Lean.PersistentHashMap Lean.MVarId (Task Lean.Elab.InfoTree))
  (trees_1 : Lean.PersistentArray Lean.Elab.InfoTree),
  ({ enabled := enabled, assignment := assignment, lazyAssignment := lazyAssignment, trees := trees } =
      { enabled := enabled_1, assignment := assignment_1, lazyAssignment := lazyAssignment_1, trees := trees_1 }) =
    (enabled = enabled_1 ∧ assignment = assignment_1 ∧ lazyAssignment = lazyAssignment_1 ∧ trees = trees_1)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
PolynormableSpace.iInf : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {t : ι → TopologicalSpace E}, (∀ (i : ι), PolynormableSpace 𝕜 E) → PolynormableSpace 𝕜 E
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Finset.indicator_sum : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [inst : AddCommMonoid β] (s : Finset ι) (t : Set κ) (f : ι → κ → β),
  t.indicator (∑ i ∈ s, f i) = ∑ i ∈ s, t.indicator (f i)
-- Init.Data.Nat.Compare
Nat.isGE_compare : ∀ {a b : ℕ}, (compare a b).isGE = true ↔ b ≤ a
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Reachable.exists_walk_length_eq_edist : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Reachable u v → ∃ p, ↑p.length = G.edist u v
-- Batteries.Data.List.Lemmas
List.insertP.loop.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (a : α) (a_1 : List α), List.insertP.loop p a [] a_1 = (a :: a_1).reverseAux []
-- Mathlib.Data.Countable.Defs
Subtype.countable : ∀ {α : Sort u} [Countable α] {p : α → Prop}, Countable { x // p x }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.compare_maxKey_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {he : (Std.DTreeMap.Const.modify t k f).isEmpty = false},
  cmp ((Std.DTreeMap.Const.modify t k f).maxKey he) (t.maxKey ⋯) = Ordering.eq
-- Mathlib.MeasureTheory.Group.Arithmetic
Finset.aemeasurable_fun_sum : ∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} [inst : AddCommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, AEMeasurable (f i) μ) → AEMeasurable (fun a => ∑ i ∈ s, f i a) μ
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.fun : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.FunDecl pu →
    Lean.Compiler.LCNF.Code pu →
      autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Alt._auto_5 → Lean.Compiler.LCNF.Code pu
-- Mathlib.Algebra.Ring.Pi
NonUnitalRingHom.compLeft_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β) (I : Type u_3) (h : I → α) (a : I), (f.compLeft I) h a = (⇑f ∘ h) a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- `pullback f g` computes the pullback of a pair of morphisms with the same target.  -/
CategoryTheory.Limits.pullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → [CategoryTheory.Limits.HasPullback f g] → C
-- Mathlib.Data.Setoid.Partition
Setoid.isPartition_classes : ∀ {α : Type u_1} (r : Setoid α), Setoid.IsPartition r.classes
-- Std.Data.HashMap.Lemmas
Std.HashMap.singleton_eq_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {p : α × β}, {p} = ∅.insert p.1 p.2
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulOperatorFullAdderInputMkFullAdderOut : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput
    Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderOut
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_ofNat' : ∀ {n : ℕ}, n < UInt8.size → (UInt8.ofNat n).toUInt32 = UInt32.ofNat n
-- Mathlib.Data.Finset.Interval
/-- A function `f` from `Finset α` is strictly antitone if and only if `f (cons a s ha) < f s` for
all `s` and `a ∉ s`.  -/
Finset.strictAnti_iff_forall_cons_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β},
  StrictAnti f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f (Finset.cons a s ha) < f s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∪ m₂)[k]! = m₁[k]!
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.inverseFunctorObjIso_hom : ∀ {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] (e : C ≌ D),
  e.inverseFunctorObjIso.hom = CategoryTheory.CategoryStruct.id (Opposite.op e.inverse)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.B_transpose : ∀ (n : ℕ), (CartanMatrix.B n).transpose = CartanMatrix.C n
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry'.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.Closed X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X ⟹ Y),
  CategoryTheory.MonoidalClosed.uncurry' g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (CategoryTheory.MonoidalClosed.uncurry g)
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_sub_apply : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f g : AdicCompletion I M) (n : ℕ), ↑(f - g) n = ↑f n - ↑g n
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `(α ≫ η ≫ ηs) ≫ θ`  -/
Mathlib.Tactic.BicategoryLike.MkEvalComp.mkEvalCompCons : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalComp m] →
    Mathlib.Tactic.BicategoryLike.Structural →
      Mathlib.Tactic.BicategoryLike.WhiskerLeft →
        Mathlib.Tactic.BicategoryLike.NormalExpr →
          Mathlib.Tactic.BicategoryLike.NormalExpr → Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → m Lean.Expr
-- Init.Data.SInt.Lemmas
Int8.le_minValue_iff : ∀ {a : Int8}, a ≤ Int8.minValue ↔ a = Int8.minValue
-- Mathlib.Topology.List
List.Vector.continuousAt_eraseIdx : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ} {i : Fin (n + 1)} {l : List.Vector α (n + 1)},
  ContinuousAt (List.Vector.eraseIdx i) l
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.mk.injEq : ∀ (toSnapshot : Lean.Language.Snapshot) (stx : Lean.Syntax) (parserState : Lean.Parser.ModuleParserState)
  (elabSnap : Lean.Language.Lean.CommandElaboratingSnapshot)
  (nextCmdSnap? : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot))
  (toSnapshot_1 : Lean.Language.Snapshot) (stx_1 : Lean.Syntax) (parserState_1 : Lean.Parser.ModuleParserState)
  (elabSnap_1 : Lean.Language.Lean.CommandElaboratingSnapshot)
  (nextCmdSnap?_1 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)),
  ({ toSnapshot := toSnapshot, stx := stx, parserState := parserState, elabSnap := elabSnap,
        nextCmdSnap? := nextCmdSnap? } =
      { toSnapshot := toSnapshot_1, stx := stx_1, parserState := parserState_1, elabSnap := elabSnap_1,
        nextCmdSnap? := nextCmdSnap?_1 }) =
    (toSnapshot = toSnapshot_1 ∧
      stx = stx_1 ∧ parserState = parserState_1 ∧ elabSnap = elabSnap_1 ∧ nextCmdSnap? = nextCmdSnap?_1)
-- Mathlib.Data.Set.Basic
/-- Variant of `nonempty_iff_ne_empty` used by `push Not`.  -/
Set.nonempty_iff_empty_ne : ∀ {α : Type u} {s : Set α}, s.Nonempty ↔ ∅ ≠ s
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vadd_finset_inter : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {s t : Finset β}
  {a : α}, a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAt.continuousOn : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {s : Set F} {f' : F → F},
  (∀ x ∈ s, HasGradientAt f (f' x) x) → ContinuousOn f s
-- Mathlib.Algebra.Jordan.Basic
two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add : ∀ {A : Type u_1} [inst : NonUnitalNonAssocCommRing A] [IsCommJordan A] (a b : A),
  2 •
      (⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (a * b)⁆ +
        ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (b * a)⁆) =
    ⁅AddMonoid.End.mulLeft (a * a), AddMonoid.End.mulLeft b⁆ + ⁅AddMonoid.End.mulLeft (b * b), AddMonoid.End.mulLeft a⁆
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₁₀_single : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (g : G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₁₀ A)) fun₀ | g => a) = (A.ρ g⁻¹) a - a
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.piecewise'.eq_1 : ∀ {X : Type u_1} {Z : Type u_3} [inst : TopologicalSpace X] {C₀ C₁ C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁)
  (h₂ : IsClosed C₂) (f₁ : LocallyConstant (↑C₁) Z) (f₂ : LocallyConstant (↑C₂) Z)
  [inst_1 : DecidablePred fun x => x ∈ C₁] (hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩),
  LocallyConstant.piecewise' h₀ h₁ h₂ f₁ f₂ hf =
    LocallyConstant.piecewise ⋯ ⋯ ⋯
      (LocallyConstant.comap { toFun := C₁.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₁)
      (LocallyConstant.comap { toFun := C₂.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₂) ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α},
  t.minKey? = some km → t.contains km = true
-- Init.Data.UInt.Lemmas
UInt64.neg_one_eq : -1 = 18446744073709551615
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.toNorm : {E : Type u_2} → [Norm E] → Norm Eᵒᵈ
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.isInvertible_inverse_iff : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂}, f.inverse.IsInvertible ↔ f.IsInvertible