mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.mem_realUnits_iff : ∀ (K : Type u_1) [inst : Field K] (u : (NumberField.RingOfIntegers K)ˣ),
  u ∈ NumberField.IsCMField.realUnits K ↔
    ∃ v,
      (algebraMap (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)) (NumberField.RingOfIntegers K)) ↑v =
        ↑u
-- Mathlib.Order.Interval.Basic
NonemptyInterval.coe_subset_coe : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : NonemptyInterval α}, ↑s ⊆ ↑t ↔ s ≤ t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_eq_fallback : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = true → ∀ {fallback : α}, t.maxKeyD fallback = fallback
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst : Inhabited β], k ∉ t₂ → (t₁ ∪ t₂)[k]! = t₁[k]!
-- Lean.Server.GoTo
Lean.Server.instToJsonGoToKind : Lean.ToJson Lean.Server.GoToKind
-- Init.Data.Array.MapIdx
Array.mapFinIdx_push : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {a : α} {f : (i : ℕ) → α → i < (xs.push a).size → β},
  (xs.push a).mapFinIdx f = (xs.mapFinIdx fun i a_1 h => f i a_1 ⋯).push (f xs.size a ⋯)
-- Init.Data.Vector.Lemmas
_private.Init.Data.Vector.Lemmas.0.Vector.mapM.go.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] (f : α → m β) (xs : Vector α n)
  (k : ℕ) (h : k ≤ n) (acc : Vector β k),
  Vector.mapM.go✝ f xs k h acc =
    if h' : k < n then do
      let __do_lift ← f xs[k]
      Vector.mapM.go✝ f xs (k + 1) ⋯ (acc.push __do_lift)
    else pure (Vector.cast ⋯ acc)
-- Init.Data.Array.Subarray
/-- Extracts an element from the subarray, or returns a default value when the index is out of bounds.

The index is relative to the start and end of the subarray, rather than the underlying array. The
default value is that provided by the `Inhabited α` instance.
 -/
Subarray.get! : {α : Type u_1} → [Inhabited α] → Subarray α → ℕ → α
-- Init.Data.Ord.Basic
/-- The result of a comparison according to a total order.

The relationship between the compared items may be:
* `Ordering.lt`: less than
* `Ordering.eq`: equal
* `Ordering.gt`: greater than
 -/
Ordering : Type
-- Std.Do.Triple.SpecLemmas
/-- A pointer at a specific location in a list. List cursors are used in loop invariants for the
`mvcgen` tactic.

Moving the cursor to the left or right takes time linear in the current position of the cursor, so
this data structure is not appropriate for run-time code.
 -/
List.Cursor : {α : Type u} → List α → Type u
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.drop.aux_none : ∀ {α : Type u} (n : ℕ), Stream'.WSeq.drop.aux n none = Computation.pure none
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.Seq.BisimO.match_1.splitter : {α : Type u_1} →
  (motive : Option (Stream'.Seq1 α) → Option (Stream'.Seq1 α) → Sort u_2) →
    (x x_1 : Option (Stream'.Seq1 α)) →
      (Unit → motive none none) →
        ((a : α) → (s : Stream'.Seq α) → (a' : α) → (s' : Stream'.Seq α) → motive (some (a, s)) (some (a', s'))) →
          ((x x_2 : Option (Stream'.Seq1 α)) →
              (x = none → x_2 = none → False) →
                (∀ (a : α) (s : Stream'.Seq α) (a' : α) (s' : Stream'.Seq α),
                    x = some (a, s) → x_2 = some (a', s') → False) →
                  motive x x_2) →
            motive x x_1
-- Mathlib.Order.Irreducible
supIrred_ofDual : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : αᵒᵈ}, SupIrred (OrderDual.ofDual a) ↔ InfIrred a
-- Mathlib.Topology.PreorderRestrict
Preorder.continuous_restrictLe : ∀ {α : Type u_1} [inst : Preorder α] {X : α → Type u_2} [inst_1 : (i : α) → TopologicalSpace (X i)] (a : α),
  Continuous (Preorder.restrictLe a)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.ofHom_hom : ∀ {X Y : AddCommGrpCat} (f : X ⟶ Y), AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f) = f
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.functorFrom_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {E : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E)
  (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c'))
  (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯)
  (hom_comp :
    ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
      hom (CategoryTheory.CategoryStruct.comp f g) =
        CategoryTheory.CategoryStruct.comp (hom f)
          (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g)) (CategoryTheory.eqToHom ⋯)))
  (X : CategoryTheory.Grothendieck F),
  (CategoryTheory.Grothendieck.functorFrom fib hom hom_id hom_comp).obj X = (fib X.base).obj X.fiber
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CongrTheoremCacheKey.mk.inj : ∀ {f : Lean.Expr} {numArgs : ℕ} {f_1 : Lean.Expr} {numArgs_1 : ℕ},
  { f := f, numArgs := numArgs } = { f := f_1, numArgs := numArgs_1 } → f = f_1 ∧ numArgs = numArgs_1
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- Consider an object of `C` as an object of the `R`-linear completion.

It may be preferable to use `(Free.embedding R C).obj X` instead;
this functor can also be used to lift morphisms.
 -/
CategoryTheory.Free.of : (R : Type u_1) → {C : Type u} → C → CategoryTheory.Free R C
-- Mathlib.Tactic.Widget.StringDiagram
/-- Nodes for identity 2-morphisms in a string diagram.  -/
Mathlib.Tactic.Widget.StringDiagram.IdNode : Type
-- Mathlib.Topology.Constructible
/-- [Stacks Tag 005J](https://stacks.math.columbia.edu/tag/005J) -/
Topology.IsConstructible.preimage_of_isOpenEmbedding : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  Topology.IsOpenEmbedding f → Topology.IsConstructible s → Topology.IsConstructible (f ⁻¹' s)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.toLp_prodMk : ∀ {Ω : Type u_1} {E : Type u_2} {F : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E]
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] [inst_6 : MeasurableSpace F] [BorelSpace F] {Y : Ω → F}
  [SecondCountableTopologyEither E F] (p : ENNReal) [Fact (1 ≤ p)],
  ProbabilityTheory.HasGaussianLaw (fun ω => (X ω, Y ω)) P →
    ProbabilityTheory.HasGaussianLaw (fun ω => WithLp.toLp p (X ω, Y ω)) P
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_insertIfNew_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {kmi : α}, (t.insertIfNew k v).minKey?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Mathlib.Analysis.Convex.Independent
/-- **Alias** of `convexIndependent_iff_notMem_convexHull_sdiff`.

---

If a family is convex independent, a point in the family is not in the convex hull of the other
points. See `convexIndependent_set_iff_notMem_convexHull_sdiff` for the `Set` version.  -/
convexIndependent_iff_notMem_convexHull_diff : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {p : ι → E},
  ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
-- Qq.Typ
/-- For a safer constructor, see `Qq.assertDefEqQ`.  -/
Qq.QuotedDefEq.unsafeIntro : ∀ {u : Lean.Level} {α : Q(Sort u)} {lhs rhs : Q(«$α»)}, «$lhs» =Q «$rhs»
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_X_mul_zero : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), (Polynomial.X * p).coeff 0 = 0
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.val_finsetProd : ∀ {ι : Type u_3} {G : Type u_4} [inst : CommGroup G] (H : Subgroup G) (f : ι → ↥H) (s : Finset ι),
  ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.Data.Nat.Bits
/-- `boddDiv2 n` returns a 2-tuple of type `(Bool, Nat)` where the `Bool` value indicates whether
`n` is odd or not and the `Nat` value returns `⌊n/2⌋`  -/
Nat.boddDiv2 : ℕ → Bool × ℕ
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
CategoryTheory.Functor.closedIhom_map_app : ∀ {D : Type u} {C : Type u_1} [inst : CategoryTheory.Groupoid D] [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (F : CategoryTheory.Functor D C) {X Y : CategoryTheory.Functor D C} (g : X ⟶ Y) (X_1 : D),
  (F.closedIhom.map g).app X_1 = (CategoryTheory.ihom (F.obj X_1)).map (g.app X_1)
-- Mathlib.Order.BooleanAlgebra.Basic
disjoint_inf_sdiff : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], Disjoint (x ⊓ y) (x \ y)
-- Mathlib.Order.RelSeries
RelSeries.subsingleton_of_length_eq_zero : ∀ {α : Type u_1} {r : SetRel α α} {s : RelSeries r}, s.length = 0 → {x | x ∈ s}.Subsingleton
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Reducible functions and projection functions should always be put in `toUnfold`, instead
of trying to use equational theorems.

The simplifiers has special support for structure and class projections, and gets
confused when they suddenly rewrite, so ignore equations for them
 -/
Lean.Meta.Simp.ignoreEquations : Lean.Name → Lean.CoreM Bool
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
/-- Variant of `MDifferentiableAt.prod_map` in which the point in the product is given as `p`
instead of a pair `(x, y)`.  -/
MDifferentiableAt.prodMap' : ∀ {𝕜 : 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_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_14} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_15}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {f : M → M'} {g : N → N'} {p : M × N},
  MDiffAt f p.1 → MDiffAt g p.2 → MDiffAt (Prod.map f g) p
-- Init.Data.String.Iterator
String.Legacy.Iterator.mk : String → String.Pos.Raw → String.Legacy.Iterator
-- Mathlib.Order.Filter.Pointwise
Filter.bot_div : ∀ {α : Type u_2} [inst : Div α] {g : Filter α}, ⊥ / g = ⊥
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.IterM.step_take.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Mathlib.Geometry.Manifold.IsManifold.Basic
OpenPartialHomeomorph.isManifold_singleton : ∀ {𝕜 : 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} {n : WithTop ℕ∞}
  {M : Type u_4} [inst_4 : TopologicalSpace M] (e : OpenPartialHomeomorph M H) (h : e.source = Set.univ),
  IsManifold I n M
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_nsmul_eq_pi_iff : ∀ {θ : Real.Angle}, 2 • θ = ↑Real.pi ↔ θ = ↑(Real.pi / 2) ∨ θ = ↑(-Real.pi / 2)
-- Plausible.Gen
/-- Create a `List` of examples using `x`. The size is controlled
by the size parameter of `Gen`.  -/
Plausible.Gen.listOf : {α : Type u} → Plausible.Gen α → Plausible.Gen (List α)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instIsZeroApplyReal : ∀ {E : Type u_3} [inst : Group E], IsZeroApply (GroupSeminorm E) E ℝ
-- Mathlib.Logic.Relation
IsTrans.comap : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} [IsTrans β r] (f : α → β), IsTrans α (Function.onFun r f)
-- Mathlib.RingTheory.Algebraic.Integral
Subalgebra.algebraicClosure_eq_integralClosure : ∀ (S : Type u_2) [inst : CommRing S] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra K S],
  Subalgebra.algebraicClosure K S = integralClosure K S
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.existsNatOneDivLTMeasure_of_not_negative : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i →
    ∃ n, MeasureTheory.SignedMeasure.ExistsOneDivLT✝ s i n
-- Init.System.IO
/-- Writes the contents of the string to the handle, followed by a newline. Uses UTF-8.
 -/
IO.FS.Handle.putStrLn : IO.FS.Handle → String → IO Unit
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited γ] {f : α → β → Option γ} {k : α},
  (Std.HashMap.filterMap f m)[k]! = (m[k]?.pbind fun x_2 h' => f (m.getKey k ⋯) x_2).get!
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] {φ : S₁ ⟶ S₂}
  {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂),
  CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso γ.φH
-- Mathlib.MeasureTheory.Integral.Layercake
MeasureTheory.meas_le_ae_eq_meas_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {R : Type u_3} [inst_1 : LinearOrder R]
  [inst_2 : MeasurableSpace R] (ν : MeasureTheory.Measure R) [MeasureTheory.NullSingletonClass ν] (g : α → R),
  (fun t => μ {a | t ≤ g a}) =ᵐ[ν] fun t => μ {a | t < g a}
-- Mathlib.Tactic.DeprecateTo
/-- Produce the syntax for the command `@[deprecated (since := "YYYY-MM-DD")] alias n := id`.  -/
Mathlib.Tactic.DeprecateTo.mkDeprecationStx : Lean.TSyntax `ident → Lean.Name → optParam (Option String) none → Lean.Elab.Command.CommandElabM (Lean.TSyntax `command)
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mulEquiv_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {R' : Type u_3} [inst_2 : CommRing R'] [inst_3 : IsDomain R']
  (g : R ≃+* R') (a : ClassGroup R'),
  (ClassGroup.mulEquiv g).symm a =
    (ClassGroup.equiv (FractionRing R)).symm
      ((QuotientGroup.congr (toPrincipalIdeal R' (FractionRing R')).range (toPrincipalIdeal R (FractionRing R)).range
          (Units.mapEquiv (↑(FractionalIdeal.ringEquivOfRingEquiv (FractionRing R) (FractionRing R') g)).symm) ⋯)
        ((ClassGroup.equiv (FractionRing R')) a))
-- Mathlib.NumberTheory.Pell
/-- If `d` is a positive integer, then there is a nontrivial solution
to the Pell equation `x^2 - d*y^2 = 1` if and only if `d` is not a square.  -/
Pell.exists_iff_not_isSquare : ∀ {d : ℤ}, 0 < d → ((∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) ↔ ¬IsSquare d)
-- Mathlib.GroupTheory.Finiteness
/-- Finite product of finitely generated subgroups is finitely generated.  -/
Subgroup.FG.pi : ∀ {ι : Type u_5} [Finite ι] {G : ι → Type u_6} [inst : (i : ι) → Group (G i)] {P : (i : ι) → Subgroup (G i)},
  (∀ (i : ι), (P i).FG) → (Subgroup.pi Set.univ P).FG
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
/-- Bijection between an additive subgroup `H` and its opposite.  -/
AddSubgroup.equivOp : {G : Type u_2} → [inst : AddGroup G] → (H : AddSubgroup G) → ↥H ≃ ↥H.op
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_Hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (X Y : B × C),
  (X ⟶ Y) = ((X.1 ⟶ Y.1) × (X.2 ⟶ Y.2))
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_single_mul_subset : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : Semiring k] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) [inst_3 : DecidableEq G] (r : k) (a : G),
  (SkewMonoidAlgebra.single a r * f).support ⊆ Finset.image (fun x => a * x) f.support
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get!_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂).get! k = if k ∈ m₂ then default else m₁.get! k
-- Mathlib.Data.PNat.Xgcd
/-- Final value of `b / d`  -/
PNat.gcdB' : ℕ+ → ℕ+ → ℕ+
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_insertUnit : ∀ {n : ℕ} (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (b : Bool)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, b) l).2.1.size = assignments.size
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Harmonic functions are continuous.
 -/
InnerProductSpace.HarmonicOnNhd.continuousOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicOnNhd f s → ContinuousOn f s
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.smul_single_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (i : ℕ)
  (f : Polynomial R) (m : M) (n : ℕ),
  (f • PolynomialModule.single R i m).coeff n = if i ≤ n then f.coeff (n - i) • m else 0
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_add_left₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Add β]
  [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.Kernel.IndepFun (f i + f j) (f k) κ μ
-- Mathlib.MeasureTheory.Integral.Layercake
/-- The layer cake formula / Cavalieri's principle / tail probability formula:

Let `f` be a non-negative measurable function on a measure space. Let `G` be an
increasing absolutely continuous function on the positive real line, vanishing at the origin,
with derivative `G' = g`. Then the integral of the composition `G ∘ f` can be written as
the integral over the positive real line of the "tail measures" `μ {ω | f(ω) > t}` of `f`
weighted by `g`.

Roughly speaking, the statement is: `∫⁻ (G ∘ f) ∂μ = ∫⁻ t in 0..∞, g(t) * μ {ω | f(ω) > t}`.

See `lintegral_comp_eq_lintegral_meas_le_mul` for a version with sets of the form `{ω | f(ω) ≥ t}`
instead.  -/
MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α),
  0 ≤ᵐ[μ] f →
    AEMeasurable f μ →
      (∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t) →
        (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), 0 ≤ g t) →
          ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
            ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a} * ENNReal.ofReal (g t)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.forget_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X Y : T.Algebra} (f : X ⟶ Y),
  T.forget.map f = f.f
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_neg₁ : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b c d : ℤ), IsEllipticNet.atomRel W (-a) b c d = IsEllipticNet.atomRel W a b c d
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.range_domRestrict_eq_range_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M},
  (f.domRestrict S).range = f.range ↔ Codisjoint S f.ker
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.grindPattern.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Counting.0.SimpleGraph.card_badVertices_le : ∀ {α : Type u_1} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {ε : ℝ} {s t : Finset α},
  2 * ε ≤ ↑(G.edgeDensity s t) → G.IsUniform ε s t → ↑(SimpleGraph.badVertices✝ G ε s t).card ≤ ↑s.card * ε
-- Init.Grind.ToIntLemmas
_private.Init.Grind.ToIntLemmas.0.Lean.Grind.IntInterval.lo?.match_1.eq_1 : ∀ (motive : Lean.Grind.IntInterval → Sort u_1) (lo hi : ℤ)
  (h_1 : (lo hi : ℤ) → motive (Lean.Grind.IntInterval.co lo hi))
  (h_2 : (lo : ℤ) → motive (Lean.Grind.IntInterval.ci lo)) (h_3 : (hi : ℤ) → motive (Lean.Grind.IntInterval.io hi))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii),
  (match Lean.Grind.IntInterval.co lo hi with
    | Lean.Grind.IntInterval.co lo hi => h_1 lo hi
    | Lean.Grind.IntInterval.ci lo => h_2 lo
    | Lean.Grind.IntInterval.io hi => h_3 hi
    | Lean.Grind.IntInterval.ii => h_4 ()) =
    h_1 lo hi
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.instGeometricallyReducedSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyReduced f],
  AlgebraicGeometry.GeometricallyReduced (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.NumberTheory.ModularForms.Cusps
CongruenceSubgroup.strictWidthInfty_Gamma : ∀ (N : ℕ) [NeZero N],
  (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)).strictWidthInfty = ↑N
-- Init.Omega.IntList
Lean.Omega.IntList.dot_mod_gcd_left : ∀ (xs ys : Lean.Omega.IntList), xs.dot ys % ↑xs.gcd = 0
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Sets the user names for the given free variables in `xs`.  -/
Lean.Elab.WF.GuessLex.withUserNames : {α : Type} → Array Lean.Expr → Array Lean.Name → Lean.MetaM α → Lean.MetaM α
-- Mathlib.Algebra.Group.Subgroup.Even
Subgroup.coe_square : ∀ {G : Type u_1} [inst : CommGroup G], ↑(Subgroup.square G) = {s | IsSquare s}
-- Aesop.Rule
Aesop.UnfoldRule.mk.injEq : ∀ (decl : Lean.Name) (unfoldThm? : Option Lean.Name) (decl_1 : Lean.Name) (unfoldThm?_1 : Option Lean.Name),
  ({ decl := decl, unfoldThm? := unfoldThm? } = { decl := decl_1, unfoldThm? := unfoldThm?_1 }) =
    (decl = decl_1 ∧ unfoldThm? = unfoldThm?_1)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidSearchFrom.matched_of_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos startPos' endPos : s.Pos} {l : List (String.Slice.Pattern.SearchStep s)},
  String.Slice.Pattern.Model.IsValidSearchFrom pat endPos l →
    String.Slice.Pattern.Model.IsLongestMatchAt pat startPos' endPos →
      startPos = startPos' →
        String.Slice.Pattern.Model.IsValidSearchFrom pat startPos'
          (String.Slice.Pattern.SearchStep.matched startPos endPos :: l)
-- Mathlib.Data.EReal.Inv
EReal.mul_div_left_comm : ∀ (a b c : EReal), a * (b / c) = b * (a / c)