mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- In a 2-truncated quasicategory, the right and left homotopy relations coincide.
 -/
SSet.Truncated.homotopicL_iff_homotopicR : ∀ {X : SSet.Truncated 2} [X.Quasicategory₂]
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f g : SSet.Truncated.Edge x y}, SSet.Truncated.HomotopicL f g ↔ SSet.Truncated.HomotopicR f g
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.whiskerLeft_id : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  (X Y : CategoryTheory.FreeMonoidalCategory C), CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Lean.Elab.Match
/-- Elaborate discriminants inferring the match-type  -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchTypeAndDiscrs.elabDiscrs : Array Lean.Syntax →
  Array Lean.Elab.Term.TermMatchAltView →
    Lean.Expr → ℕ → Array Lean.Elab.Term.Discr → Lean.Elab.TermElabM Lean.Elab.Term.ElabMatchTypeAndDiscrsResult
-- Init.ShareCommon
ShareCommon.StateFactory.mk : ShareCommon.StateFactoryBuilder → ShareCommon.StateFactory
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_le : PrimrecRel fun x1 x2 => x1 ≤ x2
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- `v` is invertible if `diagonal v` is  -/
Matrix.invertibleOfDiagonalInvertible : {n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (v : n → α) → [Invertible (Matrix.diagonal v)] → Invertible v
-- Mathlib.Order.Atoms
IsSimpleOrder.of_forall_eq_top : ∀ {α : Type u_4} [inst : LE α] [inst_1 : BoundedOrder α] [Nontrivial α], (∀ (a : α), a ≠ ⊥ → a = ⊤) → IsSimpleOrder α
-- Mathlib.Data.Sum.Interval
Sum.Ioo_inl_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (a₁ a₂ : α),
  Finset.Ioo (Sum.inl a₁) (Sum.inl a₂) = Finset.map Function.Embedding.inl (Finset.Ioo a₁ a₂)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ (α × β)]
  (t : Std.DTreeMap.Internal.Impl α fun x => β) (l : ρ) (h : t.Balanced),
  Std.DTreeMap.Internal.Impl.Const.insertMany t l h =
    (have r := ⟨t, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | (a, b) =>
              have hr := ⋯;
              have r := ⟨(Std.DTreeMap.Internal.Impl.insert a b (↑r) hr).impl, ⋯⟩;
              pure (ForInStep.yield r)
      have r : Std.DTreeMap.Internal.Impl.Const.IteratedInsertionInto t := __s
      pure r).run
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.toAut.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1)
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).obj]
  [inst_3 : CategoryTheory.PreGaloisCategory.IsNaturalSMul F G],
  CategoryTheory.PreGaloisCategory.toAut F G = CategoryTheory.PreGaloisCategory.toAut F G
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instPartialOrder : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Max α] →
      [inst_1 : Bot α] → [inst_2 : SemilatticeSup β] → [inst_3 : OrderBot β] → PartialOrder (SupBotHom α β)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function has bounded variation, then the variation on closed semi-infinite intervals
tends to `0`. We give a version with a generic filter, that applies both to left-neighborhoods of
points and to `atTop`.  -/
BoundedVariationOn.tendsto_eVariationOn_Ici_zero_of_filter : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  BoundedVariationOn f s →
    ∀ (L : Filter α), (∀ y ∈ s, s ∩ Set.Ici y ∈ L) → Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Ici y)) L (nhds 0)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
trichotomy_of_add_eq_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] {a b c d : α} [AddLeftStrictMono α] [AddRightStrictMono α],
  a + b = c + d → a = c ∧ b = d ∨ a < c ∨ b < d
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
/-- A functor `F : C ⥤ H` has a right derived functor with respect to
`W : MorphismProperty C` if it has a left Kan extension along
`W.Q : C ⥤ W.Localization` (or any localization functor `L : C ⥤ D`
for `W`, see `hasRightDerivedFunctor_iff`).  -/
CategoryTheory.Functor.HasRightDerivedFunctor : {C : Type u_1} →
  {H : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_5, u_2} H] →
        CategoryTheory.Functor C H → CategoryTheory.MorphismProperty C → Prop
-- Lean.Parser.Term
Lean.Parser.Term.let_tmp.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.smul_eq_zero : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [IsDomain R] (b : Module.Basis ι R M) {c : R} {x : M}, c • x = 0 ↔ c = 0 ∨ x = 0
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Version of `minpoly_eq` using `ExpChar`.  -/
IsPurelyInseparable.minpoly_eq' : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] (p : ℕ) [ExpChar K p] (a : L),
  minpoly K a =
    Polynomial.X ^ p ^ IsPurelyInseparable.elemExponent K a - Polynomial.C (IsPurelyInseparable.elemReduct K a)
-- Mathlib.AlgebraicGeometry.Noetherian
/-- If `R` is a Noetherian ring, `Spec R` is a Noetherian scheme.  -/
AlgebraicGeometry.instIsNoetherianSpecOfIsNoetherianRingCarrier : ∀ {R : CommRingCat} [IsNoetherianRing ↑R], AlgebraicGeometry.IsNoetherian (AlgebraicGeometry.Spec R)
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.unique : ∀ (p q r : ENNReal) [p.HolderTriple q r] (r' : ENNReal) [hr' : p.HolderTriple q r'], r = r'
-- Mathlib.Analysis.MeanInequalities
/-- **Young's inequality** equality condition, `ℝ≥0` version.  -/
NNReal.young_inequality_eq_iff : ∀ (a b : NNReal) {p q : NNReal}, p.HolderConjugate q → (a * b = a ^ ↑p / p + b ^ ↑q / q ↔ a ^ ↑p = b ^ ↑q)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.σ_zero_nerveEquiv_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : C),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (CategoryTheory.nerve C) 0))
      (CategoryTheory.nerveEquiv.symm x) =
    CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.CategoryStruct.id x)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_div_product : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t : Finset α},
  Finset.image (fun x => x.1 / x.2) (s ×ˢ t) = s / t
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput.out : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} → (self : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput old) → self.aig.Ref
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.finsetSum'`. -/
MeasureTheory.ProgMeasurable.finset_sum' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : MeasurableSpace ι] {γ : Type u_4} [inst_3 : AddCommMonoid β]
  [ContinuousAdd β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsStronglyProgressive f (U c)) → MeasureTheory.IsStronglyProgressive f (∑ c ∈ s, U c)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiff.sub_section : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x},
  (ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, s x⟩) →
    (ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, t x⟩) →
      ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, (s - t) x⟩
-- Std.Tactic.Do.Syntax
/-- `mrevert` is like `revert`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ P → R := by
  mintro ⟨HP, HQ, HR⟩
  mrevert HR
  mrevert HP
  mintro HP'
  mintro HR'
  mexact HR'
```
 -/
Lean.Parser.Tactic.mrevertError : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_mem_range : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o a : Ordinal.{u}}, Order.IsNormal f → Ordinal.veblenWith f o a ∈ Set.range f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.size : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → ℕ
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
/-- The isomorphism `(opFunctor.obj X).obj n ≅ X.obj n` when `X` is a simplicial object.  -/
SimplicialObject.opObjIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      {n : SimplexCategoryᵒᵖ} → (SimplicialObject.opFunctor.obj X).obj n ≅ X.obj n
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.map_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →A[R] B), f 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpIdIso_hom_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : CategoryTheory.AddGrp C),
  (CategoryTheory.Functor.mapAddGrpIdIso.hom.app X).hom.hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.ModelTheory.Syntax
/-- A bijection sending formulas with constants to formulas with extra free variables.  -/
FirstOrder.Language.BoundedFormula.constantsVarsEquiv : {L : FirstOrder.Language} →
  {α : Type u'} → {γ : Type u_1} → {n : ℕ} → (L.withConstants γ).BoundedFormula α n ≃ L.BoundedFormula (γ ⊕ α) n
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.lie_incl_mem_ker : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] {E : LieAlgebra.Extension R M L} (x : E.L) (y : M),
  ⁅x, E.incl y⁆ ∈ E.proj.ker
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_φ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp S.L₀X₂ToP S.φ₁ = 0
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_left_H : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ) (hpq : (c r).prev pq' = pq)
  (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') [inst_3 : X.HasSpectralSequence data]
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀
          i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).left.H =
    X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.Analysis.Complex.OpenMapping
/-- Corollary to the open mapping theorem: A holomorphic function whose real part is constant is itself
constant.
 -/
AnalyticOnNhd.eq_re_add_const_mul_I_of_re_eq_const : ∀ {f : ℂ → ℂ} {U : Set ℂ} {c₀ : ℝ},
  AnalyticOnNhd ℂ f U → (∀ x ∈ U, (f x).re = c₀) → IsOpen U → IsConnected U → ∃ c, ∀ x ∈ U, f x = ↑c₀ + ↑c * Complex.I
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i),
  CategoryTheory.CategoryStruct.comp (X.δ i) (X.σ j) =
    CategoryTheory.CategoryStruct.comp (X.σ (j.castLT ⋯)) (X.δ (i.pred ⋯))
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.instCommMonoidWithZero : {α : Type u_1} →
  [DecidableEq α] → [inst : CommMonoidWithZero α] → [NoZeroDivisors α] → [Nontrivial α] → CommMonoidWithZero (WithTop α)
-- Mathlib.Order.Filter.Prod
Filter.compl_mem_coprod : ∀ {α : Type u_1} {β : Type u_2} {s : Set (α × β)} {la : Filter α} {lb : Filter β},
  sᶜ ∈ la.coprod lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.exp_eq_one_iff_of_im_nonneg : ∀ {x : ℂ}, 0 ≤ x.im → (Complex.exp x = 1 ↔ ∃ n, x = ↑n * (2 * ↑Real.pi * Complex.I))
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.atIdxSlow?_zip : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂]
  [Std.Iterators.Productive α₁ Id] [Std.Iterators.Productive α₂ Id] {it₁ : Std.Iter β₁} {it₂ : Std.Iter β₂} {n : ℕ},
  Std.Iter.atIdxSlow? n (it₁.zip it₂) = do
    let __do_lift ← Std.Iter.atIdxSlow? n it₁
    let __do_lift_1 ← Std.Iter.atIdxSlow? n it₂
    pure (__do_lift, __do_lift_1)
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The direction of a Monge plane.  -/
Affine.Simplex.direction_mongePlane : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) {i₁ i₂ : Fin (n + 3)},
  (s.mongePlane i₁ i₂).direction = (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.comp_lift_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {V W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) {Z : C} (h_1 : X ⨯ Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift g h) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp f g)
        (CategoryTheory.CategoryStruct.comp f h))
      h_1
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Converting an augmented simplicial object to an augmented cosimplicial
object and back is isomorphic to the given object.  -/
CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (X : CategoryTheory.SimplicialObject.Augmented C) → X.rightOp.leftOp ≅ X
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.isPreimmersion_eq_inf : @AlgebraicGeometry.IsPreimmersion =
  @AlgebraicGeometry.SurjectiveOnStalks ⊓
    AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsEmbedding
-- Mathlib.MeasureTheory.Group.AEStabilizer
MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {x_1 y : G} {s : Set α},
  x_1 +ᵥ s =ᵐ[μ] s → y ∈ AddSubgroup.zmultiples x_1 → y +ᵥ s =ᵐ[μ] s
-- Init.Data.Rat.Lemmas
Rat.add_sub_cancel : ∀ {a b : ℚ}, a + b - b = a
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : Ring R]
  [inst_3 : TopologicalSpace R] [IsTopologicalRing R] [T2Space R] (𝒢 : Subgroup (GL n R)) [DiscreteTopology ↥𝒢],
  DiscreteTopology ↥𝒢.adjoinNegOne
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.function_id_comp : ∀ {α : Type u} {β : Type v} {f : α → β}, id ∘ f = f
-- Lean.Meta.Tactic.Grind.Finish
Lean.Meta.Grind.Action.mkFinish : optParam ℕ Lean.Meta.Grind.Action.maxIterationsDefault → IO Lean.Meta.Grind.Action
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- `𝔸(n; S)` is functorial w.r.t. `n`.  -/
AlgebraicGeometry.AffineSpace.reindex : {n m : Type u} →
  (m → n) → (S : AlgebraicGeometry.Scheme) → AlgebraicGeometry.AffineSpace n S ⟶ AlgebraicGeometry.AffineSpace m S
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.hasCtor : Lean.Meta.Match.Problem → Bool
-- Mathlib.Lean.Meta.Simp
/-- Constructs a proof that the original expression is true
given a simp result which simplifies the target to `True`.
 -/
Lean.Meta.Simp.Result.ofTrue : Lean.Meta.Simp.Result → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- This is the `List.prod` version of `mul_inv`  -/
List.prod_inv : ∀ {K : Type u_8} [inst : DivisionCommMonoid K] (L : List K), L.prod⁻¹ = (List.map (fun x => x⁻¹) L).prod
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_toUInt32 : ∀ (n : UInt16), n.toUInt32.toUInt64 = n.toUInt64
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.δ_comp_toMk₁_of_lt : ∀ {n : ℕ} (i : Fin (n + 3)) (j : Fin (n + 2)) (h : j.castSucc < i),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (SimplexCategory.toMk₁ i) = SimplexCategory.toMk₁ (i.pred ⋯)
-- Mathlib.LinearAlgebra.Complex.Module
/-- The natural `ℝ`-linear equivalence between `selfAdjoint ℂ` and `ℝ`.  -/
Complex.selfAdjointEquiv : ↥(selfAdjoint ℂ) ≃ₗ[ℝ] ℝ
-- Mathlib.Analysis.Analytic.IteratedFDeriv
FormalMultilinearSeries.iteratedFDerivSeries.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F),
  p.iteratedFDerivSeries 0 = (↑↑(continuousMultilinearCurryFin0 𝕜 E F).symm).compFormalMultilinearSeries p
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.natCast_kronecker_natCast : ∀ {α : Type u_3} {m : Type u_10} {n : Type u_11} [inst : NonAssocSemiring α] [inst_1 : DecidableEq m]
  [inst_2 : DecidableEq n] (a b : ℕ), Matrix.kroneckerMap (fun x1 x2 => x1 * x2) ↑a ↑b = ↑(a * b)
-- Mathlib.Data.ENat.Basic
ENat.top_pow : ∀ {n : ℕ}, n ≠ 0 → ⊤ ^ n = ⊤
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.toList_roc : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => β),
  t.Ordered →
    ∀ (lowerBound upperBound : α),
      Std.Slice.toList (Std.Roc.Sliceable.mkSlice t lowerBound<...=upperBound) =
        List.filter (fun e => decide ((compare e.1 lowerBound).isGT = true ∧ (compare e.1 upperBound).isLE = true))
          (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.neighborSet_subgraphOfAdj_subset : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (hvw : G.Adj v w), (G.subgraphOfAdj hvw).neighborSet u ⊆ {v, w}
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_subset_mul_left : ∀ {α : Type u_2} [inst : Mul α] {s t₁ t₂ : Set α}, t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂
-- Init.Grind.Lemmas
Lean.Grind.eq_congr : ∀ {α : Sort u} {a₁ b₁ a₂ b₂ : α}, a₁ = a₂ → b₁ = b₂ → (a₁ = b₁) = (a₂ = b₂)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_aux.eq_1 : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2),
  newton_seq_aux✝ hnorm 0 = ⟨a, ⋯⟩
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The `NonUnitalSubsemiring` generated by a multiplicative subsemigroup coincides with the
`NonUnitalSubsemiring.closure` of the subsemigroup itself .  -/
Subsemigroup.nonUnitalSubsemiringClosure_eq_closure : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (M : Subsemigroup R),
  M.nonUnitalSubsemiringClosure = NonUnitalSubsemiring.closure ↑M
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P) →
      RingHom.StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.Data.Set.Prod
/-- The projection $(X \times_Y Z) \times_X (X \times_Y Z) \to Z \times_Y Z$.  -/
Function.PullbackSelf.map_snd : {X : Type u_1} →
  {Y : Sort u_2} →
    {Z : Type u_3} → {f : X → Y} → {g : Z → Y} → Function.PullbackSelf Function.Pullback.fst → Function.PullbackSelf g
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.reflectsIsomorphisms_forget : ∀ {R : Type u} [inst : CommRing R], (CategoryTheory.forget (CommHopfAlgCat R)).ReflectsIsomorphisms
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If we have a coproduct of `X` and `Y`, we can access it using `coprod X Y` or `X ⨿ Y`.  -/
CategoryTheory.Limits.coprod : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (X Y : C) → [CategoryTheory.Limits.HasBinaryCoproduct X Y] → C
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.c₂.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {inst_2 : DecidableEq (K →+* ℂ)}
  [inst_3 : DecidableEq (K →+* ℂ)], NumberField.house.c₂✝ K = NumberField.house.c₂✝ K
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- Two semilinear maps `M ⊗ (N ⊗ P) ⊗ Q → P₂` which agree on all elements of the
form `m ⊗ₜ (n ⊗ₜ p) ⊗ₜ q` are equal.  -/
TensorProduct.ext_fourfold'' : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P : Type u_9} {Q : Type u_10} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid P] [inst_5 : AddCommMonoid Q] [inst_6 : AddCommMonoid P₂] [inst_7 : Module R M]
  [inst_8 : Module R N] [inst_9 : Module R₂ P₂] [inst_10 : Module R P] [inst_11 : Module R Q]
  {φ ψ : TensorProduct R (TensorProduct R M (TensorProduct R N P)) Q →ₛₗ[σ₁₂] P₂},
  (∀ (w : M) (x : N) (y : P) (z : Q), φ (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z) = ψ (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z)) → φ = ψ
-- Mathlib.Data.Set.BoolIndicator
Set.preimage_boolIndicator_true : ∀ {α : Type u_1} (s : Set α), s.boolIndicator ⁻¹' {true} = s
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
MeasureTheory.Measure.IsFiniteMeasureOnCompacts.map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  [mβ : TopologicalSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β] (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : α ≃ₜ β),
  MeasureTheory.IsFiniteMeasureOnCompacts (MeasureTheory.Measure.map (⇑f) μ)
-- Init.Data.FloatArray.Basic
FloatArray.uset : (a : FloatArray) → (i : USize) → Float → autoParam (i.toNat < a.size) FloatArray.uset._auto_1 → FloatArray