mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Multiset.Fintype
/-- If `s = t` then there's an equivalence between the appropriate types.
 -/
Multiset.cast : {α : Type u_1} → [inst : DecidableEq α] → {s t : Multiset α} → s = t → s.ToType ≃ t.ToType
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ (i : Fin (n + 1)),
      (s.signedInfDist i) (s.excenter signs) = (if i ∈ signs then -1 else 1) * (∑ j, s.excenterWeightsUnnorm signs j)⁻¹
-- Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject
CategoryTheory.InjectiveObject.instHasBinaryBiproducts : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasBinaryBiproducts C],
  CategoryTheory.Limits.HasBinaryBiproducts (CategoryTheory.InjectiveObject C)
-- Mathlib.Algebra.FreeMonoid.Basic
/-- The only invertible element of the free monoid is 1; this instance enables `units_eq_one`.  -/
FreeMonoid.uniqueUnits : {α : Type u_1} → Unique (FreeMonoid α)ˣ
-- Mathlib.Logic.Function.Basic
Function.Injective2.uncurry : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {f : α → β → γ},
  Function.Injective2 f → Function.Injective (Function.uncurry f)
-- Mathlib.LinearAlgebra.Dimension.Localization
IsLocalization.rank_eq : ∀ {R : Type uR} (S : Type uS) {N : Type uN} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] [inst_4 : Algebra R S] [inst_5 : Module S N] [IsScalarTower R S N] (p : Submonoid R)
  [IsLocalization p S], p ≤ nonZeroDivisors R → Module.rank S N = Module.rank R N
-- Init.GrindInstances.ToInt
Lean.Grind.instAddISizeSintNumBits : Lean.Grind.ToInt.Add ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.tendsto_nearestPt : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  {e : ℕ → α} {x : α},
  x ∈ closure (Set.range e) → Filter.Tendsto (fun N => (MeasureTheory.SimpleFunc.nearestPt e N) x) Filter.atTop (nhds x)
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.smulCommClass_right : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MulOneClass M'] [inst_1 : SMul α β] [inst_2 : SMul M' β]
  [SMulCommClass α M' β] (S : Submonoid M'), SMulCommClass α (↥S) β
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.im_pos : ∀ (z : UpperHalfPlane), 0 < z.im
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_exact.injEq : ∀ (lhs : Bool) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) (lhs_1 : Bool) (c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.simp_exact lhs c₁ c₂ = Lean.Meta.Grind.AC.EqCnstrProof.simp_exact lhs_1 c₁_1 c₂_1) =
    (lhs = lhs_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.instIsGaussianMapHAdd_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] (c : E),
  ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (fun x => c + x) μ)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.abs_norm_eq_max_natAbs : ∀ (n : ℕ), ‖![1, ↑n + 1]‖ = ↑n + 1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- The integral of the derivative of a product of two maps.
For improper integrals, see `MeasureTheory.integral_deriv_mul_eq_sub`,
`MeasureTheory.integral_Ioi_deriv_mul_eq_sub`, and `MeasureTheory.integral_Iic_deriv_mul_eq_sub`.  -/
intervalIntegral.integral_deriv_mul_eq_sub_of_hasDeriv_right : ∀ {a b : ℝ} {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A},
  ContinuousOn u (Set.uIcc a b) →
    ContinuousOn v (Set.uIcc a b) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) →
        (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x) →
          IntervalIntegrable u' MeasureTheory.volume a b →
            IntervalIntegrable v' MeasureTheory.volume a b →
              ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
-- Mathlib.AlgebraicGeometry.Gluing
/-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`.
```
Vᵢⱼ ⟶ Uᵢ
 |      |
 ↓      ↓
 Uⱼ ⟶ X
```
 -/
AlgebraicGeometry.Scheme.GlueData.vPullbackConeIsLimit : (D : AlgebraicGeometry.Scheme.GlueData) → (i j : D.J) → CategoryTheory.Limits.IsLimit (D.vPullbackCone i j)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] (f : α →o β)
  (hf :
    ∀ (c : OmegaCompletePartialOrder.Chain α),
      f.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map f)),
  ⇑{ toOrderHom := f, map_ωSup' := hf } = ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S}
  (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.equalizer.ι
          (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
            (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
          (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
            (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
        (CategoryTheory.Limits.pullback.fst s v)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.equalizer.ι f g)
        (CategoryTheory.Limits.pullback.fst s v))
      (CategoryTheory.Limits.equalizer.ι f g)
-- Mathlib.Order.ULift
ULift.up_sup : ∀ {α : Type u} [inst : Max α] (a b : α), { down := a ⊔ b } = { down := a } ⊔ { down := b }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.IsMinimal.mk : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K},
  MaximalFor (fun C => WeierstrassCurve.IsIntegral R (C • W)) (fun C => WeierstrassCurve.valuation_Δ_aux R (C • W)) 1 →
    WeierstrassCurve.IsMinimal R W
-- Mathlib.Algebra.Group.Action.Defs
AddSemiconjBy.vadd_left : ∀ {M : Type u_1} {α : Type u_5} [inst : VAdd M α] [inst_1 : Add α] [VAddCommClass M α α] [VAddAssocClass M α α]
  {x a b : α}, AddSemiconjBy x a b → ∀ (r : M), AddSemiconjBy (r +ᵥ x) a b
-- Mathlib.Data.Fintype.Sum
Finset.toLeft_univ : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype α] [inst_1 : Fintype β], Finset.univ.toLeft = Finset.univ
-- Mathlib.GroupTheory.Congruence.Hom
/-- The kernel of an additive homomorphism as an additive congruence relation.  -/
AddCon.ker : {M : Type u_1} →
  {N : Type u_2} →
    {F : Type u_4} → [inst : Add M] → [inst_1 : Add N] → [inst_2 : FunLike F M N] → [AddHomClass F M N] → F → AddCon M
-- Mathlib.Data.Nat.DvdSequence
IsDvdSequence.smul' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Dvd α] [inst_1 : Monoid β] [inst_2 : Monoid γ] {f : α → β}
  {g : α → γ} [inst_3 : SMul β γ] [IsScalarTower β γ γ] [IsScalarTower β β γ] [SMulCommClass β γ γ],
  IsDvdSequence f → IsDvdSequence g → IsDvdSequence (f • g)
-- Mathlib.Algebra.Quandle
Rack.act_invAct_eq : ∀ {R : Type u_1} [inst : Rack R] (x y : R), Shelf.act x (Rack.invAct x y) = y
-- Mathlib.Data.ZMod.QuotientGroup
/-- See also `Fintype.card_zpowers`.  -/
Nat.card_zpowers : ∀ {α : Type u_3} [inst : Group α] (a : α), Nat.card ↥(Subgroup.zpowers a) = orderOf a
-- Init.Data.String.Lemmas.Pattern.Split.Pred
String.Slice.toList_splitToSubslice_bool : ∀ {s : String.Slice} {p : Char → Bool},
  List.map (String.Slice.copy ∘ String.Slice.Subslice.toSlice) (s.splitToSubslice p).toList =
    List.map String.ofList (List.splitOnP p s.copy.toList)
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.State.mk.inj : ∀ {visitedLevel : Lean.LevelSet} {visitedExpr : Lean.ExprSet} {result : Array Lean.LMVarId}
  {visitedLevel_1 : Lean.LevelSet} {visitedExpr_1 : Lean.ExprSet} {result_1 : Array Lean.LMVarId},
  { visitedLevel := visitedLevel, visitedExpr := visitedExpr, result := result } =
      { visitedLevel := visitedLevel_1, visitedExpr := visitedExpr_1, result := result_1 } →
    visitedLevel = visitedLevel_1 ∧ visitedExpr = visitedExpr_1 ∧ result = result_1
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_X_sub_C : ∀ {R : Type u} [inst : Ring R] (c : R), Polynomial.derivative (Polynomial.X - Polynomial.C c) = 1
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.add_pf_add_gt : ∀ {R : Type u_1} [inst : CommSemiring R] {a b₂ c : R} (b₁ : R), a + b₂ = c → a + (b₁ + b₂) = b₁ + c
-- Mathlib.Analysis.Normed.Group.Constructions
nnnorm_toMul : ∀ {E : Type u_2} [inst : NNNorm E] (x : Additive E), ‖Additive.toMul x‖₊ = ‖x‖₊
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.insertReplacementForMainFns : Lean.Elab.Term.MutualClosure.Replacement →
  Array Lean.Expr → Array Lean.Elab.DefViewElabHeader → Array Lean.Expr → Lean.Elab.Term.MutualClosure.Replacement
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_iSup_of_mem : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_2} {S : ι → Subgroup G} (i : ι) {x : G}, x ∈ S i → x ∈ iSup S
-- Mathlib.Algebra.Group.Nat.Range
Finset.range_add : ∀ (a b : ℕ), Finset.range (a + b) = Finset.range a ∪ Finset.map (addLeftEmbedding a) (Finset.range b)
-- Mathlib.Order.Bounds.Basic
isLUB_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → IsLUB (Set.Icc a b) b
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} (f : (i : ι) → X i ⟶ S) {ι' : Type t'} {X' : ι' → C} (f' : (i' : ι') → X' i' ⟶ S),
  CategoryTheory.Sieve.ofArrows X f = CategoryTheory.Sieve.ofArrows X' f' →
    ∃ e, Nonempty ((F.toDescentData f).comp e.functor ≅ F.toDescentData f')
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
max_mul_mul_le_max_mul_max' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] [MulLeftMono α] [MulRightMono α] {a b c d : α},
  max (a * b) (c * d) ≤ max a c * max b d
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_le_minKeyD_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).isEmpty = false → ∀ {fallback : α}, (cmp (t.minKeyD fallback) ((t.erase k).minKeyD fallback)).isLE = true
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
/-- If `γ` is an integral curve of a vector field `v`, then `γ t` is tangent to `v (γ t)` when
expressed in the local chart around the initial point `γ t₀`.  -/
IsMIntegralCurveOn.hasDerivWithinAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {s : Set ℝ} {t₀ : ℝ} [inst_5 : IsManifold I 1 M],
  IsMIntegralCurveOn γ v s →
    ∀ {t : ℝ},
      t ∈ s →
        γ t ∈ (extChartAt I (γ t₀)).source →
          HasDerivWithinAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) s t
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
/-- All functors `F : J ⥤ C` from all small `J` have conical limits  -/
CategoryTheory.Enriched.HasConicalLimitsOfSize.hasConicalLimitsOfShape : ∀ {V : outParam (Type u')} {inst : CategoryTheory.Category.{v', u'} V} {inst_1 : CategoryTheory.MonoidalCategory V}
  {C : Type u} {inst_2 : CategoryTheory.Category.{v, u} C} {inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C}
  [self : CategoryTheory.Enriched.HasConicalLimitsOfSize.{v₁, u₁, v', v, u, u'} V C] (J : Type u₁)
  [inst_4 : CategoryTheory.Category.{v₁, u₁} J], CategoryTheory.Enriched.HasConicalLimitsOfShape J V C
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'_zero : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS' b c d 0 = 0
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- `SimpleFunc.lintegral` depends only on the measures of `f ⁻¹' {y}`.  -/
MeasureTheory.SimpleFunc.lintegral_eq_of_measure_preimage : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasurableSpace β]
  {f : MeasureTheory.SimpleFunc α ENNReal} {g : MeasureTheory.SimpleFunc β ENNReal} {ν : MeasureTheory.Measure β},
  (∀ (y : ENNReal), μ (⇑f ⁻¹' {y}) = ν (⇑g ⁻¹' {y})) → f.lintegral μ = g.lintegral ν
-- Init.Data.Nat.Lemmas
Nat.mul_self_inj : ∀ {m n : ℕ}, m * m = n * n ↔ m = n
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicIntInterval.default : Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval
-- Mathlib.Data.Nat.Prime.Basic
Nat.prime_eq_prime_of_dvd_pow : ∀ {m p q : ℕ}, Nat.Prime p → Nat.Prime q → p ∣ q ^ m → p = q
-- Mathlib.Analysis.Quaternion
Quaternion.norm_star : ∀ (a : Quaternion ℝ), ‖star a‖ = ‖a‖
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_roc_eq_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m<...=n).toArray[i]! = 0 ↔ (n - m).toNat ≤ i ∨ m + ↑i = -1
-- Mathlib.Topology.Constructions
IsClosedMap.mapsToRestrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsClosedMap f →
    ∀ {s : Set X} {t : Set Y}, IsClosed s → ∀ (ht : Set.MapsTo f s t), IsClosedMap (Set.MapsTo.restrict f s t ht)
-- Mathlib.GroupTheory.Finiteness
/-- A group if finitely generated if and only if there exists a surjective homomorphism from a
`FreeGroup` on an arbitrary finite type `α` to the group.  -/
Group.fg_iff_exists_freeGroup_hom_surjective_finite : ∀ {G : Type u_3} [inst : Group G], Group.FG G ↔ ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.toEnd_module_end : ∀ (R : Type u) (M : Type w) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  LieModule.toEnd R (Module.End R M) M = LieHom.id
-- Init.System.Platform
System.Platform.sixteen_le_numBits : 16 ≤ System.Platform.numBits
-- Init.Data.Dyadic.Inv
/-- `invAtPrec x prec` is the special case `divAtPrec 1 x prec` of dyadic division.  -/
Dyadic.invAtPrec_eq_divAtPrec_one : ∀ (x : Dyadic) (prec : ℤ), x.invAtPrec prec = Dyadic.divAtPrec 1 x prec
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₂₃Functor_obj_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) {X Y : C₁} (f : X ⟶ Y)
  (Y_1 : C₃) (X_1 : C₂),
  (((CategoryTheory.Functor.flip₂₃Functor.obj F).map f).app Y_1).app X_1 = ((F.map f).app X_1).app Y_1
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.lift_additive : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive],
  (CategoryTheory.Mat_.lift F).Additive
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` reflects isomorphisms and we can lift any limit cone to a limit cone,
then `F` creates limits.
In particular here we don't need to assume that F reflects limits.
 -/
CategoryTheory.createsLimitOfReflectsIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.ReflectsIsomorphisms] →
                  ((c : CategoryTheory.Limits.Cone (K.comp F)) →
                      (t : CategoryTheory.Limits.IsLimit c) → CategoryTheory.LiftsToLimit K F c t) →
                    CategoryTheory.CreatesLimit K F
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.equivMapDomain_refl : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] (l : SkewMonoidAlgebra k G),
  SkewMonoidAlgebra.equivMapDomain (Equiv.refl G) l = l
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.exists_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    ∀ {W : C} (h : X ⟶ W) (k : Y ⟶ W),
      CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k →
        ∃ d, CategoryTheory.CategoryStruct.comp inl d = h ∧ CategoryTheory.CategoryStruct.comp inr d = k
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.μ_comp_assoc : ∀ {G : Type v} [inst : Monoid G] (X Y Z : Action (Type w) G) {k : Type u} [inst_1 : CommSemiring k],
  ((Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom).comp
          (Representation.LinearizeMonoidal.μ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)).comp
      (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z)
        (Representation.LinearizeMonoidal.μ X Y)) =
    ((Representation.LinearizeMonoidal.μ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).comp
          (Representation.IntertwiningMap.lTensor (Representation.linearize k G X)
            (Representation.LinearizeMonoidal.μ Y Z))).comp
      ↑(Representation.TensorProduct.assoc (Representation.linearize k G X) (Representation.linearize k G Y)
          (Representation.linearize k G Z))
-- Mathlib.Order.BourbakiWitt
/-- `cSup` is a lower bound of the set of upper bounds of the nonempty chain  -/
ChainCompletePartialOrder.cSup_le : ∀ {α : Type u_4} [self : ChainCompletePartialOrder α] (c : NonemptyChain α) (x : α),
  (∀ y ∈ c.carrier, y ≤ x) → ChainCompletePartialOrder.cSup c ≤ x
-- Mathlib.LinearAlgebra.Reflection
Module.reflection_apply_self : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} (h : f x = 2), (Module.reflection h) x = -x
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.continuous_mk : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] {N : AddSubgroup G}, Continuous QuotientAddGroup.mk
-- Mathlib.Data.Finsupp.Single
Equiv.finsuppUnique_symm_apply_apply : ∀ {M : Type u_5} [inst : Zero M] {ι : Type u_13} [inst_1 : Unique ι] (a : M) (a_1 : ι),
  (Equiv.finsuppUnique.symm a) a_1 = a
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.mapTR.loop.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (a : α) (as : List α) (bs : List β)
  (h_1 : (bs : List β) → motive [] bs) (h_2 : (a : α) → (as : List α) → (bs : List β) → motive (a :: as) bs),
  (match a :: as, bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_2 a as bs
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        ∀ {v : β}, List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (m.insertMany l)[k']! = v
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eval_basis_self : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι},
  Set.InjOn v ↑s → i ∈ s → Polynomial.eval (v i) (Lagrange.basis s v i) = 1
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.instEssSurjOppositeLeftOp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C Dᵒᵖ} [F.EssSurj], F.leftOp.EssSurj
-- Mathlib.Analysis.Analytic.Linear
analyticWithinAt_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {t : Set (E × F)}
  {p : E × F}, AnalyticWithinAt 𝕜 (fun p => p.2) t p
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.instPow.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : MulOneClass M] [inst_1 : CommMonoid N],
  MonoidHom.instPow = { pow := fun f n => { toFun := ⇑f ^ n, map_one' := ⋯, map_mul' := ⋯ } }
-- Lean.Server.GoTo
Lean.Server.isInstanceProjection : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Data.Int.Interval
Int.Ico_eq_finset_map : ∀ (a b : ℤ), Finset.Ico a b = Finset.map (Nat.castEmbedding.trans (addLeftEmbedding a)) (Finset.range (b - a).toNat)
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
List.toArray_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {β : Type w} {l : List β},
  (l.iterM m).toArray = pure l.toArray
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.ext_iff : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f g : SchwartzMap E F}, f = g ↔ ∀ (x : E), f x = g x
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.formula_performRatCheck : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ratUnits = #[] ∧ f.assignments.size = n →
    ∀ (p : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHint : ℕ × Array ℕ),
      (f.performRatCheck p ratHint).1 = f
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.ZMod.χ₈.match_1.eq_8 : ∀ (motive : ZMod 8 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 2) (h_3 : Unit → motive 4)
  (h_4 : Unit → motive 6) (h_5 : Unit → motive 1) (h_6 : Unit → motive 7) (h_7 : Unit → motive 3)
  (h_8 : Unit → motive 5),
  (match 5 with
    | 0 => h_1 ()
    | 2 => h_2 ()
    | 4 => h_3 ()
    | 6 => h_4 ()
    | 1 => h_5 ()
    | 7 => h_6 ()
    | 3 => h_7 ()
    | 5 => h_8 ()) =
    h_8 ()
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_uIoc_eq : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : LinearOrder α] (a b : α),
  MeasureTheory.ae (μ.restrict (Set.uIoc a b)) =
    MeasureTheory.ae (μ.restrict (Set.Ioc a b)) ⊔ MeasureTheory.ae (μ.restrict (Set.Ioc b a))
-- Init.Data.SInt.Bitwise
Int8.xor_eq_zero_iff : ∀ {a b : Int8}, a ^^^ b = 0 ↔ a = b
-- Init.Data.List.Lemmas
List.all_filterMap : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → Option β} {p : β → Bool},
  (List.filterMap f l).all p =
    l.all fun a =>
      match f a with
      | some b => p b
      | none => true
-- Mathlib.CategoryTheory.Abelian.Projective.Basic
/-- The preadditive co-Yoneda functor on `P` preserves finite colimits if `P` is projective.  -/
CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (P : C)
  [hP : CategoryTheory.Projective P],
  CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj P)