mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Basic
LieHom.mk_coe : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h₁ : ∀ (x y : L₁), f (x + y) = f x + f y)
  (h₂ :
    ∀ (m : R) (x : L₁),
      { toFun := ⇑f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₁ }.toFun x)
  (h₃ :
    ∀ {x y : L₁},
      { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun ⁅x, y⁆ =
        ⁅{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun x,
          { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun y⁆),
  { toFun := ⇑f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } = f
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- The fixator of a finite subset of cardinal d in an n-transitive action
acts m transitively on the complement if d + m ≤ n.  -/
SubMulAction.ofFixingSubgroup.isMultiplyPretransitive' : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {m n : ℕ}
  [MulAction.IsMultiplyPretransitive G α n] (s : Set α) [Finite ↑s],
  s.ncard + m ≤ n →
    ↑n ≤ ENat.card α →
      MulAction.IsMultiplyPretransitive (↥(fixingSubgroup G s)) (↥(SubMulAction.ofFixingSubgroup G s)) m
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.formatterForKindUnsafe : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_of_sigmaFinite : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (hm : m ≤ m₀) [hμm : MeasureTheory.SigmaFinite (μ.trim hm)],
  μ[f | m] =
    if MeasureTheory.Integrable f μ then
      if MeasureTheory.StronglyMeasurable f then f
      else MeasureTheory.AEStronglyMeasurable.mk ↑↑(MeasureTheory.condExpL1 hm μ f) ⋯
    else 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
neg_of_add_lt_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddRightReflectLT α] {a b : α}, a + b < b → a < 0
-- Mathlib.Data.PFunctor.Univariate.M
/-- default inhabitant of `CofixA`  -/
PFunctor.Approx.CofixA.default : (F : PFunctor.{uA, uB}) → [Inhabited F.A] → (n : ℕ) → PFunctor.Approx.CofixA F n
-- Init.Data.Option.Lemmas
Option.isEqSome.eq_2 : ∀ {α : Type u_1} [inst : BEq α] (x : α), none.isEqSome x = false
-- Mathlib.Algebra.FreeAlgebra
/-- See note [partially-applied ext lemmas].  -/
FreeAlgebra.hom_ext : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {f g : FreeAlgebra R X →ₐ[R] A}, ⇑f ∘ FreeAlgebra.ι R = ⇑g ∘ FreeAlgebra.ι R → f = g
-- Lean.Meta.DiscrTree.Main
/-- Return true if `e` is one of the following
- `Nat.add _ k` where `isNumeral k`
- `Add.add Nat _ _ k` where `isNumeral k`
- `HAdd.hAdd _ Nat _ _ k` where `isNumeral k`
- `Nat.succ _`
This function assumes `e.isAppOf fName`
 -/
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.isOffset : Lean.Name → Lean.Expr → Lean.MetaM Bool
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertList.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)) (k : α) (v : β k)
  (l_1 : List ((a : α) × β a)),
  Std.Internal.List.insertList l (⟨k, v⟩ :: l_1) =
    Std.Internal.List.insertList (Std.Internal.List.insertEntry k v l) l_1
-- Mathlib.Tactic.Simps.Basic
Simps.instInhabitedConfig : Inhabited Simps.Config
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.Intermediate.zip_inj : ∀ {α₁ α₂ β₁ β₂ : Type w} [inst : Std.Iterator α₁ Id β₁] {it₁ it₁' : Std.Iter β₁}
  {memo memo' : Option { out // ∃ it, it.toIterM.IsPlausibleOutput out }} {it₂ it₂' : Std.Iter β₂},
  Std.Iter.Intermediate.zip it₁ memo it₂ = Std.Iter.Intermediate.zip it₁' memo' it₂' ↔
    it₁ = it₁' ∧ memo = memo' ∧ it₂ = it₂'
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_minValue : Int32.minValue.toNatClampNeg = 0
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
_private.Mathlib.NumberTheory.EllipticDivisibilitySequence.0.complEDS'.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_1 ()
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
CategoryTheory.Abelian.Ext.instModule : {R : Type t} →
  [inst : Ring R] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Abelian C] →
          [CategoryTheory.Linear R C] →
            [inst_4 : CategoryTheory.HasExt C] → {X Y : C} → {n : ℕ} → Module R (CategoryTheory.Abelian.Ext X Y n)
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.mk : (carrier : Type u) → [str : Semigroup carrier] → Semigrp
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.const_smul_self : ∀ {α : Type u_1} {E' : Type u_6} {R : Type u_13} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedRing R]
  {f' : α → E'} {l : Filter α} [inst_2 : Module R E'] [IsBoundedSMul R E'] (c' : R), (fun x => c' • f' x) =O[l] f'
-- Mathlib.Topology.UniformSpace.Cauchy
TotallyBounded.subset : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s₁ s₂ : Set α}, s₁ ⊆ s₂ → TotallyBounded s₂ → TotallyBounded s₁
-- Mathlib.GroupTheory.OreLocalization.OreSet
OreLocalization.oreCondition.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r : R) (s : ↥S),
  OreLocalization.oreCondition r s = ⟨OreLocalization.oreNum r s, ⟨OreLocalization.oreDenom r s, ⋯⟩⟩
-- Mathlib.Order.Category.BddLat
/-- The type of morphisms in `BddLat`.  -/
BddLat.Hom : BddLat → BddLat → Type u
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasSum_mono : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α},
  HasSum f a₁ L → HasSum g a₂ L → f ≤ g → ∀ [L.NeBot], a₁ ≤ a₂
-- Init.GetElem
outOfBounds_eq_default : ∀ {α : Sort u_1} [inst : Inhabited α], outOfBounds = default
-- Init.Data.BitVec.Lemmas
/-- When `m < w`, we give a formula for `(x.rotateLeft m).getMsbD i`.  -/
BitVec.getMsbD_rotateRight_of_lt : ∀ {w n m : ℕ} {x : BitVec w},
  m < w →
    (x.rotateRight m).getMsbD n =
      (decide (n < w) && if n < m % w then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))
-- Mathlib.Algebra.Order.Disjointed
disjointedRec_zero : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {f : ℕ → α} {p : α → Sort u_3}
  (hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)) (h₀ : p (f 0)), Nat.disjointedRec hdiff h₀ = ⋯ ▸ h₀
-- Mathlib.AlgebraicGeometry.Cover.Sigma
AlgebraicGeometry.Scheme.Cover.sigma_X : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] [inst_1 : UnivLE.{v, u}]
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S) (x : PUnit.{v + 1}),
  𝒰.sigma.X x = ∐ 𝒰.X
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.distribSMul : {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) →
      {n : (i : I) → AddZeroClass (f i)} → [(i : I) → DistribSMul α (f i)] → DistribSMul α ((i : I) → f i)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- The generators of the exterior algebra are disjoint from its scalars.  -/
ExteriorAlgebra.ι_range_disjoint_one : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Disjoint (ExteriorAlgebra.ι R).range 1
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.addWeight.eq_2 : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_3} [inst_1 : AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) (x x_1 b : V)
  (p : Quiver.Path x b) (e : b ⟶ x_1),
  Quiver.Path.addWeight w (p.cons e) = Quiver.Path.addWeight (fun {i j} => w) p + w e
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_mem_Icc : ∀ {ι : Type u_1} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f g : (i : ι) → π i}
  [inst_1 : (i : ι) → Preorder (π i)], f ≤ g → s.piecewise f g ∈ Set.Icc f g
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.compatible_iff_sieveCompatible : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {S : CategoryTheory.Sieve X} (x : CategoryTheory.Presieve.FamilyOfElements P S.arrows),
  x.Compatible ↔ x.SieveCompatible
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- If `𝓕 ≤ 𝓖`, the restricted product `Πʳ i, [R i, A i]_[𝓖]` is naturally included in
`Πʳ i, [R i, A i]_[𝓕]`. This is the corresponding map.  -/
RestrictedProduct.inclusion : {ι : Type u_1} →
  (R : ι → Type u_2) →
    (A : (i : ι) → Set (R i)) →
      {𝓕 𝓖 : Filter ι} →
        𝓕 ≤ 𝓖 → RestrictedProduct (fun i => R i) (fun i => A i) 𝓖 → RestrictedProduct (fun i => R i) (fun i => A i) 𝓕
-- Lean.Parser.Do
Lean.Parser.Term.notFollowedByRedefinedTermToken.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.List.Find
List.Sublist.findSome?_eq_none : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {l₁ l₂ : List α},
  l₁.Sublist l₂ → List.findSome? f l₂ = none → List.findSome? f l₁ = none
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.snd_comp_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.snd.comp (Monoid.Coprod.swap M N) = Monoid.Coprod.fst
-- Mathlib.RingTheory.RootsOfUnity.Complex
IsPrimitiveRoot.arg : ∀ {n : ℕ} {ζ : ℂ}, IsPrimitiveRoot ζ n → n ≠ 0 → ∃ i, ζ.arg = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ i.natAbs < n
-- Init.Data.Nat.Lcm
Nat.lcm_dvd_lcm_mul_right_right : ∀ (m n k : ℕ), m.lcm n ∣ m.lcm (n * k)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.values.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : List ((_ : α) × β) → Sort u_3) →
      (x : List ((_ : α) × β)) →
        (Unit → motive []) → ((fst : α) → (v : β) → (l : List ((_ : α) × β)) → motive (⟨fst, v⟩ :: l)) → motive x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRange.mk : ℕ → ℕ → Option Lean.Lsp.FoldingRangeKind → Lean.Lsp.FoldingRange
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_eq_of_eq_mul_right : ∀ {a b c : ℤ}, b ≠ 0 → a = b * c → a.tdiv b = c
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.isDotIdCompletionMethod.visit : Lean.Server.Completion.NameSetModPrivate✝ → Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
/-- If a commutative square `sq` is a pullback square,
then `sq.pullbackCone` is a limit.  -/
CategoryTheory.Square.IsPullback.isLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {sq : CategoryTheory.Square C} → sq.IsPullback → CategoryTheory.Limits.IsLimit sq.pullbackCone
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.step_supports : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : Inhabited Λ] [inst_1 : DecidableEq K]
  (M : Λ → Turing.TM2.Stmt Γ Λ σ) {S : Finset Λ},
  Turing.TM2.Supports M S →
    ∀ {c c' : Turing.TM2.Cfg Γ Λ σ}, c' ∈ Turing.TM2.step M c → c.l ∈ Finset.insertNone S → c'.l ∈ Finset.insertNone S
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a : ℤ),
  CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE✝ t a a ⋯ =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t a)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.dist_eq_zero_of_not_reachable : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, ¬G.Reachable u v → G.dist u v = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry!_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  [inst_1 : Inhabited ((a : α) × β a)],
  Std.Internal.List.getEntry! a (⟨k, v⟩ :: l) = bif k == a then ⟨k, v⟩ else Std.Internal.List.getEntry! a l
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.toArray_eq_fold : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β}, it.toArray = Std.Iter.fold (fun xs out => xs.push out) #[] it
-- Mathlib.Algebra.WithConv
WithConv.symm_congrLinearEquiv_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : AddCommMonoid A] [inst_1 : Semiring R] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] (f : A ≃ₗ[R] B) (x : WithConv B),
  (WithConv.congrLinearEquiv f).symm x = WithConv.toConv (f.symm x.ofConv)
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.mk.sizeOf_spec : ∀ (method : Aesop.ScriptGenerated.Method) (perfect hasMVar : Bool),
  sizeOf { method := method, perfect := perfect, hasMVar := hasMVar } =
    1 + sizeOf method + sizeOf perfect + sizeOf hasMVar
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- Auxiliary lemma for `rpow_abs_le_mul_max_exp`.  -/
ProbabilityTheory.rpow_abs_le_mul_max_exp_of_pos : ∀ (x : ℝ) {t p : ℝ}, 0 ≤ p → 0 < t → |x| ^ p ≤ (p / t) ^ p * max (Real.exp (t * x)) (Real.exp (-t * x))
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Measurable.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x : MeasurableSpace α} {x_1 : MeasurableSpace β}
  {x_2 : MeasurableSpace γ} {g : β → γ} {f : α → β}, Measurable g → Measurable f → Measurable (g ∘ f)
-- Mathlib.Topology.Compactness.Lindelof
eq_open_union_countable : ∀ {X : Type u} [inst : TopologicalSpace X] [HereditarilyLindelofSpace X] {ι : Type u_2} (U : ι → Set X),
  (∀ (i : ι), IsOpen (U i)) → ∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.completelyDistribLattice : {α : Type u_1} → [inst : LE α] → CompletelyDistribLattice (UpperSet α)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get?_eq_get?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] (k : α)
  (l : Std.DTreeMap.Internal.Impl α β), l.get? k = l.get?ₘ k
-- Mathlib.Order.RelSeries
RelSeries.ext : ∀ {α : Type u_1} {r : SetRel α α} {x y : RelSeries r} (length_eq : x.length = y.length),
  x.toFun = y.toFun ∘ Fin.cast ⋯ → x = y
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K]
  (α : LieModule.Weight K (↥H) L), ↑(LieAlgebra.corootSpace ⇑α) = K ∙ LieAlgebra.IsKilling.coroot α
-- Mathlib.Topology.UniformSpace.UniformEmbedding
SeparationQuotient.completeSpace_iff : ∀ {α : Type u} [inst : UniformSpace α], CompleteSpace (SeparationQuotient α) ↔ CompleteSpace α
-- Init.Data.UInt.Lemmas
UInt8.lt_trans : ∀ {a b c : UInt8}, a < b → b < c → a < c
-- Mathlib.Order.Interval.Set.Basic
Set.notMem_Ioo_of_ge : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ≤ c → c ∉ Set.Ioo b a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core0.injEq : ∀ (a zero a_1 zero_1 : Lean.Expr),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core0 a zero =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core0 a_1 zero_1) =
    (a = a_1 ∧ zero = zero_1)
-- Mathlib.GroupTheory.OrderOfElement
nsmulCoprime_zero : ∀ {n : ℕ} {G : Type u_6} [inst : AddGroup G] (h : (Nat.card G).Coprime n), (nsmulCoprime h) 0 = 0
-- Mathlib.Tactic.Push.Attr
/-- Returns the head of an expression.  -/
Mathlib.Tactic.Push.Head.ofExpr? : Lean.Expr → Option Mathlib.Tactic.Push.Head
-- Mathlib.Order.Cover
Eq.wcovBy' : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a = b → b ⩿ a
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.relations.Winv₂ : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (w : X ⟶ Y) (hw : W w),
  CategoryTheory.Localization.Construction.relations W
    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Construction.ψ₂ W w hw)
      (CategoryTheory.Localization.Construction.ψ₁ W w))
    (CategoryTheory.CategoryStruct.id (CategoryTheory.Localization.Construction.ιPaths W Y))
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.topology.eq_1 : ∀ {G : Type u} [inst : Group G] (B : GroupFilterBasis G), B.topology = TopologicalSpace.mkOfNhds B.N
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₂_of_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF], W.b₂ = 0
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.zero_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {b : ℕ}, 0 < b → 0 ^ b = 0
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.measurableSet_eq_fun : ∀ {α : Type u_1} {E : Type u_5} {m : MeasurableSpace α} {f g : α → E} [inst : TopologicalSpace E]
  [TopologicalSpace.MetrizableSpace E],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasurableSet {a | f a = g a}
-- Batteries.Data.Fin.Coding
Fin.decodeSubtype.eq_2 : ∀ (n_2 : ℕ) (P_2 : Fin (n_2 + 1) → Prop) (inst_2 : DecidablePred P_2) (k_2 : ℕ)
  (hk : k_2 < Fin.countP fun x => decide (P_2 x)),
  Fin.decodeSubtype P_2 ⟨k_2, hk⟩ =
    if h0 : P_2 0 then
      have this := ⋯;
      match k_2, hk with
      | 0, hk => ⟨0, h0⟩
      | k.succ, hk =>
        match Fin.decodeSubtype (fun i => P_2 i.succ) ⟨k, ⋯⟩ with
        | ⟨⟨i, hi⟩, hp⟩ => ⟨⟨i + 1, ⋯⟩, hp⟩
    else
      have this := ⋯;
      match Fin.decodeSubtype (fun i => P_2 i.succ) ⟨k_2, ⋯⟩ with
      | ⟨⟨i, hi⟩, hp⟩ => ⟨⟨i + 1, ⋯⟩, hp⟩
-- Mathlib.MeasureTheory.Function.AEEqOfLIntegral
/-- If two a.e.-measurable functions `α × β → ℝ≥0∞` with finite integrals have the same integral
on every rectangle, then they are almost everywhere equal.  -/
MeasureTheory.ae_eq_of_setLIntegral_prod_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {β : Type u_2} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure (α × β)}
  {f g : α × β → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ∫⁻ (x : α × β), f x ∂μ ≠ ⊤ →
        (∀ ⦃s : Set α⦄,
            MeasurableSet s →
              ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ) →
          f =ᵐ[μ] g
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m] (v : m → α)
  (M : Matrix m n α) (x : n), Matrix.vecMul v M x = v ⬝ᵥ fun i => M i x
-- Mathlib.Topology.Order.LeftRightNhds
nhdsLT_basis_Ico_of_exists_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α},
  (∃ b, b < a) → (nhdsWithin a (Set.Iio a)).HasBasis (fun x => x < a) fun x => Set.Ico x a
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Given an affinely independent family of points, a weighted subtraction lies in the
`vectorSpan` of two points given as affine combinations if and only if it is a weighted
subtraction with weights a multiple of the difference between the weights of the two points.  -/
weightedVSub_mem_vectorSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p →
    ∀ {w w₁ w₂ : ι → k} {s : Finset ι},
      ∑ i ∈ s, w i = 0 →
        ∑ i ∈ s, w₁ i = 1 →
          ∑ i ∈ s, w₂ i = 1 →
            ((s.weightedVSub p) w ∈
                vectorSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂} ↔
              ∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ i))
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.mkAddAction.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β),
  FreeAddMonoid.mkAddAction f =
    { vadd := fun l b => List.foldr f b (FreeAddMonoid.toList l), add_vadd := ⋯, zero_vadd := ⋯ }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastUdiv : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : BitVec w)
  (assign : α → Bool) (input : aig.BinaryRefVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv aig input).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv aig input).vec.get idx hidx }⟧ =
          (lhs / rhs).getLsbD idx
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_omega : Cardinal.preBeth Ordinal.omega0 = Cardinal.aleph0
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.coeff_tensorEquiv_apply : ∀ (R : Type u_1) {M : Type u_2} {N : Type u_3} [inst : CommSemiring R]
  (x : TensorProduct R (MonoidAlgebra R M) (MonoidAlgebra R N)),
  ((MonoidAlgebra.tensorEquiv R) x).coeff =
    (finsuppTensorFinsupp' R M N)
      ((TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv R) (MonoidAlgebra.coeffLinearEquiv R)) x)
-- Init.Data.Nat.Order
Nat.instIsLinearOrder : Std.IsLinearOrder ℕ
-- Lean.Meta.Sym.ProofInstInfo
/-- Preprocesses types that used for pattern matching and unification.
 -/
Lean.Meta.Sym.preprocessType : Lean.Expr → optParam Bool false → Lean.MetaM Lean.Expr
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.mul_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : Mul γ] [inst_4 : ContinuousMul γ] (f₁ f₂ : C(β, γ)) (g : C(α, β)),
  (f₁ * f₂).comp g = f₁.comp g * f₂.comp g
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_neg : ∀ {R : Type u_1} [inst : CommRing R] (p : Polynomial R), ↑(-p) = -↑p
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.nonempty_of_isProbabilityMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ],
  Nonempty α
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.mem_map_algebraMap_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {I : Ideal R} {z : S},
  z ∈ Ideal.map (algebraMap R S) I ↔ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.fold.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (acc : aig.Ref) (i : ℕ)
  (s : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Sat.AIG.RefVec.fold.go aig acc i len s f).aig.decls.size),
  (Std.Sat.AIG.RefVec.fold.go aig acc i len s f).aig.decls[idx] = aig.decls[idx]
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.toList_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ},
  Std.ExtDTreeMap.Const.toList (Std.ExtDTreeMap.map f t) =
    List.map (fun p => (p.1, f p.1 p.2)) (Std.ExtDTreeMap.Const.toList t)