mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
/-- The forward direction of `CliffordAlgebra.prodEquiv`.  -/
CliffordAlgebra.ofProd : {R : Type u_1} →
  {M₁ : Type u_2} →
    {M₂ : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                (Q₁ : QuadraticForm R M₁) →
                  (Q₂ : QuadraticForm R M₂) →
                    CliffordAlgebra (QuadraticMap.prod Q₁ Q₂) →ₐ[R]
                      GradedTensorProduct R (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.aleph0_lt_lift : ∀ {c : Cardinal.{u}}, Cardinal.aleph0 < Cardinal.lift.{v, u} c ↔ Cardinal.aleph0 < c
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.snd : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {n : ℕ},
  IsAddFreimanHom n (A ×ˢ B) B Prod.snd
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- preservation of colimits indexed by `Discrete (Fin n)`.  -/
CategoryTheory.Limits.PreservesFiniteCoproducts.preserves : ∀ {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.PreservesFiniteCoproducts F] (n : ℕ),
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete (Fin n)) F
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the smallest key in the tree map, panicking if the map is empty.
 -/
Std.TreeMap.minKey! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap α β cmp → α
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Functions are harmonic iff their compositions with continuous linear equivalences are harmonic.
 -/
InnerProductSpace.harmonicAt_comp_CLE_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {G : Type u_3}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ℝ G] {f : E → F} {x : E} (l : F ≃L[ℝ] G),
  InnerProductSpace.HarmonicAt (⇑l ∘ f) x ↔ InnerProductSpace.HarmonicAt f x
-- Mathlib.Algebra.Quandle
Rack.self_invAct_invAct_eq : ∀ {R : Type u_1} [inst : Rack R] {x y : R}, Rack.invAct (Rack.invAct x x) y = Rack.invAct x y
-- Init.Prelude
/-- `a >>> b` computes `a` shifted to the right by `b` places.
The meaning of this notation is type-dependent.
* On `Nat` and fixed width unsigned types like `UInt8`,
  this is equivalent to `a / 2 ^ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `>>>` in identifiers is `shiftRight`. -/
HShiftRight.hShiftRight : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HShiftRight α β γ] → α → β → γ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_eq_one_iff_of_lt_of_lt : ∀ {x : ℝ}, -(2 * Real.pi) < x → x < 2 * Real.pi → (Real.cos x = 1 ↔ x = 0)
-- Mathlib.Order.Filter.Prod
/-- Characterization of the coproduct of the `Filter.map`s of two principal filters `𝓟 {a}` and
`𝓟 {i}`, the first under the constant function `fun a => b` and the second under the identity
function. Together with the next lemma, `map_prodMap_const_id_principal_coprod_principal`, this
provides an example showing that the inequality in the lemma `map_prodMap_coprod_le` can be strict.
 -/
Filter.map_const_principal_coprod_map_id_principal : ∀ {α : Type u_6} {β : Type u_7} {ι : Type u_8} (a : α) (b : β) (i : ι),
  (Filter.map (fun x => b) (Filter.principal {a})).coprod (Filter.map id (Filter.principal {i})) =
    Filter.principal ({b} ×ˢ Set.univ ∪ Set.univ ×ˢ {i})
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.unsupportedVersion.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Error.unsupportedVersion = 1
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.instInhabitedSuggestionStyle : Inhabited Lean.Meta.Tactic.TryThis.SuggestionStyle
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the smallest key in the tree map, returning `fallback` if the tree map is empty.
 -/
Std.TreeMap.minKeyD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → α
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.mapBifunctor₂₃Desc.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃}
  (c₁₂ : ComplexShape ι₁₂) {c₂₃ : ComplexShape ι₂₃} {c₄ : ComplexShape ι₄} [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
  [inst_23 : HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] {j : ι₄} {A : C₄}
  (f f_1 : (i₁ : ι₁) → (i₂ : ι₂) → ⋯), f = f_1 → ⋯ = ⋯
-- Mathlib.GroupTheory.GroupAction.FixedPoints
AddAction.mem_fixedBy_zmultiples_iff_mem_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g : G} {a : α},
  (∀ (j : ℤ), a ∈ AddAction.fixedBy α (j • g)) ↔ a ∈ AddAction.fixedBy α g
-- Mathlib.RingTheory.Norm.Basic
Algebra.norm_zpow : ∀ {K : Type u_4} [inst : Field K] {L : Type u_7} [inst_1 : DivisionRing L] [inst_2 : Algebra K L] [Module.Finite K L]
  (x : L) (n : ℤ), (Algebra.norm K) (x ^ n) = (Algebra.norm K) x ^ n
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.domainUniqueUpToIso_hom_isHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R R' S : 𝒮} {a a' b : 𝒳} {f : R ⟶ S} {f' : R' ⟶ S} {g : R' ≅ R}
  (h : f' = CategoryTheory.CategoryStruct.comp g.hom f) (φ : a ⟶ b) (φ' : a' ⟶ b) [inst_2 : p.IsStronglyCartesian f φ]
  [inst_3 : p.IsStronglyCartesian f' φ'],
  p.IsHomLift g.inv (CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso p h φ φ').inv
-- Mathlib.Analysis.Normed.Group.Uniform
LocallyLipschitz.add : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {f g : α → E},
  LocallyLipschitz f → LocallyLipschitz g → LocallyLipschitz fun x => f x + g x
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The isomorphism between `G` and `G.overFin hc`.  -/
SimpleGraph.overFinIso : {V : Type u_1} → (G : SimpleGraph V) → [inst : Fintype V] → {n : ℕ} → (hc : Fintype.card V = n) → G ≃g G.overFin hc
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The constructed basis indeed is given by the images of the relations.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.basis_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) [inst_3 : Nontrivial S] (r : Unit ⊕ σ),
  (Algebra.Generators.PresentationOfFreeCotangent.Aux.basis✝ D) r =
    Algebra.Extension.Cotangent.mk ⟨(Algebra.Generators.PresentationOfFreeCotangent.Aux.pres✝ D).relation r, ⋯⟩
-- Mathlib.Tactic.GCongr.Core
/-- Annotate `e` with a `gcongrHole` mdata annotation.  -/
Mathlib.Tactic.GCongr.mkHoleAnnotation : Lean.Expr → Lean.Expr
-- Init.Control.MonadAttach
/-- Attaches a proof of `MonadAttach.CanReturn` to the return value of `x`. This proof
  can be used to prove the termination of well-founded recursive functions.
   -/
MonadAttach.attach : {m : Type u → Type v} → [self : MonadAttach m] → {α : Type u} → (x : m α) → m (Subtype (MonadAttach.CanReturn x))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.return.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId fvarId_1 : Lean.FVarId),
  (Lean.Compiler.LCNF.Code.return fvarId = Lean.Compiler.LCNF.Code.return fvarId_1) = (fvarId = fvarId_1)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α}, k ∈ Std.TreeMap.filterMap f t ↔ ∃ (h : k ∈ t), (f (t.getKey k h) t[k]).isSome = true
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_lt_sub_iff_lt_add' : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, -b < a - c ↔ c < a + b
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.pair_smul_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M} {S : Type u_6}
  [inst_3 : CommRing S] [IsDomain S] [inst_5 : Module S R] [inst_6 : Module S M] [SMulCommClass S R M]
  [IsScalarTower S R M] [Module.IsTorsionFree S R] {u : S},
  u ≠ 0 → (LinearIndependent R ![u • x, u • y] ↔ LinearIndependent R ![x, y])
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_add : ∀ {n : ℕ} (x y : ℕ), BitVec.ofNat n (x + y) = BitVec.ofNat n x + BitVec.ofNat n y
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatClamp n).toUInt16 = UInt16.ofNatLT n ⋯
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.trans.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Mul α] [inst_4 : Mul β] [inst_5 : Mul γ] (f : α ≃*o β) (g : β ≃*o γ),
  f.trans g = { toMulEquiv := (↑f).trans ↑g, map_le_map_iff' := ⋯ }
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseRightKanExtension F L]
  [inst_5 : L.HasPointwiseRightKanExtension F] (a : A) {Z : D} (h : G.obj (F.obj a) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a))
      (CategoryTheory.CategoryStruct.comp (G.map ((L.pointwiseRightKanExtensionCounit F).app a)) h) =
    CategoryTheory.CategoryStruct.comp ((L.pointwiseRightKanExtensionCounit (F.comp G)).app a) h
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.add.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (q₁ q₂ : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.add q₁ q₂ =
    q₁.liftOn₂ q₂
      (fun x x_1 =>
        match x with
        | (a, b) =>
          match x_1 with
          | (c, d) => Lean.Grind.IntModule.OfNatModule.Q.mk (a + c, b + d))
      ⋯
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.norm_eq : ∀ (p : ℝ) {x : ℝ}, ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
-- Mathlib.Order.Basic
/-- **Alias** of `lt_asymm`. -/
LT.lt.asymm : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬b < a
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.flattenList.toNatAux.eq_3 : ∀ {n : ℕ} (x_1 y : BitVec n) (rest : List (BitVec n)),
  BitVec.flattenList.toNatAux (x_1 :: y :: rest) =
    BitVec.flattenList.toNatAux (List.take ((x_1 :: y :: rest).length / 2) (x_1 :: y :: rest)) <<<
        (n * (List.drop ((x_1 :: y :: rest).length / 2) (x_1 :: y :: rest)).length) |||
      BitVec.flattenList.toNatAux (List.drop ((x_1 :: y :: rest).length / 2) (x_1 :: y :: rest))
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.valuation_isEquiv_adic_of_not_isEquiv_infty : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [v.IsRankOneDiscrete] [Valuation.IsTrivialOn K v] [inst_4 : DecidableEq (RatFunc K)],
  ¬v.IsEquiv (RatFunc.inftyValuation K) → ∃! u, v.IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) u)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.inl_ι : ∀ {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₂}
  (self : F.PushoutObjObj f₁ f₂), CategoryTheory.CategoryStruct.comp self.inl self.ι = (F.obj Y₁).map f₂
-- Mathlib.FieldTheory.Separable
Polynomial.separable_def' : ∀ {R : Type u} [inst : CommSemiring R] (f : Polynomial R), f.Separable ↔ ∃ a b, a * f + b * Polynomial.derivative f = 1
-- Init.Data.BitVec.Bitblast
BitVec.msb_umod_eq_false_of_left : ∀ {w : ℕ} {x : BitVec w}, x.msb = false → ∀ (y : BitVec w), (x % y).msb = false
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHomClass.mk : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [inst : MulOne M] [inst_1 : MulOne N]
  [inst_2 : FunLike F M N] [toMulHomClass : MulHomClass F M N] [toOneHomClass : OneHomClass F M N], MonoidHomClass F M N
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (CategoryTheory.LaxMonoidalFunctor C D)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.match_4.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) (n : ℤ),
  x = Lean.Grind.CommRing.Expr.num n →
    (match x with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.var x => h_2 x
      | a.add b => h_3 a b
      | a.mul b => h_4 a b
      | a.pow k => h_5 a k
      | Lean.Grind.CommRing.Expr.natCast n => h_6 n
      | a.sub b => h_7 a b
      | a.neg => h_8 a
      | Lean.Grind.CommRing.Expr.intCast k => h_9 k) ≍
      h_1 n
-- Mathlib.Geometry.Manifold.DerivationBundle
smoothFunctionsAlgebra : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                (M : Type u_4) →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] → Algebra 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.evalFinsetIccNat.match_1.splitter : (en em' : Q(ℕ)) →
  (motive : (s : Q(Finset ℕ)) × Q(Finset.Icc «$em'» «$en» = «$s») → Sort u_1) →
    (x : (s : Q(Finset ℕ)) × Q(Finset.Icc «$em'» «$en» = «$s»)) →
      ((s : Q(Finset ℕ)) → (hs : Q(Finset.Icc «$em'» «$en» = «$s»)) → motive ⟨s, hs⟩) → motive x
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.move_ok : ∀ {p : Turing.PartrecToTM2.Γ' → Bool} {k₁ k₂ : Turing.PartrecToTM2.K'} {q : Turing.PartrecToTM2.Λ'}
  {s : Option Turing.PartrecToTM2.Γ'} {L₁ : List Turing.PartrecToTM2.Γ'} {o : Option Turing.PartrecToTM2.Γ'}
  {L₂ : List Turing.PartrecToTM2.Γ'} {S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'},
  k₁ ≠ k₂ →
    Turing.PartrecToTM2.splitAtPred p (S k₁) = (L₁, o, L₂) →
      StateTransition.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr)
        { l := some (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := Function.update (Function.update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `ContinuousLinearMap.coe_comp`. -/
ContinuousLinearMap.coe_comp' : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂),
  ⇑(h ∘SL f) = ⇑h ∘ ⇑f
-- Lean.Elab.Binders
Lean.Elab.Term.FunBinders.State.lctx : Lean.Elab.Term.FunBinders.State → Lean.LocalContext
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bddAbove_range : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), BddAbove (Set.range f)
-- Mathlib.Data.Set.Lattice
Set.sInter_iUnion : ∀ {α : Type u_1} {ι : Sort u_5} (s : ι → Set (Set α)), ⋂₀ ⋃ i, s i = ⋂ i, ⋂₀ s i
-- Mathlib.Analysis.Matrix.Normed
/-- The norm of a matrix is the sup of the sup of the nnnorm of the entries  -/
Matrix.norm_eq_sup_sup_nnnorm : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α),
  ‖A‖ = ↑(Finset.univ.sup fun i => Finset.univ.sup fun j => ‖A i j‖₊)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.forget_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X} {f : U ⟶ V},
  (CategoryTheory.Under.forget X).map f = CategoryTheory.Under.Hom.right f
-- Mathlib.FieldTheory.KummerExtension
/-- The inverse function of `autAdjoinRootXPowSubC` if `K` has all roots of unity.
See `autAdjoinRootXPowSubCEquiv`.  -/
AdjoinRootXPowSubCEquivToRootsOfUnity : {K : Type u} →
  [inst : Field K] →
    {n : ℕ} →
      (primitiveRoots n K).Nonempty →
        {a : K} →
          Irreducible (Polynomial.X ^ n - Polynomial.C a) →
            [NeZero n] →
              (AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)) →
                ↥(rootsOfUnity n K)
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidal_leftUnitor : ∀ (M : Type u) [inst : AddMonoid M] (X : CategoryTheory.Discrete M),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor X = CategoryTheory.Discrete.eqToIso ⋯
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with scalar multiplication.  -/
InnerProductSpace.laplacianWithin_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra ℝ 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : InnerProductSpace ℝ E] [inst_4 : FiniteDimensional ℝ E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] [IsScalarTower ℝ 𝕜 F]
  {f : E → F} {x : E} {s : Set E} (v : 𝕜),
  ContDiffWithinAt ℝ 2 f s x →
    UniqueDiffOn ℝ s →
      x ∈ s → InnerProductSpace.laplacianWithin (v • f) s x = v • InnerProductSpace.laplacianWithin f s x
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.map_restrict : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₂₁ : R₂ →+* R}
  [inst_6 : RingHomSurjective σ₂₁] {p : Submodule R₂ M₂} {q : Submodule R M} {f : M₂ →ₛₗ[σ₂₁] M} (h : ∀ x ∈ p, f x ∈ q)
  (p' : Submodule R₂ ↥p),
  Submodule.map (f.restrict h) p' = Submodule.comap q.subtype (Submodule.map f (Submodule.map p.subtype p'))
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
Monotone.mul_const_of_nonpos : ∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : Preorder R] {a : R} [inst_2 : Preorder α] {f : α → R}
  [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R],
  Monotone f → a ≤ 0 → Antitone fun x => f x * a
-- Init.Data.Rat.Lemmas
Rat.normalize_eq_zero : ∀ {d : ℕ} {n : ℤ} (d0 : d ≠ 0), Rat.normalize n d d0 = 0 ↔ n = 0
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearEquiv.quotKerEquivRange.congr_simp : ∀ {R : Type u_1} {M : Type u_3} {Nₗ : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup Nₗ]
  [inst_3 : Module R M] [inst_4 : Module R Nₗ] {fₗ : M →ₗ[R] Nₗ} [inst_5 : TopologicalSpace M]
  [inst_6 : TopologicalSpace Nₗ] (hf : Topology.IsStrictMap ⇑fₗ),
  ContinuousLinearEquiv.quotKerEquivRange hf = ContinuousLinearEquiv.quotKerEquivRange hf
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_snd_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso f g g').inv
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f g) g') =
    CategoryTheory.Limits.pullback.snd f (CategoryTheory.CategoryStruct.comp g' g)
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseRequestTarget.absolute : Std.Http.URI.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.RequestTarget
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.semilength_outsidePart_lt : ∀ {p : DyckWord}, p ≠ 0 → p.outsidePart.semilength < p.semilength
-- Mathlib.Topology.Algebra.Group.Basic
/-- If addition is continuous in `α`, then it also is in `αᵃᵒᵖ`.  -/
instIsTopologicalAddGroupAddOpposite : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : AddGroup α] [IsTopologicalAddGroup α], IsTopologicalAddGroup αᵃᵒᵖ
-- Init.Data.SInt.Lemmas
Int64.ofIntLE.congr_simp : ∀ (i i_1 : ℤ) (e_i : i = i_1) (_hl : Int64.minValue.toInt ≤ i) (_hr : i ≤ Int64.maxValue.toInt),
  Int64.ofIntLE i _hl _hr = Int64.ofIntLE i_1 ⋯ ⋯
-- Mathlib.Algebra.DirectSum.Basic
/-- `mk β s x` is the element of `⨁ i, β i` that is zero outside `s`
and has coefficient `x i` for `i` in `s`.  -/
DirectSum.mk : {ι : Type v} →
  (β : ι → Type w) →
    [inst : (i : ι) → AddCommMonoid (β i)] →
      [DecidableEq ι] → (s : Finset ι) → ((i : ↑↑s) → β ↑i) →+ DirectSum ι fun i => β i
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_zero' : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R], HahnSeries.coeff 0 = 0