mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.instAlgebraSubtypeMemMin : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] → [inst_2 : Algebra F E] → (K₁ K₂ : IntermediateField F E) → Algebra ↥(K₁ ⊓ K₂) ↥K₁
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolResult.mk.sizeOf_spec : ∀ (syms : Array Lean.Lsp.DocumentSymbol), sizeOf { syms := syms } = 1 + sizeOf syms
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R),
  Set.BijOn ⇑(Rat.HeightOneSpectrum.adicCompletion.padicEquiv v)
    ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v)
    ↑(PadicInt.subring ↑(Rat.HeightOneSpectrum.primesEquiv v))
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_mul : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : (i : ι) → Mul (G i)]
  [inst_6 : Mul C] [inst_7 : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)]
  [∀ (i : ι), MulHomClass (H i) (G i) C] (g : (i : ι) → H i)
  (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x y : DirectLimit G f),
  DirectLimit.lift f (fun x => ⇑(g x)) h (x * y) =
    DirectLimit.lift f (fun x => ⇑(g x)) h x * DirectLimit.lift f (fun x => ⇑(g x)) h y
-- Mathlib.Algebra.Field.Defs
/-- Scalar multiplication by a nonnegative rational number.

Unless there is a risk of a `Module ℚ≥0 _` instance diamond, write `nnqsmul := _`. This will set
`nnqsmul` to `(NNRat.cast · * ·)` thanks to unification in the default proof of `nnqsmul_def`.

Do not use directly. Instead use the `•` notation.  -/
DivisionRing.nnqsmul : {K : Type u_2} → [self : DivisionRing K] → ℚ≥0 → K → K
-- Mathlib.Analysis.Normed.Group.Uniform
CauchySeq.mul_norm_bddAbove : ∀ {G : Type u_4} [inst : SeminormedGroup G] {u : ℕ → G}, CauchySeq u → BddAbove (Set.range fun n => ‖u n‖)
-- Std.Time.Format.Modifier
/-- Two-digit year format (e.g., "23" for 2023)
 -/
Std.Time.Year.twoDigit : Std.Time.Year
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_modifyKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    ∀ {h : Std.Internal.List.containsKey k (Std.Internal.List.modifyKey k f l) = true},
      Std.Internal.List.getValueCast k (Std.Internal.List.modifyKey k f l) h = f (Std.Internal.List.getValueCast k l ⋯)
-- Init.Data.SInt.Lemmas
Int16.add_sub_cancel : ∀ (a b : Int16), a + b - b = a
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_toCompletion : ∀ {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) (k : K),
  { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm k) }.toCompletion =
    ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm k)
-- Mathlib.Tactic.FunProp.Elab
/-- `fun_prop` solves a goal of the form `P f`, where `P` is a predicate and `f` is a function,
by decomposing `f` into a composition of elementary functions, and proving `P` on each of those
by matching against a set of `@[fun_prop]` lemmas.

If `fun_prop` fails to solve a goal with the error "No theorems found", you can solve this issue
by importing or adding new theorems tagged with the `@[fun_prop]` attribute. See the module
documentation for `Mathlib/Tactic/FunProp.lean` for a detailed explanation.

* `fun_prop (disch := tac)` uses `tac` to solve potential side goals. Setting this option is
  required to solve `ContinuousAt/On/Within` goals. Assumptions from the local context are
  automatically discharged.
* `fun_prop [c, ...]` will unfold the constant(s) `c`, ... before decomposing `f`.
* `fun_prop (config := cfg)` sets advanced configuration options using `cfg : FunProp.Config`
  (see `FunProp.Config` for details).
  These options can be combined: `fun_prop (config := cfg) (disch := tac) [c]`

Examples:

```lean
example : Continuous (fun x : ℝ ↦ x * sin x) := by fun_prop
```

```lean
-- Solving `ContinuousAt`/`Within`/`On` goals might require using dischargers:
example (y : ℝ) (hy : y ≠ 0) : ContinuousAt (fun x : ℝ ↦ 1/x) y := by
  fun_prop

example (y : ℝ) (hy : y ≠ 0) : ContinuousAt (fun x => x * (Real.log x) ^ 2 - Real.exp x / x) y := by
  fun_prop (disch := aesop)
```

 -/
Mathlib.Meta.FunProp.funPropTacStx : Lean.ParserDescr
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.inv_add_inv_ennreal : ∀ {p q : NNReal}, p.HolderConjugate q → ↑p⁻¹ + ↑q⁻¹ = 1
-- Mathlib.RingTheory.WittVector.StructurePolynomial
witt_structure_prop : ∀ (p : ℕ) {R : Type u_1} {idx : Type u_2} [inst : CommRing R] [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ)
  (n : ℕ),
  (MvPolynomial.aeval fun i => (MvPolynomial.map (Int.castRingHom R)) (wittStructureInt p Φ i)) (wittPolynomial p ℤ n) =
    (MvPolynomial.aeval fun i => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p R n)) Φ
-- Lean.Environment
Lean.Environment.Visibility.noConfusionType : Sort v✝ → Lean.Environment.Visibility → Lean.Environment.Visibility → Sort v✝
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_measurePreserving_sumPiEquivProdPi : ∀ {ι : Type u_1} {ι' : Type u_2} [inst : Fintype ι] [inst_1 : Fintype ι'] (X : ι ⊕ ι' → Type u_4)
  [inst_2 : (i : ι ⊕ ι') → MeasureTheory.MeasureSpace (X i)]
  [∀ (i : ι ⊕ ι'), MeasureTheory.SigmaFinite MeasureTheory.volume],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi X)) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.LinearAlgebra.DFinsupp
Submodule.dfinsuppSumAddHom_mem : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : DecidableEq ι] {β : ι → Type u_7} [inst_4 : (i : ι) → AddZeroClass (β i)] (S : Submodule R N)
  (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ N), (∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ S) → (DFinsupp.sumAddHom g) f ∈ S
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.HasPointwiseRightKanExtension.of_iso : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L L' : CategoryTheory.Functor C D} {F F' : CategoryTheory.Functor C H} [L.HasPointwiseRightKanExtension F]
  (e₁ : L ≅ L') (e₂ : F ≅ F'), L'.HasPointwiseRightKanExtension F'
-- Init.Data.Random
/-- The range of values returned by `StdGen`  -/
stdRange : ℕ × ℕ
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsUpper.topology_eq : ∀ (α : Type u_1) [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α], inst_1 = Topology.upper α
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.extend_pureCauchy : ∀ {α : Type u} [inst : UniformSpace α] {β : Type v} [inst_1 : UniformSpace β] [T0Space β] {f : α → β},
  UniformContinuous f → ∀ (a : α), CauchyFilter.extend f (CauchyFilter.pureCauchy a) = f a
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} {x : G}
  {f' : G →L[𝕜] E}, HasFDerivWithinAt (⇑iso ∘ f) (↑iso ∘SL f') s x ↔ HasFDerivWithinAt f f' s x
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_monomial : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S) {n : ℕ} {r : R},
  Polynomial.eval₂ f x ((Polynomial.monomial n) r) = f r * x ^ n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertMin_eq_insertMin! : ∀ {α : Type u} {β : α → Type v} [Ord α] {a : α} {b : β a} {t : Std.DTreeMap.Internal.Impl α β} (htb : t.Balanced),
  (Std.DTreeMap.Internal.Impl.insertMin a b t htb).impl = Std.DTreeMap.Internal.Impl.insertMin! a b t
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_one_mul : ∀ (a : ℤ), a = 1 * a
-- Mathlib.Algebra.Polynomial.Degree.Defs
/-- `degree p` is the degree of the polynomial `p`, i.e. the largest `X`-exponent in `p`.
`degree p = some n` when `p ≠ 0` and `n` is the highest power of `X` that appears in `p`, otherwise
`degree 0 = ⊥`.  -/
Polynomial.degree : {R : Type u} → [inst : Semiring R] → Polynomial R → WithBot ℕ
-- Mathlib.Tactic.NormNum.BigOperators
/-- Either show the expression `s : Q(List α)` is Nil, or remove one element from it.

Fails if we cannot determine which of the alternatives apply to the expression.
 -/
Mathlib.Meta.List.proveNilOrCons : {u : Lean.Level} → {α : Q(Type u)} → (s : Q(List «$α»)) → Lean.MetaM (Mathlib.Meta.List.ProveNilOrConsResult s)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.reverse_blocks : ∀ {n : ℕ} (c : Composition n), c.reverse.blocks = c.blocks.reverse
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminator.mk.inj : ∀ {induction : Bool} {typeNames : Array Lean.Name} {elimName : Lean.Name} {induction_1 : Bool}
  {typeNames_1 : Array Lean.Name} {elimName_1 : Lean.Name},
  { induction := induction, typeNames := typeNames, elimName := elimName } =
      { induction := induction_1, typeNames := typeNames_1, elimName := elimName_1 } →
    induction = induction_1 ∧ typeNames = typeNames_1 ∧ elimName = elimName_1
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- A `completeEquipartiteGraph` is isomorphic to a corresponding `turanGraph`.

The difference is that the former vertices are a product type whereas the latter vertices are
not.  -/
SimpleGraph.completeEquipartiteGraph.turanGraph : {r t : ℕ} → SimpleGraph.completeEquipartiteGraph r t ≃g SimpleGraph.turanGraph (r * t) r
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal epimorphism is a morphism which is the cokernel of some morphism.  -/
CategoryTheory.NormalEpi.isColimit : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {X Y : C} →
      {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} →
        {f : X ⟶ Y} →
          [self : CategoryTheory.NormalEpi f] →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ f ⋯)
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.factor_mk : ∀ {R : Type u} [inst : Ring R] {S T : Ideal R} [inst_1 : S.IsTwoSided] [inst_2 : T.IsTwoSided] (H : S ≤ T) (x : R),
  (Ideal.Quotient.factor H) ((Ideal.Quotient.mk S) x) = (Ideal.Quotient.mk T) x
-- Mathlib.NumberTheory.Padics.PadicNumbers
instNegPadic : (p : ℕ) → [inst : Fact (Nat.Prime p)] → Neg ℚ_[p]
-- Init.Data.List.Find
List.Sublist.find?_eq_none : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α}, l₁.Sublist l₂ → List.find? p l₂ = none → List.find? p l₁ = none
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable.0.EisensteinSeries.aux_isBigO_linear : ∀ (z : UpperHalfPlane) (a b : ℤ),
  (fun m => ((↑(m 0) + ↑a) * ↑z + ↑(m 1) + ↑b)⁻¹) =O[Filter.cofinite] fun m => ‖![m 0 + a, m 1 + b]‖⁻¹
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.SeenCalls.mk.sizeOf_spec : ∀ (calls : Array Lean.Expr) (seen : Std.HashSet (Lean.Name × Array Lean.Expr)),
  sizeOf { calls := calls, seen := seen } = 1 + sizeOf calls + sizeOf seen
-- Mathlib.Topology.Order.NhdsSet
Iio_mem_nhdsSet_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c : α},
  b < c → Set.Iio c ∈ nhdsSet (Set.Icc a b)
-- Mathlib.Order.Hom.Lattice
InfHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Min β] [inst_2 : Min γ] (f : InfHom β γ)
  (g : InfHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.Data.Set.Image
Set.image_nonempty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, (f '' s).Nonempty ↔ s.Nonempty
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_union_self : ∀ {α : Type u_1} {s t : Set α}, s \ t ∪ t = s ∪ t
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueSet_eq_empty_iff : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ}, G.cliqueSet n = ∅ ↔ G.CliqueFree n
-- Mathlib.Order.PiLex
Pi.trichotomous_lex : ∀ {ι : Type u_1} {β : ι → Type u_2} (r : ι → ι → Prop) (s : {i : ι} → β i → β i → Prop) [∀ (i : ι), Std.Trichotomous s],
  WellFounded r → Std.Trichotomous (Pi.Lex r s)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.copy_Indep : ∀ {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase Indep : Set α → Prop) (hE : E = M.E)
  (hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B) (hI : ∀ (I : Set α), Indep I ↔ M.Indep I) (a : Set α),
  (M.copy E IsBase Indep hE hB hI).Indep a = Indep a
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_ker : ∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), ↑f.ker = ⇑f ⁻¹' {0}
-- Mathlib.Data.Rel
SetRel.image_mono : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, Monotone R.image
-- Mathlib.Algebra.Module.Submodule.Invariant
/-- `p` is `f` invariant if and only if `p.map f ≤ p`.  -/
Module.End.mem_invtSubmodule_iff_map_le : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p : Submodule R M}, p ∈ f.invtSubmodule ↔ Submodule.map f p ≤ p
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
Continuous.integrableOn_Icc : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [inst_5 : Preorder X] [CompactIccSpace X] [T2Space X],
  Continuous f → MeasureTheory.IntegrableOn f (Set.Icc a b) μ
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.unop_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : Cᵒᵖ), (β_ X Y).unop = β_ (Opposite.unop Y) (Opposite.unop X)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor_inv_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor α).inv.τl = (CategoryTheory.Bicategory.leftUnitor α.l).inv
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_insert_neg : ∀ {α : Type u} [inst : Ring α] (x : α) (s : Set α), Ideal.span (insert (-x) s) = Ideal.span (insert x s)
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverMincard_univ : ∀ {X : Type u_1} {F : Set X} (T : X → X), F.Nonempty → ∀ (n : ℕ), Dynamics.coverMincard T F Set.univ n = 1
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Order.InitialSeg
InitialSeg.instCoeRelEmbedding : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → Coe (InitialSeg r s) (r ↪r s)
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.range_exp : Set.range Real.exp = Set.Ioi 0
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.eq_withDensity_rnDeriv₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν s : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f ν → s.MutuallySingular ν → μ = s + ν.withDensity f → ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wrepr_equiv : ∀ {F : Type u → Type v} [q : QPF F] (x : (QPF.P F).W), QPF.Wequiv (QPF.Wrepr x) x
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- The probability of an intersection of preimages conditioning on another intersection factors
into a product.  -/
ProbabilityTheory.Kernel.iIndepFun.cond_iInter : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {X : ι → Ω → α}
  {Y : ι → Ω → β} {f : ι → Set Ω} {t : ι → Set β} {s : Finset ι} [Finite ι],
  (∀ (i : ι), Measurable (Y i)) →
    ProbabilityTheory.Kernel.iIndepFun (fun i ω => (X i ω, Y i ω)) κ μ →
      (∀ i ∈ s, MeasurableSet (f i)) →
        (∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0) →
          (∀ (i : ι), MeasurableSet (t i)) →
            ∀ᵐ (a : α) ∂μ, (κ a)[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, (κ a)[f i | Y i ⁻¹' t i]
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- Given `W : MorphismProperty C`, this is the morphism property on `Arrow C` of morphisms
whose left and right parts are in `W`.  -/
CategoryTheory.MorphismProperty.arrow : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty (CategoryTheory.Arrow C)
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.nat_mul_sub_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : NonAssocRing α],
  Function.Periodic f c → ∀ (n : ℕ), f (↑n * c - x) = f (-x)
-- Aesop.Forward.LevelIndex
Aesop.instLTLevelIndex : LT Aesop.LevelIndex
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inrRangeEquiv_symm_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : StarAddMonoid R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : Star A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  (a : ↥(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom R A))),
  (Unitization.inrRangeEquiv R A).symm a = (↑a).toProd.2
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- **Alias** of `OrthonormalBasis.orthogonalProjectionOnto_apply_eq_sum`. -/
OrthonormalBasis.orthogonalProjection_apply_eq_sum : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {U : Submodule 𝕜 E} [inst_4 : U.HasOrthogonalProjection]
  (b : OrthonormalBasis ι 𝕜 ↥U) (x : E), U.orthogonalProjectionOnto x = ∑ i, inner 𝕜 (↑(b i)) x • b i
-- Std.Time.Date.Unit.Week
Std.Time.Week.Aligned.instReprOrdinal : Repr Std.Time.Week.Aligned.Ordinal
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.produces_reverse_comm : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)},
  g.reverse.Produces u v ↔ g.Produces u.reverse v.reverse
-- Mathlib.Data.Bool.Basic
Bool.not_ne_self : ∀ (b : Bool), (!b) ≠ b
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.intro.sizeOf_spec : ∀ (x : Lean.Name) (p : Mathlib.Tactic.ITauto.Proof),
  sizeOf (Mathlib.Tactic.ITauto.Proof.intro x p) = 1 + sizeOf x + sizeOf p
-- Mathlib.RingTheory.Localization.Algebra
/-- The canonical linear map from the kernel of an algebra homomorphism to its localization.  -/
AlgHom.toKerIsLocalization : {R : Type u_5} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      {A : Type u_6} →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            {B : Type u_7} →
              [inst_3 : CommSemiring B] →
                [inst_4 : Algebra R B] →
                  (Rₚ : Type u_8) →
                    [inst_5 : CommSemiring Rₚ] →
                      [inst_6 : Algebra R Rₚ] →
                        [inst_7 : IsLocalization M Rₚ] →
                          (Aₚ : Type u_9) →
                            [inst_8 : CommSemiring Aₚ] →
                              [inst_9 : Algebra R Aₚ] →
                                [inst_10 : Algebra A Aₚ] →
                                  [inst_11 : IsScalarTower R A Aₚ] →
                                    [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] →
                                      (Bₚ : Type u_10) →
                                        [inst_13 : CommSemiring Bₚ] →
                                          [inst_14 : Algebra R Bₚ] →
                                            [inst_15 : Algebra B Bₚ] →
                                              [inst_16 : IsScalarTower R B Bₚ] →
                                                [inst_17 : IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ] →
                                                  [inst_18 : Algebra Rₚ Aₚ] →
                                                    [inst_19 : Algebra Rₚ Bₚ] →
                                                      [inst_20 : IsScalarTower R Rₚ Aₚ] →
                                                        [inst_21 : IsScalarTower R Rₚ Bₚ] →
                                                          (f : A →ₐ[R] B) →
                                                            ↥(RingHom.ker f) →ₗ[A]
                                                              ↥(RingHom.ker (IsLocalization.mapₐ M Rₚ Aₚ Bₚ f))
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- The equivalence from the sum of `GoodProducts (π C (ord I · < o))` and
`(MaxProducts C ho)` to `GoodProducts C`.  -/
Profinite.NobelingProof.GoodProducts.sum_equiv : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} →
          Profinite.NobelingProof.contained C (Order.succ o) →
            (ho : o < Ordinal.type fun x1 x2 => x1 < x2) →
              ↑(Profinite.NobelingProof.GoodProducts
                      (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)) ⊕
                  ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) ≃
                ↑(Profinite.NobelingProof.GoodProducts C)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₃ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.contractibleTriangleFunctor C).map f).hom₃ = 0
-- Init.Data.BitVec.Lemmas
BitVec.pos_iff_ne_zero : ∀ {n : ℕ} (b : BitVec n), 0#n < b ↔ b ≠ 0#n
-- Init.Data.Range.Polymorphic.UInt
UInt8.instLawfulHasSize_2 : Std.Rxi.LawfulHasSize UInt8
-- Lean.Meta.Match.MatcherApp.Transform
/-- A non-failing version of `MatcherApp.refineThrough`  -/
Lean.Meta.MatcherApp.refineThrough? : Lean.Meta.MatcherApp → Lean.Expr → Lean.MetaM (Option (Array Lean.Expr))
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.getRuleBuilderInput : Aesop.Frontend.RuleConfig → Lean.Elab.TermElabM Aesop.RuleBuilderInput
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.addConst : Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly
-- Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
CategoryTheory.Limits.instHasCokernelMap'Id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (R : C)
  {α : Type u_1} {β : Type u_2} (f : α → β) [inst_2 : CategoryTheory.Limits.HasCoproduct fun x => R]
  [inst_3 : CategoryTheory.Limits.HasCoproduct fun x => R] [CategoryTheory.Limits.HasCoproduct fun x => R],
  CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.Sigma.map' f fun x => CategoryTheory.CategoryStruct.id R)
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The lift of `g` along `f`.  -/
CategoryTheory.Bicategory.RightLift.lift : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : b ⟶ a} → {g : c ⟶ a} → CategoryTheory.Bicategory.RightLift f g → (c ⟶ b)