mathlib-initiative/mathlib-types huggingface dataset:
-- Init.System.FilePath
/-- Replaces the file name at the end of the path `p` with `fname`, placing `fname` in the parent
directory of `p`.

If `p` has no parent directory, then `fname` is returned unmodified.
 -/
System.FilePath.withFileName : System.FilePath → String → System.FilePath
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Descr.name : {α β σ : Type} → Lean.ScopedEnvExtension.Descr α β σ → Lean.Name
-- Mathlib.Topology.Gluing
/-- A family of gluing data consists of
1. An index type `J`
2. A bundled topological space `U i` for each `i : J`.
3. An open set `V i j ⊆ U i` for each `i j : J`.
4. A transition map `t i j : V i j ⟶ V j i` for each `i j : ι`.

such that
6. `V i i = U i`.
7. `t i i` is the identity.
8. For each `x ∈ V i j ∩ V i k`, `t i j x ∈ V j k`.
9. `t j k (t i j x) = t i k x`.

We can then glue the topological spaces `U i` together by identifying `V i j` with `V j i`.
 -/
TopCat.GlueData.MkCore : Type (u + 1)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C)
  [P.IsStableUnderBaseChange] {X Y : C} (f : X ⟶ Y), P.IsStableUnderBaseChangeAlong f
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_self : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x : P), midpoint R x x = x
-- Batteries.Data.String.Lemmas
String.Pos.Raw.lt_addChar : ∀ (p : String.Pos.Raw) (c : Char), p < p + c
-- Init.Data.Array.Lemmas
/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`.  -/
Array.map_id_fun' : ∀ {α : Type u_1}, (Array.map fun a => a) = id
-- Mathlib.Order.CompleteLattice.Finset
Finset.iInf_insert_update : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] [inst_1 : DecidableEq α] {x : α} {t : Finset α} (f : α → β)
  {s : β}, x ∉ t → ⨅ i ∈ insert x t, Function.update f x s i = s ⊓ ⨅ i ∈ t, f i
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.aeconst_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb →
    ∀ {s : Set β},
      MeasureTheory.NullMeasurableSet s μb →
        (Filter.EventuallyConst (f ⁻¹' s) (MeasureTheory.ae μa) ↔ Filter.EventuallyConst s (MeasureTheory.ae μb))
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.instHasBesicovitchCovering : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E],
  HasBesicovitchCovering E
-- Batteries.Data.Nat.Bisect
Nat.avg.eq_1 : ∀ (a b : ℕ), a.avg b = (a + b) / 2
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.coe_sum : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R] [inst_4 : IsTopologicalSemiring R] {ι : Type u_3} (s : Finset ι)
  (f : ι → ContinuousMapZero X R), ⇑(s.sum f) = ∑ i ∈ s, ⇑(f i)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.Normal.map_conj_eq : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [H.Normal] (g : G), Subgroup.map (↑(MulAut.conj g)) H = H
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerived_fac_app : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : LF.IsLeftDerivedFunctor α W] (G : CategoryTheory.Functor D H) (β : L.comp G ⟶ F) (X : C),
  CategoryTheory.CategoryStruct.comp ((LF.leftDerivedLift α W G β).app (L.obj X)) (α.app X) = β.app X
-- Init.Data.Nat.Order
Nat.instLawfulOrderMin : Std.LawfulOrderMin ℕ
-- Init.Data.Order.Lemmas
Std.Trichotomous.rel_or_eq_or_rel_swap : ∀ {α : Sort u_1} {r : α → α → Prop} [i : Std.Trichotomous r] {a b : α}, r a b ∨ a = b ∨ r b a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_mul_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α] [MulLeftMono α] {b c : α}, b ≤ c → ∀ (a : α), a * b ≤ a * c
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.measurable_geometricPMFReal : ∀ {p : ℝ}, Measurable (ProbabilityTheory.geometricPMFReal p)
-- Mathlib.GroupTheory.GroupAction.ConjAct
/-- Group conjugation on a normal subgroup. Analogous to `MulAut.conj`.  -/
MulAut.conjNormal : {G : Type u_3} → [inst : Group G] → {H : Subgroup G} → [H.Normal] → G →* MulAut ↥H
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.BinaryRefVec.cast.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig1 aig2 : Std.Sat.AIG α}
  (h : aig1.decls.size ≤ aig2.decls.size) (lhs rhs : aig1.RefVec len),
  { lhs := lhs, rhs := rhs }.cast h = { lhs := lhs.cast h, rhs := rhs.cast h }
-- Lean.Data.Options
Lean.instInhabitedOptionDeprecation.default : Lean.OptionDeprecation
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α} {v : β k}, (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G → ↑B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((groupCohomology.cochainsMap f φ).f 1)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₁ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₁ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap₁ f φ) h)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- If `fn` is `UnifIntegrable`, then the family of limits in probability of sequences of `fn` is
`UnifIntegrable`.  -/
MeasureTheory.UnifIntegrable.unifIntegrable_of_tendstoInMeasure : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {κ : Type u_4} (u : Filter κ) [u.NeBot] [u.IsCountablyGenerated]
  {fn : ι → α → β},
  MeasureTheory.UnifIntegrable fn p μ →
    (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (fn i) μ) → MeasureTheory.UnifIntegrable (fun f => ↑f) p μ
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- `ContinuousMultilinearMap.compContinuousLinearMap` as a bundled continuous linear map.
This implementation fixes `g : ContinuousMultilinearMap 𝕜 E₁ G`.

Actually, the map is linear in `g`,
see `ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear`.

For a version fixing `f` and varying `g`, see `compContinuousLinearMapL`.  -/
ContinuousMultilinearMap.compContinuousLinearMapLRight : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      {E₁ : ι → Type wE₁} →
        {G : Type wG} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
                [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] →
                  [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)] →
                    [inst_5 : SeminormedAddCommGroup G] →
                      [inst_6 : NormedSpace 𝕜 G] →
                        [Fintype ι] →
                          ContinuousMultilinearMap 𝕜 E₁ G →
                            ContinuousMultilinearMap 𝕜 (fun i => E i →L[𝕜] E₁ i) (ContinuousMultilinearMap 𝕜 E G)
-- Mathlib.Order.Monotone.Defs
monotone_app : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder γ] (f : β → α → γ) (b : β),
  (Monotone fun a b => f b a) → Monotone (f b)
-- Mathlib.Data.Set.Basic
Set.union_eq_union_iff_left : ∀ {α : Type u} {s t u : Set α}, s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Elab.Tactic.processTermParam : Lean.Meta.Grind.Params →
  Lean.TSyntax `Lean.Parser.Tactic.grindParam →
    Option (Lean.TSyntax `Lean.Parser.Attr.grindMod) → Lean.Term → Bool → Lean.Elab.TermElabM Lean.Meta.Grind.Params
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Context.mk : List Lean.FVarId → Lean.Meta.LetToHave.Context✝
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_sup : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S T : AddSubsemigroup M) (f : M →ₙ+ N),
  AddSubsemigroup.map f (S ⊔ T) = AddSubsemigroup.map f S ⊔ AddSubsemigroup.map f T
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.mono : ∀ (f : CircleDeg1Lift) {x y : ℝ}, x ≤ y → f x ≤ f y
-- Mathlib.Topology.Category.Stonean.Basic
CompHaus.toStonean_toTop : ∀ (X : CompHaus) [inst : CategoryTheory.Projective X], X.toStonean.toTop = X.toTop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSignatureInformation : Lean.FromJson Lean.Lsp.SignatureInformation
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.map_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type w'} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → γ} {g : α → γ → δ},
  Std.ExtHashMap.map g (Std.ExtHashMap.map f m) = Std.ExtHashMap.map (fun k v => g k (f k v)) m
-- Lean.Expr
Lean.MVarIdSet.ofArray : Array Lean.MVarId → Lean.MVarIdSet
-- Mathlib.Analysis.Convex.Strict
strictConvex_iff_openSegment_subset : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : SMul 𝕜 E] {s : Set E},
  StrictConvex 𝕜 s ↔ s.Pairwise fun x y => openSegment 𝕜 x y ⊆ interior s
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.awayToSection_comp_appLE_assoc : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) {i : ℕ} {s : A},
  s ∈ 𝒜 i →
    ∀ {Z : CommRingCat}
      (h : (AlgebraicGeometry.Proj ℬ).presheaf.obj (Opposite.op (AlgebraicGeometry.Proj.basicOpen ℬ (f s))) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayToSection 𝒜 s)
          (CategoryTheory.CategoryStruct.comp
            (AlgebraicGeometry.Scheme.Hom.appLE (AlgebraicGeometry.Proj.map f hf) (AlgebraicGeometry.Proj.basicOpen 𝒜 s)
              (AlgebraicGeometry.Proj.basicOpen ℬ (f s)) ⋯)
            h) =
        CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (HomogeneousLocalization.Away.map f s))
          (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayToSection ℬ (f s)) h)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.maxEntry? : {α : Type u} → {β : Type v} → (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isAcyclic_iff_forall_adj_isBridge : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.descHomology.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} [inst_2 : S.HasHomology] (k k_1 : S.cycles ⟶ A) (e_k : k = k_1)
  (hk : CategoryTheory.CategoryStruct.comp S.toCycles k = 0), S.descHomology k hk = S.descHomology k_1 ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {len w : ℕ} {vec : aig.RefVec w}
  {start w_1 : ℕ} {vec_1 : aig.RefVec w_1} {start_1 : ℕ},
  { w := w, vec := vec, start := start } = { w := w_1, vec := vec_1, start := start_1 } →
    w = w_1 ∧ vec ≍ vec_1 ∧ start = start_1
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.absolutelyContinuous_map_add_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] (g : G),
  μ.AbsolutelyContinuous (MeasureTheory.Measure.map (fun x => x + g) μ)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.continuous : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] (F : α →𝒄 β)
  (C : OmegaCompletePartialOrder.Chain α),
  F (OmegaCompletePartialOrder.ωSup C) = OmegaCompletePartialOrder.ωSup (C.map ↑F)
-- Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
CategoryTheory.coherentCoverage.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Precoherent C],
  CategoryTheory.coherentCoverage C = CategoryTheory.coherentCoverage C
-- Mathlib.Data.PNat.Defs
PNat.mk_lt_mk : ∀ (n k : ℕ) (hn : 0 < n) (hk : 0 < k), ⟨n, hn⟩ < ⟨k, hk⟩ ↔ n < k
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.instFullIncl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.Limits.FormalCoproduct.incl C).Full
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.associator_inv_right_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'')
  (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') (x : C),
  (φ.associator φ' φ'').inv.right.app x =
    CategoryTheory.CategoryStruct.id (φ''.right.obj (φ'.right.obj (φ.right.obj x)))
-- Mathlib.Topology.Order.OrderClosed
Ioc_mem_nhdsGT_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b c : α},
  b ∈ Set.Ico c a → Set.Ioc c a ∈ nhdsWithin b (Set.Ioi b)
-- Mathlib.RingTheory.Ideal.Basic
Ideal.pi_le_pi_iff : ∀ {ι : Type u_1} {R : ι → Type u_5} [inst : (i : ι) → Semiring (R i)] {I J : (i : ι) → Ideal (R i)},
  Ideal.pi I ≤ Ideal.pi J ↔ I ≤ J
-- Mathlib.Topology.MetricSpace.Isometry
/-- **Alias** of `Isometry.preimage_eball`. -/
Isometry.preimage_emetric_ball : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ENNReal), f ⁻¹' Metric.eball (f x) r = Metric.eball x r
-- Mathlib.Data.List.Sigma
List.kunion_cons : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s : Sigma β} {l₁ l₂ : List (Sigma β)},
  (s :: l₁).kunion l₂ = s :: l₁.kunion (List.kerase s.fst l₂)
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.degBound.eq_1 : ∀ (k : ℕ) (D : ℕ → ℕ), ChevalleyThm.MvPolynomialC.degBound k D 0 = 1
-- Mathlib.Combinatorics.Quiver.Symmetric
_private.Mathlib.Combinatorics.Quiver.Symmetric.0.Quiver.Symmetrify.lift.match_1.eq_2 : ∀ {V : Type u_2} [inst : Quiver V] {X Y : Quiver.Symmetrify V} (motive : (X ⟶ Y) → Sort u_3) (g : Y ⟶ X)
  (h_1 : (g : X ⟶ Y) → motive (Sum.inl g)) (h_2 : (g : Y ⟶ X) → motive (Sum.inr g)),
  (match Sum.inr g with
    | Sum.inl g => h_1 g
    | Sum.inr g => h_2 g) =
    h_2 g
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.comp_zero : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃), g ∘SL 0 = 0
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Congr!.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Congr!.Config
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullback₁_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)],
  (CategoryTheory.PreZeroHypercover.pullback₁ f E).I₀ = E.I₀
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- the compatibility condition on `fst` and `snd` with respect to the structure
isomorphisms  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (self : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y) {Z : CategoryTheory.Functor X B}
  (h : y.snd.comp G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight self.fst F)
      (CategoryTheory.CategoryStruct.comp y.iso.hom h) =
    CategoryTheory.CategoryStruct.comp x.iso.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight self.snd G) h)
-- Mathlib.Topology.Irreducible
isPreirreducible_empty : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsPreirreducible ∅
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mulLECancellable_one : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α], MulLECancellable 1
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.mem_memberSubfamily : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
  s ∈ Finset.memberSubfamily a 𝒜 ↔ insert a s ∈ 𝒜 ∧ a ∉ s
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∉ s → s.erase a = s
-- Mathlib.Data.List.Chain
List.IsChain.sublist : ∀ {α : Type u_1} {R : α → α → Prop} {l₁ l₂ : List α} [Trans R R R],
  List.IsChain R l₂ → l₁.Sublist l₂ → List.IsChain R l₁
-- Mathlib.Topology.Connected.TotallyDisconnected
TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace_symm_apply_apply : ∀ (X : Type u_3) (Y : Type u_4) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TotallyDisconnectedSpace Y] [inst_3 : ConnectedSpace X] (y : Y) (x : X),
  ((TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace X Y).symm y) x = y
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
_private.Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms.0.SimplexCategoryGenRel.standardσ.match_1.eq_2 : ∀ {m₁ m₂ : ℕ} (motive : (L : List ℕ) → m₂ + L.length = m₁ → Sort u_1) (a : ℕ) (t : List ℕ)
  (h : m₂ + (a :: t).length = m₁) (h_1 : (h : m₂ + [].length = m₁) → motive [] h)
  (h_2 : (a : ℕ) → (t : List ℕ) → (h : m₂ + (a :: t).length = m₁) → motive (a :: t) h),
  (match a :: t, h with
    | [], h => h_1 h
    | a :: t, h => h_2 a t h) =
    h_2 a t h
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_sdiff_right : ∀ {α : Type u_2} {ι : Type u_5} [inst : BooleanAlgebra α] {s : Finset ι},
  s.Nonempty → ∀ (f : ι → α) (a : α), (s.inf fun b => f b \ a) = s.inf f \ a
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.power_zero : ∀ (a : Cardinal.{u_1}), a ^ 0 = 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyLED_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.Equiv t₂ → t₁.getKeyLED k fallback = t₂.getKeyLED k fallback
-- Init.Data.Nat.Dvd
Nat.dvd_sub_iff_right : ∀ {m n k : ℕ}, k ≤ n → m ∣ n → (m ∣ n - k ↔ m ∣ k)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_arrow_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImageSubobject f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h) =
    CategoryTheory.CategoryStruct.comp f h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_union! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, (m₁.union! m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback)
-- Mathlib.Analysis.PSeries
Real.summable_abs_int_rpow : ∀ {b : ℝ}, 1 < b → Summable fun n => |↑n| ^ (-b)
-- Lean.Elab.Tactic.Induction
/-- Return the next argument expected type. This method assumes `fType` is a function type.  -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.getArgExpectedType : Lean.Elab.Tactic.ElimApp.M✝ Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Lax unity.  -/
CategoryTheory.Lax.StrongTrans.naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.StrongTrans F G) (a : B),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a))
      (self.naturality (CategoryTheory.CategoryStruct.id a)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.app a)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).inv
        (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a)))
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_congr_set_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) {s t : Set β},
  s = t → ∑' (x : ↑s), f ↑x = ∑' (x : ↑t), f ↑x