mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.smul_iUnion : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : SMul α β] (s : Set α) (t : ι → Set β),
  s • ⋃ i, t i = ⋃ i, s • t i
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.id_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (x : E.I₀),
  (CategoryTheory.PreOneHypercover.Hom.id E).h₀ x = CategoryTheory.CategoryStruct.id (E.X x)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Around each point in `s`, one of the bump functions is equal to `1`.  -/
SmoothBumpCovering.eventuallyEq_one' : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : optParam (Set M) Set.univ}
  (self : SmoothBumpCovering ι I M s), ∀ x ∈ s, ∃ i, ↑(self.toFun i) =ᶠ[nhds x] 1
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.toContinuousMap_injective : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], Function.Injective ContinuousAddMonoidHom.toContinuousMap
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.Bool.iff_to_beq : ∀ (a b : Bool), (a = true ↔ b = true) = ((a == b) = true)
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.closure_setOfPred_re_lt`. -/
Complex.closure_setOf_re_lt : ∀ (a : ℝ), closure {z | z.re < a} = {z | z.re ≤ a}
-- Init.Data.Array.Basic
Array.Mem.val : ∀ {α : Type u} {as : Array α} {a : α}, as.Mem a → a ∈ as.toList
-- Lean.Parser.Do
Lean.Parser.Term.termFor.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- We can move `qrSign m n` from one side of an equality to the other when `m` and `n` are odd.  -/
qrSign.eq_iff_eq : ∀ {m n : ℕ}, Odd m → Odd n → ∀ (x y : ℤ), qrSign m n * x = y ↔ x = qrSign m n * y
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.Hom.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P Q : CategoryTheory.Idempotents.Karoubi C}
  {x y : P.Hom Q}, x = y ↔ x.f = y.f
-- Mathlib.Topology.MetricSpace.Thickening
Metric.mem_thickening_iff_infEDist_lt : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α},
  x ∈ Metric.thickening δ s ↔ Metric.infEDist x s < ENNReal.ofReal δ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.filter_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  (Std.DTreeMap.filter f t).Equiv t ↔ ∀ (k : α) (h : k ∈ t), f k (t.get k h) = true
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.coeHom_apply : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : StarRing 𝕜]
  [inst_6 : StarRing A] [inst_7 : StarModule 𝕜 A] [inst_8 : NormedStarGroup A] (a : A),
  DoubleCentralizer.coeHom a = ↑𝕜 a
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- **Alias** of the reverse direction of `hasStrictDerivAt_const_add_iff`. -/
HasStrictDerivAt.const_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
  HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => c + f x) f' x
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddSemigroupOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddSemigroup Mᵃᵒᵖ], DomAddAct.instAddSemigroupOfAddOpposite = inst
-- Mathlib.Order.CompleteSublattice
CompleteLatticeHom.range_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β),
  ↑f.range = Set.range ⇑f
-- Mathlib.Data.Finset.Card
Finset.card_le_five : ∀ {α : Type u_1} [inst : DecidableEq α] {a b c d e : α}, {a, b, c, d, e}.card ≤ 5
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.isQuotientMap_projectionOntoL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q),
  Topology.IsQuotientMap ⇑(p.projectionOntoL q h)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_congr : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], (↑m).WF → ∀ {k k' : α}, (k == k') = true → m.getKey! k = m.getKey! k'
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (Z Z_1 : C),
  Z = Z_1 → CategoryTheory.InjectiveResolution Z = CategoryTheory.InjectiveResolution Z_1
-- Mathlib.Combinatorics.Quiver.Path.Decomposition
/-- A path from a vertex not in `S` to a vertex in `S` must cross the boundary.  -/
Quiver.Path.exists_notMem_mem_hom_path_path_of_notMem_mem : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) (S : Set V),
  a ∉ S → b ∈ S → ∃ u ∉ S, ∃ v ∈ S, ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.BohrMollerup.logGammaSeq.eq_1 : ∀ (x : ℝ) (n : ℕ),
  Real.BohrMollerup.logGammaSeq x n =
    x * Real.log ↑n + Real.log ↑n.factorial - ∑ m ∈ Finset.range (n + 1), Real.log (x + ↑m)
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_div' : ∀ {α : Type u_1} {G : Type u_6} [inst : Group G] (s : Set α) (f g : α → G),
  s.mulIndicator (f / g) = s.mulIndicator f / s.mulIndicator g
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.hasEvalIdeal.eq_1 : ∀ {σ : Type u_1} {S : Type u_3} [inst : CommRing S] [inst_1 : TopologicalSpace S] [inst_2 : IsTopologicalRing S]
  [inst_3 : IsLinearTopology S S],
  MvPowerSeries.hasEvalIdeal =
    { carrier := {a | MvPowerSeries.HasEval a}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Mathlib.Data.Finsupp.Order
Finsupp.support_mono : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] {f g : ι →₀ α}
  [CanonicallyOrderedAdd α], f ≤ g → f.support ⊆ g.support
-- Init.Data.Nat.Basic
Nat.add_lt_add_left : ∀ {n m : ℕ}, n < m → ∀ (k : ℕ), k + n < k + m
-- Mathlib.Order.Filter.Pointwise
Filter.comap_add_comap_le : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
  [inst_2 : FunLike F α β] [AddHomClass F α β] (m : F) {f g : Filter β},
  Filter.comap (⇑m) f + Filter.comap (⇑m) g ≤ Filter.comap (⇑m) (f + g)
-- Mathlib.Data.Fintype.Sets
Finset.toFinset_coe : ∀ {α : Type u_1} (s : Finset α) [inst : Fintype ↑↑s], (↑s).toFinset = s
-- Init.Data.BitVec.Lemmas
BitVec.instLawfulIdentityHAddOfNatOfNatNat : ∀ {n : ℕ}, Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0#n
-- Mathlib.Order.BoundedOrder.Basic
/-- An order is (noncomputably) either an `OrderBot` or a `NoBotOrder`. Use as
`cases botOrderOrNoBotOrder α`.  -/
botOrderOrNoBotOrder : (α : Type u_1) → [inst : LE α] → OrderBot α ⊕' NoBotOrder α
-- Mathlib.Algebra.Order.Ring.GeomSum
geom_sum_pos' : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R},
  0 < x + 1 → n ≠ 0 → 0 < ∑ i ∈ Finset.range n, x ^ i
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)}
  (t : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)),
  (CategoryTheory.WithInitial.coconeEquiv.inverse.obj t).pt.right = t.pt
-- Mathlib.ModelTheory.Syntax
/-- Maps a bounded formula's symbols along a language map.  -/
FirstOrder.Language.LHom.onBoundedFormula : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} → {α : Type u'} → (L →ᴸ L') → {k : ℕ} → L.BoundedFormula α k → L'.BoundedFormula α k
-- Mathlib.Order.Fin.Tuple
Fin.castLEOrderIso_apply : ∀ {n m : ℕ} (h : n ≤ m) (i : Fin n), (Fin.castLEOrderIso h) i = ⟨Fin.castLE h i, ⋯⟩
-- Mathlib.GroupTheory.Submonoid.Center
MulEquivClass.apply_mem_center : ∀ {M : Type u_3} {N : Type u_1} {F : Type u_2} [inst : EquivLike F M N] [inst_1 : Mul M] [inst_2 : Mul N]
  [MulEquivClass F M N] (e : F) {x : M}, x ∈ Set.center M → e x ∈ Set.center N
-- Mathlib.Data.Sum.Basic
Sum.getRight.hcongr_4 : ∀ (α α' : Type u_1),
  α = α' →
    ∀ (β β' : Type u_2),
      β = β' →
        ∀ (ab : α ⊕ β) (ab' : α' ⊕ β'),
          ab ≍ ab' → ∀ (a : ab.isRight = true) (a' : ab'.isRight = true), a ≍ a' → ab.getRight a ≍ ab'.getRight a'
-- Std.Http.Data.URI.Basic
/-- Appends a single segment to the path. The segment will be automatically percent-encoded when building.
 -/
Std.Http.URI.Builder.appendPathSegment : Std.Http.URI.Builder → String → Std.Http.URI.Builder
-- Mathlib.GroupTheory.Index
AddSubgroup.index_toSubgroup : ∀ {G : Type u_3} [inst : AddGroup G] (H : AddSubgroup G), (AddSubgroup.toSubgroup H).index = H.index
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceGE : Lean.Meta.Simp.Simproc
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ}
  [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ) {s : Set β},
  MeasurableSet s →
    ∫ (b : β) in s, ↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) x ∂ν a = (κ a).real (s ×ˢ Set.Iic x)
-- Mathlib.Tactic.Simps.Basic
/-- Execute the projection renamings (and turning off projections) as specified by `rules`.  -/
Simps.applyProjectionRules : Array Simps.ParsedProjectionData → Array Simps.ProjectionRule → Lean.CoreM (Array Simps.ParsedProjectionData)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushout.eq_desc_of_comp_eq : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → B ⟶ objs j) [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C} (f : B ⟶ X)
  (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f)
  (g : CategoryTheory.Limits.widePushout B objs arrows ⟶ X),
  (∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι arrows j) g = fs j) →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.head arrows) g = f →
      g = CategoryTheory.Limits.WidePushout.desc f fs w
-- Aesop.Index.RulePattern
Aesop.instInhabitedRulePatternIndex.default : Aesop.RulePatternIndex
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.eq_iff_exists : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f]
  {x₁ x₂ : M}, f x₁ = f x₂ ↔ ∃ c, c • x₁ = c • x₂
-- Mathlib.AlgebraicGeometry.Spec
/-- The counit (`SpecΓIdentity.inv.op`) of the adjunction `Γ ⊣ Spec` is an isomorphism.  -/
AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity : AlgebraicGeometry.Spec.toLocallyRingedSpace.rightOp.comp AlgebraicGeometry.LocallyRingedSpace.Γ ≅
  CategoryTheory.Functor.id CommRingCat
-- Lean.Server.References
/-- No definition, no usages  -/
Lean.Lsp.RefInfo.empty : Lean.Lsp.RefInfo
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk0_eq_mk0_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDedekindDomain R]
  {I J : ↥(nonZeroDivisors (Ideal R))},
  ClassGroup.mk0 I = ClassGroup.mk0 J ↔ ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
-- Mathlib.LinearAlgebra.Ray
sameRay_smul_left_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [Module.IsTorsionFree R M] {v : M} {r : R},
  SameRay R (r • v) v ↔ 0 ≤ r ∨ v = 0
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.idealOfSet_closed : ∀ {X : Type u_1} (R : Type u_2) [inst : TopologicalSpace X] [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] [T2Space R] (s : Set X), IsClosed ↑(ContinuousMap.idealOfSet R s)
-- Mathlib.Probability.HasLawExists
MeasureTheory.Measure.exists_hasLaw : ∀ {𝓧 : Type u} {m𝓧 : MeasurableSpace 𝓧} (μ : MeasureTheory.Measure 𝓧),
  ∃ Ω x P X, Measurable X ∧ ProbabilityTheory.HasLaw X μ P
-- Mathlib.Analysis.Normed.Algebra.QuaternionExponential
/-- The odd terms of `expSeries` are real, and correspond to the series for
$\frac{q}{‖q‖} \sin ‖q‖$.  -/
Quaternion.expSeries_odd_of_imaginary : ∀ {q : Quaternion ℝ},
  q.re = 0 →
    ∀ (n : ℕ),
      ((NormedSpace.expSeries ℝ (Quaternion ℝ) (2 * n + 1)) fun x => q) =
        ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1).factorial / ‖q‖) • q
-- Mathlib.Analysis.Calculus.Deriv.ZPow
differentiableWithinAt_zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} (m : ℤ) (x : 𝕜),
  x ≠ 0 ∨ 0 ≤ m → DifferentiableWithinAt 𝕜 (fun x => x ^ m) s x
-- Init.Data.Float.Model.Float32
Float32.Model.instInhabited : Inhabited Float32.Model
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors_prime_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [Nontrivial α] {p : Associates α}
  (hp : Irreducible p) (k : ℕ), (p ^ k).factors = ↑(Multiset.replicate k ⟨p, hp⟩)
-- Init.Data.Float.Model.Float32
/-- Determine whether `a` is less than or equal to `b` according to IEEE rules.

This is not a total ordering, and `≤` is not reflexive.
 -/
Float32.Model.le : Float32.Model → Float32.Model → Bool
-- Mathlib.Order.UpperLower.Closure
LowerSet.sdiff_eq_left : ∀ {α : Type u_1} [inst : Preorder α] {s : LowerSet α} {t : Set α}, s.sdiff t = s ↔ Disjoint (↑s) t
-- Mathlib.Data.EReal.Basic
EReal.instMul : Mul EReal
-- Mathlib.Algebra.Order.Nonneg.Floor
Nonneg.floorSemiring : {α : Type u_1} →
  [inst : Semiring α] →
    [inst_1 : PartialOrder α] → [inst_2 : IsOrderedRing α] → [inst_3 : FloorSemiring α] → FloorSemiring { r // 0 ≤ r }
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.insert : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set α} {a : α},
  s.Intersecting → a ≠ ⊥ → (∀ b ∈ s, ¬Disjoint a b) → (insert a s).Intersecting
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_diff_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.isEmpty = true → (t₁ \ t₂).isEmpty = true
-- Mathlib.Order.InitialSeg
InitialSeg.mk : {α : Type u_4} →
  {β : Type u_5} →
    {r : α → α → Prop} →
      {s : β → β → Prop} →
        (toRelEmbedding : r ↪r s) →
          (∀ (a : α) (b : β), s b (toRelEmbedding a) → b ∈ Set.range ⇑toRelEmbedding) → InitialSeg r s
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.eval_map : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I)
  {X Y : (i : I) → C i} (α : X ⟶ Y), (CategoryTheory.Pi.eval C i).map α = α i
-- Mathlib.Data.Set.Operations
Set.mem_diagonal : ∀ {α : Type u} (x : α), (x, x) ∈ Set.diagonal α
-- Mathlib.GroupTheory.Finiteness
/-- Finite product of finitely generated submonoids is finitely generated.  -/
Submonoid.FG.pi : ∀ {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [inst : (i : ι) → Monoid (M i)] {P : (i : ι) → Submonoid (M i)},
  (∀ (i : ι), (P i).FG) → (Submonoid.pi Set.univ P).FG
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  {X Y : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)} (f : X ⟶ Y) (n : α),
  ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.map f).f.f n = (f.f n).f
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
Subgroup.isOpen_of_isClosed_of_finiteIndex : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G] (H : Subgroup G)
  [H.FiniteIndex], IsClosed ↑H → IsOpen ↑H
-- Mathlib.Topology.MetricSpace.Thickening
/-- The frontier of the closed thickening of a set is contained in an `Metric.infEDist` level
set.  -/
Metric.frontier_cthickening_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α) {δ : ℝ},
  frontier (Metric.cthickening δ E) ⊆ {x | Metric.infEDist x E = ENNReal.ofReal δ}
-- Mathlib.Data.Finset.Lattice.Fold
/-- Computing `inf` in a subtype (closed under `inf`) is the same as computing it in `α`.  -/
Finset.inf_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {P : α → Prop} {Ptop : P ⊤}
  {Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)} (t : Finset β) (f : β → { x // P x }), ↑(t.inf f) = t.inf fun x => ↑(f x)
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.CasesTypes.find? : Lean.Meta.Grind.CasesTypes → Lean.Name → Option Bool
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.coe_bipartiteBelow : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Finset α) (b : β) [inst : (a : α) → Decidable (r a b)],
  ↑(Finset.bipartiteBelow r s b) = {a | a ∈ s ∧ r a b}
-- Mathlib.Data.Quot
Quotient.lift_surjective_iff : ∀ {α : Sort u_3} {β : Sort u_4} {s : Setoid α} (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b),
  Function.Surjective (Quotient.lift f h) ↔ Function.Surjective f
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ι_D₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C}
  (h_1 : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h)
      (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') h_1) =
    CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i₁ i₂ i₁₂') h_1
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.sum_support_of : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (x : DirectSum ι fun i => β i),
  ∑ i ∈ DFinsupp.support x, (DirectSum.of β i) (x i) = x
-- Mathlib.RingTheory.Ideal.Pointwise
/-- Assume that `M` and `N` are isomorphic and act in a compatible way on `R`, then for any
ideal `I` of `R`, the inertia subgroup of `I` in `M` is isomorphic to the inertia subgroup
of `I` in `N`.
 -/
Ideal.inertiaEquiv : {M : Type u_1} →
  [inst : Group M] →
    {N : Type u_4} →
      [inst_1 : Group N] →
        {R : Type u_5} →
          [inst_2 : Ring R] →
            [inst_3 : MulSemiringAction M R] →
              [inst_4 : MulSemiringAction N R] →
                (I : Ideal R) →
                  (e : M ≃* N) → (∀ (m : M) (x : R), e m • x = m • x) → ↥(Ideal.inertia M I) ≃* ↥(Ideal.inertia N I)
-- Plausible.Testable
Plausible.instInhabitedTestResult : {a : Prop} → Inhabited (Plausible.TestResult a)
-- Mathlib.RingTheory.Kaehler.TensorProduct
/-- (Implementation).
The `S`-derivation `B = S ⊗[R] A` to `S ⊗[R] Ω[A⁄R]` sending `a ⊗ b` to `a ⊗ d b`.  -/
KaehlerDifferential.derivationTensorProduct : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      (B : Type u_4) →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : CommRing A] →
                [inst_4 : CommRing B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      [inst_7 : Algebra A B] →
                        [inst_8 : Algebra S B] →
                          [inst_9 : IsScalarTower R A B] →
                            [inst_10 : IsScalarTower R S B] →
                              [h : Algebra.IsPushout R S A B] → Derivation S B (TensorProduct R S Ω[A⁄R])
-- Lean.Message
Lean.instToJsonBaseMessage.toJson : {α : Type u_1} → [Lean.ToJson α] → Lean.BaseMessage α → Lean.Json
-- Mathlib.NumberTheory.Cyclotomic.Gal
/-- The `MulEquiv` that takes an automorphism `f` to the element `k : (ZMod n)ˣ` such that
`f μ = μ ^ k` for any root of unity `μ`. A strengthening of `IsPrimitiveRoot.autToPow`.  -/
IsCyclotomicExtension.autEquivPow : {n : ℕ} →
  [NeZero n] →
    {K : Type u_1} →
      [inst : Field K] →
        (L : Type u_2) →
          [inst_1 : CommRing L] →
            [IsDomain L] →
              [inst_3 : Algebra K L] →
                [IsCyclotomicExtension {n} K L] → Irreducible (Polynomial.cyclotomic n K) → (L ≃ₐ[K] L) ≃* (ZMod n)ˣ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α}, ∅.contains k = false
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_congr' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F),
  MeasureTheory.FinMeasAdditive μ T →
    ∀ {f g : MeasureTheory.SimpleFunc α E},
      MeasureTheory.Integrable (⇑f) μ →
        MeasureTheory.Integrable (⇑g) μ →
          (Pairwise fun x y => T (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0) →
            MeasureTheory.SimpleFunc.setToSimpleFunc T f = MeasureTheory.SimpleFunc.setToSimpleFunc T g
-- Mathlib.GroupTheory.SemidirectProduct
/-- The semidirect product of groups `N` and `G`, given a map `φ` from `G` to the automorphism
group of `N`. It is the product of sets with the group operation
`⟨n₁, g₁⟩ * ⟨n₂, g₂⟩ = ⟨n₁ * φ g₁ n₂, g₁ * g₂⟩`  -/
SemidirectProduct : (N : Type u_1) → (G : Type u_2) → [inst : Group N] → [inst_1 : Group G] → (G →* MulAut N) → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Localization.SmallHom
/-- The element in `SmallHom W X Y` induced by `f : X ⟶ Y`.  -/
CategoryTheory.Localization.SmallHom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      {X Y : C} →
        [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] →
          (X ⟶ Y) → CategoryTheory.Localization.SmallHom W X Y
-- Mathlib.Probability.Kernel.Composition.KernelLemmas
ProbabilityTheory.Kernel.id_parallelComp_comp_parallelComp_id : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {T : Type u_4} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} {mT : MeasurableSpace T} {κ : ProbabilityTheory.Kernel X Y}
  {η : ProbabilityTheory.Kernel Z T} [ProbabilityTheory.IsSFiniteKernel κ],
  (ProbabilityTheory.Kernel.id.parallelComp κ).comp (η.parallelComp ProbabilityTheory.Kernel.id) = η.parallelComp κ
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.sInter.eq_1 : ∀ (x : ZFSet.{u_1}), x.sInter = ZFSet.sep (fun y => ∀ z ∈ x, y ∈ z) x.sUnion
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationIsRightAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C),
  ((CategoryTheory.evaluation C D).obj c).IsRightAdjoint