mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Finite.Monad
Set.fintypeSeq' : {α β : Type u} → [DecidableEq β] → (f : Set (α → β)) → (s : Set α) → [Fintype ↑f] → [Fintype ↑s] → Fintype ↑(f <*> s)
-- Mathlib.Topology.LocallyFinite
/-- If `f : β → Set α` is a locally finite family of closed sets, then for any `x : α`, the
intersection of the complements to `f i`, `x ∉ f i`, is a neighbourhood of `x`.  -/
LocallyFinite.iInter_compl_mem_nhds : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
  LocallyFinite f → (∀ (i : ι), IsClosed (f i)) → ∀ (x : X), ⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ ∈ nhds x
-- Mathlib.Data.Set.Lattice
Set.mem_iInter₂_of_mem : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {a : α},
  (∀ (i : ι) (j : κ i), a ∈ s i j) → a ∈ ⋂ i, ⋂ j, s i j
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.inner_normalized_ortho_sq_add_inner_sq_eq_one : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  ‖x‖ = 1 → ‖y‖ = 1 → inner ℝ x (NormedSpace.normalize (InnerProductGeometry.ortho✝ y x)) ^ 2 + inner ℝ x y ^ 2 = 1
-- Init.System.IO
/-- The file should be opened for both reading and writing.

It is an error if the file does not already exist. The read/write cursor is positioned at the
start of the file.

* `open` flags: `O_RDWR`
* `fdopen` mode: `r+`
 -/
IO.FS.Mode.readWrite : IO.FS.Mode
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.mapCongr_inv_app_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] [inst_2 : P.IsStableUnderComposition]
  [inst_3 : Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) (X_1 : P.Under Q Y),
  ((CategoryTheory.MorphismProperty.Under.mapCongr Q hfg hf).inv.app X_1).right =
    CategoryTheory.CategoryStruct.id X_1.right
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.symm_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  e.symm.source = e.target
-- Mathlib.Algebra.Module.Presentation.Cokernel
/-- Given an exact sequence of `A`-modules `M₁ → M₂ → M₃ → 0`, this is the presentation
of `M₃` that is obtained from a presentation `pres₂` of `M₂`, a choice of generators
`g₁ : ι → M₁` of `M₁`, and an additional data in a `Presentation.CokernelData` structure.  -/
Module.Presentation.ofExact : {A : Type u} →
  [inst : Ring A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        {M₃ : Type v₃} →
          [inst_1 : AddCommGroup M₁] →
            [inst_2 : Module A M₁] →
              [inst_3 : AddCommGroup M₂] →
                [inst_4 : Module A M₂] →
                  [inst_5 : AddCommGroup M₃] →
                    [inst_6 : Module A M₃] →
                      {f : M₁ →ₗ[A] M₂} →
                        {g : M₂ →ₗ[A] M₃} →
                          (pres₂ : Module.Presentation A M₂) →
                            {ι : Type w₁} →
                              {g₁ : ι → M₁} →
                                pres₂.CokernelData f g₁ →
                                  Function.Exact ⇑f ⇑g →
                                    Function.Surjective ⇑g →
                                      Submodule.span A (Set.range g₁) = ⊤ → Module.Presentation A M₃
-- Init.Grind.Config
Lean.Grind.NoopConfig.toConfig : Lean.Grind.NoopConfig → Lean.Grind.Config
-- Lean.Expr
Lean.Expr.hasLevelMVarEx : Lean.Expr → Bool
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.Localization.exists_rightFraction : ∀ {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 : L.IsLocalization W] [W.HasRightCalculusOfFractions] {X Y : C}
  (f : L.obj X ⟶ L.obj Y), ∃ φ, f = φ.map L ⋯
-- Mathlib.Data.ENat.Basic
ENat.one_le_iff_ne_zero_withTop : ∀ {n : WithTop ℕ∞}, 1 ≤ n ↔ n ≠ 0
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.map_punctured_nhds_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (x : X),
  Filter.map (⇑h) (nhdsWithin x {x}ᶜ) = nhdsWithin (h x) {h x}ᶜ
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.mul_right : ∀ {α : Type u_1} {M : Type u_4} [inst : MulZeroClass M] (f : α → M) {g : α → M},
  Function.HasFiniteSupport g → Function.HasFiniteSupport (f * g)
-- Mathlib.Topology.MetricSpace.Isometry
/-- The inverse of an isometric isomorphism, as an isometric isomorphism.  -/
IsometryEquiv.symm : {α : Type u} → {β : Type v} → [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → α ≃ᵢ β → β ≃ᵢ α
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.instIsStableUnderRetractsTriangEnvelope : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C), P.triangEnvelope.IsStableUnderRetracts
-- Mathlib.RingTheory.Localization.Defs
Localization.instNoZeroDivisors : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} [NoZeroDivisors R], NoZeroDivisors (Localization M)
-- Lean.SubExpr
Lean.SubExpr.instFromJsonGoalLocation.fromJson : Lean.Json → Except String Lean.SubExpr.GoalLocation
-- Mathlib.Order.SupClosed
InfClosed.sInf_mem : ∀ {α : Type u_3} [inst : CompleteLattice α] {s t : Set α}, InfClosed s → t.Finite → ⊤ ∈ s → t ⊆ s → sInf t ∈ s
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.coe_mul : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (e e' : X ≃ᵈ X), ⇑(e * e') = ⇑e ∘ ⇑e'
-- Init.Data.String.Defs
String.Pos.Raw.offsetBy_rawEndPos_left : ∀ {p : String.Pos.Raw} {s : String}, s.rawEndPos.offsetBy p = p + s
-- Init.Grind.Norm
Lean.Grind.exists_prop : ∀ {a b : Prop}, (∃ (_ : a), b) = (a ∧ b)
-- Lean.DocString.Extension
Lean.ModuleDoc.mk : String → Lean.DeclarationRange → Lean.ModuleDoc
-- Mathlib.RingTheory.IsAdjoinRoot
/-- Choose an arbitrary representative so that `h.map (h.repr x) = x`.

If `f` is monic, use `IsAdjoinRootMonic.modByMonicHom` for a unique choice of representative.
 -/
IsAdjoinRoot.repr : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : Ring S] → {f : Polynomial R} → [inst_2 : Algebra R S] → IsAdjoinRoot S f → S → Polynomial R
-- Init.Control.ExceptCps
ExceptCpsT.runCatch_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {x : α} [inst : Monad m], (pure x).runCatch = pure x
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.comp_pushforward : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J K : C} (f : I ⟶ J) (g : J ⟶ K)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ChosenPullbacksAlong g]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)]
  [inst_4 : CategoryTheory.ExponentiableMorphism f] [inst_5 : CategoryTheory.ExponentiableMorphism g],
  CategoryTheory.ExponentiableMorphism.pushforward (CategoryTheory.CategoryStruct.comp f g) =
    (CategoryTheory.ExponentiableMorphism.pushforward f).comp (CategoryTheory.ExponentiableMorphism.pushforward g)
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.map₂_map : ∀ {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]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X Y : CategoryTheory.ThinSkeleton C} (a : X ⟶ Y),
  (CategoryTheory.ThinSkeleton.map₂ F).map a = CategoryTheory.ThinSkeleton.map₂NatTrans F a
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.whiskeringEquivalence_functor : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J),
  (CategoryTheory.Limits.Cocone.whiskeringEquivalence e).functor = CategoryTheory.Limits.Cocone.whiskering e.functor
-- Init.Data.Iterators.Combinators.Monadic.ULift
/-- `ULiftT.{v, u}` shrinks a monad on `Type max u v` to a monad on `Type u`.  -/
Std.Iterators.ULiftT : (Type (max u v) → Type v') → Type u → Type v'
-- Mathlib.Order.Preorder.Chain
Flag.chain_lt : ∀ {α : Type u_1} [inst : PartialOrder α] (s : Flag α), IsChain (fun x1 x2 => x1 < x2) ↑s
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- If every `x` has a neighbourhood on which `b ↦ ∏' i, f i b` converges uniformly
to `g`, then the product converges locally uniformly to `g`. Note that this is not a
tautology, and the converse is only true if the domain is locally compact.  -/
hasProdLocallyUniformly_of_of_forall_exists_nhds : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  (∀ (x : β), ∃ t ∈ nhds x, HasProdUniformlyOn f g t) → HasProdLocallyUniformly f g
-- Mathlib.Topology.UniformSpace.Cauchy
/-- **Alias** of `Filter.TotallyBounded.totallyBounded_setOfPred_clusterPt`. -/
Filter.TotallyBounded.totallyBounded_setOf_clusterPt : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α}, f.TotallyBounded → TotallyBounded {x | ClusterPt x f}
-- Init.Data.Nat.Div.Basic
Nat.add_mod_right : ∀ (x z : ℕ), (x + z) % z = x % z
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.exists_mem_ne_zero_of_sum_ne_zero : ∀ {M : Type u_4} [inst : AddMonoid M] {l : List M}, l.sum ≠ 0 → ∃ x ∈ l, x ≠ 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.addCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : AddCommMonoid α], Set.addCommMonoid = { toAddMonoid := Set.addMonoid, add_comm := ⋯ }
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.measurable_dirac : ∀ {α : Type u_1} {mα : MeasurableSpace α}, Measurable MeasureTheory.Measure.dirac
-- Mathlib.Topology.AlexandrovDiscrete
isClopen_iUnion : ∀ {ι : Sort u_1} {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {f : ι → Set α},
  (∀ (i : ι), IsClopen (f i)) → IsClopen (⋃ i, f i)
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.indepFun_const_left : ∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
  [ProbabilityTheory.IsZeroOrMarkovKernel κ] (c : β') (X : Ω → β), ProbabilityTheory.Kernel.IndepFun (fun x => c) X κ μ
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.ι_mapBifunctorAssociatorX_hom : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_8 : CategoryTheory.Limits.HasZeroMorphisms C₃] [inst_9 : CategoryTheory.Preadditive C₁₂]
  [inst_10 : CategoryTheory.Preadditive C₂₃] [inst_11 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_12 : F₁₂.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_14 : G.Additive]
  [inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [inst_16 : G₂₃.PreservesZeroMorphisms]
  [inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_18 : F.PreservesZeroMorphisms]
  [inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7}
  {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_20 : DecidableEq ι₄]
  {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃)
  (c₄ : ComplexShape ι₄) [inst_21 : TotalComplexShape c₁ c₂ c₁₂] [inst_22 : TotalComplexShape c₁₂ c₃ c₄]
  [inst_23 : TotalComplexShape c₂ c₃ c₂₃] [inst_24 : TotalComplexShape c₁ c₂₃ c₄], ⋯
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.eq_comp_toContinuousLinearMap_symm : ∀ {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₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_5 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {M₁ : Type u_4}
  [inst_6 : TopologicalSpace M₁] [inst_7 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_8 : TopologicalSpace M₂]
  [inst_9 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_10 : TopologicalSpace M₃] [inst_11 : AddCommMonoid M₃]
  [inst_12 : Module R₁ M₁] [inst_13 : Module R₂ M₂] [inst_14 : Module R₃ M₃] (e₁₂ : M₁ ≃SL[σ₁₂] M₂)
  [inst_15 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (f : M₂ →SL[σ₂₃] M₃) (g : M₁ →SL[σ₁₃] M₃),
  f = g ∘SL ↑e₁₂.symm ↔ f ∘SL ↑e₁₂ = g
-- Mathlib.Data.Stream.Init
Stream'.zip_eq : ∀ {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (s₁ : Stream' α) (s₂ : Stream' β),
  Stream'.zip f s₁ s₂ = Stream'.cons (f s₁.head s₂.head) (Stream'.zip f s₁.tail s₂.tail)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_insert : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a : α}, (m.insert k).get? a = if (k == a) = true ∧ k ∉ m then some k else m.get? a
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.ofIsoI_m : ∀ {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).m = CategoryTheory.CategoryStruct.comp e.inv F.m
-- Init.Data.Rat.Lemmas
Rat.normalize_num_den : ∀ {n : ℤ} {d : ℕ} {z : d ≠ 0} {n' : ℤ} {d' : ℕ} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'},
  Rat.normalize n d z = { num := n', den := d', den_nz := z', reduced := c } → ∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
-- Init.Grind.Interactive
/-- `with_annotate_state stx t` annotates the lexical range of `stx : Syntax` with
the initial and final state of running tactic `t`.
 -/
Lean.Parser.Tactic.Grind.withAnnotateState : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_K : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).K = S.X₂
-- Mathlib.Data.SProd
/-- The Cartesian product `s ×ˢ t` is the set of `(a, b)` such that `a ∈ s` and `b ∈ t`.  -/
«term_×ˢ_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuousOn_univ_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β},
  UpperSemicontinuousOn f Set.univ ↔ UpperSemicontinuous f
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.liftPropWithinAt_self : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H']
  {P : (H → H') → Set H → H → Prop} {f : H → H'} {s : Set H} {x : H},
  ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P f s x
-- Init.Data.String.Basic
List.asString_eq_empty_iff : ∀ {l : List Char}, String.ofList l = "" ↔ l = []
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.mem_adjoin_iff_div : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E} {x : E},
  x ∈ IntermediateField.adjoin F S ↔ ∃ r ∈ Algebra.adjoin F S, ∃ s ∈ Algebra.adjoin F S, x = r / s
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
/-- `#ErdosStone.filter` is arbitrarily large with respect to `n`.

This is an auxiliary lemma for the Erdős-Stone theorem.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.mul_le_card_filter_mul : ∀ {n : ℕ} {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj] {ε : ℝ} {r t t' : ℕ}
  (K : G.CompleteEquipartiteSubgraph r t'),
  0 < r →
    0 < t' →
      ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n →
        ∀ {N : ℕ},
          (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t) →
            ↑N * (↑t' - ↑t) ≤ ↑(SimpleGraph.ErdosStone.filter✝ K t).card * (↑t' - ↑t)
-- Mathlib.Topology.Inseparable
stableUnderGeneralization_compl_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, StableUnderGeneralization sᶜ ↔ StableUnderSpecialization s
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.toLieSubmodule_le_rootSpace_zero : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H], H.toLieSubmodule ≤ LieAlgebra.rootSpace H 0
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
/-- The integrand is chosen to match the conclusion of `Real.deriv_inv_log`.  -/
integral_inv_div_log_sq : ∀ {a b : ℝ}, 1 < a → 1 < b → ∫ (t : ℝ) in a..b, t⁻¹ / Real.log t ^ 2 = (Real.log a)⁻¹ - (Real.log b)⁻¹
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `toStained stx` scans the input `Syntax` `stx` extracting identifiers and atoms, making an effort
to convert them to `Stained`.
The function is used to extract "location" information about `stx`: either explicit locations as in
`rw [] at locations` or implicit ones as `rw [h]`.

Whether or not what this function extracts really is a location will be determined by the linter
using data embedded in the `InfoTree`s.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.toStained : Lean.Syntax → Std.HashSet Mathlib.Linter.Flexible.Stained✝
-- Mathlib.FieldTheory.Galois.Profinite
/-- A function from `K` to `K` defined pointwise using a family of compatible elements of
`Gal(L/k)` where `L` is a `FiniteGaloisIntermediateField`  -/
_private.Mathlib.FieldTheory.Galois.Profinite.0.InfiniteGalois.toAlgEquivAux : {k : Type u_3} →
  {K : Type u_4} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          [IsGalois k K] →
            ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop → K → K
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.neg_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {P Q : CategoryTheory.Idempotents.Karoubi C} (f : P ⟶ Q), -f = { f := -f.f, comm := ⋯ }
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.ext_iff : ∀ {E : Type u_3} [inst : AddGroup E] {p q : NonarchAddGroupSeminorm E}, p = q ↔ ∀ (x : E), p x = q x
-- Mathlib.RingTheory.FractionalIdeal.Basic
IsFractional.mul : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I J : Submodule R P}, IsFractional S I → IsFractional S J → IsFractional S (I * J)
-- Mathlib.NumberTheory.LucasLehmer
/-- If 3 is not a square and 2 is square then $\omega^{(q+1)/2}=-1$.  -/
LucasLehmer.X.pow_ω : ∀ {q : ℕ} [inst : Fact (Nat.Prime q)],
  Odd q → legendreSym q 3 = -1 → legendreSym q 2 = 1 → LucasLehmer.X.ω ^ ((q + 1) / 2) = -1
-- Init.Data.Vector.Zip
Vector.getElem?_zipWith_eq_some : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β → γ} {as : Vector α n} {bs : Vector β n} {z : γ}
  {i : ℕ}, (Vector.zipWith f as bs)[i]? = some z ↔ ∃ x y, as[i]? = some x ∧ bs[i]? = some y ∧ f x y = z
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.isPullback_map_snd_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z S : C} (f : X ⟶ S) (g : Y ⟶ S) (h : Z ⟶ S),
  CategoryTheory.IsPullback
    (CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.fst f g)
      (CategoryTheory.Limits.pullback.fst f h) g h (CategoryTheory.Limits.pullback.snd f g)
      (CategoryTheory.Limits.pullback.snd f h) f ⋯ ⋯)
    (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g)
      (CategoryTheory.Limits.pullback.fst f h))
    (CategoryTheory.Limits.pullback.fst g h) (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Analysis.Convex.BetweenList
List.exists_map_eq_of_sorted_nonempty_iff_sbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {l : List P} (hl : l ≠ []),
  (∃ l',
      l'.SortedLT ∧
        List.map (⇑(AffineMap.lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)) ↔
    List.Sbtw R l
-- Mathlib.LinearAlgebra.Complex.Module
IsSelfAdjoint.coe_realPart : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {x : A}, IsSelfAdjoint x → ↑(realPart x) = x
-- Init.Data.String.Hashable
String.instHashablePos_1 : {s : String.Slice} → Hashable s.Pos
-- Mathlib.Topology.Algebra.ConstMulAction
isOpenMap_vadd : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] (c : G), IsOpenMap fun x => c +ᵥ x
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_map_one : ∀ {ι : Type u_2} {M : Type u_3} [inst : CommMonoid M] {m : Multiset ι}, (Multiset.map (fun x => 1) m).prod = 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKey!_modifyKey_eq_maxKey! : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α]
  [inst_5 : Inhabited α] {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β},
      Std.Internal.List.maxKey! (Std.Internal.List.Const.modifyKey k f l) = Std.Internal.List.maxKey! l
-- Lean.Elab.Parallel
/-- Runs a list of TacticM computations in parallel and returns:
* a combined cancellation hook for all tasks, and
* an iterator that yields results in original order.

The iterator runs in TacticM, and as it yields each result, it updates the TacticM state
to reflect the state when that particular task completed. This means the state is
threaded through the iteration in the order of the original list.

Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
Lean.Elab.Tactic.TacticM.parIterWithCancel : {α : Type} →
  List (Lean.Elab.Tactic.TacticM α) →
    Lean.Elab.Tactic.TacticM (BaseIO PUnit.{1} × Std.IterM Lean.Elab.Tactic.TacticM (Except Lean.Exception α))
-- Mathlib.NumberTheory.Pell
/-- If `a` is a fundamental solution, then `(a^m).y < (a^n).y` if and only if `m < n`.  -/
Pell.IsFundamental.zpow_y_lt_iff_lt : ∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → ∀ (m n : ℤ), (a ^ m).y < (a ^ n).y ↔ m < n