mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.PiL2
Matrix.toEuclideanLin_eq_toLin_orthonormal : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {m : Type u_7} {n : Type u_8} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m],
  Matrix.toEuclideanLin = Matrix.toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Extract the structural 2-isomorphism.  -/
Mathlib.Tactic.BicategoryLike.CoherenceHom.unfold : Mathlib.Tactic.BicategoryLike.CoherenceHom → Lean.Expr
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.mk : {V : Type u} → {E : Type v} → {F : outParam (Type w)} → (V → E → F) → LineDeriv V E F
-- Mathlib.RingTheory.Localization.FractionRing
/-- `NNRat` is the ring of fractions of `Nat`.  -/
NNRat.isFractionRing : IsFractionRing ℕ ℚ≥0
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.of_not_le : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : LE α] [Lean.Grind.ToInt.LE α i]
  {a b : α} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ¬a ≤ b → b' + 1 ≤ a'
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.rotate_map_eq_iff : ∀ {n : ℕ} {x y : Option (BitVec n)}, BitVec.Signed.rotate✝ <$> x = y ↔ x = BitVec.Signed.rotate✝ <$> y
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the smallest element that is less than the given element,
returning `fallback` if no such element exists.
 -/
Std.TreeSet.getLTD : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → α → α
-- Init.Data.Array.Lex.Lemmas
Array.instTotalLeOfAsymmLt : ∀ {α : Type u_1} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Insert an element below all the others, without any comparisons.
(Assumes that the element is in fact below all the others).

```
insertMin {1, 2} 0 = {0, 1, 2}
insertMin {1, 2} 4 = precondition violation
```  -/
Ordnode.insertMin : {α : Type u_1} → α → Ordnode α → Ordnode α
-- Mathlib.LinearAlgebra.Dimension.OrzechProperty
setBasisOfTopLeSpanOfCardEqFinrank_repr_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : OrzechProperty R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {s : Set M} [inst_4 : Fintype ↑s] (le_span : ⊤ ≤ Submodule.span R s)
  (card_eq : s.toFinset.card = Module.finrank R M) (x : M),
  (setBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr x =
    ⋯.repr ((LinearMap.codRestrict (Submodule.span R (Set.range Subtype.val)) LinearMap.id ⋯) x)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.continuousOn_log : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [CompleteSpace A],
  ContinuousOn CFC.log {a | IsSelfAdjoint a ∧ IsUnit a}
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.one_rpow : ∀ (x : ℝ), 1 ^ x = 1
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.descResidueField.hcongr_6 : ∀ (K K' : Type u),
  K = K' →
    ∀ (inst : Field K) (inst' : Field K'),
      inst ≍ inst' →
        ∀ (X X' : AlgebraicGeometry.Scheme),
          X = X' →
            ∀ (x : ↥X) (x' : ↥X'),
              x ≍ x' →
                ∀ (f : X.presheaf.stalk x ⟶ CommRingCat.of K) (f' : X'.presheaf.stalk x' ⟶ CommRingCat.of K'),
                  f ≍ f' →
                    ∀ (inst_1 : IsLocalHom (CommRingCat.Hom.hom f)) (inst'_1 : IsLocalHom (CommRingCat.Hom.hom f')),
                      inst_1 ≍ inst'_1 →
                        AlgebraicGeometry.Scheme.descResidueField f ≍ AlgebraicGeometry.Scheme.descResidueField f'
-- Mathlib.GroupTheory.GroupAction.Defs
FixedPoints.subgroup_toSubmonoid : ∀ (M : Type u) (α : Type v) [inst : Monoid M] [inst_1 : Group α] [inst_2 : MulDistribMulAction M α],
  (FixedPoints.subgroup M α).toSubmonoid = FixedPoints.submonoid M α
-- Mathlib.Topology.Connected.TotallyDisconnected
Continuous.connectedComponentsLift_continuous : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f), Continuous h.connectedComponentsLift
-- Mathlib.Data.Nat.Find
Nat.findGreatest_zero : ∀ {P : ℕ → Prop} [inst : DecidablePred P], Nat.findGreatest P 0 = 0
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_eq' : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} (s : Finset (Equiv.Perm α)),
  (∀ f ∈ s, f.IsCycle) →
    ∀ (h2 : (↑s).Pairwise Equiv.Perm.Disjoint),
      s.noncommProd id ⋯ = σ → σ.cycleType = Multiset.map (Finset.card ∘ Equiv.Perm.support) s.val
-- Mathlib.Analysis.Convex.Strict
strictConvex_singleton : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : Module 𝕜 E] (c : E), StrictConvex 𝕜 {c}
-- Mathlib.Data.Set.Operations
/-- `kernImage f s` is the set of `y` such that `f ⁻¹ y ⊆ s`.  -/
Set.kernImage : {α : Type u} → {β : Type v} → (α → β) → Set α → Set β
-- Init.Data.Vector.Lemmas
Vector.forall_mem_push : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector α n} {a : α}, (∀ x ∈ xs.push a, p x) ↔ p a ∧ ∀ x ∈ xs, p x
-- Mathlib.Data.Set.Lattice
Set.disjoint_sUnion_right : ∀ {α : Type u_1} {s : Set α} {S : Set (Set α)}, Disjoint s (⋃₀ S) ↔ ∀ t ∈ S, Disjoint s t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryGTD_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {fallback : α × β},
          Std.DTreeMap.Internal.Impl.Const.getEntryGTD k t₁ fallback =
            Std.DTreeMap.Internal.Impl.Const.getEntryGTD k t₂ fallback
-- Mathlib.Order.Bounded
Set.bounded_le_Ioo : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Bounded (fun x1 x2 => x1 ≤ x2) (Set.Ioo a b)
-- Mathlib.Algebra.Ring.Defs
/-- A unital but not-necessarily-associative semiring.  -/
NonAssocSemiring : Type u → Type u
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The fifth simplicial identity  -/
SimplexCategory.σ_comp_σ_assoc : ∀ {n : ℕ} {i j : Fin (n + 1)},
  i ≤ j →
    ∀ {Z : SimplexCategory} (h : { len := n } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i.castSucc)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j.succ)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) h)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasCokernel S.f]
  [inst_3 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)],
  (CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel S).Q = CategoryTheory.Limits.cokernel S.f
-- Mathlib.Data.Finset.Slice
Set.Sized.card_le : ∀ {α : Type u_1} [inst : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ}, Set.Sized r ↑𝒜 → 𝒜.card ≤ (Fintype.card α).choose r
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatQuarterLong : Std.Time.DateFormatSymbols → Std.Time.Month.Quarter → String
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.sConvexComb_map : ∀ {R : Type u_1} {M : Type u_3} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] (w : Convexity.StdSimplex R I) (f : I → M),
  Convexity.sConvexComb (Convexity.StdSimplex.map f w) = Convexity.iConvexComb w f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.buckets_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {c i : ℕ}
  {h : i < (Std.DHashMap.emptyWithCapacity c).inner.buckets.size},
  (Std.DHashMap.emptyWithCapacity c).inner.buckets[i] = Std.DHashMap.Internal.AssocList.nil
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- A pretransitive action on a set of prime order is preprimitive  -/
MulAction.IsPreprimitive.of_prime_card : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [hGX : MulAction.IsPretransitive G X],
  Nat.Prime (Nat.card X) → MulAction.IsPreprimitive G X
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.zpow : ∀ {α : Type u_1} {β : Type u_3} [inst : NormedField β] {t u : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l t u → ∀ (z : ℤ), Asymptotics.IsEquivalent l (t ^ z) (u ^ z)
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Summable.hasSumUniformlyOn_log_one_add : ∀ {α : Type u_1} {ι : Type u_2} {K : Set α} {u : ι → ℝ} {f : ι → α → ℂ},
  Summable u →
    (∀ᶠ (i : ι) in Filter.cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) →
      HasSumUniformlyOn (fun i x => Complex.log (1 + f i x)) (fun x => ∑' (i : ι), Complex.log (1 + f i x)) K
-- Std.Async.Basic
Std.Async.EAsync.instMonadAwaitPromise : {ε : Type} → Std.Async.MonadAwait IO.Promise (Std.Async.EAsync ε)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
CategoryTheory.Limits.weakEqualizer.fork_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasWeakEqualizer f g],
  (CategoryTheory.Limits.weakEqualizer.fork f g).ι = CategoryTheory.Limits.weakEqualizer.ι f g
-- Batteries.Control.AlternativeMonad
mapConst_orElse : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Alternative m] [LawfulAlternative m] (x x' : m α) (y : β),
  Functor.mapConst y (x <|> x') = (Functor.mapConst y x <|> Functor.mapConst y x')
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiStruct.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      {f : Y ⟶ X} →
        (desc :
            {W : C} →
              (e : Y ⟶ W) →
                (∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
                    CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
                      CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) →
                  (X ⟶ W)) →
          (∀ {W : C} (e : Y ⟶ W)
              (h :
                ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
                  CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
                    CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e),
              CategoryTheory.CategoryStruct.comp f (desc e ⋯) = e) →
            (∀ {W : C} (e : Y ⟶ W)
                (h :
                  ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
                    CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
                      CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)
                (m : X ⟶ W), CategoryTheory.CategoryStruct.comp f m = e → m = desc e ⋯) →
              CategoryTheory.EffectiveEpiStruct f
-- Mathlib.Geometry.Euclidean.Angle.Bisector
/-- A point `p` is equidistant to two affine subspaces if and only if the angles at a point `p'`
in their intersection between `p` and its orthogonal projections onto the subspaces are equal.  -/
EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} [inst_4 : s₁.direction.HasOrthogonalProjection]
  [inst_5 : s₂.direction.HasOrthogonalProjection] (hp'₁ : p' ∈ s₁) (hp'₂ : p' ∈ s₂),
  dist p ↑((EuclideanGeometry.orthogonalProjection s₁) p) = dist p ↑((EuclideanGeometry.orthogonalProjection s₂) p) ↔
    EuclideanGeometry.angle p p' ↑((EuclideanGeometry.orthogonalProjection s₁) p) =
      EuclideanGeometry.angle p p' ↑((EuclideanGeometry.orthogonalProjection s₂) p)
-- Mathlib.RingTheory.Length
Module.length_pos : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M],
  0 < Module.length R M
-- Mathlib.CategoryTheory.Join.Basic
/-- Two natural transformations between functors out of a join are equal if they are so
after whiskering with the inclusions.  -/
CategoryTheory.Join.natTrans_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  {F F' : CategoryTheory.Functor (CategoryTheory.Join C D) E} {α β : F ⟶ F'},
  (CategoryTheory.Join.inclLeft C D).whiskerLeft α = (CategoryTheory.Join.inclLeft C D).whiskerLeft β →
    (CategoryTheory.Join.inclRight C D).whiskerLeft α = (CategoryTheory.Join.inclRight C D).whiskerLeft β → α = β
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.id_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (x : TopPair.HomologyPretheory C c) (i : ι),
  (CategoryTheory.CategoryStruct.id x).hom i =
    CategoryTheory.CategoryStruct.comp (x.iso i).hom
      (CategoryTheory.CategoryStruct.comp
        (TopPair.incl.whiskerLeft ((fun x_1 => CategoryTheory.CategoryStruct.id (x.Hₚ x_1)) i)) (x.iso i).inv)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- In a space with second countable topology and a sigma-finite measure,
an `AEMeasurable` function is `AEFinStronglyMeasurable`.  -/
MeasureTheory.aefinStronglyMeasurable_of_aemeasurable : ∀ {α : Type u_1} {G : Type u_5} [inst : SeminormedAddCommGroup G] [inst_1 : MeasurableSpace G] [BorelSpace G]
  [SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α)
  [MeasureTheory.SigmaFinite μ], AEMeasurable f μ → MeasureTheory.AEFinStronglyMeasurable f μ
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.AnchorRef.toString : Lean.Meta.Grind.AnchorRef → String
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.ofSupport_cons_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {l : List V} (hchain : List.IsChain G.Adj (u :: v :: l)),
  SimpleGraph.Walk.ofSupport (u :: v :: l) ⋯ hchain = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.ofSupport (v :: l) ⋯ ⋯)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF →
    t₂.WF →
      ∀ {k fallback : α},
        (t₁ \ t₂).getKeyD k fallback = if t₂.contains k = true then fallback else t₁.getKeyD k fallback
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.toSubmersivePresentation_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePresentation R S) (a : Fin 2), P.toSubmersivePresentation.map a = id a
-- Mathlib.Analysis.Complex.Trigonometric
Real.tan_eq_sin_div_cos : ∀ (x : ℝ), Real.tan x = Real.sin x / Real.cos x
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.karoubiUniversal_functor_eq : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.IsIdempotentComplete D],
  (CategoryTheory.Idempotents.karoubiUniversal C D).functor = CategoryTheory.Idempotents.functorExtension C D
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_iff_isSome_getKey? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, a ∈ m ↔ (m.getKey? a).isSome = true
-- Mathlib.Data.Nat.Choose.Multinomial
Finsupp.multinomial_of_support_subset : ∀ {σ : Type u_1} {d : σ →₀ ℕ} {s : Finset σ}, d.support ⊆ s → Nat.multinomial s ⇑d = d.multinomial
-- Mathlib.NumberTheory.ModularForms.Derivative
/-- Normalized derivative $D = \frac{1}{2\pi i} \frac{d}{dz}$.
 -/
Derivative.normalizedDerivOfComplex : (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂ
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.gate.eq_1 : ∀ (f : Std.Sat.AIG.Fanin), f.gate = f.val / 2
-- Mathlib.Topology.EMetricSpace.Defs
Subtype.preimage_eball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ENNReal),
  Subtype.val ⁻¹' Metric.eball (↑a) r = Metric.eball a r
-- Lean.Elab.Do.Basic
/-- The inferred type of the monad of type `Type u → Type v`.  -/
Lean.Elab.Do.MonadInfo.m : Lean.Elab.Do.MonadInfo → Lean.Expr
-- Mathlib.Data.Nat.Choose.Sum
Nat.four_pow_le_two_mul_add_one_mul_central_binom : ∀ (n : ℕ), 4 ^ n ≤ (2 * n + 1) * (2 * n).choose n
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.inter_mem : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α}, MeasureTheory.IsSetRing C → s ∈ C → t ∈ C → s ∩ t ∈ C
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.none.sizeOf_spec : sizeOf Lean.Meta.Sym.Arith.ClassifyResult.none = 1
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.col_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) (i : n) (j : m), A.col i j = A j i
-- Init.Data.Int.LemmasAux
Int.natCast_succ_pos : ∀ (n : ℕ), 0 < ↑n.succ
-- Mathlib.Algebra.Order.Module.Defs
lt_inv_smul_iff_of_pos : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : GroupWithZero α] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : MulAction α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β], 0 < a → (b₁ < a⁻¹ • b₂ ↔ a • b₁ < b₂)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`.  -/
InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x ≠ 0 → InnerProductGeometry.angle x (x + y) = Real.arctan (‖y‖ / ‖x‖)
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.image_ball_subset_compact : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : TopologicalSpace M₂]
  [inst_4 : AddCommMonoid M₂] [inst_5 : NormedSpace 𝕜₁ M₁] [inst_6 : Module 𝕜₂ M₂] [ContinuousConstSMul 𝕜₂ M₂]
  {f : M₁ →ₛₗ[σ₁₂] M₂}, IsCompactOperator ⇑f → ∀ (r : ℝ), ∃ K, IsCompact K ∧ ⇑f '' Metric.ball 0 r ⊆ K
-- Mathlib.Data.List.TakeWhile
List.find?_eq_head_dropWhile_not : ∀ {α : Type u_1} {p : α → Bool} {l : List α} (h : ∃ x ∈ l, p x = true),
  List.find? p l = some ((List.dropWhile (fun x => !p x) l).head ⋯)
-- Mathlib.Algebra.Free
FreeAddSemigroup.mk : {α : Type u} → α → List α → FreeAddSemigroup α
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportKind.mk.inj : ∀ {isPrivate isAll : Bool} {metaKind : Lean.Lsp.LeanImportMetaKind} {isPrivate_1 isAll_1 : Bool}
  {metaKind_1 : Lean.Lsp.LeanImportMetaKind},
  { isPrivate := isPrivate, isAll := isAll, metaKind := metaKind } =
      { isPrivate := isPrivate_1, isAll := isAll_1, metaKind := metaKind_1 } →
    isPrivate = isPrivate_1 ∧ isAll = isAll_1 ∧ metaKind = metaKind_1
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.indep_of_forall_finite_subset_indep : ∀ {α : Type u_1} {M : Matroid α} [M.Finitary] (I : Set α), (∀ J ⊆ I, J.Finite → M.Indep J) → M.Indep I
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.const_smul : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F} {M : Type u_3} [inst_1 : SeminormedRing M]
  [inst_2 : Module M F] [NormSMulClass M F] (α : M),
  AbsolutelyContinuousOnInterval f a b → AbsolutelyContinuousOnInterval (fun x => α • f x) a b
-- Init.Data.String.Iterator
/-- Moves the iterator's position back by the specified number of characters, stopping at the beginning
of the string.
 -/
String.Legacy.Iterator.prevn : String.Legacy.Iterator → ℕ → String.Legacy.Iterator
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.IsZero.eq : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] {χ : LieModule.Weight R L M}, χ.IsZero → ⇑χ = 0
-- Aesop.Tree.TreeM
Aesop.TreeM.Context.currentIteration : Aesop.TreeM.Context → Aesop.Iteration
-- Init.Data.Bool
Bool.xor_left_comm : ∀ (x y z : Bool), (x ^^ (y ^^ z)) = (y ^^ (x ^^ z))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N P : C} [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.MonObj N] [inst_5 : CategoryTheory.MonObj P],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) P
          (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) P)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
            (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul))
          CategoryTheory.MonObj.mul))
      (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom
        (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ M (CategoryTheory.MonoidalCategoryStruct.tensorObj N P) M
          (CategoryTheory.MonoidalCategoryStruct.tensorObj N P))
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ N P N P)
            (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul))))
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Approximate a function `α → ℝ≥0∞` by a sequence of simple functions.  -/
MeasureTheory.SimpleFunc.eapprox : {α : Type u_1} → [inst : MeasurableSpace α] → (α → ENNReal) → ℕ → MeasureTheory.SimpleFunc α ENNReal
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.optionEquivLeft_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (r : R),
  (MvPowerSeries.optionEquivLeft σ R) (MvPowerSeries.C r) = PowerSeries.C (MvPowerSeries.C r)
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.coverEntropy_eq_iSup_basis_netEntropyEntourage : ∀ {X : Type u_1} [inst : UniformSpace X] {ι : Sort u_2} {p : ι → Prop} {s : ι → SetRel X X},
  (uniformity X).HasBasis p s →
    ∀ (T : X → X) (F : Set X), Dynamics.coverEntropy T F = ⨆ i, ⨆ (_ : p i), Dynamics.netEntropyEntourage T F (s i)
-- Mathlib.RepresentationTheory.Basic
Representation.smul_tprod_one_asModule : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring k] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : Module k V] [inst_4 : AddCommMonoid W] [inst_5 : Module k W]
  (ρV : Representation k G V) (r : MonoidAlgebra k G) (x : V) (y : W),
  (r •
      have this := x ⊗ₜ[k] y;
      this) =
    (r •
        have this := x;
        this) ⊗ₜ[k]
      y
-- Mathlib.Probability.ProbabilityMassFunction.Monad
/-- `bindOnSupport` reduces to `bind` if `f` doesn't depend on the additional hypothesis.  -/
PMF.bindOnSupport_eq_bind : ∀ {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β), (p.bindOnSupport fun a x => f a) = p.bind f
-- Std.Data.Iterators.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.instProductivenessRelation : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        [inst_1 : Monad m] →
          [Std.Iterators.Productive α m] → Std.Iterators.ProductivenessRelation (Std.Iterators.Types.Drop α m β) m