mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.map_fst_pair : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β)
  (g : MeasureTheory.SimpleFunc α γ), MeasureTheory.SimpleFunc.map Prod.fst (f.pair g) = f
-- Init.Data.UInt.Lemmas
USize.add_neg_eq_sub : ∀ {a b : USize}, a + -b = a - b
-- Mathlib.MeasureTheory.Group.Convolution
/-- Convolution of a measure μ with the dirac measure at 1 returns μ.  -/
MeasureTheory.Measure.mconv_dirac_one : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] (μ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ], μ.mconv (MeasureTheory.Measure.dirac 1) = μ
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- See `exists_floor'` for a more general version which only assumes the element is bounded by
two integers.  -/
exists_floor : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R),
  ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- Wrap an element of the underlying completion `(v.valuation K).Completion` into
`adicCompletion`.  -/
IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      {K : Type u_2} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              {v : IsDedekindDomain.HeightOneSpectrum R} →
                (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion →
                  IsDedekindDomain.HeightOneSpectrum.adicCompletion K v
-- Mathlib.CategoryTheory.Functor.FunctorHom
/-- The contravariant functor taking `A : C ⥤ Type w` to `HomObj F G A`, i.e. Hom(F ⊗ -, G).  -/
CategoryTheory.Functor.homObjFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.Functor C D → CategoryTheory.Functor (CategoryTheory.Functor C (Type w))ᵒᵖ (Type (max w v' u))
-- Lean.Expr
/-- Returns `instOfNatNat n : OfNat Nat n`
 -/
Lean.mkInstOfNatNat : Lean.Expr → Lean.Expr
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- The pointwise intersection of an upper hemicontinuous function with a fixed closed set is
upper hemicontinuous.  -/
UpperHemicontinuousWithinAt.inter : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α}
  {x : α},
  UpperHemicontinuousWithinAt f s x → ∀ {u : Set β}, IsClosed u → UpperHemicontinuousWithinAt (fun x => f x ∩ u) s x
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of a multiplication with unit is commutative and associative.

This is not an instance as it forms a non-defeq diamond with `Submonoid.toMonoid` in the `npow`
field.  -/
Submonoid.center.commMonoid' : {M : Type u_1} → [inst : MulOneClass M] → CommMonoid ↥(Submonoid.center M)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.lcomp_apply : ∀ {R : Type u_1} {U : Type u_2} {V : Type u_3} (W : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid U]
  [inst_2 : Module R U] [inst_3 : TopologicalSpace U] [inst_4 : AddCommMonoid V] [inst_5 : Module R V]
  [inst_6 : TopologicalSpace V] [inst_7 : AddCommMonoid W] [inst_8 : Module R W] [inst_9 : TopologicalSpace W]
  [inst_10 : ContinuousAdd W] [inst_11 : ContinuousConstSMul R W] (f : U →L[R] V) (l : V →L[R] W),
  (ContinuousLinearMap.lcomp W f) l = l ∘SL f
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_eq_pow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] {a : A} {y : ℝ}, CFC.rpow a y = a ^ y
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `a ^ (b : ℕ)`,
such that `positivity` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.Positivity.evalPow : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The circumcenter of a 0-simplex equals its unique point.  -/
Affine.Simplex.circumcenter_eq_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : Affine.Simplex ℝ P 0) (i : Fin 1), s.circumcenter = s.points i
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.toRingHom_algebraMap : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] (self : P.Hom P') (x : R),
  self.toRingHom ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstr.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof → Sort u} (t : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof) → t.below → motive_2 t),
  t.brecOn F_1 F_2 = F_1 t (Lean.Meta.Grind.Arith.Linear.RingIneqCnstr.brecOn.go t F_1 F_2).2
-- Lean.Elab.DeclNameGen
/-- Strips out universes and arguments we decide are unnecessary for naming.
The resulting expression can have loose fvars and be mangled in other ways.
Expressions can also be replaced by `.bvar 0` if they shouldn't be mentioned.
 -/
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.winnowExpr : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Module.ZLattice.Covolume
ZLattice.covolume_comap : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [inst_5 : DiscreteTopology ↥L] [IsZLattice ℝ L]
  (μ : autoParam (MeasureTheory.Measure E) _auto_28✝) [μ.IsAddHaarMeasure] {F : Type u_2}
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace ℝ F] [FiniteDimensional ℝ F] [inst_11 : MeasurableSpace F]
  [BorelSpace F] (ν : autoParam (MeasureTheory.Measure F) ZLattice.covolume_comap._auto_1) [ν.IsAddHaarMeasure]
  {e : F ≃L[ℝ] E},
  MeasureTheory.MeasurePreserving (⇑e) ν μ → ZLattice.covolume (ZLattice.comap ℝ L ↑↑e) ν = ZLattice.covolume L μ
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.mkReal_coe : ∀ {K : Type u_1} [inst : Field K] (φ : { φ // NumberField.ComplexEmbedding.IsReal φ }),
  ↑(NumberField.InfinitePlace.mkReal φ) = NumberField.InfinitePlace.mk ↑φ
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.orthRadius_le_orthRadius_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P},
  s.orthRadius p ≤ s.orthRadius q ↔ p = q ∨ q = s.center
-- Mathlib.Data.Nat.Choose.Sum
/-- **Zhu Shijie's identity** aka hockey-stick identity, version with `range`.
Summing `(i + k).choose k` for `i ∈ [0, n]` gives `(n + k + 1).choose (k + 1)`.

Combinatorial interpretation: `(i + k).choose k` is the number of decompositions of `[0, i)` in
`k + 1` (possibly empty) intervals (this follows from a stars and bars description). In particular,
`(n + k + 1).choose (k + 1)` corresponds to decomposing `[0, n)` into `k + 2` intervals.
By putting away the last interval (of some length `n - i`),
we have to decompose the remaining interval `[0, i)` into `k + 1` intervals, hence the sum.  -/
Nat.sum_range_add_choose : ∀ (n k : ℕ), ∑ i ∈ Finset.range (n + 1), (i + k).choose k = (n + k + 1).choose (k + 1)
-- Mathlib.Data.NNReal.Basic
NNReal.image_coe_Ioi : ∀ (x : NNReal), NNReal.toReal '' Set.Ioi x = Set.Ioi ↑x
-- Mathlib.Order.Category.LinOrd
LinOrd.comp_apply : ∀ {X Y Z : LinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.ModelTheory.Substructures
/-- If `s` is a dense set in a structure `M`, `Substructure.closure L s = ⊤`, then in order to prove
that some predicate `p` holds for all `x : M` it suffices to verify `p x` for `x ∈ s`, and verify
that `p` is preserved under function symbols.  -/
FirstOrder.Language.Substructure.dense_induction : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {p : M → Prop} (x : M) {s : Set M},
  (FirstOrder.Language.Substructure.closure L).toFun s = ⊤ →
    (∀ x ∈ s, p x) → (∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f (Set.ofPred p)) → p x
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousOn_iSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {ι : Sort u_4} {δ : Type u_5} [inst_1 : CompleteLinearOrder δ]
  {f : ι → α → δ}, (∀ (i : ι), LowerSemicontinuousOn (f i) s) → LowerSemicontinuousOn (fun x' => ⨆ i, f i x') s
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
/-- The infimum of the Rayleigh quotient of a symmetric operator `T` on a nontrivial
finite-dimensional vector space is an eigenvalue for that operator.  -/
LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} [Nontrivial E],
  T.IsSymmetric → Module.End.HasEigenvalue T ↑(⨅ x, RCLike.re (inner 𝕜 (T ↑x) ↑x) / ‖↑x‖ ^ 2)
-- Batteries.Data.Char.Basic
Char.toNat_ofNat : ∀ (n : ℕ), (Char.ofNat n).toNat = if n.isValidChar then n else 0
-- Mathlib.Analysis.Complex.Basic
Complex.conjCLE_coe_toLinearMap : ↑↑Complex.conjCLE = Complex.conjAe.toLinearMap
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousComp'_inv_app_hom_app : ∀ {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] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D E} {FG : CategoryTheory.Functor C E} (eFG : F.comp G ≅ FG) (A : Type u)
  [inst_3 : CategoryTheory.Category.{t, u} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (L : CategoryTheory.GrothendieckTopology E) [inst_4 : F.IsContinuous J K]
  [inst_5 : G.IsContinuous K L] [inst_6 : FG.IsContinuous J L] (X : CategoryTheory.Sheaf L A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Functor.sheafPushforwardContinuousComp' eFG A J K L).inv.app X).hom.app X_1 =
    X.obj.map (eFG.hom.app (Opposite.unop X_1)).op
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_le_size_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, t.size - 1 ≤ (t.alter k f).size
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_X : ∀ {R : Type u} {σ : Type u_1} {n : σ} [inst : CommSemiring R] [Nontrivial R], (MvPolynomial.X n).vars = {n}
-- Mathlib.GroupTheory.Goursat
Subgroup.mk_goursatFst_eq_iff_mk_goursatSnd_eq : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {I : Subgroup (G × H)},
  Function.Surjective (Prod.fst ∘ ⇑I.subtype) →
    Function.Surjective (Prod.snd ∘ ⇑I.subtype) → ∀ {x y : G × H}, x ∈ I → y ∈ I → (↑x.1 = ↑y.1 ↔ ↑x.2 = ↑y.2)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_mul_right : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Mul β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.IndepFun (f i) (f j * f k) μ
-- Mathlib.Topology.Algebra.UniformConvergence
instCommMonoidUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [CommMonoid β] → CommMonoid (UniformOnFun α β 𝔖)
-- Mathlib.Order.Filter.Extr
isMaxFilter_const : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsMaxFilter (fun x => b) l a
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.id_homₚ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (x : TopPair.HomologyPretheory C c) (x_1 : ι),
  (CategoryTheory.CategoryStruct.id x).homₚ x_1 = CategoryTheory.CategoryStruct.id (x.Hₚ x_1)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.map_hom_inv'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ≅ Y) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map f.hom) (CategoryTheory.CategoryStruct.comp (F.map f.inv) h) = h
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.skipPrefix?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, s.skipPrefix? pat = none ↔ ¬String.Slice.Pattern.Model.MatchesAt pat s.startPos
-- Init.Data.Vector.MapIdx
Vector.getElem_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : ℕ → α → β} {xs : Vector α n} {i : ℕ} (h : i < n),
  (Vector.mapIdx f xs)[i] = f i xs[i]
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- **Alias** of `MonoidAlgebra.mapRingHom_comp_algebraMap`. -/
MonoidAlgebra.mapRangeRingHom_comp_algebraMap : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Monoid M]
  (f : R →+* S),
  (MonoidAlgebra.mapRingHom M f).comp (algebraMap R (MonoidAlgebra R M)) = (algebraMap S (MonoidAlgebra S M)).comp f
-- Init.Data.UInt.Lemmas
UInt32.neg_add : ∀ {a b : UInt32}, -(a + b) = -a - b
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Icc_union_Ioc_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ≤ b → b ≤ c → Set.Icc a b ∪ Set.Ioc b c = Set.Icc a c
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.eraseManyEntries.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ ((a : α) × β a)]
  (m : Std.DHashMap.Raw α β) (l : ρ),
  m.eraseManyEntries l = if h : 0 < m.buckets.size then ↑↑(Std.DHashMap.Internal.Raw₀.eraseManyEntries ⟨m, h⟩ l) else m
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpace_chainTopCoeff_add_one_zsmul_add : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  α ≠ 0 → LieModule.genWeightSpace M ((↑(LieModule.chainTopCoeff α β) + 1) • α + ⇑β) = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right] {X Y : CategoryTheory.Limits.WalkingParallelPair} (h : X ⟶ Y),
  I.parallelPairDiagram.map h = CategoryTheory.Limits.parallelPair.parallelPairHom I.fstPiMap I.sndPiMap h
-- Mathlib.Topology.Semicontinuity.Defs
lowerHemicontinuous_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  LowerHemicontinuous f ↔ ∀ (x : α) (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, f x' ⊆ t) → f x ⊆ t
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [OpensMeasurableSpace E] {R : NNReal} {p : ENNReal} {f : ℕ → α → E},
  (∀ (n : ℕ), Measurable (f n)) →
    (∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R) →
      ∀ᵐ (x : α) ∂μ, Filter.liminf (fun n => ‖f n x‖ₑ ^ p.toReal) Filter.atTop < ⊤
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.map_inl : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (equiv : S.Equiv S')
  (n : N), equiv (S.inl n) = S'.inl n
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- If `f` and `g` are homotopic relative to a cylinder `P`, then `g` and `f`
are homotopic relative to `P.symm`.  -/
HomotopicalAlgebra.Cylinder.LeftHomotopy.symm : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        {P : HomotopicalAlgebra.Cylinder X} → {f g : X ⟶ Y} → P.LeftHomotopy f g → P.symm.LeftHomotopy g f
-- Mathlib.Data.Vector.Snoc
List.Vector.mapAccumr₂_snoc : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} {φ : Type u_4} {n : ℕ} {s : σ} (xs : List.Vector α n)
  (ys : List.Vector β n) (f : α → β → σ → σ × φ) (x : α) (y : β),
  List.Vector.mapAccumr₂ f (xs.snoc x) (ys.snoc y) s =
    have q := f x y s;
    have r := List.Vector.mapAccumr₂ f xs ys q.1;
    (r.1, r.2.snoc q.2)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.reduceBoolPred : Lean.Name → ℕ → (ℕ → ℕ → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_whisker_right_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.Pseudofunctor B C) {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c)
  {Z : self.obj a ⟶ self.obj c} (h_1 : self.map (CategoryTheory.CategoryStruct.comp g h) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η h)) h_1 =
    CategoryTheory.CategoryStruct.comp (self.mapComp f h).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map h))
        (CategoryTheory.CategoryStruct.comp (self.mapComp g h).inv h_1))
-- Mathlib.Topology.Order.LeftRightNhds
/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)`
with `a < u < u'`, provided `a` is not a top element.  -/
mem_nhdsGE_iff_exists_Ico_subset' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a u' : α} {s : Set α},
  a < u' → (s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_eq_of_eq' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {a₁ b₁ : R} {a₂ b₂ : ↥M},
  b₁ * ↑a₂ = a₁ * ↑b₂ → IsLocalization.mk' S a₁ a₂ = IsLocalization.mk' S b₁ b₂
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_two_eq : ∀ (x : ℤ), x.tmod 2 = -1 ∨ x.tmod 2 = 0 ∨ x.tmod 2 = 1
-- Init.Data.SInt.Lemmas
ISize.toInt_mod : ∀ (a b : ISize), (a % b).toInt = a.toInt.tmod b.toInt
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_swap : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x y : K),
  Height.mulHeight ![x, y] = Height.mulHeight ![y, x]
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k fallback : α}, (t.erase k).getD k fallback = fallback
-- Mathlib.RepresentationTheory.Induced
Rep.indFunctor_obj : ∀ (k : Type u) {G : Type v} {H : Type v'} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  (A : Rep.{w, u, v} k G), (Rep.indFunctor k φ).obj A = Rep.ind φ A
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction.eq_1 : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a : α),
  hf.stieltjesFunction a =
    { toFun := ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a, mono' := ⋯, right_continuous' := ⋯ }
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
ProbabilityTheory.iIndepFun.hasGaussianLaw_add : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E]
  {X Y : Ω → E},
  ProbabilityTheory.HasGaussianLaw X P →
    ProbabilityTheory.HasGaussianLaw Y P → ProbabilityTheory.IndepFun X Y P → ProbabilityTheory.HasGaussianLaw (X + Y) P
-- Mathlib.RingTheory.Support
Module.mem_support_iff_of_finite : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p : PrimeSpectrum R} [Module.Finite R M], p ∈ Module.support R M ↔ Module.annihilator R M ≤ p.asIdeal
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (L₀ L₁ L₂ L₃ : CategoryTheory.ShortComplex C) →
        (v₀₁ : L₀ ⟶ L₁) →
          (v₁₂ : L₁ ⟶ L₂) →
            (v₂₃ : L₂ ⟶ L₃) →
              (w₀₂ :
                  autoParam (CategoryTheory.CategoryStruct.comp v₀₁ v₁₂ = 0)
                    CategoryTheory.ShortComplex.SnakeInput.w₀₂._autoParam) →
                (w₁₃ :
                    autoParam (CategoryTheory.CategoryStruct.comp v₁₂ v₂₃ = 0)
                      CategoryTheory.ShortComplex.SnakeInput.w₁₃._autoParam) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι v₀₁ w₀₂) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ v₂₃ w₁₃) →
                      L₁.Exact →
                        CategoryTheory.Epi L₁.g →
                          L₂.Exact → CategoryTheory.Mono L₂.f → CategoryTheory.ShortComplex.SnakeInput C
-- Mathlib.Logic.Relation
Relation.ReflTransGen.below : {α : Type u_1} →
  {r : α → α → Prop} →
    {a : α} →
      {motive : (a_1 : α) → Relation.ReflTransGen r a a_1 → Prop} → {a_1 : α} → Relation.ReflTransGen r a a_1 → Prop
-- Mathlib.MeasureTheory.Function.FactorsThrough
/-- If a function is measurable with respect to the σ-algebra generated by the
first coordinates, then it only depends on those first coordinates.  -/
Measurable.dependsOn_of_piFinset : ∀ {Z : Type u_3} {ι : Type u_4} {X : ι → Type u_5} [inst : (i : ι) → MeasurableSpace (X i)] {f : ((i : ι) → X i) → Z}
  {s : Finset ι} [inst_1 : MeasurableSpace Z] [MeasurableSingletonClass Z], Measurable f → DependsOn f ↑s
-- Init.Grind.Config
/-- Maximum number of theorem instances generated using E-matching in a proof search tree branch.  -/
Lean.Grind.Config.instances : Lean.Grind.Config → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.count_support_eq_one : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} {p : G.Path u v},
  w ∈ (↑p).support → List.count w (↑p).support = 1