mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_associator_inv_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {a b c d : CategoryTheory.Bicategory.InducedBicategory C F} (x : a ⟶ b) (y : b ⟶ c) (z : c ⟶ d),
  (CategoryTheory.Bicategory.associator x y z).inv.hom = (CategoryTheory.Bicategory.associator x.hom y.hom z.hom).inv
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.weaken_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K L : CategoryTheory.Precoverage C} {X : C}
  (E : K.ZeroHypercover X) (h : K ≤ L), (E.weaken h).toPreZeroHypercover = E.toPreZeroHypercover
-- Mathlib.RingTheory.FreeCommRing
/-- **Alias** of `freeCommRingPUnitEquivPolynomialInt`.

---

The free commutative ring on a type with one term is isomorphic to `ℤ[X]`.  -/
freeCommRingPunitEquivPolynomialInt : FreeCommRing PUnit.{u + 1} ≃+* Polynomial ℤ
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.lie_h_h : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (self : LieAlgebra.Basis ι H) (i j : ι), ⁅self.h i, self.h j⁆ = 0
-- Mathlib.Topology.Neighborhoods
/-- If a predicate is true in a neighbourhood of `x`, then for `y` sufficiently close
to `x` this predicate is true in a neighbourhood of `y`.  -/
Filter.Eventually.eventually_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {p : X → Prop},
  (∀ᶠ (y : X) in nhds x, p y) → ∀ᶠ (y : X) in nhds x, ∀ᶠ (x : X) in nhds y, p x
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
hasSum_sum_range_mul_of_summable_norm' : ∀ {R : Type u_1} [inst : NormedRing R] {f g : ℕ → R},
  (Summable fun x => ‖f x‖) →
    Summable f →
      (Summable fun x => ‖g x‖) →
        Summable g → HasSum (fun n => ∑ k ∈ Finset.range (n + 1), f k * g (n - k)) ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n)
-- Mathlib.Topology.Instances.CantorSet
_private.Mathlib.Topology.Instances.CantorSet.0.preCantorSet.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Topology.ShrinkingLemma
/-- If two partial refinements `v₁`, `v₂` belong to a chain (hence, they are comparable)
and `i` belongs to the carriers of both partial refinements, then `v₁ i = v₂ i`.  -/
ShrinkingLemma.PartialRefinement.apply_eq_of_chain : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  {c : Set (ShrinkingLemma.PartialRefinement u s p)},
  IsChain (fun x1 x2 => x1 ≤ x2) c →
    ∀ {v₁ v₂ : ShrinkingLemma.PartialRefinement u s p},
      v₁ ∈ c → v₂ ∈ c → ∀ {i : ι}, i ∈ v₁.carrier → i ∈ v₂.carrier → v₁.toFun i = v₂.toFun i
-- Mathlib.NumberTheory.LSeries.Basic
LSeriesHasSum_iff : ∀ {f : ℕ → ℂ} {s a : ℂ}, LSeriesHasSum f s a ↔ LSeriesSummable f s ∧ LSeries f s = a
-- Batteries.Data.Array.Lemmas
Array.toList_erase : ∀ {α : Type u_1} [inst : BEq α] (l : Array α) (a : α), (l.erase a).toList = l.toList.erase a
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The multispan index for `MultispanShape.ofLinearOrder ι` deduced from
a multispan index for `MultispanShape.prod ι` when `ι` is linearly ordered.  -/
CategoryTheory.Limits.MultispanIndex.toLinearOrder : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} →
      CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C →
        [inst_1 : LinearOrder ι] →
          CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι) C
-- Init.Internal.Order.Basic
Lean.Order.CCPO.mk : {α : Sort u} →
  [toPartialOrder : Lean.Order.PartialOrder α] →
    (∀ {c : α → Prop}, Lean.Order.chain c → Exists (Lean.Order.is_sup c)) → Lean.Order.CCPO α
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.response.inj : ∀ {id : Lean.JsonRpc.RequestID} {result : Lean.Json} {id_1 : Lean.JsonRpc.RequestID} {result_1 : Lean.Json},
  Lean.JsonRpc.Message.response id result = Lean.JsonRpc.Message.response id_1 result_1 → id = id_1 ∧ result = result_1
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) (c : F), deriv (fun x => c) x = 0
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.antidiagonal_zero : ∀ {A : Type u_1} [inst : AddCommMonoid A] [inst_1 : PartialOrder A] [CanonicallyOrderedAdd A]
  [inst_3 : Finset.HasAntidiagonal A], Finset.HasAntidiagonal.antidiagonal 0 = {(0, 0)}
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.instDescendsAlongOfIsStableUnderBaseChangeOfHasOfPrecompPropertyOfRespectsRight : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C}
  [Q.IsStableUnderBaseChange] [P.HasOfPrecompProperty Q] [P.RespectsRight Q], P.DescendsAlong Q
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.eq_of_le_of_ne_top : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) [Ring.KrullDimLE 1 ↥A] {B : ValuationSubring K},
  A ≤ B → B ≠ ⊤ → A = B
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAddMonoidMorphism.mk : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              {H' : Type u_5} →
                [inst_4 : TopologicalSpace H'] →
                  {E' : Type u_6} →
                    [inst_5 : NormedAddCommGroup E'] →
                      [inst_6 : NormedSpace 𝕜 E'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {n : WithTop ℕ∞} →
                              {G : Type u_8} →
                                [inst_7 : TopologicalSpace G] →
                                  [inst_8 : ChartedSpace H G] →
                                    [inst_9 : AddMonoid G] →
                                      {G' : Type u_9} →
                                        [inst_10 : TopologicalSpace G'] →
                                          [inst_11 : ChartedSpace H' G'] →
                                            [inst_12 : AddMonoid G'] →
                                              (toAddMonoidHom : G →+ G') →
                                                ContMDiff I I' n (↑toAddMonoidHom).toFun →
                                                  ContMDiffAddMonoidMorphism I I' n G G'
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- If `G` is monadic, it creates colimits of `G`-split pairs. This is the "boring" direction of Beck's
monadicity theorem, the converse is given in `monadicOfCreatesGSplitCoequalizers`.
 -/
CategoryTheory.Monad.createsGSplitCoequalizersOfMonadic : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        (G : CategoryTheory.Functor D C) →
          [CategoryTheory.MonadicRightAdjoint G] →
            ⦃A B : D⦄ →
              (f g : A ⟶ B) →
                [G.IsSplitPair f g] → CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair f g) G
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.exists_rep : ∀ {M : Type u_1} [inst : Monoid M] (a : Associates M), ∃ a0, Associates.mk a0 = a
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.empty_notMem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E}, ∅ ∉ K.faces
-- Mathlib.AlgebraicGeometry.Sites.BigZariski
AlgebraicGeometry.Scheme.affineOneHypercover_toPreOneHypercover_toPreZeroHypercover : ∀ (X : AlgebraicGeometry.Scheme), X.affineOneHypercover.toPreZeroHypercover = X.affineCover.toPreZeroHypercover
-- Mathlib.RingTheory.Ideal.Maps
/-- The kernel of a homomorphism to a division ring is a maximal ideal.  -/
RingHom.ker_isMaximal_of_surjective : ∀ {R : Type u_1} {K : Type u_2} {F : Type u_3} [inst : Ring R] [inst_1 : DivisionRing K] [inst_2 : FunLike F R K]
  [inst_3 : RingHomClass F R K] (f : F), Function.Surjective ⇑f → (RingHom.ker f).IsMaximal
-- Init.Data.Vector.OfFn
/-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #v[f i, ..., f(n - 1)]`  -/
_private.Init.Data.Vector.OfFn.0.Vector.ofFnM.go : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    {n : ℕ} → [Monad m] → (Fin n → m α) → (i : ℕ) → i ≤ n → (acc : Array α) → acc.size = i → m (Vector α n)
-- Mathlib.FieldTheory.SeparableDegree
/-- The `Field.finSepDegree F E` is equal to the cardinality of `E →ₐ[F] K`
if `E = F(S)` such that every element
`s` of `S` is integral (= algebraic) over `F` and whose minimal polynomial splits in `K`.  -/
Field.finSepDegree_eq_of_adjoin_splits : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] {S : Set E},
  IntermediateField.adjoin F S = ⊤ →
    (∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) →
      Field.finSepDegree F E = Nat.card (E →ₐ[F] K)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfc_subset : ∀ (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra 𝕜 A] [inst_4 : TopologicalSpace A] [inst_5 : StarModule 𝕜 A]
  [inst_6 : ContinuousFunctionalCalculus 𝕜 A p] [inst_7 : IsTopologicalRing A] [inst_8 : ContinuousStar A] {a : A},
  p a → (Set.range fun x => cfc x a) ⊆ ↑(StarAlgebra.elemental 𝕜 a)
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Ineq.WithStrictness.lt.inj : ∀ {strict strict_1 : Bool},
  Mathlib.Ineq.WithStrictness.lt strict = Mathlib.Ineq.WithStrictness.lt strict_1 → strict = strict_1
-- Lean.Meta.Iterator
/-- Provides an interface for iterating over values that are bundled with the `Meta` state
they are valid in.
 -/
Lean.Meta.Iterator : Type → Type
-- Mathlib.Topology.Compactification.StoneCech
/-- The value of `Ultrafilter.extend f` on an ultrafilter `b` is the
unique limit of the ultrafilter `b.map f` in `γ`.  -/
ultrafilter_extend_eq_iff : ∀ {α : Type u} {γ : Type u_1} [inst : TopologicalSpace γ] [T2Space γ] [CompactSpace γ] {f : α → γ} {b : Ultrafilter α}
  {c : γ}, Ultrafilter.extend f b = c ↔ ↑(Ultrafilter.map f b) ≤ nhds c
-- Mathlib.Topology.Homeomorph.Defs
/-- The inverse map of a homeomorphism is a continuous function.  -/
Homeomorph.continuous_invFun : ∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (self : X ≃ₜ Y),
  Continuous self.invFun
-- Init.SimpLemmas
iff_or_self : ∀ {a b : Prop}, (b ↔ a ∨ b) ↔ a → b
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Exact.assumption : ∀ {σs : List (Type u)} {P P' A : Std.Do.SPred σs}, (P ⊣⊢ₛ P' ∧ A) → P ⊢ₛ A
-- Init.Data.SInt.Lemmas
Int16.add_left_neg : ∀ (a : Int16), -a + a = 0
-- Mathlib.Analysis.BoxIntegral.Basic
/-- If `f` is integrable on a box `I`, then integral sums of `f` over tagged prepartitions
that cover exactly a subbox `J ≤ I` tend to the integral of `f` over `J` along `l`.  -/
BoxIntegral.Integrable.tendsto_integralSum_toFilteriUnion_single : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I J : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  [CompleteSpace F],
  BoxIntegral.Integrable I l f vol →
    ∀ (hJ : J ≤ I),
      Filter.Tendsto (BoxIntegral.integralSum f vol)
        (BoxIntegral.IntegrationParams.toFilteriUnion I (BoxIntegral.Prepartition.single I J hJ))
        (nhds (BoxIntegral.integral J l f vol))
-- Mathlib.Algebra.BigOperators.Field
Finset.dens_disjiUnion : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype β] (s : Finset α) (t : α → Finset β) (h : (↑s).PairwiseDisjoint t),
  (s.disjiUnion t h).dens = ∑ a ∈ s, (t a).dens
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.pow : Lean.Grind.CommRing.Expr → ℕ → Lean.Grind.CommRing.Expr
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.stronglyMeasurable_countableFiltration_densityProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (n : ℕ) (a : α) {s : Set β},
  MeasurableSet s → MeasureTheory.StronglyMeasurable fun x => κ.densityProcess ν n a x s
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_def : ∀ {R : Type u_3} {A : Type u_4} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  cfc f a =
    if h : p a ∧ ContinuousOn f (spectrum R a) then
      (cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }
    else 0
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.boundedSpace_iff_nndist : ∀ {α : Type u} [inst : PseudoMetricSpace α], BoundedSpace α ↔ ∃ C, ∀ (a b : α), nndist a b ≤ C
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.IsMonoidalDistrib.toIsMonoidalRightDistrib : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C} [self : CategoryTheory.IsMonoidalDistrib C],
  CategoryTheory.IsMonoidalRightDistrib C
-- Init.PropLemmas
dite_else_true : ∀ {p : Prop} [inst : Decidable p] {x : p → Prop}, (if h : p then x h else True) ↔ ∀ (h : p), x h
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_maxKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insert k v).maxKey?.isSome = true
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.HasFiniteLimits.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ (J : Type) [𝒥 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
      CategoryTheory.Limits.HasLimitsOfShape J C) →
    CategoryTheory.Limits.HasFiniteLimits C
-- Mathlib.Topology.Gluing
TopCat.GlueData.eqvGen_of_π_eq : ∀ (D : TopCat.GlueData) {x y : ↑(∐ D.U)},
  (CategoryTheory.ConcreteCategory.hom D.π) x = (CategoryTheory.ConcreteCategory.hom D.π) y →
    Relation.EqvGen
      (Function.Coequalizer.Rel ⇑(CategoryTheory.ConcreteCategory.hom D.diagram.fstSigmaMap)
        ⇑(CategoryTheory.ConcreteCategory.hom D.diagram.sndSigmaMap))
      x y
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the left commutative square of a morphism in `ShortComplex`  -/
CategoryTheory.ShortComplex.Hom.comm₁₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (self : S₁.Hom S₂),
  CategoryTheory.CategoryStruct.comp self.τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f self.τ₂
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.BifibrantObject C} (f : X ⟶ Y),
  HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject.map (HomotopicalAlgebra.BifibrantObject.toHoCat.map f) =
    HomotopicalAlgebra.CofibrantObject.toHoCat.map (HomotopicalAlgebra.CofibrantObject.homMk f.hom)
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
GenContFract.IntFractPair.stream.eq_2 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K) (n : ℕ),
  GenContFract.IntFractPair.stream v n.succ =
    (GenContFract.IntFractPair.stream v n).bind fun ap_n =>
      if ap_n.fr = 0 then none else some (GenContFract.IntFractPair.of ap_n.fr⁻¹)
-- Mathlib.Order.OrderDual
/-- The opposite linear order to a given linear order  -/
LinearOrder.swap : (α : Type u_2) → LinearOrder α → LinearOrder α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- The negation of a projective point representative on a Weierstrass curve.  -/
WeierstrassCurve.Projective.neg : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → Fin 3 → R
-- Mathlib.NumberTheory.LSeries.ZetaZeros
isDiscrete_riemannZetaZeros : IsDiscrete riemannZetaZeros
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Given a finite family of pairwise disjoint finsets, the sum over their union is
the sum of the sums over the sets.
See also `sum_biUnion_of_pairwise_eq_zero` for a version with weaker assumptions.  -/
Finset.sum_biUnion : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι]
  {s : Finset κ} {t : κ → Finset ι}, (↑s).PairwiseDisjoint t → ∑ x ∈ s.biUnion t, f x = ∑ x ∈ s, ∑ i ∈ t x, f i
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.leftUnitor_hom_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.F =
    CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from (((⊤_ C) ⨯ X.src) ⨯ X.tgt))
      CategoryTheory.Limits.prod.snd
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.map_neg : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [inst : Neg α] [inst_1 : Neg β] (f : α → β),
  (∀ (a : α), f (-a) = -f a) → ∀ (M : Matrix m n α), (-M).map f = -M.map f
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpIndSMul.congr_simp : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s s_1 : Set α} (e_s : s = s_1) [inst_1 : NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤)
  (x x_1 : G), x = x_1 → MeasureTheory.condExpIndSMul hm hs hμs x = MeasureTheory.condExpIndSMul hm ⋯ ⋯ x_1
-- Init.Data.BitVec.Lemmas
BitVec.toNat_ushiftRight : ∀ {n : ℕ} (x : BitVec n) (i : ℕ), (x >>> i).toNat = x.toNat >>> i
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
MulAction.isPreprimitive_ofFixingSubgroup_conj_iff : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {s : Set α} {g : G},
  MulAction.IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) ↔
    MulAction.IsPreprimitive ↥(fixingSubgroup G (g • s)) ↥(SubMulAction.ofFixingSubgroup G (g • s))
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₁ i₂ i₃ i₄ i₅ i₆ : ι} (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆)
  (h₅₆ : CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆) (n₁ n₂ n₃ : ℤ)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃._auto_1)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃._auto_3),
  CategoryTheory.CategoryStruct.comp
      (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯)
      (X.map f₃ f₄ f₅ f₃ f₄ f₅₆ (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯) =
    CategoryTheory.CategoryStruct.comp
      (X.map f₂₃ f₄ f₅ f₂₃ f₄ f₅₆ (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₂₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯)
      (X.map f₂₃ f₄ f₅₆ f₃ f₄ f₅₆ (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅₆ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯)
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Scheme.Hom.cover_X : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (hf : P f)
  [inst : AlgebraicGeometry.Surjective f] (x : PUnit.{v + 1}), (AlgebraicGeometry.Scheme.Hom.cover f hf).X x = X
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- A Hecke double coset: an equivalence class of `Δ`-elements under `H₁gH₂ = H₁hH₂`. This is
the basis type for the `HeckeCosetModule`.  -/
HeckeCoset : {G : Type u_1} → [inst : Group G] → Submonoid G → Subgroup G → Subgroup G → Type u_1
-- Lean.Declaration
Lean.ConstantVal.mk : Lean.Name → List Lean.Name → Lean.Expr → Lean.ConstantVal
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equivL_symm_apply : ∀ (R : Type u_1) {A : Type u_3} {E : Type u_4} [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : UniformSpace E]
  [inst_3 : Module R E] (a : E), (WithCStarModule.equivL R).symm a = (WithCStarModule.equiv A E).symm a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropEndWhile_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, (s.copy.dropEndWhile pat).copy = (s.dropEndWhile pat).copy
-- Mathlib.Data.List.Lex
List.Lex.append_right : ∀ {α : Type u} (r : α → α → Prop) {s₁ s₂ : List α} (t : List α), List.Lex r s₁ s₂ → List.Lex r s₁ (s₂ ++ t)
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.algEquivOfAlgEquiv.eq_1 : ∀ {R : Type u_8} {A : Type u_9} {K : Type u_10} {B : Type u_11} {L : Type u_12} [inst : CommSemiring R]
  [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : CommRing K] [inst_4 : CommRing L] [inst_5 : Algebra R A]
  [inst_6 : Algebra R K] [inst_7 : Algebra A K] [inst_8 : IsFractionRing A K] [inst_9 : IsScalarTower R A K]
  [inst_10 : Algebra R B] [inst_11 : Algebra R L] [inst_12 : Algebra B L] [inst_13 : IsFractionRing B L]
  [inst_14 : IsScalarTower R B L] (h : A ≃ₐ[R] B),
  IsFractionRing.algEquivOfAlgEquiv h = IsLocalization.algEquivOfAlgEquiv K L h ⋯
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
Homeomorph.toOpenPartialHomeomorphOfImageEq_toPartialHomeomorph : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X)
  (hs : IsOpen s) (t : Set Y) (h : ⇑e '' s = t),
  (e.toOpenPartialHomeomorphOfImageEq s hs t h).toPartialHomeomorph = e.toPartialHomeomorphOfImageEq s t h
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- When `S₁.f` and `S₂.f` are zero and we have chosen limit kernel forks `c₁` and `c₂`
for `S₁.g` and `S₂.g` respectively, the action on left homology of a morphism `φ : S₁ ⟶ S₂` of
short complexes is given by the unique morphism `f : c₁.pt ⟶ c₂.pt` such that
`c₁.ι ≫ φ.τ₂ = f ≫ c₂.ι`.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (hf₁ : S₁.f = 0) →
            (c₁ : CategoryTheory.Limits.KernelFork S₁.g) →
              (hc₁ : CategoryTheory.Limits.IsLimit c₁) →
                (hf₂ : S₂.f = 0) →
                  (c₂ : CategoryTheory.Limits.KernelFork S₂.g) →
                    (hc₂ : CategoryTheory.Limits.IsLimit c₂) →
                      (f : c₁.pt ⟶ c₂.pt) →
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ =
                            CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂) →
                          CategoryTheory.ShortComplex.LeftHomologyMapData φ
                            (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁)
                            (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S₂ hf₂ c₂ hc₂)