mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.mapDomainLinearEquiv_trans : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (e₁ : M ≃ N) (e₂ : N ≃ O),
  AddMonoidAlgebra.mapDomainLinearEquiv R S (e₁.trans e₂) =
    AddMonoidAlgebra.mapDomainLinearEquiv R S e₁ ≪≫ₗ AddMonoidAlgebra.mapDomainLinearEquiv R S e₂
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instTop.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenSubgroup.instTop = { top := { toSubgroup := ⊤, isOpen' := ⋯ } }
-- Mathlib.Data.Finset.NAry
Finset.image₂_inter_subset_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α} {t : Finset β}
  [inst_1 : DecidableEq α], Finset.image₂ f (s ∩ s') t ⊆ Finset.image₂ f s t ∩ Finset.image₂ f s' t
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.containsThenInsert_fst : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.containsThenInsert k v).1 = t.contains k
-- Mathlib.Order.Sublattice
Sublattice.coe_subtype : ∀ {α : Type u_2} [inst : Lattice α] (L : Sublattice α), ⇑L.subtype = Subtype.val
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.updateBucket : {α : Type u} →
  {β : α → Type v} →
    [Hashable α] →
      (self : Array (Std.DHashMap.Internal.AssocList α β)) →
        0 < self.size →
          α →
            (Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β) →
              Array (Std.DHashMap.Internal.AssocList α β)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.empty_equiv_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m.WF → (∅.Equiv m ↔ m.isEmpty = true)
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.smulLeft_eq : ∀ {M : Type u_4} [inst : AddCommMonoid M] {R : Type u_9} [inst_1 : CommSemiring R] [inst_2 : Module R M] (α : R)
  (hα : autoParam (α ∈ Set.center R) Module.End.smulLeft_eq._auto_1), Module.End.smulLeft α hα = α • LinearMap.id
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_diag : ∀ {α : Type u_1} {m : MeasurableSpace α}, Measurable Function.diag
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_succ' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (h : autoParam (n + i = m) CategoryTheory.SimplicialObject.σ₀Iter_succ'._auto_1),
  X.σ₀Iter (i + 1) ⋯ = CategoryTheory.CategoryStruct.comp (X.σ₀Iter i h) (X.σ 0)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_monotone : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ (a : α) (seq : ℕ → ℚ),
      Monotone seq →
        Filter.Tendsto seq Filter.atTop Filter.atTop →
          Filter.Tendsto (fun m => ∫ (c : β), f (a, c) (seq m) ∂ν a) Filter.atTop (nhds ((ν a).real Set.univ))
-- Mathlib.Order.Interval.Set.ProjIcc
StrictMono.strictMonoOn_IccExtend : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} (h : a ≤ b)
  {f : ↑(Set.Icc a b) → β}, StrictMono f → StrictMonoOn (Set.IccExtend h f) (Set.Icc a b)
-- Mathlib.GroupTheory.MonoidLocalization.Away
Localization.Away.monoidOf.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] (x : M),
  Localization.Away.monoidOf x = Localization.monoidOf (Submonoid.powers x)
-- Aesop.RuleSet
Aesop.LocalRuleSet.applicableUnsafeRulesWith : Aesop.LocalRuleSet →
  Aesop.ForwardRuleMatches →
    Lean.MVarId → (Aesop.UnsafeRule → Bool) → Aesop.BaseM (Array (Aesop.IndexMatchResult Aesop.UnsafeRule))
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_add : ∀ {R : Type u_1} {inst : Semiring R} [self : ValuativeRel R] {x y z : R}, x ≤ᵥ z → y ≤ᵥ z → x + y ≤ᵥ z
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicator.coeFn_eq_comp : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α),
  ⇑(thickenedIndicator δ_pos E) = ENNReal.toNNReal ∘ thickenedIndicatorAux δ E
-- Init.Data.Int.Order
Int.neg_lt_iff : ∀ {x y : ℤ}, -x < y ↔ -y < x
-- Lean.Data.AssocList
Lean.AssocList.find? : {α : Type u} → {β : Type v} → [BEq α] → α → Lean.AssocList α β → Option β
-- Aesop.Forward.State
/-- Erase a hypothesis from the cluster state's variable map.  -/
Aesop.ClusterState.eraseHyp : Lean.FVarId → Aesop.PremiseIndex → Aesop.ClusterState → Aesop.ClusterState
-- Mathlib.Control.Bitraversable.Instances
instLawfulBitraversableBicomprOfLawfulTraversable : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] (F : Type u → Type u) [inst_1 : Traversable F]
  [LawfulTraversable F] [LawfulBitraversable t], LawfulBitraversable (Function.bicompr F t)
-- Mathlib.Topology.Order
continuous_sInf_rng : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {T : Set (TopologicalSpace β)},
  Continuous f ↔ ∀ t ∈ T, Continuous f
-- Aesop.Tree.Data
Aesop.GoalUnsafe.brecOn_7.eq : ∀ {motive_1 : Aesop.GoalUnsafe → Sort u} {motive_2 : Aesop.MVarClusterUnsafe → Sort u}
  {motive_3 : Aesop.RappUnsafe → Sort u} {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u}
  {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u}
  {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u}
  {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} (t : Array (IO.Ref Aesop.MVarClusterUnsafe))
  (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t) (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t)
  (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  Aesop.GoalUnsafe.brecOn_7 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_10 t (Aesop.GoalUnsafe.brecOn_7.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The left-associated triple tensor product as a functor.  -/
CategoryTheory.MonoidalCategory.leftAssocTensor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor (C × C × C) C
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixedPoints_subgroup_antitone : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α],
  Antitone fun P => MulAction.fixedPoints (↥P) α
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.lapply_comp_lsingle_of_ne : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i i' : ι),
  i ≠ i' → DFinsupp.lapply i ∘ₗ DFinsupp.lsingle i' = 0
-- Init.Data.UInt.Bitwise
UInt8.zero_shiftRight : ∀ {a : UInt8}, 0 >>> a = 0
-- Init.Data.Vector.Extract
Vector.extract_append_right : ∀ {α : Type u_1} {n m i : ℕ} {xs : Vector α n} {ys : Vector α m},
  (xs ++ ys).extract n (n + i) = Vector.cast ⋯ (ys.extract 0 i)
-- Mathlib.Topology.MetricSpace.Completion
/-- Elements of the uniformity (defined generally for completions) can be characterized in terms
of the distance.  -/
UniformSpace.Completion.mem_uniformity_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set (UniformSpace.Completion α × UniformSpace.Completion α)),
  s ∈ uniformity (UniformSpace.Completion α) ↔ ∃ ε > 0, ∀ {a b : UniformSpace.Completion α}, dist a b < ε → (a, b) ∈ s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_of_lt_one_of_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightStrictMono α] {a b c : α},
  a < 1 → b ≤ c → a * b < c
-- Init.Omega.LinearCombo
/-- Multiplication of two linear combinations.
This is useful only if at least one of the linear combinations is constant,
and otherwise should be considered as a junk value.
 -/
Lean.Omega.LinearCombo.mul : Lean.Omega.LinearCombo → Lean.Omega.LinearCombo → Lean.Omega.LinearCombo
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextDocumentItem : Lean.ToJson Lean.Lsp.TextDocumentItem
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }).obj}
  {hom :
    (i₁ i₂ : ι) → obj i₁ ⟶ (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj (obj i₂))}
  {counit :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (hom i i) ((F.map (f i).op.toLoc).adj.counit.toNatTrans.app (obj i)) =
          CategoryTheory.CategoryStruct.id (obj i))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit._autoParam}
  {coassoc :
    autoParam
      (∀ (i₁ i₂ i₃ : ι),
        CategoryTheory.CategoryStruct.comp (hom i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom i₂ i₃))) =
          CategoryTheory.CategoryStruct.comp (hom i₁ i₃)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map
              ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app ((F.map (f i₃).op.toLoc).r.toFunctor.1 (obj i₃)))))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc._autoParam}
  {obj_1 : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }).obj}
  {hom_1 :
    (i₁ i₂ : ι) →
      obj_1 i₁ ⟶ (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj (obj_1 i₂))}
  {counit_1 :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (hom_1 i i) ((F.map (f i).op.toLoc).adj.counit.toNatTrans.app (obj_1 i)) =
          CategoryTheory.CategoryStruct.id (obj_1 i))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit._autoParam}
  {coassoc_1 :
    autoParam
      (∀ (i₁ i₂ i₃ : ι),
        CategoryTheory.CategoryStruct.comp (hom_1 i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom_1 i₂ i₃))) =
          CategoryTheory.CategoryStruct.comp (hom_1 i₁ i₃)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map
              ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app ((F.map (f i₃).op.toLoc).r.toFunctor.1 (obj_1 i₃)))))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc._autoParam},
  { obj := obj, hom := hom, counit := counit, coassoc := coassoc } =
      { obj := obj_1, hom := hom_1, counit := counit_1, coassoc := coassoc_1 } →
    obj = obj_1 ∧ hom ≍ hom_1
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instWeakEquivalenceSndOfIsStableUnderBaseChangeTrivialFibrationsOfFibration : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithFibrations C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [(HomotopicalAlgebra.trivialFibrations C).IsStableUnderBaseChange]
  [HomotopicalAlgebra.Fibration f] [HomotopicalAlgebra.WeakEquivalence f],
  HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.instBoundedSpace : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Finite ↑𝔖] [inst_1 : PseudoMetricSpace β]
  [inst_2 : BoundedSpace β], BoundedSpace (UniformOnFun α β 𝔖)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
isQuasiregular_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] {x : R}, IsQuasiregular x ↔ ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Given binary fans `sXY` over `X Y`, and `sYZ` over `Y Z`, and `s` over `X sYZ.X`,
if `sYZ` is a limit cone we can construct a binary fan over `sXY.X Z`.

This is an ingredient of building the associator for a Cartesian category.  -/
CategoryTheory.Limits.BinaryFan.assocInv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {sXY : CategoryTheory.Limits.BinaryFan X Y} →
        {sYZ : CategoryTheory.Limits.BinaryFan Y Z} →
          CategoryTheory.Limits.IsLimit sXY →
            CategoryTheory.Limits.BinaryFan X sYZ.pt → CategoryTheory.Limits.BinaryFan sXY.pt Z
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
norm_cfcₙHom : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A)
  (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) (ha : autoParam (p a) norm_cfcₙHom._auto_1), ‖(cfcₙHom ⋯) f‖ = ‖f‖
-- Mathlib.Order.LiminfLimsup
Filter.limsup_eq_sInf_sSup : ∀ {ι : Type u_6} {R : Type u_7} (F : Filter ι) [inst : CompleteLattice R] (a : ι → R),
  Filter.limsup a F = sInf ((fun I => sSup (a '' I)) '' F.sets)
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.toUnconditionalSchauderBasis_basis : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (a : ι), ↑b.toUnconditionalSchauderBasis a = b a
-- Batteries.Linter.UnnecessarySeqFocus
/-- The `multigoal` attribute keeps track of tactics that operate on multiple goals,
meaning that `tac` acts differently from `focus tac`. This is used by the
'unnecessary `<;>`' linter to prevent false positives where `tac <;> tac'` cannot
be replaced by `(tac; tac')` because the latter would expose `tac` to a different set of goals.
 -/
Batteries.Linter.UnnecessarySeqFocus.multigoalAttr : Lean.TagAttributeExtra
-- Mathlib.MeasureTheory.Measure.Haar.Disintegration
/-- To check that a property holds almost everywhere with respect to an additive Haar measure, it
suffices to check it almost everywhere along all translates of a given vector subspace. This is an
instance of a disintegration argument for additive Haar measures.  -/
MeasureTheory.ae_mem_of_ae_add_linearMap_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : MeasurableSpace E] [BorelSpace E] [inst_5 : NormedSpace 𝕜 E]
  [inst_6 : NormedAddCommGroup F] [inst_7 : MeasurableSpace F] [BorelSpace F] [inst_9 : NormedSpace 𝕜 F] (L : E →ₗ[𝕜] F)
  (μ : MeasureTheory.Measure E) (ν : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure]
  [LocallyCompactSpace E] [LocallyCompactSpace F] {s : Set F},
  MeasurableSet s → (∀ (y : F), ∀ᵐ (x : E) ∂μ, y + L x ∈ s) → ∀ᵐ (y : F) ∂ν, y ∈ s
-- Mathlib.Control.Bitraversable.Instances
/-- The bitraverse function for `bicompl`.  -/
Bicompl.bitraverse : {t : Type u → Type u → Type u} →
  [Bitraversable t] →
    (F G : Type u → Type u) →
      [Traversable F] →
        [Traversable G] →
          {m : Type u → Type u} →
            [Applicative m] →
              {α β α' β' : Type u} →
                (α → m β) → (α' → m β') → Function.bicompl t F G α α' → m (Function.bicompl t F G β β')
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.JPDecl.mk : Lean.Name → Array (Lean.Elab.Term.Do.Var × Bool) → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.JPDecl
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.RepToAction_map_hom : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] {X Y : Rep.{w, u, v} k G} (f : X ⟶ Y),
  ((Rep.RepToAction k G).map f).hom = Rep.Hom.toModuleCatHom f
-- Batteries.Recycling.RBTree.Basic
/-- Finds an element in the tree satisfying the `cut` function.  -/
RBTree.RBNode.find? : {α : Type u_1} → (α → Ordering) → RBTree.RBNode α → Option α
-- Mathlib.Data.List.Defs
List.headI_nil : ∀ {α : Type u_1} [inst : Inhabited α], [].headI = default
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ExtendTarget.vec : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {newWidth : ℕ} → (self : aig.ExtendTarget newWidth) → aig.RefVec self.w
-- Mathlib.Logic.Function.Iterate
Function.iterate_commute : ∀ {α : Type u} (m n : ℕ), Function.Commute (fun f => f^[m]) fun f => f^[n]
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the angle between three points is `π / 2`, the last two points are not equal.  -/
EuclideanGeometry.right_ne_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → p₃ ≠ p₂
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_eq_foldl : ∀ {M : Type u_3} [inst : CommMonoid M] (s : Multiset M), s.prod = Multiset.foldl (fun x1 x2 => x1 * x2) 1 s
-- Mathlib.MeasureTheory.Group.Arithmetic
AddOpposite.instMeasurableSpace : {α : Type u_2} → [h : MeasurableSpace α] → MeasurableSpace αᵃᵒᵖ
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
Lean.Meta.RefinedDiscrTree.PreDiscrTree.mk : {α : Type} →
  Std.HashMap Lean.Meta.RefinedDiscrTree.Key ℕ →
    Array (Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α)) → Lean.Meta.RefinedDiscrTree.PreDiscrTree α
-- Init.Data.Int.Order
Int.sign.eq_2 : (Int.ofNat 0).sign = 0
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bddAbove_iff_small : ∀ {s : Set Ordinal.{u}}, BddAbove s ↔ Small.{u, u + 1} ↑s
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.neg_eq_self : ∀ {G : Type u_1} [inst : AddGroup G] [IsAddKleinFour G] (x : G), -x = x
-- Mathlib.Topology.Homeomorph.Lemmas
Topology.IsOpenEmbedding.uliftMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsOpenEmbedding f → Topology.IsOpenEmbedding (ULift.map f)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.coe_restrictScalars : ∀ (R : Type u) {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂] {A : Type u_1}
  [inst_7 : Semiring A] [inst_8 : SMul R A] [inst_9 : (i : ι) → Module A (M₁ i)] [inst_10 : Module A M₂]
  [inst_11 : ∀ (i : ι), IsScalarTower R A (M₁ i)] [inst_12 : IsScalarTower R A M₂]
  (f : ContinuousMultilinearMap A M₁ M₂), ⇑(ContinuousMultilinearMap.restrictScalars R f) = ⇑f
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.φ_of_lt : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d) (i : Fin (d + 2)) (hi : i < (SSet.prodStdSimplex.pairingCore.min x hd).castSucc),
  SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd i = (SSet.prodStdSimplex.objEquiv (x.cast hd).simplex) (i.castPred ⋯)
-- Mathlib.Data.TypeVec
TypeVec.prod.mk.eq_2 : ∀ (n : ℕ) (x_4 x_5 : TypeVec.{u} n.succ), TypeVec.prod.mk Fin2.fz = Prod.mk
-- Mathlib.CategoryTheory.Square
/-- the bottom-right morphism  -/
CategoryTheory.Square.Hom.τ₄ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {sq₁ sq₂ : CategoryTheory.Square C} → sq₁.Hom sq₂ → (sq₁.X₄ ⟶ sq₂.X₄)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabRoc : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.RepresentationTheory.Tannaka
/-- The `FDRep k G` morphism induced by multiplication on `G → k`.  -/
TannakaDuality.FiniteGroup.mulRepHom : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Finite G] →
        CategoryTheory.MonoidalCategoryStruct.tensorObj TannakaDuality.FiniteGroup.rightFDRep
            TannakaDuality.FiniteGroup.rightFDRep ⟶
          TannakaDuality.FiniteGroup.rightFDRep
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.AddGrp C} {f g : A ⟶ B}, f = g ↔ f.hom.hom = g.hom.hom
-- Mathlib.RingTheory.IntegralClosure.Algebra.Defs
/-- An algebra is integral if every element of the extension is integral over the base ring.  -/
Algebra.IsIntegral : (R : Type u_1) → (A : Type u_3) → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → Prop
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.instCommGroup : {d : ℤ} → CommGroup (Pell.Solution₁ d)
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticOn.zpow_nonneg`

---

ZPowers of analytic functions (into a normed division algebra over `𝕜`) are analytic if the
exponent is nonnegative.  -/
AnalyticOn.fun_zpow_nonneg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {s : Set E} {n : ℤ}, AnalyticOn 𝕜 f s → 0 ≤ n → AnalyticOn 𝕜 (fun i => f i ^ n) s
-- Init.Data.List.MapIdx
List.mapIdx_append : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {xs ys : List α},
  List.mapIdx f (xs ++ ys) = List.mapIdx f xs ++ List.mapIdx (fun i => f (i + xs.length)) ys