mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.stalkMap.congr_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (α β : X ⟶ Y) (h : α = β) (x : ↑↑X),
  AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap β x)
-- Mathlib.Topology.Bornology.Absorbs
/-- **Alias** of the reverse direction of `Set.Finite.absorbs_sInter`. -/
Absorbs.sInter : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α] {t : Set α}
  {S : Set (Set α)}, S.Finite → (∀ s ∈ S, Absorbs G₀ s t) → Absorbs G₀ (⋂₀ S) t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap.0.WeierstrassCurve.termS : Lean.ParserDescr
-- Init.Data.Nat.Basic
Nat.instTransLe : Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Lean.Declaration
Lean.DefinitionVal.getSafetyEx : Lean.DefinitionVal → Lean.DefinitionSafety
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.run' : {α : Type} →
  Aesop.EqualUpToIdsM α →
    Option Lean.MetavarContext →
      Lean.MetavarContext → Lean.MetavarContext → Bool → Lean.MetaM (α × Aesop.EqualUpToIdsM.State)
-- Init.Meta.Defs
Lean.isIdRestAscii : UInt8 → Bool
-- Mathlib.Data.Nat.PrimeFin
Nat.Prime.mem_primeFactors : ∀ {n p : ℕ}, Nat.Prime p → p ∣ n → n ≠ 0 → p ∈ n.primeFactors
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine.go.eq_5 : ∀ (fuel_2 : ℕ) (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁_2 : Lean.Grind.CommRing.Poly) (k₂ : ℤ)
  (m₂ : Lean.Grind.CommRing.Mon) (p₂_2 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.combine.go fuel_2.succ (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁_2)
      (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂_2) =
    match m₁.grevlex m₂ with
    | Ordering.eq =>
      have k := k₁ + k₂;
      bif k == 0 then Lean.Grind.CommRing.Poly.combine.go fuel_2 p₁_2 p₂_2
      else Lean.Grind.CommRing.Poly.add k m₁ (Lean.Grind.CommRing.Poly.combine.go fuel_2 p₁_2 p₂_2)
    | Ordering.gt =>
      Lean.Grind.CommRing.Poly.add k₁ m₁
        (Lean.Grind.CommRing.Poly.combine.go fuel_2 p₁_2 (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂_2))
    | Ordering.lt =>
      Lean.Grind.CommRing.Poly.add k₂ m₂
        (Lean.Grind.CommRing.Poly.combine.go fuel_2 (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁_2) p₂_2)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- Integration of `f` from `a` to `b` using the trapezoidal rule with `N+1` total evaluations of
`f`.  (Note the off-by-one problem here: `N` counts the number of trapezoids, not the number of
evaluations.)  -/
trapezoidal_integral : (ℝ → ℝ) → ℕ → ℝ → ℝ → ℝ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotating the first of two vectors by `θ` scales their Kähler form by `cos (-θ) + sin (-θ) * I`.
 -/
Orientation.kahler_rotation_left' : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (θ : Real.Angle),
  (o.kahler ((o.rotation θ) x)) y = ↑(-θ).toCircle * (o.kahler x) y
-- Mathlib.RingTheory.FinitePresentation
RingHom.FinitePresentation.comp_surjective : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  {f : A →+* B} {g : B →+* C},
  f.FinitePresentation → Function.Surjective ⇑g → (RingHom.ker g).FG → (g.comp f).FinitePresentation
-- Mathlib.Algebra.Group.Commutator
commutatorElement_def : ∀ {G : Type u_1} [inst : Group G] (g₁ g₂ : G), ⁅g₁, g₂⁆ = g₁ * g₂ * g₁⁻¹ * g₂⁻¹
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.inclusion_self : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G]
  [inst_3 : Preorder S] [inst_4 : IsConcreteLE S G] (x : ↥H), (SubgroupClass.inclusion ⋯) x = x
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_X_pow_sub_one : ∀ {R : Type u} [inst : Ring R] {n : ℕ}, 0 < n → (Polynomial.X ^ n - 1).leadingCoeff = 1
-- Mathlib.Order.Lattice
Monotone.of_left_le_map_sup : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst_1 : Preorder β] {f : α → β},
  (∀ (x y : α), f x ≤ f (x ⊔ y)) → Monotone f
-- Mathlib.Data.Matrix.Mul
diagonal_dotProduct : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NonUnitalNonAssocSemiring α]
  (v w : m → α) (i : m), Matrix.diagonal v i ⬝ᵥ w = v i * w i
-- Aesop.Search.Expansion.Norm
Aesop.NormRuleResult.proved.injEq : ∀ (steps? steps?_1 : Option (Array Aesop.Script.LazyStep)),
  (Aesop.NormRuleResult.proved steps? = Aesop.NormRuleResult.proved steps?_1) = (steps? = steps?_1)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.commandExpandersForUnsafe : Lean.Ident →
  Lean.Elab.TermElabM
    (Array
      (Lean.Name ×
        StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)))
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis.isBasis_isRestriction : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α} {N : Matroid α},
  M.IsBasis I X → N.IsRestriction M → X ⊆ N.E → N.IsBasis I X
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The morphism `S.rightHomology ⟶ A` obtained from a morphism `k : S.X₂ ⟶ A`
such that `S.f ≫ k = 0.`  -/
CategoryTheory.ShortComplex.descRightHomology : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        {A : C} →
          (k : S.X₂ ⟶ A) →
            CategoryTheory.CategoryStruct.comp S.f k = 0 → [inst_2 : S.HasRightHomology] → S.rightHomology ⟶ A
-- Lean.Meta.Tactic.SolveByElim
/-- Create or modify a `Config` which rejects branches for which `test`,
applied to the instantiations of the original goals, fails or returns `false`.
 -/
Lean.Meta.SolveByElim.SolveByElimConfig.testPartialSolutions : optParam Lean.Meta.SolveByElim.SolveByElimConfig { } →
  (List Lean.Expr → Lean.MetaM Bool) → Lean.Meta.SolveByElim.SolveByElimConfig
-- Mathlib.CategoryTheory.Sites.Continuous
/-- When we have an isomorphism `F ⋙ G ≅ FG` between continuous functors
between sites, the composition of the pushforward functors for
`G` and `F` identifies to the pushforward functor for `FG`.  -/
CategoryTheory.Functor.sheafPushforwardContinuousComp' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D E} →
                {FG : CategoryTheory.Functor C E} →
                  (F.comp G ≅ FG) →
                    (A : Type u) →
                      [inst_3 : CategoryTheory.Category.{t, u} A] →
                        (J : CategoryTheory.GrothendieckTopology C) →
                          (K : CategoryTheory.GrothendieckTopology D) →
                            (L : CategoryTheory.GrothendieckTopology E) →
                              [inst_4 : F.IsContinuous J K] →
                                [inst_5 : G.IsContinuous K L] →
                                  [inst_6 : FG.IsContinuous J L] →
                                    (G.sheafPushforwardContinuous A K L).comp (F.sheafPushforwardContinuous A J K) ≅
                                      FG.sheafPushforwardContinuous A J L
-- Init.Data.BitVec.Lemmas
BitVec.toInt_sub_of_not_ssubOverflow : ∀ {w : ℕ} {x y : BitVec w}, ¬x.ssubOverflow y = true → (x - y).toInt = x.toInt - y.toInt
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Limits of `F` are unique up to isomorphism.  -/
CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {s t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit s → CategoryTheory.Limits.IsLimit t → (s.pt ≅ t.pt)
-- Mathlib.Data.Int.Cast.Lemmas
AddEquiv.ext_int_iff : ∀ {A : Type u_5} [inst : AddMonoid A] {f g : ℤ ≃+ A}, f = g ↔ f 1 = g 1
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv.eq_1 : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] (f : 𝕜 → 𝕜'), logDeriv f = deriv f / f
-- Init.Data.List.MinMaxOn
List.minOn_eq_min : ∀ {α : Type u_1} {β : Type u_2} [inst : Min α] [inst_1 : LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMin α]
  [inst_4 : LE β] [inst_5 : DecidableLE β] {f : α → β} {l : List α} {h : l ≠ []},
  (∀ (a b : α), f a ≤ f b ↔ a ≤ b) → List.minOn f l h = l.min h
-- Mathlib.Topology.Constructions
nhds_subtype_eq_comap : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop} {x : X} {h : p x},
  nhds ⟨x, h⟩ = Filter.comap Subtype.val (nhds x)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_of_lt_add_of_nonpos_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b c : α}, a < b + c → b ≤ 0 → a < c
-- Mathlib.GroupTheory.Commutator.Basic
closureAddCommutatorRepresentatives.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G],
  closureAddCommutatorRepresentatives G =
    AddSubgroup.closure (Prod.fst '' addCommutatorRepresentatives G ∪ Prod.snd '' addCommutatorRepresentatives G)
-- Mathlib.Topology.Path
Path.trans_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X} (γ : Path x y) (γ' : Path y z) (t : ↑unitInterval),
  (γ.trans γ') t = if h : ↑t ≤ 1 / 2 then γ ⟨2 * ↑t, ⋯⟩ else γ' ⟨2 * ↑t - 1, ⋯⟩
-- Mathlib.Algebra.Homology.Embedding.Restriction
HomologicalComplex.restrictionMap_id : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff],
  HomologicalComplex.restrictionMap (CategoryTheory.CategoryStruct.id K) e =
    CategoryTheory.CategoryStruct.id (K.restriction e)
-- Lean.Meta.AbstractNestedProofs
Lean.Meta.AbstractNestedProofs.isNonTrivialProof : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Analysis.Convex.Slope
/-- If for any three points `x < y < z`, the slope of the secant line of `f : 𝕜 → 𝕜` on `[x, y]` is
strictly greater than the slope of the secant line of `f` on `[y, z]`, then `f` is strictly concave.
 -/
strictConcaveOn_of_slope_strict_anti_adjacent : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  Convex 𝕜 s →
    (∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)) →
      StrictConcaveOn 𝕜 s f
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderivWithin_prodMap : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_14} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_15}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {s : Set M} {p : M × M'} {t : Set M'} {f : M → N} {g : M' → N'},
  MDiffAt[s] f p.1 →
    MDiffAt[t] g p.2 →
      UniqueMDiffAt[s] p.1 →
        UniqueMDiffAt[t] p.2 → mfderiv[s ×ˢ t] (Prod.map f g) p = (mfderiv[s] f p.1).prodMap (mfderiv[t] g p.2)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `sub_apply`. -/
ModularForm.sub_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Sub β}
  {inst_2 : Sub F} [self : IsSubApply F α β] (f g : F) (x : α), (f - g) x = f x - g x
-- Mathlib.Order.RelSeries
RelSeries.head_map : ∀ {α : Type u_1} {r : SetRel α α} {β : Type u_2} {s : SetRel β β} (p : RelSeries r) (f : r.Hom s),
  (p.map f).head = f p.head
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.addUnit_add : ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M} (ha : IsAddUnit a) (hb : IsAddUnit b),
  ⋯.addUnit = ha.addUnit + hb.addUnit
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
MonoidHom.finsuppProd_apply : ∀ {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [inst : Zero β] [inst_1 : MulOneClass N]
  [inst_2 : CommMonoid P] (f : α →₀ β) (g : α → β → N →* P) (x : N), (f.prod g) x = f.prod fun i fi => (g i fi) x
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- A variant of `productLimitCone` using a `Small` hypothesis rather than a function to `Type`.
 -/
CategoryTheory.Limits.Types.Small.productLimitCone : {J : Type v} → (F : J → Type u) → [Small.{u, v} J] → CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor F)
-- Mathlib.Algebra.Order.Ring.Abs
abs_pow_eq_one : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {n : ℕ} (a : α),
  n ≠ 0 → (|a ^ n| = 1 ↔ |a| = 1)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Pi.uniformSpace.eq_1 : ∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)],
  Pi.uniformSpace α =
    UniformSpace.ofCoreEq (⨅ i, UniformSpace.comap (Function.eval i) (U i)).toCore Pi.topologicalSpace ⋯
-- Aesop.Tree.Data
Aesop.RappId.instLT : LT Aesop.RappId
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.map_id_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (x : IsLocalRing.ResidueField R),
  (IsLocalRing.ResidueField.map (RingHom.id R)) x = x
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instLeftCancelMonoidOfMulOpposite : {M : Type u_1} → [LeftCancelMonoid Mᵐᵒᵖ] → LeftCancelMonoid Mᵈᵐᵃ
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypeEquivSubtypePerm_apply_of_not_mem : ∀ {α : Type u_4} {p : α → Prop} [inst : DecidablePred p] {a : α} (f : Equiv.Perm (Subtype p)),
  ¬p a → ↑((Equiv.Perm.subtypeEquivSubtypePerm p) f) a = a
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.instPatternModelForallCharBool : {p : Char → Bool} → String.Slice.Pattern.Model.PatternModel p
-- Mathlib.Analysis.LocallyConvex.AbsConvex
mem_absConvexHull_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s : Set E} {x : E}, x ∈ (absConvexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → AbsConvex 𝕜 t → x ∈ t
-- Mathlib.LinearAlgebra.Finsupp.SumProd
Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr : ∀ {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_7}
  {β : Type u_8} (fg : (α →₀ M) × (β →₀ M)) (y : β),
  ((Finsupp.sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inr y) = fg.2 y
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- **Alias** of `Polynomial.eval₂_finsetSum`. -/
Polynomial.eval₂_finset_sum : ∀ {R : Type u} {S : Type v} {ι : Type y} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (s : Finset ι)
  (g : ι → Polynomial R) (x : S), Polynomial.eval₂ f x (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.eval₂ f x (g i)
-- Aesop.RuleTac.Forward.Basic
Aesop.ForwardHypData : Type
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Equivalence.toAdjunction_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.toAdjunction.unit = e.unit
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addZ_self : ∀ {R : Type r} [inst : CommRing R] (P : Fin 3 → R), WeierstrassCurve.Jacobian.addZ P P = 0
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.xNextIso.eq_1 : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι}
  (r : c.Rel i j), C.xNextIso r = CategoryTheory.eqToIso ⋯
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.List.Sort.Basic.0.List.mergeSort.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (x : List α) (x_1 : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le) (a : α) (x_2 : α → α → Bool),
  x = [a] →
    x_1 = x_2 →
      (match x, x_1 with
        | [], x => h_1 x
        | [a], x => h_2 a x
        | a :: b :: xs, le => h_3 a b xs le) ≍
        h_2 a x_2
-- Mathlib.Data.Finset.Basic
Finset.sdiff_union_erase_cancel : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, t ⊆ s → a ∈ t → s \ t ∪ t.erase a = s.erase a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_roc_eq_fallback : ∀ {m n i fallback : ℕ}, n ≤ i + m → (m<...=n).toList.getD i fallback = fallback
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset_nin_range : ∀ {A B : GrpCat} (f : A ⟶ B),
  ∀ x ∈ (GrpCat.Hom.hom f).range,
    ∀ b ∉ (GrpCat.Hom.hom f).range,
      ((GrpCat.SurjectiveOfEpiAuxs.h f) x)
          (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨b • ↑(GrpCat.Hom.hom f).range, ⋯⟩) =
        GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨(x * b) • ↑(GrpCat.Hom.hom f).range, ⋯⟩
-- Mathlib.RingTheory.WittVector.Compare
WittVector.toZModPow_compat : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (m n : ℕ) (h : m ≤ n),
  (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (WittVector.toZModPow p n) = WittVector.toZModPow p m
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.map.match_1.eq_3 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3)
  (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1) →
        motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => h_2 a x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_3 x
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.exists_mem_set : ∀ {α : Type u_1} {𝒜 : Set (Set α)}, 𝒜.Intersecting → ∀ {s t : Set α}, s ∈ 𝒜 → t ∈ 𝒜 → ∃ a ∈ s, a ∈ t
-- Lean.Parser.Term
Lean.Parser.Term.optSemicolon.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Setoid.Basic
Setoid.mk_eq_bot : ∀ {α : Type u_1} {r : α → α → Prop} (iseqv : Equivalence r), { r := r, iseqv := iseqv } = ⊥ ↔ r = fun x1 x2 => x1 = x2
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.sinhOrderIso_symm_apply : ⇑(RelIso.symm Real.sinhOrderIso) = Real.arsinh
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          (toHom : E.Hom F.toPreZeroHypercover) →
            (s₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHom.s₀ i) (toHom.s₀ j)) →
              (h₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (s₁ k)) →
                autoParam
                    (∀ {i j : E.I₀} (k : E.I₁ i j),
                      CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₁ (s₁ k)) =
                        CategoryTheory.CategoryStruct.comp (E.p₁ k) (toHom.h₀ i))
                    CategoryTheory.PreOneHypercover.Hom.w₁₁._autoParam →
                  autoParam
                      (∀ {i j : E.I₀} (k : E.I₁ i j),
                        CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₂ (s₁ k)) =
                          CategoryTheory.CategoryStruct.comp (E.p₂ k) (toHom.h₀ j))
                      CategoryTheory.PreOneHypercover.Hom.w₁₂._autoParam →
                    E.Hom F
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.instHasCoequalizerFstSigmaMapSndSigmaMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.left] [inst_3 : CategoryTheory.Limits.HasCoproduct I.right],
  CategoryTheory.Limits.HasCoequalizer I.fstSigmaMap I.sndSigmaMap
-- Mathlib.Data.Finset.Union
Finset.biUnion_congr : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Finset α} {t₁ t₂ : α → Finset β} [inst : DecidableEq β],
  s₁ = s₂ → (∀ a ∈ s₁, t₁ a = t₂ a) → s₁.biUnion t₁ = s₂.biUnion t₂
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.prodAux.eq_1 : ∀ {M : Type u_6} [inst : Monoid M], FreeMonoid.prodAux [] = 1
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.Context.mk.sizeOf_spec : ∀ (config : Lean.Meta.Simp.Config) (userConfig : Lean.Options) (zetaDeltaSet initUsedZetaDelta : Lean.FVarIdSet)
  (metaConfig indexConfig : Lean.Meta.ConfigWithKey) (maxDischargeDepth : UInt32)
  (simpTheorems : Lean.Meta.SimpTheoremsArray) (congrTheorems : Lean.Meta.SimpCongrTheorems)
  (parent? : Option Lean.Expr) (dischargeDepth : UInt32) (lctxInitIndices : ℕ) (inDSimp : Bool),
  sizeOf
      { config := config, userConfig := userConfig, zetaDeltaSet := zetaDeltaSet,
        initUsedZetaDelta := initUsedZetaDelta, metaConfig := metaConfig, indexConfig := indexConfig,
        maxDischargeDepth := maxDischargeDepth, simpTheorems := simpTheorems, congrTheorems := congrTheorems,
        parent? := parent?, dischargeDepth := dischargeDepth, lctxInitIndices := lctxInitIndices, inDSimp := inDSimp } =
    1 + sizeOf config + sizeOf userConfig + sizeOf zetaDeltaSet + sizeOf initUsedZetaDelta + sizeOf metaConfig +
                    sizeOf indexConfig +
                  sizeOf maxDischargeDepth +
                sizeOf simpTheorems +
              sizeOf congrTheorems +
            sizeOf parent? +
          sizeOf dischargeDepth +
        sizeOf lctxInitIndices +
      sizeOf inDSimp
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
borel_eq_generateFrom_Ioi : ∀ (α : Type u_1) [inst : TopologicalSpace α] [SecondCountableTopology α] [inst_2 : LinearOrder α] [OrderTopology α],
  borel α = MeasurableSpace.generateFrom (Set.range Set.Ioi)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.forIn_eq_forIn : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ}, Std.TreeSet.forIn f init t = forIn t init f
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
Matrix.submatrix_gram : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (v : n → E) {m : Set n} (f : ↑m → n),
  (Matrix.gram 𝕜 v).submatrix f f = Matrix.gram 𝕜 (v ∘ f)