mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.HasLaw
MeasureTheory.MeasurePreserving.comp_hasLaw : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω} {𝓨 : Type u_3} {m𝓨 : MeasurableSpace 𝓨}
  {ν : MeasureTheory.Measure 𝓨} {Y : 𝓧 → 𝓨},
  MeasureTheory.MeasurePreserving Y μ ν → ProbabilityTheory.HasLaw X μ P → ProbabilityTheory.HasLaw (Y ∘ X) ν P
-- Lean.Data.KVMap
Lean.instCoeSyntaxDataValue : Coe Lean.Syntax Lean.DataValue
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_comm : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, (fun x => f₁ x - f₂ x) =o[l] g ↔ (fun x => f₂ x - f₁ x) =o[l] g
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_eq_aleph0 : ∀ (α : Type u_1) [Countable α] [Infinite α], Cardinal.mk α = Cardinal.aleph0
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.t2Space : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E]
  [T2Space F] (b : B), T2Space (E b)
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.union : ∀ {α : Type v} {s t : Set α} [inst : LinearOrder α], IsClub s → IsClub t → IsClub (s ∪ t)
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.presheafFiber.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ Φ_1 : J.Point),
  Φ = Φ_1 →
    ∀ {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
      [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A], Φ.presheafFiber = Φ_1.presheafFiber
-- Mathlib.RingTheory.FractionalIdeal.Basic
Nat.unaryCast.eq_2 : ∀ {R : Type u_1} [inst : One R] [inst_1 : Zero R] [inst_2 : Add R] (n : ℕ), n.succ.unaryCast = n.unaryCast + 1
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.go₁_zero_utf8Len : ∀ (s : List Char), String.Pos.Raw.extract.go₁ s 0 0 { byteIdx := String.utf8Len s } = s
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.pp.analyze.omitMax : Lean.Option Bool
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.forIn_filterWithPostcondition : ∀ {α β γ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [inst_4 : Std.Internal.Do.Assertion Pred]
  [inst_5 : Std.Internal.Do.Assertion EPred] [inst_6 : Std.Internal.Do.WPMonad o Pred EPred] [inst_7 : MonadLiftT n o]
  [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id] [inst_10 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o]
  {it : Std.Iter β} {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} {init : γ}
  {g : β → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        if __do_lift.down = true then g out acc else pure (ForInStep.yield acc) ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.Iter.filterWithPostcondition f it) init g ⦃ Q; eQ ⦄
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.fieldEquivOfAlgEquiv.congr_simp : ∀ {A : Type u_8} {B : Type u_9} {C : Type u_10} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] (FA : Type u_12) (FB : Type u_13) (FC : Type u_14) [inst_5 : Field FA]
  [inst_6 : Field FB] [inst_7 : Field FC] [inst_8 : Algebra A FA] [inst_9 : Algebra B FB] [inst_10 : Algebra C FC]
  [inst_11 : IsFractionRing A FA] [inst_12 : IsFractionRing B FB] [inst_13 : IsFractionRing C FC]
  [inst_14 : Algebra A FB] [inst_15 : IsScalarTower A B FB] [inst_16 : Algebra A FC] [inst_17 : IsScalarTower A C FC]
  [inst_18 : Algebra FA FB] [inst_19 : IsScalarTower A FA FB] [inst_20 : Algebra FA FC]
  [inst_21 : IsScalarTower A FA FC] (f f_1 : B ≃ₐ[A] C),
  f = f_1 → IsFractionRing.fieldEquivOfAlgEquiv FA FB FC f = IsFractionRing.fieldEquivOfAlgEquiv FA FB FC f_1
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
/-- The functor `GrpCat ⥤ AddGrpCat` by sending `X ↦ Additive X` and `f ↦ f`.
 -/
GrpCat.toAddGrp : CategoryTheory.Functor GrpCat AddGrpCat
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.isOpen_eball`. -/
EMetric.isOpen_ball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, IsOpen (Metric.eball x ε)
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsDedekindDomain.primesOverEquivPrimesOver_ramificationIdx_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Rₚ : Type u_3) [inst_4 : CommRing Rₚ] [inst_5 : Algebra R Rₚ]
  [inst_6 : IsLocalization.AtPrime Rₚ p] [inst_7 : IsLocalRing Rₚ] (Sₚ : Type u_4) [inst_8 : CommRing Sₚ]
  [inst_9 : Algebra S Sₚ] [inst_10 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
  [inst_11 : Algebra Rₚ Sₚ] [inst_12 : IsDomain R] [inst_13 : IsDedekindDomain S] [inst_14 : Module.IsTorsionFree R S]
  [inst_15 : Algebra R Sₚ] [inst_16 : IsScalarTower R S Sₚ] [inst_17 : IsScalarTower R Rₚ Sₚ] (hp : p ≠ ⊥)
  (P : ↑(p.primesOver S)),
  (↑((IsDedekindDomain.primesOverEquivPrimesOver p Rₚ Sₚ hp) P)).ramificationIdx Rₚ = (↑P).ramificationIdx R
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabOfScientific : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Countable
CategoryTheory.CountableCategory.instHomAsType : ∀ (α : Type u) [inst : CategoryTheory.Category.{v, u} α] [inst_1 : CategoryTheory.CountableCategory α],
  CategoryTheory.CountableCategory (CategoryTheory.CountableCategory.HomAsType α)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RooSlice : (α : Type u_1) → [Ord α] → Type u_1
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
MeasureTheory.condExp_stronglyMeasurable_mul_of_bound : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  m ≤ mΩ →
    ∀ [MeasureTheory.IsFiniteMeasure μ] {f g : Ω → ℝ},
      MeasureTheory.StronglyMeasurable f →
        MeasureTheory.Integrable g μ → ∀ (c : ℝ), (∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c) → μ[f * g | m] =ᵐ[μ] f * μ[g | m]
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ball_subset_of_comp_subset : ∀ {β : Type ub} {V W : Set (β × β)} {x y : β},
  x ∈ UniformSpace.ball y W → SetRel.comp W W ⊆ V → UniformSpace.ball x W ⊆ UniformSpace.ball y V
-- Mathlib.Order.Filter.AtTopBot.Field
/-- The function `fun x ↦ r * f x` tends to negative infinity along a nontrivial filter
if and only if `r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity.  -/
Filter.tendsto_const_mul_atBot_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔
    0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.atTop
-- Init.Data.Option.Array
Option.toArray_map : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → β}, (Option.map f o).toArray = Array.map f o.toArray
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_36 : HAdd Std.Time.Week.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.comap_top : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S),
  NonUnitalSubring.comap f ⊤ = ⊤
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δ_map : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {ι' : Type w₃} {σ : Type w₂} {σ' : Type w₄} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ)
  (Q' : Algebra.Generators S T ι') (P' : Algebra.Generators R S σ') (f : Q'.Hom Q) (x : Q'.toExtension.H1Cotangent),
  (Algebra.Generators.H1Cotangent.δ Q P) ((Algebra.Extension.H1Cotangent.map f.toExtensionHom) x) =
    (Algebra.Generators.H1Cotangent.δ Q' P') x
-- Mathlib.Analysis.SpecialFunctions.Exp
Complex.comap_exp_nhdsNE : Filter.comap Complex.exp (nhdsWithin 0 {0}ᶜ) = Filter.comap Complex.re Filter.atBot
-- Init.Prelude
/-- Create syntax node with 4 children  -/
Lean.Syntax.node4 : Lean.SourceInfo → Lean.SyntaxNodeKind → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax
-- Mathlib.Algebra.FreeMonoid.Symbols
FreeAddMonoid.mem_symbols : ∀ {α : Type u_1} [inst : DecidableEq α] {m : α} {a : FreeAddMonoid α}, m ∈ a.symbols ↔ m ∈ a
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.inftyValuation`. -/
FunctionField.inftyValuation : (F : Type u_1) → [inst : Field F] → [DecidableEq (RatFunc F)] → Valuation (RatFunc F) (WithZero (Multiplicative ℤ))
-- Mathlib.LinearAlgebra.FreeModule.PID
Module.Basis.SmithNormalForm.mk.injEq : ∀ {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M}
  {ι : Type u_4} {n : ℕ} (bM : Module.Basis ι R M) (bN : Module.Basis (Fin n) R ↥N) (f : Fin n ↪ ι) (a : Fin n → R)
  (snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)) (bM_1 : Module.Basis ι R M) (bN_1 : Module.Basis (Fin n) R ↥N)
  (f_1 : Fin n ↪ ι) (a_1 : Fin n → R) (snf_1 : ∀ (i : Fin n), ↑(bN_1 i) = a_1 i • bM_1 (f_1 i)),
  ({ bM := bM, bN := bN, f := f, a := a, snf := snf } = { bM := bM_1, bN := bN_1, f := f_1, a := a_1, snf := snf_1 }) =
    (bM = bM_1 ∧ bN = bN_1 ∧ f = f_1 ∧ a = a_1)
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the reverse direction of `Order.succ_le_iff_isMax`. -/
IsMax.succ_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α}, IsMax a → Order.succ a ≤ a
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.truncLEIsoTruncLT a b h).hom.app X) ((t.truncLTι b).app X) =
    (t.truncLEι a).app X
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- This is another version of `lipschitzGroup.conjAct_smul_ι_mem_range_ι` which uses `involute`.  -/
lipschitzGroup.involute_act_ι_mem_range_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} [Invertible 2] {x : (CliffordAlgebra Q)ˣ},
  x ∈ lipschitzGroup Q →
    ∀ (b : M), CliffordAlgebra.involute ↑x * (CliffordAlgebra.ι Q) b * ↑x⁻¹ ∈ (CliffordAlgebra.ι Q).range
-- Mathlib.LinearAlgebra.Dimension.Free
Module.Free.exists_linearMap_injective_of_linearIndependent_of_lift_rank_le : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  {N' : Type v'} [inst_4 : AddCommMonoid N'] [inst_5 : Module R N'] {ι : Type w} {v : ι → N'},
  LinearIndependent R v →
    Cardinal.lift.{w, v} (Module.rank R M) ≤ Cardinal.lift.{v, w} (Cardinal.mk ι) → ∃ f, Function.Injective ⇑f
-- Lean.LocalContext
Lean.LocalContext.getFVarIds : Lean.LocalContext → Array Lean.FVarId
-- Mathlib.FieldTheory.Relrank
IntermediateField.rank_bot_mul_relrank : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A ≤ B → Module.rank F ↥A * A.relrank B = Module.rank F ↥B
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_mul_cancel_right₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {b : G₀}, b ≠ 0 → ∀ (a : G₀), b / (a * b) = a⁻¹
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable and `K / E`
is separable, then the separable degree of `K / F` is equal to the degree of `K / E`.
It is a special case of `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`, and is an
intermediate result used to prove it.  -/
Field.sepDegree_eq_of_isPurelyInseparable_of_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F E]
  [Algebra.IsSeparable E K], Field.sepDegree F K = Module.rank E K
-- Init.Data.BitVec.Lemmas
/-- When the `(i+1)`th bit of `x` is true,
keeping the lower `(i + 1)` bits of `x` equals keeping the lower `i` bits
and then performing bitwise-or with `twoPow i = (1 << i)`,
 -/
BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true : ∀ {w : ℕ} {x : BitVec w} {i : ℕ},
  x.getLsbD i = true →
    BitVec.setWidth w (BitVec.setWidth (i + 1) x) = BitVec.setWidth w (BitVec.setWidth i x) ||| BitVec.twoPow w i
-- Mathlib.Data.TypeVec
TypeVec.last.inhabited : {n : ℕ} → (α : TypeVec.{u_1} (n + 1)) → [Inhabited (α Fin2.fz)] → Inhabited α.last
-- Mathlib.Logic.Basic
/-- In most of mathlib, we use the law of excluded middle (LEM) and the axiom of choice (AC) freely.
The `Decidable` namespace contains versions of lemmas from the root namespace that explicitly
attempt to avoid the axiom of choice, usually by adding decidability assumptions on the inputs.

You can check if a lemma uses the axiom of choice by using `#print axioms foo` and seeing if
`Classical.choice` appears in the list.
 -/
LibraryNote.decidable_namespace : Batteries.Util.LibraryNote
-- Mathlib.RingTheory.Coalgebra.Basic
CommSemiring.instIsCocomm : ∀ (R : Type u) [inst : CommSemiring R], Coalgebra.IsCocomm R R
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.cofanMapObjComp.eq_1 : ∀ {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) (q : J → K) (r : I → K) (hpqr : ∀ (i : I), q (p i) = r i) (k : K)
  (c : (j : J) → q j = k → X.CofanMapObjFun p j) (c' : CategoryTheory.Limits.Cofan fun j => (c ↑j ⋯).pt),
  X.cofanMapObjComp p q r hpqr k c c' =
    CategoryTheory.GradedObject.CofanMapObjFun.mk X r k c'.pt fun i hi =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩) (c'.inj ⟨p i, ⋯⟩)
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.symm_bijective : ∀ {X : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X], Function.Bijective Equidecomp.symm
-- Std.Async.UDP
/-- Represents a UDP socket.
 -/
Std.Async.UDP.Socket : Type
-- Batteries.Data.String.Matcher
/-- Returns all the substrings of `s` that match `pattern`.
 -/
Substring.findAllSubstr : Substring.Raw → Substring.Raw → Array Substring.Raw
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.toZeroLEOneClass : ∀ {α : Type u_5} (self : ConditionallyCompleteLinearOrderedField α), ZeroLEOneClass α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.toClass_some : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x y : F}
  (h : W.Nonsingular x y),
  WeierstrassCurve.Affine.Point.toClass (WeierstrassCurve.Affine.Point.some x y h) =
    (ClassGroup.mk W.FunctionField) (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h)
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.eq_and_eq_or_eq_and_eq : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {x' y' : α},
  G.IsLink e x y → G.IsLink e x' y' → x = x' ∧ y = y' ∨ x = y' ∧ y = x'
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_two : ∀ {R : Type u_1} [inst : CommRing R] (k : ℕ) (a : R),
  Polynomial.dickson k a 2 = Polynomial.X ^ 2 - Polynomial.C a * (3 - ↑k)
-- Mathlib.Algebra.Group.Defs
/-- An `AddLeftCancelSemigroup` is an additive semigroup such that
`a + b = a + c` implies `b = c`.  -/
AddLeftCancelSemigroup : Type u → Type u
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_add_right_eq_map : ∀ {m n : ℕ}, (m<...=m + n).toList = List.map (fun x => x + m + 1) (0...n).toList
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.mem_ae_iff_prob_eq_one : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasurableSet s → (s ∈ MeasureTheory.ae μ ↔ μ s = 1)
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.funMap_equiv_unify : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] (G : ι → Type w) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] {n : ℕ} (F : L.Functions n)
  (x : Fin n → FirstOrder.Language.Structure.Sigma f) (i : ι) (hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))),
  FirstOrder.Language.Structure.funMap F x ≈
    FirstOrder.Language.Structure.Sigma.mk f i
      (FirstOrder.Language.Structure.funMap F (FirstOrder.Language.DirectLimit.unify f x i hi))
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.eval_one_cyclotomic_not_prime_pow : ∀ {R : Type u_1} [inst : Ring R] {n : ℕ},
  (∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n) → Polynomial.eval 1 (Polynomial.cyclotomic n R) = 1
-- Init.Data.Dyadic.Basic
Dyadic.ofInt.eq_1 : ∀ (i : ℤ), Dyadic.ofInt i = Dyadic.ofIntWithPrec i 0
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_mul_self : ∀ {G : Type u_1} [inst : Group G] (s : Set G), ↑(MulAction.stabilizer G s) * s = s
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D)
  [inst_7 : ∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (X : CategoryTheory.Functor D E), (J.plusFunctorWhiskerLeftIso P).hom.app X = (J.plusCompIso X P).hom
-- Init.System.Platform
/-- Is the current platform Windows?
 -/
System.Platform.isWindows : Bool
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.rootSet_X_pow : ∀ {R : Type u} {S : Type v} [inst : Field R] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra R S] {n : ℕ},
  n ≠ 0 → (Polynomial.X ^ n).rootSet S = {0}
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.IsDiscrete.mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R], (∃ γ < 1, ∀ δ < 1, δ ≤ γ) → ValuativeRel.IsDiscrete R
-- Mathlib.Algebra.GroupWithZero.Invertible
invOf_eq_inv : ∀ {α : Type u} [inst : GroupWithZero α] (a : α) [inst_1 : Invertible a], ⅟a = a⁻¹
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ArbitraryShiftTarget.distance : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {m : ℕ} → (self : aig.ArbitraryShiftTarget m) → aig.RefVec self.n
-- Mathlib.Algebra.Group.Invertible.Basic
/-- Convert `IsUnit` to `Invertible` using `Classical.choice`.

Prefer `casesI h.nonempty_invertible` over `letI := h.invertible` if you want to avoid choice.  -/
IsUnit.invertible : {α : Type u} → [inst : Monoid α] → {a : α} → IsUnit a → Invertible a
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommGrp C} (f g : A ⟶ B),
  f.hom.hom.hom = g.hom.hom.hom → f = g
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabNoImplicitLambda : Lean.Elab.Term.TermElab
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- Given a charted space without topology, endow it with a genuine charted space structure with
respect to the topology constructed from the atlas.  -/
ChartedSpaceCore.toChartedSpace : {H : Type u} → {M : Type u_2} → [inst : TopologicalSpace H] → (c : ChartedSpaceCore H M) → ChartedSpace H M
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- The trivial model with corners has no boundary  -/
modelWithCornersSelf_boundaryless : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type u_2) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E], (modelWithCornersSelf 𝕜 E).Boundaryless
-- Mathlib.RingTheory.Polynomial.Radical
degree_radical_le : ∀ {k : Type u_1} [inst : Field k] [inst_1 : DecidableEq k] {a : Polynomial k},
  a ≠ 0 → (UniqueFactorizationMonoid.radical a).degree ≤ a.degree
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instToStringCodeLiveness : ToString Lean.Elab.Do.CodeLiveness
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- Coercion from `MeasureTheory.ProbabilityMeasure Ω` to `MeasureTheory.Measure Ω`.  -/
MeasureTheory.ProbabilityMeasure.toMeasure : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → MeasureTheory.ProbabilityMeasure Ω → MeasureTheory.Measure Ω
-- Init.Data.List.Lemmas
List.foldrM.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {s : Type u} {α : Type w} (f : α → s → m s) (init : s) (l : List α),
  List.foldrM f init l = List.foldlM (fun s a => f a s) init l.reverse
-- Init.Data.SInt.Lemmas
Int8.toBitVec_mod : ∀ {a b : Int8}, (a % b).toBitVec = a.toBitVec.srem b.toBitVec
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.length_iter : ∀ {β : Type w} {array : Array β}, array.iter.length = array.size
-- Mathlib.Topology.Inseparable
Specializes.antisymm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y → y ⤳ x → Inseparable x y
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} →
          (cocomplex : CochainComplex C ℕ) →
            autoParam (∀ (n : ℕ), CategoryTheory.Injective (cocomplex.X n))
                CategoryTheory.InjectiveResolution.injective._autoParam →
              [hasHomology : ∀ (i : ℕ), HomologicalComplex.HasHomology cocomplex i] →
                (ι : (CochainComplex.single₀ C).obj Z ⟶ cocomplex) →
                  autoParam (QuasiIso ι) CategoryTheory.InjectiveResolution.quasiIso._autoParam →
                    CategoryTheory.InjectiveResolution Z