mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ι_D₁_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {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_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : 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_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : ⋯ = j)
  {Z : C₄}, ⋯
-- Mathlib.RingTheory.IsAdjoinRoot
/-- Lift the algebra map `R → T` to `S →ₐ[R] T` by specifying a root `x` of `f` in `T`,
where `S` is given by adjoining a root of `f` to `R`.  -/
IsAdjoinRoot.liftHom : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : Ring S] →
        {f : Polynomial R} →
          [inst_2 : Algebra R S] →
            IsAdjoinRoot S f →
              {T : Type u_1} →
                [inst_3 : CommRing T] → (x : T) → [inst_4 : Algebra R T] → (Polynomial.aeval x) f = 0 → S →ₐ[R] T
-- Mathlib.Data.ENat.Defs
/-- Recursor for `ENat` using the preferred forms `⊤` and `↑a`.  -/
ENat.recTopCoe : {C : ℕ∞ → Sort u_1} → C ⊤ → ((a : ℕ) → C ↑a) → (n : ℕ∞) → C n
-- Init.Data.UInt.Lemmas
UInt64.ne_of_toBitVec_ne : ∀ {a b : UInt64}, a.toBitVec ≠ b.toBitVec → a ≠ b
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.PlausibleStep : {m : Type w → Type w'} →
  {β α₁ α₂ : Type w} →
    [Std.Iterator α₁ m β] → [Std.Iterator α₂ m β] → Std.IterM m β → Std.IterStep (Std.IterM m β) β → Prop
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_ric : ∀ {n i : ℕ}, (*...=n).toList[i]? = if i ≤ n then some i else none
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_exp : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, Real.exp x = Real.exp b - Real.exp a
-- Mathlib.Logic.Embedding.Set
/-- A subtype `{x // p x ∨ q x}` over a disjunction of `p q : α → Prop` is equivalent to a sum of
subtypes `{x // p x} ⊕ {x // q x}` such that `¬ p x` is sent to the right, when
`Disjoint p q`.

See also `Equiv.sumCompl`, for when `IsCompl p q`.  -/
subtypeOrEquiv : {α : Type u_1} → (p q : α → Prop) → [DecidablePred p] → Disjoint p q → { x // p x ∨ q x } ≃ { x // p x } ⊕ { x // q x }
-- Mathlib.Order.Disjoint
Codisjoint.dual : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α},
  Codisjoint a b → Disjoint (OrderDual.toDual a) (OrderDual.toDual b)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_succ_mul_X : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (φ : PowerSeries R),
  (PowerSeries.coeff (n + 1)) (φ * PowerSeries.X) = (PowerSeries.coeff n) φ
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.comp_apply : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : MulOne P] (g : N →* P)
  (f : M →* N) (x : M), (g.comp f) x = g (f x)
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
/-- A category has countable products if it has all products indexed by countable types.  -/
CategoryTheory.Limits.HasCountableProducts : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- If `gfpApprox f x a` is a fixed point, then the infimum of the whole
ordinal-indexed sequence equals the value at `a`.  -/
OrdinalApprox.iInf_gfpApprox_eq_of_mem_fixedPoints : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}},
  OrdinalApprox.gfpApprox f x a ∈ Function.fixedPoints ⇑f →
    ⨅ i, OrdinalApprox.gfpApprox f x i = OrdinalApprox.gfpApprox f x a
-- Init.Data.Ord.Basic
List.compareLex.eq_3 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : List α), (x = [] → False) → List.compareLex cmp x [] = Ordering.gt
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.coe_le_one : ∀ {α : Type u_1} [inst : LE α] {a : α} [inst_1 : One α], ↑a ≤ 1 ↔ a ≤ 1
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
prodIsoPullback_inv_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y]
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from X)
        (CategoryTheory.Limits.terminal.from Y))
      h
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.Decl.atomToCNF_eval : ∀ {α : Type u_1} {output a : α} {assign : α → Bool},
  Std.Sat.CNF.eval assign (Std.Sat.AIG.Decl.atomToCNF✝ output a) = (assign output == assign a)
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- Equality behind `SemiconjBy a x y`; useful for rewriting.  -/
SemiconjBy.eq : ∀ {S : Type u_1} [inst : Mul S] {a x y : S}, SemiconjBy a x y → a * x = y * a
-- Lean.Meta.Basic
Lean.Meta.instAddMessageContextMetaM : Lean.AddMessageContext Lean.MetaM
-- Lean.Expr
/-- String literal  -/
Lean.Literal.strVal : String → Lean.Literal
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isInf.injEq : ∀ (lhs rhs res lhs_1 rhs_1 res_1 : ℕ),
  (Mathlib.Tactic.Order.AtomicFact.isInf lhs rhs res = Mathlib.Tactic.Order.AtomicFact.isInf lhs_1 rhs_1 res_1) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ res = res_1)
-- Std.Http.Data.Chunk
Std.Http.Chunk.instDecidableEqExtensionName.decEq : (x x_1 : Std.Http.Chunk.ExtensionName) → Decidable (x = x_1)
-- Mathlib.Algebra.Lie.TransferInstance
Equiv.bracket_def : ∀ {L' : Type u_2} {L : Type u_3} [inst : LieRing L] (e : L' ≃ L) (x y : L'), ⁅x, y⁆ = e.symm ⁅e x, e y⁆
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.smul_sUnion : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] (s : Set α) (T : Set (Set β)), s • ⋃₀ T = ⋃ t ∈ T, s • t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.nonsingular_iff_variableChange : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} (x y : R),
  W.Nonsingular x y ↔ (WeierstrassCurve.toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Nonsingular 0 0
-- Mathlib.Algebra.Group.Units.Defs
Units.val_copy : ∀ {α : Type u} [inst : Monoid α] (u : αˣ) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑u⁻¹),
  ↑(u.copy val hv inv hi) = val
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpace_nsmul_add_ne_bot_of_le : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) {n : ℕ},
  n ≤ LieModule.chainTopCoeff α β → LieModule.genWeightSpace M (n • α + ⇑β) ≠ ⊥
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
_private.Mathlib.Analysis.InnerProductSpace.TensorProduct.0.TensorProduct.re_inner_self_nonneg : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (x : TensorProduct 𝕜 E F), 0 ≤ RCLike.re (inner 𝕜 x x)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_of_mem_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t.keys → k ∈ t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α},
  Array.find? (fun x => cmp x.1 k == Ordering.eq) (Std.DTreeMap.Const.toArray t) = none ↔ t.contains k = false
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.top_iff : ∀ {G : Type u_1} [inst : Group G], Group.IsPerfect ↥⊤ ↔ Group.IsPerfect G
-- Mathlib.Topology.Algebra.Star
ContinuousAt.star : ∀ {α : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Star R] [ContinuousStar R]
  [inst_3 : TopologicalSpace α] {f : α → R} {x : α}, ContinuousAt f x → ContinuousAt (fun x => star (f x)) x
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAdd : {M : Type u_1} → [inst : TopologicalSpace M] → [inst_1 : Add M] → [ContinuousAdd M] → Add (SeparationQuotient M)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_eq_zero : ∀ {x : ℝ}, Real.arccos x = 0 ↔ 1 ≤ x
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.eval_section_surjective_of_surjective : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Nonempty (F.obj j)] [∀ (j : J), Finite (F.obj j)],
  (∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) →
    ∀ (i : J), Function.Surjective fun s => ↑s i
-- Mathlib.Order.WellFoundedSet
Set.partiallyWellOrderedOn_univ_iff : ∀ {α : Type u_2} {r : α → α → Prop}, Set.univ.PartiallyWellOrderedOn r ↔ WellQuasiOrdered r
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Cat.freeMap_comp : ∀ {V₁ : Type u₁} {V₂ : Type u₂} {V₃ : Type u₃} [inst : Quiver V₁] [inst_1 : Quiver V₂] [inst_2 : Quiver V₃]
  (F : V₁ ⥤q V₂) (G : V₂ ⥤q V₃),
  CategoryTheory.Cat.freeMap (F ⋙q G) = (CategoryTheory.Cat.freeMap F).comp (CategoryTheory.Cat.freeMap G)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.lift_comp_one_left_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.MonObj B] (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (g : A ⟶ B)
  {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.MonObj.one) g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Topology.Algebra.Group.Basic
/-- On a topological group, `𝓝 : G → Filter G` can be promoted to a `MulHom`.  -/
nhdsMulHom : {G : Type w} → [inst : TopologicalSpace G] → [inst_1 : Group G] → [IsTopologicalGroup G] → G →ₙ* Filter G
-- Mathlib.Analysis.MeanInequalities
/-- **HM-GM inequality**: The harmonic mean is less than or equal to the geometric mean.  -/
Real.harm_mean_le_geom_mean : ∀ {ι : Type u_1} (s : Finset ι),
  s.Nonempty →
    ∀ (w z : ι → ℝ),
      (∀ i ∈ s, 0 < w i) →
        0 < ∑ i ∈ s, w i →
          (∀ i ∈ s, 0 < z i) → (∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹
-- Init.Data.String.Lemmas.Iterate
String.toList_revPositionsFrom : ∀ {s : String} {p : s.Pos}, (s.revPositionsFrom p).toList = String.Model.revPositionsFrom p
-- Mathlib.Topology.Order.Basic
/-- An `OrderEmbedding` is a topological embedding provided that the range of `f` is
order-connected  -/
OrderEmbedding.isEmbedding_of_ordConnected : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [inst_4 : TopologicalSpace β] [OrderTopology β] (f : α ↪o β),
  (Set.range ⇑f).OrdConnected → Topology.IsEmbedding ⇑f
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.eraseMany! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {ρ : Type u_1} [inst : ForIn Id ρ α] {l : ρ}
  {t : Std.DTreeMap.Internal.Impl α β}, t.WF → (↑(t.eraseMany! l)).WF
-- Std.Http.Data.URI.Encoding
Std.Http.URI.EncodedString.instInhabited : {r : UInt8 → Bool} → Inhabited (Std.Http.URI.EncodedString r)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertListIfNewUnit_of_contains : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k fallback : α},
  Std.Internal.List.containsKey k l = true →
    Std.Internal.List.getKeyD k (Std.Internal.List.insertListIfNewUnit l toInsert) fallback =
      Std.Internal.List.getKeyD k l fallback
-- Mathlib.NumberTheory.GaussSum
/-- When `χ` is a nontrivial quadratic character, then the square of `gaussSum χ ψ`
is `χ(-1)` times the cardinality of `R`.  -/
gaussSum_sq : ∀ {R : Type u} [inst : Field R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] [IsDomain R']
  {χ : MulChar R R'},
  χ ≠ 1 → χ.IsQuadratic → ∀ {ψ : AddChar R R'}, ψ.IsPrimitive → gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.instRatCast : {K : Type u_1} → [Field K] → {a b : K} → RatCast (QuadraticAlgebra K a b)
-- Std.Time.Time.Unit.Millisecond
/-- Converts an `Ordinal` to an `Offset`.
 -/
Std.Time.Millisecond.Ordinal.toOffset : Std.Time.Millisecond.Ordinal → Std.Time.Millisecond.Offset
-- Std.Tactic.Do.Syntax
/-- Like `rcases`, but operating on stateful `Std.Do.SPred` goals.
Example: Given a goal `h : (P ∧ (Q ∨ R) ∧ (Q → R)) ⊢ₛ R`,
`mcases h with ⟨-, ⟨hq | hr⟩, hqr⟩` will yield two goals:
`(hq : Q, hqr : Q → R) ⊢ₛ R` and `(hr : R) ⊢ₛ R`.

That is, `mcases h with pat` has the following semantics, based on `pat`:
* `pat=□h'` renames `h` to `h'` in the stateful context, regardless of whether `h` is pure
* `pat=⌜h'⌝` introduces `h' : φ`  to the pure local context if `h : ⌜φ⌝`
  (c.f. `Lean.Elab.Tactic.Do.ProofMode.IsPure`)
* `pat=h'` is like `pat=⌜h'⌝` if `h` is pure
  (c.f. `Lean.Elab.Tactic.Do.ProofMode.IsPure`), otherwise it is like `pat=□h'`.
* `pat=_` renames `h` to an inaccessible name
* `pat=-` discards `h`
* `⟨pat₁, pat₂⟩` matches on conjunctions and existential quantifiers and recurses via
  `pat₁` and `pat₂`.
* `⟨pat₁ | pat₂⟩` matches on disjunctions, matching the left alternative via `pat₁` and the right
  alternative via `pat₂`.
 -/
Lean.Parser.Tactic.mcasesError : Lean.ParserDescr
-- Mathlib.Combinatorics.SetFamily.FourFunctions
_private.Mathlib.Combinatorics.SetFamily.FourFunctions.0.collapse : {α : Type u_1} →
  {β : Type u_2} → [DecidableEq α] → [CommSemiring β] → Finset (Finset α) → α → (Finset α → β) → Finset α → β
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.arrayLit.inj : ∀ {a a_1 : List Lean.Meta.Match.Example},
  Lean.Meta.Match.Example.arrayLit a = Lean.Meta.Match.Example.arrayLit a_1 → a = a_1
-- Mathlib.Analysis.InnerProductSpace.Affine
inner_vsub_vsub_left_eq_dist_sq_left_iff : ∀ {V : Type u_2} {P : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c : P}, inner ℝ (a -ᵥ b) (a -ᵥ c) = dist a b ^ 2 ↔ inner ℝ (a -ᵥ b) (b -ᵥ c) = 0
-- Mathlib.Logic.Basic
exists_exists_eq_and : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop}, (∃ b, (∃ a, f a = b) ∧ p b) ↔ ∃ a, p (f a)
-- Mathlib.Data.Num.Basic
instZeroZNum : Zero ZNum
-- Mathlib.Probability.Kernel.Basic
/-- The deterministic kernel that maps `(x, y)` to the Dirac measure at `(y, x)`.  -/
ProbabilityTheory.Kernel.swap : (α : Type u_4) →
  (β : Type u_5) → [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → ProbabilityTheory.Kernel (α × β) (β × α)
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.tensorObj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F G : CategoryTheory.Functor C D} {X : C},
  (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).obj X =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (G.obj X)
-- Init.Data.BitVec.Basic
/-- Computes a hash of a bitvector, combining 64-bit words using `mixHash`.
 -/
BitVec.hash : {n : ℕ} → BitVec n → UInt64
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.activateNextGuard.go : Lean.Meta.Grind.EMatchTheorem →
  ℕ → List Lean.Meta.Grind.TheoremGuard → Lean.Meta.Grind.GoalM Lean.Meta.Grind.ActivateNextGuardResult
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.instantiateForallAux : Array Lean.Expr → ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.comp_map₂ : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictlyUnitaryPseudofunctor B C)
  (G : CategoryTheory.StrictlyUnitaryPseudofunctor C D) {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  (F.comp G).map₂ η = G.map₂ (F.map₂ η)
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.Props.mk.injEq : ∀ (state : Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef)
  (cancelTk : Lean.Server.WithRpcRef IO.CancelToken)
  (state_1 : Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef)
  (cancelTk_1 : Lean.Server.WithRpcRef IO.CancelToken),
  ({ state := state, cancelTk := cancelTk } = { state := state_1, cancelTk := cancelTk_1 }) =
    (state = state_1 ∧ cancelTk = cancelTk_1)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instDecidableEqCompletionItemKind : DecidableEq Lean.Lsp.CompletionItemKind
-- Mathlib.Data.Finsupp.Ext
Finsupp.mulHom_ext : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : MulOneClass N]
  ⦃f g : Multiplicative (α →₀ M) →* N⦄,
  (∀ (x : α) (y : M), f (Multiplicative.ofAdd fun₀ | x => y) = g (Multiplicative.ofAdd fun₀ | x => y)) → f = g
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.parallel_bot_iff_eq_bot : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P}, s.Parallel ⊥ ↔ s = ⊥
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.AuxGluingStruct.mk.sizeOf_spec : ∀ {A : Type} [inst : MetricSpace A] [inst_1 : SizeOf A] (Space : Type) (metric : MetricSpace Space) (embed : A → Space)
  (isom : Isometry embed),
  sizeOf { Space := Space, metric := metric, embed := embed, isom := isom } = 1 + sizeOf Space + sizeOf metric
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccPrelimit_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a : α), ¬Order.IsSuccPrelimit (Order.succ a)
-- Mathlib.Topology.Order.OrderClosed
SuccOrder.nhdsGE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {b : α} [SuccOrder α],
  nhdsWithin b (Set.Ici b) = pure b
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.comp_eqToHom_heq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Y) (h : Y = Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h) ≍ f
-- Init.Data.SInt.Bitwise
Int8.not_eq_comm : ∀ {a b : Int8}, ~~~a = b ↔ a = ~~~b
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Expr.toPoly.go.match_1.eq_5 : ∀ (motive : Nat.Internal.Linear.Expr → Sort u_1) (a : Nat.Internal.Linear.Expr) (k : ℕ)
  (h_1 : (k : ℕ) → motive (Nat.Internal.Linear.Expr.num k))
  (h_2 : (i : Nat.Internal.Linear.Var) → motive (Nat.Internal.Linear.Expr.var i))
  (h_3 : (a b : Nat.Internal.Linear.Expr) → motive (a.add b))
  (h_4 : (k : ℕ) → (a : Nat.Internal.Linear.Expr) → motive (Nat.Internal.Linear.Expr.mulL k a))
  (h_5 : (a : Nat.Internal.Linear.Expr) → (k : ℕ) → motive (a.mulR k)),
  (match a.mulR k with
    | Nat.Internal.Linear.Expr.num k => h_1 k
    | Nat.Internal.Linear.Expr.var i => h_2 i
    | a.add b => h_3 a b
    | Nat.Internal.Linear.Expr.mulL k a => h_4 k a
    | a.mulR k => h_5 a k) =
    h_5 a k
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p),
  (Ideal.span {hζ.toInteger - 1}).ramificationIdx ℤ = p - 1
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageType.info : Lean.Lsp.MessageType
-- Init.Data.Iterators.Consumers.Stream
Std.instStreamIterOfProductiveOfIteratorAccessId : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] → [Std.Iterators.Productive α Id] → [Std.IteratorAccess α Id] → Std.Stream (Std.Iter β) β
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run a custom tactic at every step in proofs, configured via environment variables.

Set `TRY_AT_EACH_STEP_TACTIC` to the tactic syntax to try (required).
Set `TRY_AT_EACH_STEP_LABEL` to the label for output messages (optional, defaults to tactic).
 -/
linter.tacticAnalysis.tryAtEachStepFromEnv : Lean.Option Bool
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Full.mk : ∀ {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}, Function.Surjective F.map) → F.Full
-- Mathlib.Order.Hom.Lattice
LatticeHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Lattice α] [inst_1 : Lattice β] (toSupHom : SupHom α β)
  (map_inf' : ∀ (a b : α), toSupHom.toFun (a ⊓ b) = toSupHom.toFun a ⊓ toSupHom.toFun b) (toSupHom_1 : SupHom α β)
  (map_inf'_1 : ∀ (a b : α), toSupHom_1.toFun (a ⊓ b) = toSupHom_1.toFun a ⊓ toSupHom_1.toFun b),
  ({ toSupHom := toSupHom, map_inf' := map_inf' } = { toSupHom := toSupHom_1, map_inf' := map_inf'_1 }) =
    (toSupHom = toSupHom_1)
-- Init.Data.Vector.Lemmas
Vector.foldl_append : ∀ {α : Type u_1} {n k : ℕ} {β : Type u_2} {f : β → α → β} {b : β} {xs : Vector α n} {ys : Vector α k},
  Vector.foldl f b (xs ++ ys) = Vector.foldl f (Vector.foldl f b xs) ys
-- Mathlib.RingTheory.WittVector.Basic
WittVector.pow_dvd_ghostComponent_of_dvd_coeff : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {x : WittVector p R} {n : ℕ},
  (∀ i ≤ n, ↑p ∣ x.coeff i) → ↑p ^ (n + 1) ∣ (WittVector.ghostComponent n) x
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.sigmaFinsetFunEquiv_apply_fst : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (a : Π₀ (i : ι), β i),
  (DFinsupp.sigmaFinsetFunEquiv a).fst = a.support
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- One can reformulate being `C^n` as continuity and being `C^n` in any extended chart in the
target.  -/
contMDiff_iff_target : ∀ {𝕜 : 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'] {f : M → M'} {n : WithTop ℕ∞}
  [IsManifold I n M] [IsManifold I' n M'],
  ContMDiff I I' n f ↔
    Continuous f ∧
      ∀ (y : M'), ContMDiffOn I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)