mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Prod
/-- Multiplying by the trivial algebra from the right does not change the structure.
This is the `AlgEquiv` version of `LinearEquiv.prodUnique` and `RingEquiv.prodZeroRing.symm`.  -/
AlgEquiv.prodUnique : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Semiring B] → [inst_4 : Algebra R B] → [Unique B] → (A × B) ≃ₐ[R] A
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.Hom.opEquiv_apply : ∀ {V : Type u_1} [inst : Quiver V] {X Y : V} (unop : X ⟶ Y), Quiver.Hom.opEquiv unop = Opposite.op unop
-- Mathlib.Data.Nat.Cast.Defs
/-- Computationally friendlier cast than `Nat.unaryCast`, using binary representation.  -/
Nat.binCast : {R : Type u_1} → [Zero R] → [One R] → [Add R] → ℕ → R
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.instIsAffinePullbackSchemeOfIsAffineHom_1 : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsAffineHom g]
  [AlgebraicGeometry.IsAffine X], AlgebraicGeometry.IsAffine (CategoryTheory.Limits.pullback f g)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.topEquiv_symm_apply_coe : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (x : R), ↑(NonUnitalSubsemiring.topEquiv.symm x) = x
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
ImplicitFunctionData.congr_simp : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type u_2) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] (F : Type u_3) [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] (G : Type u_4) [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G], ImplicitFunctionData 𝕜 E F G = ImplicitFunctionData 𝕜 E F G
-- Init.Data.String.Lemmas.Iterate
String.Model.map_get_revPositionsFrom_of_splits : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String},
  p.Splits t₁ t₂ → List.map (fun p => (↑p).get ⋯) (String.Model.revPositionsFrom p) = t₁.toList.reverse
-- Init.Data.Iterators.Basic
Std.Shrink.deflate_inflate : ∀ {α : Type u_1} {x : Std.Shrink α}, Std.Shrink.deflate x.inflate = x
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_prime_order : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α},
  Nat.Prime (orderOf σ) → ∃ n, σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castSucc_Ioo : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc '' Set.Ioo i j = Set.Ioo i.castSucc j.castSucc
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt32.reduceDiv : Lean.Meta.Simp.DSimproc
-- Mathlib.GroupTheory.Exponent
Monoid.order_dvd_exponent : ∀ {G : Type u} [inst : Monoid G] (g : G), orderOf g ∣ Monoid.exponent G
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius_sq : ∀ {n : ℕ}, ArithmeticFunction.moebius n ^ 2 = if Squarefree n then 1 else 0
-- Mathlib.Analysis.Meromorphic.Basic
/-- Finite sums of meromorphic functions are meromorphic.  -/
MeromorphicOn.fun_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {ι : Type u_5} {s : Finset ι} {f : ι → 𝕜 → E},
  (∀ (σ : ι), MeromorphicOn (f σ) U) → MeromorphicOn (fun z => ∑ n ∈ s, f n z) U
-- Mathlib.Data.Complex.Basic
Complex.mk.inj : ∀ {re im re_1 im_1 : ℝ}, { re := re, im := im } = { re := re_1, im := im_1 } → re = re_1 ∧ im = im_1
-- Init.Data.Array.Range
Array.mem_range : ∀ {m n : ℕ}, m ∈ Array.range n ↔ m < n
-- Aesop.Tree.ExtractScript
Aesop.RappRef.extractScriptCore : Aesop.RappRef → Aesop.ExtractScriptM Unit
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addXYZ_Y : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P Q : Fin 3 → R), W'.addXYZ P Q 1 = W'.addY P Q
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.rightUnitor_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.AddGrp C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor G).hom.hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor G.X).hom
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Every object in `ModuleCat k` that `G` acts on is an object in `Rep k G`.  -/
Rep.ActionToRep : (k : Type u) →
  (G : Type v) →
    [inst : Ring k] → [inst_1 : Monoid G] → CategoryTheory.Functor (Action (ModuleCat k) G) (Rep.{w, u, v} k G)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mul_lt_aleph0 : ∀ {a b : Cardinal.{u_1}}, a < Cardinal.aleph0 → b < Cardinal.aleph0 → a * b < Cardinal.aleph0
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.imPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {c : MeasureTheory.ComplexMeasure α} {μ : MeasureTheory.Measure α}
  [self : c.HaveLebesgueDecomposition μ], (MeasureTheory.ComplexMeasure.im c).HaveLebesgueDecomposition μ
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.Compatible.ofValuation : ∀ {S : Type u_3} {Γ : Type u_4} [inst : Ring S] [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation S Γ),
  v.Compatible
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Step.done.sizeOf_spec : ∀ (r : Lean.Meta.Simp.Result), sizeOf (Lean.Meta.Simp.Step.done r) = 1 + sizeOf r
-- Mathlib.Algebra.CharZero.Defs
/-- An additive monoid with one has characteristic zero if the canonical map `ℕ → R` is
injective.  -/
CharZero.cast_injective : ∀ {R : Type u_1} {inst : AddMonoidWithOne R} [self : CharZero R], Function.Injective Nat.cast
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelComparison_map_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)] {Z : C} {h : Y ⟶ Z}
  (w : CategoryTheory.CategoryStruct.comp f h = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison f G)
      (G.map (CategoryTheory.Limits.cokernel.desc f h w)) =
    CategoryTheory.Limits.cokernel.desc (G.map f) (G.map h) ⋯
-- Init.Data.List.Lemmas
List.insert_nil : ∀ {α : Type u_1} [inst : BEq α] (a : α), List.insert a [] = [a]
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.mk.injEq : ∀ (carrier : Type u) [str : Semigroup carrier] (carrier_1 : Type u) (str_1 : Semigroup carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalConvSeq1Indented : Lean.Elab.Tactic.Tactic
-- Std.Data.Internal.List.Defs
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.keys : {α : Type u} → {β : α → Type v} → List ((a : α) × β a) → List α
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.disjointOfDiffUnion.congr_simp : ∀ {α : Type u_1} {C C_1 : Set (Set α)} (e_C : C = C_1) {s s_1 : Set α} (e_s : s = s_1) {I I_1 : Finset (Set α)}
  (e_I : I = I_1) (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C),
  hC.disjointOfDiffUnion hs hI = ⋯.disjointOfDiffUnion ⋯ ⋯
-- Init.Data.Iterators.Lemmas.Producers.List
List.toArray_iter : ∀ {β : Type w} {l : List β}, l.iter.toArray = l.toArray
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop.eq_def : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ),
  p.drop n =
    match v, p, n with
    | .(u), SimpleGraph.Walk.nil, x => SimpleGraph.Walk.nil
    | v, p, 0 => p.copy ⋯ ⋯
    | v, SimpleGraph.Walk.cons h q, n.succ => q.drop n
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- the morphism from the single cochain complex with `Z` in degree `0` is a quasi-isomorphism  -/
CategoryTheory.InjectiveResolution.quasiIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.InjectiveResolution Z),
  QuasiIso self.ι
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.mapA.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.mulEquivProd_apply : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] (x : N ⋊[1] G),
  SemidirectProduct.mulEquivProd x = (x.left, x.right)
-- Mathlib.Order.CompleteLattice.Basic
Prod.snd_sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : SupSet α] [inst_1 : SupSet β] (s : Set (α × β)),
  (sSup s).2 = sSup (Prod.snd '' s)
-- Mathlib.Algebra.Torsor.Basic
Pi.instAddTorsor.eq_1 : ∀ {I : Type u} {fg : I → Type v} [inst : (i : I) → AddGroup (fg i)] {fp : I → Type w}
  [inst_1 : (i : I) → AddTorsor (fg i) (fp i)],
  Pi.instAddTorsor =
    { toAddAction := Pi.addAction', vsub := fun p₁ p₂ i => p₁ i -ᵥ p₂ i, nonempty := ⋯, vsub_vadd' := ⋯,
      vadd_vsub' := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
_private.Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate.0.SSet.ιNormalizedChainComplex.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  X.ιNormalizedChainComplex x =
    CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) ((X.toNormalizedChainComplex R).f n)
-- Init.Data.List.MapIdx
List.mapIdx_eq_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β} {b : β}, List.mapIdx f l = [b] ↔ ∃ a, l = [a] ∧ f 0 a = b
-- Mathlib.Algebra.LinearRecurrence
/-- Defining property of the solution space : `u` is a solution
iff it belongs to the solution space.  -/
LinearRecurrence.is_sol_iff_mem_solSpace : ∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) (u : ℕ → R), E.IsSolution u ↔ u ∈ E.solSpace
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_X_sub_one : ∀ {R : Type u_1} [inst : Ring R] [Nontrivial R] (r : R), (Polynomial.X - Polynomial.C r).IsMonicOfDegree 1
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instSMul.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X], OreLocalization.instSMul = { smul := OreLocalization.smul }
-- Mathlib.MeasureTheory.Order.Group.Lattice
Measurable.abs : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : AddGroup α] [inst_2 : MeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} [MeasurableNeg α] [MeasurableSup₂ α],
  Measurable f → Measurable fun x => |f x|
-- Init.Data.UInt.Lemmas
UInt8.neg_neg : ∀ {a : UInt8}, - -a = a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap! f t).getKey? k = (t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.expr.inj : ∀ {a a_1 : Lean.Widget.CodeWithInfos}, Lean.Widget.MsgEmbed.expr a = Lean.Widget.MsgEmbed.expr a_1 → a = a_1
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.instInhabitedFreeMonoidalCategory : {a : Type u_1} → Inhabited (CategoryTheory.FreeMonoidalCategory a)
-- Mathlib.Algebra.Ring.Defs
add_mul_self_eq : ∀ {α : Type u} [inst : CommSemiring α] (a b : α), (a + b) * (a + b) = a * a + 2 * a * b + b * b
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.ConfigItem.addConstInfo : Lean.Elab.ConfigEval.ConfigItem → Lean.Name → Lean.Elab.TermElabM Unit
-- Mathlib.Topology.SmallInductiveDimension
smallInductiveDimension_of_isEmpty : ∀ (X : Type u_1) [inst : TopologicalSpace X] [IsEmpty X], smallInductiveDimension X = ⊥
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.filterMap_equiv_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  {f : (a : α) → β a → γ a} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap (fun k v => some (f k v)) t ⋯).impl.Equiv (Std.DTreeMap.Internal.Impl.map f t)
-- Init.Data.String.Modify
String.Pos.set.eq_1 : ∀ {s : String} (p : s.Pos) (c : Char) (hp : p ≠ s.endPos),
  p.set c hp =
    if hc : c.utf8Size = 1 ∧ (p.byte hp).utf8ByteSize ⋯ = 1 then
      { toByteArray := s.toByteArray.set p.offset.byteIdx c.toUInt8 ⋯, isValidUTF8 := ⋯ }
    else (s.sliceTo p).copy ++ String.singleton c ++ (s.sliceFrom (p.next hp)).copy
-- Mathlib.RingTheory.DedekindDomain.GaussLemma
IsDedekindDomain.HeightOneSpectrum.intAdicAbv.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 → ∀ {b b_1 : NNReal} (e_b : b = b_1) (hb : 1 < b), v.intAdicAbv hb = v_1.intAdicAbv ⋯
-- Mathlib.RingTheory.DedekindDomain.Instances
instAlgebraAtPrimeFractionRing : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [IsDomain S] →
          [inst_3 : Algebra R S] →
            {P : Ideal R} →
              [inst_4 : P.IsPrime] → [FaithfulSMul R S] → Algebra (Localization.AtPrime P) (FractionRing S)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X : CategoryTheory.SimplicialObject C} {s : X.Splitting}
  {X_1 : CategoryTheory.SimplicialObject C} {s_1 : X_1.Splitting},
  { X := X, s := s } = { X := X_1, s := s_1 } → X = X_1 ∧ s ≍ s_1
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Cowedge.IsColimit.π_desc_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Cowedge F}
  (hc : CategoryTheory.Limits.IsColimit c) {X : C} (f : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
        CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j))
  (j : J) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π c j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cowedge.IsColimit.desc hc f hf) h) =
    CategoryTheory.CategoryStruct.comp (f j) h
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.diagramCompIso_hom_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (W : (J.Cover X)ᵒᵖ) (i : (Opposite.unop W).Arrow),
  CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P X).hom.app W)
      (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (P.comp F)) i) =
    F.map (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index P) i)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_natCast : ∀ (x : NNReal) (n : ℕ), x ^ ↑n = x ^ n
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
AdicCompletion.coe_ofTensorProductEquivOfFiniteNoetherian : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsNoetherianRing R] [inst_4 : Module.Finite R M],
  ↑(AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I M) = AdicCompletion.ofTensorProduct I M
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.Result.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (filtered : Option ProofWidgets.Html) (unfiltered : ProofWidgets.Html) (key : α)
  (pattern : ProofWidgets.Html),
  sizeOf { filtered := filtered, unfiltered := unfiltered, key := key, pattern := pattern } =
    1 + sizeOf filtered + sizeOf unfiltered + sizeOf key + sizeOf pattern
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.lift.congr_simp : ∀ (L : FirstOrder.Language) (ι : Type v) [inst : Preorder ι] (G : ι → Type w) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] {P : Type u₁} [inst_5 : L.Structure P]
  (g g_1 : (i : ι) → L.Embedding (G i) P) (e_g : g = g_1)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x),
  FirstOrder.Language.DirectLimit.lift L ι G f g Hg = FirstOrder.Language.DirectLimit.lift L ι G f g_1 ⋯
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.whiskerLeft_inclLeft_mkNatTrans : ∀ {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 F' : CategoryTheory.Functor (CategoryTheory.Join C D) E}
  (αₗ : (CategoryTheory.Join.inclLeft C D).comp F ⟶ (CategoryTheory.Join.inclLeft C D).comp F')
  (αᵣ : (CategoryTheory.Join.inclRight C D).comp F ⟶ (CategoryTheory.Join.inclRight C D).comp F')
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
          ((CategoryTheory.Prod.snd C D).whiskerLeft αᵣ) =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).whiskerLeft αₗ)
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F'))
      _auto_111✝),
  (CategoryTheory.Join.inclLeft C D).whiskerLeft (CategoryTheory.Join.mkNatTrans αₗ αᵣ h) = αₗ
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.toHom_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (x : CochainComplex.HomComplex.Cocycle K L n),
  CochainComplex.HomComplex.CohomologyClass.toHom (CochainComplex.HomComplex.CohomologyClass.mk x) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.HomComplex.Cocycle.equivHomShift.symm x)
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.toPOUFun.eq_1 : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X),
  f.toPOUFun i x = (f i) x * ∏ᶠ (j : ι) (_ : WellOrderingRel j i), (1 - (f j) x)
-- Mathlib.Data.LawfulXor.Basic
xor_right_eq_id_iff : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] {a : α}, (fun x => x ^^^ a) = id ↔ a = 0
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.kerParam_range_card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α),
  Fintype.card ↥(Equiv.Perm.OnCycleFactors.kerParam g).range =
    (Fintype.card α - g.cycleType.sum).factorial * g.cycleType.prod
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.one_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {a : R} (b : ℕ), Mathlib.Meta.NormNum.IsNat a 1 → a ^ b = a
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_inverse_map_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) {X Y : CategoryTheory.Core D} (f : X ⟶ Y), (E.core.inverse.map f).iso.hom = E.inverse.map f.iso.hom
-- Init.Grind.Norm
Lean.Grind.forall_or_forall : ∀ {α : Sort u} {β : α → Sort v} (p : α → Prop) (q : (a : α) → β a → Prop),
  (∀ (a : α), p a ∨ ∀ (b : β a), q a b) = ∀ (a : α) (b : β a), p a ∨ q a b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.constGet_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (hk : k ∈ m₁) (h : m₁.Equiv m₂),
  Std.DHashMap.Raw.Const.get m₁ k hk = Std.DHashMap.Raw.Const.get m₂ k ⋯
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.ext_iff : ∀ {R : Type u_1} {inst : CommRing R} {x y : RingPreordering R}, x = y ↔ (↑x).carrier = (↑y).carrier
-- Init.Data.Int.Pow
Int.pow_ne_zero : ∀ {n : ℤ} {m : ℕ}, n ≠ 0 → n ^ m ≠ 0
-- Mathlib.Topology.EMetricSpace.Defs
Metric.mem_closedEBall_self : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, x ∈ Metric.closedEBall x ε
-- Mathlib.Probability.Distributions.Pareto
ProbabilityTheory.paretoPDF_of_le : ∀ {t r x : ℝ}, t ≤ x → ProbabilityTheory.paretoPDF t r x = ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
-- Mathlib.Algebra.Notation.Prod
Prod.snd_one : ∀ {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N], 1.2 = 1
-- Batteries.Data.MLList.Basic
/-- Enumerate the elements of a monadic lazy list.  -/
MLList.enum : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → MLList m (ℕ × α)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_exp_pos : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [hμ : NeZero μ],
  MeasureTheory.Integrable (fun x => Real.exp (f x)) μ → 0 < ∫ (x : α), Real.exp (f x) ∂μ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_const_mul : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (r : R) (f : R → R)
  (a : A), autoParam (ContinuousOn f (spectrum R a)) cfc_const_mul._auto_1 → cfc (fun x => r * f x) a = r • cfc f a
-- Init.Core
not_false : ¬False
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` preserves colimits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits.  -/
CategoryTheory.Limits.preservesLimitsOfSize_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.instFieldExtension : (k : Type u_1) →
  [inst : Field k] →
    (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP k p] → (n : ℕ) → Field (FiniteField.Extension k p n)
-- Aesop.Rule
Aesop.NormRuleInfo.mk.injEq : ∀ (penalty penalty_1 : ℤ), ({ penalty := penalty } = { penalty := penalty_1 }) = (penalty = penalty_1)
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.instFunLike : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → FunLike (A ≃ₗc[R] B) A B