mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Constructions
/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
AnalyticWithinAt.zpow : ∀ {𝕜 : 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 → 𝕝}
  {z : E} {s : Set E} {n : ℤ}, AnalyticWithinAt 𝕜 f s z → f z ≠ 0 → AnalyticWithinAt 𝕜 (f ^ n) s z
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addCHaar_empty : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G), MeasureTheory.Measure.haar.addCHaar K₀ ⊥ = 0
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C) (j : κ.ord.ToType),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Arrow.Hom.right
        (CategoryTheory.Arrow.Hom.right (CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso I κ f j).hom))
      (CategoryTheory.Arrow.Hom.right
        (((CategoryTheory.SmallObject.iterationFunctor I κ).map (CategoryTheory.homOfLE ⋯)).app f)) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.Arrow.mk
            (((CategoryTheory.SmallObject.iterationFunctor I κ).map (CategoryTheory.homOfLE ⋯)).app f)).right.right
-- Mathlib.Analysis.Convex.Between
Sbtw.not_swap_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {x y z : P},
  Sbtw R x y z → ¬Wbtw R y x z
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.get.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} (idx : ℕ) (hidx : idx < len)
  (refs : Vector Std.Sat.AIG.Fanin len) (hrefs : ∀ {i : ℕ} (h : i < len), refs[i].gate < aig.decls.size),
  { refs := refs, hrefs := hrefs }.get idx hidx = { gate := refs[idx].gate, invert := refs[idx].invert, hgate := ⋯ }
-- Init.Data.Int.Gcd
Int.gcd_eq_natAbs_right_iff_dvd : ∀ {a b : ℤ}, a.gcd b = b.natAbs ↔ b ∣ a
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- The naturality condition.  -/
CategoryTheory.Lax.OplaxTrans.Modification.naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (self : CategoryTheory.Lax.OplaxTrans.Modification η θ) {a b : B}
  (f : a ⟶ b) {Z : F.obj a ⟶ G.obj b} (h : CategoryTheory.CategoryStruct.comp (θ.app a) (G.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b))
      (CategoryTheory.CategoryStruct.comp (θ.naturality f) h) =
    CategoryTheory.CategoryStruct.comp (η.naturality f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f)) h)
-- Mathlib.Topology.Compactness.Compact
IsCompact.elim_nhdsWithin_subcover' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s →
    ∀ (U : (x : X) → x ∈ s → Set X), (∀ (x : X) (hx : x ∈ s), U x hx ∈ nhdsWithin x s) → ∃ t, s ⊆ ⋃ x ∈ t, U ↑x ⋯
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.toLinearEquiv_injective : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂], Function.Injective ContinuousLinearEquiv.toLinearEquiv
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_add' : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  (x y : R), v x ≤ v (x + y) ∨ v y ≤ v (x + y)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddLeftCancelMonoid : {α : Type u_1} → [AddLeftCancelMonoid α] → AddLeftCancelMonoid (Lex α)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the angle between three points is `π`, the first and third points are not equal.  -/
EuclideanGeometry.left_ne_right_of_oangle_eq_pi : ∀ {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 → p₁ ≠ p₃
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonnegg_pos_neg : ∀ {c d a b : ℕ}, Zsqrtd.Nonnegg c d (↑a) (-↑b) ↔ Zsqrtd.SqLe b c a d
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- A locally finite simple graph is regular of degree `d` if every vertex has degree `d`.  -/
SimpleGraph.IsRegularOfDegree : {V : Type u_1} → (G : SimpleGraph V) → [G.LocallyFinite] → ℕ → Prop
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv : {B : Type u} →
  [inst : Quiver B] →
    {a b : CategoryTheory.FreeBicategory B} →
      (f : a ⟶ b) →
        CategoryTheory.FreeBicategory.Hom₂ f (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanExt_inv_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
  (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.cospanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingCospan.right = iY.inv
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.isDenseSubsite_of_isOneHypercoverDense : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor C₀ C) (J₀ : CategoryTheory.GrothendieckTopology C₀)
  (J : CategoryTheory.GrothendieckTopology C) [F.IsOneHypercoverDense J₀ J] [F.IsLocallyFull J] [F.IsLocallyFaithful J],
  (∀ {X₀ : C₀} {S₀ : CategoryTheory.Sieve X₀},
      CategoryTheory.Sieve.functorPushforward F S₀ ∈ J.sieves (F.obj X₀) ↔ S₀ ∈ J₀.sieves X₀) →
    CategoryTheory.Functor.IsDenseSubsite J₀ J F
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
Complex.lintegral_comp_pi_polarCoord_symm : ∀ {ι : Type u_1} [inst : Fintype ι] (f : (ι → ℂ) → ENNReal),
  (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i, ENNReal.ofReal (p i).1) * f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫⁻ (p : ι → ℂ), f p
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coprod.congr_simp : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [inst_6 : ContinuousAdd M] [inst_7 : AddCommMonoid M₁] [inst_8 : Module R M₁] [inst_9 : AddCommMonoid M₂]
  [inst_10 : Module R M₂] (f₁ f₁_1 : M₁ →L[R] M),
  f₁ = f₁_1 → ∀ (f₂ f₂_1 : M₂ →L[R] M), f₂ = f₂_1 → f₁.coprod f₂ = f₁_1.coprod f₂_1
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.counit_coe_dFinsupp : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : n → Type u_3}
  [inst_3 : (i : n) → AddCommMonoid (A i)] [inst_4 : (i : n) → Module R (A i)]
  [inst_5 : (i : n) → CoalgebraStruct R (A i)] (x : Π₀ (i : n), A i),
  CoalgebraStruct.counit ⇑x = CoalgebraStruct.counit x
-- Mathlib.Data.Finset.Image
Multiset.toFinset_map : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α → β) (m : Multiset α),
  (Multiset.map f m).toFinset = Finset.image f m.toFinset
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.box.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (ty : Lean.Expr) (fvarId : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_21) (ty_1 : Lean.Expr)
  (fvarId_1 : Lean.FVarId)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_21),
  (Lean.Compiler.LCNF.LetValue.box ty fvarId h = Lean.Compiler.LCNF.LetValue.box ty_1 fvarId_1 h_1) =
    (ty = ty_1 ∧ fvarId = fvarId_1)
-- Mathlib.Data.Rat.Defs
Rat.addCommSemigroup : AddCommSemigroup ℚ
-- Mathlib.Algebra.Group.Basic
div_mul_div_cancel' : ∀ {G : Type u_3} [inst : CommGroup G] (a b c : G), a / b * (c / a) = c / b
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm : ∀ {E : Type u_4} [inst : SeminormedAddGroup E] {x : E}, Filter.Tendsto (fun a => ‖a‖) (nhds x) (nhds ‖x‖)
-- Init.Omega.IntList
Lean.Omega.IntList.dot_nil_left : ∀ {ys : Lean.Omega.IntList}, Lean.Omega.IntList.dot [] ys = 0
-- Mathlib.Data.Fin.Fin2
Fin2.equivFin_apply : ∀ (n : ℕ) (i : Fin2 n), (Fin2.equivFin n) i = i.toFin
-- Init.Data.List.Basic
/-- Folds a function over a list from the right, accumulating a value starting with `init`. The
accumulated value is combined with each element of the list in reverse order, using `f`.

`O(|l|)`. Replaced at runtime with `List.foldrTR`.

Examples:
 * `[a, b, c].foldr f init  = f a (f b (f c init))`
 * `[1, 2, 3].foldr (toString · ++ ·) "" = "123"`
 * `[1, 2, 3].foldr (s!"({·} {·})") "!" = "(1 (2 (3 !)))"`
 -/
List.foldr : {α : Type u} → {β : Type v} → (α → β → β) → β → List α → β
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.measurable_measure_mul_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] {s : Set G}, MeasurableSet s → Measurable fun x => μ ((fun y => y * x) ⁻¹' s)
-- Mathlib.Topology.MetricSpace.Bounded
/-- Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter.  -/
Metric.isBounded_iff_ediam_ne_top : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α], Bornology.IsBounded s ↔ Metric.ediam s ≠ ⊤
-- Init.Data.List.Lemmas
List.getElem?_insert_succ : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List α} {a : α} {i : ℕ},
  (List.insert a l)[i + 1]? = if a ∈ l then l[i + 1]? else l[i]?
-- Mathlib.Data.Finset.Interval
/-- Cardinality of a non-empty `Icc` of finsets.  -/
Finset.card_Icc_finset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊆ t → (Finset.Icc s t).card = 2 ^ (t.card - s.card)
-- Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Set.Nonempty.mul_zero : ∀ {α : Type u_1} [inst : MulZeroClass α] {s : Set α}, s.Nonempty → s * 0 = 0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcomposeComp.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G H : CategoryTheory.Functor J C} (α : F ⟶ G) (β : G ⟶ H),
  CategoryTheory.Limits.Cone.postcomposeComp α β =
    CategoryTheory.NatIso.ofComponents
      (fun s =>
        CategoryTheory.Limits.Cone.ext
          (CategoryTheory.Iso.refl
            ((CategoryTheory.Limits.Cone.postcompose (CategoryTheory.CategoryStruct.comp α β)).obj s).pt)
          ⋯)
      ⋯
-- Lean.DocString.DeferredCheck
Lean.Doc.instReprDeferredCheckSite : Repr Lean.Doc.DeferredCheckSite
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgHom.toUnder.eq_1 : ∀ {R : CommRingCat} {A B : Type u} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra (↑R) A]
  [inst_3 : Algebra (↑R) B] (f : A →ₐ[↑R] B), f.toUnder = CategoryTheory.Under.homMk (CommRingCat.ofHom f.toRingHom) ⋯
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type is a subtraction monoid if `β` is a subtraction monoid.  -/
FunLike.subtractionMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] →
            [inst_3 : SMul ℕ F] →
              [inst_4 : Neg F] →
                [inst_5 : Sub F] →
                  [inst_6 : SMul ℤ F] →
                    [inst_7 : SubtractionMonoid β] →
                      [IsZeroApply F α β] →
                        [IsAddApply F α β] →
                          [IsNegApply F α β] →
                            [IsSubApply F α β] → [IsSMulApply ℕ F α β] → [IsSMulApply ℤ F α β] → SubtractionMonoid F
-- Mathlib.RingTheory.Localization.LocalizationLocalization
/-- If `M ≤ N` are submonoids of `R` such that `∀ x : N, ∃ m : R, m * x ∈ M`, then the
localization at `N` is equal to the localization of `M`.  -/
IsLocalization.isLocalization_of_is_exists_mul_mem : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (M N : Submonoid R) [IsLocalization M S], M ≤ N → (∀ (x : ↥N), ∃ m, m * ↑x ∈ M) → IsLocalization N S
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.EvenHom.mk.sizeOf_spec : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] [inst_5 : SizeOf R]
  [inst_6 : SizeOf M] [inst_7 : SizeOf A] (bilin : M →ₗ[R] M →ₗ[R] A)
  (contract : ∀ (m : M), (bilin m) m = (algebraMap R A) (Q m))
  (contract_mid : ∀ (m₁ m₂ m₃ : M), (bilin m₁) m₂ * (bilin m₂) m₃ = Q m₂ • (bilin m₁) m₃),
  sizeOf { bilin := bilin, contract := contract, contract_mid := contract_mid } = 1 + sizeOf bilin
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.roots_degree_eq_one : ∀ {R : Type u} [inst : Field R] {p : Polynomial R}, p.degree = 1 → p.roots = {-((p.coeff 1)⁻¹ * p.coeff 0)}
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.coe_id : ∀ (α : Type u_2) [inst : Max α] [inst_1 : Bot α], ⇑(SupBotHom.id α) = id
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.toMonoid.eq_1 : ∀ {M : Type u_4} [inst : Monoid M] {A : Type u_5} [inst_1 : SetLike A M] [inst_2 : SubmonoidClass A M] (S : A),
  SubmonoidClass.toMonoid S =
    { toSemigroup := MulMemClass.toSemigroup S, toOne := OneMemClass.one S, one_mul := ⋯, mul_one := ⋯,
      toNPow := NPow.ofPow, npow_zero := ⋯, npow_succ := ⋯ }
-- Aesop.Tree.Check
_private.Aesop.Tree.Check.0.Aesop.MVarClusterRef.checkIrrelevance.go : String → Bool → Bool → Lean.CoreM Bool
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toOuterMeasure_apply_finset : ∀ {α : Type u_1} (p : PMF α) (s : Finset α), p.toOuterMeasure ↑s = ∑ x ∈ s, p x
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
/-- If `w` is a ramified place over `v` then `w.Completion` has `v.Completion` dimension two.  -/
NumberField.InfinitePlace.IsRamified.finrank_eq_two : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K) {w : NumberField.InfinitePlace L} [inst_3 : w.LiesOver v],
  NumberField.InfinitePlace.IsRamified K w → Module.finrank v.Completion w.Completion = 2
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the sign of the angle between two vectors is positive, the first vector is nonzero.  -/
Orientation.left_ne_zero_of_oangle_sign_eq_one : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, (o.oangle x y).sign = 1 → x ≠ 0
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.finset_sups : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {p : SeminormFamily 𝕜 E ι} [inst_3 : TopologicalSpace E], WithSeminorms p → WithSeminorms fun s => s.sup p
-- Lean.Environment
Lean.Kernel.Exception.other.injEq : ∀ (msg msg_1 : String), (Lean.Kernel.Exception.other msg = Lean.Kernel.Exception.other msg_1) = (msg = msg_1)
-- Mathlib.Data.Set.Lattice.Image
Set.iUnion_image_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) {s : Set α} {t : Set β},
  ⋃ b ∈ t, (fun x => f x b) '' s = Set.image2 f s t
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.le_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : IsLocalRing R] {J : Ideal R}, J ≠ ⊤ → J ≤ IsLocalRing.maximalIdeal R
-- Aesop.RuleTac.Basic
/-- A single rule application, representing the application of a tactic to the input
goal. Must accurately report the following information:

- `goals`: the goals generated by the tactic.
- `postState`: the `MetaM` state after the tactic was run.
- `scriptSteps?`: script steps which produce the same effect as the rule tactic.
  If `input.options.generateScript = false` (where `input` is the
  `RuleTacInput`), this field is ignored. If the tactic does not support script
  generation, use `none`.
- `successProbability`: The success probability of this rule application. If
  `none`, we use the success probability of the applied rule.
 -/
Aesop.RuleApplication : Type
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateUnreachImp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Lean.Expr → Lean.Compiler.LCNF.Code pu
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- The first `n-1` cases are decisions (aka case-splits).  -/
Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.dec : Lean.FVarId → Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof
-- Mathlib.Topology.Algebra.Ring.Compact
IsDedekindDomain.isOpen_of_ne_bot : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R]
  [IsDedekindDomain R] {I : Ideal R}, I ≠ ⊥ → IsOpen ↑I
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_injective : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  Function.Injective (WithVal.toVal v)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The natural transformation from the composition of coextension and restriction of scalars to
identity functor.
 -/
ModuleCat.RestrictionCoextensionAdj.counit' : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          (ModuleCat.coextendScalars f).comp (ModuleCat.restrictScalars f) ⟶ CategoryTheory.Functor.id (ModuleCat R)
-- Mathlib.CategoryTheory.Sites.Subsheaf
/-- A morphism factors through the sheafification of the image presheaf.  -/
CategoryTheory.Subfunctor.toRangeSheafify : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {F F' : CategoryTheory.Functor Cᵒᵖ (Type w)} →
        (f : F' ⟶ F) → F' ⟶ (CategoryTheory.Subfunctor.sheafify J (CategoryTheory.Subfunctor.range f)).toFunctor
-- Mathlib.Computability.NFA
_private.Mathlib.Computability.NFA.0.NFA.Path.supp.match_1.eq_2 : ∀ {α : Type u_1} {σ : Type u_2} {M : NFA α σ} (motive : (x : List α) → (t s : σ) → M.Path s t x → Sort u_3)
  (t s t_1 : σ) (a : α) (x : List α) (a_1 : t_1 ∈ M.step s a) (p : M.Path t_1 t x)
  (h_1 : (s : σ) → motive [] s s (NFA.Path.nil s))
  (h_2 :
    (t s t_2 : σ) →
      (a : α) →
        (x : List α) →
          (a_2 : t_2 ∈ M.step s a) → (p : M.Path t_2 t x) → motive (a :: x) t s (NFA.Path.cons t_2 s t a x a_2 p)),
  (match a :: x, t, s, NFA.Path.cons t_1 s t a x a_1 p with
    | .([]), s, .(s), NFA.Path.nil .(s) => h_1 s
    | .(a :: x), t, s, NFA.Path.cons t_2 .(s) .(t) a x a_2 p => h_2 t s t_2 a x a_2 p) =
    h_2 t s t_1 a x a_1 p
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
/-- A compactly supported continuous function is automatically bounded. This constructor gives
an object of `α →ᵇ γ` from `g : α → γ` and these assumptions.  -/
ofCompactSupport : {α : Type u_1} →
  {γ : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : NonUnitalNormedRing γ] →
        (g : α → γ) → Continuous g → HasCompactSupport g → BoundedContinuousFunction α γ
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- Any action is 0-pretransitive.  -/
MulAction.is_zero_pretransitive' : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α], MulAction.IsMultiplyPretransitive G α 0
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mop.inj : ∀ {C : Type u₁} {unmop unmop_1 : C}, { unmop := unmop } = { unmop := unmop_1 } → unmop = unmop_1
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- **Alias** of `AddMonoidHom.domRestrictHom_apply`. -/
AddMonoidHom.restrictHom_apply : ∀ {M : Type u_1} [inst : AddZeroClass M] {S : Type u_5} [inst_1 : SetLike S M] [inst_2 : AddSubmonoidClass S M] (M' : S)
  (A : Type u_6) [inst_3 : AddCommMonoid A] (f : M →+ A), (AddMonoidHom.domRestrictHom M' A) f = f.domRestrict M'
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.quasiIsoAt_shortComplexTruncLE_g : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Abelian C] (K : HomologicalComplex C c')
  (e : c.Embedding c') [inst_2 : e.IsTruncLE] (i' : ι'),
  (∀ (i : ι), e.f i ≠ i') → QuasiIsoAt (K.shortComplexTruncLE e).g i'
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.isIso_fromTildeΓ_pushforward : ∀ {R S : CommRingCat} (φ : R ⟶ S) (M : (AlgebraicGeometry.Spec S).Modules) [h : CategoryTheory.IsIso M.fromTildeΓ],
  CategoryTheory.IsIso ((AlgebraicGeometry.Scheme.Modules.pushforward (AlgebraicGeometry.Spec.map φ)).obj M).fromTildeΓ
-- Mathlib.Testing.Plausible.Functions
List.dlookup.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a a' : α) (b : β a') (l : List (Sigma β)),
  List.dlookup a (⟨a', b⟩ :: l) = if h : a' = a then some (Eq.recOn h b) else List.dlookup a l
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_eq_zero_iff : ∀ {n k : ℕ}, n.choose k = 0 ↔ n < k
-- Mathlib.Algebra.Group.Indicator
Set.support_subset_subsingleton_of_disjoint_on_support : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero β] {s : γ → Set α} (f : α → β),
  Pairwise (Function.onFun Disjoint fun j => s j ∩ Function.support f) →
    ∀ (i : α) (j : γ), i ∈ s j → (Function.support fun d => (s d).indicator f i) ⊆ {j}
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.symm_bijective : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β],
  Function.Bijective IsometryEquiv.symm
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} [inst_1 : SizeOf C]
  (arrows : CategoryTheory.Presieve X)
  (downward_closed :
    ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (CategoryTheory.CategoryStruct.comp g f)),
  sizeOf { arrows := arrows, downward_closed := downward_closed } = 1
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.gc_map_comap : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂), GaloisConnection (Submodule.map f) (Submodule.comap f)
-- Mathlib.Data.List.Lattice
List.bagInter_nil_iff_inter_nil : ∀ {α : Type u_1} [inst : DecidableEq α] (l₁ l₂ : List α), l₁.bagInter l₂ = [] ↔ l₁ ∩ l₂ = []
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype ↑G.edgeSet], G.edgeFinset = G.edgeSet.toFinset
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_top_left : ∀ {E : Type v} [inst : Field E] (A : Subfield E), ⊤.relfinrank A = 1
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.stabilizer_eq_centralizer : ∀ {G : Type u_3} [inst : Group G] (g : G),
  MulAction.stabilizer (ConjAct G) g = Subgroup.centralizer {ConjAct.toConjAct g}