mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Constructions
Units.continuous_val : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M], Continuous Units.val
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.iUnion_disjUnion : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion),
  (π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_eq_toList_rcc : ∀ {n : ℕ}, (*...=n).toList = (0...=n).toList
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tensorAssoc_symm_apply : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] [inst_7 : Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂)
  (Q₃ : QuadraticForm R M₃) (x : TensorProduct R M₁ (TensorProduct R M₂ M₃)),
  (Q₁.tensorAssoc Q₂ Q₃).symm x = (TensorProduct.assoc R M₁ M₂ M₃).symm x
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.instLocallySmall : ∀ {J : CategoryTheory.Limits.MultispanShape},
  CategoryTheory.LocallySmall.{t, max w w', max w' w} (CategoryTheory.Limits.WalkingMultispan J)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inv_hom_h₀_comp_f_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : E.I₀) {Z : C} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (e.hom.h₀ i)) (CategoryTheory.CategoryStruct.comp (E.f i) h) =
    CategoryTheory.CategoryStruct.comp (F.f (e.hom.s₀ i)) h
-- Lean.Parser.Term
Lean.Parser.Term.motive : Lean.Parser.Parser
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.collectStructFields : Lean.Name →
  List Lean.Level →
    Array Lean.Expr →
      Array (Lean.TSyntax `Lean.Parser.Term.structInstField) →
        Lean.NameMap Lean.Expr →
          Lean.ConstructorVal →
            Lean.PrettyPrinter.Delaborator.DelabM
              (Lean.NameMap Lean.Expr × Array (Lean.TSyntax `Lean.Parser.Term.structInstField))
-- Mathlib.Algebra.Ring.Commute
Commute.sq_eq_sq_iff_eq_or_eq_neg : ∀ {R : Type u} [inst : Ring R] {a b : R} [NoZeroDivisors R], Commute a b → (a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b)
-- Init.Meta
Lean.Parser.Tactic.dsimpKind : Lean.ParserDescr
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestMatchAt_iff : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt c pos pos' ↔ ∃ (h : pos ≠ s.endPos), pos' = pos.next h ∧ pos.get h = c
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
/-- When `α` has at least 5 elements, then `alternatingGroup α` is a simple group.  -/
alternatingGroup.isSimpleGroup : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], 5 ≤ Nat.card α → IsSimpleGroup ↥(alternatingGroup α)
-- Init.Data.Int.Gcd
Int.coe_lcm_dvd_iff : ∀ {a b c : ℤ}, ↑(a.lcm b) ∣ c ↔ a ∣ c ∧ b ∣ c
-- Mathlib.Probability.Kernel.Composition.CompProd
/-- Lebesgue integral against the composition-product of two kernels.  -/
ProbabilityTheory.Kernel.lintegral_compProd₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γ → ENNReal},
  AEMeasurable f ((κ.compProd η) a) →
    ∫⁻ (z : β × γ), f z ∂(κ.compProd η) a = ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.hasColimits_commRingCat : CategoryTheory.Limits.HasColimits CommRingCat
-- Init.Data.Format.Basic
/-- Concatenates a list of `Format`s with `++`.
 -/
Std.Format.join : List Std.Format → Std.Format
-- Lean.Elab.PreDefinition.FixedParams
/-- For each function in the clique, a mapping from its parameters to the fixed parameters.
For the first function, they appear in order; for other functions they may be reordered.
  -/
Lean.Elab.FixedParamPerms.perms : Lean.Elab.FixedParamPerms → Array Lean.Elab.FixedParamPerm
-- Mathlib.Algebra.Ring.Pi
Pi.nonUnitalSemiring : {I : Type u} → {f : I → Type v} → [(i : I) → NonUnitalSemiring (f i)] → NonUnitalSemiring ((i : I) → f i)
-- Init.Data.String.Basic
String.decodeChar.congr_simp : ∀ (s s_1 : String) (e_s : s = s_1) (byteIdx byteIdx_1 : ℕ) (e_byteIdx : byteIdx = byteIdx_1)
  (h : (s.toByteArray.utf8DecodeChar? byteIdx).isSome = true), s.decodeChar byteIdx h = s_1.decodeChar byteIdx_1 ⋯
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → t.get? k = some k
-- Mathlib.Data.List.Sigma
List.perm_lookupAll : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) {l₁ l₂ : List (Sigma β)},
  l₁.NodupKeys → l₁.Perm l₂ → List.lookupAll a l₁ = List.lookupAll a l₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF),
  t.isEmpty = false →
    ∀ {k : α} {v : β k}, (compare t.maxKey! (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKey!).isLE = true
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.instIsSplitEpiF : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁ ⟶ C₂) [CategoryTheory.IsSplitEpi f] (j : ι), CategoryTheory.IsSplitEpi (f.f j)
-- Init.Data.Nat.ToString
Nat.toString_eq_repr : ∀ {n : ℕ}, toString n = n.repr
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_eq_zero_iff : ∀ {R : Type u_1} [inst : Semiring R] {N : ℕ} {f : Polynomial R}, Polynomial.reflect N f = 0 ↔ f = 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_neg : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (x : M →₀ R), MonoidAlgebra.ofCoeff (-x) = -MonoidAlgebra.ofCoeff x
-- Mathlib.Topology.Algebra.GroupCompletion
/-- Completion of a continuous group hom, as a group hom.  -/
AddMonoidHom.completion : {α : Type u_3} →
  {β : Type u_4} →
    [inst : UniformSpace α] →
      [inst_1 : AddGroup α] →
        [inst_2 : IsUniformAddGroup α] →
          [inst_3 : UniformSpace β] →
            [inst_4 : AddGroup β] →
              [inst_5 : IsUniformAddGroup β] →
                (f : α →+ β) → Continuous ⇑f → UniformSpace.Completion α →+ UniformSpace.Completion β
-- Std.Data.HashSet.Lemmas
Std.HashSet.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∉ m₁ → k ∉ m₁ ∩ m₂
-- Mathlib.Order.RelIso.Basic
RelHom.comp_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  {u : δ → δ → Prop} (h : r →r s) (g : s →r t) (f : t →r u), (f.comp g).comp h = f.comp (g.comp h)
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.dischargeDefault? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)
-- Mathlib.Data.List.Chain
List.IsChain.iff_mem : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.IsChain R l ↔ List.IsChain (fun x y => x ∈ l ∧ y ∈ l ∧ R x y) l
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The functor that takes a simplicial set to its homotopy category by passing through the
2-truncation.  -/
SSet.hoFunctor : CategoryTheory.Functor SSet CategoryTheory.Cat
-- Mathlib.Order.Bounds.Basic
mem_upperBounds : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, a ∈ upperBounds s ↔ ∀ x ∈ s, x ≤ a
-- Mathlib.Order.WellFounded
StrictMono.range_inj : ∀ {β : Type u_2} {γ : Type u_3} [inst : LinearOrder β] [inst_1 : Preorder γ] [WellFoundedLT β] {f g : β → γ},
  StrictMono f → StrictMono g → (Set.range f = Set.range g ↔ f = g)
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULift.downFunctor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : ULift.{u₂, u₁} C),
  CategoryTheory.ULift.downFunctor.obj self = self.down
-- Init.Grind.ToInt
Lean.Grind.IntInterval.nonEmpty : Lean.Grind.IntInterval → Bool
-- Init.Data.Array.Lemmas
Array.getElem_swap' : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} {hi : i < xs.size} {hj : j < xs.size} {k : ℕ} (hk : k < xs.size),
  (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]
-- Mathlib.Order.SuccPred.Basic
WithTop.instPredOrder.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α],
  WithTop.instPredOrder =
    {
      pred := fun x =>
        match x with
        | none => ↑⊤
        | some a => ↑(Order.pred a),
      pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
-- Mathlib.Data.Set.Lattice
/-- A specialization of `subset_iUnion₂`.  -/
Set.subset_biUnion_of_mem : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {u : α → Set β} {x : α}, x ∈ s → u x ⊆ ⋃ x ∈ s, u x
-- Mathlib.Topology.Order.IntermediateValue
/-- Suppose `α` is equipped with a conditionally complete linear dense order and `f : α → δ` is
continuous and injective. Then `f` is strictly monotone (increasing) if
it is strictly monotone (increasing) on some closed interval `[a, b]`.  -/
Continuous.strictMonoOn_of_inj_rigidity : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {f : α → δ}, Continuous f → Function.Injective f → ∀ {a b : α}, a < b → StrictMonoOn f (Set.Icc a b) → StrictMono f
-- Mathlib.Order.Category.PartOrd
_private.Mathlib.Order.Category.PartOrd.0.PartOrd.Hom.mk.sizeOf_spec : ∀ {X Y : PartOrd} (hom' : ↑X →o ↑Y), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft.eq_2 : ∀ (x n : ℕ), (Int.negSucc n).shiftLeft x = Int.negSucc ((n + 1) <<< x - 1)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_add`. -/
CuspForm.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instDivisionAddCommMonoidOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : SubtractionCommMonoid Mᵃᵒᵖ], DomAddAct.instDivisionAddCommMonoidOfAddOpposite = inst
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.subset_vonNeumann : ∀ {o : Ordinal.{u_1}} {x : ZFSet.{u_1}}, x ⊆ ZFSet.vonNeumann o ↔ x.rank ≤ o
-- Init.Data.UInt.Lemmas
USize.ofBitVec_toBitVec : ∀ (a : USize), { toBitVec := a.toBitVec } = a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ \ t₂).get? k = t₁.get? k
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instOne.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : One Y],
  LocallyConstant.instOne = { one := LocallyConstant.const X 1 }
-- Mathlib.Combinatorics.Enumerative.Composition
_private.Mathlib.Combinatorics.Enumerative.Composition.0.List.splitWrtCompositionAux.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α × List α → Sort u_2) (l₁ l₂ : List α) (h_1 : (l₁ l₂ : List α) → motive (l₁, l₂)),
  (match (l₁, l₂) with
    | (l₁, l₂) => h_1 l₁ l₂) =
    h_1 l₁ l₂
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_spec : ∀ {α : Type u_1} (s : Finset α) (f : α → ℕ), (∏ i ∈ s, (f i).factorial) * Nat.multinomial s f = (∑ i ∈ s, f i).factorial
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.State.mk.injEq : ∀ (pendingProducer : Option Std.Http.Body.Channel.Producer✝) (pendingConsumer : Option Std.Http.Body.Channel.Consumer✝)
  (interestWaiter : Option (Std.Async.Waiter Bool)) (closed : Bool) (knownSize : Option Std.Http.Body.Length)
  (pendingIncompleteChunk : Option Std.Http.Chunk) (pendingProducer_1 : Option Std.Http.Body.Channel.Producer✝)
  (pendingConsumer_1 : Option Std.Http.Body.Channel.Consumer✝) (interestWaiter_1 : Option (Std.Async.Waiter Bool))
  (closed_1 : Bool) (knownSize_1 : Option Std.Http.Body.Length) (pendingIncompleteChunk_1 : Option Std.Http.Chunk),
  ({ pendingProducer := pendingProducer, pendingConsumer := pendingConsumer, interestWaiter := interestWaiter,
        closed := closed, knownSize := knownSize, pendingIncompleteChunk := pendingIncompleteChunk } =
      { pendingProducer := pendingProducer_1, pendingConsumer := pendingConsumer_1, interestWaiter := interestWaiter_1,
        closed := closed_1, knownSize := knownSize_1, pendingIncompleteChunk := pendingIncompleteChunk_1 }) =
    (pendingProducer = pendingProducer_1 ∧
      pendingConsumer = pendingConsumer_1 ∧
        interestWaiter = interestWaiter_1 ∧
          closed = closed_1 ∧ knownSize = knownSize_1 ∧ pendingIncompleteChunk = pendingIncompleteChunk_1)
-- Mathlib.RingTheory.SimpleRing.Principal
IsDomain.of_isSimpleRing : ∀ {R : Type u_1} [inst : CommRing R] [IsSimpleRing R], IsDomain R
-- Init.Data.String.Basic
String.Pos.cast_eq_startPos : ∀ {s t : String} {hst : s = t} {p : s.Pos}, p.cast hst = t.startPos ↔ p = s.startPos
-- Mathlib.RingTheory.AdicCompletion.Noetherian
IsHausdorff.of_le_jacobson : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsNoetherianRing R] [Module.Finite R M], I ≤ ⊥.jacobson → IsHausdorff I M
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- the second projection  -/
CategoryTheory.Functor.PullbackObjObj.snd : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
              {X₁ Y₁ : C₁} →
                {f₁ : X₁ ⟶ Y₁} →
                  {X₃ Y₃ : C₃} →
                    {f₃ : X₃ ⟶ Y₃} → (self : G.PullbackObjObj f₁ f₃) → self.pt ⟶ (G.obj (Opposite.op Y₁)).obj Y₃
-- Mathlib.Topology.Neighborhoods
tendsto_const_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {f : Filter α},
  Filter.Tendsto (fun x_1 => x) f (nhds x)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.CompatibleSMul.intModule : ∀ {M : Type u_8} {M₂ : Type u_10} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] {S : Type u_14}
  [inst_2 : Semiring S] [inst_3 : Module S M] [inst_4 : Module S M₂], LinearMap.CompatibleSMul M M₂ ℤ S
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.get!_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Inhabited β] {l : Std.DHashMap.Internal.AssocList α fun x => β}
  {a : α}, Std.DHashMap.Internal.AssocList.get! a l = Std.Internal.List.getValue! a l.toList
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instNatCast : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → NatCast (WithVal v)
-- Init.Data.Nat.Basic
Nat.lt_pred_iff : ∀ {n : ℕ} {m : ℕ}, n < m.pred ↔ n.succ < m
-- Mathlib.Data.ZMod.Basic
ZMod.val_cast_of_lt : ∀ {n a : ℕ}, a < n → (↑a).val = a
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.condKernelUnitBorel.congr_simp : ∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (κ κ_1 : ProbabilityTheory.Kernel Unit (α × Ω)) (e_κ : κ = κ_1)
  [inst_2 : ProbabilityTheory.IsFiniteKernel κ], κ.condKernelUnitBorel = κ_1.condKernelUnitBorel
-- Mathlib.NumberTheory.EulerProduct.Basic
tprod_primes_pow_eq : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T0Space α]
  {f : ℕ → α},
  (Multipliable fun n => f ↑n) → ∏' (p : Nat.Primes) (n : ℕ), f (↑p ^ (n + 1)) = ∏' (n : { n // IsPrimePow n }), f ↑n
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.Scheme.instIsClosedImmersionιOfIsSeparated : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X ⟶ Y) [Y.IsSeparated],
  AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.equalizer.ι f g)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.comap_equiv_eq_map_symm : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] (f : R ≃+* S)
  (K : NonUnitalSubsemiring S), NonUnitalSubsemiring.comap (↑f) K = NonUnitalSubsemiring.map f.symm K
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `getEntry!` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.getEntry!ₘ : {α : Type u} →
  {β : α → Type v} → [Ord α] → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Internal.Impl α β → α → (a : α) × β a
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊤` to the domain and codomain of a `LatticeHom`.  -/
LatticeHom.withTop : {α : Type u_1} →
  {β : Type u_2} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom α β → LatticeHom (WithTop α) (WithTop β)
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.uniqueGalX : {F : Type u_1} → [inst : Field F] → Unique Polynomial.X.Gal
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.hilbertPoly_smul : ∀ {F : Type u_1} [inst : Field F] (a : F) (p : Polynomial F) (d : ℕ), (a • p).hilbertPoly d = a • p.hilbertPoly d
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- The resultant of two polynomials `f` and `g` is the determinant of the Sylvester matrix of `f`
and `g`. The size arguments `m` and `n` are implemented as `optParam`, meaning that the default
values are `f.natDegree` and `g.natDegree` respectively, but they can also be specified to be
other values.  -/
Polynomial.resultant : {R : Type u_1} → [inst : CommRing R] → (f g : Polynomial R) → optParam ℕ f.natDegree → optParam ℕ g.natDegree → R
-- ProofWidgets.Component.Basic
ProofWidgets.ppExprTagged : ProofWidgets.InteractiveExprProps → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Widget.CodeWithInfos)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- For a reduced, crystallographic, irreducible root pairing other than `𝔤₂`, if the sum of two
roots is a root, they cannot make an acute angle.

To see that this lemma fails for `𝔤₂`, let `α` (short) and `β` (long) be a base. Then the roots
`α + β` and `2α + β` make an angle `π / 3` even though `3α + 2β` is a root. We can even witness as:
```lean
example (P : RootPairing ι R M N) [P.EmbeddedG2] :
    P.pairingIn ℤ (EmbeddedG2.shortAddLong P) (EmbeddedG2.twoShortAddLong P) = 1 := by
  simp
```
 -/
RootPairing.pairingIn_le_zero_of_root_add_mem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} [Finite ι]
  [CharZero R] [IsDomain R] {i j : ι} [inst_8 : P.IsNotG2],
  P.root i + P.root j ∈ Set.range ⇑P.root → P.pairingIn ℤ i j ≤ 0
-- Lean.Elab.Command
Lean.Elab.Command.CommandElab : Type
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- The oplax functor associated with a pseudofunctor.  -/
CategoryTheory.Pseudofunctor.toOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.Pseudofunctor B C → CategoryTheory.OplaxFunctor B C
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.toList_ric : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.toList_ric._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap.Raw α β cmp},
  t.WF →
    ∀ {bound : α},
      Std.Slice.toList (Std.Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun e => (cmp e.1 bound).isLE) t.toList
-- Mathlib.Order.Category.BddOrd
BddOrd.coe_of : ∀ (X : Type u) [inst : PartialOrder X] [inst_1 : BoundedOrder X], ↑(BddOrd.of X).toPartOrd = X
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.instMax : {E : Type u_3} → [inst : Group E] → Max (GroupNorm E)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.top_lowerCentralSeries_pi_le : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → AddGroup (Gs i)] (n : ℕ),
  ⊤.lowerCentralSeries n ≤ AddSubgroup.pi Set.univ fun i => ⊤.lowerCentralSeries n
-- Mathlib.Algebra.GroupWithZero.Basic
right_eq_mul₀ : ∀ {M₀ : Type u_1} {a b : M₀} [inst : MulZeroOneClass M₀] [IsRightCancelMulZero M₀], b ≠ 0 → (b = a * b ↔ a = 1)
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Scheme.Hom.denseRange : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsDominant f], DenseRange ⇑f
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranObjObjIsoLimit.eq_1 : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (F : CategoryTheory.Functor C H)
  [inst_4 : L.HasPointwiseRightKanExtension F] (X : D),
  L.ranObjObjIsoLimit F X = (L.isPointwiseRightKanExtensionRanCounit F X).isoLimit
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- The indexing category.  -/
CategoryTheory.IndParallelPairPresentation.I : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} → CategoryTheory.IndParallelPairPresentation f g → Type v₁
-- Lean.Meta.Tactic.Induction
Lean.Meta.instInhabitedInductionSubgoal.default : Lean.Meta.InductionSubgoal
-- Mathlib.GroupTheory.Descent
/-- If `M` is a monoid and `n : ℕ`, `h : M → ℝ` satisfy
* for all `M : G`, `h (x ^ n) ≥ b * h x - c₀`,
* for all `B : ℝ`, there are only finitely many `x : M` such that `h x ≤ B`,

where `1 < b` and `c₀` are real numbers, then the set of elements of finite order in `M` is finite.
 -/
Monoid.finite_set_isOfFiniteOrder_of_descent : ∀ {M : Type u_1} [inst : Monoid M] {n : ℕ} {h : M → ℝ} {b c₀ : ℝ},
  1 < b → (∀ (x : M), b * h x - c₀ ≤ h (x ^ n)) → ∀ [Northcott h], Finite ↑{x | IsOfFinOrder x}
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mapAlgEquiv_symm : ∀ {R : Type u} (σ : Type u_1) [inst : CommSemiring R] {A₁ : Type u_2} {A₂ : Type u_3} [inst_1 : CommSemiring A₁]
  [inst_2 : CommSemiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂),
  (MvPolynomial.mapAlgEquiv σ e).symm = MvPolynomial.mapAlgEquiv σ e.symm
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.productEquiv_inverse_obj_as : ∀ {J : Type u_1} {K : Type u_2} (x : CategoryTheory.Discrete J × CategoryTheory.Discrete K),
  (CategoryTheory.Discrete.productEquiv.inverse.obj x).as = (x.1.as, x.2.as)
-- Mathlib.Algebra.Order.Group.Synonym
toLex_vadd' : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α), toLex b +ᵥ a = b +ᵥ a
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.pellZd_succ_succ : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.pellZd a1 (n + 2) + Pell.pellZd a1 n = ↑(2 * a) * Pell.pellZd a1 (n + 1)
-- Mathlib.Data.ENNReal.Inv
ENNReal.one_sub_inv_two : 1 - 2⁻¹ = 2⁻¹
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.equivLike_inv_eq_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N), EquivLike.inv f = ⇑f.symm
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If a point lies in the affine span of two points, those three points are collinear.  -/
collinear_insert_of_mem_affineSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P}, p₁ ∈ line[k, p₂, p₃] → Collinear k {p₁, p₂, p₃}