mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.SuccPred.Basic
Order.Iio_succ_eq_insert : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a : α),
  Set.Iio (Order.succ a) = insert a (Set.Iio a)
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.coprime_classification : ∀ {x y z : ℤ},
  PythagoreanTriple x y z ∧ x.gcd y = 1 ↔
    ∃ m n,
      (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
        (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.eq_1 : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] (f : α → β),
  HasCompactSupport f = IsCompact (tsupport f)
-- Init.Data.Int.Bitwise.Lemmas
Int.zero_shiftLeft : ∀ (n : ℕ), 0 <<< n = 0
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.partition_snd : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool},
  (Std.TreeSet.Raw.partition f t).2.WF
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, `Hⁱ(G, A)` is isomorphic
to the homology of the short complex of `k`-modules `A --(ρ(g) - 𝟙)--> A --N--> A` when `i` is
odd.  -/
Rep.FiniteCyclicGroup.groupCohomologyIsoOdd : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      [inst_2 : Fintype G] →
        (A : Rep.{u, u, u} k G) →
          (g : G) →
            (∀ (x : G), x ∈ Subgroup.zpowers g) →
              (i : ℕ) → Odd i → (groupCohomology A i ≅ (Rep.FiniteCyclicGroup.subCompNormHom A g).homology)
-- Init.Data.SInt.Bitwise
Int8.not_eq_neg_add : ∀ (a : Int8), ~~~a = -a - 1
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.instPreorder.eq_1 : ∀ {α : Type u_1} [inst : Preorder α], AddOpposite.instPreorder = Preorder.lift AddOpposite.unop
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffOn.neg_section : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s : (x : M) → V x} {u : Set M},
  ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u →
    ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (-s) x⟩) u
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_mono_ae_restrict : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f g : X → E}
  {s : Set X} [ClosedIciTopology E],
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.IntegrableOn g s μ → f ≤ᵐ[μ.restrict s] g → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- A function `f` from a measurable space to any type is called *simple*,
if every preimage `f ⁻¹' {x}` is measurable, and the range is finite. This structure bundles
a function with these properties.  -/
MeasureTheory.SimpleFunc : (α : Type u) → [MeasurableSpace α] → Type v → Type (max u v)
-- Mathlib.Order.JordanHolder
/-- The **Jordan-Hölder** theorem, stated for any `JordanHolderLattice`.
If two composition series start and finish at the same place, they are equivalent.  -/
CompositionSeries.jordan_holder : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s₁ s₂ : CompositionSeries X),
  RelSeries.head s₁ = RelSeries.head s₂ → RelSeries.last s₁ = RelSeries.last s₂ → s₁.Equivalent s₂
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomLeft_unop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᵒᵖ Dᵒᵖ] {c c' : Cᵒᵖ} (f : c ⟶ c') (d : Dᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.unop (Opposite.unop d) =
    Opposite.unop (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
/-- Given an inverse of `f 1`, construct the Dirichlet inverse of `f`. We use `Invertible` to make
this definition computable when `f` is computable.  -/
ArithmeticFunction.dirichletInverseFun : {R : Type u_1} → [inst : Ring R] → (f : ℕ → R) → Invertible (f 1) → ℕ → R
-- Batteries.Data.List.Lemmas
List.getElem_getElem_idxsOf : ∀ {α : Type u_1} {i : ℕ} {xs : List α} {x : α} [inst : BEq α] (h : i < (List.idxsOf x xs).length),
  (xs[(List.idxsOf x xs)[i]] == x) = true
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- Auxiliary lemma for `betaIntegral_convergent`, showing convergence at the left endpoint.  -/
Complex.betaIntegral_convergent_left : ∀ {u : ℂ},
  0 < u.re → ∀ (v : ℂ), IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) MeasureTheory.volume 0 (1 / 2)
-- Mathlib.Topology.Baire.Lemmas
/-- Definition of a Baire space.  -/
dense_iInter_of_isOpen_nat : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {f : ℕ → Set X},
  (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Matrix.transposePath.eq_1 : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] {A : Matrix n n R} {i j : n}
  (p : Quiver.Path i j),
  Matrix.transposePath p =
    Quiver.Path.rec Quiver.Path.nil
      (fun {b c} q e ih =>
        have eT := ⋯;
        (Quiver.Hom.toPath { down := eT }).comp ih)
      p
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.unitsSMulEquiv_symm_apply : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (w : HNNExtension.NormalWord d),
  (HNNExtension.NormalWord.unitsSMulEquiv φ).symm w = HNNExtension.NormalWord.unitsSMul φ (-1) w
-- Mathlib.Data.Finsupp.Basic
Finsupp.equivMapDomain_zero : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] {f : α ≃ β}, Finsupp.equivMapDomain f 0 = 0
-- Mathlib.Data.DFinsupp.Order
DFinsupp.inf_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → SemilatticeInf (α i)]
  (f g : Π₀ (i : ι), α i) (i : ι), (f ⊓ g) i = f i ⊓ g i
-- Mathlib.Order.Bounded
Set.bounded_le_Ico : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Bounded (fun x1 x2 => x1 ≤ x2) (Set.Ico a b)
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Infinite sums commute with scalar multiplication. Version for scalars living in a
`DivisionSemiring`; no summability hypothesis. This could be made to work for a
`[GroupWithZero γ]` if there was such a thing as `DistribMulActionWithZero`.  -/
tsum_const_smul'' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid α] {f : β → α}
  {L : SummationFilter β} {γ : Type u_5} [inst_2 : DivisionSemiring γ] [inst_3 : Module γ α] [ContinuousConstSMul γ α]
  [T2Space α] (g : γ), ∑'[L] (i : β), g • f i = g • ∑'[L] (i : β), f i
-- Mathlib.NumberTheory.ModularForms.SlashActions
_private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.slash_one : ∀ (k : ℤ) (f : UpperHalfPlane → ℂ), ModularForm.privateSlash✝ k 1 f = f
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.mk_list_dProd : ∀ {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMonoid A] (l : List α)
  (fι : α → ι) (fA : (a : α) → A (fι a)),
  GradedMonoid.mk (l.dProdIndex fι) (l.dProd fι fA) = (List.map (fun a => GradedMonoid.mk (fι a) (fA a)) l).prod
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.add_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄), (h.add h').h₃ = h.h₃ + h'.h₃
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.inclusion.isScalarTower_right : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  (h : S ≤ T) (X : Type u_1) [inst_3 : MulAction A X], IsScalarTower (↥S) (↥T) X
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupContent.value : Lean.Lsp.MarkupContent → String
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.cofilteredClosure.below.min : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  {f : α → C} {motive : (a : C) → CategoryTheory.IsCofiltered.cofilteredClosure f a → Prop} {j j' : C}
  (a : CategoryTheory.IsCofiltered.cofilteredClosure f j) (a_1 : CategoryTheory.IsCofiltered.cofilteredClosure f j'),
  CategoryTheory.IsCofiltered.cofilteredClosure.below a →
    motive j a →
      CategoryTheory.IsCofiltered.cofilteredClosure.below a_1 →
        motive j' a_1 → CategoryTheory.IsCofiltered.cofilteredClosure.below ⋯
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.mk : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} →
    (toSlashInvariantForm : SlashInvariantForm Γ k) →
      MDiff ⇑toSlashInvariantForm →
        (∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm.toFun k) → ModularForm Γ k
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toProp.eq_1 : ∀ (K : Type u_2) [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K],
  FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.addAssoc = ∀ (x y z : K), x + y + z = x + (y + z)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_vsub_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ : P), midpoint R p₁ p₂ -ᵥ p₁ = ⅟2 • (p₂ -ᵥ p₁)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
summable_iff_tsum_vanishing : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α] {f : β → α}
  [CompleteSpace α], Summable f ↔ ∀ e ∈ nhds 0, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∑' (b : ↑t), f ↑b ∈ e
-- Mathlib.Algebra.Group.AddChar
/-- `ψ⁻¹ = mulShift ψ (-1))`.  -/
AddChar.inv_mulShift : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M), ψ⁻¹ = ψ.mulShift (-1)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- A pair of continuous linear equivalences generates a continuous linear equivalence between
the spaces of continuous linear maps.  -/
ContinuousLinearEquiv.arrowCongr : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        {H : Type u_5} →
          [inst : AddCommGroup E] →
            [inst_1 : AddCommGroup F] →
              [inst_2 : AddCommGroup G] →
                [inst_3 : AddCommGroup H] →
                  [inst_4 : NormedField 𝕜] →
                    [inst_5 : Module 𝕜 E] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : Module 𝕜 G] →
                          [inst_8 : Module 𝕜 H] →
                            [inst_9 : TopologicalSpace E] →
                              [inst_10 : TopologicalSpace F] →
                                [inst_11 : TopologicalSpace G] →
                                  [inst_12 : TopologicalSpace H] →
                                    [inst_13 : IsTopologicalAddGroup G] →
                                      [inst_14 : IsTopologicalAddGroup H] →
                                        [inst_15 : ContinuousConstSMul 𝕜 G] →
                                          [inst_16 : ContinuousConstSMul 𝕜 H] →
                                            (E ≃L[𝕜] F) → (H ≃L[𝕜] G) → (E →L[𝕜] H) ≃L[𝕜] F →L[𝕜] G
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_one_eq_bot_iff : ∀ {G : Type u_1} [inst : Group G], ⊤.lowerCentralSeries 1 = ⊥ ↔ IsMulCommutative G
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_exp : ∀ {x : ℂ}, -Real.pi < x.im → x.im ≤ Real.pi → Complex.log (Complex.exp x) = x
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.coe_unitsWithZeroEquiv_eq_units_val : ∀ {α : Type u_1} [inst : Group α] (γ : (WithZero α)ˣ), ↑(WithZero.unitsWithZeroEquiv γ) = ↑γ
-- Init.Data.List.Lemmas
List.all_flatMap : ∀ {α : Type u_1} {β : Type u_2} {p : β → Bool} {l : List α} {f : α → List β},
  (List.flatMap f l).all p = l.all fun a => (f a).all p
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Build a `ForwardRuleMatches` structure containing the matches from `ms`.  -/
Aesop.ForwardRuleMatches.ofArray : Array Aesop.ForwardRuleMatch → Aesop.ForwardRuleMatches
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.MonoOver.inf_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  (f : CategoryTheory.MonoOver A),
  CategoryTheory.MonoOver.inf.obj f =
    (CategoryTheory.MonoOver.pullback f.arrow).comp (CategoryTheory.MonoOver.map f.arrow)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Stats.numCollisions : Lean.PersistentHashMap.Stats → ℕ
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyEntourage_empty : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X}, Dynamics.netEntropyEntourage T ∅ U = ⊥
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.instCoeFun : {R : Type u_1} → [inst : LinearOrder R] → [inst_1 : TopologicalSpace R] → CoeFun (StieltjesFunction R) fun x => R → ℝ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_assoc_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.AddMonObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.AddMonObj.add)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h))
-- Lean.Elab.ConfigEval.DeriveEvalTerm
/-- Ensures an `EvalTerm` instance exists for the given type by deriving one if necessary.
Derivation can handle `EvalTerm` instance for inductive types without universes, parameters, or indices,
and which only does simple recursion.
 -/
Lean.Elab.ConfigEval.ensureEvalTerm : Option (Lean.TSyntax `Lean.Parser.Command.visibility) →
  Lean.TSyntax `Lean.Parser.Term.attrKind → Lean.Syntax → Lean.Syntax → Lean.Expr → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
Real.hasDerivAt_Gamma_one : HasDerivAt Real.Gamma (-Real.eulerMascheroniConstant) 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso f g g').hom
      (CategoryTheory.Limits.pullback.fst f (CategoryTheory.CategoryStruct.comp g' g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f g) g')
      (CategoryTheory.Limits.pullback.fst f g)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.nodup_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.keys.Nodup
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.orthogonalProjectionOnto_orthogonal_apply_eq_zero`.

---

The orthogonal projection onto `Kᗮ` of an element of `K` is zero.  -/
Submodule.orthogonalProjection_orthogonal_apply_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : Kᗮ.HasOrthogonalProjection] {v : E}, v ∈ K → Kᗮ.orthogonalProjectionOnto v = 0
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_algEquiv_lpBCF_symm : ∀ {α : Type u_1} {A : Type u_4} {𝕜 : Type u_5} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α]
  [inst_2 : NormedRing A] [inst_3 : NormOneClass A] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedAlgebra 𝕜 A]
  (f : BoundedContinuousFunction α A), ↑((AlgEquiv.lpBCF α 𝕜).symm f) = ⇑f
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasStrictDerivAt.mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸} {c' d' : 𝔸},
  HasStrictDerivAt c c' x → HasStrictDerivAt d d' x → HasStrictDerivAt (c * d) (c' * d x + c x * d') x
-- Mathlib.Analysis.Normed.Module.Basic
instNormedRingRestrictScalars : {𝕜 : Type u_1} → {𝕜' : Type u_2} → {E : Type u_3} → [I : NormedRing E] → NormedRing (RestrictScalars 𝕜 𝕜' E)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
/-- See `expGrowthInf_mul_le` for a version with swapped argument `u` and `v`.  -/
ExpGrowth.expGrowthInf_mul_le' : ∀ {u v : ℕ → ENNReal},
  ExpGrowth.expGrowthInf u ≠ ⊥ ∨ ExpGrowth.expGrowthSup v ≠ ⊤ →
    ExpGrowth.expGrowthInf u ≠ ⊤ ∨ ExpGrowth.expGrowthSup v ≠ ⊥ →
      ExpGrowth.expGrowthInf (u * v) ≤ ExpGrowth.expGrowthInf u + ExpGrowth.expGrowthSup v
-- Mathlib.Data.ENNReal.Basic
ENNReal.one_lt_coe_iff : ∀ {p : NNReal}, 1 < ↑p ↔ 1 < p
-- Mathlib.GroupTheory.Solvable
Group.instIsSolvableProd : ∀ {G : Type u_1} [inst : Group G] {G' : Type u_3} [inst_1 : Group G'] [Group.IsSolvable G] [Group.IsSolvable G'],
  Group.IsSolvable (G × G')
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {G H : CategoryTheory.OplaxFunctor B CategoryTheory.Cat}
  (θ : CategoryTheory.Oplax.StrongTrans G H) {a b c : B} {a' : CategoryTheory.Cat} (f : a' ⟶ G.obj a) (g : a ⟶ b)
  (h : b ⟶ c) (X : ↑a'),
  CategoryTheory.CategoryStruct.comp
      ((θ.naturality (CategoryTheory.CategoryStruct.comp g h)).hom.toNatTrans.app (f.toFunctor.obj X))
      ((H.mapComp g h).toNatTrans.app ((θ.app a).toFunctor.obj (f.toFunctor.obj X))) =
    CategoryTheory.CategoryStruct.comp ((θ.app c).toFunctor.map ((G.mapComp g h).toNatTrans.app (f.toFunctor.obj X)))
      (CategoryTheory.CategoryStruct.comp
        ((θ.naturality h).hom.toNatTrans.app ((G.map g).toFunctor.obj (f.toFunctor.obj X)))
        ((H.map h).toFunctor.map ((θ.naturality g).hom.toNatTrans.app (f.toFunctor.obj X))))
-- Mathlib.RingTheory.Localization.Algebra
/-- Localizing the underlying linear map of `A →ₐ[R] B` in the sense of `IsLocalizedModule`
is the same as taking the underlying linear map of the localization in the sense of
`IsLocalization`.  -/
IsLocalization.mapExtendScalars_eq_toLinearMap_mapₐ : ∀ {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),
  (IsLocalizedModule.mapExtendScalars M (IsScalarTower.toAlgHom R A Aₚ).toLinearMap
        (IsScalarTower.toAlgHom R B Bₚ).toLinearMap Rₚ)
      f.toLinearMap =
    (IsLocalization.mapₐ M Rₚ Aₚ Bₚ f).toLinearMap
-- Mathlib.RingTheory.Finiteness.Defs
Module.Finite.of_fg_top : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⊤.FG → Module.Finite R M
-- Mathlib.CategoryTheory.Sites.Localization
CategoryTheory.GrothendieckTopology.W_adj_unit_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {A : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} A]
  {G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)}
  (adj : G ⊣ CategoryTheory.sheafToPresheaf J A) (P : CategoryTheory.Functor Cᵒᵖ A), J.W (adj.unit.app P)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.contains (t.maxKey he) = true
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- `mk_iff_of_inductive_prop i r` makes an `iff` rule for the inductively-defined proposition `i`.
The new rule `r` has the shape `∀ ps is, i as ↔ ⋁_j, ∃ cs, is = cs`, where
* `ps` are the type parameters,
* `is` are the indices,
* `j` ranges over all possible constructors,
* the `cs` are the parameters for each of the constructors, and
* the equalities `is = cs` are the instantiations for
  each constructor for each of the indices to the inductive type `i`.

In each case, we remove constructor parameters (i.e. `cs`) when the corresponding equality would
be just `c = i` for some index `i`.

For example, `mk_iff_of_inductive_prop` on `List.Chain` produces:

```lean
∀ { α : Type*} (R : α → α → Prop) (a : α) (l : List α),
  Chain R a l ↔ l = [] ∨ ∃ (b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
```

See also the `mk_iff` user attribute.
 -/
Mathlib.Tactic.MkIff.mkIffOfInductiveProp : Lean.ParserDescr
-- Init.Data.Float.Model.Float32
Float32.Model.mk.sizeOf_spec : ∀ (toBits : UInt32) (valid : Float.Model.Format.binary32.Valid toBits.toBitVec),
  sizeOf { toBits := toBits, valid := valid } = 1 + sizeOf toBits + sizeOf valid
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.alter.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp]
  (t t_1 : Std.DTreeMap.Raw α β cmp),
  t = t_1 → ∀ (a : α) (f f_1 : Option (β a) → Option (β a)), f = f_1 → t.alter a f = t_1.alter a f_1
-- Mathlib.CategoryTheory.Category.Bipointed
pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun : ∀ (X : Pointed) (a : ((CategoryTheory.Functor.id Pointed).obj X).X),
  (pointedToBipointedCompBipointedToPointedSnd.inv.app X).toFun a = a
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- Composition of `StrictlyUnitaryLaxFunctor` is strictly left unitary  -/
CategoryTheory.StrictlyUnitaryLaxFunctor.id_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.StrictlyUnitaryLaxFunctor B C), (CategoryTheory.StrictlyUnitaryLaxFunctor.id B).comp F = F
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.isEdgeReachable_one : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.IsEdgeReachable 1 u v ↔ G.Reachable u v
-- Init.Data.Nat.Lcm
Nat.lcm_div : ∀ {m n k : ℕ}, k ∣ m → k ∣ n → (m / k).lcm (n / k) = m.lcm n / k