mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.coe_autToPow_apply : ∀ (R : Type u_4) {S : Type u_5} [inst : CommRing S] [inst_1 : IsDomain S] {μ : S} {n : ℕ} (hμ : IsPrimitiveRoot μ n)
  [inst_2 : CommRing R] [inst_3 : Algebra R S] [inst_4 : NeZero n] (f : S ≃ₐ[R] S),
  ↑((IsPrimitiveRoot.autToPow R hμ) f) = ↑⋯.choose
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.coe_sInf : ∀ {R : Type u} [inst : NonAssocSemiring R] (S : Set (Subsemiring R)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.withAppRevAux : {α : Sort u_1} → (Lean.Expr → Array Lean.Expr → α) → Lean.Expr → Array Lean.Expr → α
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
/-- A pre-`0`-hypercover family on `C` is a property on the category of pre-`0`-hypercovers
for every `X : C` that is invariant under deduplication.
The data of a pre-`0`-hypercover family is the same as the data of a precoverage
(see: `Precoverage.equivPreZeroHypercoverFamily`).
 -/
CategoryTheory.PreZeroHypercoverFamily : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max (u + 1) (v + 1))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k a : α} {v : β k}, a ∈ Std.DTreeMap.Internal.Impl.insert! k v t ↔ compare k a = Ordering.eq ∨ a ∈ t
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.mem_toSubmonoid : ∀ {M : Type u_1} [inst : MulOneClass M] {s : SaturatedSubmonoid M} {x : M}, x ∈ s.toSubmonoid ↔ x ∈ s
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
fderiv_continuousAlternatingMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H] {f : E → G [⋀^ι]→L[𝕜] H} {g : E → F →L[𝕜] G} {x : E}
  [inst_9 : Fintype ι] [inst_10 : DecidableEq ι],
  DifferentiableAt 𝕜 f x →
    DifferentiableAt 𝕜 g x →
      fderiv 𝕜 (fun x => (f x).compContinuousLinearMap (g x)) x =
        ContinuousAlternatingMap.compContinuousLinearMapCLM (g x) ∘SL fderiv 𝕜 f x +
          (f x).fderivCompContinuousLinearMap (g x) ∘SL fderiv 𝕜 g x
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Bundle.Pretrivialization.continuousAlternatingMapCoordChange.eq_1 : ∀ (𝕜 : Type u_1) (ι : Type u_2) [inst : NontriviallyNormedField 𝕜] {B : Type u_3} [inst_1 : TopologicalSpace B]
  {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_5}
  [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜 (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  (e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [inst_12 : Bundle.Trivialization.IsLinear 𝕜 e₁] [inst_13 : Bundle.Trivialization.IsLinear 𝕜 e₁']
  [inst_14 : Bundle.Trivialization.IsLinear 𝕜 e₂] [inst_15 : Bundle.Trivialization.IsLinear 𝕜 e₂'] (b : B),
  Bundle.Pretrivialization.continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂' b =
    ↑((Bundle.Trivialization.coordChangeL 𝕜 e₁' e₁ b).symm.continuousAlternatingMapCongr
        (Bundle.Trivialization.coordChangeL 𝕜 e₂ e₂' b))
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_summable : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : CharZero 𝕂] [ContinuousSMul ℚ 𝕂]
  [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸),
  Summable fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyLE?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyLE? k = t₂.getKeyLE? k
-- Init.Data.Order.Ord
Array.instReflOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.ReflOrd α], Std.ReflOrd (Array α)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {fallback : β}, k ∉ t₁ → Std.ExtDTreeMap.Const.getD (t₁ \ t₂) k fallback = fallback
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.pair.inj : ∀ {ι : Type v} {a a_1 a_2 a_3 : ι},
  CategoryTheory.Pairwise.pair a a_1 = CategoryTheory.Pairwise.pair a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.eq_1 : ∀ (α : Type u_1), WithOne α = Option α
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_sub_linearMap : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (D1 D2 : Derivation R A M),
  ↑(D1 - D2) = ↑D1 - ↑D2
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instModuleOfSMulCommClassRealOfContinuousConstSMul : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} →
              {K : TopologicalSpace.Compacts E} →
                {R : Type u_5} →
                  [inst_4 : Semiring R] →
                    [inst_5 : Module R F] →
                      [SMulCommClass ℝ R F] → [ContinuousConstSMul R F] → Module R (ContDiffMapSupportedIn E F n K)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The `0`-hypercover defined by a single covering morphism.  -/
CategoryTheory.Precoverage.ZeroHypercover.singleton : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {S T : C} → (f : S ⟶ T) → CategoryTheory.Presieve.singleton f ∈ J.coverings T → J.ZeroHypercover T
-- Mathlib.Data.Fintype.Card
Finite.injective_iff_surjective : ∀ {α : Type u_1} [Finite α] {f : α → α}, Function.Injective f ↔ Function.Surjective f
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqnsExtState.mk.sizeOf_spec : ∀ (map : Lean.PHashMap Lean.Name Lean.Meta.Match.MatchEqns) (eqns : Lean.PHashSet Lean.Name),
  sizeOf { map := map, eqns := eqns } = 1 + sizeOf map + sizeOf eqns
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_subRight_nhdsNE : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {c a : G},
  Filter.map (fun x => x - c) (nhdsWithin a {a}ᶜ) = nhdsWithin (a - c) {a - c}ᶜ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isNone_maxKey?_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.maxKey?.isNone = t.isEmpty
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.cg_closure_singleton : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (x : M),
  ((FirstOrder.Language.Substructure.closure L).toFun {x}).CG
-- Lean.Elab.Tactic.Omega.Core
/-- Folding `addEquality` over a list.  -/
Lean.Elab.Tactic.Omega.Problem.addEqualities : Lean.Elab.Tactic.Omega.Problem →
  List (ℤ × Lean.Omega.Coeffs × Option Lean.Elab.Tactic.Omega.Proof) → Lean.Elab.Tactic.Omega.Problem
-- Lean.Environment
Lean.PersistentEnvExtension.mk.sizeOf_spec : ∀ {α β σ : Type} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ]
  (toEnvExtension : Lean.EnvExtension (Lean.PersistentEnvExtensionState α σ)) (name : Lean.Name)
  (addImportedFn : Array (Array α) → Lean.ImportM σ) (addEntryFn : σ → β → σ)
  (exportEntriesFn : Lean.Environment → σ → Lean.OLeanEntries (Array α)) (statsFn : σ → Std.Format),
  sizeOf
      { toEnvExtension := toEnvExtension, name := name, addImportedFn := addImportedFn, addEntryFn := addEntryFn,
        exportEntriesFn := exportEntriesFn, statsFn := statsFn } =
    1 + sizeOf toEnvExtension + sizeOf name
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Evaluation of an exact pairing.

Do not use directly. Use `ExactPairing.evaluation` instead.  -/
CategoryTheory.ExactPairing.evaluation' : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {X Y : C} →
        [self : CategoryTheory.ExactPairing X Y] →
          CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Analysis.Normed.Lp.WithLp
/-- Converts an element of `V` to an element of `WithLp p V`.  -/
WithLp.toLp : (p : ENNReal) → {V : Type u_1} → V → WithLp p V
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.Model.isSatisfiable : ∀ {L : FirstOrder.Language} {T : L.Theory} (M : Type w) [Nonempty M] [inst : L.Structure M] [M ⊨ T], T.IsSatisfiable
-- Mathlib.Algebra.Polynomial.EraseLead
/-- Let `φ : R[x] → S[x]` be an additive map, `k : ℕ` a bound, and `fu : ℕ → ℕ` a
"sufficiently monotone" map.  Assume also that
* `φ` maps to `0` all monomials of degree less than `k`,
* `φ` maps each monomial `m` in `R[x]` to a polynomial `φ m` of degree `fu (deg m)`.

Then, `φ` maps each polynomial `p` in `R[x]` to a polynomial of degree `fu (deg p)`.  -/
Polynomial.mono_map_natDegree_eq : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} {F : Type u_3} [inst_1 : Semiring S]
  [inst_2 : FunLike F (Polynomial R) (Polynomial S)] [AddMonoidHomClass F (Polynomial R) (Polynomial S)] {φ : F}
  {p : Polynomial R} (k : ℕ) (fu : ℕ → ℕ),
  (∀ {n : ℕ}, n ≤ k → fu n = 0) →
    (∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m) →
      (∀ {f : Polynomial R}, f.natDegree < k → φ f = 0) →
        (∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((Polynomial.monomial n) c)).natDegree = fu n) → (φ p).natDegree = fu p.natDegree
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
/-- The index type of cells in a relative cell complex.  -/
HomotopicalAlgebra.RelativeCellComplex.Cells : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} → {f : X ⟶ Y} → HomotopicalAlgebra.RelativeCellComplex basicCell f → Type (max u_1 w')
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.NatTrans.tensor_naturality_assoc : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  {F G F' G' : CategoryTheory.Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X Y X' Y' : J} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F'.obj Y) (G'.obj Y') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (G.map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app Y) (β.app Y')) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app X'))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F'.map f) (G'.map g)) h)
-- Mathlib.RepresentationTheory.Basic
Representation.instHMulMonoidAlgebraAsModuleOfMulAction : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring k] →
      [inst_1 : Group G] → HMul (MonoidAlgebra k G) (Representation.ofMulAction k G G).asModule (MonoidAlgebra k G)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Functor.isEquivalence_mapArrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsEquivalence], F.mapArrow.IsEquivalence
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.cell_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) (i : c.ι),
  c.cell i = CategoryTheory.CategoryStruct.comp (c.cofan₂.inj i) c.g₂
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.comp_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup P] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : LieRingModule L M] [inst_9 : LieRingModule L N]
  [inst_10 : LieRingModule L P] (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) (m : M), (f.comp g) m = f (g m)
-- Lean.Util.Diff
/-- Add an element from the left array to a histogram  -/
Lean.Diff.Histogram.addLeft : {α : Type u_1} →
  [inst : BEq α] →
    [inst_1 : Hashable α] →
      {lsize rsize : ℕ} → Lean.Diff.Histogram α lsize rsize → Fin lsize → α → Lean.Diff.Histogram α lsize rsize
-- Mathlib.Data.Seq.Basic
Stream'.Seq.fold_nil : ∀ {α : Type u} {β : Type v} (init : β) (f : β → α → β),
  Stream'.Seq.nil.fold init f = Stream'.Seq.cons init Stream'.Seq.nil
-- Mathlib.Algebra.Torsor.Defs
/-- An `AddGroup G` is a torsor for itself. -/
AddGroup.instAddTorsor : (G : Type u_1) → [inst : AddGroup G] → AddTorsor G G
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.buckets_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {c i : ℕ} {h : i < (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c)).buckets.size},
  (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c)).buckets[i] = Std.DHashMap.Internal.AssocList.nil
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
CategoryTheory.coev_expComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.MonoidalClosed D]
  [inst_6 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  (A B : C),
  CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.ihom.coev A).app B))
      ((CategoryTheory.expComparison F A).natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev (F.obj A)).app (F.obj B))
      ((CategoryTheory.ihom (F.obj A)).map
        (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)))
-- Mathlib.Topology.Compactness.Paracompact
/-- A locally compact sigma compact Hausdorff space is paracompact. See also
`refinement_of_locallyCompact_sigmaCompact_of_nhds_basis` for a more precise statement.  -/
paracompact_of_locallyCompact_sigmaCompact : ∀ {X : Type v} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] [T2Space X],
  ParacompactSpace X
-- Init.Grind.Config
Lean.Grind.CutsatConfig.mk.sizeOf_spec : ∀ (toNoopConfig : Lean.Grind.NoopConfig), sizeOf { toNoopConfig := toNoopConfig } = 1 + sizeOf toNoopConfig
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.avgRisk_of_isEmpty'' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {κ : ProbabilityTheory.Kernel 𝓧 𝓨}
  {π : MeasureTheory.Measure Θ} [IsEmpty Θ], ProbabilityTheory.avgRisk ℓ P κ π = 0
-- Mathlib.RingTheory.Invariant.Basic
Algebra.IsInvariant.charpoly_mem_lifts : ∀ (A : Type u_1) (B : Type u_2) (G : Type u_3) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [Algebra.IsInvariant A B G] [inst_6 : Fintype G] (b : B),
  MulSemiringAction.charpoly G b ∈ Polynomial.lifts (algebraMap A B)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.inter_sdiv_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s₁ s₂ t : Set β}, s₁ ∩ s₂ /ₛ t ⊆ (s₁ /ₛ t) ∩ (s₂ /ₛ t)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.differentiableOn_negMulLog : DifferentiableOn ℝ Real.negMulLog {0}ᶜ
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.isOrdered.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Option α → Sort u_2) (l r : α) (h_1 : (l r : α) → motive (some l) (some r))
  (h_2 : (x x_1 : Option α) → motive x x_1),
  (match some l, some r with
    | some l, some r => h_1 l r
    | x, x_1 => h_2 x x_1) =
    h_1 l r
-- Mathlib.LinearAlgebra.Trace
LinearMap.traceAux_def : ∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (b : Module.Basis ι R M) (f : M →ₗ[R] M),
  (LinearMap.traceAux R b) f = ((LinearMap.toMatrix b b) f).trace
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α]
  {f : α → β → γ} {k : α}, (Std.HashMap.map f m)[k]? = Option.map (f k) m[k]?
-- Mathlib.Computability.Ackermann
lt_ack_left : ∀ (m n : ℕ), m < ack m n
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_and_le_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  (Filter.blimsup u f fun x => p x ∧ q x) ≤ Filter.blimsup u f p ⊓ Filter.blimsup u f q
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add_self_of_Y_ne' : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ y₁ : F}
  {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ ≠ W.negY x₁ y₁),
  WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ + WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ =
    -WeierstrassCurve.Affine.Point.some (W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)) (W.negAddY x₁ x₁ y₁ (W.slope x₁ x₁ y₁ y₁))
        ⋯
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_lt_div_iff_lt_mul' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, b⁻¹ < a / c ↔ c < a * b
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.join_sum : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ι : Type u_3} (m : ι → MeasureTheory.Measure (MeasureTheory.Measure α)),
  (MeasureTheory.Measure.sum m).join = MeasureTheory.Measure.sum fun i => (m i).join
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_add : ∀ {R : Type u_1} [inst : Semiring R] (φ ψ : Polynomial R), ↑(φ + ψ) = ↑φ + ↑ψ
-- Mathlib.Order.Filter.Defs
/-- The supremum of two filters is the filter that contains sets that belong to both filters.  -/
Filter.instSup : {α : Type u_1} → Max (Filter α)
-- Init.System.IO
/-- The stream should be inherited from the parent process.  -/
IO.Process.Stdio.inherit : IO.Process.Stdio
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOver_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X A : C), ((CategoryTheory.toOver X).obj A).left = CategoryTheory.MonoidalCategoryStruct.tensorObj A X
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_roc : ∀ {m n i fallback : ℕ}, (m<...=n).toArray.getD i fallback = if i < n - m then m + 1 + i else fallback
-- Init.Data.Fin.Lemmas
Fin.castLT_mk : ∀ (i n m : ℕ) (hn : i < n) (hm : i < m), ⟨i, hn⟩.castLT hm = ⟨i, hm⟩
-- Init.Data.Vector.Int
Vector.sum_replicate_int : ∀ {n : ℕ} {a : ℤ}, (Vector.replicate n a).sum = ↑n * a
-- Lean.Elab.InfoTree.Types
Lean.Elab.ErrorNameInfo.stx : Lean.Elab.ErrorNameInfo → Lean.Syntax
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrArgKind.fixedNoParam.sizeOf_spec : sizeOf Lean.Meta.CongrArgKind.fixedNoParam = 1
-- Mathlib.Tactic.Ring.Common
/-- A characteristic zero ring instance on `α`, if available.  -/
Mathlib.Tactic.Ring.Common.Cache.czα : {u : Lean.Level} →
  {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → Mathlib.Tactic.Ring.Common.Cache sα → Option Q(CharZero «$α»)
-- Mathlib.Data.List.Sort
List.sortedGT_map_toDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, (List.map (⇑OrderDual.toDual) l).SortedGT ↔ l.SortedLT
-- Std.Do.Internal.Ensures.Def
/-- `IsAttach attach` says `attach` tags each value of `x` with its `MayReturn` proof
in a bind-faithful way.  -/
Std.Do.Internal.IsAttach : {m : Type u → Type v} → [inst : Bind m] → (⦃α : Type u⦄ → (x : m α) → m { a // Std.Do.Internal.MayReturn x a }) → Prop
-- Mathlib.CategoryTheory.Products.Basic
_private.Mathlib.CategoryTheory.Products.Basic.0.CategoryTheory.prodOpEquiv.match_3.splitter : (C : Type u_3) →
  [inst : CategoryTheory.Category.{u_1, u_3} C] →
    {D : Type u_4} →
      [inst_1 : CategoryTheory.Category.{u_2, u_4} D] →
        {X Y : Cᵒᵖ × Dᵒᵖ} →
          (motive : (X ⟶ Y) → Sort u_5) → (x : X ⟶ Y) → ((f : X.1 ⟶ Y.1) → (g : X.2 ⟶ Y.2) → motive (f, g)) → motive x
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.instInvolutiveStarId : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → [CompleteSpace E] → InvolutiveStar (E →L[𝕜] E)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.mono : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → ∀ {t : Set E}, t ⊆ s → ContDiffOn 𝕜 n f t
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.map_H : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.IsPreservedBy F],
  (h.map F).H = F.obj h.H
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a b : α} {fallback : β}, cmp a b = Ordering.eq → t.getD a fallback = t.getD b fallback
-- Mathlib.NumberTheory.Dioph
Poly.map_apply : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (g : Poly α) (v : β → ℕ), (Poly.map f g) v = g (v ∘ f)
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_domRestrict_le_range : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [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 τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (S : Submodule R M), (f.domRestrict S).range ≤ f.range
-- Mathlib.Data.Finmap
Finmap.keys.eq_1 : ∀ {α : Type u} {β : α → Type v} (s : Finmap β), s.keys = { val := s.entries.keys, nodup := ⋯ }
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
measurable_of_isOpen : ∀ {γ : Type u_3} {δ : Type u_5} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ]
  [inst_3 : MeasurableSpace δ] {f : δ → γ}, (∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)) → Measurable f
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.mk : {ι : Type u_3} →
  {M : Type u_4} →
    [inst : AddCommMonoid M] →
      {I : WithTop (BoxIntegral.Box ι)} →
        (toFun : BoxIntegral.Box ι → M) →
          (∀ (J : BoxIntegral.Box ι),
              ↑J ≤ I → ∀ (π : BoxIntegral.Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun Ji = toFun J) →
            BoxIntegral.BoxAdditiveMap ι M I