mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go.match_1.eq_6 : ∀ {pu : Lean.Compiler.LCNF.Purity} (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1) (fvarId : Lean.FVarId)
  (idx offset : ℕ) (y : Lean.FVarId) (ty : Lean.Expr) (h : pu = Lean.Compiler.LCNF.Purity.impure)
  (h_1 : (decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl))
  (h_2 :
    (decl : Lean.Compiler.LCNF.FunDecl pu) →
      (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h))
  (h_3 : (decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl))
  (h_4 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.Compiler.LCNF.Arg pu) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h))
  (h_5 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.FVarId) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h))
  (h_6 :
    (fvarId : Lean.FVarId) →
      (idx offset : ℕ) →
        (y : Lean.FVarId) →
          (ty : Lean.Expr) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h))
  (h_7 :
    (fvarId : Lean.FVarId) →
      (cidx : ℕ) →
        (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h))
  (h_8 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
            motive (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h))
  (h_9 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (objs? : Option ℕ) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h))
  (h_10 :
    (fvarId : Lean.FVarId) →
      (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.del fvarId h)),
  (match Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h with
    | Lean.Compiler.LCNF.CodeDecl.let decl => h_1 decl
    | Lean.Compiler.LCNF.CodeDecl.fun decl h => h_2 decl h
    | Lean.Compiler.LCNF.CodeDecl.jp decl => h_3 decl
    | Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h => h_4 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h => h_5 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h => h_6 fvarId idx offset y ty h
    | Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h => h_7 fvarId cidx h
    | Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h => h_8 fvarId n check persistent h
    | Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h => h_9 fvarId n check persistent objs? h
    | Lean.Compiler.LCNF.CodeDecl.del fvarId h => h_10 fvarId h) =
    h_6 fvarId idx offset y ty h
-- Mathlib.Data.Multiset.Powerset
Multiset.powerset_le_powerset_iff_le : ∀ {α : Type u_1} {s t : Multiset α}, s.powerset ≤ t.powerset ↔ s ≤ t
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.integrable_iff_finMeasSupp : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {f : MeasureTheory.SimpleFunc α E}, MeasureTheory.Integrable (⇑f) μ ↔ f.FinMeasSupp μ
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.symmetricIcc_le_Conditional : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G], (SummationFilter.symmetricIcc G).filter ≤ (SummationFilter.conditional G).filter
-- Init.Data.UInt.Lemmas
UInt64.not_lt_zero : ∀ {a : UInt64}, ¬a < 0
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.isUniversal_compl_iff_isIsolated : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, Gᶜ.IsUniversal v ↔ G.IsIsolated v
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.desc'_inl : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {X : ι → Type u_5}
  (x₁ : (i₁ : ι₁) → X (e₁.f i₁)) (x₂ : (i₂ : ι₂) → X (e₂.f i₂)) (i : ι₁ ⊕ ι₂) (i₁ : ι₁) (h : Sum.inl i₁ = i),
  ac.desc' x₁ x₂ i = (ComplexShape.Embedding.AreComplementary.desc.aux X (e₁.f i₁) (ac.equiv i) ⋯) (x₁ i₁)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.id_toPrelaxFunctor : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B],
  (CategoryTheory.OplaxFunctor.id B).toPrelaxFunctor = CategoryTheory.PrelaxFunctor.id B
-- Init.Data.Char.Ordinal
Char.ordinal_zero : '\x00'.ordinal = 0
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instMulZeroClass : {α : Type u_1} → [Mul α] → MulZeroClass (WithZero α)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalCoprimeFactorizationRing.factor₁_mul_factor₂ : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  ↑(Polynomial.UniversalCoprimeFactorizationRing.factor₁ m k hn p) *
      ↑(Polynomial.UniversalCoprimeFactorizationRing.factor₂ m k hn p) =
    ↑(p.map (algebraMap R (Polynomial.UniversalCoprimeFactorizationRing m k hn p)))
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- An equivalence of categories lifts to an equivalence of their monoid objects.  -/
CategoryTheory.Equivalence.mapMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (e : C ≌ D) →
              [inst_4 : e.functor.Monoidal] →
                [inst_5 : e.inverse.Monoidal] → [e.IsMonoidal] → CategoryTheory.Mon C ≌ CategoryTheory.Mon D
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
ContinuousLinearMap.fderiv_of_bilinear : ∀ {𝕜 : 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] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' → E} {g : G' → F} {x : G'},
  DifferentiableAt 𝕜 f x →
    DifferentiableAt 𝕜 g x →
      fderiv 𝕜 (fun y => (B (f y)) (g y)) x =
        ((ContinuousLinearMap.precompR G' B) (f x)) (fderiv 𝕜 g x) +
          ((ContinuousLinearMap.precompL G' B) (fderiv 𝕜 f x)) (g x)
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.surjective_eq_topologically : @AlgebraicGeometry.Surjective =
  AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective
-- Init.Data.Array.Lemmas
Array.map_filterMap_some_eq_filterMap_isSome : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α},
  Array.map some (Array.filterMap f xs) = Array.filter (fun b => b.isSome) (Array.map f xs)
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.mul_inv_le_iff_le_mul : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] (a c : R) {b : R}, 0 < b → (a * b⁻¹ ≤ c ↔ a ≤ c * b)
-- Mathlib.Topology.Algebra.Module.Compact
Submodule.isCompact_of_fg : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] [CompactSpace R]
  {N : Submodule R M}, N.FG → IsCompact ↑N
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Pos.Raw.extract.go₁.match_1.eq_1 : ∀ (motive : List Char → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw → Sort u_1) (x x_1 x_2 : String.Pos.Raw)
  (h_1 : (x x_3 x_4 : String.Pos.Raw) → motive [] x x_3 x_4)
  (h_2 :
    (s : List Char) → (c : Char) → (cs : List Char) → s = c :: cs → (i b e : String.Pos.Raw) → motive (c :: cs) i b e),
  (match [], x, x_1, x_2 with
    | [], x, x_3, x_4 => h_1 x x_3 x_4
    | s@h:(c :: cs), i, b, e => h_2 s c cs h i b e) =
    h_1 x x_1 x_2
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Functor.mapHomologicalComplex_obj_X : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂)
  [inst_4 : F.PreservesZeroMorphisms] (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i : ι),
  ((F.mapHomologicalComplex c).obj C).X i = F.obj (C.X i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.of_forall_get?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t₁.WF → t₂.WF → (∀ (k : α), t₁.get? k = t₂.get? k) → t₁.Equiv t₂
-- Init.Data.UInt.Lemmas
UInt8.zero_mod : ∀ {a : UInt8}, 0 % a = 0
-- Mathlib.Data.Set.MulAntidiagonal
Set.MulAntidiagonal.fst_eq_fst_iff_snd_eq_snd : ∀ {α : Type u_1} [inst : CommMonoid α] [IsCancelMul α] {s t : Set α} {a : α} {x y : ↑(s.mulAntidiagonal t a)},
  (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2
-- Mathlib.Topology.Order.Basic
/-- **Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities
hold everywhere.  -/
tendsto_of_tendsto_of_tendsto_of_le_of_le : ∀ {α : Type u} {β : Type v} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {f g h : β → α}
  {b : Filter β} {a : α},
  Filter.Tendsto g b (nhds a) → Filter.Tendsto h b (nhds a) → g ≤ f → f ≤ h → Filter.Tendsto f b (nhds a)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.empty_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α}, ∅ = m ↔ m = ∅
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Complex.differentiableAt_tan : ∀ {x : ℂ}, DifferentiableAt ℂ Complex.tan x ↔ Complex.cos x ≠ 0
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanStaleDependencyParams : Lean.ToJson Lean.Lsp.LeanStaleDependencyParams
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.rankD_push : ∀ {a : ℕ} {arr : Array Batteries.UFNode},
  Batteries.UnionFind.rankD (arr.push { parent := arr.size, rank := 0 }) a = Batteries.UnionFind.rankD arr a
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instAdd : (K : Type u) →
  [inst : CommRing K] → (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → Add (PerfectClosure K p)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_coconePoints : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C],
  (CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F).coconePoints = F.comp CategoryTheory.Limits.colim
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findSomeRevM?.find.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (val : β) → motive (some val)) (h_2 : Unit → motive none),
  (match none with
    | some val => h_1 val
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Logic.Function.Basic
Function.LeftInverse.eq_rec_eq : ∀ {α : Sort u_1} {β : Sort u_2} {γ : β → Sort v} {f : α → β} {g : β → α} (h : Function.LeftInverse g f)
  (C : (a : α) → γ (f a)) (a : α), ⋯ ▸ C (g (f a)) = C a
-- Std.Data.ExtDHashMap.Basic
/-- Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof
of `a ∈ m`.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDHashMap.get : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [inst : LawfulBEq α] → (m : Std.ExtDHashMap α β) → (a : α) → a ∈ m → β a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f).isEmpty = ((t.isEmpty || t.size == 1 && t.contains k) && (f t[k]?).isNone)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 0th group cohomology of `A`, defined as the 0th cohomology of the complex of inhomogeneous
cochains, is isomorphic to the invariants of the representation on `A`.  -/
groupCohomology.H0Iso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → groupCohomology.H0 A ≅ ModuleCat.of k ↥A.ρ.invariants
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- The Galois correspondence from intermediate fields to subgroups.  -/
IsGaloisGroup.intermediateFieldEquivSubgroup : (G : Type u_1) →
  (K : Type u_3) →
    (L : Type u_4) →
      [inst : Group G] →
        [inst_1 : Field K] →
          [inst_2 : Field L] →
            [inst_3 : Algebra K L] →
              [inst_4 : MulSemiringAction G L] →
                [hGKL : IsGaloisGroup G K L] → [Finite G] → IntermediateField K L ≃o (Subgroup G)ᵒᵈ
-- Mathlib.Analysis.Calculus.Deriv.Pow
hasDerivWithinAt_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} (n : ℕ) (x : 𝕜),
  HasDerivWithinAt (fun x => x ^ n) (↑n * x ^ (n - 1)) s x
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instNonUnitalSeminormedCommRing : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    [CompactSpace α] → {R : Type u_4} → [inst_2 : NonUnitalSeminormedCommRing R] → NonUnitalSeminormedCommRing C(α, R)
-- Mathlib.Algebra.MvPolynomial.NoZeroDivisors
MvPolynomial.dvd_X_iff_exists : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommRing R] [NoZeroDivisors R] {p : MvPolynomial σ R} {i : σ},
  p ∣ MvPolynomial.X i ↔ ∃ r, IsUnit r ∧ (p = MvPolynomial.C r ∨ p = r • MvPolynomial.X i)
-- Mathlib.Logic.Equiv.Defs
Equiv.exists_congr_left : ∀ {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β), (∃ a, p a) ↔ ∃ b, p (e.symm b)
-- Mathlib.Order.Disjoint
Complementeds.coe_sup : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] (a b : Complementeds α), ↑(a ⊔ b) = ↑a ⊔ ↑b
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_iff_forall_le_1 : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {σ : Type v} {P Q : σ → l},
  Lean.Order.PartialOrder.rel P Q ↔ ∀ (s : σ), Lean.Order.PartialOrder.rel (P s) (Q s)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.faces.δ : ∀ {n : ℕ} (i : Fin (n + 2)), SimplexCategoryGenRel.faces (SimplexCategoryGenRel.δ i)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigOWith_mul_iff_isBigOWith_div : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g h : α → 𝕜} {c : ℝ},
  (∀ᶠ (x : α) in l, f x ≠ 0) →
    (Asymptotics.IsBigOWith c l (fun x => f x * g x) h ↔ Asymptotics.IsBigOWith c l g fun x => h x / f x)
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
_private.Mathlib.NumberTheory.Harmonic.GammaDeriv.0.termγ : Lean.ParserDescr
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sInf_mul : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : Group M] [MulLeftMono M] [MulRightMono M] (s t : Set M),
  sInf (s * t) = sInf s * sInf t
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_ofNat : ∀ {R : Type u_1} {a b : R} [inst : AddCommMonoidWithOne R] (n : ℕ) [inst_1 : n.AtLeastTwo],
  QuadraticAlgebra.C (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Order.Cover
WCovBy.le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⩿ b → a ≤ b
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.ext : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {U V : OpenAddSubgroup G},
  (∀ (x : G), x ∈ U ↔ x ∈ V) → U = V
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.homEquivToProd_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y Z : C} (f : (Z ⟶ X) × (Z ⟶ Y)),
  CategoryTheory.CartesianMonoidalCategory.homEquivToProd.symm f = CategoryTheory.CartesianMonoidalCategory.lift f.1 f.2
-- Lean.Elab.DeclModifiers
/-- Returns `true` if `modifiers` contains an attribute satisfying `p`.  -/
Lean.Elab.Modifiers.anyAttr : Lean.Elab.Modifiers → (Lean.Elab.Attribute → Bool) → Bool
-- Mathlib.Topology.Algebra.Group.Basic
Pi.topologicalGroup : ∀ {β : Type v} {C : β → Type u_1} [inst : (b : β) → TopologicalSpace (C b)] [inst_1 : (b : β) → Group (C b)]
  [∀ (b : β), IsTopologicalGroup (C b)], IsTopologicalGroup ((b : β) → C b)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instGroupOfIsTopologicalGroup.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Group β]
  [inst_3 : IsTopologicalGroup β],
  ContinuousMap.instGroupOfIsTopologicalGroup =
    { toMonoid := ContinuousMap.instMonoidOfContinuousMul, toInv := ContinuousMap.instInvOfContinuousInv,
      toDiv := ContinuousMap.instDivOfContinuousDiv, toZPow := ZPow.ofPow, div_eq_mul_inv := ⋯, zpow_zero' := ⋯,
      zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtDTreeMap.Const.insertMany t l).getKey? k = t.getKey? k
-- Mathlib.Order.Directed
isDirected_mono : ∀ {α : Type u_1} {r : α → α → Prop} (s : α → α → Prop) [IsDirected α r], (∀ ⦃a b : α⦄, r a b → s a b) → IsDirected α s
-- Mathlib.Data.Set.Prod
AntitoneOn.set_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} [inst : Preorder α] {f : α → Set β} {g : α → Set γ},
  AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => f x ×ˢ g x) s
-- Mathlib.CategoryTheory.Functor.Category
/-- The functor `(C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E` which flips the variables.  -/
CategoryTheory.flipFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            CategoryTheory.Functor (CategoryTheory.Functor C (CategoryTheory.Functor D E))
              (CategoryTheory.Functor D (CategoryTheory.Functor C E))
-- Lean.Parser.Command
Lean.Parser.Command.structureTk : Lean.Parser.Parser
-- Mathlib.Data.Int.ModEq
Int.modEq_comm : ∀ {n a b : ℤ}, a ≡ b [ZMOD n] ↔ b ≡ a [ZMOD n]
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isRadical_bot_of_noZeroDivisors : ∀ {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R], ⊥.IsRadical
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasureClass.measure_mono : ∀ {F : Type u_2} {α : outParam (Type u_3)} {inst : FunLike F (Set α) ENNReal}
  [self : MeasureTheory.OuterMeasureClass F α] (f : F) {s t : Set α}, s ⊆ t → f s ≤ f t
-- Mathlib.Tactic.NormNum.Irrational
_private.Mathlib.Tactic.NormNum.Irrational.0.Mathlib.Meta.NormNum.not_power_rat_of_num : ∀ {a b d : ℕ}, a.Coprime b → (∀ (x : ℕ), a ≠ x ^ d) → ∀ (q : ℚ), ↑a / ↑b ≠ q ^ d
-- Std.Sat.AIG.Basic
Std.Sat.AIG.mk : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      (decls : Array (Std.Sat.AIG.Decl α)) →
        Std.Sat.AIG.Cache α decls →
          Std.Sat.AIG.IsDAG α decls → (hzero : 0 < decls.size) → decls[0] = Std.Sat.AIG.Decl.false → Std.Sat.AIG α
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.name : Aesop.ElabRuleTerm → Lean.MetaM Lean.Name
-- Mathlib.Data.Fintype.Sets
/-- **Alias** of the reverse direction of `Set.toFinset_ssubset_toFinset`. -/
Set.toFinset_strict_mono : ∀ {α : Type u_1} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s ⊂ t → s.toFinset ⊂ t.toFinset
-- Lean.Syntax
Lean.IsNode : Lean.Syntax → Prop
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (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.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Init.Data.SInt.Bitwise
Int8.toBitVec_or : ∀ (a b : Int8), (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.SMulCandidate.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} {α : R₀ ⟶ R.obj}
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} {φ : M₀.presheaf ⟶ A.obj} {X : Cᵒᵖ}
  {r : ↑(R.obj.obj X)} {m : ↑(A.obj.obj X)} (x x_1 : ↑(A.obj.obj X)) (e_x : x = x_1)
  (h :
    ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
      (CategoryTheory.ConcreteCategory.hom (α.app Y)) r₀ = (CategoryTheory.ConcreteCategory.hom (R.obj.map f)) r →
        ∀ (m₀ : ↑(M₀.obj Y)),
          (CategoryTheory.ConcreteCategory.hom (φ.app Y)) m₀ = (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) m →
            (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) x =
              (CategoryTheory.ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)),
  { x := x, h := h } = { x := x_1, h := ⋯ }
-- Mathlib.Data.List.Pairwise
List.Pairwise.decide : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] (l : List α),
  List.Pairwise R l → List.Pairwise (fun a b => decide (R a b) = true) l
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsMonHom.mul_hom : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M N : C}
  {inst_2 : CategoryTheory.MonObj M} {inst_3 : CategoryTheory.MonObj N} (f : M ⟶ N) [self : CategoryTheory.IsMonHom f],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.MonObj.mul
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight_left : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ')
  (φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''),
  (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight α φ).left =
    CategoryTheory.Functor.whiskerRight α.left φ.left
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.Plus.quotient_map_hom : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CochainComplex.Plus C} (f : X ⟶ Y),
  ((HomotopyCategory.Plus.quotient C).map f).hom = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f.hom