mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Slice.Array.Lemmas
Subarray.toArray_eq_sliceToArray : ∀ {α : Type u} {s : Subarray α}, Std.Slice.toArray s = Std.Slice.toArray s
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExSum.add.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {a b : Q(«$α»)}
  {a_1 : Mathlib.Tactic.Ring.Common.ExProd BaseType sα a} {a_2 : Mathlib.Tactic.Ring.Common.ExSum BaseType sα b}
  {a_3 : Mathlib.Tactic.Ring.Common.ExProd BaseType sα a} {a_4 : Mathlib.Tactic.Ring.Common.ExSum BaseType sα b},
  Mathlib.Tactic.Ring.Common.ExSum.add a_1 a_2 = Mathlib.Tactic.Ring.Common.ExSum.add a_3 a_4 → a_1 = a_3 ∧ a_2 = a_4
-- Mathlib.Data.Set.Function
Set.preimage_invFun_of_mem : ∀ {α : Type u_1} {β : Type u_2} [n : Nonempty α] {f : α → β},
  Function.Injective f → ∀ {s : Set α}, Classical.choice n ∈ s → Function.invFun f ⁻¹' s = f '' s ∪ (Set.range f)ᶜ
-- Mathlib.GroupTheory.CoprodI
/-- Every nonempty `Word M` can be constructed as a `NeWord M i j`  -/
Monoid.CoprodI.NeWord.of_word : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (w : Monoid.CoprodI.Word M),
  w ≠ Monoid.CoprodI.Word.empty → ∃ i j w', w'.toWord = w
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_add_mod : ∀ (a b : Ordinal.{u_4}), b * (a / b) + a % b = a
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Semiring.type : Lean.Meta.Grind.Arith.CommRing.Semiring → Lean.Expr
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets_zero_right : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {π : ι → Set (Set Ω)}, ProbabilityTheory.Kernel.iIndepSets π κ 0
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.generate_le : ∀ {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {s : Set (Set α)},
  (∀ t ∈ s, d.Has t) → MeasurableSpace.DynkinSystem.generate s ≤ d
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.Hom.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} {x y : HP.Hom HP'},
  x = y ↔ x.homₚ = y.homₚ ∧ x.hom = y.hom
-- Mathlib.Topology.Algebra.MulAction
vadd_set_closure_subset : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : VAdd M X]
  [ContinuousVAdd M X] (K : Set M) (L : Set X), closure K +ᵥ closure L ⊆ closure (K +ᵥ L)
-- Mathlib.Logic.Equiv.Set
Equiv.image_strictAnti : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {e : α ≃ β} (s : Set α),
  StrictAnti ⇑e → StrictAnti ⇑(e.image s)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.add_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z : C} {n : ℕ} (α₁ α₂ : CategoryTheory.Abelian.Ext X Y n) {m : ℕ}
  (β : CategoryTheory.Abelian.Ext Y Z m) {p : ℕ} (h : n + m = p), (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.pow_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f : CauSeq β abv) (n i : ℕ), ↑(f ^ n) i = ↑f i ^ n
-- Lean.Message
/-- The traced action succeeded (✅️, `checkEmoji`).  -/
Lean.TraceResult.success : Lean.TraceResult
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ico_succ_sub_top : ∀ {M : Type u_4} (f : ℕ → M) {m n : ℕ} [inst : AddCommGroup M],
  m ≤ n → ∑ i ∈ Finset.Ico m (n + 1), f i - f n = ∑ i ∈ Finset.Ico m n, f i
-- Mathlib.Order.Filter.Basic
Filter.mem_inf_principal : ∀ {α : Type u} {f : Filter α} {s t : Set α}, s ∈ f ⊓ Filter.principal t ↔ {x | x ∈ t → x ∈ s} ∈ f
-- Mathlib.RingTheory.HopkinsLevitzki
isArtinianRing_iff_krullDimLE_zero : ∀ {R : Type u_3} [inst : CommRing R] [IsNoetherianRing R], IsArtinianRing R ↔ Ring.KrullDimLE 0 R
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If `IsCyclotomicExtension {n} K L`, then `L` is the splitting field of `X ^ n - 1`.  -/
IsCyclotomicExtension.isSplittingField_X_pow_sub_one : ∀ (n : ℕ) [NeZero n] (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [IsCyclotomicExtension {n} K L], Polynomial.IsSplittingField K L (Polynomial.X ^ n - 1)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_sub_Ico : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a - x) ⁻¹' Set.Ico b c = Set.Ioc (a - c) (a - b)
-- Init.Data.BitVec.Lemmas
BitVec.toFin_umod : ∀ {w : ℕ} {x y : BitVec w}, (x % y).toFin = x.toFin % y.toFin
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.mk.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (I : Type w) (obj : I → C), sizeOf { I := I, obj := obj } = 1 + sizeOf I
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.add : {α : Type u} →
  [inst : Lean.Grind.NatModule α] →
    Lean.Grind.IntModule.OfNatModule.Q α → Lean.Grind.IntModule.OfNatModule.Q α → Lean.Grind.IntModule.OfNatModule.Q α
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_eq_cons : ∀ {m n : ℕ}, m + 1 < n → (m<...n).toList = (m + 1) :: ((m + 1)<...n).toList
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S),
  p.Monic → (Polynomial.map f p).Monic
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
PiTensorProduct.dualDistrib.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Finite ι], PiTensorProduct.dualDistrib = PiTensorProduct.dualDistrib
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.instIsMulCommutativeSubtypeMem : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [IsMulCommutative G], IsMulCommutative ↥H
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If `f` has a formal Taylor series `p` up to order `1` on `{x} ∪ s`, where `s` is a convex set,
then `f` is Lipschitz in a neighborhood of `x` within `s`.  -/
HasFTaylorSeriesUpToOn.exists_lipschitzOnWith : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {p : E → FormalMultilinearSeries ℝ E F} {s : Set E} {x : E},
  HasFTaylorSeriesUpToOn 1 f p (insert x s) → Convex ℝ s → ∃ K, ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
-- Mathlib.Data.FunLike.Equiv
/-- The coercion to a function in the backwards direction.  -/
EquivLike.inv : {E : Sort u_1} → {α : outParam (Sort u_2)} → {β : outParam (Sort u_3)} → [self : EquivLike E α β] → E → β → α
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.handleSignatureHelp : Lean.Lsp.SignatureHelpParams → Lean.Server.RequestM (Lean.Server.RequestTask (Option Lean.Lsp.SignatureHelp))
-- Lean.Compiler.MetaAttr
/-- Returns the IR phases of the given declaration that should be considered accessible. Does not take
additional IR loaded for language server purposes into account.
 -/
Lean.getIRPhases : Lean.Environment → Lean.Name → Lean.IRPhases
-- Mathlib.Order.WithBot
WithBot.lt_iff_exists_coe : ∀ {α : Type u_1} [inst : LT α] {x y : WithBot α}, x < y ↔ ∃ b, y = ↑b ∧ x < ↑b
-- Init.Data.String.Basic
ByteArray.validateUTF8 : ByteArray → Bool
-- Mathlib.Computability.NFA
NFA.Path.cons : {α : Type u} →
  {σ : Type v} →
    {M : NFA α σ} → (t s u : σ) → (a : α) → (x : List α) → t ∈ M.step s a → M.Path t u x → M.Path s u (a :: x)
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase.eq_1 : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰)
  [inst_2 : Small.{u, u_1} 𝒰.I₀] [inst_3 : Quiver.IsThin 𝒰.I₀],
  d.toBase =
    CategoryTheory.Limits.colimit.desc d.functor
      { pt := S,
        ι :=
          CategoryTheory.CategoryStruct.comp d.natTrans
            (AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirectedHomBase 𝒰) }
-- Mathlib.Data.Finset.Fin
Finset.attachFin_ssubset_attachFin_iff : ∀ {n : ℕ} {s t : Finset ℕ} (hs : ∀ m ∈ s, m < n) (ht : ∀ m ∈ t, m < n), s.attachFin hs ⊂ t.attachFin ht ↔ s ⊂ t
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- There exists a compatible Polish topology.  -/
StandardBorelSpace.polish : ∀ {α : Type u_1} {inst : MeasurableSpace α} [self : StandardBorelSpace α], ∃ x, BorelSpace α ∧ PolishSpace α
-- Mathlib.CategoryTheory.Discrete.SumsProducts
_private.Mathlib.CategoryTheory.Discrete.SumsProducts.0.CategoryTheory.Discrete.productEquiv.match_5.eq_1 : ∀ {J : Type u_1} {K : Type u_2} {X Y : CategoryTheory.Discrete J × CategoryTheory.Discrete K}
  (motive : (X ⟶ Y) → Sort u_3) (f₁ : X.1 ⟶ Y.1) (f₂ : X.2 ⟶ Y.2)
  (h_1 : (f₁ : X.1 ⟶ Y.1) → (f₂ : X.2 ⟶ Y.2) → motive (f₁, f₂)),
  (match (f₁, f₂) with
    | (f₁, f₂) => h_1 f₁ f₂) =
    h_1 f₁ f₂
-- Init.Data.Vector.OfFn
Vector.ofFn_add : ∀ {α : Type u_1} {n m : ℕ} {f : Fin (n + m) → α},
  Vector.ofFn f = (Vector.ofFn fun i => f (Fin.castLE ⋯ i)) ++ Vector.ofFn fun i => f (Fin.natAdd n i)
-- Lean.Util.PtrSet
Lean.Ptr.mk : {α : Type u} → α → Lean.Ptr α
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiffOn.norm_sq : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E}
  {s : Set G} {n : WithTop ℕ∞}, ContDiffOn ℝ n f s → ContDiffOn ℝ n (fun y => ‖f y‖ ^ 2) s
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
fderiv.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → f x ≠ 0 → fderiv ℝ (fun x => Real.log (f x)) x = (f x)⁻¹ • fderiv ℝ f x
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.mul_bdd : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜]
  {f g : α → 𝕜} {c : ℝ},
  MeasureTheory.Integrable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      (∀ᵐ (x : α) ∂μ, ‖g x‖ ≤ c) → MeasureTheory.Integrable (fun x => f x * g x) μ
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- The infinite place of `ℚ`, coming from the canonical map `ℚ → ℂ`.  -/
Rat.infinitePlace : NumberField.InfinitePlace ℚ
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.update_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : DecidableEq 𝕜] {f : 𝕜 → E} {z w : 𝕜} {e : E},
  MeromorphicAt (Function.update f w e) z ↔ MeromorphicAt f z
-- Mathlib.Analysis.Normed.Group.Basic
norm_pos_iff : ∀ {E : Type u_5} [inst : NormedAddGroup E] {a : E}, 0 < ‖a‖ ↔ a ≠ 0
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.isCircuit_iff_forall_ssubset : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- An auxiliary structure, used to define `S.index`.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → J.Cover X → Type (max u v)
-- Mathlib.RingTheory.Smooth.Kaehler
derivationOfSectionOfKerSqZero.congr_simp : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra R S] (f : P →ₐ[R] S) (hf' : RingHom.ker f ^ 2 = ⊥) (g g_1 : S →ₐ[R] P)
  (e_g : g = g_1) (hg : f.comp g = AlgHom.id R S),
  derivationOfSectionOfKerSqZero f hf' g hg = derivationOfSectionOfKerSqZero f hf' g_1 ⋯
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.comap_inv_atBot : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G],
  Filter.comap Inv.inv Filter.atBot = Filter.atTop
-- Mathlib.Topology.Compactness.SigmaCompact
isCompact_compactCovering : ∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X] (n : ℕ), IsCompact (compactCovering X n)
-- Mathlib.RingTheory.Adjoin.PowerBasis
Algebra.adjoin.powerBasisAux.eq_1 : ∀ {K : Type u_1} {S : Type u_2} [inst : Field K] [inst_1 : CommRing S] [inst_2 : Algebra K S] {x : S}
  (hx : IsIntegral K x), Algebra.adjoin.powerBasisAux hx = Module.Basis.mk ⋯ ⋯
-- Init.Data.Int.Order
Int.lt_irrefl : ∀ (a : ℤ), ¬a < a
-- Mathlib.Topology.QuasiSeparated
IsQuasiSeparated.of_quasiSeparatedSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] (s : Set α), IsQuasiSeparated s
-- Mathlib.Analysis.Normed.Module.Complemented
Submodule.closedComplemented_iff_isClosed_exists_isClosed_isCompl : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {p : Subspace 𝕜 E},
  Submodule.ClosedComplemented p ↔ IsClosed ↑p ∧ ∃ q, IsClosed ↑q ∧ IsCompl p q
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.diff_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ \ t₂).Equiv (t₃ \ t₄)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Antitone.neg : ∀ {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftMono α] [AddRightMono α]
  [inst_4 : Preorder β] {f : β → α}, Antitone f → Monotone fun x => -f x
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.forget₂AddCommGroup_preservesFilteredColimits : ∀ {R : Type u} [inst : Ring R],
  CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Mathlib.Topology.EMetricSpace.Defs
WeakEMetricSpace.ext : ∀ {α : Type u_2} [inst : TopologicalSpace α] {m m' : WeakEMetricSpace α}, m.toEDist = m'.toEDist → m = m'
-- Mathlib.Order.Atoms
/-- An order is strongly atomic if every nontrivial interval `[a, b]`
contains an element covering `a`.  -/
IsStronglyAtomic : (α : Type u_5) → [Preorder α] → Prop
-- Batteries.Recycling.RBTree.Basic
/-- Insert all elements from a collection into a `RBSet α cmp`.
 -/
RBTree.RBSet.insertMany : {ρ : Type u_1} →
  {α : Type u_2} → {cmp : α → α → Ordering} → [ForIn Id ρ α] → RBTree.RBSet α cmp → ρ → RBTree.RBSet α cmp
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_whiskerRight : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id X) Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.ext_iff : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} {e₁ e₂ : AddConstEquiv G H a b},
  e₁ = e₂ ↔ ∀ (x : G), e₁ x = e₂ x
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₀_comp : ∀ {X Y : SSet} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp SSet.ι₀
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (SSet.stdSimplex.obj { len := 1 })) =
    CategoryTheory.CategoryStruct.comp f SSet.ι₀
-- Mathlib.RingTheory.Localization.Ideal
/-- **Alias** of `IsLocalization.ideal_eq_iInf_under_map_away`. -/
IsLocalization.ideal_eq_iInf_comap_map_away : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Finset R},
  Ideal.span ↑S = ⊤ → ∀ (I : Ideal R), I = ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I)
-- Mathlib.Algebra.Symmetrized
SymAlg.mul_comm : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : AddCommSemigroup α] [inst_2 : One α] [inst_3 : OfNat α 2]
  [inst_4 : Invertible 2] (a b : αˢʸᵐ), a * b = b * a
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousOn_ciSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {ι : Sort u_4} {δ' : Type u_6}
  [inst_1 : ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'},
  (∀ x ∈ s, BddAbove (Set.range fun i => f i x)) →
    (∀ (i : ι), LowerSemicontinuousOn (f i) s) → LowerSemicontinuousOn (fun x' => ⨆ i, f i x') s
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.instBot : {ι : Type u_1} → Bot (AbstractSimplicialComplex ι)
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_three : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₂₃ : i₁ ⟶ i₃) (f₃₄ : i₂ ⟶ i₄) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄),
  (CategoryTheory.ComposableArrows.fourδ₃Toδ₂ f₁ f₂ f₃ f₄ f₂₃ f₃₄ h₂₃ h₃₄).app 3 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃₄).obj 3)
-- Mathlib.NumberTheory.FLT.Four
not_fermat_42 : ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → a ^ 4 + b ^ 4 ≠ c ^ 2
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- The type of open normal subgroups of a topological additive group.  -/
OpenNormalAddSubgroup : (G : Type u) → [AddGroup G] → [TopologicalSpace G] → Type u
-- Mathlib.Topology.Order.LiminfLimsup
/-- Every cluster point `x` of a filter `f` is greater than or equal to `f.limsInf`.  -/
ClusterPt.limsInf_le : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {f : Filter α} {x : α},
  ClusterPt x f → autoParam (Filter.IsBounded (fun x1 x2 => x1 ≥ x2) f) ClusterPt.limsInf_le._auto_1 → f.limsInf ≤ x
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- **Alias** of the reverse direction of `affineIndependent_smul`. -/
AffineIndependent.smul : ∀ (k : Type u_1) {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_4}
  {G : Type u_5} [inst_3 : Group G] [inst_4 : DistribMulAction G V] [SMulCommClass G k V] {p : ι → V} {a : G},
  AffineIndependent k p → AffineIndependent k (a • p)
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
/-- A bilinear form composed with a `LinearEquiv` is isometric to itself.  -/
LinearMap.BilinForm.isometryEquivOfCompLinearEquiv : {R : Type u_1} →
  {M : Type u_2} →
    {M₁ : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₁] →
            [inst_3 : Module R M] →
              [inst_4 : Module R M₁] → (B : LinearMap.BilinForm R M) → (f : M₁ ≃ₗ[R] M) → B.IsometryEquiv (B.comp ↑f ↑f)
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.HD_lipschitz_aux2 : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [Nonempty X] [Nonempty Y]
  (f g : GromovHausdorff.Cb✝ X Y), ⨆ y, ⨅ x, f (Sum.inl x, Sum.inr y) ≤ (⨆ y, ⨅ x, g (Sum.inl x, Sum.inr y)) + dist f g
-- Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
/-- Alternate statement of `AlgEquiv.eq_linearEquivConjAlgEquiv` for when `V = W`.  -/
Module.End.mulSemiringActionToAlgEquiv_conjAct_surjective : ∀ {K : Type u_1} {V : Type u_2} [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], Function.Surjective (MulSemiringAction.toAlgEquiv K (Module.End K V))
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_map : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (S : IntermediateField K L) (f : L →ₐ[K] L'),
  ↑(IntermediateField.map f S) = ⇑f '' ↑S
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.pentagon : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.associator W X Y).hom
        (CategoryTheory.CategoryStruct.id Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator W (X ⨯ Y) Z).hom
        (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W)
          (CategoryTheory.Limits.prod.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator (W ⨯ X) Y Z).hom
      (CategoryTheory.Limits.prod.associator W X (Y ⨯ Z)).hom
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.flip_flip : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.BilinForm.flipHom ≪≫ₗ LinearMap.BilinForm.flipHom = LinearEquiv.refl R (LinearMap.BilinForm R M)
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.map_succ : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  (self : F.WellOrderInductionData) (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (self.succ j hj x) = x
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.containsIdentities : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q],
  (RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q) → P.ContainsIdentities
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α},
  (Std.DTreeMap.filter f t).getKey? k = (t.getKey? k).pfilter fun x h' => f x (Std.DTreeMap.Const.get t x ⋯)
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- The tangent space at the identity of an additive Lie group is a Lie ring, for the
bracket given by the Lie bracket of invariant vector fields.  -/
instLieRingAddGroupLieAlgebra : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              {I : ModelWithCorners 𝕜 E H} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : AddGroup G] →
                        [LieAddGroup I (minSmoothness 𝕜 3) G] → [CompleteSpace E] → LieRing (AddGroupLieAlgebra I G)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofHom_nsmul : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) (n : ℕ), Rep.ofHom (n • f) = n • Rep.ofHom f
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.Context.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (pos : Lean.Lsp.Position) (completionInfoPos : ℕ) (uri_1 : Lean.Lsp.DocumentUri)
  (pos_1 : Lean.Lsp.Position) (completionInfoPos_1 : ℕ),
  ({ uri := uri, pos := pos, completionInfoPos := completionInfoPos } =
      { uri := uri_1, pos := pos_1, completionInfoPos := completionInfoPos_1 }) =
    (uri = uri_1 ∧ pos = pos_1 ∧ completionInfoPos = completionInfoPos_1)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instSub : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Sub Y] → Sub (LocallyConstant X Y)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.«priority_%» : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.compl_apply_diag : ∀ {α : Type u_1} {V : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq V] (A : Matrix V V α) [inst_2 : Zero α]
  [inst_3 : One α] (i : V), A.compl i i = 0