mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_eq_zero`. -/
SkewMonoidAlgebra.toFinsupp_eq_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a : SkewMonoidAlgebra k G}, a.coeff = 0 ↔ a = 0
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.ne_zero_of_order_ne_zero : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F}, p.order ≠ 0 → p ≠ 0
-- Mathlib.Analysis.Normed.Order.UpperLower
lowerClosure_interior_subset : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] (s : Set α),
  ↑(lowerClosure (interior s)) ⊆ interior ↑(lowerClosure s)
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Explain what we found out about the recursive calls (non-mutual case)  -/
Lean.Elab.WF.GuessLex.explainNonMutualFailure : Array Lean.Elab.WF.GuessLex.BasicMeasure → Array Lean.Elab.WF.GuessLex.RecCallCache → Lean.MetaM Std.Format
-- Mathlib.Order.OrderDual
Equiv.compl_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : Compl β] (a : α), aᶜ = e.symm (e a)ᶜ
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.coe_trans : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃] [inst_11 : AddTorsor V₃ P₃]
  [inst_12 : TopologicalSpace P₃] (e : P₁ ≃ᴬ[k] P₂) (e' : P₂ ≃ᴬ[k] P₃), ⇑(e.trans e') = ⇑e' ∘ ⇑e
-- Mathlib.Algebra.Category.MonCat.Shrink
MonCat.shrinkFunctorMap_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C MonCat} (τ : F ⟶ G)
  [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)] [inst_2 : ∀ (X : C), Small.{w, w'} ↑(G.obj X)] (X : C),
  (MonCat.shrinkFunctorMap τ).app X =
    MonCat.ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (MonCat.Hom.hom (τ.app X))).comp Shrink.mulEquiv.toMonoidHom)
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivWithinAt.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {f' g' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt g g' s x → HasFDerivWithinAt (f - g) (f' - g') s x
-- Mathlib.Analysis.Convolution
MeasureTheory.posConvolution.eq_1 : ∀ {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E']
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ E'] [inst_5 : NormedSpace ℝ F]
  (f : ℝ → E) (g : ℝ → E') (L : E →L[ℝ] E' →L[ℝ] F) (ν : MeasureTheory.Measure ℝ),
  MeasureTheory.posConvolution f g L ν = (Set.Ioi 0).indicator fun x => ∫ (t : ℝ) in 0..x, (L (f t)) (g (x - t)) ∂ν
-- Mathlib.Order.GaloisConnection.Basic
WithBot.giUnbotDBot.eq_1 : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α],
  WithBot.giUnbotDBot = { choice := fun o x => WithBot.unbotD ⊥ o, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
-- Std.Sync.Broadcast
Std.instMonadLiftBroadcastIO : MonadLift (EIO Std.Broadcast.Error) IO
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- **Alias** of `Submodule.isSymmetric_projection_iff`.

---

A linear projection onto `U` along its complement `V` is symmetric if
and only if `U` and `V` are pairwise orthogonal.  -/
Submodule.IsCompl.projection_isSymmetric_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} (hUV : IsCompl U V), (U.projection V hUV).IsSymmetric ↔ U ⟂ V
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.whiskerRight_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Adj B} {f g : a ⟶ b} (x : f ⟶ g)
  (β : b ⟶ c), (CategoryTheory.Bicategory.whiskerRight x β).τr = CategoryTheory.Bicategory.whiskerLeft β.r x.τr
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.coe_toLinearEquiv : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂),
  ⇑f.toLinearEquiv = ⇑f
-- Mathlib.Algebra.Ring.GeomSum
geom_sum₂_with_one : ∀ {R : Type u_1} [inst : Semiring R] (x : R) (n : ℕ),
  ∑ i ∈ Finset.range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i ∈ Finset.range n, x ^ i
-- Mathlib.Data.Set.Function
Set.injOn_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {B : Set (Set β)}, B ⊆ 𝒫 Set.range f → Set.InjOn (Set.preimage f) B
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] (f : α →Co β), (ContinuousOrderHom.id β).comp f = f
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.triangle_aux₁ : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.LocalizedMonoidal L W ε} (i₁ : X₁ ≅ Y₁) (i₂ : X₂ ≅ Y₂) (i₃ : X₃ ≅ Y₃),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom i₁.hom i₂.hom)
        i₃.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom
        (CategoryTheory.MonoidalCategoryStruct.tensorHom i₁.inv
          (CategoryTheory.MonoidalCategoryStruct.tensorHom i₂.inv i₃.inv))) =
    (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.exists_affineBasis : ∀ (k : Type u_5) (V : Type u_6) (P : Type u_7) [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : DivisionRing k] [inst_3 : Module k V], ∃ s b, ⇑b = Subtype.val
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.decidableLE : {d : ℕ} → DecidableLE (ℤ√↑d)
-- Mathlib.Algebra.Order.Ring.Basic
add_pow_le : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a b : R} [ExistsAddOfLE R],
  0 ≤ a → 0 ≤ b → ∀ (n : ℕ), (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.goto.sizeOf_spec : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : SizeOf Γ] [inst_1 : SizeOf Λ] [inst_2 : SizeOf σ]
  (a : Γ → σ → Λ), sizeOf (Turing.TM1.Stmt.goto a) = 1
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.coe_injective' : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K} [Fact (Irreducible f)], Function.Injective ⇑(AdjoinRoot.of f)
-- Mathlib.NumberTheory.RamificationInertia.Basic
_private.Mathlib.NumberTheory.RamificationInertia.Basic.0.Ideal.termE : Lean.ParserDescr
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instFG : ∀ (K : Type u_1) [inst : Field K] [NumberField K], AddGroup.FG (NumberField.RingOfIntegers K)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- This can't be `@[simp]`, because it would cause the more useful
`Matroid.ofIndepFinset_apply` not to be in simp normal form.  -/
IndepMatroid.ofFinset_indep' : ∀ {α : Type u_1} [inst : DecidableEq α] (E : Set α) (Indep : Finset α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E) {I : Set α},
  (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep I ↔
    ∀ (J : Finset α), ↑J ⊆ I → Indep J
-- Std.Tactic.Do.Syntax
/-- `mspecialize` is like `specialize`, but operating on a stateful `Std.Do.SPred` goal.
It specializes a hypothesis from the stateful context with hypotheses from either the pure
or stateful context or pure terms.
```lean
example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mspecialize HPQ HP
  mexact HPQ

example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
  mintro HQ HΨ
  mspecialize HΨ (y + 1) hP HQ
  mexact HΨ
```
 -/
Lean.Parser.Tactic.mspecializeError : Lean.ParserDescr
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.pairwise_toList_upwardEnumerableLt : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α], List.Pairwise (fun a b => Std.PRange.UpwardEnumerable.LT a b) r.toList
-- Lean.Data.FuzzyMatching
/-- Match the given pattern with the given word using a fuzzy matching
algorithm. The resulting scores are in the interval `[0, 1]` or `none` if no
match was found.  -/
Lean.FuzzyMatching.fuzzyMatchScore? : String → String → Option Float
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.mem_prime_of_mul_mem_pow : ∀ {S : Type u_1} [inst : CommRing S] [IsDedekindDomain S] {P : Ideal S} [P_prime : P.IsPrime],
  P ≠ ⊥ → ∀ {i : ℕ} {a b : S}, a ∉ P ^ (i + 1) → a * b ∈ P ^ (i + 1) → b ∈ P
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.SupportsStmt.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (S : Finset Λ) (k : K) (a : σ → Γ k)
  (q : Turing.TM2.Stmt Γ Λ σ), Turing.TM2.SupportsStmt S (Turing.TM2.Stmt.push k a q) = Turing.TM2.SupportsStmt S q
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → γ a}, (Std.ExtDTreeMap.map f t).size = t.size
-- Lean.InternalExceptionId
Lean.instInhabitedInternalExceptionId : Inhabited Lean.InternalExceptionId
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.inr_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N], Function.Injective ⇑AddMonoid.Coprod.inr
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Given maps `f`, `g` from a manifold into a field `𝕜` and `𝕜`-vector space `V`, respectively, the
formula for the `mfderiv` (differential) of their scalar multiplication `f • g`.

Mathematically speaking the formula is `d(f • g) = f • dg + df ⊗ g`, i.e.
`mfderiv% (f • g) x = f x • mfderiv% g x + toSpanSingleton 𝕜 (g x) ∘L mfderiv% f x`,
but this doesn't typecheck because `mfderiv% (f • g) x` and `mfderiv% g x` take values in different
tangent spaces -- respectively the tangent spaces to `V` at `(f • g) x` and `g x`. Of course, both
these tangent spaces can be canonically identified with `V`.

This lemma phrases the formula using the equiv `NormedSpace.fromTangentSpace`, which provides this
canonical identification. (It would also be possible to phrase the formula without this equiv,
instead using casting and definitional abuse.)

It is good practice to use the equiv `NormedSpace.fromTangentSpace` throughout a computation. If
this is done, typically `mfderiv% (f • g) x` will only turn up paired with this equiv (i.e., in an
expression `(fromTangentSpace _) ∘L mfderiv% (f • g) x`), and the more convenient lemma
`fromTangentSpace_mfderiv_smul` (see below) can be used instead.  -/
_private.Mathlib.Geometry.Manifold.MFDeriv.NormedSpace.0.mfderiv_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {V : Type u_18} [inst_6 : NormedAddCommGroup V]
  [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V},
  MDiffAt f x →
    MDiffAt g x →
      mfderiv% (f • g) x =
        f x •
            ↑(NormedSpace.fromTangentSpace ((f • g) x)).symm ∘SL
              ↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv% g x +
          ContinuousLinearMap.toSpanSingleton 𝕜 ((NormedSpace.fromTangentSpace ((f • g) x)).symm (g x)) ∘SL
            ↑(NormedSpace.fromTangentSpace (f x)) ∘SL mfderiv% f x
-- Mathlib.Topology.Sheaves.Sheafify
TopCat.Presheaf.stalkToFiber_surjective : ∀ {X : TopCat} (F : TopCat.Presheaf (Type v) X) (x : ↑X),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.stalkToFiber x))
-- Init.Data.List.Range
List.length_zipIdx : ∀ {α : Type u_1} {l : List α} {i : ℕ}, (l.zipIdx i).length = l.length
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.singleContinuousAddMonoidHom_apply : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α]
  [inst_2 : Fact (1 ≤ p)] (i : α) (x : E i), (lp.singleContinuousAddMonoidHom E p i) x = lp.single p i x
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.extend_comp_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (f₁ : MeasureTheory.SimpleFunc α γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : MeasureTheory.SimpleFunc β γ),
  (f₁.extend g hg f₂).comp g ⋯ = f₁
-- Mathlib.Data.Finset.Slice
/-- `Sized r A` means that every Finset in `A` has size `r`.  -/
Set.Sized : {α : Type u_1} → ℕ → Set (Finset α) → Prop
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.ofBijective_apply : ∀ {F : Type u_1} {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F)
  (hf : Function.Bijective ⇑f) (x : R), (RingEquiv.ofBijective f hf) x = f x
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.exists_lt_of_expect_lt_expect : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : Module ℚ≥0 α] [PosSMulMono ℚ≥0 α] {s : Finset ι} {f g : ι → α},
  ((s.expect fun i => g i) < s.expect fun i => f i) → ∃ x ∈ s, g x < f x
-- Mathlib.Order.Filter.Bases.Basic
Filter.disjoint_principal_left : ∀ {α : Type u_1} {f : Filter α} {s : Set α}, Disjoint (Filter.principal s) f ↔ sᶜ ∈ f
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.add_apply : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {D1 D2 : LieDerivation R L M} (a : L), (D1 + D2) a = D1 a + D2 a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.oset : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    ℕ →
      Lean.Compiler.LCNF.Arg pu →
        autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_3 →
          Lean.Compiler.LCNF.CodeDecl pu
-- Mathlib.Order.SuccPred.Basic
Order.isMax_iterate_succ_of_eq_of_lt : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α} {n m : ℕ},
  Order.succ^[n] a = Order.succ^[m] a → n < m → IsMax (Order.succ^[n] a)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.ev_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} (f : I ⟶ J)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f]
  {X Y : CategoryTheory.Over I} (g : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ChosenPullbacksAlong.pullback f).map
        ((CategoryTheory.ExponentiableMorphism.pushforward f).map g))
      ((CategoryTheory.ExponentiableMorphism.ev f).app Y) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ExponentiableMorphism.ev f).app X) g
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffAt_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G]
  {a b : G}, ContMDiffAt I I n (fun x => a + x) b
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioo_cast : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n),
  ∏ i ∈ Finset.Ioo (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Finset.Ioo a b, f (Fin.cast h i)
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_le_self' : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : One M] {s : Set α} {f : α → M},
  (∀ x ∉ s, 1 ≤ f x) → s.mulIndicator f ≤ f
-- Mathlib.Algebra.Ring.Defs
/-- A `Ring` which `IsMulCommutative` is a `CommRing`.

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.instCommRing : {R : Type v} → [inst : Ring R] → [IsMulCommutative R] → CommRing R
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X)
  (P : CategoryTheory.Functor Dᵒᵖ A),
  CategoryTheory.CategoryStruct.comp (P.map (F.map f).op) (Φ.toPresheafFiberMap F K P X x) =
    Φ.toPresheafFiberMap F K P Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.ofIsoI_e : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.MonoFactorisation f) {I' : C} (e : F.I ≅ I'),
  (F.ofIsoI e).e = CategoryTheory.CategoryStruct.comp F.e e.hom
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankLeOne.strictMono' : ∀ {R : Type u_1} {Γ₀ : Type u_2} {inst : Ring R} {inst_1 : LinearOrderedCommGroupWithZero Γ₀} {v : Valuation R Γ₀}
  [self : v.RankLeOne], StrictMono ⇑(Valuation.RankLeOne.hom' v)
-- Init.Data.Char.Basic
Char.isValidUInt32 : ∀ (n : ℕ), Char.isValidCharNat n → n < UInt32.size
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
fderiv_comp_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (c : 𝕜), fderiv 𝕜 (fun x => f (c • x)) x = c • fderiv 𝕜 f (c • x)
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.decidableMemMul : {α : Type u_2} →
  [inst : Monoid α] →
    {s t : Set α} →
      [Fintype α] →
        [DecidableEq α] →
          [DecidablePred fun x => x ∈ s] → [DecidablePred fun x => x ∈ t] → DecidablePred fun x => x ∈ s * t
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Std.Do.EStateM.instWP.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (e : ε) → (s' : σ) → motive (EStateM.Result.error e s')),
  (match EStateM.Result.ok a s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error e s' => h_2 e s') =
    h_1 a s'
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_eq_top_iff : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [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₂}
  {p : Submodule R M} [inst_6 : RingHomSurjective σ₁₂] {σ₂₁ : R₂ →+* R} [inst_7 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_8 : RingHomInvPair σ₂₁ σ₁₂] {e : M ≃ₛₗ[σ₁₂] M₂}, Submodule.map (↑e) p = ⊤ ↔ p = ⊤
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_unitGroup_iff : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : Kˣ), x ∈ A.unitGroup ↔ A.valuation ↑x = 1
-- Mathlib.Geometry.Manifold.Immersion
IsOpen.isImmersionAtOfComplement : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  IsOpen {x | Manifold.IsImmersionAtOfComplement F I J n f x}
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.nontrivial_iff_ne_bot : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), Nontrivial ↥H ↔ H ≠ ⊥
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.strictLimitsClosureStep_strictLimitsClosureIter_eq_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] (κ : Cardinal.{w}) [Fact κ.IsRegular],
  (∀ (a : α), HasCardinalLT (J a) κ) →
    (P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J = P.strictLimitsClosureIter J κ.ord
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Deficient.pos : ∀ {n : ℕ}, n.Deficient → 0 < n
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Unicode symbols in mathlib that should always be followed by the emoji variant selector.  -/
Mathlib.Linter.TextBased.UnicodeLinter.emojis : Array Char
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.add_measure_right : ∀ {α : Type u_1} {β : Type u_7} [inst : SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {x : MeasurableSpace α}
  (μ ν : MeasureTheory.Measure α),
  MeasureTheory.DominatedFinMeasAdditive μ T C → 0 ≤ C → MeasureTheory.DominatedFinMeasAdditive (μ + ν) T C
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
EReal.measurable_exp : Measurable EReal.exp
-- Std.Time.Notation
/-- Defines a syntax for UTC offset values. The string should indicate the time difference from UTC
(e.g., "-03:00").

Example:
`offset("-03:00")`
 -/
Std.Time.«termOffset(_)» : Lean.ParserDescr
-- Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.LintVerbosity.ofNat : ℕ → Batteries.Tactic.Lint.LintVerbosity
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_mul_sym : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Add α] [inst_2 : One α] [inst_3 : OfNat α 2] [inst_4 : Invertible 2]
  (a b : α), SymAlg.sym a * SymAlg.sym b = SymAlg.sym (⅟2 * (a * b + b * a))
-- Mathlib.RingTheory.Perfection
PerfectionMap.comp_equiv : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {P : Type u₃}
  [inst_3 : CommSemiring P] [inst_4 : CharP P p] [inst_5 : PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π)
  (x : P), (Perfection.coeff R p 0) (m.equiv x) = π x