mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_fun_sub : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E],
  ProbabilityTheory.IsGaussianProcess X P → ∀ {s t : T}, ProbabilityTheory.HasGaussianLaw (fun ω => X s ω - X t ω) P
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- The (colimit) cofork expressing `π₀ X` as a coequalizer
of `X.δ 0 : X _⦋1⦌ → X _⦋0⦌` and `X.δ 1`.  -/
SSet.coforkπ₀ : {X : SSet} →
  CategoryTheory.Limits.Cofork (CategoryTheory.SimplicialObject.δ X 1) (CategoryTheory.SimplicialObject.δ X 0)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.all_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {p : β → Bool},
  Std.IterM.all p it = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' x => if p x = true then Std.IterM.all p it' else pure { down := false }
      | Std.IterStep.skip it' => Std.IterM.all p it'
      | Std.IterStep.done => pure { down := true }
-- Batteries.Recycling.RBTree.WF
RBTree.RBMap.Imp.instIsMonotoneProdByKeyFstMapSnd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (cmp : α → α → Ordering) (f : α → β → γ),
  RBTree.RBNode.IsMonotone (Ordering.byKey Prod.fst cmp) (Ordering.byKey Prod.fst cmp) (RBTree.RBMap.Imp.mapSnd f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DTreeMap.Raw.Const.get! (m₁ \ m₂) k = default
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure.eq_1 : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G),
  μ.outerMeasure = MeasureTheory.inducedOuterMeasure (fun U hU => μ.innerContent { carrier := U, is_open' := hU }) ⋯ ⋯
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Ioc_pred_right_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] {a b : α},
  a < b → insert b (Finset.Ioc a (Order.pred b)) = Finset.Ioc a b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.foldM_eq_foldlM_toList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'],
  m.WF →
    ∀ {f : δ → (a : α) → β a → m' δ} {init : δ},
      Std.DHashMap.Raw.foldM f init m = List.foldlM (fun a b => f a b.fst b.snd) init m.toList
-- Batteries.Data.Random.MersenneTwister
/-- Data for current state.  -/
Batteries.Random.MersenneTwister.State.data : {cfg : Batteries.Random.MersenneTwister.Config} →
  Batteries.Random.MersenneTwister.State cfg → Vector (BitVec cfg.wordSize) cfg.stateSize
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
/-- For each nonempty, directed set `s` which is bounded below, `sInf s` is
the greatest lower bound of `s`.  -/
ConditionallyCompletePartialOrder.isGLB_csInf_of_directed : ∀ {α : Type u_3} [self : ConditionallyCompletePartialOrder α] (s : Set α),
  DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelZeroIsoSource.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C},
  CategoryTheory.Limits.kernelZeroIsoSource = CategoryTheory.Limits.equalizer.isoSourceOfSelf 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonHover.fromJson : Lean.Json → Except String Lean.Lsp.Hover
-- Mathlib.Algebra.Order.Hom.Basic
RingNormClass.toRingSeminormClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : NonUnitalNonAssocRing α}
  {inst_1 : Semiring β} {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : RingNormClass F α β],
  RingSeminormClass F α β
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.derivWithin_le_slope : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f S y → derivWithin f S y ≤ slope f x y
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.smulLeftCLM_sub : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F] {g₁ g₂ : E → ℂ},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      TemperedDistribution.smulLeftCLM F (g₁ - g₂) =
        TemperedDistribution.smulLeftCLM F g₁ - TemperedDistribution.smulLeftCLM F g₂
-- Mathlib.CategoryTheory.MarkovCategory.Positive
CategoryTheory.PositiveCategory.instDeterministicOfIsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.PositiveCategory C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  CategoryTheory.Deterministic f
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.ext_iff : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] {f g : M₁ →SL[σ₁₂] M₂},
  f = g ↔ ∀ (x : M₁), f x = g x
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.sinPoly.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((n : ℕ) → motive n.succ.succ) → motive x
-- Mathlib.Order.Ideal
Order.Ideal.directed : ∀ {P : Type u_1} [inst : LE P] (s : Order.Ideal P), DirectedOn (fun x1 x2 => x1 ≤ x2) ↑s
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.sumComm_symm : ∀ (X : Type u) (Y : Type v) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  (Homeomorph.sumComm X Y).symm = Homeomorph.sumComm Y X
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instSubsingleton : ∀ {R : Type u_1} {a b : R} [Subsingleton R], Subsingleton (QuadraticAlgebra R a b)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.lt_nfpFamily_iff : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι] {a b : Ordinal.{u}},
  a < Ordinal.nfpFamily f b ↔ ∃ l, a < List.foldr f b l
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.toAddSubgroup_mono : ∀ {R : Type u} [inst : NonAssocRing R], Monotone Subring.toAddSubgroup
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.μIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C),
  (CategoryTheory.Functor.Monoidal.μIso F X Y).inv = CategoryTheory.Functor.OplaxMonoidal.δ F X Y
-- Mathlib.Data.TypeVec
/-- `prod α β` is the pointwise product of the components of `α` and `β`  -/
MvFunctor.«term_⊗_» : Lean.TrailingParserDescr
-- Std.Internal.Do.WP.Conjunctive
Std.Internal.Do.WPConjunctive.mk : ∀ {Prog : Type u} {Value : outParam (Type v)} {Pred : outParam (Type w)} {EPred : outParam (Type z)}
  [inst : Std.Internal.Do.Assertion Pred] [inst_1 : Std.Internal.Do.Assertion EPred]
  [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred],
  (∀ (x : Prog) (Q₁ Q₂ : Value → Pred) (E : EPred),
      Lean.Order.PartialOrder.rel (Lean.Order.meet (Std.Internal.Do.wp x Q₁ E) (Std.Internal.Do.wp x Q₂ E))
        (Std.Internal.Do.wp x (Lean.Order.meet Q₁ Q₂) E)) →
    Std.Internal.Do.WPConjunctive Prog Value Pred EPred
-- Mathlib.Tactic.Finiteness
/-- `finiteness` proves goals of the form `*** < ∞` and (equivalently) `*** ≠ ∞` in the extended
nonnegative reals (`ℝ≥0∞`). If the goal cannot be proven, `finiteness` prints a warning and shows
its intermediate progress.

This tactic is based on `aesop`. It calls `assumption`, `intros`, `positivity`, and any
lemma or rule added to the `finiteness` ruleset, except that all `simp` rules are disabled.

This tactic is extensible. By adding more rules, `finiteness` can prove more goals. For example:
* `@[aesop (rule_sets := [finiteness]) safe 50] lemma ...`
* `add_aesop_rules safe tactic (rule_sets := [finiteness]) (by ...)`

(Note that a `simp` rule cannot be added this way, since all `simp` rules are disabled.)

* `finiteness (clause)` customizes the `aesop` call using the given clause. See `aesop`
  documentation for detailed explanation. Note that `finiteness` disables `simp`, so
  `finiteness (add simp [lemma1, lemma2])` does not do anything more than a bare `finiteness`.
* `finiteness [t₁, ..., tₙ]` adds the terms `t₁`, ..., `tₙ` as local hypotheses before applying
  the search rules.
* `finiteness?` additionally shows the proof that `finiteness` found.
* `finiteness_nonterminal` is a version of `finiteness` that does not report a warning if it fails
  to close the goal.
 -/
finiteness? : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.CompStruct.d₀ : ∀ {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : SSet.Edge x₀ x₁} {e₁₂ : SSet.Edge x₁ x₂}
  {e₀₂ : SSet.Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) h.simplex = e₁₂.edge
-- Init.Data.UInt.Lemmas
USize.toUInt32_toUInt64 : ∀ (n : USize), n.toUInt64.toUInt32 = n.toUInt32
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.SigmaHom.mk.inj : ∀ {I : Type w₁} {C : I → Type u₁} {inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)} {i : I} {X Y : C i}
  {a a_1 : X ⟶ Y}, CategoryTheory.Sigma.SigmaHom.mk a = CategoryTheory.Sigma.SigmaHom.mk a_1 → a = a_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_left_le_size_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₁.size ≤ (m₁ ∪ m₂).size
-- Mathlib.Geometry.Euclidean.Triangle
/-- A variant of the law of sines, requiring that the points not be collinear.  -/
EuclideanGeometry.dist_eq_dist_mul_sin_angle_div_sin_angle : ∀ {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₃ : P},
  ¬Collinear ℝ {p₁, p₂, p₃} →
    dist p₁ p₂ = dist p₃ p₁ * Real.sin (EuclideanGeometry.angle p₂ p₃ p₁) / Real.sin (EuclideanGeometry.angle p₁ p₂ p₃)
-- Mathlib.InformationTheory.Hamming
Hamming.instAddGroup : {ι : Type u_2} → {β : ι → Type u_3} → [(i : ι) → AddGroup (β i)] → AddGroup (Hamming β)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_coe : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) {x : M}, x ∈ ↑N ↔ x ∈ N
-- Batteries.Data.List.Basic
List.IsChain.below.cons_cons : ∀ {α : Type u_1} {R : α → α → Prop} {motive : (a : List α) → List.IsChain R a → Prop} {a b : α} {l : List α}
  (hr : R a b) (h : List.IsChain R (b :: l)), List.IsChain.below h → motive (b :: l) h → List.IsChain.below ⋯
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.liftRight.eq_1 : ∀ {M : Type u} {N : Type v} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N) (g : M → AddUnits N)
  (h : ∀ (x : M), ↑(g x) = f x), AddUnits.liftRight f g h = { toFun := g, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toArray_zip_of_finite_left : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂] {it₁ : Std.Iter β₁}
  {it₂ : Std.Iter β₂} [Std.Iterators.Finite α₁ Id] [Std.Iterators.Productive α₂ Id],
  (it₁.zip it₂).toArray = it₁.toArray.zip (Std.Iter.take it₁.toArray.size it₂).toArray
-- Lean.Linter.UnusedVariables
Lean.Linter.UnusedVariables.References.mk.sizeOf_spec : ∀ (constDecls : Std.HashSet Lean.Syntax.Range)
  (fvarDefs : Std.HashMap Lean.Syntax.Range Lean.Linter.UnusedVariables.FVarDefinition)
  (fvarUses : Std.HashSet Lean.FVarId) (fvarAliases : Std.HashMap Lean.FVarId Lean.FVarId)
  (assignments : Array (Lean.PersistentHashMap Lean.MVarId Lean.Expr)),
  sizeOf
      { constDecls := constDecls, fvarDefs := fvarDefs, fvarUses := fvarUses, fvarAliases := fvarAliases,
        assignments := assignments } =
    1 + sizeOf constDecls + sizeOf fvarDefs + sizeOf fvarUses + sizeOf fvarAliases + sizeOf assignments
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.Hom.ext : ∀ {R S : CommSemiRingCat} {x y : R.Hom S}, x.hom' = y.hom' → x = y
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rcc.toList_iter : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rcc α}, r.iter.toList = r.toList
-- Mathlib.Logic.Equiv.Sum
/-- `Bool` is equivalent the sum of two `PUnit`s.  -/
Equiv.boolEquivPUnitSumPUnit : Bool ≃ PUnit.{u + 1} ⊕ PUnit.{v + 1}
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
ContinuousFunctionalCalculus.toNonUnital : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [ContinuousFunctionalCalculus R A p],
  NonUnitalContinuousFunctionalCalculus R A p
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- Constructor for isomorphisms in the category `LaxBraidedFunctor C D`.  -/
CategoryTheory.LaxBraidedFunctor.isoMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F G : CategoryTheory.LaxBraidedFunctor C D} →
                  (e : F.toFunctor ≅ G.toFunctor) → [CategoryTheory.NatTrans.IsMonoidal e.hom] → F ≅ G
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_two : Nat.Prime 2
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- If a localizer morphism induces an equivalence on some choice of localized categories,
it will be so for any choice of localized categories.  -/
CategoryTheory.LocalizerMorphism.isEquivalence_imp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂]
  (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'}
  [inst_7 : CategoryTheory.Category.{v₄', u₄'} D₁'] [inst_8 : CategoryTheory.Category.{v₅', u₅'} D₂']
  (L₁' : CategoryTheory.Functor C₁ D₁') (L₂' : CategoryTheory.Functor C₂ D₂') [L₁'.IsLocalization W₁]
  [L₂'.IsLocalization W₂] (G' : CategoryTheory.Functor D₁' D₂') [CategoryTheory.CatCommSq Φ.functor L₁' L₂' G']
  [G.IsEquivalence], G'.IsEquivalence
-- Mathlib.Algebra.Group.TypeTags.Basic
ofAdd_eq_one : ∀ {A : Type u_1} [inst : Zero A] {x : A}, Multiplicative.ofAdd x = 1 ↔ x = 0
-- Mathlib.Analysis.Normed.Module.Span
LinearMap.toSpanSingleton_homothety : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [NormSMulClass 𝕜 E] (x : E) (c : 𝕜), ‖(LinearMap.toSpanSingleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖
-- Mathlib.Data.WSeq.Basic
/-- Turn a sequence into a weak sequence  -/
Stream'.WSeq.ofSeq : {α : Type u} → Stream'.Seq α → Stream'.WSeq α
-- Mathlib.Analysis.Normed.Order.Hom.Basic
/-- Constructs a `SeminormedAddGroup` structure from an `AddGroupSeminormClass` on an
`AddGroup`.  -/
AddGroupSeminormClass.toSeminormedAddGroup : {F : Type u_1} →
  {α : Type u_2} →
    [inst : FunLike F α ℝ] → [inst_1 : AddGroup α] → [AddGroupSeminormClass F α ℝ] → F → SeminormedAddGroup α
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.getFunWithGivenDomain? : Array Lean.Expr → Lean.Expr → Option Lean.Expr
-- Mathlib.CategoryTheory.Filtered.Final
/-- The diagonal functor on any cofiltered category is initial.  -/
CategoryTheory.Functor.initial_diag_of_isFiltered : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofilteredOrEmpty C],
  (CategoryTheory.Functor.diag C).Initial
-- Mathlib.Topology.Algebra.GroupWithZero
/-- Continuity at a point of the result of dividing two functions continuous at that point, where
the denominator is nonzero.  -/
ContinuousAt.div : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  [ContinuousMul G₀] {f g : α → G₀} [inst_4 : TopologicalSpace α] {a : α},
  ContinuousAt f a → ContinuousAt g a → g a ≠ 0 → ContinuousAt (f / g) a
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.sup_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Max β] (f g : MeasureTheory.SimpleFunc α β)
  (a : α), (f ⊔ g) a = f a ⊔ g a
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The lower part of the first column of the snake diagram is exact.  -/
CategoryTheory.ShortComplex.SnakeInput.exact_C₁_down : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  { X₁ := S.L₁.X₁, X₂ := S.L₂.X₁, X₃ := S.L₃.X₁, f := S.v₁₂.τ₁, g := S.v₂₃.τ₁, zero := ⋯ }.Exact
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddCommMonoidWithOne : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [AddCommMonoidWithOne M] → AddCommMonoidWithOne (l.Germ M)
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piScalarRight.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] (ι : Type u_4)
  [inst_7 : Fintype ι] [inst_8 : DecidableEq ι],
  TensorProduct.piScalarRight R S N ι =
    LinearEquiv.ofLinearMap (TensorProduct.piScalarRightHom R S N ι) (TensorProduct.piScalarRightInv R S N ι) ⋯ ⋯
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.isReflection_of_mem_rightInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) {t : W},
  t ∈ cs.rightInvSeq ω → cs.IsReflection t
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.disjoint_def : ∀ {M : Type u_1} [inst : AddZeroClass M] {p₁ p₂ : AddSubmonoid M}, Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 0
-- Mathlib.RingTheory.LaurentSeries
/-- The valuation of a power series is the order of the first non-zero coefficient.  -/
LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero : ∀ (K : Type u_2) [inst : Field K] {d : ℕ} (f : PowerSeries K),
  Valued.v ((HahnSeries.ofPowerSeries ℤ K) f) ≤ WithZero.exp (-↑d) ↔ ∀ n < d, (PowerSeries.coeff n) f = 0
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppImplicitArg.regular.injEq : ∀ (s s_1 : Lean.Term),
  (Lean.PrettyPrinter.Delaborator.AppImplicitArg.regular s =
      Lean.PrettyPrinter.Delaborator.AppImplicitArg.regular s_1) =
    (s = s_1)
-- Mathlib.GroupTheory.OrderOfElement
orderOf_le_of_pow_eq_one : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, 0 < n → x ^ n = 1 → orderOf x ≤ n
-- Mathlib.Algebra.AffineMonoid.Irreducible
/-- Any set `S` inside an additive monoid with a single unit contains the irreducible
elements of the submonoid it generates.  -/
addIrreducible_mem_addSubmonoidClosure_subset : ∀ {M : Type u_1} [inst : AddCommMonoid M] [Subsingleton (AddUnits M)] {S : Set M},
  {p | p ∈ AddSubmonoid.closure S ∧ AddIrreducible p} ⊆ S
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.toLinearMap_tracePositiveLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  (LinearMap.tracePositiveLinearMap 𝕜 E).toLinearMap = LinearMap.trace 𝕜 E
-- Mathlib.Order.Defs.Unbundled
IsPartialOrder.mk : ∀ {α : Sort u_1} {r : α → α → Prop} [toIsPreorder : IsPreorder α r] [toAntisymm : Std.Antisymm r], IsPartialOrder α r
-- Mathlib.Data.FunLike.IsApply
IsAddApply.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Init.Data.Array.Basic
/-- Returns the last element of an array, given a proof that the array is not empty.

See `Array.back!` for the version that panics if the array is empty, or `Array.back?` for the
version that returns an option.
 -/
Array.back : {α : Type u} → (xs : Array α) → autoParam (0 < xs.size) Array.back._auto_1 → α
-- Mathlib.NumberTheory.ZetaValues
periodizedBernoulli.continuous : ∀ {k : ℕ}, k ≠ 1 → Continuous (periodizedBernoulli k)
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.mul_X_divMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x : MvPolynomial σ R) (i : σ),
  ((x * MvPolynomial.X i).divMonomial fun₀ | i => 1) = x
-- Init.Prelude
Dvd.mk : {α : Type u_1} → (α → α → Prop) → Dvd α
-- Mathlib.CategoryTheory.Galois.Decomposition
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.instMonoSelfProdPermIncl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A : C}
  {u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd✝ F X} {a : (F.obj A).obj}
  (h : (CategoryTheory.ConcreteCategory.hom (F.map u)) a = CategoryTheory.PreGaloisCategory.mkSelfProdFib✝ F X)
  [inst_3 : CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.Mono u] (b : (F.obj A).obj),
  CategoryTheory.Mono (CategoryTheory.PreGaloisCategory.selfProdPermIncl✝ h b)
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousAt_iInf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {ι : Sort u_4} {δ : Type u_5} [inst_1 : CompleteLinearOrder δ]
  {f : ι → α → δ}, (∀ (i : ι), UpperSemicontinuousAt (f i) x) → UpperSemicontinuousAt (fun x' => ⨅ i, f i x') x
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_apply' : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : o → Matrix m n α) (i : m) (k : o) (j : n) (k' : o),
  Matrix.blockDiagonal M (i, k) (j, k') = if k = k' then M k i j else 0