mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Submodule.toSubalgebra_toSubsemiring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (p : Submodule R A)
  (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p),
  (p.toSubalgebra h_one h_mul).toSubsemiring =
    { carrier := p.carrier, mul_mem' := ⋯, one_mem' := h_one, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_comap_le : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂),
  AffineSubspace.map f (AffineSubspace.comap f s) ≤ s
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoid.End.instIntCast : {M : Type uM} → [inst : AddCommGroup M] → IntCast (AddMonoid.End M)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.zero_rpow_of_neg : ∀ {y : ℝ}, y < 0 → 0 ^ y = ⊤
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Context.mk.sizeOf_spec : ∀ (maxResultSize maxHeartbeats : ℕ),
  sizeOf { maxResultSize := maxResultSize, maxHeartbeats := maxHeartbeats } =
    1 + sizeOf maxResultSize + sizeOf maxHeartbeats
-- Mathlib.Data.Nat.ChineseRemainder
Nat.chineseRemainderOfList_nil : ∀ {ι : Type u_1} (a s : ι → ℕ), ↑(Nat.chineseRemainderOfList a s [] ⋯) = 0
-- Mathlib.Data.Nat.Choose.Basic
Nat.factorial_dvd_ascFactorial : ∀ (n k : ℕ), k.factorial ∣ n.ascFactorial k
-- Mathlib.Topology.Bornology.Basic
/-- `IsCobounded` is the predicate that `s` is in the filter of cobounded sets in the ambient
bornology on `α`  -/
Bornology.IsCobounded : {α : Type u_2} → [Bornology α] → Set α → Prop
-- Mathlib.MeasureTheory.Measure.Regular
/-- In a metrizable space (or even a pseudometrizable space), an open set can be approximated from
inside by closed sets.  -/
MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace : ∀ {X : Type u_3} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] [inst_2 : MeasurableSpace X]
  (μ : MeasureTheory.Measure X), μ.InnerRegularWRT IsClosed IsOpen
-- Mathlib.NumberTheory.Padics.PadicVal.Defs
/-- **Alias** of `padicValNat_eq_emultiplicity`.

---

A simplification of `padicValNat` when one input is prime, by analogy with
`padicValRat_def`.  -/
padicValNat.maxPowDiv_eq_emultiplicity : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ}, n ≠ 0 → ↑(padicValNat p n) = emultiplicity p n
-- Mathlib.SetTheory.Cardinal.Divisibility
Cardinal.nat_is_prime_iff : ∀ {n : ℕ}, Prime ↑n ↔ Nat.Prime n
-- Mathlib.Data.Multiset.Filter
Multiset.map_filter_eq_filterMap : ∀ {α : Type u_1} {β : Type v} (f : α → β) (p : α → Prop) [inst : DecidablePred p] (s : Multiset α),
  Multiset.map f (Multiset.filter p s) = Multiset.filterMap (fun a => if p a then some (f a) else none) s
-- Mathlib.Data.DFinsupp.FiniteInfinite
DFinsupp.infinite_of_left : ∀ {ι : Type u_1} {π : ι → Type u_2} [∀ (i : ι), Nontrivial (π i)] [inst : (i : ι) → Zero (π i)] [Infinite ι],
  Infinite (Π₀ (i : ι), π i)
-- Mathlib.Algebra.Ring.Action.Pointwise.Finset
Finset.neg_smul : ∀ {R : Type u_1} {G : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup G] [inst_2 : Module R G] [inst_3 : DecidableEq G]
  {s : Finset R} {t : Finset G} [inst_4 : DecidableEq R], -s • t = -(s • t)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.coeff_truncFinset : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)} [inst_1 : DecidableEq σ] {x : σ →₀ ℕ}
  (p : MvPowerSeries σ R),
  MvPolynomial.coeff x ((MvPowerSeries.truncFinset R s) p) = if x ∈ s then (MvPowerSeries.coeff x) p else 0
-- Mathlib.Combinatorics.Quiver.Push
/-- Given a function `τ : W → W'` and a prefunctor `φ : V ⥤q W'`, one can extend `τ` to be
a prefunctor `W ⥤q W'` if `τ` and `σ` factorize `φ` at the level of objects, where `W` is given
the pushforward quiver structure `Push σ`.  -/
Quiver.Push.lift : {V : Type u_1} →
  [inst : Quiver V] →
    {W : Type u_2} →
      (σ : V → W) →
        {W' : Type u_3} →
          [inst_1 : Quiver W'] → (φ : V ⥤q W') → (τ : W → W') → (∀ (x : V), φ.obj x = τ (σ x)) → Quiver.Push σ ⥤q W'
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.comp.match_1.eq_1 : ∀ {C : Type u_1}
  (motive : CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Sort u_2)
  (_X _Y _Z : C)
  (h_1 :
    (_X _Y _Z : C) →
      motive (CategoryTheory.WithInitial.of _X) (CategoryTheory.WithInitial.of _Y) (CategoryTheory.WithInitial.of _Z))
  (h_2 :
    (x : CategoryTheory.WithInitial C) →
      (_X : C) → motive CategoryTheory.WithInitial.star x (CategoryTheory.WithInitial.of _X))
  (h_3 :
    (x : CategoryTheory.WithInitial C) →
      (_X : C) → motive x (CategoryTheory.WithInitial.of _X) CategoryTheory.WithInitial.star)
  (h_4 :
    (_Y : C) →
      (x : CategoryTheory.WithInitial C) → motive (CategoryTheory.WithInitial.of _Y) CategoryTheory.WithInitial.star x)
  (h_5 : Unit → motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.of _Z with
    | CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.of _Z =>
      h_1 _X _Y _Z
    | CategoryTheory.WithInitial.star, x, CategoryTheory.WithInitial.of _X => h_2 x _X
    | x, CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.star => h_3 x _X
    | CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.star, x => h_4 _Y x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star => h_5 ()) =
    h_1 _X _Y _Z
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.all_map : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → β'}
  {p : β' → Bool}, Std.IterM.all p (Std.IterM.map f it) = Std.IterM.all (fun x => p (f x)) it
-- Mathlib.Order.Filter.CountableInter
Filter.le_countableGenerate_iff_of_countableInterFilter : ∀ {α : Type u_2} {g : Set (Set α)} {f : Filter α} [CountableInterFilter f], f ≤ Filter.countableGenerate g ↔ g ⊆ f.sets
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.ofStarMonoidHom_apply : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Star A] [inst_3 : Star B] (f : A →⋆* B)
  (g : B →⋆* A) (h₁ : g.comp f = StarMonoidHom.id A) (h₂ : f.comp g = StarMonoidHom.id B) (a : A),
  (StarMulEquiv.ofStarMonoidHom f g h₁ h₂) a = f a
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.prodₗ_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] (S : Type u_5) [inst_10 : Semiring S] [inst_11 : Module S M₂] [inst_12 : ContinuousAdd M₂]
  [inst_13 : SMulCommClass R S M₂] [inst_14 : ContinuousConstSMul S M₂] [inst_15 : Module S M₃]
  [inst_16 : ContinuousAdd M₃] [inst_17 : SMulCommClass R S M₃] [inst_18 : ContinuousConstSMul S M₃]
  (a : (M →L[R] M₂) × (M →L[R] M₃)), (ContinuousLinearMap.prodₗ S) a = ContinuousLinearMap.prodEquiv.toFun a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The left point of the walking cospan.  -/
CategoryTheory.Limits.WalkingCospan.left : CategoryTheory.Limits.WalkingCospan
-- Init.Data.Array.MapIdx
Array.mapFinIdx_eq_mapFinIdx_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f g : (i : ℕ) → α → i < xs.size → β},
  xs.mapFinIdx f = xs.mapFinIdx g ↔ ∀ (i : ℕ) (h : i < xs.size), f i xs[i] h = g i xs[i] h
-- Init.Data.Nat.Mod
Nat.mod_mul_right_div_self : ∀ (m n k : ℕ), m % (n * k) / n = m / n % k
-- Mathlib.Order.Filter.AtTopBot.Group
/-- $\lim_{x\to\infty^{-1}|x|_m=+\infty$  -/
Filter.tendsto_mabs_atBot_atTop : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G],
  Filter.Tendsto mabs Filter.atBot Filter.atTop
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.isIdRestCold : Char → Bool
-- Lean.Structure
/-- "The `badParent` must come after the `conflicts`.  -/
Lean.StructureResolutionOrderConflict : Type
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryLED_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : α × β}, t₁.Equiv t₂ → t₁.getEntryLED k fallback = t₂.getEntryLED k fallback
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
/-- Given `d : F.WellOrderInductionData`, `val₀ : F.obj (op ⊥)` and `j : J`,
this is the data of an element `val : F.obj (op j)` such that the induced
compatible family of elements in all `F.obj (op i)` for `i ≤ j`
is determined by `val₀` and the choice of "liftings" given by `d`.  -/
CategoryTheory.Functor.WellOrderInductionData.Extension : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        F.WellOrderInductionData → [inst_2 : OrderBot J] → F.obj (Opposite.op ⊥) → J → Type v
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The coercion from `Finset` to `set` as an `AddMonoidHom`.  -/
Finset.coeAddMonoidHom : {α : Type u_2} → [inst : DecidableEq α] → [inst_1 : AddZeroClass α] → Finset α →+ Set α
-- Mathlib.Order.WithBot
WithTop.ofDual.eq_1 : ∀ {α : Type u_1}, WithTop.ofDual = Equiv.refl (WithTop αᵒᵈ)
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.Result.step : Lean.Expr → Lean.Expr → Lean.Meta.MonadSimp.Result
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.mem_genWeightSpace : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : L → R) (m : M),
  m ∈ LieModule.genWeightSpace M χ ↔ ∀ (x : L), ∃ k, (((LieModule.toEnd R L M) x - χ x • 1) ^ k) m = 0
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.congr_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {c : AddCon M} {d : AddCon N} (e : M ≃+ N)
  (h : c = AddCon.comap ⇑e ⋯ d) (a : M), (AddCon.congr e h) ↑a = ↑(e a)
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Header.targetNames : Lean.Elab.Deriving.Header → Array Lean.Name
-- Mathlib.CategoryTheory.Sites.Precoverage.Generates
_private.Mathlib.CategoryTheory.Sites.Precoverage.Generates.0.CategoryTheory.Precoverage.Generates.isSheaf_of_forall_aux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {J : CategoryTheory.GrothendieckTopology C},
  K.Generates J →
    ∀ (F : CategoryTheory.Functor Cᵒᵖ (Type w)),
      (∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) →
        ∀ [∀ (Z : C), Small.{max u v, w} (F.obj (Opposite.op Z))], CategoryTheory.Presieve.IsSheaf J F
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.isRegular_X : ∀ {R : Type u} {σ : Type u_1} {n : σ} [inst : CommSemiring R], IsRegular (MvPolynomial.X n)
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.HeightOneSpectrum.natGenerator.congr_simp : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 → Rat.HeightOneSpectrum.natGenerator v = Rat.HeightOneSpectrum.natGenerator v_1
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ιTotal.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂),
  K.ιTotal c₁₂ i₁ i₂ i₁₂ h = K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h
-- Mathlib.RepresentationTheory.Coinduced
Rep.coind'_ext : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  {A : Rep.{max u w, u, v} k G} {f g : ↑(Rep.coind' φ A)},
  (∀ (h : H),
      (Rep.Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Rep.Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)) →
    f = g
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_map : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) (s : NonUnitalSubring R),
  ↑(NonUnitalSubring.map f s) = ⇑f '' ↑s
-- Mathlib.Data.Tree.Basic
_private.Mathlib.Data.Tree.Basic.0.BinaryTree.traverse.match_1.eq_1 : ∀ {α : Type u_1} (motive : BinaryTree α → Sort u_2) (h_1 : Unit → motive BinaryTree.nil)
  (h_2 : (a : α) → (l r : BinaryTree α) → motive (BinaryTree.node a l r)),
  (match BinaryTree.nil with
    | BinaryTree.nil => h_1 ()
    | BinaryTree.node a l r => h_2 a l r) =
    h_1 ()
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  α.IsNonZero →
    ∀ (n : ℤ),
      LieAlgebra.rootSpace H (n • ⇑α + ⇑β) ≠ ⊥ ↔
        n ∈ Finset.Icc (-↑(LieModule.chainBotCoeff (⇑α) β)) ↑(LieModule.chainTopCoeff (⇑α) β)
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.instEquivLike : {G : Type u_4} →
  {H : Type u_5} → [inst : Add G] → [inst_1 : Add H] → {a : G} → {b : H} → EquivLike (AddConstEquiv G H a b) G H
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.smul_sum : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] {α : Type u_1} [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] [inst_4 : DistribSMul α γ]
  {f : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} {c : α}, c • f.sum h = f.sum fun a b => c • h a b
-- Mathlib.Algebra.MvPolynomial.Division
_private.Mathlib.Algebra.MvPolynomial.Division.0.MvPolynomial.«term_%ᵐᵒⁿᵒᵐⁱᵃˡ_» : Lean.TrailingParserDescr
-- Init.Data.Vector.InsertIdx
Vector.getElem_insertIdx_of_lt : ∀ {α : Type u} {n : ℕ} {xs : Vector α n} {x : α} {i k : ℕ} (w : i ≤ n) (h : k < i), (xs.insertIdx i x w)[k] = xs[k]
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₂.eq_1 : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F),
  AlgebraicTopology.DoldKan.Compatibility.equivalence₂ eB hF =
    (AlgebraicTopology.DoldKan.Compatibility.equivalence₁ hF).trans eB.symm
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.map_i : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.IsPreservedBy F],
  (h.map F).i = F.map h.i
-- Lean.Parser.Types
Lean.Parser.Parser.fn : Lean.Parser.Parser → Lean.Parser.ParserFn
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- The context for the `LazyM` monad  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.Context : Type
-- Init.Data.SInt.Lemmas
Int64.maxValue_le_iff : ∀ {a : Int64}, Int64.maxValue ≤ a ↔ a = Int64.maxValue
-- Mathlib.Data.Rat.Cast.CharZero
Rat.cast_add : ∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α] (p q : ℚ), ↑(p + q) = ↑p + ↑q
-- Mathlib.Data.Set.Lattice
/-- A specialization of `mem_iUnion₂`.  -/
Set.mem_biUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : α → Set β} {x : α} {y : β}, x ∈ s → y ∈ t x → y ∈ ⋃ x ∈ s, t x
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.instBEqPoly.beq.match_1.eq_1 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (a b : ℤ)
  (h_1 : (a b : ℤ) → motive (Int.Internal.Linear.Poly.num a) (Int.Internal.Linear.Poly.num b))
  (h_2 :
    (a : ℤ) →
      (a_1 : Int.Internal.Linear.Var) →
        (a_2 : Int.Internal.Linear.Poly) →
          (b : ℤ) →
            (b_1 : Int.Internal.Linear.Var) →
              (b_2 : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a a_1 a_2) (Int.Internal.Linear.Poly.add b b_1 b_2))
  (h_3 : (x x_1 : Int.Internal.Linear.Poly) → motive x x_1),
  (match Int.Internal.Linear.Poly.num a, Int.Internal.Linear.Poly.num b with
    | Int.Internal.Linear.Poly.num a, Int.Internal.Linear.Poly.num b => h_1 a b
    | Int.Internal.Linear.Poly.add a a_1 a_2, Int.Internal.Linear.Poly.add b b_1 b_2 => h_2 a a_1 a_2 b b_1 b_2
    | x, x_1 => h_3 x x_1) =
    h_1 a b
-- Mathlib.Algebra.BigOperators.Finprod
/-- The product of any function over an empty set is `1`.  -/
finprod_mem_empty : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M}, ∏ᶠ (i : α) (_ : i ∈ ∅), f i = 1
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv.fun_cases_unfolding : ∀ (p n : ℕ) (motive : ℕ × ℕ → Prop),
  (∀ (h : 1 < p ∧ n ≠ 0), motive (Nat.maxPowDvdDiv.go n p h)) →
    (¬(1 < p ∧ n ≠ 0) → motive (0, n)) → motive (p.maxPowDvdDiv n)
-- Mathlib.Algebra.Group.Ideal
AddSemigroupIdeal.FG.eq_1 : ∀ {M : Type u_1} [inst : Add M] (I : AddSemigroupIdeal M), I.FG = ∃ s, s.Finite ∧ I = AddSemigroupIdeal.closure s
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableAt_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (x : E), DifferentiableAt 𝕜 0 x
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_le_iff_le_rpow_of_base_lt_one : ∀ {b x y : ℝ}, 0 < b → b < 1 → 0 < x → (Real.logb b x ≤ y ↔ b ^ y ≤ x)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
cpow_eq_nhds' : ∀ {p : ℂ × ℂ}, p.1 ≠ 0 → (fun x => x.1 ^ x.2) =ᶠ[nhds p] fun x => Complex.exp (Complex.log x.1 * x.2)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.LeftHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h).φH = CategoryTheory.CategoryStruct.id h.H
-- Mathlib.RepresentationTheory.Induced
/-- Given a group hom `φ : G →* H` and `A : Rep k G`, the functor `Rep k H ⥤ ModuleCat k` sending
`B ↦ (Ind(φ)(A) ⊗ B))_H` is naturally isomorphic to the one sending `B ↦ (A ⊗ Res(φ)(B))_G`.  -/
Rep.coinvariantsTensorIndNatIso : {k : Type u} →
  [inst : CommRing k] →
    {G H : Type u} →
      [inst_1 : Group G] →
        [inst_2 : Group H] →
          (φ : G →* H) →
            (A : Rep.{u, u, u} k G) →
              (Rep.coinvariantsTensor k H).obj (Rep.ind φ A) ≅
                (Rep.resFunctor φ).comp ((Rep.coinvariantsTensor k G).obj A)
-- Init.Data.List.Lemmas
List.replace_cons_self : ∀ {α : Type u_1} [inst : BEq α] {as : List α} {b : α} [LawfulBEq α] {a : α}, (a :: as).replace a b = b :: as
-- Mathlib.Order.Partition.Equipartition
Finpartition.IsEquipartition.card_part_le_average_add_one : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {P : Finpartition s},
  P.IsEquipartition → t ∈ P.parts → t.card ≤ s.card / P.parts.card + 1
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- In a linear `SuccOrder` that's also a `PredOrder`, `IsSuccArchimedean` and `IsPredArchimedean`
are equivalent.  -/
LinearOrder.isSuccArchimedean_iff_isPredArchimedean : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : PredOrder ι],
  IsSuccArchimedean ι ↔ IsPredArchimedean ι
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.SectionState.mk.inj : ∀ {α : Type} {results : Array (Mathlib.Tactic.ClickSuggestions.Result α)} {errors : Array ProofWidgets.Html}
  {results_1 : Array (Mathlib.Tactic.ClickSuggestions.Result α)} {errors_1 : Array ProofWidgets.Html},
  { results := results, errors := errors } = { results := results_1, errors := errors_1 } →
    results = results_1 ∧ errors = errors_1
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIsReduced : CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms fun x => AlgebraicGeometry.IsReduced x
-- Mathlib.Topology.Algebra.Support
notMem_mulTSupport_iff_eventuallyEq : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] {f : α → β} {x : α},
  x ∉ mulTSupport f ↔ f =ᶠ[nhds x] 1
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homRestrict_comp_extendMap_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {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'} {L L' : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (ψ : K ⟶ L.extend e) (β : L ⟶ L') {Z : HomologicalComplex C c} (h : L' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (e.homRestrict (CategoryTheory.CategoryStruct.comp ψ (HomologicalComplex.extendMap β e))) h =
    CategoryTheory.CategoryStruct.comp (e.homRestrict ψ) (CategoryTheory.CategoryStruct.comp β h)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.verts_sup : ∀ {V : Type u} {G : SimpleGraph V} (G₁ G₂ : G.Subgraph), (G₁ ⊔ G₂).verts = G₁.verts ∪ G₂.verts
-- Mathlib.Analysis.Analytic.Constructions
/-- A function is analytic at a point iff it is analytic after scalar
multiplication with a non-vanishing analytic function.  -/
analyticAt_iff_analytic_fun_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕝 : Type u_8}
  [inst_5 : NormedDivisionRing 𝕝] [inst_6 : NormedAlgebra 𝕜 𝕝] [inst_7 : Module 𝕝 F] [IsBoundedSMul 𝕝 F]
  [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E},
  AnalyticAt 𝕜 f z → f z ≠ 0 → (AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (fun z => f z • g z) z)
-- Mathlib.RingTheory.TotallySplit
/-- If `R` is finite split over a field `k`, the `k`-rational points of `R`
are in one-to-one correspondence with its prime spectrum.  -/
Algebra.IsFiniteSplit.algHomEquivPrimeSpectrum : (k : Type u_1) →
  (R : Type u_2) →
    [inst : Field k] →
      [inst_1 : CommRing R] → [inst_2 : Algebra k R] → [Algebra.IsFiniteSplit k R] → (R →ₐ[k] k) ≃ PrimeSpectrum R
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mul_mem_sup : ∀ {G : Type u_1} [inst : Group G] {S T : Subgroup G} {x y : G}, x ∈ S → y ∈ T → x * y ∈ S ⊔ T
-- Init.Core
false_imp_iff : ∀ (a : Prop), False → a ↔ True
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Decl.atom.injEq : ∀ {α : Type} (idx idx_1 : α), (Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.atom idx_1) = (idx = idx_1)
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
/-- The vertex group at `c`.  -/
CategoryTheory.Groupoid.vertexGroup : {C : Type u} → [inst : CategoryTheory.Groupoid C] → (c : C) → Group (c ⟶ c)