mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Polish
IsOpen.isClopenable : ∀ {α : Type u_1} [inst : TopologicalSpace α] [PolishSpace α] {s : Set α}, IsOpen s → PolishSpace.IsClopenable s
-- Init.Data.String.Slice
String.Slice.SplitInclusiveIterator.operating.inj : ∀ {σ : String.Slice → Type} {ρ : Type} {pat : ρ} {s : String.Slice}
  {inst : String.Slice.Pattern.ToForwardSearcher pat σ} {currPos : s.Pos}
  {searcher : Std.Iter (String.Slice.Pattern.SearchStep s)} {currPos_1 : s.Pos}
  {searcher_1 : Std.Iter (String.Slice.Pattern.SearchStep s)},
  String.Slice.SplitInclusiveIterator.operating currPos searcher =
      String.Slice.SplitInclusiveIterator.operating currPos_1 searcher_1 →
    currPos = currPos_1 ∧ searcher = searcher_1
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation on `R` is bounded above by 1.  -/
IsDedekindDomain.HeightOneSpectrum.valuation_le_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
  (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑r ≤ 1
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
/-- The multiplicative `v`-adic valuation on `Kˣ`.  -/
IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun : {R : Type u} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      {K : Type v} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [IsFractionRing R K] → IsDedekindDomain.HeightOneSpectrum R → Kˣ → Multiplicative ℤ
-- Lean.DocString.Markdown
/-- Records a footnote and its rendered body. Internal to the renderer.  -/
_private.Lean.DocString.Markdown.0.Lean.Doc.MarkdownM.addFootnote : String → String → Lean.Doc.MarkdownM Unit
-- Mathlib.Order.CompleteLattice.Basic
iInf_extend_top : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] {e : ι → β},
  Function.Injective e → ∀ (f : ι → α), ⨅ j, Function.extend e f ⊤ j = ⨅ i, f i
-- Init.Data.Vector.Lemmas
Vector.some_eq_getElem?_iff : ∀ {α : Type u_1} {n : ℕ} {b : α} {i : ℕ} {xs : Vector α n}, some b = xs[i]? ↔ ∃ (h : i < n), xs[i] = b
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonWorkDoneProgressParams : Lean.ToJson Lean.Lsp.WorkDoneProgressParams
-- Init.Prelude
instDecidableEqUInt16 : DecidableEq UInt16
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.Hom.ext : ∀ {R : Type u} {inst : CommRing R} {A B : CommHopfAlgCat R} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonUnitalNonAssocSemiring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Mul M],
  MonoidAlgebra.nonUnitalNonAssocSemiring =
    { toAddCommMonoid := MonoidAlgebra.instAddCommMonoid, toMul := MonoidAlgebra.instMul, left_distrib := ⋯,
      right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.forget_createsLimitsOfShape.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J],
  CommMonCat.forget_createsLimitsOfShape = { CreatesLimit := fun {K} => inferInstance }
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The morphism `tensorObj X₁ Y₁ ⟶ tensorObj X₂ Y₂` induced by morphisms of graded
objects `f : X₁ ⟶ X₂` and `g : Y₁ ⟶ Y₂`.  -/
CategoryTheory.GradedObject.Monoidal.tensorHom : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} →
            (X₁ ⟶ X₂) →
              (Y₁ ⟶ Y₂) →
                [inst_3 : X₁.HasTensor Y₁] →
                  [inst_4 : X₂.HasTensor Y₂] →
                    CategoryTheory.GradedObject.Monoidal.tensorObj X₁ Y₁ ⟶
                      CategoryTheory.GradedObject.Monoidal.tensorObj X₂ Y₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_eq_default : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α}, a ∉ t → Std.ExtDTreeMap.Const.get! t a = default
-- Mathlib.Order.Heyting.Basic
Prod.instHNot.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : HNot α] [inst_1 : HNot β], Prod.instHNot = { hnot := fun a => (￢a.1, ￢a.2) }
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
/-- When only one member of the family of multilinear maps is nonzero, the result consists only of
the component from that member.  -/
MultilinearMap.dfinsuppFamily_single_left_apply : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : Semiring R]
  [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)]
  [inst_5 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_6 : (p : (i : ι) → κ i) → Module R (N p)]
  [inst_7 : (i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i) (f : MultilinearMap R (fun i => M i (p i)) (N p))
  (x : (i : ι) → Π₀ (j : κ i), M i j),
  (MultilinearMap.dfinsuppFamily (Pi.single p f)) x = fun₀ | p => f fun i => (x i) (p i)
-- Mathlib.Order.WithBot
WithTop.le_of_forall_lt_iff_le : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : WithTop α} [DenselyOrdered α] [NoMaxOrder α],
  (∀ (z : α), x < ↑z → y ≤ ↑z) ↔ y ≤ x
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.of_op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [W.op.IsMultiplicative], W.IsMultiplicative
-- Mathlib.ModelTheory.Order
FirstOrder.Language.HomClass.strictMono : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] {N : Type u_1}
  [inst_2 : L.Structure N] {F : Type u_2} [inst_3 : FunLike F M N] [L.HomClass F M N] [EmbeddingLike F M N]
  [inst_6 : PartialOrder M] [L.OrderedStructure M] [inst_8 : PartialOrder N] [L.OrderedStructure N] (f : F),
  StrictMono ⇑f
-- Mathlib.Tactic.TermCongr
Mathlib.Tactic.TermCongr.CongrType.eq.sizeOf_spec : sizeOf Mathlib.Tactic.TermCongr.CongrType.eq = 1
-- Init.Data.Vector.Lex
_private.Init.Data.Vector.Lex.0.Array.lex.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (as bs : Array α) (lt : α → α → Bool),
  as.lex bs lt =
    (do
        let __s ←
          forIn' (0...min as.size bs.size) (none, ()) fun i h __s =>
              have __r := __s;
              have this := ⋯;
              if lt as[i] bs[i] = true then pure (ForInStep.done (some true, ()))
              else
                if (as[i] != bs[i]) = true then pure (ForInStep.done (some false, ()))
                else pure (ForInStep.yield (none, ()))
        have __r : Option Bool × Unit := __s
        match __r.1 with
          | some r => pure r
          | none => pure (decide (as.size < bs.size))).run
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.IsStarConvexSet.add : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Convexity.ConvexSpace R M]
  [Convexity.IsModuleConvexSpace R M] {x y : M} {s t : Set M},
  Convexity.IsStarConvexSet R x s → Convexity.IsStarConvexSet R y t → Convexity.IsStarConvexSet R (x + y) (s + t)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- A zero object is a retract of every object.  -/
CategoryTheory.Limits.IsZero.retract : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → (Y : C) → CategoryTheory.Limits.IsZero X → CategoryTheory.Retract X Y
-- Mathlib.Logic.Equiv.Defs
Equiv.comp_injective : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ), Function.Injective (⇑e ∘ f) ↔ Function.Injective f
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.fderivCLM.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] (n k : ℕ∞) [inst_6 : Algebra ℝ 𝕜]
  [inst_7 : IsScalarTower ℝ 𝕜 F],
  TestFunction.fderivCLM 𝕜 n k =
    TestFunction.limitCLM 𝕜
      (fun f =>
        if hk : k + 1 ≤ n then { toFun := fderiv ℝ ⇑f, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
        else 0)
      (fun K K_sub_Ω => TestFunction.ofSupportedInCLM 𝕜 K_sub_Ω ∘SL ContDiffMapSupportedIn.fderivCLM 𝕜 n k) ⋯
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
/-- Bijection between an additive subsemigroup `H` and its opposite.
 -/
AddSubsemigroup.equivOp : {M : Type u_2} → [inst : Add M] → (H : AddSubsemigroup M) → ↥H ≃ ↥H.op
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_2 : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] {𝕜 : Type u_5} [inst_5 : NormedRing 𝕜] [inst_6 : Module 𝕜 E]
  [inst_7 : IsBoundedSMul 𝕜 E], SMulCommClass 𝕜 Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Algebra.Order.Monovary
antivaryOn_neg_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommGroup β]
  [inst_2 : PartialOrder β] [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  AntivaryOn f (-g) s ↔ MonovaryOn f g s
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (Rep.coinvariantsFunctor k G).obj A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles (groupHomology.inhomogeneousChains A) 0)
      (CategoryTheory.CategoryStruct.comp (groupHomology.opcyclesIso₀ A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₀ A).hom
      (CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) h)
-- Mathlib.Topology.ContinuousMap.Basic
/-- Given two continuous maps `f` and `g`, this is the continuous map `x ↦ (f x, g x)`.  -/
ContinuousMap.prodMk : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    {β₁ : Type u_7} →
      {β₂ : Type u_8} →
        [inst_1 : TopologicalSpace β₁] → [inst_2 : TopologicalSpace β₂] → C(α, β₁) → C(α, β₂) → C(α, β₁ × β₂)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
/-- The fundamental group is the automorphism group (vertex group) of the basepoint
in the fundamental groupoid.  -/
FundamentalGroup : (X : Type u_1) → [TopologicalSpace X] → X → Type u_1
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.of_isInvertible_inverse : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂}, f.inverse.IsInvertible → f.IsInvertible
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtrOn.congr : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {f g : α → β} {a : α},
  IsLocalExtrOn f s a → f =ᶠ[nhdsWithin a s] g → a ∈ s → IsLocalExtrOn g s a
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
_private.Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno.0.OrderedFinpartition.extend.match_1.eq_1 : ∀ {n : ℕ} (c : OrderedFinpartition n) (motive : Option (Fin c.length) → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : (i : Fin c.length) → motive (some i)),
  (match none with
    | none => h_1 ()
    | some i => h_2 i) =
    h_1 ()
-- Std.Sat.AIG.Basic
/-- The `Decl` cache, valid with respect to `decls`.
 -/
Std.Sat.AIG.cache : {α : Type} → [inst : DecidableEq α] → [inst_1 : Hashable α] → (self : Std.Sat.AIG α) → Std.Sat.AIG.Cache α self.decls
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.baseSupp_apply_smul_e : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [inst_4 : Fintype ι] (i : ι) (x : ↥H),
  (b.baseSupp i) x • b.e i = ⁅x, b.e i⁆
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instReprLocalTimeType.repr : Std.Time.TimeZone.TZif.LocalTimeType → ℕ → Std.Format
-- Lean.Attributes
/-- Return true iff `n` is the name of a registered attribute.  -/
Lean.isBuiltinAttribute : Lean.Name → IO Bool
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.disjoint_iff_left : ∀ {α : Type u_1} {ι : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → (Disjoint l l' ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l')
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
IsNonarchimedean.apply_natCast_le_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3}
  [inst_2 : AddMonoidWithOne α] [inst_3 : FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] [OneHomClass F α R]
  {f : F}, IsNonarchimedean ⇑f → ∀ {n : ℕ}, f ↑n ≤ 1
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelDesc_norm_le : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0),
  ‖SemiNormedGrp.explicitCokernelDesc w‖ ≤ ‖g‖
-- Mathlib.Data.Fintype.Sets
Finset.univ_eq_attach : ∀ {α : Type u} (s : Finset α), Finset.univ = s.attach
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.sigmaFinite : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb → ∀ [MeasureTheory.SigmaFinite μb], MeasureTheory.SigmaFinite μa
-- Mathlib.RingTheory.Coalgebra.Convolution
/-- Convolution product on linear maps from a coalgebra to an algebra.  -/
LinearMap.convMul : {R : Type u_1} →
  {A : Type u_3} →
    {C : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : AddCommMonoid C] → [inst_6 : Module R C] → [CoalgebraStruct R C] → Mul (WithConv (C →ₗ[R] A))
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_subtype : ∀ {𝕜 : Type u_1} {U : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U] [inst_2 : InnerProductSpace 𝕜 U]
  [inst_3 : FiniteDimensional 𝕜 U] (p : Submodule 𝕜 U), p.subtype.normDet = 1
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.Monic.of_subsingleton : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [Subsingleton R] {f : MvPolynomial σ R},
  m.Monic f
-- Mathlib.Order.Filter.Pointwise
Filter.HasBasis.smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {g : Filter β} {ιf : Type u_7} {ιg : Type u_8}
  {pf : ιf → Prop} {sf : ιf → Set α} {pg : ιg → Prop} {sg : ιg → Set β},
  f.HasBasis pf sf → g.HasBasis pg sg → (f • g).HasBasis (fun i => pf i.1 ∧ pg i.2) fun i => sf i.1 • sg i.2
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.codChart_mem_maximalAtlas : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAtOfComplement F I J n f x), h.codChart ∈ IsManifold.maximalAtlas J n N
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeSort : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrix_le_zero_of_ne : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [CharZero R] [IsDomain R] [Finite ι] (i j : ↥b.support),
  i ≠ j → b.cartanMatrix i j ≤ 0
-- Mathlib.SetTheory.Lists
Lists.Equiv.trans : ∀ {α : Type u_1} {l₁ l₂ l₃ : Lists α}, l₁.Equiv l₂ → l₂.Equiv l₃ → l₁.Equiv l₃
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.prod_pi_mulSingle'`.  -/
Fintype.prod_pi_mulSingle' : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι) (a : M),
  ∏ j, Pi.mulSingle i a j = a
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.tsupport_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c), tsupport ↑f = Metric.closedBall c f.rOut
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.invRotate_map_hom₁ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  ((CategoryTheory.Pretriangulated.invRotate C).map f).hom₁ = (CategoryTheory.shiftFunctor C (-1)).map f.hom₃
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_mem_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β} {a : α} {b : β}, a ∈ s → b ∈ t → a • b ∈ s • t
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max!_le_max!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {k : α}, (cmp t.max! (t.insert k).max!).isLE = true
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_eq_nhds_of_re_pos : ∀ {x : ℂ}, 0 < x.re → Complex.arg =ᶠ[nhds x] fun x => Real.arcsin (x.im / ‖x‖)
-- Mathlib.Topology.Algebra.Order.Support
HasCompactSupport.sup : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : Zero M] [inst_2 : SemilatticeSup M] {f g : X → M},
  HasCompactSupport f → HasCompactSupport g → HasCompactSupport (f ⊔ g)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), a ≠ 0 → (Polynomial.C a * Polynomial.X ^ n).natDegree = n
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- Reinterpret a `NonUnitalSubalgebra` as a `NonUnitalSubsemiring`.  -/
NonUnitalSubalgebra.toNonUnitalSubsemiring : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : Module R A] → NonUnitalSubalgebra R A → NonUnitalSubsemiring A
-- Init.Grind.Offset
Lean.Grind.Nat.lo_ro_2 : ∀ (u w v k₁ k₂ : ℕ), u + k₁ ≤ w → w ≤ v + k₂ → u ≤ v + (k₂ - k₁)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.map.congr_simp : ∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : FunLike F (Polynomial R) (Polynomial S)] [inst_3 : MonoidHomClass F (Polynomial R) (Polynomial S)]
  (φ φ_1 : F) (e_φ : φ = φ_1)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))),
  RatFunc.map φ hφ = RatFunc.map φ_1 ⋯
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.isoMap.congr_simp : ∀ {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] {F : CategoryTheory.Functor J C} {i₀ i₀_1 : J} (e_i₀ : i₀ = i₀_1)
  (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ φ_1 : i ⟶ j),
  φ = φ_1 → ∀ (hφ : Nonempty (j ⟶ i₀)), h.isoMap φ hφ = ⋯.isoMap φ_1 ⋯
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
/-- If `g` is an orientation-preserving map,
then the fixed points of its action on the upper half-plane
can be found from a quadratic equation.

If `c ≠ 0`, then this equation has a unique solution in the upper half-plane
given by `UpperHalfPlane.fixedPt`.
If `c = 0`, then the equation degenerates to a linear equation,
which has no solutions in the upper half-plane unless `g` is a scalar matrix.

See also `Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff`
for a similar lemma about the action on the projective line,
encoded as `OnePoint R`, where `R` is the ring of coefficients.
 -/
UpperHalfPlane.gl_smul_eq_self_iff_quadratic : ∀ {g : GL (Fin 2) ℝ} {z : UpperHalfPlane},
  0 < (↑g).det → (g • z = z ↔ ↑(↑g 1 0) * (↑z * ↑z) + (↑(↑g 1 1) - ↑(↑g 0 0)) * ↑z + -↑(↑g 0 1) = 0)
-- Mathlib.Algebra.Tropical.Basic
Tropical.add_pow : ∀ {R : Type u} [inst : LinearOrder R] [inst_1 : AddMonoid R] [AddLeftMono R] [AddRightMono R] (x y : Tropical R)
  (n : ℕ), (x + y) ^ n = x ^ n + y ^ n
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.face_univ : ∀ (n : ℕ), SSet.stdSimplex.face Finset.univ = ⊤
-- Mathlib.Order.Category.Frm
Frm.Iso.mk_inv : ∀ {α β : Frm} (e : ↑α ≃o ↑β),
  (Frm.Iso.mk e).inv = Frm.ofHom { toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.isAddUnit_mul : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  {A B : Matrix n n R} {d : n → R}, A * B = Matrix.diagonal d → ∀ (i j k : n), i ≠ j → IsAddUnit (A i k * B k j)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.SMulMemClass.toAddAction.eq_1 : ∀ {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] {A : Type u_1} [inst_2 : SetLike A M]
  [hA : VAddMemClass A R M] (S' : A),
  SubAddAction.SMulMemClass.toAddAction S' = Function.Injective.addAction Subtype.val ⋯ ⋯
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.Minpoly.toAdjoin.surjective : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S),
  Function.Surjective ⇑(AdjoinRoot.Minpoly.toAdjoin R x)
-- Mathlib.Analysis.Calculus.LHopital
/-- **L'Hôpital's rule** for approaching a real, `deriv` version  -/
deriv.lhopital_zero_nhds : ∀ {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in nhds a, DifferentiableAt ℝ f x) →
    (∀ᶠ (x : ℝ) in nhds a, deriv g x ≠ 0) →
      Filter.Tendsto f (nhds a) (nhds 0) →
        Filter.Tendsto g (nhds a) (nhds 0) →
          Filter.Tendsto (fun x => deriv f x / deriv g x) (nhds a) l →
            Filter.Tendsto (fun x => f x / g x) (nhdsWithin a {a}ᶜ) l
-- Mathlib.Order.OrderIsoNat
exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le : ∀ {α : Type u_2} [inst : PartialOrder α] [wfl : WellFoundedLT α] [wfg : WellFoundedGT α] {x y : α},
  x ≤ y → ∃ a, a 0 = x ∧ ∃ n, a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)
-- Lean.Widget.InteractiveGoal
/-- In the infoview, if multiple hypotheses `h₁`, `h₂` have the same type `α`, they are rendered
as `h₁ h₂ : α`. We call this a 'hypothesis bundle'. We use `none` instead of `some false` for
booleans to save space in the json encoding.  -/
Lean.Widget.InteractiveHypothesisBundle : Type
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ D` creates finite limits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates finite
colimits.  -/
CategoryTheory.Limits.createsFiniteColimitsOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.CreatesFiniteLimits F] → CategoryTheory.Limits.CreatesFiniteColimits F.op
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.NullMeasurableSet.fundamentalFrontier : ∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α) [Countable G]
  [inst_3 : MeasurableSpace α] [MeasurableConstSMul G α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.SMulInvariantMeasure G α μ],
  MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet (MeasureTheory.fundamentalFrontier G s) μ