mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.domRestrict_domain : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ.[σ] F)
  {S_1 : Submodule R E}, (f.domRestrict S_1).domain = S_1 ⊓ f.domain
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.iInf_adj : ∀ {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a b : V} {f : ι → G.Subgraph},
  (⨅ i, f i).Adj a b ↔ (∀ (i : ι), (f i).Adj a b) ∧ G.Adj a b
-- Mathlib.Order.Filter.Extr
/-- **Alias** of the forward direction of `isExtrOn_dual_iff`. -/
IsExtrOn.undual : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsExtrOn (⇑OrderDual.toDual ∘ f) s a → IsExtrOn f s a
-- Mathlib.CategoryTheory.GradedObject
/-- Given `X : GradedObject I C`, `p : I → J` and `j : J`, `X.mapObj p j` satisfies
the universal property of the coproduct of those `X i` such that `p i = j`.  -/
CategoryTheory.GradedObject.isColimitCofanMapObj : {I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        (X : CategoryTheory.GradedObject I C) →
          (p : I → J) → [inst_1 : X.HasMap p] → (j : J) → CategoryTheory.Limits.IsColimit (X.cofanMapObj p j)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt64.reduceToNat : Lean.Meta.Simp.DSimproc
-- Aesop.Check
Aesop.Check.mk.injEq : ∀ (toOption toOption_1 : Lean.Option Bool),
  ({ toOption := toOption } = { toOption := toOption_1 }) = (toOption = toOption_1)
-- Mathlib.GroupTheory.ArchimedeanDensely
LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete_of_ne_zero : ∀ {G₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] {g : G₀},
  g ≠ 0 → (({x | x ≤ g}.WellFoundedOn fun x1 x2 => x1 > x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ)))
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.isoOfNatIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (w : F ≅ G),
  CategoryTheory.Limits.HasLimit.isoOfNatIso w =
    (CategoryTheory.Limits.limit.isLimit F).conePointsIsoOfNatIso (CategoryTheory.Limits.limit.isLimit G) w
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D}
  [self : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] (J : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsFiltered J],
  CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.Topology.Algebra.Constructions
Units.continuous_coe_inv : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M], Continuous fun u => ↑u⁻¹
-- Mathlib.CategoryTheory.Functor.OfSequence
_private.Mathlib.CategoryTheory.Functor.OfSequence.0.CategoryTheory.Functor.OfSequence.map.match_3.splitter : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    (motive : (x : ℕ → C) → ((n : ℕ) → x n ⟶ x (n + 1)) → ℕ → ℕ → Sort u_3) →
      (x : ℕ → C) →
        (x_1 : (n : ℕ) → x n ⟶ x (n + 1)) →
          (x_2 x_3 : ℕ) →
            ((x : ℕ → C) → (x_4 : (n : ℕ) → x n ⟶ x (n + 1)) → motive x x_4 0 0) →
              ((x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → motive x f 0 1) →
                ((x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → (l : ℕ) → (l = 0 → False) → motive x f 0 l.succ) →
                  ((x : ℕ → C) → (x_4 : (n : ℕ) → x n ⟶ x (n + 1)) → (n : ℕ) → motive x x_4 n.succ 0) →
                    ((x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → (k l : ℕ) → motive x f k.succ l.succ) →
                      motive x x_1 x_2 x_3
-- Mathlib.Topology.MetricSpace.Bounded
Metric.diam_le_of_subset_closedBall : ∀ {α : Type u} {s : Set α} {x : α} [inst : PseudoMetricSpace α] {r : ℝ},
  0 ≤ r → s ⊆ Metric.closedBall x r → Metric.diam s ≤ 2 * r
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Unitization.sqrt_inr : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {a : A},
  CFC.sqrt ↑a = ↑(CFC.sqrt a)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.map_piecewise_add : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [inst_7 : DecidableEq ι] (m m' : ι → M) (t : Finset ι),
  f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
-- Mathlib.Analysis.Calculus.Implicit
/-- **Alias** of `ImplicitFunctionData.hasStrictFDerivAt_implicitFunction`. -/
ImplicitFunctionData.implicitFunction_hasStrictFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) (g'inv : G →L[𝕜] E),
  φ.rightDeriv ∘SL g'inv = ContinuousLinearMap.id 𝕜 G →
    φ.leftDeriv ∘SL g'inv = 0 → HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt)) g'inv (φ.rightFun φ.pt)
-- Mathlib.Analysis.MeanInequalities
/-- **AM-GM inequality - equality condition**.
The condition is that all elements of `z` with a nonzero weight are equal to each other;
see `geom_mean_eq_arith_mean_weighted_iff_of_nonneg'` for a version that compares the elements to
their center of mass `∑ i ∈ s, w i * z i` instead.  -/
Real.geom_mean_eq_arith_mean_weighted_iff_of_nonneg : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 ≤ w i) →
    ∑ i ∈ s, w i = 1 →
      (∀ i ∈ s, 0 ≤ z i) → (∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, w j ≠ 0 → ∀ k ∈ s, w k ≠ 0 → z j = z k)
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.mk_self_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G) (x : V),
  (Representation.Coinvariants.mk ρ) ((ρ g) x) = (Representation.Coinvariants.mk ρ) x
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_algHom : ∀ {R : Type u_1} [inst : CommSemiring R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B],
  (Polynomial.map (algebraMap R A) f).Splits → ∀ (e : A →ₐ[R] B), (Polynomial.map (algebraMap R B) f).Splits
-- Mathlib.Data.Vector.Basic
List.Vector.ofFn.eq_2 : ∀ {α : Type u_1} (n : ℕ) (f : Fin (n + 1) → α), List.Vector.ofFn f = f 0 ::ᵥ List.Vector.ofFn fun i => f i.succ
-- Init.Data.Range.Polymorphic.PRange
Std.Rcc.HasRcoIntersection.mk : {α : Type w} → (Std.Rcc α → Std.Rco α → Std.Rco α) → Std.Rcc.HasRcoIntersection α
-- Mathlib.Order.Heyting.Basic
/-- a version of `sdiff_sup_sdiff_cancel` with more general hypotheses.  -/
sdiff_sup_sdiff_cancel' : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ⊓ c ≤ b → b ≤ a ⊔ c → a \ b ⊔ b \ c = a \ c
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat : ∀ {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) (X : C) (n : ℤ), t.IsLE ((t.triangleLTGE n).obj X).obj₁ (n - 1)
-- Mathlib.Data.Nat.Bitwise
Nat.xor_mod_two_eq : ∀ {m n : ℕ}, (m ^^^ n) % 2 = (m + n) % 2
-- Mathlib.Order.Interval.Basic
NonemptyInterval.dual_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (a : NonemptyInterval α),
  NonemptyInterval.dual (NonemptyInterval.map f a) = NonemptyInterval.map (OrderHom.dual f) (NonemptyInterval.dual a)
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F) {s : Set (G × ((i : ι) → Em i))},
  CPolynomialOn 𝕜 (fun p => (f p.1) p.2) s
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_succ_Ioi : ∀ {n : ℕ} (i : Fin n), Finset.image Fin.succ (Finset.Ioi i) = Finset.Ioi i.succ
-- Init.Data.UInt.Lemmas
USize.toNat_neg : ∀ (a : USize), (-a).toNat = (USize.size - a.toNat) % USize.size
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
/-- Given a functor `F : Set.Iio j ⥤ C` and a cocone `c : Cocone F`,
where `j : J` and `J` is linearly ordered, this is the functor
`Set.Iic j ⥤ C` which extends `F` and sends the top element to `c.pt`.  -/
CategoryTheory.SmallObject.SuccStruct.ofCocone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        {j : J} →
          {F : CategoryTheory.Functor (↑(Set.Iio j)) C} →
            CategoryTheory.Limits.Cocone F → CategoryTheory.Functor (↑(Set.Iic j)) C
-- Lean.Meta.Tactic.Grind.ProveEq
/-- Types of the new variables created for the auxiliary `fun`.  -/
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.State.varTypes : Lean.Meta.Grind.AbstractM.State✝ → Array Lean.Expr
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.of_const_mul_right : ∀ {α : Type u_1} {E : Type u_3} {R : Type u_13} [inst : Norm E] [inst_1 : SeminormedRing R] {f : α → E} {l : Filter α}
  {g : α → R} {c : R}, (f =O[l] fun x => c * g x) → f =O[l] g
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct an isomorphism between whiskered lifts.  -/
CategoryTheory.Bicategory.LeftLift.whiskerIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {s t : CategoryTheory.Bicategory.LeftLift f g} → (s ≅ t) → {x : B} → (h : x ⟶ c) → s.whisker h ≅ t.whisker h
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.State.mk.injEq : ∀ (vars : Lean.PArray Lean.Expr) (varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var)
  (vars' : Lean.PArray Lean.Expr) (varMap' : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var)
  (natToIntMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr))
  (natDef : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var)
  (dvds : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr))
  (lowers uppers : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.LeCnstr))
  (diseqs : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr))
  (elimEqs : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr)) (elimStack : List Int.Internal.Linear.Var)
  (occurs : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.VarSet) (assignment : Lean.PArray ℚ) (nextCnstrId : ℕ)
  (caseSplits : Bool) (steps : ℕ) (conflict? : Option Lean.Meta.Grind.Arith.Cutsat.UnsatProof)
  (diseqSplits : Lean.PHashMap Int.Internal.Linear.Poly Lean.FVarId) (divMod : Lean.PHashSet (Lean.Expr × ℤ))
  (toIntIds : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (toIntInfos : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.ToIntInfo)
  (toIntTermMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo)
  (toIntVarMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr) (usedCommRing : Bool)
  (nonlinearOccs : Lean.PHashMap Int.Internal.Linear.Var (List Int.Internal.Linear.Var))
  (vars_1 : Lean.PArray Lean.Expr) (varMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var)
  (vars'_1 : Lean.PArray Lean.Expr) (varMap'_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var)
  (natToIntMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr))
  (natDef_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var)
  (dvds_1 : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr))
  (lowers_1 uppers_1 : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.LeCnstr))
  (diseqs_1 : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr))
  (elimEqs_1 : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr)) (elimStack_1 : List Int.Internal.Linear.Var)
  (occurs_1 : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.VarSet) (assignment_1 : Lean.PArray ℚ) (nextCnstrId_1 : ℕ)
  (caseSplits_1 : Bool) (steps_1 : ℕ) (conflict?_1 : Option Lean.Meta.Grind.Arith.Cutsat.UnsatProof)
  (diseqSplits_1 : Lean.PHashMap Int.Internal.Linear.Poly Lean.FVarId) (divMod_1 : Lean.PHashSet (Lean.Expr × ℤ))
  (toIntIds_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (toIntInfos_1 : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.ToIntInfo)
  (toIntTermMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo)
  (toIntVarMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr) (usedCommRing_1 : Bool)
  (nonlinearOccs_1 : Lean.PHashMap Int.Internal.Linear.Var (List Int.Internal.Linear.Var)), ⋯ = ⋯
-- Mathlib.RingTheory.Localization.Module
LinearEquiv.extendScalarsOfIsLocalization_apply : ∀ {R : Type u_3} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_5} {N : Type u_6} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Module A M] [inst_7 : IsScalarTower R A M] [inst_8 : AddCommMonoid N]
  [inst_9 : Module R N] [inst_10 : Module A N] [inst_11 : IsScalarTower R A N] (f : M ≃ₗ[R] N) (a : M),
  (LinearEquiv.extendScalarsOfIsLocalization S A f) a = f a
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_smul_inter_smul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G) (x y : G),
  (x • A ∩ y • B).card = A.convolution B⁻¹ (x⁻¹ * y)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.tendsto_iff_tendstoUniformlyOn : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] {ι : Type u_6} {p : Filter ι} [inst_7 : UniformSpace F]
  [inst_8 : IsUniformAddGroup F] (𝔖 : Set (Set E)) {a : ι → UniformConvergenceCLM σ F 𝔖}
  {a₀ : UniformConvergenceCLM σ F 𝔖},
  Filter.Tendsto a p (nhds a₀) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (fun x1 x2 => (a x1) x2) (⇑a₀) p s
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.right_unitor_hom_apply : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {X : (i : I) → C i} {i : I},
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom i =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X i)).hom
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec_zeroLocus : ∀ {R : CommRingCat} (s : Set ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤))),
  (AlgebraicGeometry.Spec R).zeroLocus s =
    PrimeSpectrum.zeroLocus (⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso R).inv) ⁻¹' s)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquivClass.toLinearEquivClass : ∀ (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : EquivLike F A B]
  [h : AlgEquivClass F R A B], LinearEquivClass F R A B
-- Mathlib.Algebra.GradedMulAction
/-- A version of `GradedMonoid.GSMul` for internally graded objects.  -/
SetLike.GradedSMul : {ιA : Type u_1} →
  {ιB : Type u_2} →
    {S : Type u_5} →
      {R : Type u_6} →
        {N : Type u_7} →
          {M : Type u_8} → [SetLike S R] → [SetLike N M] → [SMul R M] → [VAdd ιA ιB] → (ιA → S) → (ιB → N) → Prop
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
LinearMap.IsReflective.reflective_reflection : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (B : M →ₗ[R] M →ₗ[R] R) {x : M},
  B.IsSymm → ∀ {y : M} (hx : B.IsReflective x), B.IsReflective y → B.IsReflective ((Module.reflection ⋯) y)
-- Mathlib.Algebra.Order.Algebra
/-- Extension for `algebraMap`.  -/
Mathlib.Meta.Positivity.evalAlgebraMap : Mathlib.Meta.Positivity.PositivityExt
-- Aesop.Tree.Data
Aesop.GoalOrigin.droppedMVar.sizeOf_spec : sizeOf Aesop.GoalOrigin.droppedMVar = 1
-- Mathlib.LinearAlgebra.CrossProduct
/-- The scalar triple product expansion of the vector triple product.  -/
cross_cross_eq_smul_sub_smul : ∀ {R : Type u_1} [inst : CommRing R] (u v w : Fin 3 → R),
  (crossProduct ((crossProduct u) v)) w = (u ⬝ᵥ w) • v - (v ⬝ᵥ w) • u
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.map_map_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') {X Y : CategoryTheory.Comma L R} (φ : X ⟶ Y),
  ((CategoryTheory.Comma.map α β).map φ).left = F₁.map φ.left
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.singleton_eq_insert : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {p : α × β}, {p} = ∅.insert p.1 p.2
-- Lean.Meta.LazyDiscrTree
/-- A partial match captures the intermediate state of a match
execution.

N.B. The discriminator tree in Lean has non-determinism due to
star and function arrows, so matching loop maintains a stack of
partial match results.
 -/
Lean.Meta.LazyDiscrTree.PartialMatch : Type
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Let `M` be a σ-compact Hausdorff finite-dimensional topological manifold. Let `t : M → Set F` be
a family of convex sets. Suppose that for each point `x : M` there exists a vector `c : F` such that
for all `y` in a neighborhood of `x` we have `c ∈ t y`. Then there exists a smooth function
`g : C^n⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` for all `x`. See also
`exists_contMDiffMap_forall_mem_convex_of_local`.  -/
exists_contMDiffMap_forall_mem_convex_of_local_const : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {H : Type uH} [inst_4 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM}
  [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M] [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M]
  [SigmaCompactSpace M] [T2Space M] {t : M → Set F} {n : ℕ∞},
  (∀ (x : M), Convex ℝ (t x)) → (∀ (x : M), ∃ c, ∀ᶠ (y : M) in nhds x, c ∈ t y) → ∃ g, ∀ (x : M), g x ∈ t x
-- Init.Data.List.Find
List.lookup_eq_none_iff : ∀ {α : Type u_2} [inst : BEq α] {β : Type u_1} {l : List (α × β)} {k : α},
  List.lookup k l = none ↔ ∀ p ∈ l, (k != p.1) = true
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- If `v` is a complex infinite place, then the embedding `v.Completion →+* ℂ` is surjective.  -/
NumberField.InfinitePlace.Completion.surjective_extensionEmbedding_of_isComplex : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K},
  v.IsComplex → Function.Surjective ⇑(NumberField.InfinitePlace.Completion.extensionEmbedding v)
-- Init.Data.List.MinMax
List.min?_eq_some_iff : ∀ {α : Type u_1} {a : α} [inst : Min α] [inst_1 : LE α] {xs : List α} [Std.IsLinearOrder α] [Std.LawfulOrderMin α],
  xs.min? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, a ≤ b
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ}
  [P.IsStableUnderCobaseChange], P.unop.IsStableUnderBaseChange
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_subset_Ico_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α}, a₁ < b₁ → (Set.Ico a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂)
-- Std.Time.DateTime.PlainDateTime
/-- Extracts the `PlainDate` component from a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.toPlainDate : Std.Time.PlainDateTime → Std.Time.PlainDate
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- If there is a multiplicative character of order `n` on `F`, then `#F ≡ 1 mod n`.  -/
MulChar.orderOf_dvd_card_sub_one : ∀ (F : Type u_1) [inst : Field F] [inst_1 : Fintype F] {R : Type u_2} [inst_2 : CommRing R] (χ : MulChar F R),
  orderOf χ ∣ Fintype.card F - 1
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.card_neighborFinset_eq_degree : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)], (G.neighborFinset v).card = G.degree v
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_inv : ∀ {x : ℝ}, Irrational x⁻¹ → Irrational x
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.comp_actionHomLeft : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {w x y : D} (f : w ⟶ x) (g : x ⟶ y) (z : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (CategoryTheory.CategoryStruct.comp f g) z =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f z)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft g z)
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.radius_pos : ∀ {𝕜 : 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 → 0 < p.radius
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.constantCoeff_invUnitsSub : ∀ {R : Type u_1} [inst : Ring R] (u : Rˣ), PowerSeries.constantCoeff (PowerSeries.invUnitsSub u) = 1 /ₚ u
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p ≠ 0 → (p.trailingDegree = ↑n ↔ p.natTrailingDegree = n)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_cos : ∀ (x : ℝ), ↑(Real.cos x) = Complex.cos ↑x
-- Mathlib.Order.UpperLower.Basic
OrderEmbedding.image_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β),
  IsLowerSet (Set.range ⇑e) → ∀ (a : α), ⇑e '' Set.Iic a = Set.Iic (e a)
-- Mathlib.Analysis.Normed.Group.Uniform
uniformContinuous_norm' : ∀ {E : Type u_2} [inst : SeminormedGroup E], UniformContinuous norm
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.core.inj : ∀ {a b : Lean.Expr} {ea eb : Lean.Grind.AC.Expr} {a_1 b_1 : Lean.Expr} {ea_1 eb_1 : Lean.Grind.AC.Expr},
  Lean.Meta.Grind.AC.DiseqCnstrProof.core a b ea eb = Lean.Meta.Grind.AC.DiseqCnstrProof.core a_1 b_1 ea_1 eb_1 →
    a = a_1 ∧ b = b_1 ∧ ea = ea_1 ∧ eb = eb_1