mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Galois.GaloisObjects
/-- The natural action of `Aut X` on `F.obj X`.  -/
CategoryTheory.PreGaloisCategory.autMulFiber : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) → (X : C) → MulAction (CategoryTheory.Aut X) (F.obj X).obj
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.π_colimitOfIsReflexivePairIsoCoequalizer_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B}
  [inst_1 : CategoryTheory.IsReflexivePair f g] [h : CategoryTheory.Limits.HasCoequalizer f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g)
      CategoryTheory.Limits.colimitOfIsReflexivePairIsoCoequalizer.inv =
    CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.ofIsReflexivePair f g)
      CategoryTheory.Limits.WalkingReflexivePair.zero
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.ParserContext.mk.sizeOf_spec : ∀ (toParserContextCore : Lean.Parser.ParserContextCore),
  sizeOf { toParserContextCore := toParserContextCore } = 1 + sizeOf toParserContextCore
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.instInhabitedRing.default : Lean.Meta.Grind.Arith.CommRing.Ring
-- Mathlib.MeasureTheory.Group.AEStabilizer
MulAction.aestabilizer_of_aeconst : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α},
  Filter.EventuallyConst s (MeasureTheory.ae μ) → MulAction.aestabilizer G μ s = ⊤
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mem_mk : ∀ {G : Type u_1} [inst : AddGroup G] {s : AddSubmonoid G} {x : G} (h_neg : ∀ {x : G}, x ∈ s.carrier → -x ∈ s.carrier),
  x ∈ { toAddSubmonoid := s, neg_mem' := h_neg } ↔ x ∈ s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPullback.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C)
  (h : CategoryTheory.Limits.IsLimit sq.pullbackCone), sq.IsPullback
-- Init.Data.Vector.InsertIdx
Vector.eraseIdx_insertIdx_self : ∀ {α : Type u} {a : α} {n i : ℕ} {xs : Vector α n} {h : i ≤ n}, (xs.insertIdx i a h).eraseIdx i ⋯ = xs
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_right_inj : ∀ {a b c : ENNReal}, a ≠ ⊤ → (a + b = a + c ↔ b = c)
-- Lean.Meta.MkIffOfInductiveProp
/-- Splits the goal `n` times via `refine ⟨?_,?_⟩`, and then applies `constructor` to
close the resulting subgoals.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.splitThenConstructor : Lean.MVarId → ℕ → Lean.MetaM Unit
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_mod_mul : ∀ (x y z : Ordinal.{u_4}), x * y % (x * z) = x * (y % z)
-- Mathlib.Data.Prod.TProd
List.TProd.elim_self : ∀ {ι : Type u} {α : ι → Type v} {i : ι} {l : List ι} [inst : DecidableEq ι] (v : List.TProd α (i :: l)), v.elim ⋯ = v.1
-- Mathlib.Data.Finsupp.Order
Finsupp.mapDomain_tsub : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : CanonicallyOrderedAdd α] [inst_3 : Sub α] [inst_4 : OrderedSub α] {f : ι → κ},
  Function.Injective f →
    ∀ (f1 f2 : ι →₀ α), Finsupp.mapDomain f (f1 - f2) = Finsupp.mapDomain f f1 - Finsupp.mapDomain f f2
-- Mathlib.Order.Category.OmegaCompletePartialOrder
/-- The underlying type.  -/
ωCPO.carrier : ωCPO → Type u
-- Mathlib.Order.MinMax
max_min_distrib_left : ∀ {α : Type u} [inst : LinearOrder α] (a b c : α), max a (min b c) = min (max a b) (max a c)
-- Mathlib.Data.NNRat.Defs
Rat.coe_toNNRat : ∀ (q : ℚ), 0 ≤ q → ↑q.toNNRat = q
-- Mathlib.Analysis.Calculus.Deriv.Prod
hasDerivAtFilter_finCons : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : (i : Fin n.succ) → F' i} {l : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) φ' l ↔
    HasDerivAtFilter φ (φ' 0) l ∧ HasDerivAtFilter φs (fun i => φ' i.succ) l
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι]
  (hτ : MeasureTheory.IsStoppingTime f τ) (hπ : MeasureTheory.IsStoppingTime f π) (s : Set Ω),
  MeasurableSet (s ∩ {ω | τ ω ≤ π ω}) ↔ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.mem_center_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] [Module.Free R V]
  [Module.Finite R V] {g : SpecialLinearGroup R V},
  g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.mem_resolventSet_of_left_right_inverse : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a b c : A},
  ((algebraMap R A) r - a) * b = 1 → c * ((algebraMap R A) r - a) = 1 → r ∈ resolventSet R a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_eq_getD_get? : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {a : α} {fallback : β},
      Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = (Std.DHashMap.Internal.Raw₀.Const.get? m a).getD fallback
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ne_endPos_of_slice_ne_endPos : ∀ {s : String.Slice} {p p₀ p₁ : s.Pos} {h₁ : p₀ ≤ p} {h₂ : p ≤ p₁},
  p.slice p₀ p₁ h₁ h₂ ≠ (s.slice p₀ p₁ ⋯).endPos → p ≠ s.endPos
-- Mathlib.Data.Nat.GCD.BigOperators
/-- See `IsCoprime.prod_left` for the corresponding lemma about `IsCoprime`  -/
Nat.Coprime.prod_left : ∀ {ι : Type u_1} {t : Finset ι} {s : ι → ℕ} {x : ℕ}, (∀ i ∈ t, (s i).Coprime x) → (∏ i ∈ t, s i).Coprime x
-- Mathlib.Topology.Separation.Basic
T0Space.mk : ∀ {X : Type u} [inst : TopologicalSpace X], (∀ ⦃x y : X⦄, Inseparable x y → x = y) → T0Space X
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.oreDiv_one_smul : ∀ {M : Type u_3} {X : Type u_4} [inst : Monoid M] {S : Submonoid M} [inst_1 : OreLocalization.OreSet S]
  [inst_2 : MulAction M X] (r : M) (x : OreLocalization S X), (r /ₒ 1) • x = r • x
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedRing.projZeroRingHom'.congr_simp : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜], GradedRing.projZeroRingHom' 𝒜 = GradedRing.projZeroRingHom' 𝒜
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNClique.not_cliqueFree : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α}, G.IsNClique n s → ¬G.CliqueFree n
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.homMk''.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.Grp C} (f : A.X ⟶ B.X)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
        CategoryTheory.MonObj.mul),
  CategoryTheory.Grp.homMk'' f one_f mul_f = CategoryTheory.Grp.homMk f
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.Hom.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C}
  [inst_1 : SizeOf C] (base : ↑X ⟶ ↑Y) (c : Y.presheaf ⟶ (TopCat.Presheaf.pushforward C base).obj X.presheaf),
  sizeOf { base := base, c := c } = 1 + sizeOf base + sizeOf c
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mk : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : LieRingModule L M] →
                (toSubmodule : Submodule R M) →
                  (∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier) → LieSubmodule R L M
-- Mathlib.NumberTheory.Divisors
/-- `Finset.antidiagonal k` embeds as a subset of `Nat.divisorsAntidiagonal (q ^ k)`.  -/
Nat.antidiagonal_map_subset_divisorsAntidiagonal_pow : ∀ {q : ℕ} (hq : 1 < q) (k : ℕ),
  Finset.map ({ toFun := fun k => q ^ k, inj' := ⋯ }.prodMap { toFun := fun k => q ^ k, inj' := ⋯ })
      (Finset.HasAntidiagonal.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_union!_of_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₁ = true → Std.DTreeMap.Internal.Impl.contains k (m₁.union! m₂) = true
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.faithful_whiskeringRight_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} [F.Faithful],
  ((CategoryTheory.Functor.whiskeringRight C D E).obj F).Faithful
-- Mathlib.Data.Stream.Init
Stream'.get_succ_iterate' : ∀ {α : Type u} (n : ℕ) (f : α → α) (a : α), (Stream'.iterate f a).get n.succ = f ((Stream'.iterate f a).get n)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.smul_eq : ∀ {R : Type r} [inst : CommRing R] (P : Fin 3 → R) {u : R}, IsUnit u → ⟦u • P⟧ = ⟦P⟧
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insert.go : ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (k : α),
  m₁.Equiv m₂ → (m₁.insert k).Equiv (m₂.insert k)
-- Lean.HeadIndex
/-- Quick version that may fail if it "hits" a loose bound variable.
This can happen, for example, if the input expression is of the form.
```
let f := fun x => x + 1;
f 0
```
 -/
_private.Lean.HeadIndex.0.Lean.Expr.toHeadIndexQuick? : Lean.Expr → Option Lean.HeadIndex
-- Mathlib.Algebra.Torsor.Basic
Prod.fst_vsub : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup G']
  [inst_2 : AddTorsor G P] [inst_3 : AddTorsor G' P'] (p₁ p₂ : P × P'), (p₁ -ᵥ p₂).1 = p₁.1 -ᵥ p₂.1
-- Mathlib.CategoryTheory.Shift.Pullback
/-- If an adjunction `F ⊣ G` is compatible with `CommShift` structures on `F` and `G`, then
it is also compatible with the pulled back `CommShift` structures by an additive map
`φ : B →+ A`.
 -/
CategoryTheory.Adjunction.commShiftPullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) {D : Type u_4}
  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] [inst_5 : CategoryTheory.HasShift D B]
  {F : CategoryTheory.Functor C D} [inst_6 : F.CommShift B] {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [inst_7 : G.CommShift B] [adj.CommShift B], (CategoryTheory.PullbackShift.adjunction φ adj).CommShift A
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.pointWeightsWithCircumcenter.eq_2 : ∀ {n : ℕ} (i : Fin (n + 1)),
  Affine.Simplex.pointWeightsWithCircumcenter i Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyLT!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited α],
          Std.DTreeMap.Internal.Impl.getKeyLT! k t₁ = Std.DTreeMap.Internal.Impl.getKeyLT! k t₂
-- Mathlib.Order.Fin.Basic
Fin.castAddOrderEmb_apply : ∀ {n : ℕ} (m : ℕ) (a : Fin n), (Fin.castAddOrderEmb m) a = Fin.castAdd m a
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_injective : Function.Injective ⇑GaussianInt.toComplex
-- Mathlib.Topology.Convenient.GeneratedBy
TopologicalSpace.generatedBy_mono : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} {t₁ t₂ : TopologicalSpace Y},
  t₁ ≤ t₂ → TopologicalSpace.generatedBy X ≤ TopologicalSpace.generatedBy X
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- Given a type `e`, an assumption `i : MeasurableSpace e`, and an instance `[BorelSpace e]`,
replace `i` with `borel e`.  -/
Mathlib.Tactic.Borelize.borelToRefl : Lean.Expr → Lean.FVarId → Lean.Elab.Tactic.TacticM Unit
-- Init.Data.Range.Polymorphic.Basic
Std.Rio.Internal.get_elem_helper_upper_open : ∀ {α : Type u} {r : Std.Rio α} {hi a : α} [LE α] [inst : LT α], a ∈ r → r.upper = hi → a < hi
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_intCast_mul : ∀ (x : ENNReal) (n : ℤ) (z : ℝ), x ^ (↑n * z) = (x ^ n) ^ z
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅} {hc : t.minKey he ∈ t}, t.getKey (t.minKey he) hc = t.minKey he
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_const_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a : E → 𝔸},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 a s x → ∀ (b : 𝔸), fderivWithin 𝕜 (fun y => b * a y) s x = b • fderivWithin 𝕜 a s x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.any_eq_true : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [LawfulHashable α] [EquivBEq α] {p : α → β → Bool},
  (↑m).WF →
    ((↑m).any p = true ↔
      ∃ a, ∃ (h : m.contains a = true), p (m.getKey a h) (Std.DHashMap.Internal.Raw₀.Const.get m a h) = true)
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_mono' : ∀ {a b : ENNReal}, a ≤ b → (b = ⊤ → a = ⊤) → a.toReal ≤ b.toReal
-- Mathlib.Algebra.Order.Monovary
antivary_neg_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommGroup β]
  [inst_2 : PartialOrder β] [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β}, Antivary f (-g) ↔ Monovary f g
-- Init.Data.UInt.Bitwise
UInt16.neg_one_or : ∀ {a : UInt16}, -1 ||| a = -1
-- Init.Data.Cast
/-- The canonical homomorphism `Nat → R`. In most use cases, the target type will have a (semi)ring
structure, and this homomorphism should be a (semi)ring homomorphism.

`NatCast` and `IntCast` exist to allow different libraries with their own types that can be notated
as natural numbers to have consistent `simp` normal forms without needing to create coercion
simplification sets that are aware of all combinations. Libraries should make it easy to work with
`NatCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus a
`NatCast R` instance) whenever `R` is an additive monoid with a `1`.

The prototypical example is `Int.ofNat`.
 -/
NatCast : Type u → Type u
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.toList_roc : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered →
    ∀ (lowerBound upperBound : α),
      Std.Slice.toList (Std.Roc.Sliceable.mkSlice t lowerBound<...=upperBound) =
        List.filter (fun e => decide ((compare e.fst lowerBound).isGT = true ∧ (compare e.fst upperBound).isLE = true))
          t.toList
-- Lean.Declaration
Lean.instInhabitedConstructor.default : Lean.Constructor
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.setGcd_mono : ∀ {s t : Set ℕ}, s ⊆ t → Nat.setGcd t ∣ Nat.setGcd s
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- A product of path-connected, locally path-connected spaces is locally path-connected. Note
that an arbitrary product of locally path-connected spaces need not be locally path-connected, so
the path-connectedness assumption cannot be dropped entirely (though it can be dropped for
finitely many factors, see `Pi.locallyPathConnectedSpace_of_finite_not_pathConnectedSpace`).  -/
Pi.locallyPathConnectedSpace : ∀ {ι : Type u_3} {Z : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (Z i)]
  [∀ (i : ι), LocallyPathConnectedSpace (Z i)] [∀ (i : ι), PathConnectedSpace (Z i)],
  LocallyPathConnectedSpace ((i : ι) → Z i)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.coe_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (f : M ≃* N) (hf1 : Continuous f.toFun) (hf2 : Continuous f.invFun),
  ⇑{ toMulEquiv := f, continuous_toFun := hf1, continuous_invFun := hf2 } = ⇑f
-- Mathlib.CategoryTheory.Widesubcategory
/-- The induced functor `wideInducedFunctor F P : InducedWideCategory D F P ⥤ D`
is faithful.  -/
CategoryTheory.InducedWideCategory.faithful : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] (F : C → D)
  (P : CategoryTheory.MorphismProperty D) [inst_1 : P.IsMultiplicative],
  (CategoryTheory.wideInducedFunctor F P).Faithful
-- Init.Data.Bool
Bool.eq_and_self : ∀ {a b : Bool}, b = (a && b) ↔ b = true → a = true
-- Mathlib.Data.Multiset.UnionInter
Multiset.zero_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, 0 ∪ s = s
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMap_app : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A] {X : C}
  (data : F.PreOneHypercoverDenseData X) {P Q : CategoryTheory.Functor C₀ᵒᵖ A} (f : P ⟶ Q)
  (x : CategoryTheory.Limits.WalkingMulticospan data.multicospanShape),
  (data.multicospanMap f).app x =
    match x with
    | CategoryTheory.Limits.WalkingMulticospan.left i => f.app (Opposite.op (data.X i))
    | CategoryTheory.Limits.WalkingMulticospan.right j => f.app (Opposite.op (data.Y j.snd))
-- Lean.Elab.Tactic.Omega.Core
/-- A delayed proof that a constraint is satisfied at the atoms.
 -/
Lean.Elab.Tactic.Omega.Proof : Type
-- Mathlib.CategoryTheory.Subobject.Limits
/-- Postcomposing by a monomorphism does not change the kernel subobject.  -/
CategoryTheory.Limits.kernelSubobject_comp_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {Z : C} (h : Y ⟶ Z) [inst_3 : CategoryTheory.Mono h],
  CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.Limits.kernelSubobject f
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mk : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] →
          [inst_3 : Module R M] → (toSubmodule : Submodule R M) → IsClosed toSubmodule.carrier → ClosedSubmodule R M
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.op_δ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.op.δ = S.δ.op
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.constructor.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.constructor = 1
-- Mathlib.LinearAlgebra.Semisimple
Module.End.eq_zero_of_isNilpotent_of_isFinitelySemisimple : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M}, IsNilpotent f → f.IsFinitelySemisimple → f = 0
-- Mathlib.Topology.Order.Lattice
ContinuousAt.sup' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Max L]
  [ContinuousSup L] {f g : X → L} {x : X}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (f ⊔ g) x
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.adjoin_eq_top_iff_of_isAlgebraic : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E},
  (∀ x ∈ S, IsAlgebraic F x) → (IntermediateField.adjoin F S = ⊤ ↔ Algebra.adjoin F S = ⊤)
-- Mathlib.NumberTheory.Primorial
primorial_two : primorial 2 = 2
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.toCircle_nsmul : ∀ {T : ℝ} (x : AddCircle T) (n : ℕ), (n • x).toCircle = x.toCircle ^ n
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.constantCoeff_X : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (s : σ), MvPowerSeries.constantCoeff (MvPowerSeries.X s) = 0
-- Std.Time.Duration
Std.Time.instReprDuration.repr : Std.Time.Duration → ℕ → Std.Format
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO_def : ∀ {α : Type u_18} {E : Type u_19} {F : Type u_20} [inst : Norm E] [inst_1 : Norm F] (l : Filter α) (f : α → E)
  (g : α → F), f =O[l] g = ∃ c, Asymptotics.IsBigOWith c l f g
-- Mathlib.Topology.Algebra.Order.Field
tendsto_const_mul_pow_nhds_iff : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {n : ℕ} {c d : 𝕜},
  c ≠ 0 → (Filter.Tendsto (fun x => c * x ^ n) Filter.atTop (nhds d) ↔ n = 0 ∧ c = d)
-- Std.Sat.AIG.CNF
/-- The invariant that `cnf` has to maintain as we build it up.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.inv : ∀ {aig : Std.Sat.AIG ℕ} (self : Std.Sat.AIG.toCNF.State✝ aig),
  Std.Sat.AIG.toCNF.State.Inv✝ aig (Std.Sat.AIG.toCNF.State.cnf✝ self)
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Measure.integral_condKernel : ∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ] {E : Type u_3}
  {f : β × Ω → E} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace ℝ E],
  MeasureTheory.Integrable f ρ → ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.finsuppProd_single : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [inst : CommSemiring R] [inst_1 : CommMonoid M]
  [inst_2 : AddCommMonoid N] (f : ι →₀ N) (m : ι → N → M) (r : ι → N → R),
  (f.prod fun i n => MonoidAlgebra.single (m i n) (r i n)) = MonoidAlgebra.single (f.prod m) (f.prod r)
-- Mathlib.Order.Category.Lat
/-- The type of morphisms in `Lat R`.  -/
Lat.Hom : Lat → Lat → Type u
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.aevalEquiv.congr_simp : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (hx : AlgebraicIndependent R x), hx.aevalEquiv = hx.aevalEquiv
-- Mathlib.Order.Disjoint
Subsingleton.instComplementedLattice : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] [Subsingleton α], ComplementedLattice α
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPStructureInstancesFlatten : Lean.Options → Bool
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.mem_pointwise_smul_iff_inv_smul_mem : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S : Ideal R} {x : R}, x ∈ a • S ↔ a⁻¹ • x ∈ S
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_ne_zero_iff : ∀ {x y : ℂ}, x ^ y ≠ 0 ↔ x ≠ 0 ∨ y = 0