mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Defs
mul_eq_mul_right_iff : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [IsRightCancelMulZero M₀] {a b c : M₀}, a * c = b * c ↔ a = b ∨ c = 0
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instIsDominantCompScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsDominant f]
  [AlgebraicGeometry.IsDominant g], AlgebraicGeometry.IsDominant (CategoryTheory.CategoryStruct.comp f g)
-- Std.Internal.Do.Triple.SpecLemmas
/-- Specification for `repeatM`. The user supplies a termination `measure`, an invariant, and a step
`Triple` whose post either continues with a strictly smaller measure or finishes with the `.inr`
invariant.
 -/
Std.Internal.Do.Spec.repeatM : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [Lean.Order.MonadTail m]
  [inst_2 : Std.Internal.Do.Assertion Pred] [inst_3 : Std.Internal.Do.Assertion EPred]
  [inst_4 : Std.Internal.Do.WPMonad m Pred EPred] {init : α} {f : α → m (α ⊕ β)} [inst_5 : Nonempty β]
  (measure : Std.Internal.Do.RepeatVariant α) (inv : Std.Internal.Do.RepeatInvariant α β Pred) (einv : EPred),
  (∀ (a : α),
      ⦃ inv (Sum.inl a) ⦄ f a ⦃ fun r =>
        match r with
        | Sum.inl a' => Lean.Order.meet (Lean.Order.CompleteLattice.ofProp (measure a' < measure a)) (inv (Sum.inl a'))
        | Sum.inr b => inv (Sum.inr b);
        einv ⦄) →
    ⦃ inv (Sum.inl init) ⦄ repeatM f init ⦃ fun b => inv (Sum.inr b); einv ⦄
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.lambdaTelescopeDSimp : {α : Type} → Lean.Expr → (Array Lean.Expr → Lean.Expr → Lean.Meta.SimpM α) → Lean.Meta.SimpM α
-- Mathlib.RingTheory.WittVector.Identities
WittVector.iterate_verschiebung_coeff_eq_zero : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x : WittVector p R) {n m : ℕ},
  m < n → ((⇑WittVector.verschiebung)^[n] x).coeff m = 0
-- Mathlib.Analysis.Complex.Basic
/-- The slit plane includes the open unit ball of radius `1` around `1`.  -/
Complex.mem_slitPlane_of_norm_lt_one : ∀ {z : ℂ}, ‖z‖ < 1 → 1 + z ∈ Complex.slitPlane
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d_sub_two_sub_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L), h.d (-2) (-1) = K.d 1 0
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
/-- **Alias** of `CategoryTheory.LocalizerMorphism.Derives.isIso_of_isRightDerivedFunctor`. -/
CategoryTheory.LocalizerMorphism.Derives.isIso : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H] {D₂ : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  {F : CategoryTheory.Functor C₂ H},
  Φ.Derives F →
    ∀ [Φ.IsRightDerivabilityStructure] {L₂ : CategoryTheory.Functor C₂ D₂} [inst_5 : L₂.IsLocalization W₂]
      {RF : CategoryTheory.Functor D₂ H} (α : F ⟶ L₂.comp RF) (X₁ : C₁) [RF.IsRightDerivedFunctor α W₂],
      CategoryTheory.IsIso (α.app (Φ.functor.obj X₁))
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.RwKey.mk : ℕ → Bool → ℕ → ℕ → String → Lean.Meta.AbstractMVarsResult → Mathlib.Tactic.ClickSuggestions.RwKey
-- Aesop.Forward.State
/-- The cluster's slots.  -/
Aesop.ClusterState.slots : Aesop.ClusterState → Array Aesop.Slot
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
tsum_prod_pow_eq_tsum_sigma : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] (k : ℕ) {r : 𝕜},
  ‖r‖ < 1 → ∑' (d : ℕ+) (c : ℕ+), ↑↑c ^ k * r ^ (↑d * ↑c) = ∑' (e : ℕ+), ↑((ArithmeticFunction.sigma k) ↑e) * r ^ ↑e
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : Inhabited α],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).getKey! k' =
        if compare k k' = Ordering.eq then if (f (t.get? k)).isSome = true then k else default else t.getKey! k'
-- Mathlib.Topology.Constructions
nhds_ofAdd : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X),
  nhds (Multiplicative.ofAdd x) = Filter.map (⇑Multiplicative.ofAdd) (nhds x)
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.Server.shared : Std.Http.Internal.Mock.Server → Std.Http.Internal.Mock.SharedState✝
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveCodiscrete
/-- Since the morphisms in a codiscrete category do not carry information, an n-simplex of
coherentIso is equivalent to an X-vector of length (n + 1).  -/
CategoryTheory.Codiscrete.equivFun : {X : Type u} →
  {n : ℕ} → (CategoryTheory.nerve (CategoryTheory.Codiscrete X)).obj (Opposite.op { len := n }) ≃ (Fin (n + 1) → X)
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrRight_refl : ∀ {M : Type u_4} {N : Type u_8} [inst : MulOneClass M] [inst_1 : CommMonoid N],
  (MulEquiv.refl N).monoidHomCongrRight = MulEquiv.refl (M →* N)
-- Mathlib.Algebra.Group.Basic
mul_one_div : ∀ {G : Type u_3} [inst : DivInvMonoid G] (x y : G), x * (1 / y) = x / y
-- Init.Data.Array.Find
Array.isSome_idxOf? : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {a : α}, (xs.idxOf? a).isSome = true ↔ a ∈ xs
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalCoprimeFactorizationRing.factor₂.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  Polynomial.UniversalCoprimeFactorizationRing.factor₂ m k hn p =
    (Polynomial.UniversalFactorizationRing.factor₂ m k hn p).map
      (algebraMap (Polynomial.UniversalFactorizationRing m k hn p)
        (Polynomial.UniversalCoprimeFactorizationRing m k hn p))
-- Init.Data.SInt.Basic
/-- Negates word-sized signed integers. Usually accessed via the `-` prefix operator.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.neg : ISize → ISize
-- Mathlib.Tactic.Ring.PNat
Mathlib.Tactic.Ring.instCSLiftValPNatNatSuccPNatHAddOfNat : ∀ {n : ℕ}, Mathlib.Tactic.Ring.CSLiftVal n.succPNat (n + 1)
-- Mathlib.SetTheory.Ordinal.Rank
Acc.rank_eq : ∀ {α : Type u} {a : α} {r : α → α → Prop} (h : Acc r a), h.rank = ⨆ b, Order.succ ⋯.rank
-- Mathlib.CategoryTheory.Monad.Limits
/-- The forgetful functor from the Eilenberg-Moore category for a monad creates any colimit
which the monad itself preserves.
 -/
CategoryTheory.monadicCreatesColimitOfPreservesColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} J] →
            (R : CategoryTheory.Functor D C) →
              (K : CategoryTheory.Functor J D) →
                [inst_3 : CategoryTheory.MonadicRightAdjoint R] →
                  [CategoryTheory.Limits.PreservesColimit (K.comp R) ((CategoryTheory.monadicLeftAdjoint R).comp R)] →
                    [CategoryTheory.Limits.PreservesColimit
                          ((K.comp R).comp ((CategoryTheory.monadicLeftAdjoint R).comp R))
                          ((CategoryTheory.monadicLeftAdjoint R).comp R)] →
                      CategoryTheory.CreatesColimit K R
-- Mathlib.Topology.Connected.PathConnected
pathConnectedSpace_iff : ∀ (X : Type u_4) [inst : TopologicalSpace X], PathConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Joined x y
-- Lean.Server.Requests
Lean.Server.LspResponse.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (response : α) (isComplete : Bool),
  sizeOf { response := response, isComplete := isComplete } = 1 + sizeOf response + sizeOf isComplete
-- Batteries.Tactic.Trans
/-- refining `tgt ← mkAppM' rel #[x, z]` dropping more arguments if possible  -/
Batteries.Tactic.getExplicitRelArgCore : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mem_sup_left : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M} {x : M}, x ∈ S → x ∈ S ⊔ T
-- Lean.Meta.Sym.Pattern
/-- Substitutes uvars in `u` with their assignments.  -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.substAssignedUVars : Array (Option Lean.Level) → Lean.Level → Lean.Level
-- Mathlib.Analysis.Calculus.LHopital
HasDerivAt.lhopital_zero_atTop_on_Ioi : ∀ {a : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  (∀ x ∈ Set.Ioi a, HasDerivAt f (f' x) x) →
    (∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x) →
      (∀ x ∈ Set.Ioi a, g' x ≠ 0) →
        Filter.Tendsto f Filter.atTop (nhds 0) →
          Filter.Tendsto g Filter.atTop (nhds 0) →
            Filter.Tendsto (fun x => f' x / g' x) Filter.atTop l → Filter.Tendsto (fun x => f x / g x) Filter.atTop l
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.indicator_const : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : Zero β] {s : Set α},
  Filter.EventuallyConst s l → ∀ (c : β), Filter.EventuallyConst (s.indicator fun x => c) l
-- Mathlib.Analysis.InnerProductSpace.Projection.Minimal
/-- Characterization of minimizers in the projection on a subspace, in the real case.
Let `u` be a point in a real inner product space, and let `K` be a nonempty subspace.
Then point `v` minimizes the distance `‖u - v‖` over points in `K` if and only if
for all `w ∈ K`, `⟪u - v, w⟫ = 0` (i.e., `u - v` is orthogonal to the subspace `K`).
This is superseded by `norm_eq_iInf_iff_inner_eq_zero` that gives the same conclusion over
any `RCLike` field.
 -/
Submodule.norm_eq_iInf_iff_real_inner_eq_zero : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (K : Submodule ℝ F) {u v : F},
  v ∈ K → (‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, inner ℝ (u - v) w = 0)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffineAddEquiv_apply : ∀ {F : Type u} [inst : Field F] (W : WeierstrassCurve.Projective F) [inst_1 : DecidableEq F] (P : W.Point),
  (WeierstrassCurve.Projective.Point.toAffineAddEquiv W) P = P.toAffineLift
-- Mathlib.NumberTheory.Height.NumberField
NumberField.prod_archAbsVal_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {M : Type u_2} [inst_2 : CommMonoid M]
  (f : AbsoluteValue K ℝ → M), (Multiset.map f Height.AdmissibleAbsValues.archAbsVal).prod = ∏ v, f ↑v ^ v.mult
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.insertManyIfNewUnit_list_equiv_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} {l : List α},
  (Std.DHashMap.Const.insertManyIfNewUnit m l).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) m l)
-- Init.Grind.Offset
Lean.Grind.Nat.ro_eq_true_of_ro : ∀ (u v k₁ k₂ : ℕ), Lean.Grind.isLE k₁ k₂ = true → u ≤ v + k₁ → (u ≤ v + k₂) = True
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
Multiset.smul_prod : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : CommMonoid N] [inst_2 : MulAction M N] [IsScalarTower M N N]
  [SMulCommClass M N N] (s : Multiset N) (b : M), b ^ s.card • s.prod = (Multiset.map (fun x => b • x) s).prod
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- the family of type (I) simplices  -/
SSet.Subcomplex.PairingCore.simplex : {X : SSet} → {A : X.Subcomplex} → (self : A.PairingCore) → (s : self.ι) → X.obj (Opposite.op { len := self.dim s + 1 })
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).contains k' = if cmp k k' = Ordering.eq then (f (t.get? k)).isSome else t.contains k'
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.instPreadditiveOpposite : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Preadditive C] → CategoryTheory.Preadditive Cᵒᵖ
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.lintegral_tilted : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ℝ) (g : α → ENNReal),
  ∫⁻ (x : α), g x ∂μ.tilted f = ∫⁻ (x : α), ENNReal.ofReal (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) * g x ∂μ
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.oneEquiv_ιMulti : ∀ {R : Type u} [inst : CommRing R] {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Fin 1 → M),
  (exteriorPower.oneEquiv R M) ((exteriorPower.ιMulti R 1) f) = f 0
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.eq_symm_comp : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] {α : Type u_3} (e : M ≃ₜ+ N) (f : α → M) (g : α → N), f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
-- Mathlib.Algebra.Lie.Free
_private.Mathlib.Algebra.Lie.Free.0.«termLib.of» : Lean.ParserDescr
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_5 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.reverse with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_5 ()
-- Mathlib.MeasureTheory.Measure.MeasuredSets
/-- Measure on `MeasuredSets` is a 1-lipschitz function.

We cannot state this in terms of `LipschitzWith`, because `ℝ≥0∞` is not a `PseudoEMetricSpace`.  -/
MeasureTheory.MeasuredSets.sub_le_edist : ∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s t : MeasureTheory.MeasuredSets μ),
  μ ↑s - μ ↑t ≤ edist s t
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_1.eq_4 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_4 ()
-- Mathlib.RingTheory.LocalIso
Algebra.IsLocalIso.instOfIsStandardOpenImmersion : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [Algebra.IsStandardOpenImmersion R S], Algebra.IsLocalIso R S
-- Mathlib.RingTheory.Ideal.Colon
Submodule.mem_colon_span_singleton : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {x : M} {r : R}, r ∈ N.colon ↑(R ∙ x) ↔ r • x ∈ N
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_updateRow_smul_left : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R)
  (j : n) (s : R) (u : n → R), ((s • M).updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateRow j u).det
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.add_subset_iff_left : ∀ {α : Type u_2} [inst : Add α] {s t u : Set α}, s + t ⊆ u ↔ ∀ a ∈ s, a +ᵥ t ⊆ u
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.addFn? : Lean.Meta.Sym.Arith.Ring → Option Lean.Expr
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Implementation detail for `widePullbackShapeEquiv`.  -/
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.widePullbackShapeEquivMap : {J : Type u_1} →
  (x y : CategoryTheory.Limits.WidePullbackShape J) →
    (x ⟶ y) ≃
      (CategoryTheory.WithTerminal.widePullbackShapeEquivObj✝ x ⟶
        CategoryTheory.WithTerminal.widePullbackShapeEquivObj✝ y)
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.addEquivAddHaarChar_smul_integral_map : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalAddGroup G] [inst_5 : LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure]
  [μ.Regular] {f : G → ℝ} (φ : G ≃ₜ+ G),
  MeasureTheory.addEquivAddHaarChar φ • ∫ (a : G), f a ∂MeasureTheory.Measure.map (⇑φ) μ = ∫ (a : G), f a ∂μ
-- Aesop.Tree.TreeM
Aesop.Tree.root : Aesop.Tree → Aesop.MVarClusterRef
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {v : β},
  List.find? (fun x => cmp x.1 k == Ordering.eq) t.toList = some (k', v) ↔ t.getKey? k = some k' ∧ t[k]? = some v
-- Mathlib.Combinatorics.Enumerative.Composition
_private.Mathlib.Combinatorics.Enumerative.Composition.0.Composition.recOnSingleAppend.match_3.splitter : (motive : (n : ℕ) → Composition n → Sort u_1) →
  (n : ℕ) →
    (c : Composition n) →
      ((blocks : List ℕ) →
          (blocks_pos : ∀ {i : ℕ}, i ∈ blocks → 0 < i) →
            motive blocks.sum { blocks := blocks, blocks_pos := blocks_pos, blocks_sum := ⋯ }) →
        motive n c
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)], k ∈ t₂ → (t₁ ∩ t₂).get! k = t₁.get! k
-- Init.Data.Format.Basic
Std.Format.FlattenAllowability.disallow : Std.Format.FlattenAllowability
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false} {hc : t.minKey he ∈ t}, t.getKey (t.minKey he) hc = t.minKey he
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nhdsWithin_Ioi_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a b : α} [ClosedIicTopology α], (nhdsWithin a (Set.Ioi b)).IsMeasurablyGenerated
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority.percent.sizeOf_spec : ∀ (p : Aesop.Percent), sizeOf (Aesop.Frontend.Priority.percent p) = 1 + sizeOf p
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcompose₂_map_right_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor H D')
  {X Y :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)}
  (φ : X ⟶ Y) (X_1 : D),
  ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).map φ).right.app X_1 = G.map (φ.right.app X_1)
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.hom_ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' : Φ.LeftResolution X₂} {φ₁ φ₂ : L ⟶ L'}, φ₁.f = φ₂.f → φ₁ = φ₂
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.neg : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : SubtractionCommMonoid β] {A : Set α} {B : Set β}
  {f : α → β} {n : ℕ}, IsAddFreimanHom n A B f → IsAddFreimanHom n A (-B) (-f)
-- Batteries.Data.List.Basic
List.foldrIdxTR.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : ℕ → α → β → β) (init : β) (l : List α) (start : ℕ),
  List.foldrIdxTR f init l start =
    (List.foldr
        (fun a x =>
          match x with
          | (acc, n) => (f (n - 1) a acc, n - 1))
        (init, start + l.length) l).1
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.mono_measure : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s : Set α} {μ ν : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f s ν → μ ≤ ν → MeasureTheory.IntegrableOn f s μ
-- Mathlib.LinearAlgebra.Dimension.Localization
/-- The **rank-nullity theorem** for commutative domains. Also see `rank_quotient_add_rank`.  -/
rank_quotient_add_rank_of_isDomain : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  (M' : Submodule R M), Module.rank R (M ⧸ M') + Module.rank R ↥M' = Module.rank R M
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.CommandCodeActionEntry.mk.sizeOf_spec : ∀ (declName : Lean.Name) (cmdKinds : Array Lean.Name),
  sizeOf { declName := declName, cmdKinds := cmdKinds } = 1 + sizeOf declName + sizeOf cmdKinds
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- A constant function is uniformly integrable.  -/
MeasureTheory.unifIntegrable_const : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {g : α → β},
  1 ≤ p → p ≠ ⊤ → MeasureTheory.MemLp g p μ → MeasureTheory.UnifIntegrable (fun x => g) p μ
-- Init.Data.Array.Lemmas
Array.size_shrink : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, (xs.shrink i).size = min i xs.size
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.coeff_inv_units : ∀ {R : Type u} [inst : Field R] (u : (Polynomial R)ˣ) (n : ℕ), ((↑u).coeff n)⁻¹ = (↑u⁻¹).coeff n
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.snd_apply : ∀ (M : Type u_1) (α : Type u_2) (β : Type u_3) [inst : SMul M α] [inst_1 : SMul M β],
  ⇑(MulActionHom.snd M α β) = Prod.snd
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.toGeneralLinearGroup_toLinearEquiv_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (u : SpecialLinearGroup R V),
  (SpecialLinearGroup.toGeneralLinearGroup u).toLinearEquiv = SpecialLinearGroup.toLinearEquiv u
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The third projection `Triangle C ⥤ C`.  -/
CategoryTheory.Pretriangulated.Triangle.π₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] → CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C) C
-- Mathlib.Order.Interval.Finset.Basic
/-- A sort of triangle inequality.  -/
Finset.uIcc_subset_uIcc_union_uIcc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c : α},
  Finset.uIcc a c ⊆ Finset.uIcc a b ∪ Finset.uIcc b c
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.mem_invtSubmodule : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p : Submodule R M}, p ∈ f.invtSubmodule ↔ p ≤ Submodule.comap f p