mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Icc_iff_integrableOn_Ico : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {a b : α} [MeasureTheory.NullSingletonClass μ],
  autoParam (‖f b‖ₑ ≠ ⊤) integrableOn_Icc_iff_integrableOn_Ico._auto_1 →
    (MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ico a b) μ)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.alternatingMapLinearEquiv_ιMulti : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  exteriorPower.alternatingMapLinearEquiv (exteriorPower.ιMulti R n) = LinearMap.id
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_symm : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ}
  (a b : ℝ), ∫ (x : ℝ) in b..a, f x ∂μ = -∫ (x : ℝ) in a..b, f x ∂μ
-- Mathlib.CategoryTheory.Action.Concrete
/-- Shorthand notation for the quotient of `G` by `H` as a finite `G`-set.  -/
Action.FintypeCat.«term_⧸ₐ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.δlastFunctor_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C (n + 1))
  (X : Fin (n + 1)), (CategoryTheory.ComposableArrows.δlastFunctor.obj F).obj X = F.obj X.castSucc
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
RingFilterBasis.SubmodulesBasis.mk : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {BR : RingFilterBasis R} {B : ι → Submodule R M},
  (∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j) →
    (∀ (m : M) (i : ι), ∃ U ∈ BR, U ⊆ (fun x => x • m) ⁻¹' ↑(B i)) → BR.SubmodulesBasis B
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₂ : ∀ (l : ℕ) (pq : ℤ × Fin l), (CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin l).i₂ pq = pq.2.succ
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
/-- Pseudometric space structure pulled back by a function.  -/
PseudoMetricSpace.induced : {α : Type u_3} → {β : Type u_4} → (α → β) → PseudoMetricSpace β → PseudoMetricSpace α
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.Hom.id_f : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  (X : CategoryTheory.DifferentialObject S C),
  (CategoryTheory.DifferentialObject.Hom.id X).f = CategoryTheory.CategoryStruct.id X.obj
-- Std.Do.WP.Sound
/-- Soundness lemma for `StateM.run'`: `Id`-specialization of `StateT.of_wp_run`.  -/
Std.Do.StateM.of_wp_run'_eq : ∀ {α σ : Type} {x : α} {s : σ} {prog : StateM σ α},
  StateT.run' prog s = x →
    ∀ (P : α → Prop), (⊢ₛ (Std.Do.wp prog).apply (Std.Do.PostCond.noThrow fun a => ⌜P a⌝) s) → P x
-- Init.BinderPredicates
/-- The notation `∀ x < 2, p x` is shorthand for `∀ x, x < 2 → p x`,
and similarly for other binary operators.
 -/
Lean.«term∀__,_» : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.enum_lt_nat : ∀ (x : ℕ), (Ordinal.enum LT.lt) ⟨↑x, ⋯⟩ = x
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.comp_α_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n i : ℤ),
  CategoryTheory.CategoryStruct.comp (f.f i) ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.α✝ f n).f i) = 0
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
ClosedSubmodule.top_orthogonal_eq_bot : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ⊤ᗮ = ⊥
-- Mathlib.Topology.Sets.Compacts
/-- The type of nonempty compact sets of a topological space.  -/
TopologicalSpace.NonemptyCompacts : (α : Type u_4) → [TopologicalSpace α] → Type u_4
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp]
  (t t_1 : Std.ExtDTreeMap α (fun x => β) cmp),
  t = t_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (fallback fallback_1 : β),
          fallback = fallback_1 →
            Std.ExtDTreeMap.Const.getD t a fallback = Std.ExtDTreeMap.Const.getD t_1 a_1 fallback_1
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The chosen cone is a limit cone.
(Generally, you'll just want to use `limit.cone F`.)
 -/
CommMonCat.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommMonCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] →
        CategoryTheory.Limits.IsLimit (CommMonCat.limitCone F)
-- Mathlib.Algebra.Algebra.Field
algebraMap.coe_div : ∀ {R : Type u_1} (A : Type u_2) [inst : Semifield R] [inst_1 : DivisionSemiring A] [inst_2 : Algebra R A] (r s : R),
  ↑(r / s) = ↑r / ↑s
-- Mathlib.Algebra.Category.Grp.Basic
/-- Construct a bundled `GrpCat` from the underlying type and typeclass.  -/
GrpCat.of : (M : Type u) → [Group M] → GrpCat
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeObj_tensor : ∀ {C : Type u} (X Y : CategoryTheory.FreeMonoidalCategory C)
  (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).normalizeObj n = Y.normalizeObj (X.normalizeObj n)
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupKind.markdown : Lean.Lsp.MarkupKind
-- Mathlib.CategoryTheory.Filtered.CostructuredArrow
/-- Given functors `L : A ⥤ T` and `R : B ⥤ T` with a common codomain we can conclude that `A`
is filtered given that `R` is final, `B` is filtered and each costructured arrow category
`CostructuredArrow L (R.obj b)` is filtered.  -/
CategoryTheory.isFiltered_of_isFiltered_costructuredArrow : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [CategoryTheory.IsFiltered B] [R.Final]
  [∀ (b : B), CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow L (R.obj b))], CategoryTheory.IsFiltered A
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : β → β}, (m.modify k f).getKey? k = if k ∈ m then some k else none
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.declModifiersDocStatus : Lean.Syntax → Lean.Elab.Command.CommandElabM (Option Bool)
-- Mathlib.Tactic.Polynomial.Basic
/-- `polynomial` solves equalities of `Polynomial`s and similar types.

Given a goal which is an equality in `Polynomial R` with a commutative ring `R`, `polynomial`
turns both sides of the equation into a normal form by expanding out the brackets. It then closes
the goal if both sides contain the same terms and fails otherwise. `polynomial_nf` normalizes all
subexpressions at a given location.

Variants of `polynomial` include:
* `polynomial`: normalize both sides of an equation and close the goal if they are equal
* `polynomial!`: run `polynomial` at default transparency
* `polynomial_nf`: normalize all subexpression of the goal
* `polynomial_nf at h₁ h₂ ⊢`: normalize all subexpressions at hypotheses `h₁` `h₁` and the goal
* `polynomial_nf at *`: normalize all subexpressions of all local hypotheses and the goal
* `polynomial_nf!`: run `polynomial_nf` at default transparency

The `polynomial` tactic can be extended to work with algebras other than `Polynomial` using the
attributes `polynomial_infer_base`, `polynomial_pre` and `polynomial_post`. This is only possible
if the base ring can be inferred from the structure of the type.

Examples:

```
example (a : ℚ) : (X + C a) * (X - C a) = X^2 + C (a^2) := by polynomial

example {P : ℚ[X] → Prop} (h : P (X ^ 2 + X + C 4⁻¹)) : P ((X + C 2⁻¹) ^ 2) := by
  polynomial_nf at h ⊢
  exact h
```

 -/
Mathlib.Tactic.Polynomial.polynomialNF : Lean.ParserDescr
-- Init.Data.List.Lemmas
List.reverse_eq_nil_iff : ∀ {α : Type u_1} {xs : List α}, xs.reverse = [] ↔ xs = []
-- Batteries.CodeAction.Misc
/-- Return the syntax stack leading to `target` from `root`, if one exists.  -/
Batteries.CodeAction.findStack? : Lean.Syntax → Lean.Syntax → Option Lean.Syntax.Stack
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- Kernel of a product map (right-exactness of tensor product)  -/
TensorProduct.map_ker : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P},
  Function.Exact ⇑f ⇑g →
    Function.Surjective ⇑g →
      ∀ {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [inst_7 : AddCommGroup M'] [inst_8 : AddCommGroup N']
        [inst_9 : AddCommGroup P'] [inst_10 : Module R M'] [inst_11 : Module R N'] [inst_12 : Module R P']
        {f' : M' →ₗ[R] N'} {g' : N' →ₗ[R] P'},
        Function.Exact ⇑f' ⇑g' →
          Function.Surjective ⇑g' →
            (TensorProduct.map g g').ker = (LinearMap.lTensor N f').range ⊔ (LinearMap.rTensor N' f).range
-- Mathlib.Order.Comparable
CompRel.of_lt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], a < b → CompRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The Fourier integral of an `L^1` function is a continuous function.  -/
VectorFourier.fourierIntegral_continuous : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module 𝕜 W] {E : Type u_4}
  [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace ℂ E] [inst_8 : TopologicalSpace 𝕜] [IsTopologicalRing 𝕜]
  [inst_10 : TopologicalSpace V] [BorelSpace V] [inst_12 : TopologicalSpace W] {e : AddChar 𝕜 Circle}
  {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} [FirstCountableTopology W],
  Continuous ⇑e →
    (Continuous fun p => (L p.1) p.2) →
      ∀ {f : V → E}, MeasureTheory.Integrable f μ → Continuous (VectorFourier.fourierIntegral e μ L f)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.IsBipartite.four_mul_encard_edgeSet_le : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsBipartite → 4 * G.edgeSet.encard ≤ ENat.card V ^ 2
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.homologyπ_extendHomologyIso_hom : ∀ {ι : 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.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'],
  CategoryTheory.CategoryStruct.comp ((K.extend e).homologyπ j') (K.extendHomologyIso e hj').hom =
    CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom (K.homologyπ j)
-- Mathlib.Algebra.Group.Conj
/-- Given an element `a`, `conjugatesOf a` is the set of conjugates.  -/
conjugatesOf : {α : Type u} → [Monoid α] → α → Set α
-- Mathlib.MeasureTheory.Measure.Regular
/-- Any finite measure on a metrizable space (or even a pseudometrizable space)
is weakly regular.  -/
MeasureTheory.Measure.WeaklyRegular.of_pseudoMetrizableSpace_of_isFiniteMeasure : ∀ {X : Type u_3} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] [inst_2 : MeasurableSpace X]
  [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ], μ.WeaklyRegular
-- Mathlib.Probability.Kernel.Proper
MeasureTheory.Measure.instSMul.congr_simp : ∀ {α : Type u_1} {R : Type u_6} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal]
  {x : MeasurableSpace α}, MeasureTheory.Measure.instSMul = MeasureTheory.Measure.instSMul
-- Batteries.Data.Fin.Lemmas
Fin.isSome_findSome?_of_isSome : ∀ {n : ℕ} {α : Type u_1} {i : Fin n} {f : Fin n → Option α}, (f i).isSome = true → (Fin.findSome? f).isSome = true
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
CochainComplex.isKProjective_iff_leftOrthogonal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ),
  K.IsKProjective ↔
    (HomotopyCategory.subcategoryAcyclic C).leftOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
-- Batteries.Data.Nat.Bisect
Nat.bisect_lt_stop : ∀ {start stop : ℕ} {p : ℕ → Bool} (h : start < stop) (hstart : p start = true) (hstop : p stop = false),
  Nat.bisect h hstart hstop < stop
-- Mathlib.Algebra.Group.Submonoid.BigOperators
AddSubmonoid.multiset_noncommSum_mem : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) (m : Multiset M) (comm : {x | x ∈ m}.Pairwise AddCommute),
  (∀ x ∈ m, x ∈ S) → m.noncommSum comm ∈ S
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanIso.isMulFreimanHom : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β}
  {n : ℕ}, IsMulFreimanIso n A B f → IsMulFreimanHom n A B f
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.comap_id : ∀ {α : Type u} (f : Ultrafilter α) (h₀ : optParam (Function.Injective id) ⋯) (h₁ : optParam (Set.range id ∈ f) ⋯),
  f.comap h₀ h₁ = f
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f` is an immersion, it is an immersion at each point.

Note that the converse statement is false in general:
if `f` is an immersion at each `x`, but with the choice of complement possibly depending on `x`,
there need not be a global choice of complement for which `f` is an immersion at each point.
The complement of `f` at `x` is isomorphic to the cokernel of `mfderiv I J f x`, but the `mfderiv`
of `f` at (even nearby) points `x` and `x'` are not directly related. They have the same rank
(the dimension of `E`, as will follow from injectivity), but if `E''` is infinite-dimensional this
is not conclusive. If `E''` is infinite-dimensional, this dimension can indeed change between
different connected components of `M`.
 -/
Manifold.IsImmersion.isImmersionAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsImmersion I J n f → ∀ (x : M), Manifold.IsImmersionAt I J n f x
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.eq_one_of_roots_le : ∀ {F : Type u_3} {K : Type u_4} [inst : CommRing F] [inst_1 : NormedField K] {p : Polynomial F} {f : F →+* K} {B : ℝ},
  B < 0 → p.Monic → (Polynomial.map f p).Splits → (∀ z ∈ (Polynomial.map f p).roots, ‖z‖ ≤ B) → p = 1
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.vcDim_mono : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 ℬ : Finset (Finset α)}, 𝒜 ⊆ ℬ → 𝒜.vcDim ≤ ℬ.vcDim
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.naturality_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {p f pf : C}
  (η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf),
  CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.Iso.refl f) ≪≫ η_f = η_f
-- Std.Data.TreeMap.Raw.Iterator
Std.TreeMap.Raw.valuesIter_toList : ∀ {α β : Type u_1} {cmp : α → α → Ordering} (m : Std.TreeMap.Raw α β cmp), m.valuesIter.toList = m.values
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.choose_fst_mem : ∀ {α : Type u} {s : Set α} (hs : s.Nontrivial), hs.choose.1 ∈ s
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- Given two maps `r : I₁ × I₂ × I₃ → J` and `π : I₁ × I₃ → J`, this structure is the
input in the formulation of the triangle equality `mapBifunctor_triangle` which
relates the left and right unitor and the associator for `GradedObject.mapBifunctor`.  -/
CategoryTheory.GradedObject.TriangleIndexData : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₃ : Type u_3} → {J : Type u_4} → [Zero I₂] → (I₁ × I₂ × I₃ → J) → (I₁ × I₃ → J) → Type (max (max u_1 u_2) u_3)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
ExteriorAlgebra.basis_mul_of_not_disjoint : ∀ {R : Type u_1} {M : Type u_2} {m n : ℕ} {I : Type u_3} [inst : LinearOrder I] [inst_1 : CommRing R]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I m))
  (t : ↑(Set.powersetCard I n)), ¬Disjoint ↑s ↑t → b.ExteriorAlgebra ↑s * b.ExteriorAlgebra ↑t = 0
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.instInhabitedExprVisited : Inhabited Lean.Meta.Canonicalizer.ExprVisited
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.cast_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_5} {A : ι → Type u_6} [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] [inst_3 : (i : ι) → TopologicalSpace (A i)] {i j : ι} (h : i = j) (x : A i),
  (ContinuousAlgEquiv.cast h) x = (Equiv.cast ⋯) x
-- Mathlib.Algebra.Ring.Commute
neg_pow : ∀ {R : Type u} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R) (n : ℕ), (-a) ^ n = (-1) ^ n * a ^ n
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.pow_succ_eq : ∀ {M : Type u_1} [inst : Monoid M] {a : M} (n : ℕ), IsIdempotentElem a → a ^ (n + 1) = a
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instSubmonoidClass : ∀ {M : Type u_1} [inst : MulOneClass M], SubmonoidClass (Submonoid M) M
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Given a point in an affine subspace, the set of vectors in its direction equals the set of
vectors subtracting that point on the left.  -/
AffineSubspace.coe_direction_eq_vsub_set_left : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P}, p ∈ s → ↑s.direction = (fun x => p -ᵥ x) '' ↑s
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_eq_fallback : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, a ∉ t → t.getKeyD a fallback = fallback
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.cons.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι} (g : G i)
  (w : Monoid.PushoutI.NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range),
  Monoid.PushoutI.NormalWord.cons g w hmw hgr =
    { toWord := Monoid.CoprodI.Word.cons (↑(⋯.equiv (g * (φ i) w.head)).2) w.toWord hmw ⋯,
      head := (MonoidHom.ofInjective ⋯).symm (⋯.equiv (g * (φ i) w.head)).1, normalized := ⋯ }
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidSaveTextDocumentParams.mk : Lean.Lsp.TextDocumentIdentifier → Option String → Lean.Lsp.DidSaveTextDocumentParams
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {f : β → α} {b : β}, {b}.inf f = f b
-- Mathlib.Data.Finset.Empty
Finset.Nonempty.forall_const : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → ∀ {p : Prop}, (∀ x ∈ s, p) ↔ p
-- Mathlib.Data.Set.Opposite
/-- The unop of a set `s` is the set obtained by taking the unop of each member of `s`.  -/
Set.unop : {α : Type u_1} → Set αᵒᵖ → Set α
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mapEquiv_refl : ∀ {R : Type u} (σ : Type u_1) [inst : CommSemiring R],
  MvPolynomial.mapEquiv σ (RingEquiv.refl R) = RingEquiv.refl (MvPolynomial σ R)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- If `P` is a strong FE pair, then `P.Λ` is entire.  -/
IsStrongFEPair.differentiable_Λ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P → Differentiable ℂ P.Λ
-- Init.Data.Option.Lemmas
Option.not_mem_none : ∀ {α : Type u_1} (a : α), a ∉ none
-- Mathlib.Topology.NoetherianSpace
/-- In a Noetherian space, all sets are compact.  -/
TopologicalSpace.NoetherianSpace.isCompact : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] (s : Set α), IsCompact s
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
Submonoid.mem_closure_image_one_lt_iff : ∀ {ι : Type u_1} {M : Type u_2} {S : Type u_4} [inst : Monoid M] [inst_1 : LinearOrder S] [inst_2 : CommMonoid S]
  [IsOrderedCancelMonoid S] (v : ι → M) (f : M →* S) (i : ι),
  v i ≠ 1 → (v i ∈ Submonoid.closure (v '' {i | 1 < f (v i)}) ↔ 1 < f (v i))
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_iff_comap_le : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β},
  Measurable f ↔ MeasurableSpace.comap f m₂ ≤ m₁
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_natCast_div : ∀ {x : ℝ} (m : ℕ), Irrational (↑m / x) → Irrational x
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.coe_vadd_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] (a : α) (s : Finset β), ↑(a +ᵥ s) = a +ᵥ ↑s
-- Mathlib.RingTheory.Adjoin.FG
Subalgebra.fg_adjoin_finset : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Finset A),
  (Algebra.adjoin R ↑s).FG
-- Mathlib.Analysis.PSeries
Finset.le_sum_schlomilch : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M} {u : ℕ → ℕ},
  (∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) →
    (∀ (n : ℕ), 0 < u n) →
      Monotone u →
        ∀ (n : ℕ),
          ∑ k ∈ Finset.range (u n), f k ≤
            ∑ k ∈ Finset.range (u 0), f k + ∑ k ∈ Finset.range n, (u (k + 1) - u k) • f (u k)
-- Mathlib.Order.GameAdd
Sym2.GameAdd.recursion_eq : ∀ {α : Type u_1} {rα : α → α → Prop} {C : α → α → Sort u_3} (hr : WellFounded rα)
  (IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a b : α),
  Sym2.GameAdd.recursion hr IH a b = IH a b fun a' b' x => Sym2.GameAdd.recursion hr IH a' b'
-- ImportGraph.Imports.Redundant
_private.ImportGraph.Imports.Redundant.0.Lean.Environment.findRedundantImports.visit : Lean.NameMap (Array Lean.Name) → Array Lean.Name → Lean.NameSet → Lean.NameSet → Lean.Name → Lean.NameSet × Lean.NameSet
-- Mathlib.Algebra.Regular.SMul
IsSMulRegular.isRightRegular : ∀ {R : Type u_1} [inst : Mul R] {a : R}, IsSMulRegular R (MulOpposite.op a) → IsRightRegular a