mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorAdd'_inv_app_f' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (a b ab : ℤ) (h : a + b = ab) (n : ℤ),
  ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).inv.app K).f n =
    (HomologicalComplex.XIsoOfEq K ⋯).hom
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_castAdd : ∀ {m n : ℕ} {α : Fin (n + m + 1) → Sort u_2} (f : (i : Fin (n + m)) → α i.castSucc) (a : α (Fin.last (n + m)))
  (i : Fin n), Fin.snoc f a (Fin.castAdd (m + 1) i) = f (Fin.castAdd m i)
-- Mathlib.Algebra.CharP.Defs
ringChar.eq_zero : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [CharZero R], ringChar R = 0
-- Mathlib.Analysis.Convex.Between
Collinear.wbtw_or_wbtw_or_wbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Collinear R {x, y, z} → Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Focus.right : ∀ {σs : List (Type u)} {P Q Q' C R : Std.Do.SPred σs}, (Q ⊣⊢ₛ Q' ∧ R) → (P ∧ Q' ⊣⊢ₛ C) → P ∧ Q ⊣⊢ₛ C ∧ R
-- Init.Data.Range.Polymorphic.Basic
Std.Roo.mem_iff : ∀ {α : Type u} {r : Std.Roo α} {a : α} [inst : LT α], a ∈ r ↔ r.lower < a ∧ a < r.upper
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Limits.cocone_ι_app : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  {F : CategoryTheory.Functor J PartOrdEmb}
  {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))}
  (hc : CategoryTheory.Limits.IsColimit c) (j : J),
  (PartOrdEmb.Limits.cocone hc).ι.app j =
    PartOrdEmb.ofHom { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j)), inj' := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtype_symm_apply_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β) (e : α ≃ { y // y ≠ x }) (b : { y // y ≠ x }),
  (↑((Equiv.optionSubtype x).symm e)).symm ↑b = some (e.symm b)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Oriented angles are continuous when neither endpoint equals the middle point.  -/
EuclideanGeometry.continuousAt_oangle : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {x : P × P × P}, x.1 ≠ x.2.1 → x.2.2 ≠ x.2.1 → ContinuousAt (fun y => EuclideanGeometry.oangle y.1 y.2.1 y.2.2) x
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.vertex_injective : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X]
  [inst_3 : IsOrderedRing S] [Nontrivial S] [inst_5 : DecidableEq X], Function.Injective stdSimplex.vertex
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_subset_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, b₂ ≤ b₁ → a₁ < a₂ → Set.Ioc b₁ a₁ ⊆ Set.Ioo b₂ a₂
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.toComon_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommComon C), A.toComon.X = A.X
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
_private.Mathlib.FieldTheory.IsAlgClosed.Spectrum.0.spectrum.termσ_1 : Lean.ParserDescr
-- Mathlib.Data.Seq.Defs
Stream'.Seq.cons_injective2 : ∀ {α : Type u}, Function.Injective2 Stream'.Seq.cons
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The `d` field of `truncGE'`.  -/
HomologicalComplex.truncGE'.d : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [e.IsTruncGE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      (i j : ι) → HomologicalComplex.truncGE'.X K e i ⟶ HomologicalComplex.truncGE'.X K e j
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.mem_traceDual_iff_isIntegral : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [IsFractionRing A K]
  [IsIntegrallyClosed A] {I : Submodule B L} {x : L},
  x ∈ Submodule.traceDual A K I ↔ ∀ a ∈ I, IsIntegral A (((Algebra.traceForm K L) x) a)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedEMatchTheoremKind.default : Lean.Meta.Grind.EMatchTheoremKind
-- Init.Prelude
/-- The only element of the universe-polymorphic unit type.  -/
PUnit.unit : PUnit.{u}
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.RankFunction.wf_ancestralRel : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] [WellFoundedLT α]
  (f : P.RankFunction α), WellFounded P.AncestralRel
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.of.sizeOf_spec : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] [inst_1 : SizeOf ι]
  [inst_2 : (a : ι) → SizeOf (X a)] (carrier : Type v) [str : TopologicalSpace carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_insertManyIfNew_list : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : BEq α] [Std.LawfulBEqOrd α] [Std.TransOrd α]
  {l : List ((a : α) × β a)} {t : Std.DTreeMap.Internal.Impl α β} (h : t.WF),
  (↑(t.insertManyIfNew l ⋯)).toListModel.Perm (Std.Internal.List.insertListIfNew t.toListModel l)
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.toTopologicalSpace_sInf : ∀ {α : Type u} [inst : Group α] (s : Set (GroupTopology α)),
  (sInf s).toTopologicalSpace = sInf (GroupTopology.toTopologicalSpace '' s)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.comapMonoidHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6}
  [inst_2 : MulOneClass Z] (f : C(X, Y)) (g : LocallyConstant Y Z),
  (LocallyConstant.comapMonoidHom f) g = LocallyConstant.comap f g
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (c : R) [h : Decidable (c = 0)],
  (MvPolynomial.C c).support = if c = 0 then ∅ else {0}
-- Mathlib.Data.Rat.Floor
/-- `norm_num` extension for `Int.fract`  -/
Rat.evalIntFract : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {x y : E.Hom F},
  x.s₀ = y.s₀ →
    x.h₀ ≍ y.h₀ →
      @CategoryTheory.PreOneHypercover.Hom.s₁ C inst S E F x ≍ @CategoryTheory.PreOneHypercover.Hom.s₁ C inst S E F y →
        @CategoryTheory.PreOneHypercover.Hom.h₁ C inst S E F x ≍
            @CategoryTheory.PreOneHypercover.Hom.h₁ C inst S E F y →
          x = y
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.CommGrpCat.Hom.mk.injEq : ∀ {A B : CommGrpCat} (hom' hom'_1 : ↑A →* ↑B), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Order.DirSupClosed
IsLowerSet.dirSupInacc : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], IsLowerSet s → DirSupInacc s
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
writtenInExtChartAt_comp : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} {x : M} {s : Set M} {g : M' → M''},
  ContinuousWithinAt f s x →
    writtenInExtChartAt I I'' x
        (g ∘ f) =ᶠ[nhdsWithin (↑(extChartAt I x) x) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)]
      writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Add an entry to the `PreDiscrTree`.  -/
Lean.Meta.RefinedDiscrTree.PreDiscrTree.push : {α : Type} →
  Lean.Meta.RefinedDiscrTree.PreDiscrTree α →
    Lean.Meta.RefinedDiscrTree.Key →
      Lean.Meta.RefinedDiscrTree.LazyEntry × α → Lean.Meta.RefinedDiscrTree.PreDiscrTree α
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalTacticCDot : Lean.Elab.Tactic.Tactic
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_biUnion_toMeasurable : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {I : Set β},
  I.Countable → ∀ (s : β → Set α), μ (⋃ b ∈ I, MeasureTheory.toMeasurable μ (s b)) = μ (⋃ b ∈ I, s b)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer.0.CategoryTheory.Limits.WalkingMultispan.functorExt.match_1.splitter : {J : CategoryTheory.Limits.MultispanShape} →
  (motive : CategoryTheory.Limits.WalkingMultispan J → Sort u_3) →
    (j : CategoryTheory.Limits.WalkingMultispan J) →
      ((i : J.L) → motive (CategoryTheory.Limits.WalkingMultispan.left i)) →
        ((i : J.R) → motive (CategoryTheory.Limits.WalkingMultispan.right i)) → motive j
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.instMonoidalCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.MonoidalCategory (CategoryTheory.Dial C)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.subtype_comp_d₀₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom A.ρ.invariants.subtype) (groupCohomology.d₀₁ A) = 0
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- Interpret `Finsupp.single a` as a linear map.  -/
Finsupp.lsingle : {α : Type u_1} →
  {M : Type u_2} →
    {R : Type u_5} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → α → M →ₗ[R] α →₀ M
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddGroupOfAddOpposite : {M : Type u_1} → [AddGroup Mᵃᵒᵖ] → AddGroup Mᵈᵃᵃ
-- Mathlib.Algebra.Group.MinimalAxioms
Group.ofLeftAxioms.eq_1 : ∀ {G : Type u} [inst : Mul G] [inst_1 : Inv G] [inst_2 : One G] (assoc : ∀ (a b c : G), a * b * c = a * (b * c))
  (one_mul : ∀ (a : G), 1 * a = a) (inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1),
  Group.ofLeftAxioms assoc one_mul inv_mul_cancel =
    { toMul := inst, mul_assoc := assoc, toOne := inst_2, one_mul := one_mul, mul_one := ⋯, npow := npowRecAuto,
      npow_zero := ⋯, npow_succ := ⋯, toInv := inst_1, div := DivInvMonoid.div', zpow := zpowRec, div_eq_mul_inv := ⋯,
      zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := inv_mul_cancel }
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.laxMonoidalPi : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        {D : I → Type u₂} →
          [inst_2 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] →
            [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)] →
              (F : (i : I) → CategoryTheory.Functor (D i) (C i)) →
                [(i : I) → (F i).LaxMonoidal] → (CategoryTheory.Functor.pi F).LaxMonoidal
-- Mathlib.Data.Sigma.Order
Sigma.Lex.noMinOrder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → Preorder (α i)]
  [∀ (i : ι), NoMinOrder (α i)], NoMinOrder (Σₗ (i : ι), α i)
-- Mathlib.Topology.EMetricSpace.Defs
/-- Make a `PseudoEMetricSpace` from a metric. Warning: the uniformity and topology included herein
are the ones generated by the metric. If the type has a pre-existing topology or uniformity,
`PseudoEMetricSpace.ofEDistOfTopology` should be used instead.  -/
PseudoEMetricSpace.ofEDist : {α : Type u} →
  (edist : α → α → ENNReal) →
    (∀ (x : α), edist x x = 0) →
      (∀ (x y : α), edist x y = edist y x) → (∀ (x y z : α), edist x z ≤ edist x y + edist y z) → PseudoEMetricSpace α
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.head.eq_1 : Turing.ToPartrec.Code.head = Turing.ToPartrec.Code.id.cons Turing.ToPartrec.Code.nil
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
Finsupp.linearCombination_one_tmul : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) (ι : Type u_5) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring S] [inst_4 : Algebra R S] [inst_5 : DecidableEq ι] {v : ι → M},
  ↑R (Finsupp.linearCombination S fun x => 1 ⊗ₜ[R] v x) =
    LinearMap.lTensor S (Finsupp.linearCombination R v) ∘ₗ ↑(TensorProduct.finsuppScalarRight R R S ι).symm
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.mk : {A : Type u} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          (vars rels : Type) →
            (P : Algebra.Presentation A B vars rels) →
              (B →ₐ[A] MvPolynomial vars A ⧸ P.ker ^ 2) →
                (h : vars → MvPolynomial vars A) →
                  (p : rels → MvPolynomial rels (MvPolynomial vars A)) →
                    (∀ (j : rels), (p j).IsHomogeneous 2) →
                      (∀ (j : rels), (MvPolynomial.eval P.relation) (p j) = (MvPolynomial.aeval h) (P.relation j)) →
                        (q : vars → MvPolynomial rels P.Ring) →
                          (∀ (i : vars), (q i).IsHomogeneous 1) →
                            (∀ (i : vars), (MvPolynomial.eval P.relation) (q i) = h i - MvPolynomial.X i) →
                              Algebra.Smooth.DescentAux✝ A B
-- Mathlib.RingTheory.Ideal.Cotangent
/-- `I ⧸ I ^ 2` as a quotient of `I`.  -/
Ideal.Cotangent : {R : Type u} → [inst : CommRing R] → Ideal R → Type u
-- Mathlib.Analysis.Normed.Module.Basic
NormedAlgebra.id : (𝕜 : Type u_1) → [inst : NormedField 𝕜] → NormedAlgebra 𝕜 𝕜
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `lowerSemicontinuous_iff_frequently`. -/
LowerSemicontinuous.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β},
  (∀ (x : α) (y : β), (∃ᶠ (x' : α) in nhds x, f x' ≤ y) → f x ≤ y) → LowerSemicontinuous f
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.of_tendsto_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {a : Filter α} {b : Filter β} {c : Filter γ},
  Filter.Tendsto (g ∘ f) a c → Filter.comap g c ≤ b → Filter.Tendsto f a b
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.coe_trans : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Mul α] [inst_4 : Mul β] [inst_5 : Mul γ] (f : α ≃*o β) (g : β ≃*o γ), ⇑(f.trans g) = ⇑g ∘ ⇑f
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.congr : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : Filter α},
  f₁ =O[𝕜; l] g₁ → (∀ (x : α), f₁ x = f₂ x) → (∀ (x : α), g₁ x = g₂ x) → f₂ =O[𝕜; l] g₂
-- Mathlib.NumberTheory.Pell
/-- If `d` is positive and not a square, then a fundamental solution exists.  -/
Pell.IsFundamental.exists_of_not_isSquare : ∀ {d : ℤ}, 0 < d → ¬IsSquare d → ∃ a, Pell.IsFundamental a
-- Lean.Server.CodeActions.Basic
Lean.Server.instToJsonCodeActionResolveData : Lean.ToJson Lean.Server.CodeActionResolveData
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.ext : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β}, (∀ (x : α), f x = g x) → f = g
-- Mathlib.Order.Filter.Basic
Filter.join_le : ∀ {α : Type u} {f : Filter (Filter α)} {l : Filter α}, (∀ᶠ (m : Filter α) in f, m ≤ l) → f.join ≤ l
-- Mathlib.Data.Set.Function
Function.Semiconj.mapsTo_image : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β} {s t : Set α},
  Function.Semiconj f fa fb → Set.MapsTo fa s t → Set.MapsTo fb (f '' s) (f '' t)
-- Mathlib.Combinatorics.Graph.Basic
Graph.banana_isLink : ∀ {α : Type u_1} {β : Type u_2} (u v : α) (edgeSet : Set β) (e : β) (x y : α),
  (Graph.banana u v edgeSet).IsLink e x y = (e ∈ edgeSet ∧ (x = u ∧ y = v ∨ x = v ∧ y = u))
-- Lean.Meta.KExprMap
/-- Return `some v` if there is an entry `e ↦ v` in `m`.  -/
Lean.Meta.KExprMap.find? : {α : Type} → Lean.Meta.KExprMap α → Lean.Expr → Lean.MetaM (Option α)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.canonicalEquiv_flip : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (P' : Type u_3) [inst_3 : CommRing P'] [inst_4 : Algebra R P'] [inst_5 : IsLocalization S P]
  [inst_6 : IsLocalization S P'] (I : FractionalIdeal S P'),
  (FractionalIdeal.canonicalEquiv S P P') ((FractionalIdeal.canonicalEquiv S P' P) I) = I
-- Mathlib.Order.Bounds.Basic
IsGreatest.orderTop.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α} (h : IsGreatest s a),
  h.orderTop = { top := ⟨a, ⋯⟩, le_top := ⋯ }
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ιMulti_zero_apply : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (v : Fin 0 → M),
  (ExteriorAlgebra.ιMulti R 0) v = 1
-- Aesop.Tree.Data
Aesop.Goal.failedRapps : Aesop.Goal → Array Aesop.RegularRule
-- Mathlib.Data.Finsupp.Fin
Finsupp.tail_update_zero : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M] (y : M) (t : Fin (n + 1) →₀ M), (t.update 0 y).tail = t.tail
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.Measure.integrableOn_of_bounded : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {s : Set α}
  {μ : MeasureTheory.Measure α} {f : α → E},
  μ s ≠ ⊤ →
    MeasureTheory.AEStronglyMeasurable f μ →
      ∀ {M : ℝ}, (∀ᵐ (a : α) ∂μ.restrict s, ‖f a‖ ≤ M) → MeasureTheory.IntegrableOn f s μ
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.isTopologicalBasis_isOpen_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsLocallyFiniteMeasure μ], TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ μ s < ⊤}
-- Mathlib.Data.Matrix.Mul
Matrix.zero_mul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m]
  (M : Matrix m n α), 0 * M = 0
-- Mathlib.Data.Multiset.Filter
Multiset.Nodup.mem_erase_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {l : Multiset α}, l.Nodup → (a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.nonempty_of_sum_ne_zero : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} {f : ι → M} [inst : AddCommMonoid M], ∑ x ∈ s, f x ≠ 0 → s.Nonempty
-- Mathlib.Algebra.Module.NatInt
DistribSMul.toAddMonoidHom_eq_nsmulAddMonoidHom : ∀ {M : Type u_3} [inst : AddCommMonoid M], DistribSMul.toAddMonoidHom M = nsmulAddMonoidHom
-- Init.Data.BitVec.Lemmas
BitVec.le_total : ∀ {n : ℕ} (x y : BitVec n), x ≤ y ∨ y ≤ x
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.measure_eq_zero_of_trim_eq_zero : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0),
  (μ.trim hm) s = 0 → μ s = 0
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `f` is meromorphic at `x`, then `f - g` is meromorphic at `x` if and only if `g` is meromorphic
at `x`.
 -/
MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₁ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E},
  MeromorphicAt f x → (MeromorphicAt (fun z => f z - g z) x ↔ MeromorphicAt g x)
-- Mathlib.Tactic.Algebra.Basic
/-- The data used by the `algebra` tactic to normalize the constant coefficients, which are
expressions in `R` normalized by `ring`.  -/
Mathlib.Tactic.Algebra.ringCompare : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          (sAlg : Q(Algebra «$R» «$A»)) → Mathlib.Tactic.Ring.Common.RingCompare (Mathlib.Tactic.Algebra.BaseType sAlg)
-- Lean.Parser.Command
Lean.Parser.Command.showDeprecatedModules.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.oneEquiv_symm_apply : ∀ (R : Type u) [inst : CommRing R] (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (a : M),
  (exteriorPower.oneEquiv R M).symm a = (exteriorPower.ιMulti R 1) fun x => a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.pi_nonneg : 0 ≤ Real.pi
-- Mathlib.Computability.Primrec.Basic
Primrec.dom_bool₂ : ∀ {α : Type u_1} [inst : Primcodable α] (f : Bool → Bool → α), Primrec₂ f
-- Init.Data.List.Lemmas
List.IsSuffix.eq_1 : ∀ {α : Type u} (l₁ l₂ : List α), (l₁ <:+ l₂) = ∃ t, t ++ l₁ = l₂
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G)
  {a b : F.CoGrothendieck} (f : a ⟶ b),
  ((CategoryTheory.Pseudofunctor.CoGrothendieck.map α).map f).fiber =
    CategoryTheory.CategoryStruct.comp ((α.app { as := Opposite.op a.base }).toFunctor.map f.fiber)
      ((α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAdd : ∀ {M : Type u_1} [inst : AddZeroClass M],
  CanLift (Set M) (AddSubmonoid M) SetLike.coe fun s => 0 ∈ s ∧ ∀ {x y : M}, x ∈ s → y ∈ s → x + y ∈ s
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isRat_lt_true : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α} {na nb : ℤ} {da db : ℕ},
  Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → decide (na * ↑db < nb * ↑da) = true → a < b
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.InlayHintState.oldFinishedSnaps : Lean.Server.FileWorker.InlayHintState → ℕ
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.coe_pointwise_smul : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] (m : M)
  (S : Subring R), ↑(m • S) = m • ↑S
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∉ t₁ → (t₁ ∪ t₂).getD k fallback = t₂.getD k fallback
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.of_forall_getKey_eq_of_forall_constGet?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  (∀ (k : α) (hk : k ∈ t₁) (hk' : k ∈ t₂), t₁.getKey k hk = t₂.getKey k hk') →
    (∀ (k : α), Std.DTreeMap.Const.get? t₁ k = Std.DTreeMap.Const.get? t₂ k) → t₁.Equiv t₂
-- Init.Data.List.Basic
List.filterTR.loop.eq_1 : ∀ {α : Type u} (p : α → Bool) (a : List α), List.filterTR.loop p [] a = a.reverse