mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Conv
/-- * `pattern pat` traverses to the first subterm of the target that matches `pat`.
* `pattern (occs := *) pat` traverses to every subterm of the target that matches `pat`
  which is not contained in another match of `pat`. It generates one subgoal for each matching
  subterm.
* `pattern (occs := 1 2 4) pat` matches occurrences `1, 2, 4` of `pat` and produces three subgoals.
  Occurrences are numbered left to right from the outside in.

Note that skipping an occurrence of `pat` will traverse inside that subexpression, which means
it may find more matches and this can affect the numbering of subsequent pattern matches.
For example, if we are searching for `f _` in `f (f a) = f b`:
* `occs := 1 2` (and `occs := *`) returns `| f (f a)` and `| f b`
* `occs := 2` returns `| f a`
* `occs := 2 3` returns `| f a` and `| f b`
* `occs := 1 3` is an error, because after skipping `f b` there is no third match.
 -/
Lean.Parser.Tactic.Conv.pattern : Lean.ParserDescr
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.comm_from : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁.Hom C₂) (i : ι),
  CategoryTheory.CategoryStruct.comp (f.f i) (C₂.dFrom i) = CategoryTheory.CategoryStruct.comp (C₁.dFrom i) (f.next i)
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.coe_one : ∀ {A : Type u_2} [inst : Monoid A] [inst_1 : Star A], ⇑1 = id
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
_private.Mathlib.AlgebraicGeometry.Morphisms.FlatRank.0.AlgebraicGeometry.Scheme.Hom.finrank.eq_1 : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (s : ↥S),
  AlgebraicGeometry.Scheme.Hom.finrank f s =
    AlgebraicGeometry.IsAffine.finrank✝
      (CategoryTheory.Limits.pullback.snd f (S.affineOpenCover.f (S.affineOpenCover.idx s))) (Exists.choose ⋯)
-- Mathlib.Data.Fin.Init
Fin.xor_self : ∀ {k : ℕ} [inst : NeZero k] (a : Fin k), a ^^^ a = 0
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Horizontal and vertical composition of squares commutes.  -/
CategoryTheory.Bicategory.leftAdjointSquare.comp_hvcomp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e f x y z : B} {g₁ : a ⟶ d} {h₁ : b ⟶ e} {k₁ : c ⟶ f}
  {g₂ : d ⟶ x} {h₂ : e ⟶ y} {k₂ : f ⟶ z} {l₁ : a ⟶ b} {l₂ : b ⟶ c} {l₃ : d ⟶ e} {l₄ : e ⟶ f} {l₅ : x ⟶ y} {l₆ : y ⟶ z}
  (α : CategoryTheory.CategoryStruct.comp g₁ l₃ ⟶ CategoryTheory.CategoryStruct.comp l₁ h₁)
  (β : CategoryTheory.CategoryStruct.comp h₁ l₄ ⟶ CategoryTheory.CategoryStruct.comp l₂ k₁)
  (γ : CategoryTheory.CategoryStruct.comp g₂ l₅ ⟶ CategoryTheory.CategoryStruct.comp l₃ h₂)
  (δ : CategoryTheory.CategoryStruct.comp h₂ l₆ ⟶ CategoryTheory.CategoryStruct.comp l₄ k₂),
  CategoryTheory.Bicategory.leftAdjointSquare.comp α β γ δ =
    CategoryTheory.Bicategory.leftAdjointSquare.hcomp (CategoryTheory.Bicategory.leftAdjointSquare.vcomp α γ)
      (CategoryTheory.Bicategory.leftAdjointSquare.vcomp β δ)
-- Mathlib.Algebra.Lie.Basis.Base
LieAlgebra.Basis.root_mem_or_mem_neg : ∀ {ι : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Fintype ι] [inst_1 : Field K] [inst_2 : CharZero K]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  (b : LieAlgebra.Basis ι H) [inst_6 : LieModule.IsTriangularizable K (↥H) L] [inst_7 : LieAlgebra.IsKilling K L]
  (χ : ↥LieSubalgebra.root),
  (LieAlgebra.IsKilling.rootSystem H).root χ ∈
      AddSubmonoid.closure (⇑(LieAlgebra.IsKilling.rootSystem H).root '' Set.range b.baseSupp') ∨
    -(LieAlgebra.IsKilling.rootSystem H).root χ ∈
      AddSubmonoid.closure (⇑(LieAlgebra.IsKilling.rootSystem H).root '' Set.range b.baseSupp')
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivative_invOf : ∀ {R : Type u_1} [inst : CommRing R] (f : PowerSeries R) [inst_1 : Invertible f],
  (PowerSeries.derivative R) ⅟f = -⅟f ^ 2 * (PowerSeries.derivative R) f
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State.iPending : Lean.Meta.Sym.UnifyM.State✝ → Array (Lean.Expr × Lean.Expr)
-- Std.Data.DHashMap.Lemmas
/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `get_insertIfNew`.  -/
Std.DHashMap.contains_of_contains_insertIfNew' : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β k},
  (m.insertIfNew k v).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsSlice : {M : Type u_1} → [Add M] → Set M → Prop
-- Mathlib.RingTheory.Perfection
Perfection.instCommMonoid : (M : Type u_1) → [inst : CommMonoid M] → (p : ℕ) → CommMonoid (Perfection M p)
-- Mathlib.SetTheory.Cardinal.NatCard
/-- Similar to `Finite.equivFin` but with control over the term used for the cardinality.  -/
Finite.equivFinOfCardEq : {α : Type u_1} → [Finite α] → {n : ℕ} → Nat.card α = n → α ≃ Fin n
-- Mathlib.Order.WithBot
WithTop.le_coe_iff : ∀ {α : Type u_1} {a : α} [inst : LE α] {x : WithTop α}, x ≤ ↑a ↔ ∃ b, x = ↑b ∧ b ≤ a
-- Mathlib.Topology.GDelta.Basic
/-- If a set `s` is nowhere dense, so is its closure.  -/
IsNowhereDense.closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsNowhereDense s → IsNowhereDense (closure s)
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_succ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) {n : ℕ} (j : Fin (n + 1)) {Z : C}
  (h : Y.obj (Opposite.op { len := n + 1 }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.h j.succ) (CategoryTheory.CategoryStruct.comp (Y.δ j.castSucc.succ) h) =
    CategoryTheory.CategoryStruct.comp (self.h j.castSucc) (CategoryTheory.CategoryStruct.comp (Y.δ j.castSucc.succ) h)
-- Mathlib.Analysis.Real.Sqrt
/-- The square root of a real number. This returns 0 for negative inputs.

This has notation `√x`. Note that `√x⁻¹` is parsed as `√(x⁻¹)`.  -/
Real.«term√_» : Lean.ParserDescr
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.map_comp : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
  [inst_2 : UniformSpace γ] {g : β → γ} {f : α → β},
  UniformContinuous g →
    UniformContinuous f →
      UniformSpace.Completion.map g ∘ UniformSpace.Completion.map f = UniformSpace.Completion.map (g ∘ f)
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.join_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α}, MeasureTheory.Measure.join 0 = 0
-- Mathlib.Order.Hom.Order
OrderHom.instBotOfOrderBot : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → [OrderBot β] → Bot (α →o β)
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- Spawn a task that computes a piece of `Html` to be displayed when finished.  -/
Mathlib.Tactic.ClickSuggestions.spawnTask : {α : Type} →
  Mathlib.Tactic.ClickSuggestions.Premise →
    Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM α →
      Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM (Task (Except ProofWidgets.Html (Option α)))
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_nonpos_iff' : ∀ {b x : ℝ}, 1 < b → 0 ≤ x → (Real.logb b x ≤ 0 ↔ x ≤ 1)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
  {h : Std.Internal.List.containsKey a (Std.Internal.List.eraseKey k l) = true} (hl : Std.Internal.List.DistinctKeys l),
  Std.Internal.List.getValueCast a (Std.Internal.List.eraseKey k l) h = Std.Internal.List.getValueCast a l ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
continuous_cfcₙHom_of_cfcHom : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a),
  Continuous ⇑(cfcₙHom_of_cfcHom R ha)
-- Init.Data.SInt.Lemmas
Int16.ne_of_lt : ∀ {a b : Int16}, a < b → a ≠ b
-- Init.Data.List.Basic
List.tailD_nil : ∀ {α : Type u} {l' : List α}, [].tailD l' = l'
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.mk_center : ∀ {P : Type u_2} [inst : MetricSpace P] (c : P) (r : ℝ), { center := c, radius := r }.center = c
-- Mathlib.Algebra.Symmetrized
SymAlg.instOne.eq_1 : ∀ {α : Type u_1} [inst : One α], SymAlg.instOne = { one := SymAlg.sym 1 }
-- Lean.Meta.Match.SimpH
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.isDone : Lean.Meta.Match.SimpH.M✝ Bool
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k k' : α}
  {fallback : β} {f : Option β → Option β},
  Std.DTreeMap.Const.getD (Std.DTreeMap.Const.alter t k f) k' fallback =
    if cmp k k' = Ordering.eq then (f (Std.DTreeMap.Const.get? t k)).getD fallback
    else Std.DTreeMap.Const.getD t k' fallback
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.getElem?_zipWith.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          ((a : α) → (b : β) → motive (some a) (some b)) →
            ((x : Option α) →
                (x_2 : Option β) → (∀ (a : α) (b : β), x = some a → x_2 = some b → False) → motive x x_2) →
              motive x x_1
-- Lean.Meta.MkIffOfInductiveProp
/-- Proves the right to left direction of a generated iff theorem.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.toInductive : Lean.MVarId → List Lean.Name → List Lean.Expr → List Lean.Meta.Shape✝ → Lean.FVarId → Lean.MetaM Unit
-- Init.Data.Range.Basic
Membership.mem.step : ∀ {i : ℕ} {r : Std.Legacy.Range}, i ∈ r → (i - r.start) % r.step = 0
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ioi₀ : ∀ {G₀ : Type u_2} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {c : G₀} (a : G₀),
  0 < c → (fun x => c * x) ⁻¹' Set.Ioi a = Set.Ioi (a / c)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_smul_of_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {r : ℝ},
  0 ≤ r → ∀ (s : Set E), μ (r • s) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ s
-- Lean.Parser.Do
Lean.Parser.Term.doIdbg.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_tmod_unique' : ∀ {a b r q : ℤ}, a ≤ 0 → b ≠ 0 → (a.tdiv b = q ∧ a.tmod b = r ↔ r + b * q = a ∧ -↑b.natAbs < r ∧ r ≤ 0)
-- Mathlib.Probability.IdentDistrib
/-- **Alias** of `ProbabilityTheory.IdentDistrib.measure_mem_eq`. -/
ProbabilityTheory.IdentDistrib.measure_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ},
  ProbabilityTheory.IdentDistrib f g μ ν → ∀ {s : Set γ}, MeasurableSet s → μ (f ⁻¹' s) = ν (g ⁻¹' s)
-- Mathlib.Data.NNReal.Defs
NNReal.iSup_eq_zero : ∀ {ι : Sort u_1} {f : ι → NNReal}, BddAbove (Set.range f) → (⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0)
-- Mathlib.Data.DFinsupp.Multiset
DFinsupp.toMultiset_toDFinsupp : ∀ {α : Type u_1} [inst : DecidableEq α] (f : Π₀ (x : α), ℕ), Multiset.toDFinsupp (DFinsupp.toMultiset f) = f
-- Aesop.Tree.Data
Aesop.GoalUnsafe.brecOn_2.eq : ∀ {motive_1 : Aesop.GoalUnsafe → Sort u} {motive_2 : Aesop.MVarClusterUnsafe → Sort u}
  {motive_3 : Aesop.RappUnsafe → Sort u} {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u}
  {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u}
  {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u}
  {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t)
  (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t) (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  Aesop.GoalUnsafe.brecOn_2 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_5 t (Aesop.GoalUnsafe.brecOn_2.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.liftOn.congr_simp : ∀ {K : Type u} [inst : CommRing K] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] {L : Type u_1}
  (x x_1 : PerfectClosure K p),
  x = x_1 →
    ∀ (f f_1 : ℕ × K → L) (e_f : f = f_1) (hf : ∀ (x y : ℕ × K), PerfectClosure.R K p x y → f x = f y),
      x.liftOn f hf = x_1.liftOn f_1 ⋯
-- Lean.Meta.Tactic.Injection
Lean.Meta.getCtorNumPropFields : Lean.ConstructorVal → Lean.MetaM ℕ
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.get?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.get? k = t₂.get? k
-- Mathlib.RingTheory.RingHom.LocallyStandardSmooth
/-- Any standard smooth ring homomorphism is smooth.  -/
RingHom.IsStandardSmooth.smooth : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, f.IsStandardSmooth → f.Smooth
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.toNonUnitalSubsemiring_strictMono : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], StrictMono NonUnitalSubring.toNonUnitalSubsemiring
-- Lean.Language.Basic
Lean.Language.SnapshotTreeTransform.mk : Substring.Raw → Lean.Language.SnapshotTreeTransform
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.coe_rangeRestrict : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S) (x : R),
  ↑(f.rangeRestrict x) = f x
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.constMonoidHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MulOneClass Y] (y : Y),
  LocallyConstant.constMonoidHom y = LocallyConstant.const X y
-- Lean.Meta.Basic
Lean.Meta.withIncSynthPending : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.CategoryTheory.Enriched.Basic
/-- The type of `A`-graded natural transformations between `V`-functors `F` and `G`.
This is the type of morphisms in `V` from `A` to the `V`-object of natural transformations.
 -/
CategoryTheory.GradedNatTrans : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              CategoryTheory.Center V →
                CategoryTheory.EnrichedFunctor V C D → CategoryTheory.EnrichedFunctor V C D → Type (max u₁ w)
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [MeasureTheory.SigmaFinite μ] {f g : α → E},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ) →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn g s μ) →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ) → f =ᵐ[μ] g
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.lift_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  {X Y : CategoryTheory.Mat_ C} (f : X ⟶ Y),
  (CategoryTheory.Mat_.lift F).map f = CategoryTheory.Limits.biproduct.matrix fun i j => F.map (f i j)
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E}, Meromorphic f → Meromorphic g → Meromorphic (f - g)
-- Batteries.Data.Random.MersenneTwister
Batteries.Random.MersenneTwister.State.mk.inj : ∀ {cfg : Batteries.Random.MersenneTwister.Config} {data : Vector (BitVec cfg.wordSize) cfg.stateSize}
  {index : Fin cfg.stateSize} {data_1 : Vector (BitVec cfg.wordSize) cfg.stateSize} {index_1 : Fin cfg.stateSize},
  { data := data, index := index } = { data := data_1, index := index_1 } → data = data_1 ∧ index = index_1
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasurableEmbedding.map_withDensity_rnDeriv : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν],
      MeasureTheory.Measure.map f (ν.withDensity (μ.rnDeriv ν)) =
        (MeasureTheory.Measure.map f ν).withDensity
          ((MeasureTheory.Measure.map f μ).rnDeriv (MeasureTheory.Measure.map f ν))
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Swaps two rows.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.swapRows : {α : ℕ → ℕ → Type} →
  [self : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm α] → {n m : ℕ} → α n m → ℕ → ℕ → α n m
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_getElem_utf8EncodeChar_one_of_utf8Size_eq_two : ∀ {c : Char} (hc : c.utf8Size = 2),
  ByteArray.utf8DecodeChar?.isInvalidContinuationByte (String.utf8EncodeChar c)[1] = false
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- Conjugation by `GL(2, ℚ)` preserves arithmetic subgroups.  -/
Subgroup.IsArithmetic.conj : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] (g : GL (Fin 2) ℚ),
  (ConjAct.toConjAct ((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ)) g) • 𝒢).IsArithmetic
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comapSubtypeEquivOfLe_symm_apply : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p q : Submodule R M} (hpq : p ≤ q) (x : ↥p), (Submodule.comapSubtypeEquivOfLe hpq).symm x = ⟨⟨↑x, ⋯⟩, ⋯⟩
-- Init.Prelude
/-- Gets the `i`'th argument of the syntax node. This can also be written `stx[i]`.
Returns `missing` if `i` is out of range.
 -/
Lean.Syntax.getArg : Lean.Syntax → ℕ → Lean.Syntax
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The forgetful map from `Subalgebra` to `Submodule` as an `OrderEmbedding`  -/
Subalgebra.toSubmodule : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Subalgebra R A ↪o Submodule R A
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `UInt64.ofNat 5 = 5`
* `UInt64.ofNat 65539 = 65539`
* `UInt64.ofNat 4_294_967_299 = 4_294_967_299`
* `UInt64.ofNat 18_446_744_073_709_551_620 = 4`
 -/
UInt64.ofNat : ℕ → UInt64
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.first_cont_eq : ∀ {K : Type u_1} {g : GenContFract K} [inst : DivisionRing K] {gp : GenContFract.Pair K},
  g.s.get? 0 = some gp → g.conts 1 = { a := gp.b * g.h + gp.a, b := gp.b }
-- Mathlib.LinearAlgebra.Complex.Module
realPart_one : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : Module ℂ A] [inst_3 : StarModule ℂ A], realPart 1 = 1
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimFlipObjMap_comp_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W W' W'' : CategoryTheory.Functor J (Type w)} (g : W ⟶ W') (g' : W' ⟶ W'') (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] [inst_3 : CategoryTheory.Limits.HasWeightedLimit W' F]
  [inst_4 : CategoryTheory.Limits.HasWeightedLimit W'' F] {Z : C} (h : W.weightedLimObjObj F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.weightedLimFlipObjMap g' F)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.weightedLimFlipObjMap g F) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.weightedLimFlipObjMap (CategoryTheory.CategoryStruct.comp g g') F) h
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsRightUniformGroup.toIsTopologicalGroup : ∀ {G : Type u_7} {inst : UniformSpace G} {inst_1 : Group G} [self : IsRightUniformGroup G], IsTopologicalGroup G
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertManyIfNewUnit_empty_list : ∀ {α : Type u} {instOrd : Ord α} {l : List α} {k : α},
  Std.DTreeMap.Internal.Impl.Const.get!
      (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)) k =
    ()
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.foldlM.eq_2 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : δ → (a : α) → β a → m δ)
  (x : δ) (a : α) (b : β a) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.foldlM f x (Std.DHashMap.Internal.AssocList.cons a b es) = do
    let d ← f x a b
    Std.DHashMap.Internal.AssocList.foldlM f d es
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zsmul.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Zero α] [inst_2 : Add α] [inst_3 : Neg α],
  Finset.zsmul = { smul := fun n s => zsmulRec nsmulRec n s }
-- Mathlib.MeasureTheory.Measure.Map
MeasurableEquiv.map_measurableEquiv_injective : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSpace β] (e : α ≃ᵐ β),
  Function.Injective (MeasureTheory.Measure.map ⇑e)
-- Mathlib.Data.Finsupp.Option
Finsupp.some_zero : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M], Finsupp.some 0 = 0
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.ext : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i}
  {f g : X ⟶ Y}, (∀ (i : I), f i = g i) → f = g