mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Basic
Nat.le_of_not_ge : ∀ {a b : ℕ}, ¬a ≥ b → a ≤ b
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.sub : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] [SecondCountableTopology E]
  {Y : Ω → E}, ProbabilityTheory.HasGaussianLaw (fun ω => (X ω, Y ω)) P → ProbabilityTheory.HasGaussianLaw (X - Y) P
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)} {k : α},
  (m.insertMany l).contains k = (m.contains k || (List.map Sigma.fst l).contains k)
-- Std.Http.Data.URI.Basic
Std.Http.URI.Path.mk : Array Std.Http.URI.EncodedSegment → Bool → Std.Http.URI.Path
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceTMod : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Group.Units.Opposite
/-- The additive units of the additive opposites are equivalent to the additive opposites
of the additive units.  -/
AddUnits.opEquiv : {M : Type u_2} → [inst : AddMonoid M] → AddUnits Mᵃᵒᵖ ≃+ (AddUnits M)ᵃᵒᵖ
-- Lean.Server.FileWorker.RequestHandling
_private.Lean.Server.FileWorker.RequestHandling.0.Lean.Server.FileWorker.handleFoldingRange.isImport : Lean.Syntax → Bool
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Given a collinear set of points, and two distinct points `p₂` and `p₃` in it, a point `p₁` is
collinear with the set if and only if it is collinear with `p₂` and `p₃`.  -/
Collinear.collinear_insert_iff_of_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P},
  Collinear k s → ∀ {p₁ p₂ p₃ : P}, p₂ ∈ s → p₃ ∈ s → p₂ ≠ p₃ → (Collinear k (insert p₁ s) ↔ Collinear k {p₁, p₂, p₃})
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Removal.0.SimpleGraph.aux : ∀ {n k : ℕ}, 0 < k → k ≤ n → n < 2 * k * (n / k)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.mkOfLe_refl : ∀ {n : ℕ} (j : Fin (n + 1)), SimplexCategory.mkOfLe j j ⋯ = { len := 1 }.const { len := n } j
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.coe_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (S : Submonoid N) (f : F), ↑(Submonoid.comap f S) = ⇑f ⁻¹' ↑S
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.State.switch : Lean.Compiler.CSimp.State → Lean.Compiler.CSimp.State
-- Mathlib.Topology.EMetricSpace.Weak
Option.some_eball : ∀ {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] (a : α) (r : ENNReal),
  some '' Metric.eball a r = Metric.eball (some a) r
-- Mathlib.Data.Set.Insert
Set.disjoint_insert_left : ∀ {α : Type u_1} {s t : Set α} {a : α}, Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_iSup_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {ι : Type u_5} {f : M →ₙ* N},
  Function.Surjective ⇑f → ∀ (S : ι → Subsemigroup N), Subsemigroup.map f (⨆ i, Subsemigroup.comap f (S i)) = iSup S
-- Lean.Meta.GetUnfoldableConst
/-- As with `getUnfoldableConst?` but return `none` instead of failing if the constant is not found.
 -/
Lean.Meta.getUnfoldableConstNoEx? : Lean.Name → Lean.MetaM (Option Lean.ConstantInfo)
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.sum_tmul_tmul_eq : ∀ {R : Type u} {A : Type v} {ι : Type u_1} {κ : ι → Type u_2} {Λ : ι → Type u_3} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] [inst_3 : Coalgebra R A] {a : A} (repr : Coalgebra.Repr R a ι)
  (a₁ : (i : ι) → Coalgebra.Repr R (repr.left i) (κ i)) (a₂ : (i : ι) → Coalgebra.Repr R (repr.right i) (Λ i)),
  ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- A Type synonym for `A ⊗[R] B`, but with multiplication as `TensorProduct.gradedMul`.

This has notation `𝒜 ᵍ⊗[R] ℬ`.  -/
TensorProduct.«term_ᵍ⊗[_]_» : Lean.TrailingParserDescr
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.compAddMonoidHom'_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_3}
  [inst_2 : TopologicalSpace γ] [inst_3 : AddZeroClass γ] [inst_4 : ContinuousAdd γ] (g : C(α, β)) (f : C(β, γ)),
  g.compAddMonoidHom' f = f.comp g
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv_base_pow_mul : ∀ {p n : ℕ}, 1 < p → n ≠ 0 → ∀ (k : ℕ), p.maxPowDvdDiv (p ^ k * n) = (padicValNat p n + k, n.divMaxPow p)
-- Mathlib.Topology.Algebra.Ring.Compact
IsLocalRing.isOpen_maximalIdeal : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R]
  [inst_5 : IsLocalRing R] [IsNoetherianRing R], IsOpen ↑(IsLocalRing.maximalIdeal R)
-- Lean.DocString.Markdown
/-- The current code is inside strong emphasis (`**…**`).  -/
Lean.Doc.MarkdownM.InlineCtx.inBold : Lean.Doc.MarkdownM.InlineCtx → Bool
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.Nondegenerate.mk : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Finite m]
  [inst_2 : Finite n] {M : Matrix m n R}, M.SeparatingLeft → M.SeparatingRight → M.Nondegenerate
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- A morphism of `FiniteGrp` induces a morphism of the associated profinite groups.  -/
ProfiniteGrp.ofFiniteGrpHom : {G H : FiniteGrp.{u}} → (G ⟶ H) → (ProfiniteGrp.ofFiniteGrp G ⟶ ProfiniteGrp.ofFiniteGrp H)
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.IntermediateField.adjoin_X : ∀ {K : Type u_1} [inst : Field K] (E : IntermediateField K (RatFunc K)), (↥E)⟮RatFunc.X⟯ = ⊤
-- Std.Sat.AIG.RelabelNat
/-- Obtain the atom mapping from α to `Nat` for a given `AIG`.
 -/
Std.Sat.AIG.RelabelNat.State.ofAIG : {α : Type} → [inst : DecidableEq α] → [inst_1 : Hashable α] → Std.Sat.AIG α → Std.HashMap α ℕ
-- Lean.Elab.Command
/-- Snapshot after macro expansion of a command.  -/
Lean.Elab.Command.MacroExpandedSnapshot : Type
-- Mathlib.Data.NNReal.Defs
NNReal.coe_toRealHom : ⇑NNReal.toRealHom = NNReal.toReal
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofBijective_symm_apply_apply : ∀ {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₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [inst_4 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_5 : RingHomInvPair σ₂₁ σ₁₂] {h : Function.Bijective ⇑f} (x : M), (LinearEquiv.ofBijective f h).symm (f x) = x
-- Mathlib.NumberTheory.Padics.PadicNorm
padicNorm.sum_lt' : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {α : Type u_1} {F : α → ℚ} {t : ℚ} {s : Finset α},
  (∀ i ∈ s, padicNorm p (F i) < t) → 0 < t → padicNorm p (∑ i ∈ s, F i) < t
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C)
  (X_1 : CategoryTheory.WithInitial SimplexCategory),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.unitIso.hom.app X).app X_1 =
    (match X_1 with
      | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).hom
-- Mathlib.Tactic.FieldSimp
/-- `field` is a `simp` set that clears denominators in (semi-)field (in)equalities.

The `field` simp set is a variant of the `field_simp` tactic. The latter operates recursively on
subexpressions, bringing every field-expression encountered to the form `n / d`, and then attempts
to clear the denominator. (For confluence reasons, the `field` simprocs also have a slightly
different normal form from `field_simp`'s.)

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging
fails. These denominators are made out of denominators appearing in the input expression,
by repeatedly taking products or divisors. The discharger can be non-universal, i.e. can be specific
to the field at hand (order properties, explicit `≠ 0` hypotheses, `CharZero` if that is known,
etc). See `field_simp_discharge` for full details of the discharger algorithm.

* `simp [field, t₁, ..., tₙ]` provides terms `t₁`, ..., `tₙ` to the discharger for
  nonzeroness/positivity proofs.

Examples:
```
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
    (x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
  simp only [field]
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
```
 -/
fieldLt : Lean.Meta.Simp.Simproc
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
_private.Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone.0.NumberField.mixedEmbedding.fundamentalCone.idealSetMap.match_1.splitter : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) →
        (motive : ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J) → Sort u_2) →
          (x : ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J)) →
            ((a : NumberField.mixedEmbedding.mixedSpace K) →
                (ha : a ∈ NumberField.mixedEmbedding.fundamentalCone.idealSet K J) → motive ⟨a, ha⟩) →
              motive x
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- Let `𝔖` be a family of bounded subsets of `F`, and `B : E × F → G` a bilinear map.
If `B` is (jointly) continuous, then it is `𝔖`-**hypocontinuous**:
in curried form, it defines a continuous linear map `E →L[𝕜] (F →Lᵤ[𝕜, 𝔖] G)`.

Note that, in full generality, the converse is not true.
See also `ContinuousLinearMap.continuous_of_continuous_uncurry`.  -/
UniformConvergenceCLM.continuous_of_continuous_uncurry : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜₂ F] {𝕜₁ : Type u_6}
  [inst_5 : NontriviallyNormedField 𝕜₁] {σ : 𝕜₁ →+* 𝕜₂} [inst_6 : Module 𝕜₁ E] [inst_7 : AddCommGroup G] {𝕜₃ : Type u_7}
  [inst_8 : NormedField 𝕜₃] [inst_9 : Module 𝕜₃ G] {τ : 𝕜₃ →+* 𝕜₂} [RingHomSurjective τ] [inst_11 : TopologicalSpace F]
  [inst_12 : IsTopologicalAddGroup F] [inst_13 : ContinuousConstSMul 𝕜₂ F] [inst_14 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] {𝔖 : Set (Set E)},
  (∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜₁ s) →
    ∀ (B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖), (Continuous fun p => (B p.1) p.2) → Continuous ⇑B
-- Mathlib.Algebra.Group.Hom.Defs
/-- If `M` and `N` have additions, `f : M →ₙ+ N` is a surjective additive map,
and `M` is commutative, then `N` is commutative.  -/
Function.Surjective.add_comm : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Surjective ⇑f → IsAddCommutative M → IsAddCommutative N
-- Mathlib.Order.Antichain
IsAntichain.minimal_mem_iff : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : Preorder α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → (Minimal (fun x => x ∈ s) a ↔ a ∈ s)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentBundleCore_coordChange : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_6)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (i j : ↑(atlas H M)) (x : M),
  (tangentBundleCore I M).coordChange i j x =
    fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (Set.range ↑I) (↑((↑i).extend I) x)
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.essentiallySmall_congr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (e : C ≌ D), CategoryTheory.EssentiallySmall.{w, v, u} C ↔ CategoryTheory.EssentiallySmall.{w, v', u'} D
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.tendsto_extend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [inst_2 : TopologicalSpace γ] (di : IsDenseInducing i) {f : α → γ} {a : α},
  ContinuousAt f a → Filter.Tendsto f (nhds a) (nhds (di.extend f (i a)))
-- Mathlib.LinearAlgebra.AffineSpace.Combination
affineCombination_mem_affineSpan_image : ∀ {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [Nontrivial k] {s : Finset ι} {w : ι → k},
  ∑ i ∈ s, w i = 1 →
    ∀ {s' : Set ι},
      (∀ i ∈ s, i ∉ s' → w i = 0) → ∀ (p : ι → P), (Finset.affineCombination k s p) w ∈ affineSpan k (p '' s')
-- Lean.Widget.UserWidget
/-- Get the panel widgets present around a particular position.  -/
Lean.Widget.getWidgets : Lean.Lsp.Position → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Widget.GetWidgetsResponse)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.Hom.mk_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Over Q X}
  (f :
    (CategoryTheory.MorphismProperty.Over.forget P Q X).obj A ⟶
      (CategoryTheory.MorphismProperty.Over.forget P Q X).obj B)
  (hf : Q (CategoryTheory.Over.Hom.left f)),
  CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Over.Hom.mk f hf) = f
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.liftOfIsRightKanExtension_fac_assoc : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H) (β : L.comp G ⟶ F)
  {Z : CategoryTheory.Functor C H} (h : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (F'.liftOfIsRightKanExtension α G β))
      (CategoryTheory.CategoryStruct.comp α h) =
    CategoryTheory.CategoryStruct.comp β h
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatInt64SintOfNatNat : Lean.Grind.ToInt.OfNat Int64 (Lean.Grind.IntInterval.sint 64)
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.mapₐ_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal A) [inst_5 : I.IsPrime] (J : Ideal B) [inst_6 : J.IsPrime]
  (f : A →ₐ[R] B) (hf : I = Ideal.comap f.toRingHom J) (x : I.ResidueField),
  (Ideal.ResidueField.mapₐ I J f hf) x = (Ideal.ResidueField.map I J f.toRingHom hf) x
-- Mathlib.Algebra.Order.Module.Defs
/-- Do not use this. Use `smul_lt_smul_of_pos_right` instead.  -/
SMulPosStrictMono.smul_lt_smul_of_pos_right : ∀ {α : Type u_1} {β : Type u_2} {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero β}
  [self : SMulPosStrictMono α β] ⦃b : β⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, a₁ < a₂ → a₁ • b < a₂ • b
-- Mathlib.Analysis.Normed.Operator.Extend
LinearMap.opNorm_extendOfNorm_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : NormedAddCommGroup F]
  [inst_3 : SeminormedAddCommGroup Eₗ] [inst_4 : NormedSpace 𝕜₂ F] [inst_5 : NormedSpace 𝕜 Eₗ] [inst_6 : AddCommGroup E]
  [inst_7 : Module 𝕜 E] [inst_8 : CompleteSpace F] {f : E →ₛₗ[σ₁₂] F} {e : E →ₗ[𝕜] Eₗ},
  DenseRange ⇑e → ∀ {C : ℝ}, 0 ≤ C → (∀ (x : E), ‖f x‖ ≤ C * ‖e x‖) → ‖f.extendOfNorm e‖ ≤ C
-- Init.Data.List.Lemmas
List.foldl_hom : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂} {l : List β}
  {init : α₁}, (∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) → List.foldl g₂ (f init) l = f (List.foldl g₁ init l)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
Unitary.coe_linearIsometryEquiv_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] (u : ↥(unitary (H →L[𝕜] H))), ↑↑(Unitary.linearIsometryEquiv u) = ↑u
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Complex.differentiable_exp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ], Differentiable 𝕜 Complex.exp
-- Mathlib.Topology.Constructions
IsOpenMap.codRestrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f → ∀ {s : Set Y} (hs : ∀ (a : X), f a ∈ s), IsOpenMap (Set.codRestrict f s hs)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.subset_normalizer_of_normal : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G} [hH : H.Normal], S ⊆ ↑(Subgroup.normalizer ↑H)
-- Mathlib.Data.PFun
PFun.fn.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (f f_1 : α →. β) (e_f : f = f_1) (a a_1 : α) (e_a : a = a_1) (a_2 : a ∈ f.Dom),
  f.fn a a_2 = f_1.fn a_1 ⋯
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_mul_X_pow_of_ne : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {i j : σ} (k : ℕ),
  i ≠ j → MvPolynomial.degreeOf i (p * MvPolynomial.X j ^ k) = MvPolynomial.degreeOf i p
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_toLp_single : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : DecidableEq ι] (i : ι) (b : β i),
  ‖WithLp.toLp p (Pi.single i b)‖ = ‖b‖
-- Lean.Parser.Basic
Lean.Parser.sepByElemParser : Lean.Parser.Parser → String → Lean.Parser.Parser
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometryEquiv.coe_withLpUniqueProd : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : Semiring 𝕜]
  [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β] [inst_4 : Module 𝕜 β]
  [inst_5 : Unique α], ⇑(LinearIsometryEquiv.withLpUniqueProd p 𝕜 α β) = WithLp.snd
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionObj : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᴹᵒᵖ D] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d { unmop := c }
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.mulEquivCongr.congr_simp : ∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : IsDomain B] [inst_5 : Algebra A B] [inst_6 : FaithfulSMul A B]
  [inst_7 : MulSemiringAction G B] [inst_8 : MulSemiringAction G' B] [inst_9 : IsGaloisGroup G A B]
  [inst_10 : IsGaloisGroup G' A B] [inst_11 : Finite G] [inst_12 : Finite G'],
  IsGaloisGroup.mulEquivCongr G G' A B = IsGaloisGroup.mulEquivCongr G G' A B
-- Mathlib.GroupTheory.GroupAction.Primitive
MulAction.IsBlock.subsingleton_or_eq_univ : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] [MulAction.IsPreprimitive G X] {B : Set X},
  MulAction.IsBlock G B → B.Subsingleton ∨ B = Set.univ
-- Mathlib.Algebra.Group.Defs
AddZero.toAdd : {M : Type u_2} → [self : AddZero M] → Add M
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} [inst_1 : SizeOf C] (obj : (X : Cᵒᵖ) → Submodule ↑(R.obj X) ↑(M.obj X))
  (map : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj X ≤ Submodule.comap (M.restrictₛₗ f) (obj Y)),
  sizeOf { obj := obj, map := map } = 1
-- Mathlib.Data.Sym.NatCard
Sym.instInfiniteOfNeZeroNat : ∀ (α : Type u_1) {k : ℕ} [Infinite α] [NeZero k], Infinite (Sym α k)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDeclExtState.builtin : Lean.Meta.Simp.SimprocDeclExtState → Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)
-- Init.Data.Vector.Lemmas
Vector.any_eq_not_all_not : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, xs.any p = !xs.all fun x => !p x
-- Init.Data.BitVec.Basic
/-- Count the number of leading zeros.  -/
BitVec.clz : {w : ℕ} → BitVec w → BitVec w
-- Mathlib.Order.Interval.Finset.Defs
IsEmpty.toLocallyFiniteOrderTop.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : IsEmpty α],
  IsEmpty.toLocallyFiniteOrderTop =
    { finsetIoi := fun a => isEmptyElim a, finsetIci := fun a => isEmptyElim a, finset_mem_Ici := ⋯,
      finset_mem_Ioi := ⋯ }
-- Std.Do.WP.Sound
Std.Do.instWPSoundStateTArgOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} {ps : Std.Do.PostShape} {σ : Type u_1} [inst : Monad m] [LawfulMonad m]
  [inst_2 : Std.Do.WP m ps] [Std.Do.WPSound m ps], Std.Do.WPSound (StateT σ m) (Std.Do.PostShape.arg σ ps)
-- Init.Control.Basic
Alternative.mk : {f : Type u → Type v} →
  [toApplicative : Applicative f] → ({α : Type u} → f α) → ({α : Type u} → f α → (Unit → f α) → f α) → Alternative f
-- Lean.Elab.ComputedFields
/-- Sets the computed fields for a block of mutual inductives,
adding the implementation via `implemented_by`.

The `computedFields` argument contains a pair
for every inductive in the mutual block,
consisting of the name of the inductive
and the names of the associated computed fields.
 -/
Lean.Elab.ComputedFields.setComputedFields : Array (Lean.Name × Array Lean.Name) → Lean.MetaM Unit
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Cardinal.lt_cof_ord_power : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → 1 < b → a < (b ^ a).ord.cof
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.sSup_singleton_bot : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SupSet α], sSup {⊥} = ⊥
-- Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
/-- Every non-zero prime ideal in a unique factorization domain contains a prime element.  -/
Ideal.IsPrime.exists_mem_prime_of_ne_bot : ∀ {R : Type u_2} [inst : CommSemiring R] [UniqueFactorizationMonoid R] {I : Ideal R},
  I.IsPrime → I ≠ ⊥ → ∃ x ∈ I, Prime x
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.mk : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [toComplementedLattice : ComplementedLattice (Submodule R M)], IsSemisimpleModule R M
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.fst_toProd : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] (x : AddMonoid.Coprod M N),
  (AddMonoid.Coprod.toProd x).1 = AddMonoid.Coprod.fst x
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coroot_root_eq_pairing : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  (P.flip (P.coroot i)) (P.root j) = P.pairing j i
-- Mathlib.Logic.Equiv.Sum
Equiv.prodSumDistrib_symm_apply_left : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α × β),
  (Equiv.prodSumDistrib α β γ).symm (Sum.inl a) = (a.1, Sum.inl a.2)