mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.cons.eq_1 : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G)
  (u : ℤˣ) (w : HNNExtension.NormalWord d) (h1 : w.head ∈ d.set u)
  (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'),
  HNNExtension.NormalWord.cons g u w h1 h2 = { head := g, toList := (u, w.head) :: w.toList, chain := ⋯, mem_set := ⋯ }
-- Lean.Elab.PreDefinition.Structural.SmartUnfolding
Lean.Elab.Structural.addSmartUnfoldingDef : Lean.LocalContext × Lean.LocalInstances → Lean.Elab.PreDefinition → ℕ → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorIso_hom_app_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : Cᴹᵒᵖ × Cᴹᵒᵖ),
  ((CategoryTheory.MonoidalOpposite.tensorIso C).hom.app X).unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.2.unmop X.1.unmop)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- Evaluate a TM to completion, resulting in an output list on the tape (with an indeterminate
number of blanks on the end).  -/
Turing.TM1.eval : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      [Inhabited Λ] →
        [inst : Inhabited Γ] → [Inhabited σ] → (Λ → Turing.TM1.Stmt Γ Λ σ) → List Γ → Part (Turing.ListBlank Γ)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.size_eq_match_rcc : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxc.HasSize α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α] [Std.Rxc.LawfulHasSize α],
  r.size =
    match Std.PRange.least? with
    | none => 0
    | some next => (next...=r.upper).size
-- Init.Data.ToString.Basic
instToStringOption : {α : Type u} → [ToString α] → ToString (Option α)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (n : σ →₀ ℕ) (φ ψ : MvPowerSeries σ R) [inst_1 : DecidableEq σ],
  (MvPowerSeries.coeff n) (φ * ψ) =
    ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, (MvPowerSeries.coeff p.1) φ * (MvPowerSeries.coeff p.2) ψ
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LeftExtension.IsAbsKan.hasAbsLeftKanExtension : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {t : CategoryTheory.Bicategory.LeftExtension f g} (H : t.IsAbsKan),
  CategoryTheory.Bicategory.HasAbsLeftKanExtension f g
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (f : α →* β) (h : Monotone (↑f).toFun), ⇑{ toMonoidHom := f, monotone' := h } = ⇑f
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_neg : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NormedCommRing 𝔸]
  [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (A : Matrix m m 𝔸), NormedSpace.exp (-A) = (NormedSpace.exp A)⁻¹
-- Mathlib.Order.MinMax
le_max_of_le_left : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ b → a ≤ max b c
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_univ : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f Set.univ μ ↔ MeasureTheory.Integrable f μ
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.length_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective : ∀ {σ : Type u_1} {A : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {d e : ℕ} {f : A} (hf : f ∈ 𝒜 d) {g : A} (hg : g ∈ 𝒜 e) {x : A} (hx : x = f * g),
  0 < d →
    Function.Surjective
      ⇑(Algebra.TensorProduct.lift (HomogeneousLocalization.awayMapₐ 𝒜 hg hx) (HomogeneousLocalization.awayMapₐ 𝒜 hf ⋯)
          ⋯)
-- Mathlib.Logic.Embedding.Basic
/-- The type of embeddings `α ↪ β` is equivalent to
the subtype of all injective functions `α → β`.  -/
Equiv.subtypeInjectiveEquivEmbedding : (α : Sort u_1) → (β : Sort u_2) → { f // Function.Injective f } ≃ (α ↪ β)
-- Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
/-- The uncurrying operation taking a morphism `y ⟶ C(x, z)` to a morphism `(x ⊗ y) ⟶ z`,
constructed as a morphism in `C` between internal homs.  -/
CategoryTheory.MonoidalClosed.ihomUncurry : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (x y z : C) →
        [inst_2 : CategoryTheory.Closed x] →
          [inst_3 : CategoryTheory.Closed y] →
            [inst_4 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)] →
              y ⟹ x ⟹ z ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟹ z
-- Init.Data.Nat.Lemmas
/-- A version of `Nat.sub_succ` in the form `_ - 1` instead of `Nat.pred _`.  -/
Nat.sub_succ' : ∀ (m n : ℕ), m - n.succ = m - n - 1
-- Init.Data.Range.Polymorphic.UInt
UInt32.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite UInt32
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.centerCongr.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] (e : G ≃+ H),
  AddSubgroup.centerCongr e = AddSubmonoid.centerCongr e
-- Mathlib.CategoryTheory.Sites.Point.Presheaf
CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeToPresheafFiberNatTransPointBotCoeEquivHomUnopOpObjTypeShrinkYonedaSymmShrinkYonedaObjObjEquivId : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] (X : C)
  (A : Type u_1) [inst_2 : CategoryTheory.Category.{u_2, u_1} A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, u_2, u_1} A],
  CategoryTheory.IsIso
    ((CategoryTheory.GrothendieckTopology.pointBot X).toPresheafFiberNatTrans X
      (CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.id X)))
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- Build an isomorphism in the category `Module R` from a `LinearEquiv` between `Module`s.  -/
LinearEquiv.toModuleIsoₛ : {R : Type u} →
  [inst : Semiring R] →
    {X₁ X₂ : Type v} →
      {g₁ : AddCommMonoid X₁} →
        {g₂ : AddCommMonoid X₂} →
          {m₁ : Module R X₁} → {m₂ : Module R X₂} → (X₁ ≃ₗ[R] X₂) → (SemimoduleCat.of R X₁ ≅ SemimoduleCat.of R X₂)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsAddMonHom.instNormalOfIsCommAddMonObjOfMono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H] {φ : H ⟶ G}
  [inst_4 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj G] [CategoryTheory.IsAddMonHom φ]
  [CategoryTheory.Mono φ], CategoryTheory.IsAddMonHom.Normal φ
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
totallyBounded_iff_subset_finite_iUnion_nhds_one : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {s : Set α},
  TotallyBounded s ↔ ∀ U ∈ nhds 1, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y • U
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If a functor creates coequalizers and the appropriate coproducts, it creates colimits.

We additionally require the rather strong condition that the functor reflects isomorphisms. It is
unclear whether the statement remains true without this condition. There are various definitions of
"creating colimits" in the literature, and whether or not the condition can be dropped seems to
depend on the specific definition that is used.  -/
CategoryTheory.Limits.createsColimitsOfShapeOfCreatesCoequalizersAndCoproducts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        {D : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
            [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete J) D] →
              [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) D] →
                [CategoryTheory.Limits.HasCoequalizers D] →
                  (G : CategoryTheory.Functor C D) →
                    [G.ReflectsIsomorphisms] →
                      [CategoryTheory.CreatesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] →
                        [CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete J) G] →
                          [CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2)))
                                G] →
                            CategoryTheory.CreatesColimitsOfShape J G
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getDivThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.tensorAddUnit_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.AddGrp C)).X =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphismClass.exists_map_eq_of_map_le : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : Preorder α} {inst_1 : Preorder β}
  {inst_2 : FunLike F α β} [self : PseudoEpimorphismClass F α β] (f : F) ⦃a : α⦄ ⦃b : β⦄, f a ≤ b → ∃ c, a ≤ c ∧ f c = b
-- Mathlib.Geometry.Manifold.Algebra.Monoid
mdifferentiableAt_mul_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} {G : Type u_4}
  [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I 1 G] {a b : G},
  (MDiffAt fun x => a * x) b
-- Init.Data.String.TakeDrop
String.Internal.dropImpl : String → ℕ → String
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If a category `C` has 0-morphisms, there is a canonical inclusion from the first component `X`
into any product of objects `X ⨯ Y`.  -/
CategoryTheory.Limits.prod.inl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) → [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y] → X ⟶ X ⨯ Y
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_mul_rank_top : ∀ {E : Type v} [inst : Field E] {A B : Subfield E}, A ≤ B → A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Iic_pred_eq_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : PredOrder α] [NoMinOrder α]
  (b : α), Finset.Iic (Order.pred b) = Finset.Iio b
-- Mathlib.Data.Rel
SetRel.preimage_eq_image : ∀ {α : Type u_1} {s : Set α} {R : SetRel α α} [R.IsSymm], R.preimage s = R.image s
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_add_bmod : ∀ {x : ℤ} {n : ℕ} {y : ℤ}, (x.bmod n + y).bmod n = (x + y).bmod n
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_comp_cyclesIso₀_hom : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap f φ 0) (groupHomology.cyclesIso₀ B).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).hom (Rep.Hom.toModuleCatHom φ)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_eq_top : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R}, x.orderTop = ⊤ ↔ x = 0
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.toEquiv_injective : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β],
  Function.Injective IsometryEquiv.toEquiv
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_liftWith_StateT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ α : Type u}
  {post : α → σ → Pred} {epost : EPred} {s : σ} (f : ({β : Type u} → StateT σ m β → m (β × σ)) → m α),
  Std.Internal.Do.wp (MonadControl.liftWith f) post epost s =
    Std.Internal.Do.wp ((fun a => (a, s)) <$> f fun {β} x => x.run s)
      (fun x =>
        match x with
        | (a, s) => post a s)
      epost
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfLocalizations_right_inv : ∀ {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) (k : S.LocalizationMap P),
  f.ofAddEquivOfLocalizations (f.addEquivOfLocalizations k) = k
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- In this file we normalise the measure on `ℝ / ℤ` to have total volume 1.  -/
instMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle
-- Aesop.RuleSet.Filter
/-- Returns the identifier of the local norm simp rule matched by `f`, if any.
 -/
Aesop.RuleFilter.matchesLocalNormSimpRule? : Aesop.RuleFilter → Option Lean.Name
-- Mathlib.Order.Filter.Defs
Filter.mem_principal : ∀ {α : Type u_1} {s t : Set α}, s ∈ Filter.principal t ↔ t ⊆ s
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.instIsProbabilityMeasureBindCoeKernelOfIsMarkovKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.IsMarkovKernel κ],
  MeasureTheory.IsProbabilityMeasure (μ.bind ⇑κ)
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- The real exponential function tends to `0` at `-∞` or, equivalently, `exp(-x)` tends to `0`
at `+∞`  -/
Real.tendsto_exp_neg_atTop_nhds_zero : Filter.Tendsto (fun x => Real.exp (-x)) Filter.atTop (nhds 0)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_filter_eq_size_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool},
  (Std.ExtDHashMap.filter f m).size = m.size ↔
    ∀ (a : α) (h : a ∈ m), f (m.getKey a h) (Std.ExtDHashMap.Const.get m a h) = true
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z : C} [inst_3 : HasDerivedCategory C] {a b : ℕ}
  (α : CategoryTheory.Abelian.Ext X Y a) (β : CategoryTheory.Abelian.Ext Y Z b) {c : ℕ} (h : a + b = c),
  (α.comp β h).hom = α.hom.comp β.hom ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withTopCongr_toEquiv : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β), ↑e.withTopCongr = (↑e).withTopCongr
-- Mathlib.RingTheory.Spectrum.Prime.Noetherian
IsArtinianRing.instDiscreteTopologyPrimeSpectrum : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R], DiscreteTopology (PrimeSpectrum R)
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.fibres_compl_eq_iUnion : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} (π : T → S × Option X) (σ : Option X → S → T),
  (∀ (x : Option X) (s : S), (π (σ x s)).2 = x) →
    (InternalProjectivityProof.fibres✝ π σ)ᶜ = ⋃ i, (Set.range (σ (some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {↑i}
-- Mathlib.Topology.UniformSpace.Equicontinuity
Filter.HasBasis.uniformEquicontinuousOn_iff : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {κ₁ : Type u_11}
  {κ₂ : Type u_12} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set (β × β)} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → β → α}
  {S : Set β},
  (uniformity β ⊓ Filter.principal (S ×ˢ S)).HasBasis p₁ s₁ →
    (uniformity α).HasBasis p₂ s₂ →
      (UniformEquicontinuousOn F S ↔
        ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.comp_eq_of_monotoneOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {β : Type u_3}
  [inst_2 : LinearOrder β] (f : α → E) {t : Set β} (φ : β → α),
  MonotoneOn φ t → eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)
-- Init.Data.Option.Lemmas
Option.map_inj_right : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {o o' : Option α},
  (∀ (x y : α), f x = f y → x = y) → (Option.map f o = Option.map f o' ↔ o = o')
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.alterₘ.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.μ_apply_single_single : ∀ {G : Type v} [inst : Monoid G] {X Y : Action (Type w) G} {k : Type u} [inst_1 : CommSemiring k] (x : X.V) (y : Y.V)
  (r s : k),
  (Representation.LinearizeMonoidal.μ X Y) (MonoidAlgebra.single x r ⊗ₜ[k] MonoidAlgebra.single y s) =
    MonoidAlgebra.single (x, y) (r * s)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂), S₁.Exact → S₂.Exact
-- Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
/-- The **Erdős–Ginzburg–Ziv theorem** for `ℤ`.

Any sequence of at least `2 * n - 1` elements of `ℤ` contains a subsequence of `n` elements whose
sum is divisible by `n`.  -/
Int.erdos_ginzburg_ziv : ∀ {ι : Type u_1} {n : ℕ} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ s.card → ∃ t ⊆ s, t.card = n ∧ ↑n ∣ ∑ i ∈ t, a i
-- Mathlib.Order.Category.HeytAlg
/-- The underlying Heyting algebra.  -/
HeytAlg.carrier : HeytAlg → Type u_1
-- Mathlib.Control.Fold
Traversable.foldMap : {t : Type u → Type u} → [Traversable t] → {α ω : Type u} → [One ω] → [Mul ω] → (α → ω) → t α → ω
-- Lean.Meta.Tactic.Grind.ForallProp
_private.Lean.Meta.Tactic.Grind.ForallProp.0.Lean.Meta.Grind.propagateForallPropUp.propagateImpliesUp : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.StainData.mk.sizeOf_spec : ∀ (stained : Mathlib.Linter.Flexible.Stained✝) (stx : Lean.Syntax) (ci : Lean.Elab.ContextInfo)
  (mctx : Lean.MetavarContext) (goals : List Lean.MVarId),
  sizeOf { stained := stained, stx := stx, ci := ci, mctx := mctx, goals := goals } =
    1 + sizeOf stained + sizeOf stx + sizeOf ci + sizeOf mctx + sizeOf goals
-- Mathlib.Data.Set.Basic
Set.monotone_powerset : ∀ {α : Type u}, Monotone Set.powerset
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_comp_map : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) {U V : TopologicalSpace.Opens ↑Z} (i : U ⟶ V),
  (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g)).map i =
    (TopologicalSpace.Opens.map f).map ((TopologicalSpace.Opens.map g).map i)
-- Init.Data.UInt.Bitwise
UInt64.toFin_shiftRight : ∀ (a b : UInt64), b < 64 → (a >>> b).toFin = a.toFin >>> b.toFin
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_range_eq_iSup : ∀ {α : Type u} [inst : Semiring α] {ι : Type u_1} (x : ι → α), Ideal.span (Set.range x) = ⨆ i, Ideal.span {x i}
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.pi_empty : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → MulOneClass (M i)] (H : (i : ι) → Submonoid (M i)),
  Submonoid.pi ∅ H = ⊤
-- Mathlib.Algebra.Algebra.Unitization
/-- See note [partially-applied ext lemmas]  -/
Unitization.algHom_ext' : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] {C : Type u_5} [inst_5 : Semiring C]
  [inst_6 : Algebra R C] {φ ψ : Unitization R A →ₐ[R] C},
  (↑φ).comp (Unitization.inrNonUnitalAlgHom R A) = (↑ψ).comp (Unitization.inrNonUnitalAlgHom R A) → φ = ψ
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.arrow_mk_iso_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso]
  {W X Y Z : C} {f : W ⟶ X} {g : Y ⟶ Z} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g), P f ↔ P g
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h : t.WF) {a : α} {h' : (t.get? a).isSome = true}, (t.get? a).get h' = t.get a ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.univ_div_univ : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionMonoid α] [inst_2 : Fintype α],
  Finset.univ / Finset.univ = Finset.univ
-- Mathlib.Order.Filter.Pointwise
Filter.HasBasis.mul : ∀ {α : Type u_2} [inst : Mul α] {f g : Filter α} {ιf : Type u_7} {ιg : Type u_8} {pf : ιf → Prop} {sf : ιf → Set α}
  {pg : ιg → Prop} {sg : ιg → Set α},
  f.HasBasis pf sf → g.HasBasis pg sg → (f * g).HasBasis (fun i => pf i.1 ∧ pg i.2) fun i => sf i.1 * sg i.2
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.mkCommaMorphism_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D} (η : F ⟶ G),
  (CategoryTheory.WithTerminal.mkCommaMorphism η).right = η.app CategoryTheory.WithTerminal.star
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_elem : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  {A : X → Matrix m n R}, Continuous A → ∀ (i : m) (j : n), Continuous fun x => A x i j
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
/-- A morphism of schemes is dominant if the underlying map has dense range.  -/
AlgebraicGeometry.IsDominant : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.min_apply : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {e₁ e₂ : (a : α) × β a} {f : (a : α) × β a → (a : α) × β a},
  compare e₁.fst e₂.fst = compare (f e₁).fst (f e₂).fst → f e₁ ⊓ f e₂ = f (e₁ ⊓ e₂)
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- The `AddSubmonoid` generated by a set  -/
AddSubmonoid.closure : {M : Type u_1} → [inst : AddZeroClass M] → Set M → AddSubmonoid M
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.π_comp_hom_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  {s t : CategoryTheory.Limits.Cofork f g} (f_1 : s ⟶ t) {Z : C} (h : t.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.π (CategoryTheory.CategoryStruct.comp f_1.hom h) =
    CategoryTheory.CategoryStruct.comp t.π h