mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_inter_eq_size_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (∀ (a : α), m₂.contains a = true → m₁.contains a = true) → (↑(m₁.inter m₂)).size = (↑m₂).size
-- Mathlib.NumberTheory.NumberField.DirichletDensity
NumberField.Set.primeIdealZetaSum_nonneg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (s : ℝ),
  0 ≤ NumberField.Set.primeIdealZetaSum S s
-- Mathlib.Algebra.Ring.Defs
Semiring.toNonAssocSemiring : {α : Type u} → [self : Semiring α] → NonAssocSemiring α
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `IsClosed.hausdorffEDist_zero_iff`.

---

Two closed sets are at zero Hausdorff edistance if and only if they coincide.  -/
EMetric.hausdorffEdist_zero_iff_eq_of_closed : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  IsClosed s → IsClosed t → (Metric.hausdorffEDist s t = 0 ↔ s = t)
-- Mathlib.Algebra.Group.Hom.Instances
/-- Flipping arguments of additive monoid morphisms (`AddMonoidHom.flip`)
as an additive monoid morphism.  -/
AddMonoidHom.flipHom : {M : Type uM} →
  {N : Type uN} →
    {P : Type uP} →
      {x : AddZeroClass M} → {x_1 : AddZeroClass N} → {x_2 : AddCommMonoid P} → (M →+ N →+ P) →+ N →+ M →+ P
-- Mathlib.Algebra.Category.FGModuleCat.Basic
LinearEquiv.toFGModuleCatIso_hom : ∀ {R : Type u} [inst : Ring R] {V W : Type v} [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Finite R V] [inst_4 : AddCommGroup W] [inst_5 : Module R W] [inst_6 : Module.Finite R W]
  (e : V ≃ₗ[R] W), e.toFGModuleCatIso.hom = CategoryTheory.ConcreteCategory.ofHom ↑e
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.injective : ∀ {α : Sort u_1} {β : Sort u_2} (f : α ↪ β), Function.Injective ⇑f
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.instIsClosedUnderIsomorphismsGe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), (t.ge n).IsClosedUnderIsomorphisms
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.comp_mapAddMon_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal]
  (X : CategoryTheory.AddMon C),
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) X.X X.X)
      ((F.comp G).map CategoryTheory.AddMonObj.add)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.val_preimage_orbit : ∀ {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] {p : SubAddAction R M} (m : ↥p),
  Subtype.val ⁻¹' AddAction.orbit R ↑m = AddAction.orbit R m
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar_extract_congr : ∀ {bytes : ByteArray} (i j j' : ℕ) {h : ((bytes.extract i j).utf8DecodeChar? 0).isSome = true}
  {h' : ((bytes.extract i j').utf8DecodeChar? 0).isSome = true},
  (bytes.extract i j).utf8DecodeChar 0 h = (bytes.extract i j').utf8DecodeChar 0 h'
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instInhabited : {R : Type u_3} → {A : Type u_4} → [Inhabited R] → [Inhabited A] → Inhabited (Unitization R A)
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.mk : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicOnNhd f s → ContinuousOn f (closure s) → InnerProductSpace.HarmonicContOnCl f s
-- Init.Data.Option.Attach
Option.toList_pfilter : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool},
  (o.pfilter p).toList = (List.filter (fun x => p ↑x ⋯) o.toList.attach).unattach
-- Mathlib.RingTheory.Coalgebra.GroupLike
GroupLike.instCoeOut : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [inst_3 : Coalgebra R A] → CoeOut (GroupLike R A) A
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.baseSupp_apply_h' : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [inst_4 : Fintype ι] (i j : ι),
  (b.baseSupp i) (b.h' j) = ↑(b.A i j)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasProd_lt : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommGroup α] [inst_1 : PartialOrder α]
  [IsOrderedMonoid α] [inst_3 : TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α}
  {a₁ a₂ : α} {i : ι} [L.NeBot] [L.LeAtTop], f ≤ g → f i < g i → HasProd f a₁ L → HasProd g a₂ L → a₁ < a₂
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarSpaceCoord_symm_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (a : NumberField.mixedEmbedding.polarSpace K),
  ↑(NumberField.mixedEmbedding.polarSpaceCoord K).symm a =
    (fun w => a.1 ↑w, Pi.map (fun i => ↑Complex.polarCoord.symm) fun w => (a.1 ↑w, a.2 w))
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂ : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).inv.hom₂ =
    CategoryTheory.CategoryStruct.id (Opposite.op (F.obj T.obj₂))
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.isoMk_inv_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g : f.right ≅ f'.right)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom)
      CategoryTheory.StructuredArrow.isoMk._auto_1),
  (CategoryTheory.StructuredArrow.isoMk g w).inv.right = g.inv
-- Mathlib.Topology.UniformSpace.Closeds
IsUniformEmbedding.compacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β}
  (hf : IsUniformEmbedding f), IsUniformEmbedding (TopologicalSpace.Compacts.map f ⋯)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → (Std.DHashMap.Raw.ofList l).get? k' = some (cast ⋯ v)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- One direction of `le_mul_inv_iff₀` where `c` is allowed to be `0` (but `b` must be nonnegative).
 -/
mul_le_of_le_mul_inv₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 ≤ b → 0 ≤ c → a ≤ b * c⁻¹ → a * c ≤ b
-- Init.Data.Nat.Gcd
Nat.gcd_dvd_gcd_mul_right_right : ∀ (m n k : ℕ), m.gcd n ∣ m.gcd (n * k)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_diff_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α], (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → (m₁.diff m₂).get? k = none
-- Mathlib.Combinatorics.Matroid.Closure
/-- For a nonempty collection of subsets of a given independent set,
the closure of the intersection is the intersection of the closure.  -/
Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subset : ∀ {α : Type u_2} {M : Matroid α} {I : Set α} {Js : Set (Set α)},
  M.Indep I → Js.Nonempty → (∀ J ∈ Js, J ⊆ I) → M.closure (⋂₀ Js) = ⋂ J ∈ Js, M.closure J
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.setLIntegral_strict_mono : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} {s : Set α},
  MeasurableSet s →
    μ s ≠ 0 →
      Measurable g →
        ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤ →
          (∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x) → ∫⁻ (x : α) in s, f x ∂μ < ∫⁻ (x : α) in s, g x ∂μ
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.map_unop_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : Mᵃᵒᵖ),
  Filter.map AddOpposite.unop (nhds x) = nhds (AddOpposite.unop x)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.cotangentEquivCotangentKer_symm_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (x : P.ker.Cotangent), Algebra.Extension.cotangentEquivCotangentKer.symm x = Algebra.Extension.Cotangent.of x
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sum_Ioc_zeta : ∀ (N : ℕ), ∑ n ∈ Finset.Ioc 0 N, ArithmeticFunction.zeta n = N
-- Mathlib.Order.RelClasses
/-- A connected order is one satisfying the condition `a < c → a < b ∨ b < c`.  -/
IsOrderConnected.conn : ∀ {α : Type u} {lt : α → α → Prop} [self : IsOrderConnected α lt] (a b c : α), lt a c → lt a b ∨ lt b c
-- Init.Data.Vector.Lemmas
Vector.mem_flatten_of_mem : ∀ {α : Type u_1} {n n_1 : ℕ} {xss : Vector (Vector α n) n_1} {xs : Vector α n} {a : α},
  xs ∈ xss → a ∈ xs → a ∈ xss.flatten
-- Mathlib.Algebra.Order.AddTorsor
/-- An ordered cancellative scalar multiplication is an ordered scalar multiplication that is
cancellative.  -/
IsOrderedCancelSMul : (G : Type u_3) → (P : Type u_4) → [LE G] → [LE P] → [SMul G P] → Prop
-- Mathlib.Order.Category.Frm
Frm.Hom.ext : ∀ {X Y : Frm} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.symm_apply_eq : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) {x : M₂}
  {y : M₁}, f.symm x = y ↔ x = f y
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.LClause.mk.injEq : ∀ (lits : Array ℤ) (expr : Lean.Expr) (depth : ℕ) (lits_1 : Array ℤ) (expr_1 : Lean.Expr) (depth_1 : ℕ),
  ({ lits := lits, expr := expr, depth := depth } = { lits := lits_1, expr := expr_1, depth := depth_1 }) =
    (lits = lits_1 ∧ expr = expr_1 ∧ depth = depth_1)
-- Init.Data.List.Range
List.getElem?_zipIdx : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, (l.zipIdx i)[j]? = Option.map (fun a => (a, i + j)) l[j]?
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instIsMulApplyEqCompId : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], IsMulApplyEqComp (M₁ →L[R₁] M₁) M₁
-- Mathlib.Analysis.Calculus.FDeriv.Const
tsupport_fderiv_apply_subset : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} (v : E), (tsupport fun x => (fderiv 𝕜 f x) v) ⊆ tsupport f
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.EToCycles_i : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.EToCycles_i._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.EToCycles_i._auto_3),
  CategoryTheory.CategoryStruct.comp (X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂) (X.iCycles f₁ f₂₃ n₁) =
    CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁)
-- Mathlib.Order.Hom.Bounded
BotHom.instSemilatticeSup.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : SemilatticeSup β] [inst_2 : OrderBot β],
  BotHom.instSemilatticeSup = Function.Injective.semilatticeSup DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.integrable_map_cast_poissonMeasure_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {R : Type u_2} [inst_1 : NatCast R] [inst_2 : MeasurableSpace R]
  {r : NNReal} [Countable R] [MeasurableSingletonClass R] {f : R → E},
  MeasureTheory.Integrable f (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r)) ↔
    MeasureTheory.Integrable (f ∘ Nat.cast) (ProbabilityTheory.poissonMeasure r)
-- Init.Data.SInt.Basic
/-- Obtains the `ISize` that is 2's complement equivalent to the `USize`.  -/
USize.toISize : USize → ISize
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_eq_of_eq_sub_negPart : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A] [StarOrderedRing A]
  {a b : A}, a = b - a⁻ → autoParam (0 ≤ b) CFC.posPart_eq_of_eq_sub_negPart._auto_1 → a⁺ = b
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Right.self_le_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α] [AddRightMono α] {a : α}, a ≤ 0 → a ≤ -a
-- Init.Prelude
/-- The homogeneous version of `HShiftLeft`: `a <<< b : α` where `a b : α`.  -/
ShiftLeft : Type u → Type u
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.leftHomologyData'_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n m p : ℤ) (hm : n + 1 = m) (hp : m + 1 = p),
  (CochainComplex.HomComplex.leftHomologyData' K L n m p hm hp).i =
    AddCommGrpCat.ofHom (CochainComplex.HomComplex.Cocycle.toCochainAddMonoidHom K L m)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOf.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), H.subgroupOf K = Subgroup.comap K.subtype H
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- The compatibility relations between the functions underlying a polynomial law  -/
PolynomialLaw.isCompat' : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (self : M →ₚₗ[R] N) {S : Type u} [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S] {S' : Type u} [inst_7 : CommSemiring S'] [inst_8 : Algebra R S'] (φ : S →ₐ[R] S'),
  ⇑(LinearMap.rTensor N φ.toLinearMap) ∘ self.toFun' S = self.toFun' S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)
-- Mathlib.Data.W.Constructions
WType.toList.eq_def : ∀ (γ : Type u) (x : WType (WType.Listβ γ)),
  WType.toList γ x =
    match x with
    | WType.mk WType.Listα.nil f => []
    | WType.mk (WType.Listα.cons hd) f => hd :: WType.toList γ (f PUnit.unit)
-- Lean.Elab.DefView
Lean.Elab.instNonemptyBodyProcessedSnapshot : Nonempty Lean.Elab.BodyProcessedSnapshot
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'_three : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS' b c d 3 = c
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_neg : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R}, (-p).support = p.support
-- Mathlib.Tactic.Translate.Core
/-- `shouldTranslate e` tests whether the expression `e` contains a constant
that is not applied to any arguments and that doesn't have a translation itself.
This is used for deciding which subexpressions to translate: we only translate
constants if `shouldTranslate` applied to their relevant argument returns `true`.
This means we will replace expression applied to e.g. `α` or `α × β`, but not when applied to
e.g. `ℕ` or `ℝ × α`.
We ignore all arguments specified by the `ignore` `NameMap`.  -/
Mathlib.Tactic.Translate.shouldTranslate : Lean.Environment →
  Mathlib.Tactic.Translate.TranslateData → Lean.Expr → Mathlib.Tactic.Translate.ReplacementM (Option Lean.Expr)
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.term.injEq : ∀ (term : Lean.Term) (expr : Lean.Expr) (term_1 : Lean.Term) (expr_1 : Lean.Expr),
  (Aesop.ElabRuleTerm.term term expr = Aesop.ElabRuleTerm.term term_1 expr_1) = (term = term_1 ∧ expr = expr_1)
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.of_symm_X_smul : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] (m : Module.AEval R M a),
  (Module.AEval.of R M a).symm (Polynomial.X • m) = a • (Module.AEval.of R M a).symm m
-- Mathlib.Topology.Order
continuous_inf_rng : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β},
  Continuous f ↔ Continuous f ∧ Continuous f
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The `finrank` of `(ι → R)` is `Fintype.card ι`.  -/
Module.finrank_pi : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] {ι : Type v} [inst_2 : Fintype ι],
  Module.finrank R (ι → R) = Fintype.card ι
-- Mathlib.Data.Set.Insert
Set.pair_eq_pair_iff : ∀ {α : Type u_1} {x y z w : α}, {x, y} = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `DFunLike.coe` as an `AlgHom`.  -/
LocallyConstant.coeFnAlgHom : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      (R : Type u_6) →
        [inst_1 : CommSemiring R] → [inst_2 : Semiring Y] → [inst_3 : Algebra R Y] → LocallyConstant X Y →ₐ[R] X → Y
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
/-- **Alias** of the reverse direction of `Multiplicative.ofAdd_lt`. -/
Multiplicative.ofAdd_strictMono : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → Multiplicative.ofAdd a < Multiplicative.ofAdd b
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.sup_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (F G : M.Submodule) (X : Cᵒᵖ), (SemilatticeSup.sup F G).obj X = F.obj X ⊔ G.obj X
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev_ofToSlice : ∀ {s : String} {p : s.toSlice.Pos} {h : String.Pos.ofToSlice p ≠ s.startPos},
  (String.Pos.ofToSlice p).prev h = String.Pos.ofToSlice (p.prev ⋯)
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.addGroupObj : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddGrpCat) → (j : J) → AddGroup ((F.comp (CategoryTheory.forget AddGrpCat)).obj j)
-- Lean.Parser.Term
Lean.Parser.Term.letEqnsDecl : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.yonedaEquiv_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X : C} {F G : CategoryTheory.Sheaf J (Type v)} (α : J.yoneda.obj X ⟶ F) (β : F ⟶ G),
  J.yonedaEquiv (CategoryTheory.CategoryStruct.comp α β) =
    (CategoryTheory.ConcreteCategory.hom (β.hom.app (Opposite.op X))) (J.yonedaEquiv α)
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Represent a `Rewrite` as `MessageData`.  -/
Mathlib.Tactic.LibraryRewrite.Rewrite.toMessageData : Mathlib.Tactic.LibraryRewrite.Rewrite → Lean.Name → Lean.MetaM Lean.MessageData
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.leftRelDecidable : {α : Type u_1} →
  [inst : Group α] → (s : Subgroup α) → [DecidablePred fun x => x ∈ s] → DecidableRel ⇑(QuotientGroup.leftRel s)
-- Aesop.Stats.Basic
Aesop.MonadStats.mk : {m : Type → Type} →
  [toMonadOptions : Lean.MonadOptions m] →
    ({α : Type} → (Aesop.Stats → α × Aesop.Stats) → m α) →
      m Aesop.Stats → ((Aesop.Stats → Aesop.Stats) → m Unit) → Aesop.MonadStats m
-- Mathlib.LinearAlgebra.TensorProduct.Opposite
/-- `MulOpposite` distributes over `TensorProduct`. Note this is an `S`-algebra morphism, where
`A/S/R` is a tower of algebras.  -/
Algebra.TensorProduct.opAlgEquiv : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      (B : Type u_4) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Semiring A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      [inst_7 : Algebra S A] →
                        [inst_8 : IsScalarTower R S A] → TensorProduct R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₐ[S] (TensorProduct R A B)ᵐᵒᵖ
-- Mathlib.Topology.Bases
TopologicalSpace.eq_generateFrom_countableBasis : ∀ (α : Type u) [t : TopologicalSpace α] [inst : SecondCountableTopology α],
  t = TopologicalSpace.generateFrom (TopologicalSpace.countableBasis α)
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {K : CategoryTheory.Precoverage C} {ι : C → Type w} {X : C}
  {R : CategoryTheory.Presieve X} {hR : R ∈ K.coverings X}
  {h : ⦃W : C⦄ → (r : W ⟶ X) → R r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W}
  {R_1 : CategoryTheory.Presieve X} {hR_1 : R_1 ∈ K.coverings X}
  {h_1 : ⦃W : C⦄ → (r : W ⟶ X) → R_1 r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W},
  CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h =
      CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR_1 h_1 →
    R = R_1 ∧ h ≍ h_1
-- Batteries.Lean.Meta.UnusedNames
Lean.Name.MatchUpToIndexSuffix.suffixMatch.inj : ∀ {i i_1 : ℕ}, Lean.Name.MatchUpToIndexSuffix.suffixMatch i = Lean.Name.MatchUpToIndexSuffix.suffixMatch i_1 → i = i_1
-- Init.System.IO
/-- Creates a directory at the specified path, creating all missing parents as directories.
 -/
IO.FS.createDirAll : System.FilePath → IO Unit
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_ne_zero : ∀ {A : Type u_1} {M₀ : Type u_2} [inst : AddGroup A] [inst_1 : MonoidWithZero M₀] [Nontrivial M₀] (ψ : AddChar A M₀),
  ⇑ψ ≠ 0
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.hom_ext_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  {f g : QuaternionAlgebra R c₁ c₂ c₃ →ₐ[R] A},
  f = g ↔
    f (QuaternionAlgebra.Basis.self R).i = g (QuaternionAlgebra.Basis.self R).i ∧
      f (QuaternionAlgebra.Basis.self R).j = g (QuaternionAlgebra.Basis.self R).j
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an additive commutative monoid, if it
admits an injective map that preserves `0` and `+` to an additive commutative monoid.  -/
Function.Injective.addCommMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : AddCommMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 0 = 0 →
                  (∀ (x y : M₁), f (x + y) = f x + f y) → (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) → AddCommMonoid M₁