mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Logic
eq_rec_constant : ∀ {α : Sort u_1} {a a' : α} {β : Sort u_2} (y : β) (h : a = a'), h ▸ y = y
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- If `ed` is an extradegeneracy for an augmented simplicial object `X`, then this
is a homotopy from `X.hom ≫ ed.section_` to `𝟙 X.left`.  -/
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject.Augmented C} →
      (ed : X.ExtraDegeneracy) →
        CategoryTheory.SimplicialObject.Homotopy (CategoryTheory.CategoryStruct.comp X.hom ed.section_)
          (CategoryTheory.CategoryStruct.id X.left)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instInv : {α : Type u} → Inv (FreeGroup α)
-- Lean.Expr
Lean.Expr.projExpr! : Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
preserves binary products.  -/
CategoryTheory.Limits.preservesBinaryProducts_of_preservesBinaryBiproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBinaryBiproducts F],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negY_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R) (u : R),
  W'.negY (u • P) = u ^ 3 * W'.negY P
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.mk.inj : ∀ {V : Type u} {G : SimpleGraph V} {verts : Set V} {Adj : V → V → Prop} {adj_sub : ∀ {v w : V}, Adj v w → G.Adj v w}
  {edge_vert : ∀ {v w : V}, Adj v w → v ∈ verts} {symm : autoParam (Std.Symm Adj) SimpleGraph.Subgraph.symm._autoParam}
  {verts_1 : Set V} {Adj_1 : V → V → Prop} {adj_sub_1 : ∀ {v w : V}, Adj_1 v w → G.Adj v w}
  {edge_vert_1 : ∀ {v w : V}, Adj_1 v w → v ∈ verts_1}
  {symm_1 : autoParam (Std.Symm Adj_1) SimpleGraph.Subgraph.symm._autoParam},
  { verts := verts, Adj := Adj, adj_sub := adj_sub, edge_vert := edge_vert, symm := symm } =
      { verts := verts_1, Adj := Adj_1, adj_sub := adj_sub_1, edge_vert := edge_vert_1, symm := symm_1 } →
    verts = verts_1 ∧ Adj = Adj_1
-- Mathlib.RingTheory.Finiteness.NilpotentKer
/-- If `I` is a finitely generated nilpotent ideal of an `R`-algebra `S`, and `T = S / I` is
`R`-finite, then `S` is also `R`-finite.  -/
Module.finite_of_surjective_of_ker_le_nilradical : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [Module.Finite R T] (f : S →ₐ[R] T),
  Function.Surjective ⇑f → RingHom.ker f ≤ nilradical S → (RingHom.ker f).FG → Module.Finite R S
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
/-- Bilipschitz maps send Delone sets to Delone sets.  -/
Delone.DeloneSet.mapBilipschitz : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : MetricSpace X] →
      [inst_1 : MetricSpace Y] →
        (f : X ≃ Y) →
          (K₁ K₂ : NNReal) →
            0 < K₁ → 0 < K₂ → AntilipschitzWith K₁ ⇑f → LipschitzWith K₂ ⇑f → Delone.DeloneSet X → Delone.DeloneSet Y
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of `Order.le_pred_of_lt`. -/
LT.lt.le_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, b < a → b ≤ Order.pred a
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_fun_finsetSum : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : AddCommMonoid γ] [inst_3 : ContinuousAdd γ] {ι : Type u_5} (s : Finset ι) (f : ι → α →ₘ[μ] γ),
  ↑(∑ i ∈ s, f i) =ᵐ[μ] fun x => ∑ i ∈ s, ↑(f i) x
-- Init.Data.BitVec.Lemmas
BitVec.getElem_extract : ∀ {n hi lo : ℕ} {x : BitVec n} {i : ℕ} (h : i < hi - lo + 1), (BitVec.extractLsb hi lo x)[i] = x.getLsbD (lo + i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P : Fin 3 → R),
  W'.dblY P = W'.negY ![W'.dblX P, W'.negDblY P, W'.dblZ P]
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `Add` across an `Equiv`  -/
Equiv.add : {α : Type u_2} → {β : Type u_3} → α ≃ β → [Add β] → Add α
-- Mathlib.NumberTheory.Multiplicity
emultiplicity_pow_sub_pow_of_prime : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {p : R},
  Prime p →
    ∀ {x y : R}, p ∣ x - y → ¬p ∣ x → ∀ {n : ℕ}, ¬p ∣ ↑n → emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y)
-- Mathlib.Topology.MetricSpace.Gluing
/-- The maps `toInductiveLimit n` are compatible with the maps `f n`.  -/
Metric.toInductiveLimit_commute : ∀ {X : ℕ → Type u} [inst : (n : ℕ) → MetricSpace (X n)] {f : (n : ℕ) → X n → X (n + 1)} (I : ∀ (n : ℕ), Isometry (f n))
  (n : ℕ), Metric.toInductiveLimit I n.succ ∘ f n = Metric.toInductiveLimit I n
-- Mathlib.Data.Multiset.Sum
Multiset.disjSum_mono_right : ∀ {α : Type u_1} {β : Type u_2} (s : Multiset α), Monotone s.disjSum
-- Mathlib.CategoryTheory.Products.Associator
/-- The associator functor `(C × D) × E ⥤ C × (D × E)`.
 -/
CategoryTheory.prod.associator : (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] → CategoryTheory.Functor ((C × D) × E) (C × D × E)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.dropWhile_prop_eq_dropWhile_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.dropWhile p = s.dropWhile fun x => decide (p x)
-- Mathlib.Logic.Equiv.Finset
Encodable.sortedUniv_nodup : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Encodable α], (Encodable.sortedUniv α).Nodup
-- Mathlib.Logic.Equiv.Defs
/-- Quotients are congruent on equivalences under equality of their relation.
An alternative is just to use rewriting with `eq`, but then computational proofs get stuck.  -/
Quot.congrRight : {α : Sort u} → {r r' : α → α → Prop} → (∀ (a₁ a₂ : α), r a₁ a₂ ↔ r' a₁ a₂) → Quot r ≃ Quot r'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} [inst_2 : Inhabited (β k')] {f : Option (β k) → Option (β k)},
  (t.alter k f).get! k' = if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).get! else t.get! k'
-- Mathlib.Analysis.Convex.Segment
mem_openSegment_of_ne_left_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [ZeroLEOneClass 𝕜] [inst_4 : Module 𝕜 E] {x y z : E}, x ≠ z → y ≠ z → z ∈ segment 𝕜 x y → z ∈ openSegment 𝕜 x y
-- Mathlib.Algebra.Order.Field.Pointwise
LinearOrderedField.smul_Ici : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {a r : K},
  0 < r → r • Set.Ici a = Set.Ici (r * a)
-- Mathlib.Topology.Semicontinuity.Basic
IsOpen.lowerSemicontinuousAt_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {x : α} {y : β} [inst_1 : Zero β]
  [inst_2 : Preorder β], IsOpen s → 0 ≤ y → LowerSemicontinuousAt (s.indicator fun _x => y) x
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
IsTranscendenceBasis.to_subtype_range : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  IsTranscendenceBasis R x → IsTranscendenceBasis R Subtype.val
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.associator_obj_inr : ∀ (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] (X : E),
  (CategoryTheory.sum.associator C D E).obj (Sum.inr X) = Sum.inr (Sum.inr X)
-- Init.Data.List.Lemmas
List.splitAt_go : ∀ {α : Type u_1} {xs : List α} {i : ℕ} {l acc : List α},
  List.splitAt.go l xs i acc = if i < xs.length then (acc.reverse ++ List.take i xs, List.drop i xs) else (l, [])
-- Lean.Elab.PreDefinition.Mutual
Lean.Elab.Mutual.addPreDefsFromUnary : Lean.LocalContext × Lean.LocalInstances →
  Array Lean.Elab.PreDefinition →
    Array Lean.Elab.PreDefinition → Lean.Elab.PreDefinition → optParam Bool true → Lean.Elab.TermElabM Unit
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.adaptExcept_EStateM : ∀ {ε ε' σ α : Type} (f : ε → ε') (x : EStateM ε σ α) (post : α → σ → Prop) (epost : ε' → σ → Prop),
  ⦃ Std.Internal.Do.wp x post fun e => epost (f e) ⦄ EStateM.adaptExcept f x ⦃ post; epost ⦄
-- Mathlib.Topology.Constructions
/-- `Pi.single i x` is continuous in `x`.  -/
continuous_single : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] [inst : (i : ι) → Zero (A i)]
  [inst_1 : DecidableEq ι] (i : ι), Continuous fun x => Pi.single i x
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.coeff_supportedEquivFinsupp_symm_apply_coe_support_val : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M) (a : ↑s →₀ S),
  (↑((MonoidAlgebra.supportedEquivFinsupp s).symm a)).coeff.support.val = Multiset.map Subtype.val a.support.val
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
/-- Given an iterator `it` and a monadic predicate `P`, `it.takeWhileM P` is an iterator that outputs
the values emitted by `it` until one of those values is rejected by `P`.
If some emitted value is rejected by `P`, the value is dropped and the iterator terminates.

If `P` is pure, then the simpler variant `takeWhile` can be used instead.

**Marble diagram (ignoring monadic effects):**

Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:

```text
it                ---a----b---c--d-e--⊥
it.takeWhileM P   ---a----b---⊥

it                ---a----⊥
it.takeWhileM P   ---a----⊥
```

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is productive

Depending on `P`, it is possible that `it.takeWhileM P` is finite (or productive) although `it` is not.
In this case, the `Finite` (or `Productive`) instance needs to be proved manually.

**Performance:**

This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then
it terminates.
 -/
Std.IterM.takeWhileM : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [Monad m] → [inst : MonadAttach m] → (P : β → m (ULift.{w, 0} Bool)) → Std.IterM m β → Std.IterM m β
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Left.pow_lt_one_iff' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftStrictMono M] {n : ℕ} {x : M},
  0 < n → (x ^ n < 1 ↔ x < 1)
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- **Class formula**. This is a special case of
`MulAction.self_equiv_sigma_orbits_quotient_stabilizer'` with `φ = Quotient.out`.  -/
MulAction.selfEquivSigmaOrbitsQuotientStabilizer : (G : Type u) →
  (X : Type v) →
    [inst : Group G] →
      [inst_1 : MulAction G X] → X ≃ (ω : Quotient (MulAction.orbitRel G X)) × G ⧸ MulAction.stabilizer G ω.out
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.ofSubsingletonLIE_apply : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] [inst_6 : Subsingleton ι] (i : ι) (a : E →L[𝕜] F),
  (ContinuousAlternatingMap.ofSubsingletonLIE i) a = (ContinuousAlternatingMap.ofSubsingleton 𝕜 E F i) a
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.SemanticTokensState : Type
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_one : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype n] (A : Matrix m n α),
  A.mulVec 1 = ∑ j, A.transpose j
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_pow_right : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m n : ℕ),
  f.natDegree ≤ m → g.leadingCoeff ^ n ≠ 0 → f.resultant (g ^ n) m = f.resultant g m ^ n
-- Plausible.Shrinkable
Plausible.instShrinkableSum : {α : Type u_1} → {β : Type u_2} → [Plausible.Shrinkable α] → [Plausible.Shrinkable β] → Plausible.Shrinkable (α ⊕ β)
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.length_vertices_pos : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), 0 < p.vertices.length
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.ComputableSmall : Type v → Type (max (u + 1) v)
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- **Alias** of `FreeGroup.reduce.eq_of_red`.

---

If a word reduces to another word, then they have a common maximal reduction.  -/
FreeGroup.red.reduce_eq : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.Red L₁ L₂ → FreeGroup.reduce L₁ = FreeGroup.reduce L₂
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.map : {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
  Std.Tactic.BVDecide.BVExpr.Cache aig →
    Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_le_maxKey_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {he : t ≠ ∅}, (cmp (t.maxKey he) ((t.insertIfNew k v).maxKey ⋯)).isLE = true
-- Mathlib.Data.NNReal.Defs
NNReal.instZero : Zero NNReal
-- Init.Data.Order.Factories
/-- This lemma characterizes in terms of `LE α` when a `Max α` instance "behaves like a supremum
operator".
 -/
Std.LawfulOrderSup.of_le : ∀ {α : Type u} [inst : Max α] [inst_1 : LE α], (∀ (a b c : α), a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c) → Std.LawfulOrderSup α
-- Aesop.RulePattern
Aesop.RulePattern.mk.inj : ∀ {pattern : Lean.Meta.AbstractMVarsResult} {argMap levelArgMap : Array (Option ℕ)}
  {discrTreeKeys : Array Lean.Meta.DiscrTree.Key} {pattern_1 : Lean.Meta.AbstractMVarsResult}
  {argMap_1 levelArgMap_1 : Array (Option ℕ)} {discrTreeKeys_1 : Array Lean.Meta.DiscrTree.Key},
  { pattern := pattern, argMap := argMap, levelArgMap := levelArgMap, discrTreeKeys := discrTreeKeys } =
      { pattern := pattern_1, argMap := argMap_1, levelArgMap := levelArgMap_1, discrTreeKeys := discrTreeKeys_1 } →
    pattern = pattern_1 ∧ argMap = argMap_1 ∧ levelArgMap = levelArgMap_1 ∧ discrTreeKeys = discrTreeKeys_1
-- Mathlib.RingTheory.MvPolynomial.Localization
/-- If `S` is the localization of `R` at a submonoid `M`, then `MvPolynomial σ S`
is the localization of `MvPolynomial σ R` at `M.map MvPolynomial.C`.

See also `Polynomial.isLocalization` for the univariate case.  -/
MvPolynomial.isLocalization : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] (M : Submonoid R) (S : Type u_3) [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [IsLocalization M S], IsLocalization (Submonoid.map MvPolynomial.C M) (MvPolynomial σ S)
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.grw.injEq : ∀ (i : Mathlib.Tactic.ClickSuggestions.GrwInfo) (arr : Array Mathlib.Tactic.ClickSuggestions.GrwLemma)
  (i_1 : Mathlib.Tactic.ClickSuggestions.GrwInfo) (arr_1 : Array Mathlib.Tactic.ClickSuggestions.GrwLemma),
  (Mathlib.Tactic.ClickSuggestions.Candidates.grw✝ i arr = Mathlib.Tactic.ClickSuggestions.Candidates.grw✝ i_1 arr_1) =
    (i = i_1 ∧ arr = arr_1)
-- Mathlib.Data.Nat.Init
Nat.decreasingInduction_succ' : ∀ {n : ℕ} {motive : (m : ℕ) → m ≤ n + 1 → Sort u_1}
  (of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯) (self : motive (n + 1) ⋯),
  Nat.decreasingInduction of_succ self ⋯ = of_succ n ⋯ self
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.of_linearEquiv_right : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') (e : M'' ≃ₗ[R] M) [hf : IsLocalizedModule S f],
  IsLocalizedModule S (f ∘ₗ ↑e)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Given an action `μ` of a Type `M` on a Type `N` and a relation `r` on `N`, informally, the
`CovariantClass` says that "the action `μ` preserves the relation `r`."

More precisely, the `CovariantClass` is a class taking two Types `M N`, together with an "action"
`μ : M → N → N` and a relation `r : N → N → Prop`.  Its unique field `elim` is the assertion that
for all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the pair
`(n₁, n₂)`, then, the relation `r` also holds for the pair `(μ m n₁, μ m n₂)`,
obtained from `(n₁, n₂)` by acting upon it by `m`.

If `m : M` and `h : r n₁ n₂`, then `CovariantClass.elim m h : r (μ m n₁) (μ m n₂)`.
 -/
CovariantClass : (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.iterate.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.SeparatingRight.toMatrix₂' : ∀ {R : Type u_1} {n : Type u_11} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] {B : (m → R) →ₗ[R] (n → R) →ₗ[R] R},
  B.SeparatingRight → ((LinearMap.toMatrix₂' R) B).SeparatingRight
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mkD_of_not_zero : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : Zero X] {f : X → R} {g : ContinuousMapZero X R}, f 0 ≠ 0 → ContinuousMapZero.mkD f g = g
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negAddY_of_X_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → W.negAddY P Q = -WeierstrassCurve.Projective.addU P Q
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.coe_singletonMonoidHom : ∀ {α : Type u_2} [inst : MulOneClass α], ⇑Set.singletonMonoidHom = singleton
-- Lean.LocalContext
/-- Returns true if this is an `ldecl` with a visible value.

If `allowNondep` is true then includes `ldecl`s with `nondep := true`, whose values are normally hidden.
 -/
Lean.LocalDecl.isLet : Lean.LocalDecl → optParam Bool false → Bool
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.coproductIso_mk_comp_inv : ∀ {J : Type v} (F : J → Type (max v u)) (j : J),
  CategoryTheory.CategoryStruct.comp (TypeCat.ofHom fun x => ⟨j, x⟩) (CategoryTheory.Limits.Types.coproductIso F).inv =
    CategoryTheory.Limits.Sigma.ι F j
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.notValue.sizeOf_spec : ∀ (bvarIdx : ℕ) (strict : Bool),
  sizeOf (Lean.Meta.Grind.EMatchTheoremConstraint.notValue bvarIdx strict) = 1 + sizeOf bvarIdx + sizeOf strict
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.mem_cycleFactorsFinset_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f p : Equiv.Perm α},
  p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.symm_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A),
  P.symm.ι = P.ι
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulElemClosedBallOfNatReal : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [NormedSpace 𝕜 E] → {r : ℝ} → SMul ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)
-- Mathlib.Order.Bounds.Basic
bddAbove_singleton : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, BddAbove {a}
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_apply_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜) (x : E) (n : ℕ),
  ((FormalMultilinearSeries.ofScalars E c n) fun x_1 => x) = c n • x ^ n
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_map_ite_eq : ∀ {G : Type u_7} [inst : AddCommGroup G] {A : Type u_8} [inst_1 : DecidableEq A] (l : List A) (f g : A → G) (a : A),
  (List.map (fun x => if x = a then f x else g x) l).sum = List.count a l • (f a - g a) + (List.map g l).sum
-- Mathlib.Data.Finset.Image
Finset.Nonempty.image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α},
  s.Nonempty → ∀ (f : α → β), (Finset.image f s).Nonempty
-- Mathlib.Data.Set.Card
Set.encard_sdiff : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → s.Finite → (t \ s).encard = t.encard - s.encard
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.instReprLabel.repr : Lean.Meta.NormCast.Label → ℕ → Std.Format
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.norm_up : ∀ {E : Type u_2} [inst : Norm E] (x : E), ‖{ down := x }‖ = ‖x‖
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.coe_neLocus : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N] (f g : α →₀ N),
  ↑(f.neLocus g) = {x | f x ≠ g x}
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.mul_of_isUnit : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x y : R)
  [IsLocalization.Away x S], IsUnit ((algebraMap R S) y) → IsLocalization.Away (x * y) S
-- Std.Internal.UV.Timer
/-- This function has different behavior depending on the state of the `Timer`:
- If it is initial or finished this is a no-op.
- If it is running, the promise generated by the `next` function is dropped.
  - If `repeating` is `false` then it sets the timer to the initial state.
 -/
Std.Internal.UV.Timer.cancel : Std.Internal.UV.Timer → IO Unit
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.String.pushHex.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive n
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_mapDomain : ∀ {α : Type u_1} (R : Type u_5) [inst : Semiring R] {α' : Type u_7} {M' : Type u_8} [inst_1 : AddCommMonoid M']
  [inst_2 : Module R M'] {v' : α' → M'} (f : α → α') (l : α →₀ R),
  (Finsupp.linearCombination R v') (Finsupp.mapDomain f l) = (Finsupp.linearCombination R (v' ∘ f)) l
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.continuous_mk : ∀ {M : Type u_1} [inst : TopologicalSpace M], Continuous ⇑DomMulAct.mk
-- Mathlib.Order.Interval.Multiset
Multiset.Ioc_eq_zero_iff : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, Multiset.Ioc a b = 0 ↔ ¬a < b
-- Mathlib.NumberTheory.LucasPrimality
/-- If `p` is prime, then there exists an `a` such that `a^(p-1) = 1 mod p`
and `a^((p-1)/q) ≠ 1 mod p` for all prime factors `q` of `p-1`.
The multiplicative group mod `p` is cyclic, so `a` can be any generator of the group
(which must have order `p-1`).
 -/
reverse_lucas_primality : ∀ (p : ℕ), Nat.Prime p → ∃ a, a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.map_variableChange : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) {A : Type v}
  [inst_1 : CommRing A] (φ : R →+* A), C.map φ • W.map φ = (C • W).map φ
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.logRatio_mono : ∀ {c d : ENNReal},
  2⁻¹ < c → d < 1 → c ≤ d → ProbabilityTheory.Fernique.logRatio c ≤ ProbabilityTheory.Fernique.logRatio d
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem.detail? : Lean.Lsp.ResolvableCompletionItem → Option String