mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Exponent
/-- If there exists an addition-preserving equivalence between `G` and `H`,
then the exponent of `G` is equal to the exponent of `H`.  -/
AddMonoid.exponent_eq_of_addEquiv : ∀ {G : Type u} [inst : AddMonoid G] {H : Type u_1} [inst_1 : AddMonoid H] (e : G ≃+ H),
  AddMonoid.exponent G = AddMonoid.exponent H
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrLeft_trans : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_8} [inst : MulOneClass M₁] [inst_1 : MulOneClass M₂]
  [inst_2 : MulOneClass M₃] [inst_3 : CommMonoid N] (e₁₂ : M₁ ≃* M₂) (e₂₃ : M₂ ≃* M₃),
  (e₁₂.trans e₂₃).monoidHomCongrLeft = e₁₂.monoidHomCongrLeft.trans e₂₃.monoidHomCongrLeft
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.coe_decompose_mul_of_left_mem : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] {a b : A} {i : ι} [inst_8 : Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (n : ι)
  [inst_11 : Decidable (i ≤ n)],
  a ∈ 𝒜 i → ↑(((DirectSum.decompose 𝒜) (a * b)) n) = if i ≤ n then a * ↑(((DirectSum.decompose 𝒜) b) (n - i)) else 0
-- Mathlib.Order.Extension.Linear
instLinearOrderLinearExtensionOfPartialOrder : {α : Type u} → [PartialOrder α] → LinearOrder (LinearExtension α)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Colimits of `F` are unique up to isomorphism.  -/
CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {s t : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit s → CategoryTheory.Limits.IsColimit t → (s.pt ≅ t.pt)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C} {I₀ : Type w} {X : I₀ → C} {f : (i : I₀) → X i ⟶ S}
  {I₀_1 : Type w} {X_1 : I₀_1 → C} {f_1 : (i : I₀_1) → X_1 i ⟶ S},
  { I₀ := I₀, X := X, f := f } = { I₀ := I₀_1, X := X_1, f := f_1 } → I₀ = I₀_1 ∧ X ≍ X_1 ∧ f ≍ f_1
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.const_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β},
  ProbabilityTheory.Kernel.const α 0 = 0
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_revPerm_Iic : ∀ {n : ℕ} (i : Fin n), Finset.map (Equiv.toEmbedding Fin.revPerm) (Finset.Iic i) = Finset.Ici i.rev
-- Lean.DocString.Extension
/-- A custom inline element `val`. The type `α` determines how it is interpreted. In contexts where `α`
is not understood, `content` is used as a fallback.
 -/
Lean.Doc.Inline.custom : {α : Type u_1} → [TypeName α] → α → Array (Lean.Doc.Inline Lean.ElabInline) → Lean.Doc.Inline Lean.ElabInline
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
FDerivMeasurableAux.differentiable_set_eq_D : ∀ {𝕜 : 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] {f : E → F}
  (K : Set (E →L[𝕜] F)), IsComplete K → {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} = FDerivMeasurableAux.D f K
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.J_smul : ∀ (τ : UpperHalfPlane), UpperHalfPlane.J • τ = ↑UpperHalfPlane.ofComplex (-(starRingEnd ℂ) ↑τ)
-- Mathlib.MeasureTheory.Group.Arithmetic
DiscreteMeasurableSpace.toMeasurableAdd₂ : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Add α] [DiscreteMeasurableSpace (α × α)], MeasurableAdd₂ α
-- Init.Data.Array.Perm
Array.Perm.append : ∀ {α : Type u_1} {xs ys as bs : Array α}, xs.Perm ys → as.Perm bs → (xs ++ as).Perm (ys ++ bs)
-- Mathlib.Analysis.Analytic.Order
/-- The order of vanishing of `f` at `z₀`, as an element of `ℕ`.

The order is defined to be `0` if `f` is identically zero on a neighbourhood of `z₀`,
and is otherwise the unique `n` such that `f` can locally be written as `f z = (z - z₀) ^ n • g z`,
where `g` is analytic and does not vanish at `z₀`. See `AnalyticAt.analyticOrderAt_eq_top` and
`AnalyticAt.analyticOrderAt_eq_natCast` for these equivalences.

If `f` isn't analytic at `z₀`, then `analyticOrderNatAt f z₀` returns a junk value of `0`.  -/
analyticOrderNatAt : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → 𝕜 → ℕ
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The characterization of weak convergence of finite measures by the condition that the
integrals of every continuous bounded nonnegative function are continuous.  -/
MeasureTheory.FiniteMeasure.continuous_iff_forall_continuousMap_continuous_lintegral : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {X : Type u_2} [inst_3 : TopologicalSpace X] {μs : X → MeasureTheory.FiniteMeasure Ω} [CompactSpace Ω],
  Continuous μs ↔ ∀ (f : C(Ω, NNReal)), Continuous fun x => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs x)
-- Init.Data.List.Lemmas
List.mem_map : ∀ {α : Type u_1} {β : Type u_2} {b : β} {f : α → β} {l : List α}, b ∈ List.map f l ↔ ∃ a ∈ l, f a = b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_eq_some_getKey : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a : α} {h' : m.contains a = true}, m.getKey? a = some (m.getKey a h')
-- Mathlib.Data.Sym.Sym2
/-- `Sym2.map` as an embedding.  -/
Function.Embedding.sym2Map : {α : Type u_1} → {β : Type u_2} → (α ↪ β) → Sym2 α ↪ Sym2 β
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dCokernelSequence_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dCokernelSequence_exact._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dCokernelSequence_exact._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dCokernelSequence_exact._auto_5),
  (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).Exact
-- Mathlib.GroupTheory.IsSubnormal
AddSubgroup.IsSubnormal.below : {G : Type u_2} →
  [inst : AddGroup G] →
    {motive : (a : AddSubgroup G) → a.IsSubnormal → Prop} → {a : AddSubgroup G} → a.IsSubnormal → Prop
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.neg_toEquiv : ∀ (G : Type u_4) [inst : MeasurableSpace G] [inst_1 : InvolutiveNeg G] [inst_2 : MeasurableNeg G],
  (MeasurableEquiv.neg G).toEquiv = Equiv.neg G
-- Mathlib.Topology.Compactness.Compact
prod_nhdsSet_le_of_disjoint_cocompact : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {t : Set Y} {f : Filter X},
  IsCompact t → Disjoint f (Filter.cocompact X) → f ×ˢ nhdsSet t ≤ nhdsSet (Set.univ ×ˢ t)
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.essentiallySmall_iff_objectPropertyEssentiallySmall : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  CategoryTheory.EssentiallySmall.{w, v_1, u_1} C ↔
    CategoryTheory.LocallySmall.{w, v_1, u_1} C ∧ CategoryTheory.ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤
-- Init.Grind.Order
Lean.Grind.Order.le_unsat_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a : α} {k : ℤ}, k.blt' 0 = true → a ≤ a + ↑k → False
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Accumulate names (`Syntax.ident`s with position information) of the current, unfinished
binder group `(d e ...)` as determined by `shouldGroupWithNext`. We cannot do grouping
inside-out, on the Syntax level, because it depends on comparing the Expr binder types.

The `allNames` set is used to make sure names in the same `fun` binders are unique.
Users have reported than `fun x x x => x` is confusing.
 -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabBinders : Lean.NameSet →
  Array Lean.Syntax →
    Bool →
      Bool →
        (Lean.NameSet → Lean.PrettyPrinter.Delaborator.Delab) →
          (Lean.NameSet → Array Lean.Syntax → Bool → Bool → Lean.Syntax → Lean.PrettyPrinter.Delaborator.Delab) →
            Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.ext : ∀ {X Y : MagmaCat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.ModelTheory.Substructures
/-- The embedding associated to an inclusion of substructures.  -/
FirstOrder.Language.Substructure.inclusion : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → {S T : L.Substructure M} → S ≤ T → L.Embedding ↥S ↥T
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.himp_meet_himp_le : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel (Lean.Order.meet (Lean.Order.himp P Q) (Lean.Order.himp Q R)) (Lean.Order.himp P R)
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_densityProcess_atTop_empty_of_antitone : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsFiniteKernel κ] (n : ℕ) (a : α) (x : γ) (seq : ℕ → Set β),
  Antitone seq →
    ⋂ i, seq i = ∅ →
      (∀ (m : ℕ), MeasurableSet (seq m)) →
        Filter.Tendsto (fun m => κ.densityProcess ν n a x (seq m)) Filter.atTop (nhds (κ.densityProcess ν n a x ∅))
-- Mathlib.Topology.Algebra.Module.Star
starL'_symm_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousStar A] [inst_8 : TrivialStar R] (x : A), (starL' R).symm x = starAddEquiv.symm x
-- Mathlib.Analysis.Calculus.ContDiff.Comp
iteratedFDerivWithin_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {g : F → G} {x : E}
  {n : WithTop ℕ∞} {t : Set F},
  ContDiffWithinAt 𝕜 n g t (f x) →
    ContDiffWithinAt 𝕜 n f s x →
      UniqueDiffOn 𝕜 t →
        UniqueDiffOn 𝕜 s →
          x ∈ s →
            Set.MapsTo f s t →
              ∀ {i : ℕ},
                ↑i ≤ n →
                  iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
                    (ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f s x) i
-- Init.Data.Ord.Array
Array.compareLex_eq_compareLex_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {a₁ a₂ : Array α},
  Array.compareLex cmp a₁ a₂ = List.compareLex cmp a₁.toList a₂.toList
-- Mathlib.CategoryTheory.Localization.Linear
CategoryTheory.Localization.instLinearLocalization'Q' : ∀ (R : Type w) [inst : Ring R] {C : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} C]
  [inst_2 : CategoryTheory.Preadditive C] (W : CategoryTheory.MorphismProperty C) [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : W.HasLocalization] [inst_5 : CategoryTheory.Preadditive W.Localization'] [inst_6 : W.Q'.Additive],
  CategoryTheory.Functor.Linear R W.Q'
-- Mathlib.Algebra.Order.Floor.Defs
Int.fract.eq_1 : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] (a : α), Int.fract a = a - ↑⌊a⌋
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∪ t₂).contains k = (t₁.contains k || t₂.contains k)
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.functorEquivalence_counitIso : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C],
  (CategoryTheory.ShortComplex.functorEquivalence J C).counitIso =
    CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
NumberField.Units.dvd_torsionOrder_of_isPrimitiveRoot : ∀ {n : ℕ} {K : Type u} [inst : Field K] [NeZero n] {ζ : K}, IsPrimitiveRoot ζ n → n ∣ NumberField.Units.torsionOrder K
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.isEmpty_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β},
  Std.DHashMap.Internal.Raw.WFImp m → m.isEmpty = (Std.DHashMap.Internal.toListModel m.buckets).isEmpty
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ofCoeff_eq_zero : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : ℕ →₀ M},
  { coeff := x } = 0 ↔ x = 0
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_map_eq_charFunDual_smul : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure E} [OpensMeasurableSpace E] (L : StrongDual ℝ E) (u : ℝ),
  MeasureTheory.charFun (MeasureTheory.Measure.map (⇑L) μ) u = MeasureTheory.charFunDual μ (u • L)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.map_prod_of_prime : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {f : ArithmeticFunction R},
  f.IsMultiplicative → ∀ (t : Finset ℕ), (∀ p ∈ t, Nat.Prime p) → f (∏ a ∈ t, a) = ∏ a ∈ t, f a
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.addBottom_nth_snd : ∀ {K : Type u_1} {Γ : K → Type u_2} (L : Turing.ListBlank ((k : K) → Option (Γ k))) (n : ℕ),
  ((Turing.TM2to1.addBottom L).nth n).2 = L.nth n
-- Mathlib.RingTheory.Idempotents
/-- The corner associated to an element `e` in a semiring without 1
is the subsemiring without 1 of all elements of the form `e * r * e`.  -/
NonUnitalSubsemiring.corner : {R : Type u_1} → R → [inst : NonUnitalSemiring R] → NonUnitalSubsemiring R
-- Mathlib.MeasureTheory.Measure.AddContent
/-- For an `m : addContent C` on a `SetSemiring C`, if `I` is a `Finset` of pairwise disjoint
sets in `C` and `⋃₀ I ⊆ t` for `t ∈ C`, then `∑ s ∈ I, m s ≤ m t`.  -/
MeasureTheory.sum_addContent_le_of_subset : ∀ {α : Type u_1} {C : Set (Set α)} {t : Set α} {I : Finset (Set α)} {G : Type u_2} [inst : AddCommMonoid G]
  {m : MeasureTheory.AddContent G C} [inst_1 : PartialOrder G] [CanonicallyOrderedAdd G],
  MeasureTheory.IsSetSemiring C → ↑I ⊆ C → (↑I).PairwiseDisjoint id → t ∈ C → (∀ s ∈ I, s ⊆ t) → ∑ u ∈ I, m u ≤ m t
-- Mathlib.Analysis.Seminorm
Seminorm.ball_finset_sup : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ},
  0 < r → (s.sup p).ball x r = s.inf fun i => (p i).ball x r
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {fallback : β k},
  Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.union m₂ ⋯ ⋯).getD k fallback = m₁.getD k fallback
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Rep.applyAsHom.eq_1 : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : CommMonoid G] (A : Rep.{u_1, u, v} k G) (g : G),
  A.applyAsHom g = Rep.ofHom { toLinearMap := A.ρ g, isIntertwining' := ⋯ }
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_mem : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M}
  (x : ↥p), ↑x ∈ p
-- Lean.Meta.Tactic.Grind.ForallProp
/-- Propagator for dependent forall terms
`forall (h : p), q[h]` where p is a proposition.
 -/
Lean.Meta.Grind.propagateForallPropUp : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instTop.eq_1 : ∀ {α : Type u_1} [inst : LE α], UpperSet.instTop = { top := { carrier := ∅, upper' := ⋯ } }
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.linearIndependent_one_tmul : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Semiring S] [inst_4 : Algebra R S] [Module.Flat R S] {ι : Type u_5} {v : ι → M},
  LinearIndependent R v → LinearIndependent S fun x => 1 ⊗ₜ[R] v x
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `Finset.analyticWithinAt_sum`

---

Finite sums of analytic functions are analytic  -/
Finset.analyticWithinAt_fun_sum : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {f : α → E → F} {c : E} {s : Set E} (N : Finset α),
  (∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) → AnalyticWithinAt 𝕜 (fun a => ∑ c ∈ N, f c a) s c
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.toList_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  {f : α → β → Option γ},
  t.WF →
    Std.DTreeMap.Raw.Const.toList (Std.DTreeMap.Raw.filterMap f t) =
      List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) (Std.DTreeMap.Raw.Const.toList t)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Sync.forIn : {m : Type → Type u_1} →
  {α β : Type} → [Monad m] → [MonadLiftT BaseIO m] → Std.CloseableChannel.Sync α → (α → β → m (ForInStep β)) → β → m β
-- Init.Data.List.Erase
List.length_erase_le : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : List α}, (l.erase a).length ≤ l.length
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
/-- The explicit coproduct for `F : discrete ι ⥤ LocallyRingedSpace`.  -/
AlgebraicGeometry.LocallyRingedSpace.coproduct : {ι : Type v} →
  [Small.{u, v} ι] →
    CategoryTheory.Functor (CategoryTheory.Discrete ι) AlgebraicGeometry.LocallyRingedSpace →
      AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.Analysis.Convex.Basic
convex_Ico : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_5 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β),
  Convex 𝕜 (Set.Ico r s)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_source_inter : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X), e.restr (e.source ∩ s) = e.restr s
-- Lean.Elab.Tactic.Grind.Main
_private.Lean.Elab.Tactic.Grind.Main.0.Lean.Elab.Tactic.elabGrindPattern.elabDefEq : Array Lean.Expr → Lean.Syntax → Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.Analysis.Normed.Field.WithAbs
WithAbs.toAbs_div : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Field R] (v : AbsoluteValue R S)
  (x y : R), WithAbs.toAbs v (x / y) = WithAbs.toAbs v x / WithAbs.toAbs v y
-- Mathlib.Algebra.Field.Opposite
AddOpposite.instNNRatCast.eq_1 : ∀ {α : Type u_1} [inst : NNRatCast α], AddOpposite.instNNRatCast = { nnratCast := fun q => AddOpposite.op ↑q }
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.killCompl_map : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  {e : σ ↪ τ} (φ : R →+* S) (p : MvPowerSeries τ R),
  (MvPowerSeries.killCompl e) ((MvPowerSeries.map φ) p) = (MvPowerSeries.map φ) ((MvPowerSeries.killCompl e) p)
-- Mathlib.CategoryTheory.Bicategory.Free
/-- Bicategory structure on the free bicategory.  -/
CategoryTheory.FreeBicategory.bicategory : {B : Type u} → [Quiver B] → CategoryTheory.Bicategory (CategoryTheory.FreeBicategory B)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α} {b : β}, (t.insert a b).getKeyD a fallback = a
-- Init.Data.UInt.Lemmas
UInt16.toFin_add : ∀ (a b : UInt16), (a + b).toFin = a.toFin + b.toFin
-- Mathlib.Algebra.Category.CommBialgCat
commBialgCatEquivComonCommAlgCat_functor_obj_unop_X : ∀ (R : Type u) [inst : CommRing R] (A : CommBialgCat R),
  (Opposite.unop ((commBialgCatEquivComonCommAlgCat R).functor.obj A)).X = Opposite.op (CommAlgCat.of R ↑A)
-- Mathlib.Order.Filter.Extr
IsMinFilter.sub : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f g : α → β}
  {a : α} {l : Filter α}, IsMinFilter f l a → IsMaxFilter g l a → IsMinFilter (fun x => f x - g x) l a
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.diagonalInvertibleEquivInvertible_symm_apply : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (v : n → α)
  [inst_3 : Invertible v], (Matrix.diagonalInvertibleEquivInvertible v).symm inst_3 = Matrix.diagonalInvertible v
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normIntOfNatInst : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.Fintype.Basic
Fin.univ_val_map : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → α), Multiset.map f Finset.univ.val = ↑(List.ofFn f)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Make an object of `P.Over Q X` from a morphism `f : A ⟶ X` and a proof of `P f`.  -/
CategoryTheory.MorphismProperty.Over.mk : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P : CategoryTheory.MorphismProperty T} →
      (Q : CategoryTheory.MorphismProperty T) → {X A : T} → (f : A ⟶ X) → P f → P.Over Q X
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.le_sum : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (μ : ι → MeasureTheory.Measure α) (i : ι),
  μ i ≤ MeasureTheory.Measure.sum μ
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- We have the congruence `legendreSym p a ≡ a ^ (p / 2) mod p`.  -/
legendreSym.eq_pow : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (a : ℤ), ↑(legendreSym p a) = ↑a ^ (p / 2)
-- Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1 : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} {W : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  [inst_6 : NormedAddCommGroup W] [inst_7 : NormedSpace ℝ W] [inst_8 : MeasurableSpace E] {μ : MeasureTheory.Measure E}
  [MeasureTheory.SigmaFinite μ] {f f' : E × ℝ → F} {g g' : E × ℝ → G} {B : F →L[ℝ] G →L[ℝ] W},
  MeasureTheory.Integrable (fun x => (B (f' x)) (g x)) (μ.prod MeasureTheory.volume) →
    MeasureTheory.Integrable (fun x => (B (f x)) (g' x)) (μ.prod MeasureTheory.volume) →
      MeasureTheory.Integrable (fun x => (B (f x)) (g x)) (μ.prod MeasureTheory.volume) →
        (∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)) →
          (∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)) →
            ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ.prod MeasureTheory.volume =
              -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ.prod MeasureTheory.volume
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.symm_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y), α.symm.inv = α.hom