mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.StronglyMeasurable.integral_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F}
  [inst_5 : NormedSpace ℝ F],
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable fun x => ∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x
-- Lean.Expr
Lean.MVarId.mk : Lean.Name → Lean.MVarId
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If the double cover of `G` contains `completeBipartiteGraph α β`, then `G` also
contains `completeBipartiteGraph α β`.  -/
SimpleGraph.completeBipartiteGraph_isContained_bipartiteDoubleCover : ∀ {V : Type u_1} {G : SimpleGraph V} {α : Type u_2} {β : Type u_3} [Finite α] [Finite β] [Nonempty α] [Nonempty β],
  (completeBipartiteGraph α β).IsContained G.bipartiteDoubleCover ↔ (completeBipartiteGraph α β).IsContained G
-- Mathlib.Computability.Partrec
Nat.Partrec.below.zero : ∀ {motive : (a : ℕ →. ℕ) → Nat.Partrec a → Prop}, Nat.Partrec.below Nat.Partrec.zero
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.sqrt_eq_rpow : ∀ (x : ℝ), √x = x ^ (1 / 2)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.sq_eq_trace_smul_sub_norm : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (z : QuadraticAlgebra R a b),
  z ^ 2 = QuadraticAlgebra.trace z • z - (algebraMap R (QuadraticAlgebra R a b)) (QuadraticAlgebra.norm z)
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_prod_of_discrete_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [DiscreteTopology α] {f : α × β → γ} {s : Set (α × β)} {x : α × β},
  ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 => f (x.1, x_1)) {b | (x.1, b) ∈ s} x.2
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A)
  (U :
    (TopologicalSpace.Opens
        ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace)ᵒᵖ),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).inv
      (CategoryTheory.CategoryStruct.comp
        ((AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).presheaf.map
          (CategoryTheory.homOfLE ⋯).op)
        ((AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).c.app U)) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ 𝒜 f)
      (((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).presheaf.map (CategoryTheory.homOfLE ⋯).op)
-- Init.Data.Fin.Lemmas
Fin.last_eq_zero_iff : ∀ {n : ℕ}, Fin.last n = 0 ↔ n = 0
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.Iso.maxDegree_eq : ∀ {V : Type u_1} {G : SimpleGraph V} {W : Type u_2} {G' : SimpleGraph W} [inst : Fintype V]
  [inst_1 : DecidableRel G.Adj] [inst_2 : Fintype W] [inst_3 : DecidableRel G'.Adj] (f : G ≃g G'),
  G.maxDegree = G'.maxDegree
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
/-- This is almost a duplicate of `IsIntegrallyClosedIn.integralClosure_eq_bot`,
except the `Module.IsTorsionFree` hypothesis isn't inferred automatically from `IsFractionRing`.  -/
IsIntegrallyClosed.integralClosure_eq_bot : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_3) [inst_1 : CommRing K] [inst_2 : Algebra R K]
  [ifr : IsFractionRing R K] [IsIntegrallyClosed R], integralClosure R K = ⊥
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftKanExtension_hom_ext : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasLeftKanExtension F]
  {G : CategoryTheory.Functor D H} (γ₁ γ₂ : L.leftKanExtension F ⟶ G),
  CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit F) (L.whiskerLeft γ₁) =
      CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit F) (L.whiskerLeft γ₂) →
    γ₁ = γ₂
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.ofHom_hom : ∀ {M N : AddCommMonCat} (f : M ⟶ N), AddCommMonCat.ofHom (AddCommMonCat.Hom.hom f) = f
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.exists_zigzag' : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsConnected J] (j₁ j₂ : J),
  ∃ l, List.IsChain CategoryTheory.Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.eq_1 : ∀ {ι : Type u'} (R : Type u_2) {M : Type u_4} (v : ι → M) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent R v = Function.Injective ⇑(Finsupp.linearCombination R v)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.cbmApplyMeasure_union : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) {s t : Set X},
  MeasurableSet s →
    MeasurableSet t →
      Disjoint s t →
        MeasureTheory.cbmApplyMeasure μ B (s ∪ t) =
          MeasureTheory.cbmApplyMeasure μ B s + MeasureTheory.cbmApplyMeasure μ B t
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If `G` acts properly on `X`, then for each pair of compacts `U, V ⊆ X`,
the set of `g` such that `g +ᵥ U` intersects `V` is compact.

See `AddAction.properVAdd_iff_isCompact_setOfPred_inter_nonempty` for the two-way implication
under additional conditions on `G` and `X`.  -/
ProperVAdd.isCompact_setOfPred_inter_nonempty : ∀ {X : Type u_2} [inst : TopologicalSpace X] {G : Type u_3} [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [inst_3 : TopologicalSpace G] [ProperVAdd G X] {U V : Set X},
  IsCompact U → IsCompact V → IsCompact {g | ((g +ᵥ U) ∩ V).Nonempty}
-- Mathlib.Order.UpperLower.Relative
/-- A subset that is an upper set is additionally a _relative_ upper set.  -/
IsRelUpperSet.mono_isUpperSet : ∀ {α : Type u_1} {s t : Set α} {P : α → Prop} [inst : LE α],
  IsRelUpperSet t P → IsUpperSet s → s ⊆ t → IsRelUpperSet s P
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- If `f` is a collection of linear maps, then the construction `MultilinearMap.compLinearMap`
sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g` and multilinear in
`f₁, ..., fₙ`.  -/
MultilinearMap.compLinearMapMultilinear : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₁' : ι → Type v₁'} →
        {M₂ : Type v₂} →
          [inst : CommSemiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : (i : ι) → Module R (M₁ i)] →
                  [inst_4 : Module R M₂] →
                    [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] →
                      [inst_6 : (i : ι) → Module R (M₁' i)] →
                        MultilinearMap R (fun i => M₁ i →ₗ[R] M₁' i)
                          (MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_symm_single_one : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (i : ι), (b.repr.symm fun₀ | i => 1) = b i
-- Mathlib.Algebra.Category.Ring.Limits
SemiRingCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget SemiRingCat)
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Aut.toEnd_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) (x : CategoryTheory.Aut X),
  (CategoryTheory.Aut.toEnd X) x = ↑((CategoryTheory.Aut.unitsEndEquivAut X).symm x)
-- Mathlib.Analysis.Analytic.CPolynomial
CPolynomialOn.sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  CPolynomialOn 𝕜 f s → CPolynomialOn 𝕜 g s → CPolynomialOn 𝕜 (f - g) s
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.ofProp_eq_top : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {φ : Prop},
  φ → Lean.Order.CompleteLattice.ofProp φ = Lean.Order.top
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.OplaxTrans F G) (a : B) {Z : F.obj a ⟶ G.obj a}
  (h : CategoryTheory.CategoryStruct.comp (self.app a) (G.map (CategoryTheory.CategoryStruct.id a)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a))
      (CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.app a)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a)) h))
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.prod_eq_of_forall_apply_prod : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G}
  {ρ : MeasureTheory.VectorMeasure (X × Y) G},
  (∀ (s : Set X) (t : Set Y), MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = (B (μ s)) (ν t)) → μ.prod ν B = ρ
-- Mathlib.Algebra.Ring.Parity
odd_iff_exists_bit1 : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Odd a ↔ ∃ b, a = 2 * b + 1
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : C) {y z : D} (f : y ≅ z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f.inv)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f.hom) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x z)
-- Mathlib.Order.Minimal
MinimalFor.of_strictMonoOn_comp : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {Q : ι → Prop} {f : ι → α}
  {g : α → β} {i : ι}, StrictMonoOn g (f '' Set.ofPred Q) → MinimalFor Q (g ∘ f) i → MinimalFor Q f i
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.le_mul_inv_of_mul_le : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, 0 < b → a * b ≤ c → a ≤ c * b⁻¹
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
GromovHausdorff.HD_below_aux2 : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {f : GromovHausdorff.Cb✝ X Y} (C : ℝ)
  {y : Y}, BddBelow (Set.range fun x => f (Sum.inl x, Sum.inr y) + C)
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearMap.codRestrict.eq_1 : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) (h : ∀ (c : M), f c ∈ p),
  LinearMap.codRestrict p f h = { toFun := fun c => ⟨f c, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
-- Init.MetaTypes
/-- When `true` (default : `true`), then `simp` removes unused `let` and `have` expressions:
`let x := v; e` simplifies to `e` when `x` does not occur in `e`.
This option takes precedence over `zeta` and `zetaHave`.
 -/
Lean.Meta.Simp.Config.zetaUnused : Lean.Meta.Simp.Config → Bool
-- Init.Data.Repr
/-- Converts a natural number to a string that contains the its decimal representation as Unicode
subscript digit characters.

Examples:
 * `Nat.toSubscriptString 0 = "₀"`
 * `Nat.toSubscriptString 35 = "₃₅"`
 -/
Nat.toSubscriptString : ℕ → String
-- Mathlib.Data.List.Cycle
Cycle.Subsingleton.congr : ∀ {α : Type u_1} {s : Cycle α}, s.Subsingleton → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ΨSq.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ),
  W.ΨSq n = W.preΨ n ^ 2 * if Even n then W.Ψ₂Sq else 1
-- Mathlib.Tactic.ITauto
/-- `(p₁: A ∨ B) (p₂: (x: A) ⊢ C) (p₃: (x: B) ⊢ C) ⊢ C`  -/
Mathlib.Tactic.ITauto.Proof.orElim' : Mathlib.Tactic.ITauto.Proof →
  Lean.Name → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.δ.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁),
  X.δ f g n₀ n₁ hn₁ = X.δ f g n₀ n₁ hn₁
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences_monotone_and_antitone : ∀ {x y : NNReal}, (Monotone fun n => (x.agmSequences y n).1) ∧ Antitone fun n => (x.agmSequences y n).2
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- The orthogonal group of `F` is generated by reflections.  -/
LinearIsometryEquiv.reflections_generate : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [FiniteDimensional ℝ F],
  Subgroup.closure (Set.range fun v => (ℝ ∙ v)ᗮ.reflection) = ⊤
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
/-- The bijection `(freeObj F ⟶ G) ≃ (F ⟶ G.presheaf ⋙ forget _)` when
`F` is a presheaf of types and `G` a presheaf of modules.  -/
PresheafOfModules.freeHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {F : CategoryTheory.Functor Cᵒᵖ (Type u)} →
        {G : PresheafOfModules R} → (PresheafOfModules.freeObj F ⟶ G) ≃ (F ⟶ G.presheaf.comp (CategoryTheory.forget Ab))
-- Init.Data.String.Lemmas.Splits
String.Slice.splits_singleton_iff : ∀ {s : String.Slice} {p : s.Pos} {c : Char} {t : String},
  p.Splits (String.singleton c) t ↔
    ∃ (h : s.startPos ≠ s.endPos), p = s.startPos.next h ∧ s.startPos.get h = c ∧ s.copy = String.singleton c ++ t
-- Mathlib.Algebra.Algebra.Operations
Submodule.span_mul_span : ∀ (R : Type u) [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (S T : Set A),
  Submodule.span R S * Submodule.span R T = Submodule.span R (S * T)
-- Mathlib.Topology.Semicontinuity.Defs
/-- A real function `f` is upper semicontinuous on a set `s` if, for any `ε > 0`, for any `x ∈ s`,
for all `x'` close enough to `x` in `s`, then `f x'` is at most `f x + ε`. We formulate this in a
general preordered space, using an arbitrary `y > f x` instead of `f x + ε`.  -/
UpperSemicontinuousOn : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [Preorder β] → (α → β) → Set α → Prop
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.State.mk.injEq : ∀ (exp : ℕ) (rings : Array Lean.Meta.Sym.Arith.CommRing) (semirings : Array Lean.Meta.Sym.Arith.CommSemiring)
  (ncRings : Array Lean.Meta.Sym.Arith.Ring) (ncSemirings : Array Lean.Meta.Sym.Arith.Semiring)
  (typeClassify : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.Arith.ClassifyResult) (exp_1 : ℕ)
  (rings_1 : Array Lean.Meta.Sym.Arith.CommRing) (semirings_1 : Array Lean.Meta.Sym.Arith.CommSemiring)
  (ncRings_1 : Array Lean.Meta.Sym.Arith.Ring) (ncSemirings_1 : Array Lean.Meta.Sym.Arith.Semiring)
  (typeClassify_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.Arith.ClassifyResult),
  ({ exp := exp, rings := rings, semirings := semirings, ncRings := ncRings, ncSemirings := ncSemirings,
        typeClassify := typeClassify } =
      { exp := exp_1, rings := rings_1, semirings := semirings_1, ncRings := ncRings_1, ncSemirings := ncSemirings_1,
        typeClassify := typeClassify_1 }) =
    (exp = exp_1 ∧
      rings = rings_1 ∧
        semirings = semirings_1 ∧ ncRings = ncRings_1 ∧ ncSemirings = ncSemirings_1 ∧ typeClassify = typeClassify_1)
-- Lean.Meta.Tactic.Grind.Injective
Lean.Meta.Grind.mkInjectiveTheorem : Lean.Name → Lean.MetaM Lean.Meta.Grind.InjectiveTheorem
-- Init.Data.Slice.List.Lemmas
instSliceableListSliceNat_1.eq_1 : ∀ {α : Type u},
  instSliceableListSliceNat_1 =
    {
      mkSlice := fun xs range =>
        have stop :=
          match xs.internalRepresentation.stop with
          | none => range.upper
          | some stop => min stop range.upper;
        Std.Rco.Sliceable.mkSlice xs.internalRepresentation.list range.lower...stop }
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castAdd_Iic : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.castAdd m '' Set.Iic i = Set.Iic (Fin.castAdd m i)
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_mul_relfinrank : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B C : IntermediateField F E},
  A ≤ B → B ≤ C → A.relfinrank B * B.relfinrank C = A.relfinrank C
-- Mathlib.Algebra.CharP.Lemmas
sub_pow_char_pow : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) (n : ℕ) {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p],
  (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α} {b : β a}, (t.insert a b).getKey! a = a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_modify : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k k' : α} [hi : Inhabited (β k')] {f : β k → β k},
      (m.modify k f).get! k' =
        if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).get! else m.get! k'
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.prodComm_apply : ∀ (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (a : P₁ × P₂), (ContinuousAffineEquiv.prodComm k P₁ P₂) a = a.swap
-- Init.Data.Nat.Lcm
Nat.instAssociativeLcm : Std.Associative Nat.lcm
-- Init.Data.Nat.ToString
Nat.repr_eq_ofList_toDigits : ∀ {n : ℕ}, n.repr = String.ofList (Nat.toDigits 10 n)
-- Mathlib.Algebra.Homology.AlternatingConst
/-- The `n`-th homology of the alternating constant complex is `X` for `n ≠ 0`.  -/
ChainComplex.alternatingConst_exactAt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasZeroObject C] (X : C) (n : ℕ),
  n ≠ 0 → HomologicalComplex.ExactAt (ChainComplex.alternatingConst.obj X) n
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_apply : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {s : Set α},
  MeasurableSet s → (μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.getElem?_zipWith.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (x : Option α) (x_1 : Option β)
  (h_1 : (a : α) → (b : β) → motive (some a) (some b)) (h_2 : (x : Option α) → (x_2 : Option β) → motive x x_2),
  (∀ (a : α) (b : β), x = some a → x_1 = some b → False) →
    (match x, x_1 with
      | some a, some b => h_1 a b
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t' : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) (i j k : ι),
  (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).t' i j k =
    ⋯.lift₃ (f k) (f i) (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ ⋯ (f j) (f k))
      (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ ⋯ (f j) (f k))
      (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯
-- Init.Data.Array.MinMax
Array.min?_singleton : ∀ {α : Type u_1} [inst : Min α] {x : α}, #[x].min? = some x
-- Init.Data.List.Attach
List.findSome?_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Option β} {g : α → Option β},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → List.findSome? f l = List.findSome? g l.unattach
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instOne : {R : Type u_1} → {A : Type u_2} → [One R] → [Zero A] → One (Unitization R A)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_star : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : StarModule R A] (S : NonUnitalSubalgebra R A),
  ↑(star S) = star ↑S
-- Mathlib.Algebra.Order.AddGroupWithTop
WithTop.LinearOrderedAddCommGroup.sub_top : ∀ {G : Type u_1} [inst : AddCommGroup G] (x : WithTop G), x - ⊤ = ⊤
-- Aesop.Script.Util
_private.Aesop.Script.Util.0.Aesop.Script.matchGoals.getProperGoals : Lean.Meta.SavedState → Array Lean.MVarId → Lean.MetaM (Array Lean.MVarId)
-- Lean.Elab.Quotation
/-- actually run the specified head check, with the discriminant bound to `__discr`  -/
Lean.Elab.Term.Quotation.HeadInfo.doMatch : Lean.Elab.Term.Quotation.HeadInfo →
  (List Lean.Term → Lean.Elab.TermElabM Lean.Term) → Lean.Elab.TermElabM Lean.Term → Lean.Elab.TermElabM Lean.Term
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.instIsSplitMonoBiproductComparison' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms],
  CategoryTheory.IsSplitMono (F.biproductComparison' f)
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_one : ∀ (α : Type u_1) [inst : AddMonoidWithOne α], Mathlib.Meta.NormNum.IsNat One.one 1
-- Mathlib.Algebra.Group.Equiv.Defs
/-- **Alias** of `EmbeddingLike.map_eq_zero_iff`. -/
AddEquivClass.map_eq_zero_iff : ∀ {F : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M}, f x = 0 ↔ x = 0