mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Defs
/-- A `NonAssocSemiring` which `IsMulCommutative` is a `NonAssocCommSemiring`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsMulCommutative.instNonAssocCommSemiring : {R : Type v} → [inst : NonAssocSemiring R] → [IsMulCommutative R] → NonAssocCommSemiring R
-- Mathlib.Algebra.Order.SuccPred.TypeTags
instPredOrderMultiplicative : {X : Type u_1} → [inst : Preorder X] → [h : PredOrder X] → PredOrder (Multiplicative X)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure
/-- The pointwise bound `‖s i‖ₑ ≤ s.totalVariation i` for any signed measure.  -/
MeasureTheory.SignedMeasure.enorm_le_totalVariation : ∀ {X : Type u_1} {mX : MeasurableSpace X} (s : MeasureTheory.SignedMeasure X) (i : Set X), ‖s i‖ₑ ≤ s.totalVariation i
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with scalar multiplication.  -/
InnerProductSpace.laplacian_smul_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra ℝ 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : InnerProductSpace ℝ E] [inst_4 : FiniteDimensional ℝ E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] [IsScalarTower ℝ 𝕜 F]
  {f : E → F} {x : E} (v : 𝕜), ContDiffAt ℝ 2 f x → Laplacian.laplacian (v • f) =ᶠ[nhds x] v • Laplacian.laplacian f
-- Mathlib.Analysis.Analytic.Uniqueness
HasFPowerSeriesAt.eq_formalMultilinearSeries_of_eventually : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p q : FormalMultilinearSeries 𝕜 𝕜 E} {f g : 𝕜 → E} {x : 𝕜},
  HasFPowerSeriesAt f p x → HasFPowerSeriesAt g q x → (∀ᶠ (z : 𝕜) in nhds x, f z = g z) → p = q
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.TotallyBounded.exists_subset_of_mem : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α},
  f.TotallyBounded → ∀ {s : Set α}, s ∈ f → ∀ {U : SetRel α α}, U ∈ uniformity α → ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → ∀ {h : k' ∈ m.insertMany l}, (m.insertMany l).getKey k' h = k
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyLT! : {α : Type u} → {β : α → Type v} → [Ord α] → [Inhabited α] → α → Std.DTreeMap.Internal.Impl α β → α
-- Init.Control.Lawful.Instances
StateT.run_bind : ∀ {m : Type u_1 → Type u_2} {σ α β : Type u_1} [inst : Monad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ),
  (x >>= f).run s = do
    let p ← x.run s
    (f p.1).run p.2
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The pointwise distance between any two integral curves `α` and `β` over their domains is bounded
by a constant `L'` times the distance between their respective initial points. This is the result of
taking the limit of `dist_iterate_iterate_next_le_of_lipschitzWith` as `n → ∞`. This implies that
the local solution of a vector field is Lipschitz continuous in the initial condition.  -/
ODE.FunSpace.exists_forall_closedBall_funSpace_dist_le_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} [CompleteSpace E] (hf : IsPicardLindelof f t₀ x₀ a r L K),
  ∃ L',
    ∀ (x y : E) (hx : x ∈ Metric.closedBall x₀ ↑r) (hy : y ∈ Metric.closedBall x₀ ↑r) (α β : ODE.FunSpace t₀ x₀ r L),
      Function.IsFixedPt (ODE.FunSpace.next hf hx) α →
        Function.IsFixedPt (ODE.FunSpace.next hf hy) β → dist α β ≤ ↑L' * dist x y
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
/-- Given a functor `F : C ⥤ 𝒳` such that `F ⋙ p` is constant at some `S : 𝒮`, then
we get an induced functor `C ⥤ Fiber p S` that `F` factors through.  -/
CategoryTheory.Functor.Fiber.inducedFunctor : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          {S : 𝒮} →
            {C : Type u₃} →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                {F : CategoryTheory.Functor C 𝒳} →
                  F.comp p = (CategoryTheory.Functor.const C).obj S → CategoryTheory.Functor C (p.Fiber S)
-- Mathlib.Data.Int.SuccPred
Int.instPredSubOrder : PredSubOrder ℤ
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a seminormed group from a translation-invariant pseudodistance.  -/
SeminormedAddCommGroup.ofAddDist' : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : AddCommGroup E] →
      [inst_2 : PseudoMetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 0 x) → (∀ (x y z : E), dist (z + x) (z + y) ≤ dist x y) → SeminormedAddCommGroup E
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The unoriented angle at `p` between two points not equal to `p` is zero if and only if the
unoriented angle is zero.  -/
EuclideanGeometry.oangle_eq_zero_iff_angle_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ : P}, p₁ ≠ p → p₂ ≠ p → (EuclideanGeometry.oangle p₁ p p₂ = 0 ↔ EuclideanGeometry.angle p₁ p p₂ = 0)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- `stratum` and `FiniteArchimedeanClass.ball`
are codisjoint under `FiniteArchimedeanClass.closedBall`.  -/
HahnEmbedding.ArchimedeanStrata.ball_sup_stratum_eq : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] (self : HahnEmbedding.ArchimedeanStrata K M)
  (c : FiniteArchimedeanClass M),
  FiniteArchimedeanClass.ball K c ⊔ self.stratum c = FiniteArchimedeanClass.closedBall K c
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
one_le_pow_iff : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftMono M] {x : M} {n : ℕ}, n ≠ 0 → (1 ≤ x ^ n ↔ 1 ≤ x)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.memLp_enorm_rpow_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_6}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {q : ENNReal} {f : α → ε},
  MeasureTheory.AEStronglyMeasurable f μ →
    q ≠ 0 → q ≠ ⊤ → (MeasureTheory.MemLp (fun x => ‖f x‖ₑ ^ q.toReal) (p / q) μ ↔ MeasureTheory.MemLp f p μ)
-- Mathlib.Algebra.Algebra.Tower
IsScalarTower.of_algebraMap_smul : ∀ {R : Type u} {A : Type w} {M : Type v₁} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : MulAction A M] [inst_4 : SMul R M],
  (∀ (r : R) (x : M), (algebraMap R A) r • x = r • x) → IsScalarTower R A M
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_erase_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t.erase k).size ≤ t.size
-- Init.GrindInstances.Ring.Rat
Lean.Grind.instNoNatZeroDivisorsRat : Lean.Grind.NoNatZeroDivisors ℚ
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.IsDedekindDomain.ramificationIdx'_ne_zero`. -/
Ideal.IsDedekindDomain.ramificationIdx_ne_zero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  [IsDedekindDomain S],
  Ideal.map (algebraMap R S) p ≠ ⊥ → P.IsPrime → Ideal.map (algebraMap R S) p ≤ P → p.ramificationIdx' P ≠ 0
-- Mathlib.Tactic.Says
/-- `tac₁ says tac₂` runs `tac₂`. In CI it also runs `tac₁` and validates that `tac₁` produces
a "Try this: `tac₂`" message. Use `set_option says.verify true` to enable the validation step on
your own machine.

The `says` combinator is intended to be used when `tac₁` is meaningful but slow and `tac₂` is faster
but hard to read: for example, `simp? [X] says simp only [X, Y, Z]`.

To generate or update the correct value of `tac₂`, write `tac₁ says`. You will get a message
"Try this: `tac₁ says tac₂`.
 -/
Mathlib.Tactic.Says.says : Lean.TrailingParserDescr
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_mul : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (e e' : P ≃ᵃⁱ[𝕜] P),
  ⇑(e * e') = ⇑e ∘ ⇑e'
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_add_QInfty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C},
  AlgebraicTopology.DoldKan.PInfty + AlgebraicTopology.DoldKan.QInfty =
    CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X)
-- Mathlib.Computability.TuringMachine.Tape
Turing.PointedMap.mk_val : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Γ → Γ') (pt : f default = default),
  { f := f, map_pt' := pt }.f = f
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.addConjMap_ofFixingAddSubgroup_bijective : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} {g : M} {hst : g +ᵥ s = t},
  Function.Bijective ⇑(SubAddAction.addConjMap_ofFixingAddSubgroup hst)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_rpow : ∀ {b x : ℝ}, 0 < b → b ≠ 1 → Real.logb b (b ^ x) = x
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tsum_nat_add_neg : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : ℤ → M},
  Summable f → ∑' (n : ℕ), (f ↑n + f (-↑n)) = ∑' (n : ℤ), f n + f 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.diff m₂).getKey? k = if m₂.contains k = true then none else m₁.getKey? k
-- Mathlib.Order.SymmDiff
IsCompl.bihimp_eq_bot : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, IsCompl a b → bihimp a b = ⊥
-- Mathlib.FieldTheory.Finite.GaloisField
/-- Any finite field is (possibly noncanonically) isomorphic to some Galois field.  -/
GaloisField.algEquivGaloisField : (p : ℕ) →
  [h_prime : Fact (Nat.Prime p)] →
    (n : ℕ) →
      {K : Type u_1} →
        [inst : Field K] → [inst_1 : Algebra (ZMod p) K] → Nat.card K = p ^ n → K ≃ₐ[ZMod p] GaloisField p n
-- Mathlib.LinearAlgebra.Projectivization.Cardinality
/-- `ℙ k V` is equivalent to the quotient of the non-zero elements of `V` by `kˣ`.  -/
Projectivization.equivQuotientOrbitRel : (k : Type u_1) →
  (V : Type u_2) →
    [inst : DivisionRing k] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module k V] → Projectivization k V ≃ Quotient (MulAction.orbitRel kˣ { v // v ≠ 0 })
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.forgetPreservesLimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (D : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Sheaf J RingCat) [Small.{v, u₂} D],
  CategoryTheory.Limits.PreservesLimitsOfShape D (SheafOfModules.forget R)
-- Aesop.Script.Step
Aesop.Script.LazyStep.BuildInput.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (tac : Lean.MetaM α) (postGoals : α → Array Lean.MVarId)
  (tacticBuilder : α → Aesop.Script.TacticBuilder),
  sizeOf { tac := tac, postGoals := postGoals, tacticBuilder := tacticBuilder } = 1
-- Init.Data.List.Monadic
List.mapM.loop.eq_def : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m β) (x : List α) (x_1 : List β),
  List.mapM.loop f x x_1 =
    match x, x_1 with
    | [], bs => pure bs.reverse
    | a :: as, bs => do
      let __do_lift ← f a
      List.mapM.loop f as (__do_lift :: bs)
-- Mathlib.Topology.Path
Path.extend_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), γ.extend 0 = x
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_rio : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : Std.PRange.Least? α] [inst_3 : LT α] [inst_4 : DecidableLT α] [inst_5 : Std.PRange.UpwardEnumerable α]
  [inst_6 : Std.Rxo.IsAlwaysFinite α] [inst_7 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Rio α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.congr_apply : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (G' : Subgroup G) (H' : Subgroup H)
  [inst_2 : G'.Normal] [inst_3 : H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G),
  (QuotientGroup.congr G' H' e he) ↑x = (QuotientGroup.mk' H') (e x)
-- Batteries.Data.List.Basic
List.takeDTR_go_eq : ∀ {α : Type u_1} {dflt : α} {acc : Array α} (n : ℕ) (l : List α),
  List.takeDTR.go dflt n l acc = acc.toList ++ List.takeD n l dflt
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coe_comp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂),
  ⇑(h ∘SL f) = ⇑h ∘ ⇑f
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integral_sub : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f g : ↥(MeasureTheory.Lp E 1 μ)),
  MeasureTheory.L1.integral (f - g) = MeasureTheory.L1.integral f - MeasureTheory.L1.integral g
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapComp_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictlyUnitaryPseudofunctor B C)
  (G : CategoryTheory.StrictlyUnitaryPseudofunctor C D) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  ((F.comp G).mapComp f g).hom =
    CategoryTheory.CategoryStruct.comp (G.map₂ (F.mapComp f g).hom) (G.mapComp (F.map f) (F.map g)).hom
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.limit_ext_iff : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}}
  {x y : ↑(ProfiniteAddGrp.limit F).toProfinite.toTop}, x = y ↔ ∀ (j : J), ↑x j = ↑y j
-- Lean.Elab.Syntax
/-- Infer syntax kind `k` from first pattern, put alternatives of same kind into new `macro/elab_rules (kind := k)` via `mkCmd (some k)`,
leave remaining alternatives (via `mkCmd none`) to be recursively expanded.  -/
Lean.Elab.Command.expandNoKindMacroRulesAux : Array (Lean.TSyntax `Lean.Parser.Term.matchAlt) →
  String →
    (Option Lean.Name → Array (Lean.TSyntax `Lean.Parser.Term.matchAlt) → Lean.Elab.Command.CommandElabM Lean.Command) →
      Lean.Elab.Command.CommandElabM Lean.Command
-- Lean.Parser.Term
Lean.Parser.Term.mdataDiagnostic.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Nat.Bits
_private.Mathlib.Data.Nat.Bits.0.Nat.boddDiv2.match_1.eq_1 : ∀ (motive : Bool × ℕ → Sort u_1) (m : ℕ) (h_1 : (m : ℕ) → motive (false, m)) (h_2 : (m : ℕ) → motive (true, m)),
  (match (false, m) with
    | (false, m) => h_1 m
    | (true, m) => h_2 m) =
    h_1 m
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.supDegree_toLex_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : LinearOrder σ] (r : R),
  AddMonoidAlgebra.supDegree (⇑toLex) (MvPolynomial.C r) = 0
-- Lean.Meta.Reduce
_private.Lean.Meta.Reduce.0.Lean.Meta.reduce.visit : Bool → Bool → Bool → Lean.Expr → Lean.MonadCacheT Lean.Expr Lean.Expr Lean.MetaM Lean.Expr
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.nndist_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : PseudoMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X} {x y : X}, HolderOnWith C r f s → x ∈ s → y ∈ s → nndist (f x) (f y) ≤ C * nndist x y ^ ↑r
-- Mathlib.Order.ModularLattice
codisjoint_inf_right_of_codisjoint_inf_right : ∀ {α : Type u_1} {a b c : α} [inst : Lattice α] [inst_1 : OrderTop α] [IsModularLattice α],
  Codisjoint a (b ⊓ c) → Codisjoint b (c ⊓ a) → Codisjoint c (a ⊓ b)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.all_eq_false_iff_exists_contains_get : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {p : (a : α) → β a → Bool}, m.WF → (m.all p = false ↔ ∃ a, ∃ (h : m.contains a = true), p a (m.get a h) = false)
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
ArithmeticFunction.ofPowerSeries_apply_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {q : ℕ},
  1 < q → ∀ (f : PowerSeries R) (k : ℕ), ((ArithmeticFunction.ofPowerSeries q) f) (q ^ k) = (PowerSeries.coeff k) f
-- Mathlib.Logic.Basic
Or.elim3 : ∀ {a b c d : Prop}, a ∨ b ∨ c → (a → d) → (b → d) → (c → d) → d
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.addConstants_expansion : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] (α : Type u_1)
  [inst_1 : (FirstOrder.Language.constantsOn α).Structure M] {L' : FirstOrder.Language} [inst_2 : L'.Structure M]
  (φ : L →ᴸ L') [φ.IsExpansionOn M], (FirstOrder.Language.LHom.addConstants α φ).IsExpansionOn M
-- Init.Data.Vector.Lemmas
Vector.map_inj_right : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {xs ys : Vector α n} {f : α → β},
  (∀ (x y : α), f x = f y → x = y) → (Vector.map f xs = Vector.map f ys ↔ xs = ys)
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- The chosen end construction as a functor out of the bifunctor category.  -/
CategoryTheory.Limits.chosenEndFunctor : {J : Type u_3} →
  {C : Type u_4} →
    [inst : CategoryTheory.Category.{v_3, u_4} C] →
      [inst_1 : CategoryTheory.Category.{v_4, u_3} J] →
        [CategoryTheory.Limits.ChosenEndsOfShape J C] →
          CategoryTheory.Functor (CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) C
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomain_mul : ∀ {F : Type u_2} {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Add M] [inst_2 : Add N]
  [inst_3 : FunLike F M N] [AddHomClass F M N] (f : F) (x y : AddMonoidAlgebra R M),
  AddMonoidAlgebra.mapDomain (⇑f) (x * y) = AddMonoidAlgebra.mapDomain (⇑f) x * AddMonoidAlgebra.mapDomain (⇑f) y
-- Mathlib.Topology.MetricSpace.Closeds
/-- **Alias** of `Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt`. -/
EMetric.mem_hausdorffEntourage_of_hausdorffEdist_lt : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {s t : Set α} {δ : ENNReal},
  Metric.hausdorffEDist s t < δ → (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 < δ}
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.normalize_lcm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s : Multiset α),
  normalize s.lcm = s.lcm
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- When the subgroup `N < G` is not necessarily `Normal`, we have a `CosetSpace` as opposed
to `QuotientGroup` (the next `instance`).
TODO: typeclass inference should normally find this, but currently doesn't.
E.g., `MeasurableSMul G (G ⧸ Γ)` fails to synthesize, even though `G ⧸ Γ` is the quotient
of `G` by the action of `Γ`; it seems unable to pick up the `BorelSpace` instance.  -/
CosetSpace.borelSpace : ∀ {G : Type u_3} [inst : TopologicalSpace G] [PolishSpace G] [inst_2 : Group G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] {N : Subgroup G} [T2Space (G ⧸ N)] [SecondCountableTopology (G ⧸ N)], BorelSpace (G ⧸ N)
-- Plausible.Testable
/-- Add some formatting to the information recorded by `addInfo`.  -/
Plausible.TestResult.addVarInfo : {p q : Prop} →
  {γ : Type u_1} →
    [Repr γ] →
      String → γ → (q → p) → Plausible.TestResult p → optParam (Unit ⊕' (p → q)) (PSum.inl ()) → Plausible.TestResult q
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.IntFractPair.stream_nth_fr_num_le_fr_num_sub_n_rat : ∀ {q : ℚ} {n : ℕ} {ifp_n : GenContFract.IntFractPair ℚ},
  GenContFract.IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (GenContFract.IntFractPair.of q).fr.num - ↑n
-- Mathlib.Data.Finset.NAry
Finset.mem_image₂_of_mem : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {a : α} {b : β}, a ∈ s → b ∈ t → f a b ∈ Finset.image₂ f s t
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.of_eq_of_ne : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] (i j : ι) (x : β i),
  j ≠ i → ((DirectSum.of β i) x) j = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- Variant of `of_isLimit` for an arbitrary cone on a diagram `WalkingCospan ⥤ C`.  -/
CategoryTheory.IsPullback.of_isLimit_cone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  {D : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} {c : CategoryTheory.Limits.Cone D}
  (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.IsPullback (c.π.app CategoryTheory.Limits.WalkingCospan.left)
    (c.π.app CategoryTheory.Limits.WalkingCospan.right) (D.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
    (D.map CategoryTheory.Limits.WalkingCospan.Hom.inr)
-- Mathlib.Logic.Function.Basic
Function.Involutive.injective : ∀ {α : Sort u} {f : α → α}, Function.Involutive f → Function.Injective f
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.Sheaf.isLocallyBijective_iff_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F G : CategoryTheory.Sheaf J A} (f : F ⟶ G) [(CategoryTheory.forget A).ReflectsIsomorphisms]
  [J.HasSheafCompose (CategoryTheory.forget A)],
  CategoryTheory.Sheaf.IsLocallyInjective f ∧ CategoryTheory.Sheaf.IsLocallySurjective f ↔ CategoryTheory.IsIso f