mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Defs
/-- The fundamental scalar multiplication in an additive group. `zpowRec n a = a+a+...+a` n
times, for integer `n`. Use instead `n • a`, which has better definitional behavior.  -/
zsmulRec : {G : Type u_1} → [inst : Zero G] → [inst_1 : Add G] → [Neg G] → optParam (ℕ → G → G) nsmulRec → ℤ → G → G
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- If we want to construct a relative CW complex of finite type, we can add the condition
`finite_cell` and relax the condition `mapsTo`.  -/
Topology.RelCWComplex.mkFiniteType : {X : Type u} →
  [inst : TopologicalSpace X] →
    (C : Set X) →
      (D : outParam (Set X)) →
        (cell : ℕ → Type u) →
          (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) →
            (∀ (n : ℕ), Finite (cell n)) →
              (∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) →
                (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) →
                  (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) →
                    (Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) →
                      (∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' Metric.ball 0 1) D) →
                        (∀ (n : ℕ) (i : cell n),
                            Set.MapsTo (↑(map n i)) (Metric.sphere 0 1)
                              (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1)) →
                          (∀ A ⊆ C,
                              (∀ (n : ℕ) (j : cell n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) ∧
                                  IsClosed (A ∩ D) →
                                IsClosed A) →
                            IsClosed D →
                              D ∪ ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C → Topology.RelCWComplex C D
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_map : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f : R →+* S} {s : Subsemiring R}
  {y : S}, y ∈ Subsemiring.map f s ↔ ∃ x ∈ s, f x = y
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.ψ₂.congr_simp : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) {X Y : C}
  (w w_1 : X ⟶ Y) (e_w : w = w_1) (hw : W w),
  CategoryTheory.Localization.Construction.ψ₂ W w hw = CategoryTheory.Localization.Construction.ψ₂ W w_1 ⋯
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- Polynomial evaluation commutes with `Multiset.sum`.  -/
Polynomial.eval_multisetSum : ∀ {R : Type u} [inst : Semiring R] (s : Multiset (Polynomial R)) (x : R),
  Polynomial.eval x s.sum = (Multiset.map (Polynomial.eval x) s).sum
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F),
  (Lagrange.interpolate s v) r =
    ∑ i ∈ s,
      Polynomial.C (Lagrange.nodalWeight s v i) * (Lagrange.nodal s v / (Polynomial.X - Polynomial.C (v i))) *
        Polynomial.C (r i)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.ext : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f],
  (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) → ∀ ⦃j k : M' →ₗ[R] M''⦄, j ∘ₗ f = k ∘ₗ f → j = k
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k k' fallback : α},
  (k == k') = true →
    k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertMany l).getD k' fallback = k
-- Mathlib.Algebra.Group.Defs
/-- One is a left neutral element for multiplication  -/
MulOneClass.one_mul : ∀ {M : Type u} [self : MulOneClass M] (a : M), 1 * a = a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_erase!_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, (Std.DTreeMap.Internal.Impl.erase! k t).size ≤ t.size
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : P.IsStableUnderBaseChangeAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong g] [inst_4 : P.HasPullbacksAlong f] [inst_5 : P.HasPullbacksAlong g]
  [inst_6 : Q.RespectsIso] [inst_7 : Q.IsStableUnderBaseChange] (A : P.Over Q Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.MorphismProperty.Over.pullbackComp f g (CategoryTheory.CategoryStruct.comp f g) ⋯).hom.app
          A).left
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd A.hom g) f)
        (CategoryTheory.Limits.pullback.fst A.hom g)) =
    CategoryTheory.Limits.pullback.fst A.hom (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The inner product between a multiple of a `π / 2` rotation of a vector and that vector is
zero.  -/
Orientation.inner_smul_rotation_pi_div_two_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) (r : ℝ), inner ℝ (r • (o.rotation ↑(Real.pi / 2)) x) x = 0
-- Mathlib.Data.Finset.Card
Finset.card_union_eq_card_add_card : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], (s ∪ t).card = s.card + t.card ↔ Disjoint s t
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.naturality' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C n}
  (φ : F ⟶ G) (i j : ℕ) (hij : autoParam (i ≤ j) CategoryTheory.ComposableArrows.naturality'._auto_1)
  (hj : autoParam (j ≤ n) CategoryTheory.ComposableArrows.naturality'._auto_3),
  CategoryTheory.CategoryStruct.comp (F.map' i j hij hj) (CategoryTheory.ComposableArrows.app' φ j hj) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ i ⋯) (G.map' i j hij hj)
-- Mathlib.Algebra.Algebra.Operations
Submodule.map_pow : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A)
  {A' : Type u_1} [inst_3 : Semiring A'] [inst_4 : Algebra R A'] (f : A →ₐ[R] A') (n : ℕ),
  Submodule.map f.toLinearMap (M ^ n) = Submodule.map f.toLinearMap M ^ n
-- Init.Data.Array.Attach
Array.map_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} {g : β → γ} {f : (a : α) → p a → β} {xs : Array α}
  (H : ∀ a ∈ xs, p a), Array.map g (Array.pmap f xs H) = Array.pmap (fun a h => g (f a h)) xs H
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- If `s = s'` on `u` and `s i` is a local frame on `u`, then so is `s'`.  -/
IsLocalFrameOn.congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s s' : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞},
  IsLocalFrameOn I F n s u → (∀ (i : ι), ∀ x ∈ u, s i x = s' i x) → IsLocalFrameOn I F n s' u
-- Std.Data.HashSet.Lemmas
Std.HashSet.length_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m.toList.length = m.size
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mclosure_range_inl_union_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Submonoid.closure (Set.range ⇑Monoid.Coprod.inl ∪ Set.range ⇑Monoid.Coprod.inr) = ⊤
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IicExtend_self : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {b : α} (f : ↑(Set.Iic b) → β), Set.IicExtend f b = f ⟨b, ⋯⟩
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.of_zsmul : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G} {z : ℤ}, a ≡ b [PMOD z • p] → a ≡ b [PMOD p]
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.List.filterRevM.eq_1 : ∀ {m : Type → Type v} [inst : Monad m] {α : Type} (p : α → m Bool) (as : List α),
  List.filterRevM p as = List.filterAuxM p as.reverse []
-- Mathlib.Topology.Sequences
/-- In a sequential space, a set is closed iff it's sequentially closed.  -/
isSeqClosed_iff_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [SequentialSpace X] {M : Set X}, IsSeqClosed M ↔ IsClosed M
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
AdicCompletion.ofTensorProduct_comp_ofTensorProductInvOfPiFintype : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (ι : Type u_4) [inst_1 : Fintype ι] [inst_2 : DecidableEq ι],
  AdicCompletion.ofTensorProduct I (ι → R) ∘ₗ ↑(AdicCompletion.ofTensorProductInvOfPiFintype I ι) = LinearMap.id
-- Init.Data.String.Lemmas.FindPos
_private.Init.Data.String.FindPos.0.String.Slice.Pos.prevn.match_1.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ) (n_1 : ℕ),
  n = n_1.succ →
    (match n with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_2 n_1
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.continuousAt : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x : E}, ContinuousAt (⇑e) x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp] (t t_1 : Std.DTreeMap α β cmp),
  t = t_1 → ∀ (a : α), t.get? a = t_1.get? a
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.primitiveEdge_coe_down : ∀ {n : ℕ} {i : Fin (n + 1)} (h₀ : 0 < i) (hₙ : i < Fin.last n) (j : Fin n),
  (↑(SSet.horn.primitiveEdge h₀ hₙ j)).down = SimplexCategory.Hom.mk { toFun := ![j.castSucc, j.succ], monotone' := ⋯ }
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.symm_k : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E), P.symm.k = P.k
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.imageUnopOp_hom_comp_image_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.imageUnopOp g).hom (CategoryTheory.Limits.image.ι g) =
    (CategoryTheory.Limits.factorThruImage g.unop).op
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
/-- Let `F` be a prestack for a Grothendieck topology `J`,
`f : X i ⟶ S` and `f' : X' j ⟶ S` be two families of morphisms.
Assume that `f'` is a covering family for `J`, then
functors `F.pullFunctor .. : F.DescentData f ⥤ F.DescentData f'`
are fully faithful.  -/
CategoryTheory.Pseudofunctor.DescentData.fullyFaithfulPullFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {J : CategoryTheory.GrothendieckTopology C} →
        [F.IsPrestack J] →
          {ι : Type t} →
            {S : C} →
              {X : ι → C} →
                {f : (i : ι) → X i ⟶ S} →
                  {ι' : Type t'} →
                    {X' : ι' → C} →
                      {f' : (j : ι') → X' j ⟶ S} →
                        {α : ι' → ι} →
                          {p' : (j : ι') → X' j ⟶ X (α j)} →
                            (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j) →
                              CategoryTheory.Sieve.ofArrows X' f' ∈ J S →
                                (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).FullyFaithful
-- Mathlib.Data.Multiset.Fintype
Multiset.sum_eq_sum_toEnumFinset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommMonoid α] (m : Multiset α), m.sum = ∑ x ∈ m.toEnumFinset, x.1
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftCoyonedaEquiv_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor C (Type (max w v₁))}
  (f : CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.uliftCoyonedaEquiv f) =
    CategoryTheory.uliftCoyonedaEquiv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.map g.op) f)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trCont.eq_2 : ∀ (c : Turing.ToPartrec.Code) (a : List ℕ) (k : Turing.ToPartrec.Cont),
  Turing.PartrecToTM2.trCont (Turing.ToPartrec.Cont.cons₁ c a k) =
    Turing.PartrecToTM2.Cont'.cons₁ c (Turing.PartrecToTM2.trCont k)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toList_roo : ∀ {m n fallback : ℤ} {i : ℕ}, (m<...n).toList.getD i fallback = if i < (n - (m + 1)).toNat then m + 1 + ↑i else fallback
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.deriv_limit : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}) {o : Ordinal.{u_1}},
  Order.IsSuccLimit o → Ordinal.deriv f o = ⨆ a, Ordinal.deriv f ↑a
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
/-- For any `I : Ideal A`, not necessarily homogeneous, `I.homogeneousHull 𝒜` is
the smallest homogeneous ideal containing `I`.  -/
Ideal.homogeneousHull : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] → (𝒜 : ι → σ) → [inst_5 : GradedRing 𝒜] → Ideal A → HomogeneousIdeal 𝒜
-- Mathlib.Algebra.Lie.Basic
leibniz_lie : ∀ {L₁ : Type u_1} {L₂ : Type u_2} {M : Type u_3} [inst : Bracket L₁ L₂] [inst_1 : Bracket L₁ M] [inst_2 : Bracket L₂ M]
  [inst_3 : Add M] [IsLieTower L₁ L₂ M] (x : L₁) (y : L₂) (m : M), ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
-- Mathlib.Combinatorics.Colex
Finset.equivBitIndices_symm_apply : ∀ (s : Finset ℕ), Finset.equivBitIndices.symm s = ∑ i ∈ s, 2 ^ i
-- Mathlib.RingTheory.LocalProperties.Basic
/-- Variant of `RingHom.OfLocalizationSpan.ofIsLocalization` where
`fᵣ = IsLocalization.Away.map`.  -/
RingHom.OfLocalizationSpan.ofIsLocalization' : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
      ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set R),
        Ideal.span s = ⊤ →
          (∀ (r : ↑s),
              ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
                ∃ (x_4 : IsLocalization.Away (↑r) Rᵣ) (x_5 : IsLocalization.Away (f ↑r) Sᵣ),
                  P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)) →
            P f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- Auxiliary definition for `SimpleGraph.Walk.concatRec`  -/
SimpleGraph.Walk.concatRecAux : {V : Type u} →
  {G : SimpleGraph V} →
    {motive : (u v : V) → G.Walk u v → Sort u_1} →
      ({u : V} → motive u u SimpleGraph.Walk.nil) →
        ({u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)) →
          {u v : V} → (p : G.Walk u v) → motive v u p.reverse
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
doublyStochastic.eq_1 : ∀ (R : Type u_3) (n : Type u_4) [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R],
  doublyStochastic R n =
    { carrier := {M | (∀ (i j : n), 0 ≤ M i j) ∧ M.mulVec 1 = 1 ∧ Matrix.vecMul 1 M = 1}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Lean.Parser.Term
Lean.Parser.Termination.terminationBy.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Part
Part.neg_mem_neg : ∀ {α : Type u_1} [inst : Neg α] (a : Part α), ∀ ma ∈ a, -ma ∈ -a
-- Mathlib.Order.Interval.Finset.Floor
Nat.cast_mem_Icc_iff : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [inst_2 : FloorSemiring α] {a b : α} {n : ℕ},
  0 ≤ b → (↑n ∈ Set.Icc a b ↔ n ∈ Finset.Icc ⌈a⌉₊ ⌊b⌋₊)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
_private.Mathlib.MeasureTheory.VectorMeasure.Basic.0.MeasureTheory.VectorMeasure.restrict.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M) (i : Set α),
  v.restrict i =
    if hi : MeasurableSet i then
      { measureOf' := fun s => if MeasurableSet s then v (s ∩ i) else 0, empty' := ⋯, not_measurable' := ⋯,
        m_iUnion' := ⋯ }
    else 0
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.comp.congr_simp : ∀ {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'} {R'' : Type u_4} {S'' : Type u_5} [inst_6 : CommRing R''] [inst_7 : CommRing S'']
  [inst_8 : Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [inst_9 : Algebra R R'] [inst_10 : Algebra R' R'']
  [inst_11 : Algebra R R''] [inst_12 : Algebra S S'] [inst_13 : Algebra S' S''] [inst_14 : Algebra S S'']
  [inst_15 : IsScalarTower R R' R''] [inst_16 : IsScalarTower S S' S''] (f f_1 : P'.Hom P''),
  f = f_1 → ∀ (g g_1 : P.Hom P'), g = g_1 → f.comp g = f_1.comp g_1
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- A vector lies in the `vectorSpan` of two points if and only if it is a multiple of their
difference.  -/
mem_vectorSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ : P} {v : V}, v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.ext : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} ⦃f g : B₁ →bᵢ B₂⦄, (∀ (x : M₁), f x = g x) → f = g
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNegQuotient : {R : Type u_1} → [inst : AddGroup R] → [inst_1 : Mul R] → (c : RingCon R) → Neg c.Quotient
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
_private.Mathlib.Analysis.CStarAlgebra.ApproximateUnit.0.termσₙ : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyRel.factorsThroughLocalization : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.RightHomotopyRel.FactorsThroughLocalization (HomotopicalAlgebra.weakEquivalences C)
-- Mathlib.Topology.Order.Lattice
LinearOrder.topologicalLattice : ∀ {L : Type u_1} [inst : TopologicalSpace L] [inst_1 : LinearOrder L] [OrderClosedTopology L], TopologicalLattice L
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.instInhabitedConfig : Inhabited Mathlib.Meta.FunProp.Config
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- **Alias** of `ContMDiffWithinAt.curry_left`.

---

Curried `C^n` functions are `C^n` in the first coordinate.  -/
ContMDiffWithinAt.along_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {x : M} {y : M'} {s : Set (M × M')},
  ContMDiffWithinAt (I.prod I') J n (Function.uncurry f) s (x, y) →
    ContMDiffWithinAt I J n (fun x => f x y) {x | (x, y) ∈ s} x
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.rfind'.inj : ∀ {a a_1 : Nat.Partrec.Code}, a.rfind' = a_1.rfind' → a = a_1
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  {F : TopCat.Presheaf C X} {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {G : TopCat.Presheaf C X} (α : F ≅ G),
  TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIso U α =
    CategoryTheory.NatIso.ofComponents
      (fun X_1 =>
        CategoryTheory.Limits.WalkingParallelPair.casesOn X_1
          (TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.isoOfIso U α)
          (TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.isoOfIso U α))
      ⋯
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.coe_compl : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : Subtype MeasurableSet), ↑sᶜ = (↑s)ᶜ
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- Project the Frobenius automorphism from an isocrystal. Denoted by `Φ(p, k)` when V can be inferred.
 -/
WittVector.Isocrystal.frobenius : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (k : Type u_1) →
      [inst_1 : CommRing k] →
        [inst_2 : CharP k p] →
          [inst_3 : PerfectRing k p] →
            {V : Type u_2} →
              [inst_4 : AddCommGroup V] →
                [inst_5 : WittVector.Isocrystal p k V] → V ≃ₛₗ[WittVector.FractionRing.frobeniusRingHom p k] V
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- The pair `f,g` is a cosplit pair if there is an `h : W ⟶ X` so that `f, g, h` forms a split
equalizer in `C`.
 -/
CategoryTheory.HasSplitEqualizer : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → (X ⟶ Y) → Prop
-- Mathlib.CategoryTheory.EqToHom
/-- Two morphisms are conjugate via eqToHom if and only if they are heterogeneously equal.
Note this used to be in the Functor namespace, where it doesn't belong.  -/
CategoryTheory.conj_eqToHom_iff_heq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y)
  (h' : X = Z),
  f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h)
        (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom ⋯)) ↔
    f ≍ g
-- Mathlib.Geometry.Manifold.Complex
/-- **Maximum modulus principle**: if `f : M → F` is complex differentiable in a neighborhood of `c`
and the norm `‖f z‖` has a local maximum at `c`, then `‖f z‖` is locally constant in a neighborhood
of `c`. This is a manifold version of `Complex.norm_eventually_eq_of_isLocalMax`.  -/
Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {H : Type u_3} [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless]
  {M : Type u_4} [inst_6 : TopologicalSpace M] [inst_7 : ChartedSpace H M] [IsManifold I 1 M] {f : M → F} {c : M},
  (∀ᶠ (z : M) in nhds c, MDiffAt f z) → IsLocalMax (norm ∘ f) c → ∀ᶠ (y : M) in nhds c, ‖f y‖ = ‖f c‖