mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_eq_get! : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)] {h : a ∈ m}, m.get a h = m.get! a
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralValue.eq_1 : ∀ {R : Type u_1} [inst : SeminormedRing R] (p : Polynomial R), spectralValue p = iSup (spectralValueTerms p)
-- Lean.Meta.Tactic.Grind.Types
/-- Generated while instantiating an extensionality theorem with name `declName`  -/
Lean.Meta.Grind.SplitSource.ext : Lean.Name → Lean.Meta.Grind.SplitSource
-- Lean.Parser.Basic
Lean.Parser.hygieneInfoFn : Lean.Parser.ParserFn
-- Std.Http.Data.Method
Std.Http.Method.move.sizeOf_spec : sizeOf Std.Http.Method.move = 1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isEmpty_eq_false_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m.isEmpty = false ↔ ¬m = ∅
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.ClosureState.mk.sizeOf_spec : ∀ (newLocalDecls localDecls newLetDecls : Array Lean.LocalDecl) (exprArgs : Array Lean.Expr),
  sizeOf
      { newLocalDecls := newLocalDecls, localDecls := localDecls, newLetDecls := newLetDecls, exprArgs := exprArgs } =
    1 + sizeOf newLocalDecls + sizeOf localDecls + sizeOf newLetDecls + sizeOf exprArgs
-- Batteries.Logic
/-- **Alias** of the forward direction of `Decidable.not_forall`. -/
Decidable.exists_not_of_not_forall : ∀ {α : Sort u_1} {p : α → Prop} [Decidable (∃ x, ¬p x)] [(x : α) → Decidable (p x)], (¬∀ (x : α), p x) → ∃ x, ¬p x
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The composition of the isomorphism `pullbackSpecIso R S T` (from the pullback of
`Spec S ⟶ Spec R` and `Spec T ⟶ Spec R` to `Spec (S ⊗[R] T)`) with the morphism
`Spec (S ⊗[R] T) ⟶ Spec T` obtained by applying `Spec.map` to the ring morphism `t ↦ 1 ⊗ₜ[R] t`
is the second projection.
 -/
AlgebraicGeometry.pullbackSpecIso_hom_snd : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).hom
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) =
    CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))
-- Init.Data.List.Attach
List.pmap_append' : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {l₁ l₂ : List α} (h₁ : ∀ a ∈ l₁, p a)
  (h₂ : ∀ a ∈ l₂, p a), List.pmap f (l₁ ++ l₂) ⋯ = List.pmap f l₁ h₁ ++ List.pmap f l₂ h₂
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.instCommGroup.eq_1 : ∀ (A : Type u_2) (E : Type u_6) [inst : Monoid A] [inst_1 : TopologicalSpace A] [inst_2 : CommGroup E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalGroup E],
  ContinuousMonoidHom.instCommGroup A E =
    { toMonoid := inferInstance.toMonoid, inv := fun f => (ContinuousMonoidHom.inv E).comp f,
      div := fun f g => { toMonoidHom := divMonoidHom, continuous_toFun := ⋯ }.comp (f.prod g), zpow := zpowRec,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯, mul_comm := ⋯ }
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.RecArgCandidate.mk.sizeOf_spec : ∀ (group : Lean.Elab.Structural.IndGroupInst) (comb : Array Lean.Elab.Structural.RecArgInfo),
  sizeOf { group := group, comb := comb } = 1 + sizeOf group + sizeOf comb
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
/-- If `S` contains `0` then the localization at `S` is trivial.  -/
Submonoid.LocalizationMap.subsingleton : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  (f : S.LocalizationMap N), 0 ∈ S → Subsingleton N
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
/-- The type of finite-index normal additive subgroups of an additive group.  -/
FiniteIndexNormalAddSubgroup : (G : Type u_1) → [AddGroup G] → Type u_1
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValueD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] {fallback : γ} {f : α → β → Option γ}
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      Std.Internal.List.getValueD k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l)
          fallback =
        ((Std.Internal.List.getValue? k l).pbind fun v h => f (Std.Internal.List.getKey k l ⋯) v).getD fallback
-- Mathlib.Data.Finsupp.Order
Finsupp.tsub_apply : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : CanonicallyOrderedAdd α]
  [inst_3 : Sub α] [inst_4 : OrderedSub α] (f g : ι →₀ α) (a : ι), (f - g) a = f a - g a
-- Mathlib.NumberTheory.RamificationInertia.Galois
/-- If `p` is a maximal ideal of `A`, `P` and `Q` are prime ideals
lying over `p`, then there exists `σ ∈ Aut (B / A)` such that `σ P = Q`. In other words,
the Galois group `Gal(L / K)` acts transitively on the set of all prime ideals lying over `p`.  -/
Ideal.exists_smul_eq_of_isGaloisGroup : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (p : Ideal A)
  (P Q : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] [hQp : Q.IsPrime] [Q.LiesOver p] (G : Type u_3)
  [inst_4 : Group G] [Finite G] [inst_6 : MulSemiringAction G B] [IsGaloisGroup G A B], ∃ σ, σ • P = Q
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_subset_Ico_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], Finset.Ioo a b ⊆ Finset.Ico a b
-- Mathlib.Order.CompleteLattice.Defs
instCompleteSemilatticeSupOrderDualOfCompleteSemilatticeInf : {α : Type u_8} → [CompleteSemilatticeInf α] → CompleteSemilatticeSup αᵒᵈ
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
/-- An invertible matrix yields a linear equivalence from the free module to itself.

See `Matrix.toLinearEquiv` for the same map on arbitrary modules.
 -/
Matrix.toLinearEquiv' : {n : Type u_1} →
  [inst : Fintype n] →
    {R : Type u_2} →
      [inst_1 : CommRing R] → [inst_2 : DecidableEq n] → (P : Matrix n n R) → Invertible P → (n → R) ≃ₗ[R] n → R
-- Init.Prelude
/-- The context name, a globally unique prefix.  -/
Lean.MacroScopesView.ctx : Lean.MacroScopesView → Lean.Name
-- Mathlib.Tactic.Translate.Core
/-- Linter to check whether the user correctly specified that the translated declaration already
exists  -/
Mathlib.Tactic.Translate.linter.translateExisting : Lean.Option Bool
-- Mathlib.Order.Basic
min_def_lt : ∀ {α : Type u_2} [inst : LinearOrder α] (a b : α), min a b = if a < b then a else b
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
IsCyclotomicExtension.zeta_pow : ∀ (n : ℕ) [inst : NeZero n] (A : Type w) (B : Type z) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra A B]
  [inst_4 : IsCyclotomicExtension {n} A B], IsCyclotomicExtension.zeta n A B ^ n = 1
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.corepresentable_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v))
  {G : CategoryTheory.Functor C (Type v)} (i : F ≅ G) [F.IsCorepresentable], G.IsCorepresentable
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.extensionHom.eq_1 : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α] [inst_3 : IsUniformAddGroup α]
  {β : Type u} [inst_4 : UniformSpace β] [inst_5 : Ring β] [inst_6 : IsUniformAddGroup β] [inst_7 : IsTopologicalRing β]
  (f : α →+* β) (hf : Continuous ⇑f) [inst_8 : CompleteSpace β] [inst_9 : T0Space β],
  UniformSpace.Completion.extensionHom f hf =
    { toFun := UniformSpace.Completion.extension ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Batteries.Data.Fin.Lemmas
Fin.findSome?_succ_of_isNone : ∀ {n : ℕ} {α : Type u_1} {f : Fin (n + 1) → Option α},
  (f 0).isNone = true → Fin.findSome? f = Fin.findSome? fun x => f x.succ
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E → F) (s : Set E) (x : E),
  DifferentiableWithinAt 𝕜 f s x = ∃ f', HasFDerivWithinAt f f' s x
-- Lean.LoadDynlib
/-- Returns the symbol of the dynamic library with the specified name (if any).   -/
Lean.Dynlib.get? : (dynlib : Lean.Dynlib) → String → Option dynlib.Symbol
-- Mathlib.Topology.ContinuousOn
continuousOn_of_locally_continuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  (∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)) → ContinuousOn f s
-- Mathlib.Topology.Instances.AddCircle.Real
ZMod.toAddCircle.congr_simp : ∀ {N : ℕ} [inst : NeZero N], ZMod.toAddCircle = ZMod.toAddCircle
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.mk.inj : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} {toHom : A →g B}
  {injective' : Function.Injective ⇑toHom} {toHom_1 : A →g B} {injective'_1 : Function.Injective ⇑toHom_1},
  { toHom := toHom, injective' := injective' } = { toHom := toHom_1, injective' := injective'_1 } → toHom = toHom_1
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- candidates are bounded by `maxVar X Y`  -/
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidates_dist_bound : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {f : GromovHausdorff.ProdSpaceFun✝ X Y},
  f ∈ GromovHausdorff.candidates X Y → ∀ {x y : X ⊕ Y}, f (x, y) ≤ ↑(GromovHausdorff.maxVar✝ X Y) * dist x y
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' : Φ.LeftResolution X₂} {x y : L.Hom L'}, x.f = y.f → x = y
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_eq_of_dist_bounded : ∀ {f g : CircleDeg1Lift} (C : ℝ),
  (∀ (n : ℕ), dist ((f ^ n) 0) ((g ^ n) 0) ≤ C) → f.translationNumber = g.translationNumber
-- Mathlib.Order.Category.PartOrd
PartOrd.coe_comp : ∀ {X Y Z : PartOrd} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Init.Data.Int.Bitwise.Basic
Int.instHShiftLeftNat : HShiftLeft ℤ ℕ ℤ
-- Init.Data.SInt.Lemmas
Int16.right_eq_add : ∀ {a b : Int16}, b = a + b ↔ a = 0
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.level.parenthesizer : Lean.PrettyPrinter.CategoryParenthesizer
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateReturn! : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Lean.FVarId → Lean.Compiler.LCNF.Code pu
-- Lean.Parser.Term
/-- Synthesizes a default value for a structure, making use of `Inhabited` instances for
missing fields, as well as `Inhabited` instances for parent structures.
 -/
Lean.Parser.Term.structInstDefault : Lean.Parser.Parser
-- Mathlib.Data.Multiset.FinsetOps
Multiset.mem_ndinter : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} {a : α}, a ∈ s.ndinter t ↔ a ∈ s ∧ a ∈ t
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapCompIso_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B] (F : CategoryTheory.LaxFunctor B' B) {a b c : B'} (f : a ⟶ b)
  (g : b ⟶ c),
  ((CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid F).mapCompIso f g).hom =
    CategoryTheory.inv (F.mapComp f g)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  ProbabilityTheory.IsZeroOrMarkovKernel κ.fst
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.card_le_multiplicity : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Finset E},
  (∀ c ∈ s, ‖c‖ ≤ 2) → (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖) → s.card ≤ Besicovitch.multiplicity E
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.kernelSequence_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShortComplex.kernelSequence f).f = CategoryTheory.Limits.kernel.ι f
-- Lean.Declaration
Lean.InductiveType.name : Lean.InductiveType → Lean.Name
-- Batteries.Data.Fin.Fold
Fin.dfoldl.eq_1 : ∀ (n : ℕ) (α : Fin (n + 1) → Type u_1) (f : (i : Fin n) → α i.castSucc → α i.succ) (init : α 0),
  Fin.dfoldl n α f init = Fin.dfoldlM n α f init
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.continuous_of_continuous_uncurry : ∀ {B : Type u_3} {C : Type u_4} [inst : Monoid B] [inst_1 : Monoid C] [inst_2 : TopologicalSpace B]
  [inst_3 : TopologicalSpace C] {A : Type u_7} [inst_4 : TopologicalSpace A] (f : A → B →ₜ* C),
  Continuous (Function.uncurry fun x y => (f x) y) → Continuous f
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.injective_type₁' : ∀ {X : SSet} {A : X.Subcomplex} (self : A.PairingCore) {s t : self.ι},
  { dim := self.dim s + 1, simplex := self.simplex s } = { dim := self.dim t + 1, simplex := self.simplex t } → s = t
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.map.eq_1 : ∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : FunLike F (Polynomial R) (Polynomial S)] [inst_3 : MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))),
  RatFunc.map φ hφ =
    {
      toFun := fun f =>
        f.liftOn
          (fun n d =>
            if h : φ d ∈ nonZeroDivisors (Polynomial S) then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ }
            else 0)
          ⋯,
      map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.eval : ∀ {ι : Type x} {α : ι → Type u} [inst : (i : ι) → PseudoEMetricSpace (α i)] [inst_1 : Fintype ι] (i : ι),
  LipschitzWith 1 (Function.eval i)
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- The isomorphism between the roots of unity and the center of the special linear group.  -/
SpecialLinearGroup.centerEquivRootsOfUnity : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] →
          [Module.Free R V] →
            [Module.Finite R V] →
              ↥(Subgroup.center (SpecialLinearGroup R V)) ≃* ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
-- Init.Data.Random
StdGen.mk.inj : ∀ {s1 s2 s1_1 s2_1 : ℕ}, { s1 := s1, s2 := s2 } = { s1 := s1_1, s2 := s2_1 } → s1 = s1_1 ∧ s2 = s2_1
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The bijection between ideals of `R` dividing `I` and the ideals of `A` dividing `J` induced by
an isomorphism `f : R/I ≅ A/J`.  -/
IsDedekindDomain.idealFactorsEquivOfQuotEquiv : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [IsDedekindDomain A] →
          {I : Ideal R} → {J : Ideal A} → [IsDedekindDomain R] → R ⧸ I ≃+* A ⧸ J → ↑{p | p ∣ I} ≃o ↑{p | p ∣ J}
-- Init.Data.List.TakeDrop
List.takeWhile_append_of_pos : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α},
  (∀ a ∈ l₁, p a = true) → List.takeWhile p (l₁ ++ l₂) = l₁ ++ List.takeWhile p l₂
-- Aesop.Tree.Data
Aesop.GoalData.origin : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Aesop.GoalOrigin
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- The natural homeomorphism between `Snowflaking X α hα₀ hα₁` and `X`.  -/
Metric.Snowflaking.homeomorph : {X : Type u_1} →
  {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → [inst : TopologicalSpace X] → Metric.Snowflaking X α hα₀ hα₁ ≃ₜ X
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
/-- The property that a simplex is uniquely a `1`-codimensional face of another simplex  -/
SSet.S.IsUniquelyCodimOneFace : {X : SSet} → X.S → X.S → Prop
-- Mathlib.Algebra.Torsor.Basic
sdiv_smul_comm : ∀ {G : Type u_1} {P : Type u_2} [inst : CommGroup G] [inst_1 : Torsor G P] (p₁ p₂ p₃ : P),
  (p₁ /ₛ p₂) • p₃ = (p₃ /ₛ p₂) • p₁
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.sigmaSigmaIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C)
  [inst_1 : ∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)]
  [inst_2 : CategoryTheory.Limits.HasCoproduct fun i => ∐ g i],
  (CategoryTheory.Limits.sigmaSigmaIso f g).hom =
    CategoryTheory.Limits.Sigma.desc fun i =>
      CategoryTheory.Limits.Sigma.desc fun x => CategoryTheory.Limits.Sigma.ι (fun p => g p.fst p.snd) ⟨i, x⟩
-- Mathlib.Topology.Sheaves.EtaleSpace
/-- Let `F` be a presheaf with the following property.

For each `x`, there exists an open neighborhood `U ∋ x` such that for each `y ∈ U`,
the map `Presheaf.germ F U y hyU` from sections of `F` over `U` to the stalk at `y`
is bijective.

Then the projection from the etale space of `F` to the base is a covering map.  -/
TopCat.Presheaf.EtaleSpace.isCoveringMap_base : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X}
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)],
  (∀ (x : ↑X),
      ∃ U,
        x ∈ U ∧ ∀ (y : ↑X) (hyU : y ∈ U), Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (F.germ U y hyU))) →
    IsCoveringMap TopCat.Presheaf.EtaleSpace.base
-- Std.Time.Date.Unit.Month
/-- The ordinal value representing the month of April.
 -/
Std.Time.Month.Ordinal.april : Std.Time.Month.Ordinal
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
rieszContent.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : LocallyCompactSpace X]
  (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal),
  rieszContent Λ = { toFun := rieszContentAux Λ, mono' := ⋯, sup_disjoint' := ⋯, sup_le' := ⋯ }
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- If `G` is a Galois group for `C/A`, and the normal subgroup `N ≤ G` is a Galois group for
`C/B`, then the quotient `G ⧸ N` is a Galois group for `B/A`.  -/
IsGaloisGroup.quotient : ∀ (G : Type u_1) [inst : Group G] (A : Type u_5) (B : Type u_6) (C : Type u_7) [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [IsDomain C] [inst_5 : Algebra A B] [inst_6 : Algebra A C]
  [inst_7 : Algebra B C] [FaithfulSMul A B] [FaithfulSMul B C] [IsScalarTower A B C] [Finite G] (N : Subgroup G)
  [inst_12 : N.Normal] [inst_13 : MulSemiringAction G C] [hG : IsGaloisGroup G A C] [inst_14 : MulSemiringAction G B]
  [inst_15 : MulSemiringAction (G ⧸ N) B] [SMulCommClass (G ⧸ N) A B] [SMulDistribClass G B C]
  [IsScalarTower G (G ⧸ N) B] [IsGaloisGroup (↥N) B C], IsGaloisGroup (G ⧸ N) A B
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.instCategoryOppositeShift : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (A : Type u_2) →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] → CategoryTheory.Category.{v_1, u_1} (CategoryTheory.OppositeShift C A)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_le_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : t.contains k = true), (cmp (t.minKey ⋯) k).isLE = true
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.instStarMulId : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → [CompleteSpace E] → StarMul (E →L[𝕜] E)
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsPreLocalizingSequence.isLocalizingSequence_biInf : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : ConditionallyCompleteLinearOrderBot ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  {𝓕 : MeasureTheory.Filtration ι mΩ} [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι]
  {τ : ℕ → Ω → WithTop ι} [𝓕.IsRightContinuous],
  ProbabilityTheory.IsPreLocalizingSequence 𝓕 τ P →
    ProbabilityTheory.IsLocalizingSequence 𝓕 (fun i ω => ⨅ j, ⨅ (_ : j ≥ i), τ j ω) P
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Break.runK.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.homologyFunctor_shift : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] (n : ℤ),
  (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shift n =
    HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) n
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrable_comap : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X},
  MeasurableSet s →
    (MeasureTheory.LocallyIntegrable (fun x => f ↑x) (MeasureTheory.Measure.comap Subtype.val μ) ↔
      MeasureTheory.LocallyIntegrableOn f s μ)
-- Mathlib.Logic.Denumerable
Nat.Subtype.succ_le_of_lt : ∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s] {x y : ↑s}, y < x → Nat.Subtype.succ y ≤ x
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- If a vector is central, then its right action is measurable when its left
action is.  -/
AddOpposite.instMeasurableConstVAdd : ∀ {M : Type u_2} {α : Type u_4} {m : MeasurableSpace α} [inst : VAdd M α] [inst_1 : VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α]
  [MeasurableConstVAdd M α], MeasurableConstVAdd Mᵃᵒᵖ α
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.le_mul_right : ∀ {a b : Cardinal.{u_1}}, b ≠ 0 → a ≤ a * b
-- Std.Http.Data.URI.Encoding
/-- Checks if all characters in a `ByteArray` are allowed in an encoded query parameter. Allows '+' as an
alternative encoding for space (application/x-www-form-urlencoded).
 -/
Std.Http.URI.IsAllowedEncodedQueryChars : (UInt8 → Bool) → ByteArray → Prop
-- Init.Data.List.Sublist
List.isInfixOf_internal_iff_isInfix : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ : List α}, l₁.isInfixOf_internal l₂ = true ↔ l₁ <:+: l₂
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β},
  m.WF →
    (m.modify k f).getD k' fallback =
      if (k == k') = true then (Option.map f m[k]?).getD fallback else m.getD k' fallback
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.closure_induction_right : ∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M} {motive : (m : M) → m ∈ AddSubmonoid.closure s → Prop},
  motive 0 ⋯ →
    (∀ (x : M) (hx : x ∈ AddSubmonoid.closure s) (y : M) (hy : y ∈ s), motive x hx → motive (x + y) ⋯) →
      ∀ {x : M} (h : x ∈ AddSubmonoid.closure s), motive x h