mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.map_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.LimitPresentation J X) {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape J F],
  (P.map F).π =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.constComp J X F).inv
      (CategoryTheory.Functor.whiskerRight P.π F)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  (X_1 : CategoryTheory.Sheaf (J.over Z) A) (X_2 : (CategoryTheory.Over X)ᵒᵖ),
  ((J.overMapPullbackComp A f g).inv.app X_1).hom.app X_2 =
    X_1.obj.map ((CategoryTheory.Over.mapComp f g).inv.app (Opposite.unop X_2)).op
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.apply_eq_iff_symm_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N) {x : M} {y : N}, e x = y ↔ x = e.symm y
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.dirichletInverseFun.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (f : ℕ → R) (hf : Invertible (f 1)) (n : ℕ),
  ArithmeticFunction.dirichletInverseFun f hf n =
    if n = 0 then 0
    else
      if n = 1 then ⅟(f 1)
      else
        -⅟(f 1) *
          ∑ d,
            have this := ⋯;
            f (n / ↑d) * ArithmeticFunction.dirichletInverseFun f hf ↑d
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- A smooth Riemannian metric defines in particular a Riemannian metric.  -/
Bundle.ContMDiffRiemannianMetric.toRiemannianMetric : {EB : Type u_1} →
  [inst : NormedAddCommGroup EB] →
    [inst_1 : NormedSpace ℝ EB] →
      {HB : Type u_2} →
        [inst_2 : TopologicalSpace HB] →
          {IB : ModelWithCorners ℝ EB HB} →
            {n : WithTop ℕ∞} →
              {B : Type u_3} →
                [inst_3 : TopologicalSpace B] →
                  [inst_4 : ChartedSpace HB B] →
                    {F : Type u_4} →
                      [inst_5 : NormedAddCommGroup F] →
                        [inst_6 : NormedSpace ℝ F] →
                          {E : B → Type u_5} →
                            [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] →
                              [inst_8 : (b : B) → TopologicalSpace (E b)] →
                                [inst_9 : (b : B) → AddCommGroup (E b)] →
                                  [inst_10 : (b : B) → Module ℝ (E b)] →
                                    [inst_11 : FiberBundle F E] →
                                      [inst_12 : VectorBundle ℝ F E] →
                                        Bundle.ContMDiffRiemannianMetric IB n F E → Bundle.RiemannianMetric E
-- Mathlib.CategoryTheory.Products.Basic
/-- The Cartesian product of two natural isomorphisms.  -/
CategoryTheory.NatIso.prod : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {D : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                {F F' : CategoryTheory.Functor A B} →
                  {G G' : CategoryTheory.Functor C D} → (F ≅ F') → (G ≅ G') → (F.prod G ≅ F'.prod G')
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biprod.ofComponents_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂)
  (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
      CategoryTheory.Limits.biprod.snd =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f₁₂ +
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd f₂₂
-- Mathlib.Algebra.Group.Hom.Defs
map_eq_one_iff : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
  [OneHomClass F M N] (f : F), Function.Injective ⇑f → ∀ {x : M}, f x = 1 ↔ x = 1
-- Mathlib.Geometry.Manifold.PoincareConjecture
_private.Mathlib.Geometry.Manifold.PoincareConjecture.0.ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere : (M : Type u_1) →
  [inst : TopologicalSpace M] →
    [T2Space M] →
      (n : ℕ) →
        [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] →
          ProofWanted (∀ (a : ContinuousMap.HomotopyEquiv M ↑(Metric.sphere 0 1)), Nonempty (M ≃ₜ ↑(Metric.sphere 0 1)))
-- Std.Sat.AIG.Lemmas
_private.Std.Sat.AIG.Lemmas.0.Std.Sat.AIG.toGraphviz.go.match_1.eq_1 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1)
  (h_1 : Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx : α) → Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx))
  (h_3 :
    (lhs rhs : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match elem : Std.Sat.AIG.Decl.false with
    | Std.Sat.AIG.Decl.false => h_1 elem
    | Std.Sat.AIG.Decl.atom idx => h_2 idx elem
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs elem) =
    h_1 ⋯
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.coe_zero : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G], ⇑0 = 0
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_mem : ∀ {α : Type u_2} [inst : SemilatticeInf α] (s : Set α),
  (∀ x ∈ s, ∀ y ∈ s, x ⊓ y ∈ s) →
    ∀ {ι : Type u_7} (t : Finset ι) (H : t.Nonempty) (p : ι → α), (∀ i ∈ t, p i ∈ s) → t.inf' H p ∈ s
-- Mathlib.Order.Ideal
Order.Cofinal.mk : {P : Type u_2} → [inst : Preorder P] → (carrier : Set P) → IsCofinal carrier → Order.Cofinal P
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapIsometry_apply_coveringRadius : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ᵢ Y) (D : Delone.DeloneSet X),
  ((Delone.DeloneSet.mapIsometry f) D).coveringRadius = D.coveringRadius
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.NamespaceEntry.mk.injEq : ∀ (name : List Lean.Name) (stx selection : Lean.Syntax) (prevSiblings : Array Lean.Lsp.DocumentSymbol)
  (name_1 : List Lean.Name) (stx_1 selection_1 : Lean.Syntax) (prevSiblings_1 : Array Lean.Lsp.DocumentSymbol),
  ({ name := name, stx := stx, selection := selection, prevSiblings := prevSiblings } =
      { name := name_1, stx := stx_1, selection := selection_1, prevSiblings := prevSiblings_1 }) =
    (name = name_1 ∧ stx = stx_1 ∧ selection = selection_1 ∧ prevSiblings = prevSiblings_1)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan
Measurable.arctan : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => Real.arctan (f x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_filter_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool} {k k' : α},
  t.getKey? k = some k' →
    Std.DTreeMap.Const.get? (Std.DTreeMap.filter f t) k = Option.filter (fun x => f k' x) (Std.DTreeMap.Const.get? t k)
-- Mathlib.Data.Num.Basic
Num.pos.sizeOf_spec : ∀ (a : PosNum), sizeOf (Num.pos a) = 1 + sizeOf a
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.errorAtSavedPos.parenthesizer : String → Bool → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimit_of_succ_lt : ∀ {α : Type u_1} {b : α} [inst : PartialOrder α] [inst_1 : SuccOrder α],
  (∀ a < b, Order.succ a < b) → Order.IsSuccPrelimit b
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_eq_bot : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree = ⊥ ↔ p = 0
-- Lean.Elab.App
Lean.Elab.Term.LValResolution.projFn.inj : ∀ {baseStructName structName fieldName : Lean.Name} {levels : List Lean.Level}
  {baseStructName_1 structName_1 fieldName_1 : Lean.Name} {levels_1 : List Lean.Level},
  Lean.Elab.Term.LValResolution.projFn baseStructName structName fieldName levels =
      Lean.Elab.Term.LValResolution.projFn baseStructName_1 structName_1 fieldName_1 levels_1 →
    baseStructName = baseStructName_1 ∧ structName = structName_1 ∧ fieldName = fieldName_1 ∧ levels = levels_1
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.rTensorAlgEquiv_apply : ∀ {R : Type u} {N : Type v} [inst : CommSemiring R] {σ : Type u_1} {S : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : CommSemiring N] [inst_4 : Algebra R N] (x : TensorProduct R N (MvPolynomial σ S)),
  MvPolynomial.rTensorAlgEquiv x = MvPolynomial.rTensorAlgHom x
-- Mathlib.Topology.MetricSpace.Infsep
Finset.infsep_zero_iff_subsingleton : ∀ {α : Type u_1} [inst : MetricSpace α] (s : Finset α), (↑s).infsep = 0 ↔ (↑s).Subsingleton
-- Mathlib.Order.Lattice
OrderDual.instDistribLattice : (α : Type u_1) → [DistribLattice α] → DistribLattice αᵒᵈ
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instOrdOrdinal : Ord Std.Time.Hour.Ordinal
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `finsum_mem_union_inter` that requires `s ∩ support f` and
`t ∩ support f` rather than `s` and `t` to be finite.  -/
finsum_mem_union_inter' : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
  (s ∩ Function.support f).Finite →
    (t ∩ Function.support f).Finite →
      ∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i + ∑ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
        ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- `leftRetraction` splits `ι`  -/
CategoryTheory.IsSplitEqualizer.ι_leftRetraction_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X}
  (self : CategoryTheory.IsSplitEqualizer f g ι) {Z : C} (h : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp ι (CategoryTheory.CategoryStruct.comp self.leftRetraction h) = h
-- Mathlib.Order.Monotone.Monovary
AntitoneOn.antivaryOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι} [inst_2 : LinearOrder ι], AntitoneOn f s → MonotoneOn g s → AntivaryOn f g s
-- Mathlib.Tactic.Widget.Calc
/-- Create a `calc` proof.  -/
Lean.Elab.Tactic.tacticCalc? : Lean.ParserDescr
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {km : α}, t.min? = some km → t.get! km = km
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.op_w : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  (L : Φ.LeftResolution X₂), L.op.w = L.w.op
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.upperBound?_eq_find? : ∀ {α : Type u_1} {x : α} {t : RBTree.RBNode α} {cut : α → Ordering} (ub : Option α),
  RBTree.RBNode.find? cut t = some x → RBTree.RBNode.upperBound? cut t ub = some x
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.assoc_toLinearEquiv : ∀ (R : Type uR) (S : Type uS) (T : Type u_2) (A : Type uA) (C : Type uC) (D : Type uD) [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Algebra S C]
  [inst_10 : IsScalarTower R S C] [inst_11 : Semiring D] [inst_12 : Algebra R D] [inst_13 : CommSemiring T]
  [inst_14 : Algebra R T] [inst_15 : Algebra S T] [inst_16 : Algebra T A] [inst_17 : IsScalarTower R T A]
  [inst_18 : IsScalarTower S T A],
  ↑(Algebra.TensorProduct.assoc R S T A C D) = TensorProduct.AlgebraTensorModule.assoc R S T A C D
-- Lean.Meta.AppBuilder
/-- Given `h₁ : a = b` and `h₂ : b = c`, returns a proof of `a = c`.  -/
Lean.Meta.mkEqTrans : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.norm_of : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), (FreeGroup.of a).norm = 1
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_lt : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α],
  |a| < b ↔ -b < a ∧ a < b
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.natCast_mul : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a b : ℕ), ↑(a * b) = ↑a * ↑b
-- Mathlib.Analysis.Analytic.IteratedFDeriv
FormalMultilinearSeries.iteratedFDerivSeries.eq_def : ∀ {𝕜 : 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) (k : ℕ),
  p.iteratedFDerivSeries k =
    match k with
    | 0 => (↑↑(continuousMultilinearCurryFin0 𝕜 E F).symm).compFormalMultilinearSeries p
    | k.succ =>
      (↑↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm).compFormalMultilinearSeries
        (p.iteratedFDerivSeries k).derivSeries
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.ofHom.eq_1 : ∀ {X Y : Type u} [inst : Mul X] [inst_1 : Mul Y] (f : X →ₙ* Y),
  MagmaCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Batteries.Data.Array.Match
/-- Prefix table for the Knuth-Morris-Pratt matching algorithm

This is an array of the form `t = [(x₀,n₀), (x₁,n₁), (x₂, n₂), ...]` where for each `i`, `nᵢ` is
the length of the longest proper prefix of `xs = [x₀,x₁,...,xᵢ]` which is also a suffix of `xs`.
 -/
Array.PrefixTable : Type u_1 → Type u_1
-- Mathlib.GroupTheory.Finiteness
/-- Finite product of finitely generated additive subgroups is finitely generated.  -/
AddSubgroup.FG.pi : ∀ {ι : Type u_5} [Finite ι] {G : ι → Type u_6} [inst : (i : ι) → AddGroup (G i)] {P : (i : ι) → AddSubgroup (G i)},
  (∀ (i : ι), (P i).FG) → (AddSubgroup.pi Set.univ P).FG
-- Mathlib.LinearAlgebra.Dimension.Localization
IsLocalization.linearIndepOn_finsetIntegerMultiple : ∀ {R : Type uR} {S : Type uS} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A : Type u_1}
  [inst_3 : CommRing A] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A] (M : Submonoid S)
  [inst_7 : IsLocalization M A] [FaithfulSMul S A] {s : Finset A},
  LinearIndepOn R id ↑s → ∀ [inst_9 : DecidableEq S], LinearIndepOn R id ↑(IsLocalization.finsetIntegerMultiple M s)
-- Mathlib.Data.List.Lemmas
List.foldl_range_eq_of_range_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → α} {g : α → γ → α},
  ((Set.range fun a c => f c a) = Set.range fun b c => g c b) →
    ∀ (a : α), Set.range (List.foldl f a) = Set.range (List.foldl g a)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The inverse of a bijective `DistribMulActionHom` is a `DistribMulActionHom`.  -/
DistribMulActionHom.inverse : {M : Type u_1} →
  [inst : Monoid M] →
    {A : Type u_4} →
      [inst_1 : AddMonoid A] →
        [inst_2 : DistribMulAction M A] →
          {B₁ : Type u_6} →
            [inst_3 : AddMonoid B₁] →
              [inst_4 : DistribMulAction M B₁] →
                (f : A →+[M] B₁) → (g : B₁ → A) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → B₁ →+[M] A
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.splitMin'.match_3.splitter : {α : Type u_1} →
  (motive : Ordnode α → α → Ordnode α → Sort u_2) →
    (x : Ordnode α) →
      (x_1 : α) →
        (x_2 : Ordnode α) →
          ((x : α) → (r : Ordnode α) → motive Ordnode.nil x r) →
            ((size : ℕ) →
                (ll : Ordnode α) →
                  (lx : α) → (lr : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node size ll lx lr) x r) →
              motive x x_1 x_2
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- **Alias** of the reverse direction of `SimpleGraph.neighborSet_eq_empty`. -/
SimpleGraph.IsIsolated.neighborSet_eq_empty : ∀ {V : Type u} (G : SimpleGraph V) {v : V}, G.IsIsolated v → G.neighborSet v = ∅
-- Init.Grind.AC
Lean.Grind.AC.Seq.contains_k.eq_1 : ∀ (s : Lean.Grind.AC.Seq) (x : Lean.Grind.AC.Var),
  s.contains_k x = Lean.Grind.AC.Seq.rec (fun y => Nat.beq x y) (fun y x_1 ih => (Nat.beq x y).or' ih) s
-- Batteries.Data.PairingHeap
/-- `O(n)`. Convert the heap to an array in arbitrary order.  -/
Batteries.PairingHeap.toArrayUnordered : {α : Type u} → {le : α → α → Bool} → Batteries.PairingHeap α le → Array α
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.respectsIso : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => RingHom.Flat
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indCoindNatIso.congr_simp : ∀ (k : Type u) {G : Type v} [inst : CommRing k] [inst_1 : Group G] (S : Subgroup G)
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex],
  Rep.indCoindNatIso k S = Rep.indCoindNatIso k S
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.coe_divRight : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] (a : G),
  ⇑(Homeomorph.divRight a) = fun x => x / a
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_inf_normal : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G) [hH : H.Normal] [hK : K.Normal], (H ⊓ K).Normal
-- Init.Data.Int.Gcd
Int.natAbs_div_gcd_pos_of_ne_zero_right : ∀ {b : ℤ} (a : ℤ), b ≠ 0 → 0 < b.natAbs / a.gcd b
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cochainComplexFunctor.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f f_1 : K ⟶ L) (e_f : f = f_1) [inst_2 : CategoryTheory.EnoughInjectives C]
  [inst_3 : CategoryTheory.Mono f] (n₀ n₀_1 : ℤ) (e_n₀ : n₀ = n₀_1) [inst_4 : K.IsStrictlyGE (n₀ + 1)]
  [inst_5 : L.IsStrictlyGE (n₀ + 1)],
  CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cochainComplexFunctor✝ f n₀ =
    CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cochainComplexFunctor✝ f_1 n₀_1
-- Plausible.Testable
Plausible.Testable.runPropE : (p : Prop) → [Plausible.Testable p] → Plausible.Configuration → Bool → Plausible.Gen (Plausible.TestResult p)
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- Reinterpret an equivalence relation as a reflexive relation.  -/
CategoryTheory.EquivalenceRelation.toReflexiveRelation : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} → {p₁ p₂ : R ⟶ X} → CategoryTheory.EquivalenceRelation p₁ p₂ → CategoryTheory.ReflexiveRelation p₁ p₂
-- Mathlib.CategoryTheory.Iso
CategoryTheory.asIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.IsIso f],
  CategoryTheory.asIso f = { hom := f, inv := CategoryTheory.inv f, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getLT?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getLT? k = t₂.getLT? k
-- Mathlib.Data.Multiset.Sections
Multiset.card_sections : ∀ {α : Type u_1} {s : Multiset (Multiset α)}, s.Sections.card = (Multiset.map Multiset.card s).prod
-- Mathlib.FieldTheory.FinTrdeg
instFinTrdegOfIsAlgebraic : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsAlgebraic K L],
  FinTrdeg K L
-- Mathlib.Data.Matrix.Mul
Matrix.single_vecMul_diagonal : ∀ {n : Type u_3} {R : Type u_7} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : NonUnitalNonAssocSemiring R]
  (v : n → R) (j : n) (x : R), Matrix.vecMul (Pi.single j x) (Matrix.diagonal v) = Pi.single j (x * v j)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS.eq_8 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (a : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteS ctx a.neg = 0
-- Mathlib.Topology.MetricSpace.DilationEquiv
/-- Type of equivalences `X ≃ Y` such that `∀ x y, edist (f x) (f y) = r * edist x y` for some
`r : ℝ≥0`, `r ≠ 0`.  -/
DilationEquiv : (X : Type u_1) → (Y : Type u_2) → [PseudoEMetricSpace X] → [PseudoEMetricSpace Y] → Type (max u_1 u_2)
-- Mathlib.Algebra.Lie.Abelian
/-- **Alias** of `isMulCommutative_iff_isLieAbelian`. -/
commutative_ring_iff_abelian_lie_ring : ∀ {A : Type v} [inst : Ring A], IsMulCommutative A ↔ IsLieAbelian A
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.prod_top : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α},
  la.HasBasis pa sa → (la ×ˢ ⊤).HasBasis pa fun x => sa x ×ˢ Set.univ
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The braiding natural isomorphism.  -/
CategoryTheory.BraidedCategory.braiding : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      [self : CategoryTheory.BraidedCategory C] →
        (X Y : C) →
          CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mem_range_iff : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f : E →ₗ.[R] F} {y : F}, y ∈ Set.range ↑f ↔ ∃ x, (x, y) ∈ f.graph
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.isIso_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), S.g = 0 → CategoryTheory.IsIso h.ι
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isUnramifiedIn_comap : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K]
  {w : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsUnramifiedIn K (w.comap (algebraMap k K)) ↔ NumberField.InfinitePlace.IsUnramified k w
-- Mathlib.Algebra.Torsor.Defs
/-- Cancellation adding the results of two subtractions.  -/
vsub_add_vsub_cancel : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p₁ p₂ p₃ : P), p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) = p₁ -ᵥ p₃
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_add_left_nhdsLT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousAdd H] {c a : H},
  Filter.map (fun x => c + x) (nhdsWithin a (Set.Iio a)) = nhdsWithin (c + a) (Set.Iio (c + a))
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.sum_X_index : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] {f : ℕ → R → S},
  f 1 0 = 0 → SkewPolynomial.X.sum f = f 1 1
-- Mathlib.Order.Lattice
Antitone.map_sup : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : SemilatticeInf β] {f : α → β},
  Antitone f → ∀ (x y : α), f (max x y) = f x ⊓ f y
-- Mathlib.Tactic.FunProp.Mor
/-- coercion `F → α → β`  -/
Mathlib.Meta.FunProp.Mor.Arg.coe : Mathlib.Meta.FunProp.Mor.Arg → Option Lean.Expr
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverMincard_finite_of_isCompact_invariant : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} [inst : UniformSpace X],
  IsCompact F → Set.MapsTo T F F → U ∈ uniformity X → ∀ (n : ℕ), Dynamics.coverMincard T F U n < ⊤
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.omega0_lt_epsilon : ∀ (o : Ordinal.{u_1}), Ordinal.omega0 < o.epsilon