mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.mk.injEq : ∀ {dir : Std.Http.Protocol.H1.Direction} (userData : Array Std.Http.Chunk)
  (outputData : Std.Http.Internal.ChunkedBuffer) (state : Std.Http.Protocol.H1.Writer.State)
  (knownSize : Option Std.Http.Body.Length) (messageHead : Std.Http.Protocol.H1.Message.Head dir.swap)
  (sentMessage userClosedBody omitBody : Bool) (userDataBytes : ℕ) (userData_1 : Array Std.Http.Chunk)
  (outputData_1 : Std.Http.Internal.ChunkedBuffer) (state_1 : Std.Http.Protocol.H1.Writer.State)
  (knownSize_1 : Option Std.Http.Body.Length) (messageHead_1 : Std.Http.Protocol.H1.Message.Head dir.swap)
  (sentMessage_1 userClosedBody_1 omitBody_1 : Bool) (userDataBytes_1 : ℕ),
  ({ userData := userData, outputData := outputData, state := state, knownSize := knownSize, messageHead := messageHead,
        sentMessage := sentMessage, userClosedBody := userClosedBody, omitBody := omitBody,
        userDataBytes := userDataBytes } =
      { userData := userData_1, outputData := outputData_1, state := state_1, knownSize := knownSize_1,
        messageHead := messageHead_1, sentMessage := sentMessage_1, userClosedBody := userClosedBody_1,
        omitBody := omitBody_1, userDataBytes := userDataBytes_1 }) =
    (userData = userData_1 ∧
      outputData = outputData_1 ∧
        state = state_1 ∧
          knownSize = knownSize_1 ∧
            messageHead = messageHead_1 ∧
              sentMessage = sentMessage_1 ∧
                userClosedBody = userClosedBody_1 ∧ omitBody = omitBody_1 ∧ userDataBytes = userDataBytes_1)
-- Batteries.Data.String.Lemmas
String.validFor_toSubstring : ∀ (s : String), Substring.Raw.ValidFor [] s.toList [] s.toRawSubstring
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- Given two morphisms `f₁ : X₁ ⟶ S` and `f₂ : X₂ ⟶ S`, this is the choice
of a pullback of `f₁` and `f₂`.  -/
CategoryTheory.Limits.ChosenPullback : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X₁ X₂ S : C} → (X₁ ⟶ S) → (X₂ ⟶ S) → Type (max u v)
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.contDiff : ∀ {n : ℕ∞}, ContDiff ℝ (↑n) Real.smoothTransition
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.newLocal.injEq : ∀ (fvarId : Lean.FVarId) (goal : Lean.Meta.Grind.Goal) (fvarId_1 : Lean.FVarId) (goal_1 : Lean.Meta.Grind.Goal),
  (Lean.Meta.Grind.IntroResult.newLocal✝ fvarId goal = Lean.Meta.Grind.IntroResult.newLocal✝ fvarId_1 goal_1) =
    (fvarId = fvarId_1 ∧ goal = goal_1)
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.π₁_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  {Z : HomologicalComplex C c} (h : K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.ι K)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.π₁ K) h) =
    h
-- Lean.Util.MonadCache
Lean.MonadStateCacheT.instMonadHashMapCacheAdapter : {α β : Type} →
  {m : Type → Type} →
    [inst : BEq α] → [inst_1 : Hashable α] → [Monad m] → Lean.MonadHashMapCacheAdapter α β (Lean.MonadStateCacheT α β m)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
/-- Turn a morphism in `QuadraticModuleCat` back into a `Isometry`.  -/
QuadraticModuleCat.Hom.toIsometry : {R : Type u} → [inst : CommRing R] → {X Y : QuadraticModuleCat R} → X.Hom Y → X.form →qᵢ Y.form
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {Q : Type u_4} [inst_3 : AddCommMonoid Q]
  {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) (x : M),
  (f.addEquivOfAddEquiv k H) (f x) = k (j x)
-- Mathlib.AlgebraicGeometry.Morphisms.FlatMono
/-- Flat monomorphisms that are locally of finite presentation are open immersions. In particular,
every smooth monomorphism is an open immersion.
The converse holds by `inferInstance`.
 -/
AlgebraicGeometry.IsOpenImmersion.of_flat_of_mono : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f]
  [AlgebraicGeometry.LocallyOfFinitePresentation f] [CategoryTheory.Mono f], AlgebraicGeometry.IsOpenImmersion f
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.Hom.ι_comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} {I : CategoryTheory.InjectiveResolution Z} {Z' : C}
  {I' : CategoryTheory.InjectiveResolution Z'} {f : Z ⟶ Z'} (φ : I.Hom I' f),
  CategoryTheory.CategoryStruct.comp I.ι φ.hom =
    CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) I'.ι
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.isPell_norm : ∀ {d : ℤ} {b : ℤ√d}, Pell.IsPell b ↔ b * star b = 1
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_eq_one_iff_right₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a : G₀} [PosMulStrictMono G₀]
  [ZeroLEOneClass G₀], 0 ≤ a → a ≠ 1 → ∀ {n : ℤ}, a ^ n = 1 ↔ n = 0
-- Aesop.Percent
Aesop.Percent.mk.inj : ∀ {toFloat toFloat_1 : Float}, { toFloat := toFloat } = { toFloat := toFloat_1 } → toFloat = toFloat_1
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.arrowCongrEquiv_symm_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7}
  {V₃ : Type u_8} {V₄ : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : AddCommGroup V₄] [inst_5 : Module k V₁] [inst_6 : Module k V₂]
  [inst_7 : Module k V₃] [inst_8 : Module k V₄] [inst_9 : AddTorsor V₁ P₁] [inst_10 : AddTorsor V₂ P₂]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₃ ≃ᵃ[k] P₄) (f : P₂ →ᵃ[k] P₄)
  (x : P₁), ((e₁.arrowCongrEquiv e₂).symm f) x = e₂.symm (f (e₁ x))
-- Mathlib.Algebra.Group.Hom.Instances
/-- If `G` is an additive group, then so is `ZeroHom M G`.  -/
ZeroHom.instAddGroup : {M : Type uM} → {N : Type uN} → [inst : Zero M] → [inst_1 : AddGroup N] → AddGroup (ZeroHom M N)
-- Mathlib.FieldTheory.Galois.Basic
/-- If `K / E / k` is a field extension tower with `E / k` normal,
`L` is an intermediate field of `E / k`, then the fixing subgroup of `L` viewed as an
intermediate field of `K / k` is equal to the preimage of the fixing subgroup of `L` viewed as an
intermediate field of `E / k` under the natural map `Aut(K / k) → Aut(E / k)`
(`AlgEquiv.restrictNormalHom`).  -/
IntermediateField.map_fixingSubgroup : ∀ {F : Type u_1} {E : Type u_2} (E' : Type u_3) [inst : Field F] [inst_1 : Field E] [inst_2 : Field E']
  [inst_3 : Algebra F E] [inst_4 : Algebra F E'] [inst_5 : Algebra E E'] [inst_6 : IsScalarTower F E E']
  (L : IntermediateField F E) [inst_7 : Normal F E],
  (IntermediateField.map (IsScalarTower.toAlgHom F E E') L).fixingSubgroup =
    Subgroup.comap (AlgEquiv.restrictNormalHom E) L.fixingSubgroup
-- Lean.SubExpr
/-- Same as `Expr.traverseApp` but also includes a
`SubExpr.Pos` argument for tracking subexpression position.  -/
Lean.Expr.traverseAppWithPos : {M : Type → Type u_1} →
  [Monad M] → (Lean.SubExpr.Pos → Lean.Expr → M Lean.Expr) → Lean.SubExpr.Pos → Lean.Expr → M Lean.Expr
-- Mathlib.Algebra.MvPolynomial.Degrees
/-- **Alias** of `MvPolynomial.totalDegree_finsetProd`. -/
MvPolynomial.totalDegree_finset_prod : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} (s : Finset ι) (f : ι → MvPolynomial σ R),
  (s.prod f).totalDegree ≤ ∑ i ∈ s, (f i).totalDegree
-- Mathlib.Order.CountableSupClosed
upperBounds_countableSupClosure : ∀ {α : Type u_2} [inst : Preorder α] (s : Set α), upperBounds (countableSupClosure s) = upperBounds s
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Iso.map_inv_hom_id_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {X Y : C} (e : X ≅ Y)
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D) {Z_1 : E} (h : (F.obj Y).obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z)
      (CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) h) =
    h
-- Mathlib.MeasureTheory.Group.Measure
/-- A measure on an additive group is an additive Haar measure if it is left-invariant, and
gives finite mass to compact sets and positive mass to open sets.

Textbooks generally require an additional regularity assumption to ensure nice behavior on
arbitrary locally compact groups. Use `[IsAddHaarMeasure μ] [Regular μ]` or
`[IsAddHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our
sense is automatically regular and inner regular on second countable locally compact groups, as
checked just below this definition.  -/
MeasureTheory.Measure.IsAddHaarMeasure : {G : Type u_3} → [AddGroup G] → [TopologicalSpace G] → [inst : MeasurableSpace G] → MeasureTheory.Measure G → Prop
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.iSup_affineOpens_eq_top : ∀ (X : AlgebraicGeometry.Scheme), ⨆ i, ↑i = ⊤
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ),
  autoParam (n₀ < n₁) CategoryTheory.Triangulated.TStructure.zero._auto_1 → ∀ [t.IsLE X n₀] [t.IsGE Y n₁], f = 0
-- Mathlib.Order.Zorn
zorn_le : ∀ {α : Type u_1} [inst : Preorder α], (∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → BddAbove c) → ∃ m, IsMax m
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.regularEpiCategoryOfSplitEpiCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.SplitEpiCategory C],
  CategoryTheory.IsRegularEpiCategory C
-- Lean.Parser.Attr
Lean.Parser.Attr.instance.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The condition that a functor `F` has a pointwise left Kan extension along `L` at `Y`.
It means that the functor `CostructuredArrow.proj L Y ⋙ F : CostructuredArrow L Y ⥤ H`
has a colimit.  -/
CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            CategoryTheory.Functor C D → CategoryTheory.Functor C H → D → Prop
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Right.min_le_max_of_add_le_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] {a b c d : α} [AddLeftMono α] [AddRightStrictMono α],
  a + b ≤ c + d → min a b ≤ max c d
-- Mathlib.Lean.Meta.CongrTheorems
/-- `mkRichHCongr fType funInfo fixedFun fixedParams forceHEq`
create a congruence lemma to prove that `Eq/HEq (f a₁ ... aₙ) (f' a₁' ... aₙ')`.
The functions have type `fType` and the number of arguments is governed by the `funInfo` data.
Each argument produces an `Eq/HEq aᵢ aᵢ'` hypothesis, but we also provide these hypotheses
the additional facts that the preceding equalities have been proved (unlike in `mkHCongrWithArity`).
The first two arguments of the resulting theorem are for `f` and `f'`, followed by a proof
of `f = f'`, unless `fixedFun` is `true` (see below).

When including hypotheses about previous hypotheses, we make use of dependency information
and only include relevant equalities.

The argument `fty` denotes the type of `f`. The arity of the resulting congruence lemma is
controlled by the size of the `info` array.

For the purpose of generating nicer lemmas (to help `to_additive` for example),
this function supports generating lemmas where certain parameters
are meant to be fixed:

* If `fixedFun` is `false` (the default) then the lemma starts with three arguments for `f`, `f'`,
  and `h : f = f'`. Otherwise, if `fixedFun` is `true` then the lemma starts with just `f`.

* If the `fixedParams` argument has `true` for a particular argument index, then this is a hint
  that the congruence lemma may use the same parameter for both sides of the equality. There is
  no guarantee -- it respects it if the types are equal for that parameter (i.e., if the parameter
  does not depend on non-fixed parameters).

If `forceHEq` is `true` then the conclusion of the generated theorem is a `HEq`.
Otherwise it might be an `Eq` if the equality is homogeneous.

This is the interpretation of the `CongrArgKind`s in the generated congruence theorem:
* `.eq` corresponds to having three arguments `(x : α) (x' : α) (h : x = x')`.
  Note that `h` might have additional hypotheses.
* `.heq` corresponds to having three arguments `(x : α) (x' : α') (h : x ≍ x')`
  Note that `h` might have additional hypotheses.
* `.fixed` corresponds to having a single argument `(x : α)` that is fixed between the LHS and RHS
* `.subsingletonInst` corresponds to having two arguments `(x : α) (x' : α')` for which the
  congruence generator was able to prove that `x ≍ x'` already. This is a slight abuse of
  this `CongrArgKind` since this is used even for types that are not subsingleton typeclasses.

Note that the first entry in this array is for the function itself.
 -/
Lean.Meta.mkRichHCongr : Lean.Expr →
  Lean.Meta.FunInfo →
    optParam Bool false → optParam (Array Bool) #[] → optParam Bool false → Lean.MetaM Lean.Meta.CongrTheorem
-- Mathlib.Order.Category.Lat
Lat.mk.inj : ∀ {carrier : Type u_1} {str : Lattice carrier} {carrier_1 : Type u_1} {str_1 : Lattice carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Std.Async.DNS
/-- Performs a reverse DNS lookup on a `SocketAddress`.
 -/
Std.Async.DNS.getNameInfo : Std.Net.SocketAddress → Std.Async.Async Std.Async.DNS.NameInfo
-- Std.Data.TreeSet.Raw.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.TreeSet.Raw.get? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → Option α
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.contains_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  m₁.Equiv m₂ → m₁.contains k = m₂.contains k
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp' : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃))
      (F.mapComp' f₀₁ f₁₃ f hf) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) (F.mapComp' f₀₂ f₂₃ f ⋯))
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- Create a bilinear map (represented as a map `E →L[𝕜] F →L[𝕜] G`) from the corresponding linear
map and a bound on the norm of the image. The linear map can be constructed using
`LinearMap.mk₂`. Lemmas `LinearMap.mkContinuous₂_norm_le'` and `LinearMap.mkContinuous₂_norm_le`
provide estimates on the norm of an operator constructed using this function.  -/
LinearMap.mkContinuous₂ : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {𝕜₃ : Type u_3} →
      {E : Type u_4} →
        {F : Type u_6} →
          {G : Type u_8} →
            [inst : SeminormedAddCommGroup E] →
              [inst_1 : SeminormedAddCommGroup F] →
                [inst_2 : SeminormedAddCommGroup G] →
                  [inst_3 : NontriviallyNormedField 𝕜] →
                    [inst_4 : NontriviallyNormedField 𝕜₂] →
                      [inst_5 : NontriviallyNormedField 𝕜₃] →
                        [inst_6 : NormedSpace 𝕜 E] →
                          [inst_7 : NormedSpace 𝕜₂ F] →
                            [inst_8 : NormedSpace 𝕜₃ G] →
                              {σ₂₃ : 𝕜₂ →+* 𝕜₃} →
                                {σ₁₃ : 𝕜 →+* 𝕜₃} →
                                  [RingHomIsometric σ₂₃] →
                                    (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) →
                                      (C : ℝ) → (∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) → E →SL[σ₁₃] F →SL[σ₂₃] G
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid γ] {A : Set α} {B : Set β} {C : Set γ} {f : α → β} {g : β → γ} {n : ℕ},
  IsAddFreimanHom n B C g → IsAddFreimanHom n A B f → IsAddFreimanHom n A C (g ∘ f)
-- Lean.ScopedEnvExtension
Lean.SimpleScopedEnvExtension.Descr.name : {α σ : Type} → Lean.SimpleScopedEnvExtension.Descr α σ → Lean.Name
-- Mathlib.NumberTheory.Fermat
/-- `Fₙ = 2^(2^n)+1` is prime if `3^((Fₙ - 1)/2) = -1 mod Fₙ` (**Pépin's test**).  -/
Nat.pepin_primality' : ∀ (n : ℕ), 3 ^ ((n.fermatNumber - 1) / 2) = -1 → Nat.Prime n.fermatNumber
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn'_congr : ∀ {γ α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_3 : Std.IteratorLoop α Id m] {ita itb : Std.Iter β} (w : ita = itb) {b b' : γ},
  b = b' →
    ∀ {f : (a' : β) → a' ∈ ita → γ → m (ForInStep γ)} {g : (a' : β) → a' ∈ itb → γ → m (ForInStep γ)},
      (∀ (a : β) (m_1 : a ∈ itb) (b : γ), f a ⋯ b = g a m_1 b) → forIn' ita b f = forIn' itb b' g
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galLiftEquiv_apply : ∀ {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [inst : CommRing A]
  [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : Field K]
  [inst_6 : Field L] [inst_7 : Field L₂] [inst_8 : Algebra A K] [inst_9 : IsFractionRing A K] [inst_10 : Algebra K L]
  [inst_11 : Algebra A L] [inst_12 : IsScalarTower A K L] [inst_13 : Algebra K L₂] [inst_14 : Algebra A L₂]
  [inst_15 : IsScalarTower A K L₂] [inst_16 : Algebra B L] [inst_17 : IsScalarTower A B L]
  [inst_18 : IsIntegralClosure B A L] [inst_19 : Algebra B₂ L₂] [inst_20 : IsScalarTower A B₂ L₂]
  [inst_21 : IsIntegralClosure B₂ A L₂] [inst_22 : Algebra.IsAlgebraic K L] [inst_23 : Algebra.IsAlgebraic K L₂]
  (σ : B ≃ₐ[A] B₂), ⇑(galLiftEquiv K L L₂ σ) = ⇑(galLift K L L₂ ↑σ)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_single_one_mul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] (x : MonoidAlgebra R M) (r : R) (m : M),
  (MonoidAlgebra.single 1 r * x).coeff m = r * x.coeff m
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α}, s.Nonempty → t.Nonempty → (s + t).Nonempty
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.congr_trans : ∀ (p : ENNReal) {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} (f : V ≃ V') (g : V' ≃ V''),
  WithLp.congr p (f.trans g) = (WithLp.congr p f).trans (WithLp.congr p g)
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.lt : ℝ → ℝ → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- This is a more convenient formulation to show that a `KernelFork` constructed using
`KernelFork.ofι` is a limit cone.
 -/
CategoryTheory.Limits.KernelFork.IsLimit.ofι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {W : C} →
            (g : W ⟶ X) →
              (eq : CategoryTheory.CategoryStruct.comp g f = 0) →
                (lift : {W' : C} → (g' : W' ⟶ X) → CategoryTheory.CategoryStruct.comp g' f = 0 → (W' ⟶ W)) →
                  (∀ {W' : C} (g' : W' ⟶ X) (eq' : CategoryTheory.CategoryStruct.comp g' f = 0),
                      CategoryTheory.CategoryStruct.comp (lift g' eq') g = g') →
                    (∀ {W' : C} (g' : W' ⟶ X) (eq' : CategoryTheory.CategoryStruct.comp g' f = 0) (m : W' ⟶ W),
                        CategoryTheory.CategoryStruct.comp m g = g' → m = lift g' eq') →
                      CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι g eq)
-- Mathlib.Data.Finset.SDiff
Finset.union_sdiff_cancel_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, Disjoint s t → (s ∪ t) \ t = s
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ₂Sq_eq : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.Ψ₂Sq = W.twoTorsionPolynomial.toPoly
-- Mathlib.Probability.Independence.ZeroOne
/-- **Kolmogorov's 0-1 law** : any event in the tail σ-algebra of an independent sequence of
sub-σ-algebras has probability 0 or 1.  -/
ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atBot : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι],
  (∀ (n : ι), s n ≤ m0) → ProbabilityTheory.iIndep s μ → ∀ {t : Set Ω}, MeasurableSet t → μ t = 0 ∨ μ t = 1
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.instLinearEquivClass : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W}, LinearEquivClass (σ.Equiv ρ) A W V
-- Mathlib.Probability.Kernel.RadonNikodym
/-- A set of points in `α × γ` related to the absolute continuity / mutual singularity of
`κ` and `η`.  -/
ProbabilityTheory.Kernel.mutuallySingularSet : {α : Type u_1} →
  {γ : Type u_2} →
    {mα : MeasurableSpace α} →
      {mγ : MeasurableSpace γ} →
        [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] →
          ProbabilityTheory.Kernel α γ → ProbabilityTheory.Kernel α γ → Set (α × γ)
-- Init.Data.Vector.Lemmas
Vector.getElem_setIfInBounds : ∀ {α : Type u_1} {n j i : ℕ} {xs : Vector α n} {x : α} (hj : j < n),
  (xs.setIfInBounds i x)[j] = if i = j then x else xs[j]
-- Init.Data.Int.Linear
Int.Internal.Linear.instBEqExpr : BEq Int.Internal.Linear.Expr
-- Mathlib.GroupTheory.Sylow
Sylow.orbit_eq_top : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G),
  MulAction.orbit G P = ⊤
-- Init.Data.SInt.Lemmas
Int8.mul_neg : ∀ (a b : Int8), a * -b = -(a * b)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.isIso_rightHomologyι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology], S.g = 0 → CategoryTheory.IsIso S.rightHomologyι
-- Init.Data.Option.Attach
Option.attach_eq_none_iff : ∀ {α : Type u_1} {o : Option α}, o.attach = none ↔ o = none