mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.LocallyConvex.Basic
balanced_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E], Balanced 𝕜 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_filter_key : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {f : α → Bool} {k : α},
  (Std.ExtDHashMap.filter (fun k x => f k) m).getKey! k = (Option.filter f (m.getKey? k)).get!
-- Aesop.Frontend.Tactic
_private.Aesop.Frontend.Tactic.0.Aesop.Frontend.elabOptions.unsafe_impl_2 : Lean.Syntax → Lean.Elab.TermElabM Aesop.Options
-- Mathlib.Order.Types.Arithmetic
OrderType.instAdd : Add OrderType.{u}
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.preimage_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C},
  hF.preimage (CategoryTheory.CategoryStruct.id (F.obj X)) = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Order.Group.Abs
eq_of_abs_sub_lt_all : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {x y : G},
  (∀ ε > 0, |x - y| < ε) → x = y
-- Mathlib.Topology.Connected.Basic
/-- A connected space is a nonempty one where there is no non-trivial open partition.  -/
ConnectedSpace : (α : Type u) → [TopologicalSpace α] → Prop
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WOppSide.map : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : CommRing R]
  [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V]
  [inst_5 : AddTorsor V P] [inst_6 : AddCommGroup V'] [inst_7 : Module R V'] [inst_8 : AddTorsor V' P']
  {s : AffineSubspace R P} {x y : P}, s.WOppSide x y → ∀ (f : P →ᵃ[R] P'), (AffineSubspace.map f s).WOppSide (f x) (f y)
-- Mathlib.Analysis.CStarAlgebra.Projection
isStarProjection_iff_spectrum_subset_and_isStarNormal : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {p : A},
  IsStarProjection p ↔ spectrum ℂ p ⊆ {0, 1} ∧ IsStarNormal p
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.func.injEq : ∀ {L : FirstOrder.Language} {α : Type u'} {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α) (l_1 : ℕ)
  (_f_1 : L.Functions l_1) (_ts_1 : Fin l_1 → L.Term α),
  (FirstOrder.Language.func _f _ts = FirstOrder.Language.func _f_1 _ts_1) = (l = l_1 ∧ _f ≍ _f_1 ∧ _ts ≍ _ts_1)
-- Lean.Message
/-- Moves `unreported` messages to `reported`.  -/
Lean.MessageLog.markAllReported : Lean.MessageLog → Lean.MessageLog
-- Mathlib.Data.Finset.Sort
Finset.sort_perm_toList : ∀ {α : Type u_1} (s : Finset α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], (s.sort r).Perm s.toList
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.toWeightBasis_repr_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsRootSystem] (i : ↥b.support), b.toWeightBasis.repr (P.root ↑i) = fun₀ | i => 1
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_sum_eq_of_disjoint : ∀ {R : Type u} {S : Type v} [inst : Semiring R] (f : S → Polynomial R) (s : Finset S),
  {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Function.onFun Ne (Polynomial.degree ∘ f)) →
    (s.sum f).degree = s.sup fun i => (f i).degree
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.withAntiquot.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {f : Option β → Option β},
  (m.alter k f).getKey? k' = if (k == k') = true then if (f m[k]?).isSome = true then some k else none else m.getKey? k'
-- Lean.Elab.Tactic.Basic
/-- Add the given goals to the front of the current list of goals.  -/
Lean.Elab.Tactic.pushGoals : List Lean.MVarId → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_star : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], (star a).imJ = -a.imJ
-- Init.Data.Int.Gcd
Int.gcd_mul_left_sub_left : ∀ (m n k : ℤ), (m * k - n).gcd m = n.gcd m
-- Std.Http.Data.Method
/-- Update a redirect reference resource.
Source: https://www.rfc-editor.org/rfc/rfc4437#section-7
 -/
Std.Http.Method.updateredirectref : Std.Http.Method
-- Mathlib.Logic.Equiv.Defs
Function.swap_bijective : ∀ {α : Sort u_1} {β : Sort u_2} {γ : α → β → Sort u_3}, Function.Bijective Function.swap
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.mk.inj : ∀ {const : ℤ} {coeffs : Lean.Omega.Coeffs} {const_1 : ℤ} {coeffs_1 : Lean.Omega.Coeffs},
  { const := const, coeffs := coeffs } = { const := const_1, coeffs := coeffs_1 } → const = const_1 ∧ coeffs = coeffs_1
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_add : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : Add α] (A : Matrix n l α)
  (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (A' : Matrix n l α) (B' : Matrix n m α) (C' : Matrix o l α)
  (D' : Matrix o m α),
  Matrix.fromBlocks A B C D + Matrix.fromBlocks A' B' C' D' = Matrix.fromBlocks (A + A') (B + B') (C + C') (D + D')
-- Mathlib.MeasureTheory.Integral.CircleTransform
/-- The derivative of a `circleTransform` is locally bounded.  -/
Complex.circleTransformDeriv_bound : ∀ {R : ℝ},
  0 < R →
    ∀ {z x : ℂ} {f : ℂ → ℂ},
      x ∈ Metric.ball z R →
        ContinuousOn f (Metric.sphere z R) →
          ∃ B ε,
            0 < ε ∧
              Metric.ball x ε ⊆ Metric.ball z R ∧
                ∀ (t : ℝ), ∀ y ∈ Metric.ball x ε, ‖Complex.circleTransformDeriv R z y f t‖ ≤ B
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.rad : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (α : E) (n : ℕ),
  n ≠ 0 → IsSolvableByRad F (α ^ n) → IsSolvableByRad F α
-- Mathlib.Algebra.Group.Units.Hom
/-- If `f` is a homomorphism from a group `G` to a monoid `M`,
then its image lies in the units of `M`,
and `f.toHomUnits` is the corresponding monoid homomorphism from `G` to `Mˣ`.  -/
MonoidHom.toHomUnits : {G : Type u_1} → {M : Type u_2} → [inst : Group G] → [inst_1 : Monoid M] → (G →* M) → G →* Mˣ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
/-- Predicate stating that the first non-zero exponent is negative.  -/
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg : Tactic.ComputeAsymptotics.UnitMonomial → Prop
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Option.getD.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match none with
    | some x => h_1 x
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Order.SuccPred
Order.lt_add_one_iff_of_not_isMax' : ∀ {α : Type u_1} {x y : α} [inst : LinearOrder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α],
  ¬IsMax x → (x < y + 1 ↔ x ≤ y)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.measure_preimage_inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G)
  [μ.IsInvInvariant] (A : Set G), μ (Inv.inv ⁻¹' A) = μ A
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.getState : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Meta.Grind.GoalM σ
-- Mathlib.Data.Multiset.UnionInter
Multiset.union_le_add : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s ∪ t ≤ s + t
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.Hom.ext_iff : ∀ {R : Type u} {inst : CommRing R} {A B : CommBialgCat R} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.δ_descCochain : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cochain G K n) (h : m + 1 = n)
  (n' : ℤ) (hn' : n + 1 = n'),
  CochainComplex.HomComplex.δ n n' (CochainComplex.mappingCone.descCochain φ α β h) =
    (↑(CochainComplex.mappingCone.fst φ)).comp
        (CochainComplex.HomComplex.δ m n α + n'.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp β ⋯) ⋯ +
      (CochainComplex.mappingCone.snd φ).comp (CochainComplex.HomComplex.δ n n' β) ⋯
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_pos : ∀ {S : Type u_5} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Semiring R] (abv : R → S)
  [IsAbsoluteValue abv] {a : R}, 0 < abv a ↔ a ≠ 0
-- Mathlib.GroupTheory.Schreier
Subgroup.rank_le_index_mul_rank : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [hG : Group.FG G] [inst_1 : H.FiniteIndex],
  Group.rank ↥H ≤ H.index * Group.rank G
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max!_eq_maxD_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.max! = t.maxD default
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.instTypeNameCancelToken_proofWidgets : TypeName IO.CancelToken
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.xor_eq_zero_iff : ∀ {x y : ℕ}, x ^^^ y = 0 ↔ x = y
-- Mathlib.Analysis.Normed.Group.Quotient
NormedAddGroupHom.lift_norm_le : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (S : AddSubgroup M) (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) {c : NNReal},
  ‖f‖ ≤ ↑c → ‖NormedAddGroupHom.lift S f hf‖ ≤ ↑c
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSupBotHom.eq_1 : ExpGrowth.expGrowthSupBotHom =
  { toFun := ExpGrowth.expGrowthSup, map_sup' := ⋯, map_bot' := ExpGrowth.expGrowthSup_zero }
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesLimit_iff_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  {F G : CategoryTheory.Functor C D} (h : F ≅ G),
  CategoryTheory.Limits.PreservesLimit K F ↔ CategoryTheory.Limits.PreservesLimit K G
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.write_mk : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (a b : Γ) (L R : Turing.ListBlank Γ),
  Turing.Tape.write b { head := a, left := L, right := R } = { head := b, left := L, right := R }
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.unop_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) {X Y : C} (f : X ⟶ Y), F.unop.map f = (F.map f.op).unop
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLT?_eq_map : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α},
  Std.DTreeMap.Internal.Impl.Const.getEntryLT? k t =
    Option.map (fun x => (x.fst, x.snd)) (Std.DTreeMap.Internal.Impl.getEntryLT? k t)
-- Mathlib.Data.Real.ConjExponents
/-- Real numbers `p q r : ℝ` are said to be a **Hölder triple** if `p` and `q` are positive
and `p⁻¹ + q⁻¹ = r⁻¹`.  -/
Real.HolderTriple : ℝ → ℝ → ℝ → Prop
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.toFun_eq_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}, f.toFun = ⇑f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertMany_empty_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] {l : List (α × β)} {k k' : α},
  compare k k' = Ordering.eq →
    ∀ {v : β} [inst : Inhabited β],
      List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l →
          Std.DTreeMap.Internal.Impl.Const.get!
              (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)) k' =
            v
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (inner inner_1 : Std.ExtDHashMap α fun x => β),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_toInt32 : ∀ (n : ISize) (h : System.Platform.numBits = 64), n.toInt32.toBitVec = BitVec.signExtend 32 (n.toBitVec64 h)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → k ∉ t₁ ∩ t₂
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_linear_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v w : V),
  (signedDist v).linear w = ContinuousAffineMap.const ℝ P (inner ℝ (-NormedSpace.normalize v) w)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivAtFilter.fst : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {L : Filter (E × E)} {f₂ : E → F × G}
  {f₂' : E →L[𝕜] F × G},
  HasFDerivAtFilter f₂ f₂' L → HasFDerivAtFilter (fun x => (f₂ x).1) (ContinuousLinearMap.fst 𝕜 F G ∘SL f₂') L
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.SemiRingCat.Hom.mk : {R S : SemiRingCat} → (↑R →+* ↑S) → R.Hom S
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.casesOn_mk : ∀ {motive : Complex.UnitClosedDisc → Sort u_1}
  (mk' : (z : ℂ) → (hz : ‖z‖ ≤ 1) → motive (Complex.UnitClosedDisc.mk z hz)) {z : ℂ} (hz : ‖z‖ ≤ 1),
  Complex.UnitClosedDisc.casesOn mk' (Complex.UnitClosedDisc.mk z hz) = mk' z hz
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Cat.freeMap_id : ∀ (V : Type u_1) [inst : Quiver V],
  CategoryTheory.Cat.freeMap (𝟭q V) = CategoryTheory.Functor.id (CategoryTheory.Paths V)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.LinarithData.mk : ℕ → Mathlib.Tactic.Linarith.PCompSet → Mathlib.Tactic.Linarith.LinarithData
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.i_mul_k : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃), q.i * q.k = c₁ • q.j + c₂ • q.k
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.instReprWeekday.repr.match_1.eq_3 : ∀ (motive : Std.Time.Weekday → Sort u_1) (h_1 : Unit → motive Std.Time.Weekday.monday)
  (h_2 : Unit → motive Std.Time.Weekday.tuesday) (h_3 : Unit → motive Std.Time.Weekday.wednesday)
  (h_4 : Unit → motive Std.Time.Weekday.thursday) (h_5 : Unit → motive Std.Time.Weekday.friday)
  (h_6 : Unit → motive Std.Time.Weekday.saturday) (h_7 : Unit → motive Std.Time.Weekday.sunday),
  (match Std.Time.Weekday.wednesday with
    | Std.Time.Weekday.monday => h_1 ()
    | Std.Time.Weekday.tuesday => h_2 ()
    | Std.Time.Weekday.wednesday => h_3 ()
    | Std.Time.Weekday.thursday => h_4 ()
    | Std.Time.Weekday.friday => h_5 ()
    | Std.Time.Weekday.saturday => h_6 ()
    | Std.Time.Weekday.sunday => h_7 ()) =
    h_3 ()
-- Init.Data.List.Attach
List.map_unattach : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : List (Subtype P)} {f : α → β},
  List.map f xs.unattach =
    List.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
      xs
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.instModule.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S],
  AddMonoidAlgebra.instModule =
    { toDistribMulAction := AddMonoidAlgebra.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_of_mul_lt_mul_right' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α] [i : MulRightReflectLT α] {a b c : α}, b * a < c * a → b < c
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
/-- If `f` and `g` have derivatives `df` and `dg` at `x`, respectively,
then `x ↦ (f x, g x)` has derivative `df.prod dg`.  -/
HasMFDerivAt.prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {x : M} {f : M → M'} {g : M → M''} {df : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
  HasMFDerivAt% f x df →
    ∀ {dg : TangentSpace I x →L[𝕜] TangentSpace I'' (g x)},
      HasMFDerivAt% g x dg → HasMFDerivAt% (fun y => (f y, g y)) x (df.prod dg)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {Q : CategoryTheory.ObjectProperty C},
  P ≤ Q → P.limitsClosure J ≤ Q.limitsClosure J
-- Lean.Meta.LazyDiscrTree
/-- Hash function  -/
Lean.Meta.LazyDiscrTree.Key.hash : Lean.Meta.LazyDiscrTree.Key → UInt64
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aevalTower_comp_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S : Type u_2} {A : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring A] [inst_3 : Algebra S R] [inst_4 : Algebra S A] (g : R →ₐ[S] A) (y : σ → A),
  (↑(MvPolynomial.aevalTower g y)).comp MvPolynomial.C = ↑g
-- Init.Data.SInt.Bitwise
ISize.ofBitVec_and : ∀ (a b : BitVec System.Platform.numBits), ISize.ofBitVec (a &&& b) = ISize.ofBitVec a &&& ISize.ofBitVec b
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
/-- If `E` has pairwise pullbacks, this is the canonical map from the minimal `1`-hypercover
to the saturation.  -/
CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} → (E : CategoryTheory.PreZeroHypercover S) → [inst_1 : E.HasPullbacks] → E.toPreOneHypercover ⟶ E.saturate
-- Mathlib.Topology.Homotopy.Lifting
/-- The lift to a covering space of a homotopy between two continuous maps relative to a set
given compatible lifts of the continuous maps.  -/
IsCoveringMap.liftHomotopyRel : {E : Type u_1} →
  {X : Type u_2} →
    {A : Type u_3} →
      [inst : TopologicalSpace E] →
        [inst_1 : TopologicalSpace X] →
          [inst_2 : TopologicalSpace A] →
            {p : E → X} →
              IsCoveringMap p →
                {f₀ f₁ : C(A, X)} →
                  {S : Set A} →
                    f₀.HomotopyRel f₁ S →
                      [PreconnectedSpace A] →
                        {f₀' f₁' : C(A, E)} →
                          (∃ a ∈ S, f₀' a = f₁' a) → p ∘ ⇑f₀' = ⇑f₀ → p ∘ ⇑f₁' = ⇑f₁ → f₀'.HomotopyRel f₁' S
-- Mathlib.Analysis.Convex.Strict
StrictConvex.affinity : ∀ {𝕜 : Type u_1} {𝕝 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : TopologicalSpace E] [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : Field 𝕝] [inst_6 : Module 𝕝 E]
  [ContinuousConstSMul 𝕝 E] [LinearMap.CompatibleSMul E E 𝕜 𝕝] {s : Set E} [ContinuousAdd E],
  StrictConvex 𝕜 s → ∀ (z : E) (c : 𝕝), StrictConvex 𝕜 (z +ᵥ c • s)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.liftEquiv_apply : ∀ {ι : Type u_1} [inst : Fintype ι] (𝕜 : Type u_2) (E : ι → Type u_3) [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (F : Type u_4)
  [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] (f : ContinuousMultilinearMap 𝕜 E F),
  (PiTensorProduct.liftEquiv 𝕜 E F) f = (PiTensorProduct.lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯
-- Mathlib.Order.Defs.Unbundled
/-- `IsTrans X r` means the binary relation `r` on `X` is transitive.  -/
IsTrans : (α : Sort u_1) → (α → α → Prop) → Prop
-- Mathlib.Topology.Constructions
instWeaklyLocallyCompactSpaceMultiplicative : ∀ {X : Type u} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X], WeaklyLocallyCompactSpace (Multiplicative X)
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.HasDetOne.mk : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R]
  {Γ : Subgroup (GL n R)}, (∀ {g : GL n R}, g ∈ Γ → Matrix.GeneralLinearGroup.det g = 1) → Γ.HasDetOne
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.addEquivAddHaarChar_pos : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalAddGroup G] [inst_5 : LocallyCompactSpace G] (φ : G ≃ₜ+ G),
  0 < MeasureTheory.addEquivAddHaarChar φ
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.liftAlgHom_toRingHom : ∀ {A : Type u_4} [inst : CommSemiring A] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : Algebra A R]
  {M : Submonoid R} {S : Type u_6} [inst_3 : CommSemiring S] [inst_4 : Algebra A S] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower A R S] {P : Type u_7} [inst_7 : CommSemiring P] [inst_8 : Algebra A P]
  [inst_9 : IsLocalization M S] {f : R →ₐ[A] P} (hf : ∀ (y : ↥M), IsUnit (f ↑y)),
  (IsLocalization.liftAlgHom hf).toRingHom = IsLocalization.lift hf
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.depthLt.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mk_le_mk : ∀ {M : Type u_1} [inst : AddZeroClass M] {s t : AddSubsemigroup M} (h_zero : 0 ∈ s.carrier) (h_zero' : 0 ∈ t.carrier),
  { toAddSubsemigroup := s, zero_mem' := h_zero } ≤ { toAddSubsemigroup := t, zero_mem' := h_zero' } ↔ s ≤ t
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_eq_zero_iff_of_mem_Ico : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)]
  {a : 𝕜} [Archimedean 𝕜], a ∈ Set.Ico 0 p → (↑a = 0 ↔ a = 0)
-- Std.Data.DHashMap.RawDef
Std.DHashMap.Raw.mk : {α : Type u} → {β : α → Type v} → ℕ → Array (Std.DHashMap.Internal.AssocList α β) → Std.DHashMap.Raw α β
-- Mathlib.Analysis.Normed.Operator.Basic
/-- **Alias** of the reverse direction of `ContinuousLinearMap.opNorm_le_iff_lipschitz`. -/
ContinuousLinearMap.opNorm_le_of_lipschitz : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F}
  {K : NNReal}, LipschitzWith K ⇑f → ‖f‖ ≤ ↑K
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.withTacticInfoContext : {α : Type} → Lean.Syntax → Lean.Elab.Tactic.Grind.GrindTacticM α → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Mathlib.RingTheory.RingHom.Etale
RingHom.Etale.eq_1 : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), f.Etale = Algebra.Etale R S