mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.BilinearMap
/-- Composing a semilinear map `M → N` and a semilinear map `N → P` to form a semilinear map
`M → P` is itself a linear map.  -/
LinearMap.lcompₛₗ : {R : Type u_14} →
  {R₂ : Type u_15} →
    {R₃ : Type u_16} →
      (R₅ : Type u_18) →
        {M : Type u_19} →
          {N : Type u_20} →
            (P : Type u_21) →
              [inst : Semiring R] →
                [inst_1 : Semiring R₂] →
                  [inst_2 : Semiring R₃] →
                    [inst_3 : Semiring R₅] →
                      {σ₁₂ : R →+* R₂} →
                        (σ₂₃ : R₂ →+* R₃) →
                          {σ₁₃ : R →+* R₃} →
                            [inst_4 : AddCommMonoid M] →
                              [inst_5 : AddCommMonoid N] →
                                [inst_6 : AddCommMonoid P] →
                                  [inst_7 : Module R M] →
                                    [inst_8 : Module R₂ N] →
                                      [inst_9 : Module R₃ P] →
                                        [inst_10 : Module R₅ P] →
                                          [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                            [inst_12 : SMulCommClass R₃ R₅ P] →
                                              (M →ₛₗ[σ₁₂] N) → (N →ₛₗ[σ₂₃] P) →ₗ[R₅] M →ₛₗ[σ₁₃] P
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.eqToHom_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y} (h : f = g),
  (CategoryTheory.eqToHom h).hom = CategoryTheory.eqToHom ⋯
-- Mathlib.SetTheory.Ordinal.Basic
/-- `Quotient.inductionOn₃` specialized to ordinals.

Not to be confused with well-founded induction `WellFoundedLT.induction`.  -/
Ordinal.inductionOn₃ : ∀ {motive : Ordinal.{u_1} → Ordinal.{u_2} → Ordinal.{u_3} → Prop} (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_2})
  (o₃ : Ordinal.{u_3}),
  (∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r] (β : Type u_2) (s : β → β → Prop)
      [inst_1 : IsWellOrder β s] (γ : Type u_3) (t : γ → γ → Prop) [inst_2 : IsWellOrder γ t],
      motive (Ordinal.type r) (Ordinal.type s) (Ordinal.type t)) →
    motive o₁ o₂ o₃
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.range_asFiberHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  Set.range ⇑(AlgebraicGeometry.Scheme.Hom.asFiberHom f x) = {AlgebraicGeometry.Scheme.Hom.asFiber f x}
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.comp_eq_nil_iff : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} {p : Quiver.Path a b} {q : Quiver.Path b a},
  p.comp q = Quiver.Path.nil ↔ p.length = 0 ∧ q.length = 0
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- `LinearMap.bound_of_ball_bound'` is a version of this lemma over a field satisfying `RCLike`
that produces a concrete bound.
 -/
LinearMap.bound_of_ball_bound : ∀ {𝕜 : Type u_1} {E : Type u_5} {Fₗ : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ] {r : ℝ},
  0 < r → ∀ (c : ℝ) (f : E →ₗ[𝕜] Fₗ), (∀ z ∈ Metric.ball 0 r, ‖f z‖ ≤ c) → ∃ C, ∀ (z : E), ‖f z‖ ≤ C * ‖z‖
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.map_comap_eq_self_of_surjective : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] {f : L →ₐ[K] L'},
  Function.Surjective ⇑f → ∀ (S : IntermediateField K L'), IntermediateField.map f (IntermediateField.comap f S) = S
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
mul_sup₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : SemilatticeSup G₀] [PosMulReflectLT G₀] {c : G₀},
  0 ≤ c → ∀ (a b : G₀), c * (a ⊔ b) = c * a ⊔ c * b
-- Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
ZMod.gauss_lemma_aux : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {a : ℤ},
  ↑a ≠ 0 → ↑a ^ (p / 2) = ↑((-1) ^ {x ∈ Finset.Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}.card)
-- Batteries.Data.List.Lemmas
List.getElem_idxOf_eq_idxOfNth_add : ∀ {α : Type u_1} {n : ℕ} {x : α} {s : ℕ} {xs : List α} [inst : BEq α] {h : n < (List.idxsOf x xs s).length},
  (List.idxsOf x xs s)[n] = List.idxOfNth x xs n + s
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
AddAction.stabilizerEquivStabilizer_compTriple : ∀ {G : Type u_3} [inst : AddGroup G] {α : Type u_4} [inst_1 : AddAction G α] {g h k : G} {a b c : α} {hg : b = g +ᵥ a}
  {hh : c = h +ᵥ b} {hk : c = k +ᵥ a},
  k = h + g →
    CompTriple ⇑(AddAction.stabilizerEquivStabilizer hg) ⇑(AddAction.stabilizerEquivStabilizer hh)
      ⇑(AddAction.stabilizerEquivStabilizer hk)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraFunctorOfMonadHomComp_hom_app_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ T₃ : CategoryTheory.Monad C} (f : T₁ ⟶ T₂)
  (g : T₂ ⟶ T₃) (X : T₃.Algebra),
  ((CategoryTheory.Monad.algebraFunctorOfMonadHomComp f g).hom.app X).f =
    (CategoryTheory.Iso.refl
        ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.comp f g)).obj X).A).hom
-- Mathlib.GroupTheory.GroupAction.Jordan
/-- A criterion due to Jordan for being 2-preprimitive (Wielandt, 13.1)  -/
MulAction.IsPreprimitive.is_two_preprimitive : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  MulAction.IsPreprimitive G α →
    ∀ {s : Set α} {n : ℕ},
      s.ncard = n + 1 →
        n + 2 < Nat.card α →
          MulAction.IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
            MulAction.IsMultiplyPreprimitive G α 2
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_withBot_some_comp : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {s : AddMonoidAlgebra R A},
  s.coeff.support.Nonempty → AddMonoidAlgebra.supDegree (WithBot.some ∘ D) s = ↑(AddMonoidAlgebra.supDegree D s)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.interface.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.interface = 1
-- Mathlib.Data.Multiset.NatAntidiagonal
Multiset.Nat.antidiagonal_succ' : ∀ {n : ℕ},
  Multiset.Nat.antidiagonal (n + 1) = (n + 1, 0) ::ₘ Multiset.map (Prod.map id Nat.succ) (Multiset.Nat.antidiagonal n)
-- Init.Data.Vector.Monadic
Vector.forM_congr : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} [inst : Monad m] {as bs : Vector α n},
  as = bs → ∀ {f : α → m PUnit.{u_1 + 1}}, forM as f = forM bs f
-- Mathlib.Data.Rat.Cast.Defs
NNRat.cast_mul_of_ne_zero : ∀ {α : Type u_3} [inst : DivisionSemiring α] {q r : ℚ≥0}, ↑q.den ≠ 0 → ↑r.den ≠ 0 → ↑(q * r) = ↑q * ↑r
-- Init.Data.UInt.Lemmas
UInt64.sub_self : ∀ (a : UInt64), a - a = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageMap.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {f g : CategoryTheory.Arrow C}
  {inst_1 : CategoryTheory.Limits.HasImage f.hom} {inst_2 : CategoryTheory.Limits.HasImage g.hom} {sq : f ⟶ g}
  {map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom}
  {map_ι :
    autoParam
      (CategoryTheory.CategoryStruct.comp map (CategoryTheory.Limits.image.ι g.hom) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq))
      CategoryTheory.Limits.ImageMap.map_ι._autoParam}
  {map_1 : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom}
  {map_ι_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp map_1 (CategoryTheory.Limits.image.ι g.hom) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq))
      CategoryTheory.Limits.ImageMap.map_ι._autoParam},
  { map := map, map_ι := map_ι } = { map := map_1, map_ι := map_ι_1 } → map = map_1
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.instCoeSortType : {R : Type u} → [inst : CommRing R] → CoeSort (CommAlgCat R) (Type v)
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
_private.Mathlib.GroupTheory.FreeGroup.NielsenSchreier.0.IsFreeGroupoid.SpanningTree.homOfPath.match_1.eq_2 : ∀ {G : Type u_1} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)]
  (motive :
    (x : G) →
      Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) x → Sort u_2)
  (x b : WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)
  (p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) b)
  (f : b ⟶ x)
  (h_1 :
    Unit →
      motive (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) Quiver.Path.nil)
  (h_2 :
    (x b : WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T) →
      (p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) b) →
        (f : b ⟶ x) → motive x (p.cons f)),
  (match x, p.cons f with
    | .(Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)), Quiver.Path.nil =>
      h_1 ()
    | x, p.cons f => h_2 x b p f) =
    h_2 x b p f
-- Mathlib.Topology.Algebra.Module.LocallyConvex
Topology.IsInducing.locallyConvexSpace : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [LocallyConvexSpace 𝕜 F] [inst_8 : TopologicalSpace E] {f : E →ₗ[𝕜] F},
  Topology.IsInducing ⇑f → LocallyConvexSpace 𝕜 E
-- Mathlib.Order.CompleteLattice.Basic
iSup_neg : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : p → α}, ¬p → ⨆ (h : p), f h = ⊥
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_dvd_prod_of_dvd : ∀ {M : Type u_5} {N : Type u_6} [inst : CommMonoid N] {S : Multiset M} (g1 g2 : M → N),
  (∀ a ∈ S, g1 a ∣ g2 a) → (Multiset.map g1 S).prod ∣ (Multiset.map g2 S).prod
-- Mathlib.Dynamics.OmegaLimit
isClosed_omegaLimit : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α),
  IsClosed (omegaLimit f ϕ s)
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.lipschitzWith_eval : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : PseudoEMetricSpace β] [inst_1 : Finite ↑𝔖] {x : α},
  x ∈ ⋃₀ 𝔖 → LipschitzWith 1 fun f => (UniformOnFun.toFun 𝔖) f x
-- Mathlib.Data.Matrix.Diagonal
Matrix.natCast_apply : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddMonoidWithOne α] {i j : n} {d : ℕ},
  ↑d i j = ↑(if i = j then d else 0)
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalWhiskerRight_nil : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (α : f ≅ g) (h : b ⟶ c),
  CategoryTheory.Bicategory.whiskerRight α.hom h = CategoryTheory.Bicategory.whiskerRight α.hom h
-- Std.Net.Addr
Std.Net.SocketAddress.v4.injEq : ∀ (addr addr_1 : Std.Net.SocketAddressV4),
  (Std.Net.SocketAddress.v4 addr = Std.Net.SocketAddress.v4 addr_1) = (addr = addr_1)
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `hasFDerivWithinAt_const_add_iff`. -/
HasFDerivWithinAt.const_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} (c : F), HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => c + f x) f' s x
-- Mathlib.Data.Finset.Max
Finset.notMem_of_coe_lt_min : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α} {s : Finset α}, ↑a < s.min → a ∉ s
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.add_le_add_left : ∀ {α : Type u_1} [inst : CommSemiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {b c : α},
  b ≤ c → ∀ (a : α), b + a ≤ c + a
-- Lean.CompactedRegion
/-- Whether the region's buffer is backed by a memory mapping of its file.  -/
Lean.CompactedRegion.isMemoryMapped : Lean.CompactedRegion → Bool
-- Mathlib.FieldTheory.SeparableClosure
/-- If `E` and `K` are isomorphic as `F`-algebras, then they have the same
inseparable degree over `F`.  -/
Field.lift_insepDegree_eq_of_equiv : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E ≃ₐ[F] K),
  Cardinal.lift.{w, v} (Field.insepDegree F E) = Cardinal.lift.{v, w} (Field.insepDegree F K)
-- Mathlib.Data.Countable.Basic
nonempty_embedding_nat : ∀ (α : Sort u_1) [Countable α], Nonempty (α ↪ ℕ)
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.isoMk_inv_hom : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A}
  (iso : (a : A) → F.functor a ≅ G.functor a)
  (comm :
    ∀ (n a a' : A) (ha' : n + a = a'),
      CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (iso a).hom =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (iso a').hom (CategoryTheory.shiftFunctor D n))
          (G.shiftIso n a a' ha').hom)
  (a : A), (CategoryTheory.SingleFunctors.isoMk iso comm).inv.hom a = (iso a).inv
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.supp_map : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F],
  MvQPF.IsUniform →
    ∀ {α β : TypeVec.{u} n} (g : α.Arrow β) (x : F α) (i : Fin2 n),
      MvFunctor.supp (MvFunctor.map g x) i = g i '' MvFunctor.supp x i
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_mul_add_fmod : ∀ (a b : ℤ), a.fdiv b * b + a.fmod b = a
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The additive map `Cochain K L n →+ Cochain (K⟦a⟧) (L⟦a⟧) n`.  -/
CochainComplex.HomComplex.Cochain.shiftAddHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K L : CochainComplex C ℤ) →
        (n a : ℤ) →
          CochainComplex.HomComplex.Cochain K L n →+
            CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K)
              ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearMap.mem_fixedSubmodule_iff : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_3} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {f : V →ₗ[R] V}
  {v : V}, v ∈ f.fixedSubmodule ↔ f v = v
-- Mathlib.GroupTheory.GroupAction.Defs
FixedPoints.mem_submonoid : ∀ (M : Type u) (α : Type v) [inst : Monoid M] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction M α] (a : α),
  a ∈ FixedPoints.submonoid M α ↔ ∀ (m : M), m • a = a
-- Aesop.Tree.Data
Aesop.Rapp.setOriginalSubgoals : Array Lean.MVarId → Aesop.Rapp → Aesop.Rapp
-- Mathlib.Combinatorics.SetFamily.HarrisKleitman
/-- **Harris-Kleitman inequality**: Lower sets and upper sets of finsets anticorrelate.  -/
IsLowerSet.card_inter_le_finset : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 ℬ : Finset (Finset α)} [inst_1 : Fintype α],
  IsLowerSet ↑𝒜 → IsUpperSet ↑ℬ → 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card ≤ 𝒜.card * ℬ.card
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
CompactConvergenceCLM.instT2Space : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F] [T2Space F],
  T2Space (CompactConvergenceCLM σ E F)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ofList_equiv_foldl : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {l : List (α × β)},
  (Std.TreeMap.ofList l cmp).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) ∅ l)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- Let `f` be a function defined on a finite-dimensional real normed space. If `f` is `C¹`-smooth
on a convex set `s`, then the Hausdorff dimension of `f '' s` is less than or equal to the Hausdorff
dimension of `s`.

TODO: do we actually need `Convex ℝ s`?  -/
ContDiffOn.dimH_image_le : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s t : Set E},
  ContDiffOn ℝ 1 f s → Convex ℝ s → t ⊆ s → dimH (f '' t) ≤ dimH t
-- Lean.Meta.Tactic.FunIndCollect
/-- only function name and relevant arguments  -/
Lean.Meta.FunInd.SeenCalls.seen : Lean.Meta.FunInd.SeenCalls → Std.HashSet (Lean.Name × Array Lean.Expr)
-- Init.Data.List.Nat.Find
List.find?_eq_some_iff_getElem : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {b : α},
  List.find? p xs = some b ↔
    p b = true ∧ ∃ i, ∃ (h : i < xs.length), xs[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p xs[j]) = true
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.hom_ofHom : ∀ {R S : Type u} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S), RingCat.Hom.hom (RingCat.ofHom f) = f
-- Mathlib.Data.List.Map2
List.zipLeft'_cons_cons : ∀ {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β),
  (a :: as).zipLeft' (b :: bs) =
    have r := as.zipLeft' bs;
    ((a, some b) :: r.1, r.2)
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.hasse_preconnected_of_succ : ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α], (SimpleGraph.hasse α).Preconnected
-- Mathlib.Topology.Algebra.Group.Extension
TopologicalGroup.IsSES.isOpenQuotientMap : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C},
  TopologicalGroup.IsSES φ ψ → IsOpenQuotientMap ⇑ψ
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasFDerivWithinAt_iff_hasDerivWithinAt`.

---

Expressing `HasFDerivWithinAt f f' s x` in terms of `HasDerivWithinAt`  -/
HasFDerivWithinAt.hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} [inst_4 : ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F},
  HasFDerivWithinAt f f' s x → HasDerivWithinAt f (f' 1) s x
-- Mathlib.Analysis.Analytic.Composition
/-- If two functions `g` and `f` are analytic respectively on `s.image f` and `s`, then `g ∘ f` is
analytic on `s`.  -/
AnalyticOnNhd.comp' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {g : F → G} {f : E → F},
  AnalyticOnNhd 𝕜 g (f '' s) → AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (g ∘ f) s
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.pair_inj : ∀ {x y x' y' : ZFSet.{u_1}}, x.pair y = x'.pair y' ↔ x = x' ∧ y = y'
-- Mathlib.Topology.CompactOpen
/-- Any pair of homeomorphisms `X ≃ₜ Z` and `Y ≃ₜ T` gives rise to a homeomorphism
`C(X, Y) ≃ₜ C(Z, T)`.  -/
Homeomorph.arrowCongr : {X : Type u_2} →
  {Y : Type u_3} →
    {Z : Type u_4} →
      {T : Type u_5} →
        [inst : TopologicalSpace X] →
          [inst_1 : TopologicalSpace Y] →
            [inst_2 : TopologicalSpace Z] → [inst_3 : TopologicalSpace T] → X ≃ₜ Z → Y ≃ₜ T → C(X, Y) ≃ₜ C(Z, T)
-- Lean.Meta.CtorRecognizer
/-- Similar to `isConstructorApp?`, but uses `whnf`.
It also uses `isOffset?` for `Nat`.

See also `Lean.Meta.constructorApp'?`.
 -/
Lean.Meta.isConstructorApp'? : Lean.Expr → Lean.MetaM (Option Lean.ConstructorVal)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.discr_ne_zero_iff_roots_ne : ∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K} {x y z : K},
  P.a ≠ 0 → (Cubic.map φ P).roots = {x, y, z} → (P.discr ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z)
-- Mathlib.Topology.FiberBundle.Basic
instMemTrivializationAtlasTrivializationAt : ∀ {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {E : B → Type u_5}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
  [inst_4 : FiberBundle F E] (b : B), MemTrivializationAtlas (trivializationAt F E b)
-- Mathlib.Algebra.Module.Bimodule
/-- A constructor for a subbimodule which demands closure under the two sets of scalars
individually, rather than jointly via their tensor product.

Note that `R` plays no role but it is convenient to make this generalisation to support the cases
`R = ℕ` and `R = ℤ` which both show up naturally. See also `Subbimodule.baseChange`.  -/
Subbimodule.mk : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {M : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : Semiring A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Module A M] →
                    [inst_6 : Module B M] →
                      [inst_7 : Algebra R A] →
                        [inst_8 : Algebra R B] →
                          [inst_9 : IsScalarTower R A M] →
                            [inst_10 : IsScalarTower R B M] →
                              [inst_11 : SMulCommClass A B M] →
                                (p : AddSubmonoid M) →
                                  (∀ (a : A) {m : M}, m ∈ p → a • m ∈ p) →
                                    (∀ (b : B) {m : M}, m ∈ p → b • m ∈ p) → Submodule (TensorProduct R A B) M
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isLocalization_stalk' : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (y : PrimeSpectrum ↑(X.presheaf.obj (Opposite.op U))),
  hU.fromSpec y ∈ U → IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec y))) y.asIdeal
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAt.prod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x₀ : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x₀) → ContMDiffAt I' I n (fun x => ∏ i ∈ t, f i x) x₀
-- Init.Data.SInt.Bitwise
Int8.ofBitVec_intMin : Int8.ofBitVec (BitVec.intMin 8) = Int8.minValue
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
Algebra.TensorProduct.map_surjective : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A : Type u_6}
  {B : Type u_7} {C : Type u_8} {D : Type u_9} [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Ring C] [inst_6 : Ring D]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : Algebra R C] [inst_10 : Algebra R D] [inst_11 : Algebra S A]
  [inst_12 : Algebra S B] [inst_13 : IsScalarTower R S A] [inst_14 : IsScalarTower R S B] (f : A →ₐ[S] B)
  (g : C →ₐ[R] D),
  Function.Surjective ⇑f → Function.Surjective ⇑g → Function.Surjective ⇑(Algebra.TensorProduct.map f g)
-- Mathlib.Data.EReal.Operations
/-- If `a < -b` then `b < -a` on `EReal`.  -/
EReal.lt_neg_of_lt_neg : ∀ {a b : EReal}, a < -b → b < -a