mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.dualBasis.congr_simp : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_9}
  [inst_3 : DecidableEq ι] [inst_4 : Finite ι] (B B_1 : LinearMap.BilinForm K V) (e_B : B = B_1) (hB : B.Nondegenerate)
  (b b_1 : Module.Basis ι K V), b = b_1 → B.dualBasis hB b = B_1.dualBasis ⋯ b_1
-- Mathlib.Data.Fintype.EquivFin
/-- Noncomputable equivalence between a finset `s` coerced to a type and `Fin #s`.  -/
Finset.equivFin : {α : Type u_1} → (s : Finset α) → ↥s ≃ Fin s.card
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instFinite : ∀ {R : Type u_3} (c₁ c₂ c₃ : R) [inst : CommRing R], Module.Finite R (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.exp_two_pi_mul_I_mul_div_eq_one_iff : ∀ {k N : ℕ}, N ≠ 0 → (Complex.exp (2 * ↑Real.pi * Complex.I * ↑k / ↑N) = 1 ↔ N ∣ k)
-- Mathlib.Algebra.Lie.Subalgebra
/-- We can restrict a morphism to a (surjective) map to its range.  -/
LieHom.rangeRestrict : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {L₂ : Type w} → [inst_3 : LieRing L₂] → [inst_4 : LieAlgebra R L₂] → (f : L →ₗ⁅R⁆ L₂) → L →ₗ⁅R⁆ ↥f.range
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.exp_cgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [hμ : NeZero μ],
  MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
    Real.exp (ProbabilityTheory.cgf X μ t) = ProbabilityTheory.mgf X μ t
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_mk : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (f : A → M) (map_zero_eq_one' : f 0 = 1)
  (map_add_eq_mul' : ∀ (a b : A), f (a + b) = f a * f b),
  ⇑{ toFun := f, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' } = f
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap_ite : ∀ {α : Type u_1} {β : Type u_2} (p : Prop) [inst : Decidable p] (t e : Option α)
  (f : (a : α) → (if p then t else e) = some a → β),
  Std.Internal.List.Option.dmap✝ (if p then t else e) f =
    if h : p then Std.Internal.List.Option.dmap✝ t fun a h' => f a ⋯
    else Std.Internal.List.Option.dmap✝ e fun a h' => f a ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The cofork defined in `BinaryBicone.inlCokernelCofork` is indeed a cokernel.  -/
CategoryTheory.Limits.BinaryBicone.isColimitInlCokernelCofork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {c : CategoryTheory.Limits.BinaryBicone X Y} →
          CategoryTheory.Limits.IsColimit c.toCocone → CategoryTheory.Limits.IsColimit c.inlCokernelCofork
-- Init.Data.Fin.Lemmas
Fin.coe_castLT : ∀ {m n : ℕ} (i : Fin m) (h : ↑i < n), ↑(i.castLT h) = ↑i
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
/-- **Alias** of `summable_finsetProd_of_summable_nonneg`. -/
summable_finset_prod_of_summable_nonneg : ∀ {ι : Type u_1} {f : ι → ℝ}, (∀ (i : ι), 0 ≤ f i) → Summable f → Summable fun s => ∏ i ∈ s, f i
-- Mathlib.Data.Set.Function
Set.injOn_of_eq_iff_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} (s : Set α), (∀ (x y : α), f x = f y ↔ x = y) → Set.InjOn f s
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.mul_k_eq_mul : ∀ (k : ℤ) (p : Int.Internal.Linear.Poly), p.mul_k k = p.mul k
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- the degree of a multivariate polynomial with respect to a monomial ordering, where the
polynomial `0` has degree `0`. For the variant mapping polynomial `0` to `⊥` which is less than
`0`, see `MonomialOrder.withBotDegree`.  -/
MonomialOrder.degree : {σ : Type u_1} → MonomialOrder σ → {R : Type u_2} → [inst : CommSemiring R] → MvPolynomial σ R → σ →₀ ℕ
-- Init.Data.Float.Model.Float32
/-- Pack an `UnpackedFloat` into the corresponding `Float32.Model`.
This operation only gives a meaningful result if the float is
already correctly rounded for the `Format.binary32` format.
 -/
Float32.Model.pack : Float.Model.UnpackedFloat → Float32.Model
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- the bottom morphism of the pushout square `isPushout i d`.  -/
SSet.relativeCellComplexOfMono.b : {X Y : SSet} →
  (i : X ⟶ Y) → (d : ℕ) → SSet.relativeCellComplexOfMono.sigmaStdSimplex i d ⟶ ((SSet.skeletonOfMono i) (d + 1)).toSSet
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instCommMonoid : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [CommMonoid β] → CommMonoid (MeasureTheory.SimpleFunc α β)
-- Init.Data.Rat.Lemmas
Rat.intCast_one : ↑1 = 1
-- Mathlib.Data.Matrix.Mul
Matrix.col_vecMulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Mul α] (w : m → α) (v : n → α) (j : n),
  (Matrix.vecMulVec w v).col j = MulOpposite.op (v j) • w
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.insertMany_nil : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}, t.insertMany [] = t
-- Mathlib.RingTheory.HopfAlgebra.Basic
/-- One of the antipode axioms for a Hopf algebra.  -/
HopfAlgebra.mul_antipode_rTensor_comul : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : Semiring A} [self : HopfAlgebra R A],
  LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul =
    Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit
-- Mathlib.Topology.Maps.Strict.Basic
/-- A strict map is continuous, since the range factorization is continuous.  -/
Topology.IsStrictMap.continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsStrictMap f → Continuous f
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.comp_fst : ∀ {X Y Z : TopPair} {f₀ f₁ : X ⟶ Y} {g₀ g₁ : Y ⟶ Z} (G : TopPair.Homotopy g₀ g₁) (F : TopPair.Homotopy f₀ f₁),
  (G.comp F).fst = G.fst.comp F.fst
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- `IsRegularEpi f` is the assertion that `f` is a regular epimorphism.  -/
CategoryTheory.IsRegularEpi : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (X ⟶ Y) → Prop
-- Mathlib.Algebra.Quaternion
Quaternion.eq_re_iff_mem_range_coe : ∀ {R : Type u_3} [inst : CommRing R] {a : Quaternion R}, a = ↑a.re ↔ a ∈ Set.range Quaternion.coe
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Alternatizing a multilinear map that is already alternating results in a scale factor of `n!`,
where `n` is the number of inputs.  -/
AlternatingMap.coe_alternatization : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
  (a : M [⋀^ι]→ₗ[R] N'), MultilinearMap.alternatization ↑a = (Fintype.card ι).factorial • a
-- Init.Data.BitVec.Bitblast
/-- Extracting a bit from a `BitVec.extractAndExtend` is the same as extracting a bit
from a zero-extended bit at a certain position in the original bitvector.
 -/
BitVec.getLsbD_extractAndExtend : ∀ {w v k : ℕ} {x : BitVec w},
  0 < v → (BitVec.extractAndExtend v x).getLsbD k = (BitVec.extractAndExtendBit ((k - k % v) / v) v x).getLsbD (k % v)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_whiskerLeft_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z Z' : C} (f : Z ⟶ Z') {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) f) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y f))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z').inv h))
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mul_mem_nonZeroDivisorsLeft_of_mem_nonZeroDivisorsLeft : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x y : M₀},
  x ∈ nonZeroDivisorsLeft M₀ → y ∈ nonZeroDivisorsLeft M₀ → x * y ∈ nonZeroDivisorsLeft M₀
-- Mathlib.Topology.MetricSpace.Similarity
Similar.trans : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂} {v₃ : ι → P₃}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃],
  Similar v₁ v₂ → Similar v₂ v₃ → Similar v₁ v₃
-- Lean.Environment
Lean.ConstMap : Type
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhds_coe : ∀ {r : NNReal}, nhds ↑r = Filter.map ENNReal.ofNNReal (nhds r)
-- Mathlib.Data.List.Chain
List.isChain_cons_map : ∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} (f : β → α) {l : List β} {b : β},
  List.IsChain R (f b :: List.map f l) ↔ List.IsChain (fun a b => R (f a) (f b)) (b :: l)
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
IsLocalRing.maximalIdeal_sq_lt_maximalIdeal : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  IsLocalRing.maximalIdeal R ^ 2 < IsLocalRing.maximalIdeal R ↔ ¬IsField R
-- Mathlib.Analysis.Complex.Trigonometric
/-- The definition of `tanh` in terms of `exp`.  -/
Real.tanh_eq : ∀ (x : ℝ), Real.tanh x = (Real.exp x - Real.exp (-x)) / (Real.exp x + Real.exp (-x))
-- Mathlib.RingTheory.PowerSeries.Inverse
/-- `Inv_divided_by_X_pow_order` is the inverse of the element obtained by diving a non-zero power
series by the largest power of `X` dividing it. Useful to create a term of type `Units`, done in
`Unit_divided_by_X_pow_order`  -/
PowerSeries.Inv_divided_by_X_pow_order : {k : Type u_2} → [inst : Field k] → {f : PowerSeries k} → f ≠ 0 → PowerSeries k
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonneg_muld : ∀ {d : ℕ} {a : ℤ√↑d}, a.Nonneg → (Zsqrtd.sqrtd * a).Nonneg
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_eq_isEmpty_eraseKey_and_not_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ (k : α), l.isEmpty = ((Std.Internal.List.eraseKey k l).isEmpty && !Std.Internal.List.containsKey k l)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceBifibrantObjectBifibrantResolutionMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X₁ X₂ : HomotopicalAlgebra.CofibrantObject C} (f : X₁ ⟶ X₂) [HomotopicalAlgebra.WeakEquivalence f],
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap f)
-- Std.Http.Data.URI.Basic
/-- Creates a query string from a list of key-value pairs.
 -/
Std.Http.URI.Query.ofList : List (Std.Http.URI.EncodedQueryParam × Option Std.Http.URI.EncodedQueryParam) → Std.Http.URI.Query
-- Mathlib.Geometry.Manifold.Submersion
/-- A choice of complement of the model normed space `E` of `M` in the model normed space
`E'` of `N`  -/
Manifold.IsSubmersionAt.complement : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {H : Type u_7} →
      {G : Type u_9} →
        {E : Type u} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup E''] →
                  [inst_4 : NormedSpace 𝕜 E''] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              {N : Type u_13} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} → {x : M} → Manifold.IsSubmersionAt I J n f x → Type u
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.instPartialOrder.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E], AddGroupNorm.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
-- Mathlib.Topology.Order.LeftRightNhds
mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a l' : α} {s : Set α},
  l' < a → (s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Ico l' a, Set.Ioc l a ⊆ s)
-- Mathlib.Algebra.Homology.ShortComplex.Linear
/-- Given a left homology map data for morphism `φ`, this is the induced left homology
map data for `a • φ`.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.smul : {R : Type u_1} →
  {C : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Linear R C] →
            {S₁ S₂ : CategoryTheory.ShortComplex C} →
              {φ : S₁ ⟶ S₂} →
                {h₁ : S₁.LeftHomologyData} →
                  {h₂ : S₂.LeftHomologyData} →
                    CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂ →
                      (a : R) → CategoryTheory.ShortComplex.LeftHomologyMapData (a • φ) h₁ h₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofIsInitialLeft_pt : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂)
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.flip.obj X₂)]
  [inst_4 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.flip.obj Y₂)]
  (h : CategoryTheory.Limits.IsInitial X₁),
  (CategoryTheory.Functor.PushoutObjObj.ofIsInitialLeft F f₁ f₂ h).pt = (F.obj Y₁).obj X₂
-- Init.Data.Fin.Basic
Fin.val_add_one_le_of_lt : ∀ {n : ℕ} {a b : Fin n}, a < b → ↑a + 1 ≤ ↑b
-- Mathlib.Data.Finset.Image
Function.Injective.mem_finset_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {a : α},
  Function.Injective f → (f a ∈ Finset.image f s ↔ a ∈ s)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryProductTriangle_mor₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).mor₃ = 0
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.congr_tmul : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] {σ₂₁ : R₂ →+* R} [inst_10 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_11 : RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) (m : M) (n : N),
  (TensorProduct.congr f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R₂] g n
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndep.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (m : ι → MeasurableSpace Ω) (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.iCondIndep m' hm' m μ =
    ProbabilityTheory.Kernel.iIndep m (ProbabilityTheory.condExpKernel μ m') (μ.trim hm')
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.mkENode' : Lean.Expr → ℕ → optParam Bool false → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion on a ball, then it is continuous there.  -/
HasFPowerSeriesOnBall.continuousOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → ContinuousOn f (Metric.eball x r)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.dvd.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.dvd c = Lean.Meta.Grind.Arith.Cutsat.UnsatProof.dvd c_1) = (c = c_1)
-- Mathlib.Combinatorics.Additive.Convolution
Finset.addConvolution_neg : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  A.addConvolution B (-x) = (-B).addConvolution (-A) x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k : α} {f : Option β → Option β} {h : k ∈ m.alter k f},
  (m.alter k f).getKey k h = k
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.codeSupp'.match_1.splitter : (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) →
  (x : Turing.ToPartrec.Code) →
    (x_1 : Turing.PartrecToTM2.Cont') →
      ((k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k) →
        ((k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k) →
          ((k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k) →
            ((f fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k) →
              ((f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k) →
                ((f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k) →
                  ((f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive f.fix k) → motive x x_1
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
/-- Typecheck a `BialgHom` as a morphism in `HopfAlgCat R`.  -/
HopfAlgCat.ofHom : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : Ring X] →
        [inst_2 : Ring Y] →
          [inst_3 : HopfAlgebra R X] →
            [inst_4 : HopfAlgebra R Y] → (X →ₐc[R] Y) → (HopfAlgCat.of R X ⟶ HopfAlgCat.of R Y)
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.iInf_Ioi_eq_iInf_rat_gt : ∀ {f : ℝ → ℝ} (x : ℝ), BddBelow (f '' Set.Ioi x) → Monotone f → ⨅ r, f ↑r = ⨅ q, f ↑↑q
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_eq_Ioo_same_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioc a b = Set.Ioo a b ↔ ¬a < b
-- Init.Data.Range.Polymorphic.PRange
Std.Rio.mk.inj : ∀ {α : Type u} {upper upper_1 : α}, ((*...upper) = *...upper_1) → upper = upper_1
-- Mathlib.Data.Finset.Sups
Finset.sups_nonempty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t : Finset α},
  (s ⊻ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.RepresentationTheory.Coinvariants
/-- The linear map underlying a `G`-representation morphism `A ⟶ B`, where `B` has the trivial
representation, factors through `A_G`.  -/
Rep.desc : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        {A B : Rep.{w, u, v} k G} →
          [B.ρ.IsTrivial] → (A ⟶ B) → ((Rep.coinvariantsFunctor k G).obj A ⟶ ModuleCat.of k ↑B)
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjointAux.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  [inst_5 : CompleteSpace E] (hT : Dense ↑T.domain), LinearPMap.adjointAux hT = LinearPMap.adjointAux hT
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.snd : ∀ {Ω : Type u_1} {E : Type u_2} {F : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] {X : Ω → E} [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : MeasurableSpace F] [BorelSpace F] {Y : Ω → F},
  ProbabilityTheory.HasGaussianLaw (fun ω => (X ω, Y ω)) P → ProbabilityTheory.HasGaussianLaw Y P
-- Init.Data.Array.Lemmas
Array.getElem_fin_eq_getElem_toList : ∀ {α : Type u_1} {xs : Array α} {i : Fin xs.size}, xs[i] = xs.toList[i]
-- Mathlib.Order.Bounds.Image
IsCoinitialFor.image_of_antitone : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s t : Set α} {f : α → β},
  IsCoinitialFor s t → Antitone f → IsCofinalFor (f '' s) (f '' t)
-- Mathlib.Analysis.Complex.AbsMax
/-- **Maximum modulus principle**: if `f : E → F` is complex differentiable on a set `s`, the norm
of `f` takes it maximum on `s` at `z`, and `w` is a point such that the closed ball with center `z`
and radius `dist w z` is included in `s`, then `‖f w‖ = ‖f z‖`.  -/
Complex.norm_eq_norm_of_isMaxOn_of_ball_subset : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {f : E → F} {s : Set E} {z w : E},
  DiffContOnCl ℂ f s → IsMaxOn (norm ∘ f) s z → Metric.ball z (dist w z) ⊆ s → ‖f w‖ = ‖f z‖
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.aeval.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {a a_1 : S} (e_a : a = a_1)
  [inst_2 : UniformSpace R] [inst_3 : UniformSpace S] [inst_4 : IsUniformAddGroup R] [inst_5 : IsTopologicalSemiring R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : T2Space S] [inst_8 : CompleteSpace S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] (ha : PowerSeries.HasEval a),
  PowerSeries.aeval ha = PowerSeries.aeval ⋯
-- Mathlib.Algebra.Order.Group.Defs
/-- **Alias** of `lt_of_add_lt_add_left`. -/
OrderedCommGroup.lt_of_add_lt_add_left : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α] [AddLeftReflectLT α] {a b c : α}, a + b < a + c → b < c
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.IsSRGWith.card : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ},
  G.IsSRGWith n k ℓ μ → Fintype.card V = n
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_assoc : ∀ {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) (n : ℤ) {Z : CategoryTheory.Functor C C} (h : t.truncGE n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.truncLTι n) (CategoryTheory.CategoryStruct.comp (t.truncGEπ n) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.Internal.List.Associative
Std.Internal.List.modifyKey_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l l' : List ((a : α) × β a)} {k : α}
  {f : β k → β k},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → (Std.Internal.List.modifyKey k f l).Perm (Std.Internal.List.modifyKey k f l')