mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- If `ξ` is rational, then the good rational approximations to `ξ` have bounded
numerator and denominator.  -/
Rat.den_le_and_le_num_le_of_sub_lt_one_div_den_sq : ∀ {ξ q : ℚ}, |ξ - q| < 1 / ↑q.den ^ 2 → q.den ≤ ξ.den ∧ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
-- Init.WF
WellFounded.fix_eq : ∀ {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x)
  (x : α), hwf.fix F x = F x fun y x => hwf.fix F y
-- Batteries.Lean.Meta.Basic
/-- Erase any assignment or delayed assignment of the given metavariable.
 -/
Lean.MVarId.eraseAssignment : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MVarId → m Unit
-- Mathlib.Data.ENNReal.Basic
ENNReal.le_coe_iff : ∀ {a : ENNReal} {r : NNReal}, a ≤ ↑r ↔ ∃ p, a = ↑p ∧ p ≤ r
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformlyOn.neg` -/
TendstoUniformlyOn.fun_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f : ι → β → α} {g : β → α} {s : Set β},
  TendstoUniformlyOn f g l s → TendstoUniformlyOn (fun i i_1 => -f i i_1) (fun i => -g i) l s
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
AffineBasis.card_eq_finrank_add_one : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : DivisionRing k] [inst_3 : Module k V] [inst_4 : Fintype ι] (b : AffineBasis ι k P),
  Fintype.card ι = Module.finrank k V + 1
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] [inst_5 : SMul N α] [SMulCommClass M N α]
  [inst_7 : MeasureTheory.SMulInvariantMeasure N α μ] [inst_8 : MeasurableConstSMul N α],
  SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)
-- Std.Time.DateTime
Std.Time.DateTime.instHAddOffset_3 : HAdd Std.Time.DateTime Std.Time.Minute.Offset Std.Time.DateTime
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- A **left-uniform group** is a topological group endowed with the associated
left uniform structure: the uniformity filter `𝓤 G` is the inverse image of `𝓝 1` by the map
`(x, y) ↦ x⁻¹ * y`.

In other words, we declare that two points `x` and `y` are infinitely close
precisely when `x⁻¹ * y` is infinitely close to `1`.  -/
IsLeftUniformGroup : (G : Type u_7) → [UniformSpace G] → [Group G] → Prop
-- Mathlib.FieldTheory.Finite.Basic
/-- In a finite field of characteristic `2`, all elements are squares.  -/
FiniteField.isSquare_of_char_two : ∀ {F : Type u_3} [inst : Field F] [Finite F], ringChar F = 2 → ∀ (a : F), IsSquare a
-- Batteries.Data.Fin.Lemmas
Fin.find?_eq_some_iff : ∀ {n : ℕ} {i : Fin n} {p : Fin n → Bool}, Fin.find? p = some i ↔ p i = true ∧ ∀ j < i, p j = false
-- Init.Data.Slice.Operations
/-- Allocates a new list that contains the elements of the slice.  -/
Std.Slice.toList : {γ : Type u_1} → {α β : Type u_2} → [Std.ToIterator (Std.Slice γ) Id α β] → [Std.Iterator α Id β] → Std.Slice γ → List β
-- Mathlib.Combinatorics.Matroid.Sum
_private.Mathlib.Combinatorics.Matroid.Sum.0.Equiv.sumEquivSigmaBool.match_1.splitter : (α β : Type u_1) →
  (motive : ((b : Bool) × bif b then β else α) → Sort u_2) →
    (s : (b : Bool) × bif b then β else α) →
      ((a : bif false then β else α) → motive ⟨false, a⟩) → ((b : bif true then β else α) → motive ⟨true, b⟩) → motive s
-- Mathlib.Topology.Bornology.BoundedOperation
BoundedAdd.mk : ∀ {R : Type u_1} [inst : Bornology R] [inst_1 : Add R],
  (∀ {s t : Set R}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s + t)) → BoundedAdd R
-- Lean.Meta.Basic
/-- Similar to `withLocalDecl`, but it does **not** check whether the new variable is a local instance or not.
 -/
Lean.Meta.withLocalDeclNoLocalInstanceUpdate : {α : Type} → Lean.Name → Lean.BinderInfo → Lean.Expr → (Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biprod.ext_from_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {Z : C} {f g : X ⊞ Y ⟶ Z},
  f = g ↔
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl f =
        CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl g ∧
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr f =
        CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr g
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.leadingCoeff_quadratic : ∀ {R : Type u} {a b c : R} [inst : Semiring R],
  a ≠ 0 → (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).leadingCoeff = a
-- Mathlib.RingTheory.Polynomial.Basic
/-- The `R`-submodule of `R[X]` consisting of polynomials of degree ≤ `n`.  -/
Polynomial.degreeLE : (R : Type u) → [inst : Semiring R] → WithBot ℕ → Submodule R (Polynomial R)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toArray_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} {it : Std.IterM m β} [inst : Monad m] [LawfulMonad m]
  [inst_2 : Std.Iterator α m β] [Std.Iterators.Finite α m],
  it.toArray = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => do
        let __do_lift ← it'.toArray
        pure (#[out] ++ __do_lift)
      | Std.IterStep.skip it' => it'.toArray
      | Std.IterStep.done => pure #[]
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- Monomorphisms over an object `f : Over A` in an over category
are equivalent to monomorphisms over the source of `f`.
 -/
CategoryTheory.MonoOver.slice : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : C} →
      {f : CategoryTheory.Over A} →
        (∀ (g : CategoryTheory.MonoOver f),
            CategoryTheory.Mono (f.iteratedSliceEquiv.functor.obj ((CategoryTheory.MonoOver.forget f).obj g)).hom) →
          (∀ (g : CategoryTheory.MonoOver f.left),
              CategoryTheory.Mono
                (f.iteratedSliceEquiv.inverse.obj ((CategoryTheory.MonoOver.forget f.left).obj g)).hom) →
            (CategoryTheory.MonoOver f ≌ CategoryTheory.MonoOver f.left)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.mk.inj : ∀ {R : Type u_1} {R₂ : Type u_2} {inst : Semiring R} {inst_1 : Semiring R₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  {inst_2 : RingHomInvPair σ₁₂ σ₂₁} {inst_3 : RingHomInvPair σ₂₁ σ₁₂} {E : Type u_11} {E₂ : Type u_12}
  {inst_4 : SeminormedAddCommGroup E} {inst_5 : SeminormedAddCommGroup E₂} {inst_6 : Module R E} {inst_7 : Module R₂ E₂}
  {toLinearEquiv : E ≃ₛₗ[σ₁₂] E₂} {norm_map' : ∀ (x : E), ‖toLinearEquiv x‖ = ‖x‖} {toLinearEquiv_1 : E ≃ₛₗ[σ₁₂] E₂}
  {norm_map'_1 : ∀ (x : E), ‖toLinearEquiv_1 x‖ = ‖x‖},
  { toLinearEquiv := toLinearEquiv, norm_map' := norm_map' } =
      { toLinearEquiv := toLinearEquiv_1, norm_map' := norm_map'_1 } →
    toLinearEquiv = toLinearEquiv_1
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isClosed_setOfPred_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {q : Y → Prop}
  (f : X ≃ₜ Y), IsClopen {x | p x} → IsClopen {y | q y} → IsClosed {x | p x ↔ q (f x)}
-- Mathlib.Analysis.Calculus.Deriv.Pow
derivWithin_pow_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜},
  UniqueDiffWithinAt 𝕜 s x → ∀ (n : ℕ), derivWithin (fun x => x ^ n) s x = ↑n * x ^ (n - 1)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_directed : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ∞}, Directed (fun x1 x2 => x1 ≤ x2) fun l => (f.genEigenspace μ) ↑↑l
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.surjectiveOnStalks_iff_forall_maximal' : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S},
  f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.map_comp : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₀ x₁ : X} {Z : Type u_1}
  [inst_2 : TopologicalSpace Z] {p : Path.Homotopic.Quotient x₀ x₁} {f : C(X, Y)} {g : C(Y, Z)},
  p.map (g.comp f) = (p.map f).map g
-- Batteries.Tactic.Lint.Misc
/-- A linter for checking that declarations aren't syntactic tautologies.
Checks whether a lemma is a declaration of the form `∀ a b ... z, e₁ = e₂`
where `e₁` and `e₂` are identical exprs.
We call declarations of this form syntactic tautologies.
Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving basic facts
with rfl when elaboration results in a different term than the user intended.  -/
Batteries.Tactic.Lint.synTaut : Batteries.Tactic.Lint.Linter
-- Mathlib.Topology.Constructions
nhds_toAdd : ∀ {X : Type u} [inst : TopologicalSpace X] (x : Multiplicative X),
  nhds (Multiplicative.toAdd x) = Filter.map (⇑Multiplicative.toAdd) (nhds x)
-- Mathlib.CategoryTheory.Sums.Basic
_private.Mathlib.CategoryTheory.Sums.Basic.0.CategoryTheory.sum.match_3.eq_1 : ∀ (C : Type u_1) (D : Type u_2) (motive : C ⊕ D → Sort u_3) (X : C) (h_1 : (X : C) → motive (Sum.inl X))
  (h_2 : (X : D) → motive (Sum.inr X)),
  (match Sum.inl X with
    | Sum.inl X => h_1 X
    | Sum.inr X => h_2 X) =
    h_1 X
-- Mathlib.Order.UpperLower.Relative
IsRelLowerSet.sUnion : ∀ {α : Type u_1} {P : α → Prop} [inst : LE α] {S : Set (Set α)}, (∀ s ∈ S, IsRelLowerSet s P) → IsRelLowerSet (⋃₀ S) P
-- Mathlib.Data.Matrix.Mul
Matrix.transpose_vecMulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : CommMagma α] (w : m → α) (v : n → α),
  (Matrix.vecMulVec w v).transpose = Matrix.vecMulVec v w
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `NonAssocCommRing` instance along a surjective function.  -/
Function.Surjective.nonAssocCommRing : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : Neg S] →
                  [inst_5 : Sub S] →
                    [inst_6 : SMul ℕ S] →
                      [inst_7 : SMul ℤ S] →
                        [inst_8 : NatCast S] →
                          [inst_9 : IntCast S] →
                            [inst_10 : NonAssocCommRing R] →
                              f 0 = 0 →
                                f 1 = 1 →
                                  (∀ (x y : R), f (x + y) = f x + f y) →
                                    (∀ (x y : R), f (x * y) = f x * f y) →
                                      (∀ (x : R), f (-x) = -f x) →
                                        (∀ (x y : R), f (x - y) = f x - f y) →
                                          (∀ (n : ℕ) (x : R), f (n • x) = n • f x) →
                                            (∀ (n : ℤ) (x : R), f (n • x) = n • f x) →
                                              (∀ (n : ℕ), f ↑n = ↑n) → (∀ (n : ℤ), f ↑n = ↑n) → NonAssocCommRing S
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValueD_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] {f : α → β → γ} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α} {fallback : γ},
      Std.Internal.List.getKey? k l = some k' →
        Std.Internal.List.getValueD k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) fallback =
          (Option.map (f k') (Std.Internal.List.getValue? k l)).getD fallback
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- **Alias** of the forward direction of `SimpleGraph.neighborFinset_eq_empty`. -/
SimpleGraph.IsIsolated.of_neighborFinset_eq_empty : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)],
  G.neighborFinset v = ∅ → G.IsIsolated v
-- Mathlib.Dynamics.BirkhoffSum.NormedSpace
/-- The Birkhoff averages of a function `g` over the orbit of a fixed point `x` of `f`
tend to `g x` as `N → ∞`. In fact, they are equal to `g x` for all `N ≠ 0`,
see `Function.IsFixedPt.birkhoffAverage_eq`.

TODO: add a version for a periodic orbit.  -/
Function.IsFixedPt.tendsto_birkhoffAverage : ∀ {α : Type u_1} {E : Type u_2} (R : Type u_3) [inst : DivisionSemiring R] [CharZero R] [inst_2 : AddCommMonoid E]
  [inst_3 : TopologicalSpace E] [inst_4 : Module R E] {f : α → α} {x : α},
  Function.IsFixedPt f x →
    ∀ (g : α → E), Filter.Tendsto (fun x_1 => birkhoffAverage R f g x_1 x) Filter.atTop (nhds (g x))
-- Mathlib.GroupTheory.CoprodI
/-- A `NeWord M i j` is a representation of a non-empty reduced words where the first letter comes
from `M i` and the last letter comes from `M j`. It can be constructed from singletons and via
concatenation, and thus provides a useful induction principle.  -/
Monoid.CoprodI.NeWord : {ι : Type u_1} → (M : ι → Type u_2) → [(i : ι) → Monoid (M i)] → ι → ι → Type (max u_1 u_2)
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.mk : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → IsOpenMap f → Function.Bijective f → IsHomeomorph f
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.instPartialOrder : {E : Type u_3} → [inst : Group E] → PartialOrder (GroupNorm E)
-- Lean.Widget.UserWidget
Lean.Widget.GetWidgetsResponse.mk : Array Lean.Widget.PanelWidgetInstance → Lean.Widget.GetWidgetsResponse
-- Mathlib.Data.Finset.Empty
Finset.not_ssubset_empty : ∀ {α : Type u_1} (s : Finset α), ¬s ⊂ ∅
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDeclExtState.mk : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey) →
  Lean.PHashMap Lean.Name (Array Lean.Meta.SimpTheoremKey) → Lean.Meta.Simp.SimprocDeclExtState
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mk_cancel : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : ↥S) (m : M), LocalizedModule.mk (s • m) s = LocalizedModule.mk m 1
-- Batteries.Data.List.Lemmas
List.get_finRange : ∀ {n : ℕ} (i : Fin (List.finRange n).length), (List.finRange n).get i = Fin.cast ⋯ i
-- Mathlib.Order.Filter.Map
/-- **Alias** of the reverse direction of `Filter.filter_injOn_Iic_iff_injOn`. -/
Set.InjOn.filter_map_Iic : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {m : α → β},
  Set.InjOn m s → Set.InjOn (Filter.map m) (Set.Iic (Filter.principal s))
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.measurable_llr : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), Measurable (MeasureTheory.llr μ ν)
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- In a second countable complete metric space, a set of probability measures with compact closure
is tight.  -/
MeasureTheory.isTightMeasureSet_of_isCompact_closure : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} [inst : PseudoMetricSpace 𝓧] [inst_1 : OpensMeasurableSpace 𝓧]
  [SecondCountableTopology 𝓧] {S : Set (MeasureTheory.ProbabilityMeasure 𝓧)} [CompleteSpace 𝓧],
  IsCompact (closure S) → MeasureTheory.IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.rnDeriv_ne_top : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
  ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ⊤
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.getInvFn : {m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Lean.MonadError m] →
      [Monad m] → [Lean.Meta.Sym.Arith.MonadCanon m] → [Lean.Meta.Grind.Arith.CommRing.MonadCommRing m] → m Lean.Expr
-- Mathlib.Data.Set.Operations
Set.rangeFactorization_injective : ∀ {α : Type u} {ι : Sort u_1} {f : ι → α}, Function.Injective (Set.rangeFactorization f) ↔ Function.Injective f
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.decidableMemAdd.eq_1 : ∀ {α : Type u_2} [inst : AddMonoid α] {s t : Set α} [inst_1 : Fintype α] [inst_2 : DecidableEq α]
  [inst_3 : DecidablePred fun x => x ∈ s] [inst_4 : DecidablePred fun x => x ∈ t] (x : α),
  Set.decidableMemAdd x = decidable_of_iff (∃ x_1 ∈ s, ∃ y ∈ t, x_1 + y = x) ⋯
-- Mathlib.Data.Finset.Sups
Finset.filter_infs_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] [inst_2 : DecidableLE α] (s t : Finset α) (a : α),
  {b ∈ s ⊼ t | a ≤ b} = {b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b}
-- Init.PropLemmas
exists_prop_congr : ∀ {p p' : Prop} {q q' : p → Prop}, (∀ (h : p), q h ↔ q' h) → ∀ (hp : p ↔ p'), Exists q ↔ ∃ (h : p'), q' ⋯
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.iUnion_ball_nat_succ : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), ⋃ n, Metric.ball x (↑n + 1) = Set.univ
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that a type has `MeasurableDiv` if `(c / ·)` and `(· / c)` are measurable functions.
For a typeclass assuming measurability of `uncurry (· / ·)` see `MeasurableDiv₂`.  -/
MeasurableDiv : (G₀ : Type u_2) → [MeasurableSpace G₀] → [Div G₀] → Prop
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Pos.Raw.utf8GetAux.match_1.eq_2 : ∀ (motive : List Char → String.Pos.Raw → String.Pos.Raw → Sort u_1) (c : Char) (cs : List Char) (i p : String.Pos.Raw)
  (h_1 : (x x_1 : String.Pos.Raw) → motive [] x x_1)
  (h_2 : (c : Char) → (cs : List Char) → (i p : String.Pos.Raw) → motive (c :: cs) i p),
  (match c :: cs, i, p with
    | [], x, x_1 => h_1 x x_1
    | c :: cs, i, p => h_2 c cs i p) =
    h_2 c cs i p
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.singleton.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X}, CategoryTheory.Presieve.singleton f f
-- Mathlib.RingTheory.RingHom.FiniteType
RingHom.finiteType_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.FiniteType
-- Mathlib.Algebra.Lie.SkewAdjoint
Matrix.isSkewAdjoint_bracket : ∀ {R : Type u} {n : Type w} [inst : CommRing R] [inst_1 : Fintype n] (J : Matrix n n R) [inst_2 : DecidableEq n]
  {A B : Matrix n n R},
  A ∈ skewAdjointMatricesSubmodule J → B ∈ skewAdjointMatricesSubmodule J → ⁅A, B⁆ ∈ skewAdjointMatricesSubmodule J
-- Mathlib.Topology.Category.Compactum
Compactum.instCompactSpaceA : ∀ {X : Compactum}, CompactSpace X.A
-- Mathlib.Topology.ContinuousOn
/-- See also `ContinuousOn.comp'` using the form `fun y ↦ g (f y)` instead of `g ∘ f`.  -/
ContinuousOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {s : Set α} {g : β → γ} {t : Set β},
  ContinuousOn g t → ContinuousOn f s → Set.MapsTo f s t → ContinuousOn (g ∘ f) s
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.conjugate_eq : ∀ {p q : NNReal}, p.HolderConjugate q → q = p / (p - 1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.distinct_keys_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) t.toList
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOverIsoToOverUnit_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C),
  (CategoryTheory.toOverIsoToOverUnit.inv.app X).left =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.equivToOverUnit C).counit.app X)
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- If `X ← Z → Y` is a pullback diagram over `X ⨿ Y`, `Z` is initial.  -/
CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] →
        [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y] →
          (s : CategoryTheory.Limits.PullbackCone CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr) →
            CategoryTheory.Limits.IsLimit s → CategoryTheory.Limits.IsInitial s.pt
-- Init.Data.BitVec.Basic
BitVec.instInhabited : {n : ℕ} → Inhabited (BitVec n)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mem_sSup : ∀ {α : Type u_2} [inst : TopologicalSpace α] {Us : Set (TopologicalSpace.Opens α)} {x : α},
  x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u
-- Lean.Data.AssocList
Lean.AssocList.mapKey : {α : Type u} → {β : Type v} → {δ : Type w} → (α → δ) → Lean.AssocList α β → Lean.AssocList δ β
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.keysArray_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {f : α → Bool},
  t.WF → (Std.DTreeMap.Raw.filter (fun k x => f k) t).keysArray = Array.filter f t.keysArray
-- Mathlib.ModelTheory.Syntax
/-- Applies a binary relation to two terms as a bounded formula.  -/
FirstOrder.Language.Relations.boundedFormula₂ : {L : FirstOrder.Language} →
  {α : Type u'} → {n : ℕ} → L.Relations 2 → L.Term (α ⊕ Fin n) → L.Term (α ⊕ Fin n) → L.BoundedFormula α n
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `tendsto_finsetProd`. -/
tendsto_finset_prod : ∀ {ι : Type u_1} {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : CommMonoid M] [ContinuousMul M]
  {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι),
  (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun b => ∏ c ∈ s, f c b) x (nhds (∏ c ∈ s, a c))
-- Lean.Meta.Tactic.Grind.MatchCond
/-- Propagates `MatchCond` upwards  -/
Lean.Meta.Grind.propagateMatchCondUp : Lean.Meta.Grind.Propagator
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
/-- The forgetful functor from a concrete category to the category of types.  -/
CategoryTheory.forget : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : outParam (C → C → Type u_2)} →
      {CC : outParam (C → Type w)} →
        [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] →
          [CategoryTheory.ConcreteCategory C FC] → CategoryTheory.Functor C (Type w)
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Equivalence.commShift_of_inverse : ∀ {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] (E : C ≌ D) (A : Type u_3) [inst_2 : AddGroup A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : E.inverse.CommShift A],
  E.CommShift A
-- Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
WithTop.measurable_coe : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  [inst_3 : MeasurableSpace ι] [BorelSpace ι], Measurable fun x => ↑x
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_erase_of_comm : ∀ {M : Type u_4} [inst : Monoid M] {l : List M} {a : M} [inst_1 : DecidableEq M],
  a ∈ l → (∀ x ∈ l, ∀ y ∈ l, x * y = y * x) → a * (l.erase a).prod = l.prod
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_def_gt : ∀ {n : ℕ} {i j : Fin n}, i < j → j.cycleIcc i = 1
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedAddGroup.toContinuousENorm : {E : Type u_4} → [inst : SeminormedAddGroup E] → ContinuousENorm E
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.mapSubgroup_symm_apply : ∀ {G : Type u_1} [inst : Group G] {H : Type u_6} [inst_1 : Group H] (f : G ≃* H) (H_1 : Subgroup H),
  (RelIso.symm f.mapSubgroup) H_1 = Subgroup.map (↑f.symm) H_1
-- Mathlib.Algebra.Lie.InvariantForm
LieAlgebra.InvariantForm.mem_orthogonal : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (Φ : LinearMap.BilinForm R M)
  (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (N : LieSubmodule R L M) (y : M),
  y ∈ LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv N ↔ ∀ x ∈ N, (Φ x) y = 0