mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Quotation
/-- Given `rhss` the right-hand-sides of a `match`-syntax notation,
We tag them with fresh identifiers `alt_idx`. We use them to detect whether an alternative
has been used or not.
The result is a triple `(altIdxMap, ignoreIfUnused, rhssNew)` where
- `altIdxMap` is a mapping from the `alt_idx` identifiers to right-hand-side indices.
  That is, the map contains the entry `alt_idx ↦ i` if `alt_idx` was used to mark `rhss[i]`.
- `i ∈ ignoreIfUnused` if `rhss[i]` is marked with `no_error_if_unused%`
- `rhssNew` is the updated array of right-hand-sides.
 -/
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.markRhss : Array Lean.Term → Lean.Elab.TermElabM (Lean.NameMap ℕ × Lean.Elab.Term.Quotation.IdxSet × Array Lean.Term)
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidalFunctor_obj : ∀ {M : Type u} [inst : AddMonoid M] {N : Type u'} [inst_1 : AddMonoid N] (F : M →+ N) (m : M),
  (CategoryTheory.Discrete.addMonoidalFunctor F).obj { as := m } = { as := F m }
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.eq_zero_of_mul_eq_zero_of_smul : ∀ {R : Type u} [inst : CommSemiring R] (P : Polynomial R),
  (∀ (r : R), r • P = 0 → r = 0) → ∀ (Q : Polynomial R), P * Q = 0 → Q = 0
-- Lean.Elab.Do.Basic
/-- A mutable variable declared by `let mut` in a `do` block.  -/
Lean.Elab.Do.MutVar : Type
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.presburgerFunc.add : FirstOrder.presburgerFunc 2
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indResAdjunction.eq_1 : ∀ (k : Type u) {G : Type v} {H : Type v'} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H),
  Rep.indResAdjunction k φ =
    CategoryTheory.Adjunction.mkOfHomEquiv
      { homEquiv := fun A B => (Rep.indResHomEquiv φ A B).toEquiv, homEquiv_naturality_left_symm := ⋯,
        homEquiv_naturality_right := ⋯ }
-- Batteries.Data.List.Perm
List.Subperm.cons_left : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α],
  l₁.Subperm l₂ → ∀ (x : α), List.count x l₁ < List.count x l₂ → (x :: l₁).Subperm l₂
-- Std.Sat.AIG.Basic
/-- Get the inverter bit.
 -/
Std.Sat.AIG.Fanin.invert : Std.Sat.AIG.Fanin → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_const_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a : E → 𝔸},
  DifferentiableAt 𝕜 a x → ∀ (b : 𝔸), fderiv 𝕜 (fun y => b * a y) x = b • fderiv 𝕜 a x
-- Mathlib.Data.Finset.Image
/-- When `f` is an embedding of `α` in `β` and `s` is a finset in `α`, then `s.map f` is the image
finset in `β`. The embedding condition guarantees that there are no duplicates in the image.  -/
Finset.map : {α : Type u_1} → {β : Type u_2} → (α ↪ β) → Finset α → Finset β
-- Aesop.Util.Unfold
Aesop.unfoldMany : (Lean.Name → Option (Option Lean.Name)) → Lean.Expr → Lean.MetaM (Option (Lean.Expr × Array Lean.Name))
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.instIsIsoFunctorTypeιTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)},
  CategoryTheory.IsIso ⊤.ι
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ShortComplex.mk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X₁ X₂ X₃ : C} (f f_1 : X₁ ⟶ X₂) (e_f : f = f_1) (g g_1 : X₂ ⟶ X₃) (e_g : g = g_1)
  (zero : CategoryTheory.CategoryStruct.comp f g = 0),
  { X₁ := X₁, X₂ := X₂, X₃ := X₃, f := f, g := g, zero := zero } =
    { X₁ := X₁, X₂ := X₂, X₃ := X₃, f := f_1, g := g_1, zero := ⋯ }
-- Mathlib.LinearAlgebra.Dimension.Localization
/-- If `K` is the fraction ring of `A` and `L` is the fraction ring of `B`, then the finrank
`finrank K L` of the fraction rings equals the finrank `finrank A B` of the base rings.

See `IsFractionRing.finrank_left_eq` and `IsFractionRing.finrank_right_eq` for one-sided versions.
See `Algebra.IsAlgebraic.rank_of_isFractionRing` for a rank version with additional assumptions.  -/
IsFractionRing.finrank_eq : ∀ (A : Type u_1) (K : Type u_2) (B : Type u_3) (L : Type u_4) [inst : CommRing A] [inst_1 : CommRing K]
  [inst_2 : CommRing B] [inst_3 : CommRing L] [inst_4 : Algebra A B] [inst_5 : Module K L] [inst_6 : Algebra A K]
  [inst_7 : Algebra B L] [inst_8 : Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsFractionRing A K]
  [IsFractionRing B L], Module.finrank K L = Module.finrank A B
-- Mathlib.Algebra.Algebra.StrictPositivity
IsStrictlyPositive.spectrum_pos : ∀ {A : Type u_1} {𝕜 : Type u_2} [inst : Ring A] [inst_1 : PartialOrder A] [inst_2 : CommSemiring 𝕜]
  [inst_3 : PartialOrder 𝕜] [inst_4 : Algebra 𝕜 A] [NonnegSpectrumClass 𝕜 A] {a : A},
  IsStrictlyPositive a → ∀ {x : 𝕜}, x ∈ spectrum 𝕜 a → 0 < x
-- Mathlib.Order.Closure
LowerAdjoint.mk.sizeOf_spec : ∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toFun : α → β) (gc' : GaloisConnection toFun u), sizeOf { toFun := toFun, gc' := gc' } = 1
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A product of a function over a `Finset` in a subtype equals a
product in the main type of a function that agrees with the first
function on that `Finset`.  -/
Finset.prod_subtype_map_embedding : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {p : ι → Prop} {s : Finset { x // p x }} {f : { x // p x } → M}
  {g : ι → M}, (∀ x ∈ s, g ↑x = f x) → ∏ x ∈ Finset.map (Function.Embedding.subtype fun x => p x) s, g x = ∏ x ∈ s, f x
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.ext_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β}, f = g ↔ ∀ (x : α), f x = g x
-- Batteries.Data.String.Lemmas
String.anyAux_of_valid : ∀ (p : Char → Bool) (l m r : List Char),
  String.Legacy.anyAux (String.ofList (l ++ m ++ r)) { byteIdx := String.utf8Len l + String.utf8Len m } p
      { byteIdx := String.utf8Len l } =
    m.any p
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addCHaar_mono : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {K₁ K₂ : TopologicalSpace.Compacts G},
  ↑K₁ ⊆ ↑K₂ → MeasureTheory.Measure.haar.addCHaar K₀ K₁ ≤ MeasureTheory.Measure.haar.addCHaar K₀ K₂
-- Init.Data.Int.Linear
Int.Internal.Linear.le_unsat : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly),
  p.isUnsatLe = true → Int.Internal.Linear.Poly.denote' ctx p ≤ 0 → False
-- Mathlib.Order.JordanHolder
CompositionSeries.toList_sorted : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X),
  (RelSeries.toList s).SortedLT
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- A type synonym used for the compact coherentification of a topological space.  -/
CompactCoherentification : Type u_1 → Type u_1
-- Mathlib.CategoryTheory.Abelian.Basic
/-- There is a canonical isomorphism between the abelian coimage and the abelian image of a
morphism.  -/
CategoryTheory.Abelian.coimageIsoImage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Abelian.coimage f ≅ CategoryTheory.Abelian.image f
-- Mathlib.Data.Set.Semiring
SetSemiring.add_def : ∀ {α : Type u_1} (s t : SetSemiring α), s + t = Set.up (SetSemiring.down s ∪ SetSemiring.down t)
-- Init.Data.Array.Erase
Array.eraseP_append_left : ∀ {α : Type u_1} {p : α → Bool} {a : α},
  p a = true → ∀ {xs ys : Array α}, a ∈ xs → (xs ++ ys).eraseP p = xs.eraseP p ++ ys
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (n d : aig.RefVec w)
  (wn wr : ℕ) (q r : aig.RefVec w) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr n d wn wr q r).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr n d wn wr q r).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.encode.match_1.eq_1 : ∀ (motive : Mathlib.Deriving.Encodable.S✝ → Sort u_1) (n : ℕ)
  (h_1 : (n : ℕ) → motive (Mathlib.Deriving.Encodable.S.nat✝ n))
  (h_2 : (a b : Mathlib.Deriving.Encodable.S✝) → motive (Mathlib.Deriving.Encodable.S.cons✝ a b)),
  (match Mathlib.Deriving.Encodable.S.nat✝ n with
    | Mathlib.Deriving.Encodable.S.nat✝ n => h_1 n
    | Mathlib.Deriving.Encodable.S.cons✝ a b => h_2 a b) =
    h_1 n
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- Graded ring homomorphisms preserve multiplication.  -/
GradedRingHom.map_mul : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) (a b : A), f (a * b) = f a * f b
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainBotCoeff_neg : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  LieModule.chainBotCoeff (-α) β = LieModule.chainTopCoeff α β
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- **Alias** of `Metric.Snowflaking.preimage_toSnowflaking_closedEBall`. -/
Metric.Snowflaking.preimage_toSnowflaking_emetricClosedBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁)
  (d : ENNReal),
  ⇑Metric.Snowflaking.toSnowflaking ⁻¹' Metric.closedEBall x d =
    Metric.closedEBall (Metric.Snowflaking.ofSnowflaking x) (d ^ α⁻¹)
-- Std.Time.DateTime
/-- Creates a new `DateTime` out of a `Timestamp` and a `ZoneRules`.
 -/
Std.Time.DateTime.ofTimestamp : Std.Time.Timestamp → Std.Time.TimeZone.ZoneRules → Std.Time.DateTime
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_mul_finrank_top : ∀ {E : Type v} [inst : Field E] {A B : Subfield E},
  A ≤ B → A.relfinrank B * Module.finrank (↥B) E = Module.finrank (↥A) E
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] (f : α →*₀o β), f.comp (OrderMonoidWithZeroHom.id α) = f
-- Mathlib.Order.Hom.Lattice
SupHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Max α] → [inst_1 : Max β] → (toFun : α → β) → (∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b) → SupHom α β
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_sub_nat_mul_pi : ∀ (x : ℝ) (n : ℕ), Real.sin (x - ↑n * Real.pi) = (-1) ^ n * Real.sin x
-- Std.Time.Date.Unit.Day
Std.Time.Day.Ordinal.instLawfulEqOrdOfYear : ∀ {leap : Bool}, Std.LawfulEqOrd (Std.Time.Day.Ordinal.OfYear leap)
-- Mathlib.Algebra.Order.IsBotOne
min_one : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : One α] [IsBotOneClass α] (a : α), min a 1 = 1
-- Init.Data.List.Erase
List.le_length_erase : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, l.length - 1 ≤ (l.erase a).length
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformlyOn.congr : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] {f' : ι → β → α},
  HasProdUniformlyOn f g s →
    (∀ᶠ (n : Finset ι) in Filter.atTop, Set.EqOn (fun x => ∏ i ∈ n, f i x) (fun x => ∏ i ∈ n, f' i x) s) →
      HasProdUniformlyOn f' g s
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_le_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t → ∀ {fallback : α}, (cmp (t.minD fallback) k).isLE = true
-- Mathlib.Algebra.Order.Floor.Div
/-- Do not use this. Use `ceilDiv_nonpos` instead.  -/
CeilDiv.ceilDiv_nonpos : ∀ {α : Type u_2} {β : Type u_3} {inst : AddCommMonoid α} {inst_1 : PartialOrder α} {inst_2 : AddCommMonoid β}
  {inst_3 : PartialOrder β} {inst_4 : SMulZeroClass α β} [self : CeilDiv α β] ⦃a : α⦄, a ≤ 0 → ∀ (b : β), b ⌈/⌉ a = 0
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.map_smul₂ : ∀ {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedField 𝕜₂]
  [inst_1 : NormedField 𝕜₃] [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜₃ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : AddCommGroup G]
  [inst_9 : Module 𝕜₃ G] [inst_10 : TopologicalSpace G] [inst_11 : IsTopologicalAddGroup G]
  [inst_12 : ContinuousConstSMul 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →L[𝕜₃] F →SL[σ₂₃] G) (c : 𝕜₃) (x : E) (y : F),
  (f (c • x)) y = c • (f x) y
-- Mathlib.Data.Fintype.OfMap
/-- Given an injective function to a fintype, the domain is also a
fintype. This is noncomputable because injectivity alone cannot be
used to construct preimages.  -/
Fintype.ofInjective : {α : Type u_1} → {β : Type u_2} → [Fintype β] → (f : α → β) → Function.Injective f → Fintype α
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.ExprWithHoles.ref : Lean.Elab.Term.ExprWithHoles✝ → Lean.Syntax
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.modify.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (f : β a → β a)
  (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.modify a f x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => Std.DHashMap.Internal.AssocList.nil
    | Std.DHashMap.Internal.AssocList.cons k v l =>
      if h : (k == a) = true then
        have h' := ⋯;
        have b := f (cast ⋯ v);
        Std.DHashMap.Internal.AssocList.cons a b l
      else Std.DHashMap.Internal.AssocList.cons k v (Std.DHashMap.Internal.AssocList.modify a f l)
-- Mathlib.GroupTheory.OrderOfElement
infinite_not_isOfFinAddOrder : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] {x : G}, ¬IsOfFinAddOrder x → {y | ¬IsOfFinAddOrder y}.Infinite
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.type.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {expr : Lean.Expr}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Arg._auto_1} {expr_1 : Lean.Expr}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Arg._auto_1},
  Lean.Compiler.LCNF.Arg.type expr h = Lean.Compiler.LCNF.Arg.type expr_1 h_1 → expr = expr_1
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- If `C` has all limits, it has finite limits.  -/
CategoryTheory.Limits.hasFiniteLimits_of_hasLimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C],
  CategoryTheory.Limits.HasFiniteLimits C
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.instEssSurjCoalgebraToComonadAdjComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C),
  (CategoryTheory.Comonad.comparison G.adj).EssSurj
-- Mathlib.Algebra.Lie.TensorProduct
/-- The universal property for tensor product of modules of a Lie algebra: the `R`-linear
tensor-hom adjunction is equivariant with respect to the `L` action.  -/
TensorProduct.LieModule.lift : (R : Type u) →
  [inst : CommRing R] →
    (L : Type v) →
      (M : Type w) →
        (N : Type w₁) →
          (P : Type w₂) →
            [inst_1 : LieRing L] →
              [inst_2 : LieAlgebra R L] →
                [inst_3 : AddCommGroup M] →
                  [inst_4 : Module R M] →
                    [inst_5 : LieRingModule L M] →
                      [inst_6 : LieModule R L M] →
                        [inst_7 : AddCommGroup N] →
                          [inst_8 : Module R N] →
                            [inst_9 : LieRingModule L N] →
                              [inst_10 : LieModule R L N] →
                                [inst_11 : AddCommGroup P] →
                                  [inst_12 : Module R P] →
                                    [inst_13 : LieRingModule L P] →
                                      [inst_14 : LieModule R L P] →
                                        (M →ₗ[R] N →ₗ[R] P) ≃ₗ⁅R,L⁆ TensorProduct R M N →ₗ[R] P
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If a family is affinely independent, and the spans of points
indexed by two subsets of the index type have a point in common, those
subsets of the index type have an element in common, if the underlying
ring is nontrivial.  -/
AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P},
  AffineIndependent k p →
    ∀ {s1 s2 : Set ι} {p0 : P}, p0 ∈ affineSpan k (p '' s1) → p0 ∈ affineSpan k (p '' s2) → ∃ i, i ∈ s1 ∩ s2
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.map_K : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.IsPreservedBy F],
  (h.map F).K = F.obj h.K
-- Mathlib.Data.Setoid.Basic
/-- The quotient by the trivial relation is equivalent to the original space.  -/
Setoid.quotientBotEquiv : {α : Type u_1} → Quotient ⊥ ≃ α
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Poly.denoteS.match_1.splitter : (motive : Lean.Grind.CommRing.Poly → Sort u_1) →
  (p : Lean.Grind.CommRing.Poly) →
    ((k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k)) →
      ((k : ℤ) →
          (m : Lean.Grind.CommRing.Mon) →
            (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p)) →
        motive p
-- Mathlib.Logic.Denumerable
/-- An infinite encodable type is denumerable.  -/
Denumerable.ofEncodableOfInfinite : (α : Type u_3) → [Encodable α] → [Infinite α] → Denumerable α
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toStarAlgHom_symm_ofStarAlgHom : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] [inst_5 : Star A₁] [inst_6 : Star A₂] (f : A₁ →⋆ₐ[R] A₂)
  (g : A₂ →⋆ₐ[R] A₁) (h₁ : g.comp f = StarAlgHom.id R A₁) (h₂ : f.comp g = StarAlgHom.id R A₂),
  (StarAlgEquiv.ofStarAlgHom f g h₁ h₂).symm.toStarAlgHom = g
-- Mathlib.Analysis.MeanInequalities
_private.Mathlib.Analysis.MeanInequalities.0.NNReal.inner_le_Lp_mul_Lp_of_norm_le_one : ∀ {ι : Type u} (s : Finset ι) (f g : ι → NNReal) {p q : ℝ},
  p.HolderConjugate q → ∑ i ∈ s, f i ^ p ≤ 1 → ∑ i ∈ s, g i ^ q ≤ 1 → ∑ i ∈ s, f i * g i ≤ 1
-- Init.Data.List.Nat.Range
List.le_snd_of_mem_zipIdx : ∀ {α : Type u_1} {x : α × ℕ} {k : ℕ} {l : List α}, x ∈ l.zipIdx k → k ≤ x.2
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppScalarRight_smul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {ι : Type u_5}
  [inst_7 : DecidableEq ι] (s : S) (t : TensorProduct R M (ι →₀ R)),
  (TensorProduct.finsuppScalarRight R S M ι) (s • t) = s • (TensorProduct.finsuppScalarRight R S M ι) t
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.two_dvd_card_support : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α}, σ ^ 2 = 1 → 2 ∣ σ.support.card
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the largest key that is less than the given key,
returning `none` if no such key exists.
 -/
Std.ExtTreeMap.getKeyLT? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → Option α
-- Mathlib.Algebra.Algebra.Unitization
Unitization.toProd_surjective : ∀ {R : Type u_1} {A : Type u_2}, Function.Surjective Unitization.toProd
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.map_dite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} {P : Prop} [inst_2 : Decidable P] (f : P → (X ⟶ Y)) (g : ¬P → (X ⟶ Y)),
  F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h)
-- Mathlib.Order.Lattice.Nat
Nat.iInf_of_empty : ∀ {ι : Sort u_1} [IsEmpty ι] (f : ι → ℕ), iInf f = 0
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.map_isGreatest : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  LeftOrdContinuous f → ∀ {s : Set α} {x : α}, IsGreatest s x → IsGreatest (f '' s) (f x)
-- Mathlib.Algebra.Group.Conj
/-- An `AddMonoidHom` maps additive conjugacy classes of one additive group to
additive conjugacy classes of another.  -/
AddConjClasses.map : {α : Type u} →
  {β : Type v} → [inst : AddMonoid α] → [inst_1 : AddMonoid β] → (α →+ β) → AddConjClasses α → AddConjClasses β
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.le_tsub_iff_left : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable a → a ≤ c → (b ≤ c - a ↔ a + b ≤ c)
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A finprod of meromorphic functions in normal form is in normal form if at most one of the factors
vanishes.
 -/
meromorphicNFOn_finprod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {ι : Type u_3} {f : ι → 𝕜 → 𝕜},
  (∀ (i : ι), MeromorphicNFOn (f i) U) → (∀ x ∈ U, {σ | f σ x = 0}.Subsingleton) → MeromorphicNFOn (∏ᶠ (i : ι), f i) U
-- Mathlib.Logic.Equiv.Prod
/-- The equivalence between a product of two dependent functions types and a single dependent
function type. Basically a symmetric version of `Equiv.sumPiEquivProdPi`.  -/
Equiv.prodPiEquivSumPi : {ι : Type u_9} →
  {ι' : Type u_10} →
    (π : ι → Type u) → (π' : ι' → Type u) → ((i : ι) → π i) × ((i' : ι') → π' i') ≃ ((i : ι ⊕ ι') → Sum.elim π π' i)
-- Init.PropLemmas
exists_eq_right_right' : ∀ {α : Sort u_1} {p q : α → Prop} {a' : α}, (∃ a, p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a'
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- If `F : C ⥤ D` is a fully faithful monoidal functor, then
`F.mapGrp : Grp C ⥤ Grp D` is fully faithful too.  -/
CategoryTheory.Functor.FullyFaithful.mapGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {F : CategoryTheory.Functor C D} → [inst_4 : F.Monoidal] → F.FullyFaithful → F.mapGrp.FullyFaithful
-- Mathlib.NumberTheory.ModularForms.NormTrace
ModularForm.norm_ne_zero : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} {f : F} [inst : FunLike F UpperHalfPlane ℂ]
  {k : ℤ} [inst_1 : 𝒢.IsFiniteRelIndex ℋ] [inst_2 : ℋ.HasDetPlusMinusOne] [inst_3 : ModularFormClass F 𝒢 k],
  ⇑f ≠ 0 → ModularForm.norm ℋ f ≠ 0
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.pi_top : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)] (I : Set η), (Subgroup.pi I fun i => ⊤) = ⊤
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The right whiskering of an isomorphism is an isomorphism.  -/
CategoryTheory.MonoidalCategory.«term_▷ᵢ_» : Lean.TrailingParserDescr