mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- Construct a continuous linear map given the value at a finite basis.  -/
Module.Basis.constrL : {𝕜 : Type u} →
  [hnorm : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst : AddCommGroup E] →
        [inst_1 : Module 𝕜 E] →
          [inst_2 : TopologicalSpace E] →
            [IsTopologicalAddGroup E] →
              [ContinuousSMul 𝕜 E] →
                {F : Type w} →
                  [inst_5 : AddCommGroup F] →
                    [inst_6 : Module 𝕜 F] →
                      [inst_7 : TopologicalSpace F] →
                        [IsTopologicalAddGroup F] →
                          [ContinuousSMul 𝕜 F] →
                            [CompleteSpace 𝕜] →
                              {ι : Type u_1} → [Finite ι] → [T2Space E] → Module.Basis ι 𝕜 E → (ι → F) → E →L[𝕜] F
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.sup_def : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  (S T : IntermediateField F E), S ⊔ T = IntermediateField.adjoin F (↑S ∪ ↑T)
-- Mathlib.RingTheory.PowerSeries.Basic
/-- Constructor for formal power series.  -/
PowerSeries.mk : {R : Type u_2} → (ℕ → R) → PowerSeries R
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.pointEquiv_symm_none : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : Nontrivial R]
  [inst_2 : WeierstrassCurve.IsElliptic W'], W'.pointEquiv.symm none = WeierstrassCurve.Affine.Point.zero
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (k, v) ∈ m.toList ↔ m.getKey? k = some k ∧ m[k]? = some v
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
/-- Condition that a topology is generated by 1-hypercovers of size `w`.  -/
CategoryTheory.GrothendieckTopology.IsGeneratedByOneHypercovers : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C → Prop
-- Mathlib.Topology.Algebra.ConstMulAction
continuous_const_smul_iff₀ : ∀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀]
  [inst_2 : MulAction G₀ α] [ContinuousConstSMul G₀ α] [inst_4 : TopologicalSpace β] {f : β → α} {c : G₀},
  c ≠ 0 → ((Continuous fun x => c • f x) ↔ Continuous f)
-- Mathlib.CategoryTheory.Sites.Types
/-- The discrete presieve on a type, which only includes arrows whose domain is a singleton.  -/
CategoryTheory.discretePresieve : (α : Type u) → CategoryTheory.Presieve α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_alter_of_beq_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)}, (k == k') = false → (k' ∈ m.alter k f ↔ k' ∈ m)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {hc : t.minKey! ∈ t}, t.getKey t.minKey! hc = t.minKey!
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioo_of_Ico : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α},
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun i => Set.Ico (a i) (b i)
-- Lean.ResolveName
/-- Adds any macro scopes to `n`, then returns it if it resolves to `n₀` and isn't filtered out.  -/
_private.Lean.ResolveName.0.Lean.unresolveNameGlobal?.tryResolve : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] →
            [Lean.AddMessageContext m] →
              Lean.Name → (Lean.Name → m Bool) → Option Lean.MacroScopesView → Lean.Name → OptionT m Lean.Name
-- Mathlib.Data.EReal.Basic
EReal.toENNReal.eq_1 : ∀ (x : EReal), x.toENNReal = if x = ⊤ then ⊤ else ENNReal.ofReal x.toReal
-- Init.Data.List.Attach
List.unattach_attachWith : ∀ {α : Type u_1} {p : α → Prop} {l : List α} {H : ∀ a ∈ l, p a}, (l.attachWith p H).unattach = l
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.restrict_union : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} {s t : Set Ω},
  Disjoint s t → MeasurableSet t → μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
-- Mathlib.Order.Filter.Bases.Finite
Filter.HasBasis.iInf : ∀ {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop}
  {s : (i : ι) → ι' i → Set α},
  (∀ (i : ι), (l i).HasBasis (p i) (s i)) →
    (⨅ i, l i).HasBasis (fun If => If.fst.Finite ∧ ∀ (i : ↑If.fst), p (↑i) (If.snd i)) fun If => ⋂ i, s (↑i) (If.snd i)
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.iInter : ∀ {R : Type u_1} {X : Type u_2} {ι : Sort u_4} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R X] {x : X} {s : ι → Set X},
  (∀ (i : ι), Convexity.IsStarConvexSet R x (s i)) → Convexity.IsStarConvexSet R x (⋂ i, s i)
-- Init.Prelude
/-- The canonical universe-polymorphic type with just one element.

It should be used in contexts that require a type to be universe polymorphic, thus disallowing
`Unit`.
 -/
PUnit : Sort u
-- Mathlib.Data.ENNReal.Action
ENNReal.coe_smul : ∀ {R : Type u_1} (r : R) (s : NNReal) [inst : SMul R NNReal] [inst_1 : SMul R ENNReal] [IsScalarTower R NNReal NNReal]
  [IsScalarTower R NNReal ENNReal], ↑(r • s) = r • ↑s
-- Std.Data.HashMap.Lemmas
Std.HashMap.keys_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool},
  (Std.HashMap.filter f m).keys.Perm
    (List.filter
        (fun x_2 =>
          match x_2 with
          | ⟨x_3, h'⟩ => f x_3 m[x_3])
        m.keys.attach).unattach
-- Mathlib.Topology.Algebra.ConstMulAction
/-- If a scalar is central, then its right action is continuous when its left action is.  -/
ContinuousConstSMul.op : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α]
  [inst_3 : SMul Mᵐᵒᵖ α] [IsCentralScalar M α], ContinuousConstSMul Mᵐᵒᵖ α
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
_private.Mathlib.Analysis.CStarAlgebra.Module.Constructions.0.WithCStarModule.lipschitzWith_one_equiv_prod_aux : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {E : Type u_2} {F : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : SMul A F] [inst_8 : CStarModule A E] [inst_9 : CStarModule A F]
  [inst_10 : StarOrderedRing A], LipschitzWith 1 ⇑(WithCStarModule.equiv A (E × F))
-- Std.Data.DTreeMap.Raw.Iterator
/-- Returns a finite iterator over the values of a tree map.
The iterator yields the values in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.DTreeMap.Raw.valuesIter : {α β : Type u} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α (fun x => β) cmp → Std.Iter β
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
/-- The identity isometry between equal bilinear forms.  -/
LinearMap.BilinForm.Isometry.ofEq : {R : Type u_1} →
  {M₁ : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M₁] → [inst_2 : Module R M₁] → {B₁ B₂ : LinearMap.BilinForm R M₁} → B₁ = B₂ → B₁ →bᵢ B₂
-- Mathlib.Algebra.Ring.Associator
associator_eq_zero : ∀ {R : Type u_1} [inst : NonUnitalRing R], associator = 0
-- Init.Data.String.Lemmas.FindPos
String.Pos.ofSlice_prev : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {h' : p ≠ (s.slice p₀ p₁ h).startPos},
  String.Pos.ofSlice (p.prev h') = (String.Pos.ofSlice p).prev ⋯
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instBot : {α : Type u_1} → [inst : LE α] → Bot (UpperSet α)
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk_eq_of_le_of_finite_of_flat : ∀ {R : Type uR} (M : Type uM) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M] {p q : PrimeSpectrum R}, p ≤ q → Module.rankAtStalk M p = Module.rankAtStalk M q
-- Lean.Linter.UnusedVariables
/-- Enables or disables unused variable linter warnings in patterns  -/
Lean.Linter.linter.unusedVariables.patternVars : Lean.Option Bool
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- A disequality `lhs ≠ rhs` asserted by the core.  -/
Lean.Meta.Grind.Arith.CommRing.DiseqCnstr : Type
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.SpecMap_residue_apply : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X) (s : ↥(AlgebraicGeometry.Spec (X.residueField x))),
  (AlgebraicGeometry.Spec.map (X.residue x)) s = IsLocalRing.closedPoint ↑(X.presheaf.stalk x)
-- Mathlib.Data.Num.Bitwise
/-- A dependent induction principle for `SNum` which avoids relying on `NzsNum`.  -/
SNum.drec' : {C : SNum → Sort u_1} →
  ((b : Bool) → C (SNum.zero b)) → ((b : Bool) → (p : SNum) → C p → C (SNum.bit b p)) → (p : SNum) → C p
-- Mathlib.FieldTheory.Galois.NormalBasis
AdjoinRoot.powerBasisAux.congr_simp : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K} (hf : f ≠ 0),
  AdjoinRoot.powerBasisAux hf = AdjoinRoot.powerBasisAux hf
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.startsWith_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, s.startsWith pat = true ↔ String.Slice.Pattern.Model.MatchesAt pat s.startPos
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJNe0Or1728.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (j : R),
  WeierstrassCurve.ofJNe0Or1728 j =
    { a₁ := j - 1728, a₂ := 0, a₃ := 0, a₄ := -36 * (j - 1728) ^ 3, a₆ := -(j - 1728) ^ 5 }
-- Init.Data.String.Lemmas.Basic
String.Slice.sliceFrom_startPos : ∀ {s : String.Slice}, s.sliceFrom s.startPos = s
-- Mathlib.MeasureTheory.Measure.Restrict
indicator_ae_eq_of_restrict_compl_ae_eq_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β}
  [inst_1 : Zero β], MeasurableSet s → f =ᵐ[μ.restrict sᶜ] 0 → s.indicator f =ᵐ[μ] f
-- Init.Data.List.Monadic
List.idRun_mapM : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → Id β}, (List.mapM f l).run = List.map (fun x => (f x).run) l
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.forIn_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} {δ : Type w}
  {m : Type w → Type w'} [Std.TransOrd α] [inst : Monad m] [LawfulMonad m],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ},
          Std.DTreeMap.Internal.Impl.forIn f init t₁ = Std.DTreeMap.Internal.Impl.forIn f init t₂
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitLeftOpIsoUnopColimit_inv_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : Jᵒᵖ),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitLeftOpIsoUnopColimit F).inv
      (CategoryTheory.Limits.limit.π F.leftOp j) =
    (CategoryTheory.Limits.colimit.ι F (Opposite.unop j)).unop
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- If `D` is an `R`-algebra, finite as an `R`-module, and if `D` has the module topology,
then multiplication on `D` is automatically continuous.  -/
IsModuleTopology.continuous_mul_of_finite : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] (D : Type u_2)
  [inst_3 : Ring D] [inst_4 : Algebra R D] [Module.Finite R D] [inst_6 : TopologicalSpace D] [IsModuleTopology R D],
  Continuous fun ab => ab.1 * ab.2
-- Init.Data.BitVec.Bitblast
/-- Complete fast overflow detection circuit for unsigned multiplication.
 -/
BitVec.fastUmulOverflow : ∀ {w : ℕ} (x y : BitVec w),
  x.umulOverflow y =
    if hw : w ≤ 1 then false else (BitVec.setWidth (w + 1) x * BitVec.setWidth (w + 1) y)[w] || x.resRec y (w - 1) ⋯ ⋯
-- Mathlib.Algebra.Group.Hom.Instances
ZeroHom.nsmul_apply : ∀ {M : Type uM} {N : Type uN} [inst : Zero M] [inst_1 : AddMonoid N] (f : ZeroHom M N) (n : ℕ) (x : M),
  (n • f) x = n • f x
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
/-- The non-zero divisors of associates of a monoid with zero `M₀` are isomorphic to the associates
of the non-zero divisors of `M₀` under the map `⟨⟦a⟧, _⟩ ↦ ⟦⟨a, _⟩⟧`.  -/
associatesNonZeroDivisorsEquiv : {M₀ : Type u_1} →
  [inst : CommMonoidWithZero M₀] → ↥(nonZeroDivisors (Associates M₀)) ≃* Associates ↥(nonZeroDivisors M₀)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.δ_comp_σ_self_assoc : ∀ {n : ℕ} {i : Fin (n + 1)} {Z : SimplexCategoryGenRel} (h : SimplexCategoryGenRel.mk n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i.castSucc)
      (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ i) h) =
    h
-- Init.Data.SInt.Lemmas
ISize.toInt_toInt64 : ∀ (x : ISize), x.toInt64.toInt = x.toInt
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.sInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : Set (CategoryTheory.MorphismProperty C)},
  (∀ W' ∈ W, W'.IsMultiplicative) → (sInf W).IsMultiplicative
-- Lean.Environment
/-- Starts the asynchronous addition of a constant to the environment. The environment is split into a
"main" branch that holds a reference to the constant to be added but will block on access until the
corresponding information has been added on the "async" environment branch and committed there; see
the respective fields of `AddConstAsyncResult` as well as the [Environment Branches] note for more
information.

`exportedKind?` must be passed if the eventual kind of the constant in the exported constant map
will differ from that of the private version. It must be `none` if the constant will not be
exported.
 -/
Lean.Environment.addConstAsync : Lean.Environment →
  Lean.Name →
    (kind : Lean.ConstantKind) →
      optParam (Option Lean.ConstantKind) (some kind) →
        optParam Bool true → optParam Bool true → IO Lean.Environment.AddConstAsyncResult
-- Init.Data.SInt.Lemmas
Int8.toUInt8_add : ∀ (a b : Int8), (a + b).toUInt8 = a.toUInt8 + b.toUInt8
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.mk : ∀ {α : Type u_1} {m : MeasurableSpace α} {c : MeasureTheory.ComplexMeasure α} {μ : MeasureTheory.Measure α},
  (MeasureTheory.ComplexMeasure.re c).HaveLebesgueDecomposition μ →
    (MeasureTheory.ComplexMeasure.im c).HaveLebesgueDecomposition μ → c.HaveLebesgueDecomposition μ
-- Mathlib.Data.Set.Equitable
Set.equitableOn_iff_exists_eq_eq_add_one : ∀ {α : Type u_1} {s : Set α} {f : α → ℕ}, s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, f a = b ∨ f a = b + 1
-- Init.Data.Int.Order
Int.add_neg_of_neg_of_nonpos : ∀ {a b : ℤ}, a < 0 → b ≤ 0 → a + b < 0
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsTree.card_edgeFinset : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype V] [inst_1 : Fintype ↑G.edgeSet],
  G.IsTree → G.edgeFinset.card + 1 = Fintype.card V
-- Mathlib.Logic.Equiv.Prod
/-- The type of functions to a product `β × γ` is equivalent to the type of pairs of functions
`α → β` and `β → γ`.  -/
Equiv.arrowProdEquivProdArrow : (α : Type u_9) → (β : α → Type u_10) → (γ : α → Type u_11) → ((i : α) → β i × γ i) ≃ ((i : α) → β i) × ((i : α) → γ i)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.CosimplicialObject C} {f g : X ⟶ Y},
  f = g ↔ ∀ (n : SimplexCategory), f.app n = g.app n
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.singleton.congr_simp : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (x x_1 : M i) (e_x : x = x_1) (a : x ≠ 1),
  Monoid.CoprodI.NeWord.singleton x a = Monoid.CoprodI.NeWord.singleton x_1 ⋯
-- Mathlib.RingTheory.Artinian.Defs
isArtinian_iff : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsArtinian R M ↔ WellFounded fun x1 x2 => x1 < x2
-- Mathlib.Data.PFun
PFun.dom_prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ),
  (f.prodMap g).Dom = {x | (f x.1).Dom ∧ (g x.2).Dom}
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
panicking if no such pair exists.
 -/
Std.ExtDTreeMap.Const.getEntryGT! : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtDTreeMap α (fun x => β) cmp → α → α × β
-- Mathlib.Tactic.TacticAnalysis
/-- The function that runs this pass. Takes an array of infotree nodes corresponding
to a sequence of tactics from the source file. Should do all reporting itself,
for example by `Lean.Linter.logLint`.
 -/
Mathlib.TacticAnalysis.Config.run : Mathlib.TacticAnalysis.Config → Array Mathlib.TacticAnalysis.TacticNode → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_zero : ↑0 = 0
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.coconesEquiv_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.Final.coconesEquiv F G).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun c =>
        CategoryTheory.Limits.Cocone.ext
          (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone (F.comp G))).obj c).pt) ⋯)
      ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β}, k ∈ t₂ → Std.DTreeMap.Const.getD (t₁ ∩ t₂) k fallback = Std.DTreeMap.Const.getD t₁ k fallback
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_self_eq_dirac : ∀ {X : Type u_1} [inst : MeasurableSpace X] (x : X) (p : ↑unitInterval),
  ProbabilityTheory.bernoulliMeasure x x p = MeasureTheory.Measure.dirac x
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.equivalence_unitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  (CategoryTheory.ShrinkHoms.equivalence C).unitIso =
    CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).obj x)) ⋯
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
CommMonCat.forget_isCorepresentable : (CategoryTheory.forget CommMonCat).IsCorepresentable
-- Batteries.Tactic.GeneralizeProofs
/-- Monad used to generalize proofs.
Carries `Mathlib.Tactic.GeneralizeProofs.Config` and `Mathlib.Tactic.GeneralizeProofs.State`.  -/
Batteries.Tactic.GeneralizeProofs.MGen : Type → Type
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_sInf : ∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] {A : Set (Ideal R)} {f : F},
  Function.Surjective ⇑f → (∀ J ∈ A, RingHom.ker f ≤ J) → Ideal.map f (sInf A) = sInf (Ideal.map f '' A)
-- Aesop.Script.Tactic
Aesop.Script.TacticBuilder : Type
-- Mathlib.Data.Nat.ModEq
/-- A common factor that's coprime with the modulus can be cancelled from a `ModEq`  -/
Nat.ModEq.cancel_right_of_coprime : ∀ {m a b c : ℕ}, m.gcd c = 1 → a * c ≡ b * c [MOD m] → a ≡ b [MOD m]
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pushout.instIsSplitMonoInr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f f], CategoryTheory.IsSplitMono (CategoryTheory.Limits.pushout.inr f f)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.zero_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ 0 = 0
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
RingHom.IsIntegralElem.of_comp : ∀ {R : Type u_1} {S : Type u_4} {T : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring T] {f : R →+* S}
  {g : S →+* T} {x : T}, (g.comp f).IsIntegralElem x → g.IsIntegralElem x
-- Init.Data.List.Basic
List.intersperseTR.eq_2 : ∀ {α : Type u} (sep x_1 : α), List.intersperseTR sep [x_1] = [x_1]
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative commutes with shifting the function by a constant on the right.  -/
iteratedFDerivWithin_comp_add_right' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} (n : ℕ) (a : E),
  iteratedFDerivWithin 𝕜 n (fun z => f (z + a)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {c₁ c₂ : CategoryTheory.Limits.PushoutCocone f g} (a : c₁ ⟶ c₂),
  (CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.functor.map a).hom = CategoryTheory.Under.homMk a.hom ⋯
-- Init.Data.Vector.Algebra
Vector.getElem_zero : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] (i : ℕ) (h : i < n), 0[i] = 0
-- Init.Data.Float.Model.Float
/-- Computes `m * 10^e`.  -/
Float.Model.ofScientific : ℕ → ℤ → Float.Model
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
MeasureTheory.VectorMeasure.enorm_apply_le_bound : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  {μ : MeasureTheory.VectorMeasure X E} {s : Set X}, ‖μ s‖ₑ ≤ ↑μ.bound
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.reverse = 0 ↔ f = 0
-- Init.Data.SInt.Bitwise
Int64.not_xor : ∀ {a b : Int64}, ~~~a ^^^ b = ~~~(a ^^^ b)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.lift_self : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c),
  t.lift c = CategoryTheory.CategoryStruct.id c.pt
-- Mathlib.Topology.Algebra.Group.Pointwise
compl_mul_closure_one_eq : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {t : Set G},
  t * closure {1} = t → tᶜ * closure {1} = tᶜ
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.ι_p₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (self : HomotopicalAlgebra.PrepathObject A),
  CategoryTheory.CategoryStruct.comp self.ι self.p₀ = CategoryTheory.CategoryStruct.id A
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv.eq_1 : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] (f : 𝕜 → F) (x : 𝕜), deriv f x = (fderiv 𝕜 f x) 1