mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `eq_condition f f'`, for morphisms `f f' : j ⟶ j'`, is the proof that
`eqHom f f' ≫ f = eqHom f f' ≫ f'`.
 -/
CategoryTheory.IsCofiltered.eq_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {j j' : C}
  (f f' : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') f'
-- Mathlib.Data.Set.Notation
/-- Given two sets `A` and `B`, `A ↓∩ B` denotes the intersection of `A` and `B` as a set in `Set A`.

The notation is short for `((↑) ⁻¹' B : Set A)`, while giving hints to the elaborator
that both `A` and `B` are terms of `Set α` for the same `α`.
This set is the same as `{x : ↑A | ↑x ∈ B}`.
 -/
Set.Notation.«term_↓∩_» : Lean.TrailingParserDescr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β] {f : β → β},
  Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.Const.modify m k f) k =
    (Option.map f (Std.ExtDHashMap.Const.get? m k)).get!
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_mul₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  AEMeasurable f μ → AEMeasurable g μ → μ.withDensity (f * g) = (μ.withDensity f).withDensity g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_eq_getElem?_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey? = t.keysArray[0]?
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a functor `F` preserves the right homology of a short complex `S`, this is the
canonical isomorphism `(S.map F).homology ≅ F.obj S.homology`.  -/
CategoryTheory.ShortComplex.mapHomologyIso' : {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) →
              (F : CategoryTheory.Functor C D) →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : S.HasHomology] →
                    [inst_6 : (S.map F).HasHomology] →
                      [F.PreservesRightHomologyOf S] → (S.map F).homology ≅ F.obj S.homology
-- Aesop.Tree.TreeM
Aesop.Tree.mk.injEq : ∀ (root : Aesop.MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) (numGoals numRapps : ℕ)
  (nextGoalId : Aesop.GoalId) (nextRappId : Aesop.RappId) (allIntroducedMVars : Std.HashSet Lean.MVarId)
  (root_1 : Aesop.MVarClusterRef) (rootMetaState_1 : Lean.Meta.SavedState) (numGoals_1 numRapps_1 : ℕ)
  (nextGoalId_1 : Aesop.GoalId) (nextRappId_1 : Aesop.RappId) (allIntroducedMVars_1 : Std.HashSet Lean.MVarId),
  ({ root := root, rootMetaState := rootMetaState, numGoals := numGoals, numRapps := numRapps, nextGoalId := nextGoalId,
        nextRappId := nextRappId, allIntroducedMVars := allIntroducedMVars } =
      { root := root_1, rootMetaState := rootMetaState_1, numGoals := numGoals_1, numRapps := numRapps_1,
        nextGoalId := nextGoalId_1, nextRappId := nextRappId_1, allIntroducedMVars := allIntroducedMVars_1 }) =
    (root = root_1 ∧
      rootMetaState = rootMetaState_1 ∧
        numGoals = numGoals_1 ∧
          numRapps = numRapps_1 ∧
            nextGoalId = nextGoalId_1 ∧ nextRappId = nextRappId_1 ∧ allIntroducedMVars = allIntroducedMVars_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
CategoryTheory.PreservesImage.factorThruImage_comp_hom : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Limits.HasEqualizers A] [inst_3 : CategoryTheory.Limits.HasImages A]
  [inst_4 : CategoryTheory.StrongEpiCategory B] [inst_5 : CategoryTheory.Limits.HasImages B]
  (L : CategoryTheory.Functor A B)
  [inst_6 :
    ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L]
  [inst_7 :
    ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L]
  {X Y : A} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (L.map f))
      (CategoryTheory.PreservesImage.iso L f).hom =
    L.map (CategoryTheory.Limits.factorThruImage f)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.monotone_semilength : Monotone DyckWord.semilength
-- Mathlib.Algebra.Group.Invertible.Defs
mul_left_inj_of_invertible : ∀ {α : Type u} [inst : Monoid α] {a b : α} (c : α) [Invertible c], a * c = b * c ↔ a = b
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.zero_X : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {i : σ}, MvPowerSeries.HasSubst ![0, MvPowerSeries.X i]
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.equivOfEq_rfl : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  S.equivOfEq S ⋯ = AlgEquiv.refl
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAt.matches_slice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos endPos : s.Pos}
  (h : String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos),
  String.Slice.Pattern.Model.PatternModel.Matches pat (s.slice startPos endPos ⋯).copy
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
instBracketAddGroupLieAlgebra.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G],
  instBracketAddGroupLieAlgebra =
    { bracket := fun v w => VectorField.mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w) 0 }
-- Mathlib.Algebra.Notation.Prod
Prod.instPow.eq_1 : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : Pow α E] [inst_1 : Pow β E],
  Prod.instPow = { pow := fun p c => (p.1 ^ c, p.2 ^ c) }
-- Init.Data.Option.Lemmas
Option.min_eq_left_of_lt : ∀ {α : Type u_1} [inst : LT α] [inst_1 : Min α],
  (∀ (x y : α), x < y → x ⊓ y = x) → ∀ {a b : Option α}, a < b → a ⊓ b = a
-- Mathlib.Order.Filter.Bases.Basic
Filter.le_iff_forall_inf_principal_compl : ∀ {α : Type u_1} {f g : Filter α}, f ≤ g ↔ ∀ V ∈ g, f ⊓ Filter.principal Vᶜ = ⊥
-- Init.Data.SInt.Lemmas
Int8.le_or_lt : ∀ (a b : Int8), a ≤ b ∨ b < a
-- Mathlib.CategoryTheory.Abelian.SerreClass.Basic
CategoryTheory.ObjectProperty.IsSerreClass.toIsClosedUnderQuotients : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Abelian C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsSerreClass], P.IsClosedUnderQuotients
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- Fixing submonoid of union is intersection  -/
fixingSubmonoid_union : ∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : MulAction M α] {s t : Set α},
  fixingSubmonoid M (s ∪ t) = fixingSubmonoid M s ⊓ fixingSubmonoid M t
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- Represent `log (1 + z)` as an integral over the unit interval  -/
Complex.log_eq_integral : ∀ {z : ℂ}, 1 + z ∈ Complex.slitPlane → Complex.log (1 + z) = z * ∫ (t : ℝ) in 0..1, (1 + t • z)⁻¹
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- Any element of the spectrum of a selfadjoint is real.  -/
IsSelfAdjoint.im_eq_zero_of_mem_spectrum : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a : A}, IsSelfAdjoint a → ∀ {z : ℂ}, z ∈ spectrum ℂ a → z.im = 0
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indep_iSup_of_directed_le : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {m1 _mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ],
  (∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ) →
    (∀ (i : ι), m i ≤ _mΩ) → m1 ≤ _mΩ → Directed (fun x1 x2 => x1 ≤ x2) m → ProbabilityTheory.Indep (⨆ i, m i) m1 μ
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.coreComp_inv_app_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (X : CategoryTheory.Core C),
  ((F.coreComp G).inv.app X).iso.hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.of))
-- Init.Data.UInt.Lemmas
UInt32.toNat_ofFin : ∀ (x : Fin UInt32.size), (UInt32.ofFin x).toNat = ↑x
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- The angle at the center of a circle equals twice the angle at the circumference, oriented vector
angle form with the radius specified.  -/
Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y z : V},
  x ≠ y → x ≠ z → ∀ {r : ℝ}, ‖x‖ = r → ‖y‖ = r → ‖z‖ = r → o.oangle y z = 2 • o.oangle (y - x) (z - x)
-- Mathlib.Algebra.Order.Floor.Defs
FloorRing.mk : {α : Type u_4} →
  [inst : Ring α] →
    [inst_1 : LinearOrder α] →
      (floor ceil : α → ℤ) → GaloisConnection Int.cast floor → GaloisConnection ceil Int.cast → FloorRing α
-- Mathlib.NumberTheory.FunctionField
FunctionField.finiteDimensional_of_adjoin_transcendental : ∀ {F : Type u_3} {K : Type u_4} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (RatFunc F) K] [FunctionField F K]
  [inst_4 : Algebra F K] [IsScalarTower F (RatFunc F) K] {y : K}, Transcendental F y → FiniteDimensional (↥F⟮y⟯) K
-- Mathlib.Data.Fintype.Quotient
Trunc.finChoiceEquiv_apply : ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] {α : ι → Sort u_2} (q : (i : ι) → Trunc (α i)),
  Trunc.finChoiceEquiv q = Trunc.finChoice q
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.pred : Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Λ'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.instIsIsoWhiskerRight : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ')
  [CategoryTheory.IsIso η] {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''},
  CategoryTheory.IsIso (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ)
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.le_total : ∀ (A : Type u) [inst : CommRing A] (K : Type v) [inst_1 : Field K] [inst_2 : Algebra A K] [inst_3 : IsDomain A]
  [ValuationRing A] [IsFractionRing A K] (a b : ValuationRing.ValueGroup A K), a ≤ b ∨ b ≤ a
-- Mathlib.Data.Num.Lemmas
PosNum.cast_bit0 : ∀ {α : Type u_1} [inst : One α] [inst_1 : Add α] (n : PosNum), ↑n.bit0 = ↑n + ↑n
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instAdd.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Add G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffAdd I' n G], ContMDiffMap.instAdd = { add := fun f g => ⟨⇑f + ⇑g, ⋯⟩ }
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsFiniteLimits F
-- Mathlib.Algebra.Order.SuccPred.TypeTags
Order.pred_ofAdd : ∀ {X : Type u_1} [inst : Preorder X] [inst_1 : PredOrder X] (x : X),
  Order.pred (Multiplicative.ofAdd x) = Multiplicative.ofAdd (Order.pred x)
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
/-- `factorPow` for `m = n + 1`  -/
Ideal.Quotient.factorPowSucc : {R : Type u_1} → [inst : Ring R] → (I : Ideal R) → [inst_1 : I.IsTwoSided] → (n : ℕ) → R ⧸ I ^ (n + 1) →+* R ⧸ I ^ n
-- Init.Data.List.Nat.Count
List.IsSuffix.le_count : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α},
  l₁ <:+ l₂ → ∀ (a : α), List.count a l₂ - (l₂.length - l₁.length) ≤ List.count a l₁
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.instZeroHom_1 : {M N : AddCommGrpCat} → Zero (M ⟶ N)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isEmpty_filter_key_eq_true : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {f : α → Bool} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst) l).isEmpty = true ↔
      ∀ (k : α) (h : Std.Internal.List.containsKey k l = true), f (Std.Internal.List.getKey k l h) = false)
-- Mathlib.Logic.Basic
/-- **Alias** of `ne_of_eq_of_ne`. -/
Eq.trans_ne : ∀ {α : Sort u_1} {a b c : α}, a = b → b ≠ c → a ≠ c
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RccSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : SizeOf β]
  (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Rcc α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.WF.merge : ∀ {α : Type u_1} {le : α → α → Bool} {s₁ s₂ : Batteries.PairingHeapImp.Heap α},
  Batteries.PairingHeapImp.Heap.WF le s₁ →
    Batteries.PairingHeapImp.Heap.WF le s₂ →
      Batteries.PairingHeapImp.Heap.WF le (Batteries.PairingHeapImp.Heap.merge le s₁ s₂)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) {Z : CommRingCat} (h : (↑U).presheaf.obj (Opposite.op ⊤) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop U.toSpecΓ) h =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom
      (CategoryTheory.CategoryStruct.comp U.topIso.inv h)
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
MeasureTheory.Measure.addHaar.congr_simp : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : LocallyCompactSpace G],
  MeasureTheory.Measure.addHaar = MeasureTheory.Measure.addHaar
-- Init.Data.SInt.Lemmas
Int64.ofInt_bitVecToInt : ∀ (n : BitVec 64), Int64.ofInt n.toInt = Int64.ofBitVec n
-- Mathlib.Order.Basic
Decidable.eq_or_lt_of_le' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α} [DecidableLE α], b ≤ a → a = b ∨ b < a
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_one`. -/
SkewMonoidAlgebra.toFinsupp_one : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k], SkewMonoidAlgebra.coeff 1 = fun₀ | 1 => 1
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instContinuousSMul : ∀ {M : Type u_1} {X : Type u_2} [inst : SMul M X] [inst_1 : TopologicalSpace M] [inst_2 : TopologicalSpace X]
  [inst_3 : ContinuousSMul M X], ContinuousSMul M (SeparationQuotient X)
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_blockDiag' : ∀ {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace R] {A : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R},
  Continuous A → Continuous fun x => (A x).blockDiag'
-- Mathlib.Algebra.DirectSum.Ring
/-- Multiplication from the right with any graded component's zero vanishes.  -/
DirectSum.GNonUnitalNonAssocSemiring.mul_zero : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : Add ι} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  [self : DirectSum.GNonUnitalNonAssocSemiring A] {i j : ι} (a : A i), GradedMonoid.GMul.mul a 0 = 0
-- Lean.Meta.Closure
Lean.Meta.Closure.MkValueTypeClosureResult.mk.sizeOf_spec : ∀ (levelParams : Array Lean.Name) (type value : Lean.Expr) (levelArgs : Array Lean.Level) (exprArgs : Array Lean.Expr),
  sizeOf { levelParams := levelParams, type := type, value := value, levelArgs := levelArgs, exprArgs := exprArgs } =
    1 + sizeOf levelParams + sizeOf type + sizeOf value + sizeOf levelArgs + sizeOf exprArgs
-- Mathlib.Algebra.BigOperators.Intervals
/-- Telescopic product over `Fin`.  -/
Fin.prod_Iic_div : ∀ {M : Type u_3} [inst : CommGroup M] {n : ℕ} (a : Fin n) (f : Fin (n + 1) → M),
  ∏ i ≤ a, f i.succ / f i.castSucc = f a.succ / f 0
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangleIso.inv.hom₁ = ((DerivedCategory.singleFunctorsPostcompQIso C).inv.hom 0).app S.X₁
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- The number of side goals created.  -/
Mathlib.Tactic.ClickSuggestions.RwKey.numGoals : Mathlib.Tactic.ClickSuggestions.RwKey → ℕ
-- Mathlib.Algebra.NeZero
four_ne_zero' : ∀ (α : Type u_2) [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], 4 ≠ 0
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (m.insertMany l).getKeyD k' fallback = k
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_codRestrict : ∀ {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) (p : Subalgebra R B) (h : ∀ (x : A), f x ∈ p), ↑(f.codRestrict p h) = (↑f).codRestrict p h
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_minKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insertIfNew k v).minKey?.isSome = true
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_subset_uIcc_self : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.uIoo a b ⊆ Set.uIcc a b
-- Init.Data.Rat.Basic
Rat.mk'.injEq : ∀ (num : ℤ) (den : ℕ) (den_nz : autoParam (den ≠ 0) Rat.den_nz._autoParam)
  (reduced : autoParam (num.natAbs.Coprime den) Rat.reduced._autoParam) (num_1 : ℤ) (den_1 : ℕ)
  (den_nz_1 : autoParam (den_1 ≠ 0) Rat.den_nz._autoParam)
  (reduced_1 : autoParam (num_1.natAbs.Coprime den_1) Rat.reduced._autoParam),
  ({ num := num, den := den, den_nz := den_nz, reduced := reduced } =
      { num := num_1, den := den_1, den_nz := den_nz_1, reduced := reduced_1 }) =
    (num = num_1 ∧ den = den_1)
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.GeneralLinearGroup.swap.eq_1 : ∀ (R : Type u_1) {n : Type u_2} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j : n),
  Matrix.GeneralLinearGroup.swap R i j =
    { val := Matrix.swap R i j, inv := Matrix.swap R i j, val_inv := ⋯, inv_val := ⋯ }
-- Mathlib.Algebra.Order.Pi
Pi.one_lt_mulSingle : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : DecidableEq ι] [inst_1 : (i : ι) → One (α i)]
  [inst_2 : (i : ι) → Preorder (α i)] {i : ι} {a : α i}, 1 < Pi.mulSingle i a ↔ 1 < a
-- Lean.Expr
Lean.instInhabitedBinderInfo : Inhabited Lean.BinderInfo
-- Lean.ToExpr
Lean.instToExprRat.mkNat : ℕ → Lean.Expr
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `IsLeftCancelMul` across an `Equiv`  -/
Equiv.isLeftCancelMul : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Mul β] [IsLeftCancelMul β], IsLeftCancelMul α
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_eq_zero : ∀ {R : Type u} {a : R} [inst : Semiring R], Polynomial.C a = 0 ↔ a = 0
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instReprSpan : Repr Std.Time.Nanosecond.Span
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow.eq_1 : ∀ (n : ℕ), n.primesBelow = {p ∈ Finset.range n | Nat.Prime p}
-- Mathlib.Data.PFun
PFun.dom_mk : ∀ {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : (a : α) → p a → β),
  (PFun.Dom fun x => { Dom := p x, get := f x }) = {x | p x}
-- Mathlib.Combinatorics.Tiling.Tile
/-- The tiles in the protoset. Use the coercion to a function rather than using `tiles`
directly.  -/
DiscreteTiling.Protoset.tiles : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      [inst : Group G] → [inst_1 : MulAction G X] → DiscreteTiling.Protoset G X ιₚ → ιₚ → DiscreteTiling.Prototile G X
-- Mathlib.Algebra.Module.Presentation.DirectSum
/-- The direct sum operations on `Relations A`. Given a family
`relations : ι → Relations A`, the type of generators and relations
in `directSum relations` are the corresponding `Sigma` types.  -/
Module.Relations.directSum : {A : Type u} → [inst : Ring A] → {ι : Type w} → (ι → Module.Relations A) → Module.Relations A
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.ins.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (y : α)
  (parent : RBTree.RBNode.Path α) (b : RBTree.RBNode α) (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b) a)
  (h_3 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent) b)
  (h_4 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b) a)
  (h_5 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent) b),
  (match RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a => h_2 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b => h_3 a y parent b
    | RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a => h_4 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b => h_5 a y parent b) =
    h_3 a y parent b
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_smul : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace β] [inst_1 : Group α] [inst_2 : MulAction α β]
  [ContinuousConstSMul α β] {s : Set α} {t : Set β} [inst_4 : TopologicalSpace α],
  interior s • interior t ⊆ interior (s • t)
-- Init.Data.UInt.Lemmas
UInt16.ofInt_neg : ∀ (x : ℤ), UInt16.ofInt (-x) = -UInt16.ofInt x