mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.BorelCantelli
MeasureTheory.filtrationOfSet.congr_simp : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {s s_1 : ι → Set Ω} (e_s : s = s_1)
  (hsm : ∀ (i : ι), MeasurableSet (s i)), MeasureTheory.filtrationOfSet hsm = MeasureTheory.filtrationOfSet ⋯
-- Mathlib.Data.Matrix.Basis
Matrix.row_eq_zero_of_commute_single : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Semiring α] {i j k : n}
  {M : Matrix n n α}, Commute (Matrix.single i j 1) M → k ≠ j → M j k = 0
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroUInt16UintOfNatNat : Lean.Grind.ToInt.Zero UInt16 (Lean.Grind.IntInterval.uint 16)
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.exists_eq_X_add_C_of_natDegree_le_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.natDegree ≤ 1 → ∃ a b, p = Polynomial.C a * Polynomial.X + Polynomial.C b
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.unit_of_mem_ofUnits_spec_val_eq_of_mem : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) {x : M} (h : x ∈ S.ofUnits), ↑(S.unit_of_mem_ofUnits h) = x
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.mixedEmbedding.minkowskiBound.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  NumberField.mixedEmbedding.minkowskiBound K I =
    MeasureTheory.volume (ZSpan.fundamentalDomain (NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I)) *
      2 ^ Module.finrank ℝ (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.empty_zpow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionMonoid α] {n : ℤ}, n ≠ 0 → ∅ ^ n = ∅
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- An `n`-independent set in the complement graph is an `n`-clique and vice versa.  -/
SimpleGraph.isNIndepSet_compl : ∀ {α : Type u_1} (G : SimpleGraph α) {n : ℕ} {s : Finset α}, Gᶜ.IsNIndepSet n s ↔ G.IsNClique n s
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
/-- If `A` has no columns, then it is totally unimodular.  -/
Matrix.emptyCols_isTotallyUnimodular : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] [IsEmpty n] (A : Matrix m n R), A.IsTotallyUnimodular
-- Mathlib.Topology.DerivedSet
IsPreconnected.inter_derivedSet_nonempty : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {U : Set X},
  IsPreconnected U →
    ∀ (a b : Set X),
      U ⊆ a ∪ b →
        (U ∩ derivedSet a).Nonempty → (U ∩ derivedSet b).Nonempty → (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
-- Init.Data.Rat.Lemmas
Rat.den_intCast : ∀ (a : ℤ), (↑a).den = 1
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.FibrantObject.localizerMorphism C).IsLocalizedEquivalence
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_fn_integral_add : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] {E' : Type u_5} [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace ℝ E']
  ⦃f g : β × γ → E⦄ (F : E → E'),
  MeasureTheory.Integrable f ((κ.compProd η) a) →
    MeasureTheory.Integrable g ((κ.compProd η) a) →
      ∫ (x : β), F (∫ (y : γ), f (x, y) + g (x, y) ∂η (a, x)) ∂κ a =
        ∫ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) + ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a
-- Mathlib.Order.Birkhoff
OrderIso.infIrredUpperSet.congr_simp : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Finite α], OrderIso.infIrredUpperSet = OrderIso.infIrredUpperSet
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.adjoin_le_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {s : Set A},
  NonUnitalAlgebra.adjoin R s ≤ S ↔ s ⊆ ↑S
-- Mathlib.Order.Defs.LinearOrder
max_eq_right_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a < b → max a b = b
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.category_id_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C)
  (X : CategoryTheory.Cokleisli U), (CategoryTheory.CategoryStruct.id X).of = U.ε.app X.of
-- Init.Data.Array.Lemmas
Array.contains_iff_exists_mem_beq : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α} {a : α}, xs.contains a = true ↔ ∃ a' ∈ xs, (a == a') = true
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.instIsRootSystemMap : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {ι₂ : Type u_5}
  {M₂ : Type u_6} {N₂ : Type u_7} [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂]
  [inst_8 : Module R N₂] [P.IsRootSystem] (e : ι ≃ ι₂) (f : M ≃ₗ[R] M₂) (g : N ≃ₗ[R] N₂),
  (RootPairing.map e f g).IsRootSystem
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.ringEquivOfRingEquiv_symm : ∀ {A : Type u_8} {K : Type u_9} {B : Type u_10} {L : Type u_11} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing K] [inst_3 : CommRing L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K]
  [inst_6 : Algebra B L] [inst_7 : IsFractionRing B L] (h : A ≃+* B),
  (IsFractionRing.ringEquivOfRingEquiv h).symm = IsFractionRing.ringEquivOfRingEquiv h.symm
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality : ∀ (X Y : SSet.Truncated 2)
  [inst : Unique (X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))]
  [inst_1 :
    Subsingleton
      (X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.HomotopyCategory.isoTerminal._proof_1 }))],
  CategoryTheory.Prod.snd (↑CategoryTheory.Cat.chosenTerminal) Y.HomotopyCategory =
    ((SSet.Truncated.HomotopyCategory.isoTerminal X).inv.toFunctor.prod
          (CategoryTheory.Functor.id Y.HomotopyCategory)).comp
      ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
        (SSet.Truncated.mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)))
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.run? : {α : Type} → Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ α → Lean.MetaM (Option α)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mk'_mem_incidenceSet_iff : ∀ {V : Type u} (G : SimpleGraph V) {a b c : V}, s(b, c) ∈ G.incidenceSet a ↔ G.Adj b c ∧ (a = b ∨ a = c)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_zero : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A), ↑0 = 0
-- Mathlib.Algebra.Ring.InjSurj
/-- A type endowed with `-` and `*` has distributive negation, if it admits a surjective map that
preserves `-` and `*` from a type which has distributive negation.  -/
Function.Surjective.hasDistribNeg : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Mul S] →
          [inst_1 : Neg S] →
            [inst_2 : Mul R] →
              [inst_3 : HasDistribNeg R] →
                (∀ (a : R), f (-a) = -f a) → (∀ (a b : R), f (a * b) = f a * f b) → HasDistribNeg S
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticAt.re_ofReal : ∀ {f : ℂ → ℂ} {x : ℝ}, AnalyticAt ℂ f ↑x → AnalyticAt ℝ (fun x => (f ↑x).re) x
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- The points with `v.limRatioMeas hρ x = 0` have measure `0` for `ρ`.  -/
VitaliFamily.measure_limRatioMeas_zero : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α]
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ), ρ (v.limRatioMeas hρ ⁻¹' {0}) = 0
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.mk.inj : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} {inst : CommSemiring R} {inst_1 : AddCommMonoid M₁}
  {inst_2 : AddCommMonoid M₂} {inst_3 : AddCommMonoid N} {inst_4 : Module R M₁} {inst_5 : Module R M₂}
  {inst_6 : Module R N} {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {toLinearMap : M₁ →ₗ[R] M₂}
  {map_app' : ∀ (m : M₁), Q₂ (toLinearMap.toFun m) = Q₁ m} {toLinearMap_1 : M₁ →ₗ[R] M₂}
  {map_app'_1 : ∀ (m : M₁), Q₂ (toLinearMap_1.toFun m) = Q₁ m},
  { toLinearMap := toLinearMap, map_app' := map_app' } = { toLinearMap := toLinearMap_1, map_app' := map_app'_1 } →
    toLinearMap = toLinearMap_1
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.universallyClosed_isStableUnderComposition : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.UniversallyClosed
-- Std.Http.Data.URI.Basic
Std.Http.URI.instReprUserInfo.repr : Std.Http.URI.UserInfo → ℕ → Std.Format
-- Mathlib.MeasureTheory.Measure.Prod
/-- Change the order of Lebesgue integration.  -/
MeasureTheory.lintegral_lintegral_swap : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] ⦃f : α → β → ENNReal⦄,
  AEMeasurable (Function.uncurry f) (μ.prod ν) →
    ∫⁻ (x : α), ∫⁻ (y : β), f x y ∂ν ∂μ = ∫⁻ (y : β), ∫⁻ (x : α), f x y ∂μ ∂ν
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.decidableElim.inj : ∀ {classical : Bool} {p₁ x : Lean.Name} {p₂ p₃ : Mathlib.Tactic.ITauto.Proof} {classical_1 : Bool}
  {p₁_1 x_1 : Lean.Name} {p₂_1 p₃_1 : Mathlib.Tactic.ITauto.Proof},
  Mathlib.Tactic.ITauto.Proof.decidableElim classical p₁ x p₂ p₃ =
      Mathlib.Tactic.ITauto.Proof.decidableElim classical_1 p₁_1 x_1 p₂_1 p₃_1 →
    classical = classical_1 ∧ p₁ = p₁_1 ∧ x = x_1 ∧ p₂ = p₂_1 ∧ p₃ = p₃_1
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofRingEquiv_symm_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {f : A₁ ≃+* A₂}
  (hf : ∀ (x : R), f ((algebraMap R A₁) x) = (algebraMap R A₂) x) (a : A₂), (AlgEquiv.ofRingEquiv hf).symm a = f.symm a
-- Mathlib.Logic.Function.Basic
Function.rightInverse_surjInv : ∀ {α : Sort u} {β : Sort v} {f : α → β} (hf : Function.Surjective f), Function.RightInverse (Function.surjInv hf) f
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{0, 0, v, u} C],
  CategoryTheory.Limits.HasFiniteColimits C
-- Mathlib.Data.Prod.PProd
PProd.mk.injArrow : {α : Type u_5} →
  {β : Type u_6} →
    {x₁ : α} → {y₁ : β} → {x₂ : α} → {y₂ : β} → (x₁, y₁) = (x₂, y₂) → ⦃P : Sort u_7⦄ → (x₁ = x₂ → y₁ = y₂ → P) → P
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.isCyclic_units_two_mul_iff_of_odd : ∀ (n : ℕ), Odd n → (IsCyclic (ZMod (2 * n))ˣ ↔ IsCyclic (ZMod n)ˣ)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The induced map `∐ I.left ⟶ ∐ I.right` via `I.snd`.  -/
CategoryTheory.Limits.MultispanIndex.sndSigmaMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct I.left] →
          [inst_2 : CategoryTheory.Limits.HasCoproduct I.right] → ∐ I.left ⟶ ∐ I.right
-- Mathlib.Topology.MetricSpace.Infsep
Finset.infsep_pos_iff_nontrivial : ∀ {α : Type u_1} [inst : MetricSpace α] (s : Finset α), 0 < (↑s).infsep ↔ (↑s).Nontrivial
-- Init.Data.Int.DivMod.Lemmas
Int.sub_mul_fmod_self_left : ∀ (a b c : ℤ), (a - b * c).fmod b = a.fmod b
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Given a pair of multiplicative homomorphisms `f`, `g` such that `g.comp f = id` and
`f.comp g = id`, returns a multiplicative equivalence with `toFun = f` and `invFun = g`. This
constructor is useful if the underlying type(s) have specialized `ext` lemmas for multiplicative
homomorphisms.  -/
MulHom.toMulEquiv : {M : Type u_4} →
  {N : Type u_5} →
    [inst : Mul M] →
      [inst_1 : Mul N] → (f : M →ₙ* N) → (g : N →ₙ* M) → g.comp f = MulHom.id M → f.comp g = MulHom.id N → M ≃* N
-- Mathlib.Order.Category.PartOrdEmb
/-- Constructs an equivalence between partial orders from an order isomorphism between them.  -/
PartOrdEmb.Iso.mk : {α β : PartOrdEmb} → ↑α ≃o ↑β → (α ≅ β)
-- Mathlib.Algebra.Group.Commute.Units
Commute.inv_mul_eq_inv_mul_iff_of_isUnit : ∀ {M : Type u_1} [inst : DivisionMonoid M] {a b c d : M},
  Commute b d → IsUnit b → IsUnit d → (b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivAt.finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ},
  HasFDerivAt φ φ' x → HasFDerivAt φs φs' x → HasFDerivAt (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionList : Type
-- Init.Data.List.Basic
/-- Lexicographic ordering of lists with respect to an ordering on their elements.

`as < bs` if
* `as` is empty and `bs` is non-empty, or
* both `as` and `bs` are non-empty, and the head of `as` is less than the head of `bs`, or
* both `as` and `bs` are non-empty, their heads are equal, and the tail of `as` is less than the
  tail of `bs`.
 -/
List.lt : {α : Type u} → [LT α] → List α → List α → Prop
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
/-- If `G` has a topology, and `H ≤ K` are subgroups, then `H` as a subgroup of `K` is isomorphic,
as a topological group, to `H` as a subgroup of `G`. This is `subgroupOfEquivOfLe` upgraded to a
`ContinuousMulEquiv`.  -/
Subgroup.subgroupOfContinuousMulEquivOfLe : {G : Type u_1} →
  [inst : Group G] → [inst_1 : TopologicalSpace G] → {H K : Subgroup G} → H ≤ K → ↥(H.subgroupOf K) ≃ₜ* ↥H
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharNeTwoNF.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : Invertible 2],
  W.toCharNeTwoNF = { u := 1, r := 0, s := ⅟2 * -W.a₁, t := ⅟2 * -W.a₃ }
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.Adj.snd_mem : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u v : V}, H.Adj u v → v ∈ H.verts
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.antidiagonalTuple.eq_1 : List.Nat.antidiagonalTuple 0 0 = [![]]
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.mapComp'_eq_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂),
  F.mapComp' f g (CategoryTheory.CategoryStruct.comp f g) ⋯ = F.mapComp f g
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
/-- If `M` is an additive monoid object acting on `X`, then morphisms into `M` act on
morphisms into `X`.  -/
CategoryTheory.Hom.addAction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {M : C} →
        [inst_2 : CategoryTheory.AddMonObj M] →
          {X : C} → [CategoryTheory.AddModObj M X] → (Z : C) → AddAction (Z ⟶ M) (Z ⟶ X)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.dualEquiv_inverse : PartOrdEmb.dualEquiv.inverse = PartOrdEmb.dual
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_inter_add_sdiff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [T2Space M] [inst_3 : ContinuousAdd M] {v : MeasureTheory.VectorMeasure α M} {s t : Set α},
  MeasurableSet s → MeasurableSet t → v.restrict (s ∩ t) + v.restrict (s \ t) = v.restrict s
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_bijective : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] {f : M →ₗ[R] N}
  {g : P →ₗ[R] Q}, Function.Bijective ⇑f → Function.Bijective ⇑g → Function.Bijective ⇑(TensorProduct.map f g)
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.vec_iff : ∀ {m n : ℕ} {f : List.Vector ℕ m → List.Vector ℕ n}, Nat.Primrec'.Vec f ↔ Primrec f
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.FinMeasSupp.mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : MulZeroClass β]
  {f g : MeasureTheory.SimpleFunc α β}, f.FinMeasSupp μ → g.FinMeasSupp μ → (f * g).FinMeasSupp μ
-- Mathlib.Order.Compare
Ordering.Compares.eq_gt : ∀ {α : Type u_1} [inst : Preorder α] {o : Ordering} {a b : α}, o.Compares a b → (o = Ordering.gt ↔ b < a)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.injOn_pow : ∀ {M : Type u_1} [inst : CommMonoid M] {n : ℕ} {ζ : M},
  IsPrimitiveRoot ζ n → Set.InjOn (fun x => ζ ^ x) ↑(Finset.range n)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.completeOn_vertexSet : ∀ {α : Type u_1} (f : Set α), (Hypergraph.completeOn f).vertexSet = f
-- Mathlib.Algebra.Group.Units.Hom
Units.coeHom.eq_1 : ∀ (M : Type u) [inst : Monoid M], Units.coeHom M = { toFun := Units.val, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.ProdL2
WithLp.instProdInnerProductSpace : {𝕜 : Type u_1} →
  {E : Type u_4} →
    {F : Type u_5} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] → [InnerProductSpace 𝕜 F] → InnerProductSpace 𝕜 (WithLp 2 (E × F))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P 2 = 0 → Q 2 ≠ 0 → ¬P ≈ Q
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.ofRestrict_app : ∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : X.Opens),
  AlgebraicGeometry.Scheme.Hom.app (X.ofRestrict h) V = X.presheaf.map (⋯.adjunction.counit.app V).op
-- Init.Data.BitVec.Basic
BitVec.sub_eq : ∀ {w : ℕ} (x y : BitVec w), x.sub y = x - y
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterM.match_1.splitter : {β : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → n (ULift.{u_1, 0} Bool)} →
      [inst : MonadAttach n] →
        (out : β) →
          (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) →
            (__do_lift : Subtype (MonadAttach.CanReturn (f out))) →
              ((hf : MonadAttach.CanReturn (f out) { down := false }) → motive ⟨{ down := false }, hf⟩) →
                ((hf : MonadAttach.CanReturn (f out) { down := true }) → motive ⟨{ down := true }, hf⟩) →
                  motive __do_lift
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coeAddMonoidHom.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddZeroClass α],
  Finset.coeAddMonoidHom = { toFun := SetLike.coe, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Time.Format.DateFormat
/-- Narrow weekday names (7 elements, index 0 = M).
 -/
Std.Time.DateFormatSymbols.weekdayNarrow : Std.Time.DateFormatSymbols → Vector String 7
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.bihimp_def : ∀ {α : Type u_1} {s t : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α], bihimp s t = (s ∪ tᶜ) ∩ (t ∪ sᶜ)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.eq_of_eqOn_top : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.Hom M N}, Set.EqOn ⇑f ⇑g ↑⊤ → f = g
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.mapMulHom.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : Mul β] (f : α →ₙ* β),
  WithOne.mapMulHom f = WithOne.lift (WithOne.coeMulHom.comp f)
-- Mathlib.Analysis.MeanInequalities
/-- **Weighted Hölder inequality** in terms of `Finset.expect`.  -/
Real.compact_inner_le_weight_mul_Lp_of_nonneg : ∀ {ι : Type u} (s : Finset ι) {p : ℝ},
  1 ≤ p →
    ∀ {w f : ι → ℝ},
      (∀ (i : ι), 0 ≤ w i) →
        (∀ (i : ι), 0 ≤ f i) →
          (s.expect fun i => w i * f i) ≤ (s.expect fun i => w i) ^ (1 - p⁻¹) * (s.expect fun i => w i * f i ^ p) ^ p⁻¹
-- Mathlib.CategoryTheory.Action.Continuous
ContAction.resCongr.congr_simp : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3}
  [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_2 : CategoryTheory.ConcreteCategory V FV]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  {H : Type u_5} [inst_6 : Monoid H] [inst_7 : TopologicalSpace H] (f f' : G →ₜ* H) (h : f = f'),
  ContAction.resCongr V f f' h = ContAction.resCongr V f f' h
-- Mathlib.Algebra.Order.Sub.Unbundled.Hom
map_tsub_of_le : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [ExistsAddOfLE α]
  [AddLeftMono α] [inst_4 : Sub α] [OrderedSub α] [inst_6 : PartialOrder β] [inst_7 : AddCommSemigroup β]
  [inst_8 : Sub β] [OrderedSub β] [AddLeftReflectLE β] [inst_11 : FunLike F α β] [AddHomClass F α β] (f : F) (a b : α),
  b ≤ a → f a - f b = f (a - b)
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.π_r : {S : Type u_1} →
  {T : Type u_2} →
    {X : Type u_3} →
      (π : T → S × Option X) → (σ : Option X → S → T) → ↑(InternalProjectivityProof.fibres✝ π σ) → S × Option X
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.ker_coFG_iff_hasFiniteRange : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂}, f.ker.CoFG ↔ f.HasFiniteRange
-- Mathlib.Topology.ContinuousMap.Bounded.Star
BoundedContinuousFunction.instStarRing : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : NonUnitalNormedRing β] →
        [inst_2 : StarRing β] → [NormedStarGroup β] → StarRing (BoundedContinuousFunction α β)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {t : CategoryTheory.Limits.PushoutCocone f g} (ht : CategoryTheory.Limits.IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
  CategoryTheory.CategoryStruct.comp t.inl (CategoryTheory.Limits.PushoutCocone.IsColimit.desc ht h k w) = h