mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformLeft_inv : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommGroup α] (e : α) (x : Finset α × Finset α),
  Finset.mulETransformLeft e⁻¹ x = (Finset.mulETransformRight e x.swap).swap
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.toPoly'.go.eq_5 : ∀ (coeff k : ℤ) (a : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Expr.toPoly'.go coeff (Int.Internal.Linear.Expr.mulL k a) =
    bif k == 0 then id else Int.Internal.Linear.Expr.toPoly'.go (coeff.mul k) a
-- Mathlib.Order.Fin.Basic
Fin.predAbove_le_predAbove : ∀ {n : ℕ} {p q : Fin n}, p ≤ q → ∀ {i j : Fin (n + 1)}, i ≤ j → p.predAbove i ≤ q.predAbove j
-- Mathlib.NumberTheory.Divisors
Int.divisorsAntidiag.eq_2 : ∀ (n : ℕ),
  (Int.negSucc n).divisorsAntidiag =
    (Finset.map (Nat.castEmbedding.prodMap (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))))
          (n + 1).divisorsAntidiagonal).disjUnion
      (Finset.map ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap Nat.castEmbedding)
        (n + 1).divisorsAntidiagonal)
      ⋯
-- Mathlib.Analysis.Normed.Order.Lattice
isClosed_le_of_isClosed_nonneg : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] [inst_3 : TopologicalSpace G]
  [ContinuousSub G], IsClosed {x | 0 ≤ x} → IsClosed {p | p.1 ≤ p.2}
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.edist_toLp_zero : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : α → E) (hf : MeasureTheory.MemLp f p μ),
  edist (MeasureTheory.MemLp.toLp f hf) 0 = MeasureTheory.eLpNorm f p μ
-- Mathlib.CategoryTheory.Widesubcategory
/-- The category of which this is a wide subcategory  -/
CategoryTheory.WideSubcategory.obj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {_P : CategoryTheory.MorphismProperty C} → [inst_1 : _P.IsMultiplicative] → CategoryTheory.WideSubcategory _P → C
-- Lean.Data.Lsp.Basic
Lean.Lsp.ResolveSupport : Type
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is `C^1` on `[a, b]`,
then `∫ y in a..b, derivWithin f (Icc a b) y` equals `f b - f a`.  -/
intervalIntegral.integral_derivWithin_Icc_of_contDiffOn_Icc : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E],
  ContDiffOn ℝ 1 f (Set.Icc a b) → a ≤ b → ∫ (x : ℝ) in a..b, derivWithin f (Set.Icc a b) x = f b - f a
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.trans_apply : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (equiv : S.Equiv S')
  {E'' : Type u_5} [inst_4 : Group E''] {S'' : GroupExtension N E'' G} (equiv' : S'.Equiv S'') (a : E),
  (equiv.trans equiv') a = equiv' (equiv a)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.ToLinear.State.vars : Lean.Meta.Simp.Arith.Nat.ToLinear.State → Array Lean.Expr
-- Mathlib.Data.Part
Part.elim_toOption : ∀ {α : Type u_4} {β : Type u_5} (a : Part α) [inst : Decidable a.Dom] (b : β) (f : α → β),
  a.toOption.elim b f = if h : a.Dom then f (a.get h) else b
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets_univ_mem : ∀ {R : Type u_1} {E : Type u_6} {ι : Type u_9} [inst : SeminormedRing R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p : SeminormFamily R E ι), Set.univ ∈ p.basisSets
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.nnnorm_single : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (i : ι) (a : 𝕜),
  ‖EuclideanSpace.single i a‖₊ = ‖a‖₊
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertMany_eq_foldl_impl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {t₁ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.Balanced)
  {t₂ : Std.DTreeMap.Internal.Impl α β},
  ↑(t₁.insertMany t₂ h₁) =
    Std.DTreeMap.Internal.Impl.foldl (fun acc k v => Std.DTreeMap.Internal.Impl.insert! k v acc) t₁ t₂
-- Mathlib.Order.UpperLower.Prod
LowerSet.instSProd : {α : Type u_1} →
  {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → SProd (LowerSet α) (LowerSet β) (LowerSet (α × β))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k fallback : α} {f : Option β → Option β},
  (m.alter k f).getKeyD k fallback = if (f m[k]?).isSome = true then k else fallback
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hom_id : ∀ {M : SemiNormedGrp}, SemiNormedGrp.Hom.hom (CategoryTheory.CategoryStruct.id M) = NormedAddGroupHom.id M.carrier
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsAddLeftInvariant.comap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G] {H : Type u_3} [inst_3 : AddGroup H]
  {mH : MeasurableSpace H} [MeasurableAdd H] (μ : MeasureTheory.Measure H) [μ.IsAddLeftInvariant] {f : G →+ H},
  MeasurableEmbedding ⇑f → (MeasureTheory.Measure.comap (⇑f) μ).IsAddLeftInvariant
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- Coercion of SL `n` `ℤ` to SL `n` `R` for a commutative ring `R`.  -/
Matrix.SpecialLinearGroup.instCoeInt : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} → [inst_2 : CommRing R] → Coe (Matrix.SpecialLinearGroup n ℤ) (Matrix.SpecialLinearGroup n R)
-- Init.Data.List.Lemmas
List.getLast?_replicate : ∀ {α : Type u_1} {a : α} {n : ℕ}, (List.replicate n a).getLast? = if n = 0 then none else some a
-- Mathlib.Algebra.Ring.Parity
neg_one_pow_eq_neg_one_iff_odd : ∀ {R : Type u_4} [inst : Monoid R] [inst_1 : HasDistribNeg R] {n : ℕ}, -1 ≠ 1 → ((-1) ^ n = -1 ↔ Odd n)
-- Mathlib.Combinatorics.Schnirelmann
_private.Mathlib.Combinatorics.Schnirelmann.0.add_eq_univ_of_one_le_schirelmannDensity_add_schnirelmannDensity.match_1_1.splitter : (motive : ℕ ⊕ ℕ → Sort u_1) → (x : ℕ ⊕ ℕ) → ((x : ℕ) → motive (Sum.inl x)) → ((y : ℕ) → motive (Sum.inr y)) → motive x
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
_private.Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic.0.ProfiniteAddGrp.Hom.mk.inj : ∀ {A B : ProfiniteAddGrp.{u}} {hom' hom'_1 : ↑A.toProfinite.toTop →ₜ+ ↑B.toProfinite.toTop},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The derivative of Weierstrass `℘` function.
This has the notation `℘'[L]` in the namespace `PeriodPairs`.  -/
PeriodPair.derivWeierstrassP : PeriodPair → ℂ → ℂ
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppRight_symm_apply_single : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  [inst_7 : AddCommMonoid N] [inst_8 : Module R N] {ι : Type u_5} [inst_9 : DecidableEq ι] (i : ι) (m : M) (n : N),
  ((TensorProduct.finsuppRight R S M N ι).symm fun₀ | i => m ⊗ₜ[R] n) = m ⊗ₜ[R] fun₀ | i => n
-- Init.Prelude
/-- Use the indexing notation `a[i]!` instead.

Access an element from an array, or panic if the index is out of bounds.
 -/
Array.get!Internal : {α : Type u} → [Inhabited α] → Array α → ℕ → α
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.elab : Lean.Syntax → Aesop.ElabM Aesop.Frontend.RuleExpr
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- `lcm a b` is a (non-unique) element such that `a ∣ lcm a b` `b ∣ lcm a b`, and for
any element `c` such that `a ∣ c` and `b ∣ c`, then `lcm a b ∣ c`  -/
EuclideanDomain.lcm : {R : Type u} → [EuclideanDomain R] → [DecidableEq R] → R → R → R
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.starRing : (K : Type u_1) →
  [inst : Field K] → [inst_1 : CharZero K] → [NumberField.IsCMField K] → [Algebra.IsIntegral ℚ K] → StarRing K
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.inv_hom_h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  {i j : F.I₀} (k : F.I₁ i j),
  CategoryTheory.CategoryStruct.comp (e.inv.h₁ k) (e.hom.h₁ (e.inv.s₁ k)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ k).inv
      (CategoryTheory.eqToHom ⋯)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.iteratedDerivWithin_cos_Ioo : ∀ (n : ℕ) {a b x : ℝ}, x ∈ Set.Ioo a b → iteratedDerivWithin n Real.cos (Set.Ioo a b) x = iteratedDeriv n Real.cos x
-- Mathlib.NumberTheory.Modular
/-- Second Fundamental Domain Lemma: if both `z` and `g • z` are in the open domain `𝒟ᵒ`,
where `z : ℍ` and `g : SL(2, ℤ)`, then `z = g • z`.  -/
ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fdo → g • z ∈ ModularGroup.fdo → z = g • z
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.mk.inj : ∀ {M : Type u_9} {N : Type u_10} {inst : Mul M} {inst_1 : Mul N} {toEquiv : M ≃ N}
  {map_mul' : ∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y} {toEquiv_1 : M ≃ N}
  {map_mul'_1 : ∀ (x y : M), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y},
  { toEquiv := toEquiv, map_mul' := map_mul' } = { toEquiv := toEquiv_1, map_mul' := map_mul'_1 } → toEquiv = toEquiv_1
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.FunInfoEnvCacheKey.c : Lean.Meta.FunInfoEnvCacheKey✝ → Lean.Name
-- Lean.Meta.Instances
_private.Lean.Meta.Instances.0.Lean.Meta.warnClassDefReducibility : Lean.Option Bool
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneUnopOfCocone_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.coneUnopOfCocone c).pt = Opposite.unop c.pt
-- Mathlib.Analysis.InnerProductSpace.Projection.Minimal
_private.Mathlib.Analysis.InnerProductSpace.Projection.Minimal.0.termAbsR : Lean.ParserDescr
-- Mathlib.CategoryTheory.Galois.Examples
/-- A nonempty finite `G`-set is connected if and only if the `G`-action is transitive.  -/
CategoryTheory.FintypeCat.Action.isConnected_iff_transitive : ∀ (G : Type u) [inst : Group G] (X : Action FintypeCat G) [Nonempty X.V.obj],
  CategoryTheory.PreGaloisCategory.IsConnected X ↔ MulAction.IsPretransitive G X.V.obj
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.image_source_eq_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  ↑e '' e.source = e.target
-- Mathlib.Data.Set.Finite.Lemmas
Set.exists_min_image : ∀ {α : Type u} {β : Type v} [inst : LinearOrder β] (s : Set α) (f : α → β),
  s.Finite → s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- The First-Derivative Test from calculus, maxima version,
expressed in terms of left and right filters.  -/
isLocalMax_of_deriv' : ∀ {f : ℝ → ℝ} {b : ℝ},
  ContinuousAt f b →
    (∀ᶠ (x : ℝ) in nhdsWithin b (Set.Iio b), DifferentiableAt ℝ f x) →
      (∀ᶠ (x : ℝ) in nhdsWithin b (Set.Ioi b), DifferentiableAt ℝ f x) →
        (∀ᶠ (x : ℝ) in nhdsWithin b (Set.Iio b), 0 ≤ deriv f x) →
          (∀ᶠ (x : ℝ) in nhdsWithin b (Set.Ioi b), deriv f x ≤ 0) → IsLocalMax f b
-- Mathlib.Analysis.InnerProductSpace.Subspace
/-- An orthogonal family forms an independent family of subspaces; that is, any collection of
elements each from a different subspace in the family is linearly independent. In particular, the
pairwise intersections of elements of the family are 0.  -/
OrthogonalFamily.independent : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {V : ι → Submodule 𝕜 E}, (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → iSupIndep V
-- Mathlib.Algebra.Group.Prod
MulHom.prod_comp_prodMap : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} [inst : Mul M] [inst_1 : Mul N]
  [inst_2 : Mul M'] [inst_3 : Mul N'] [inst_4 : Mul P] (f : P →ₙ* M) (g : P →ₙ* N) (f' : M →ₙ* M') (g' : N →ₙ* N'),
  (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_prod : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  {s : NonUnitalSubsemiring R} {t : NonUnitalSubsemiring S} {p : R × S}, p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
-- Init.Data.BitVec.Bitblast
BitVec.not_sub_one_eq_not_add_one : ∀ {w : ℕ} {x : BitVec w}, ~~~(x - 1#w) = ~~~x + 1#w
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.coe_toHomeomorph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n),
  ⇑h.toHomeomorph = ⇑h
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.H : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Hour.Ordinal
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_mono_ae : ∀ {α : Type u_1} {F : Type u_5} {G : Type u_6} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
  0 ≤ q → (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖) → MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNorm' g q μ
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.uniqueAlgEquiv_apply : ∀ (R : Type u) [inst : CommSemiring R] (σ : Type u_2) [inst_1 : Unique σ] (p : MvPolynomial σ R),
  (MvPolynomial.uniqueAlgEquiv R σ) p = MvPolynomial.eval₂ Polynomial.C (fun x => Polynomial.X) p
-- Mathlib.LinearAlgebra.Orientation
Module.Basis.adjustToOrientation.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  [inst_7 : Nonempty ι] (e e_1 : Module.Basis ι R M),
  e = e_1 → ∀ (x x_1 : Orientation R M ι), x = x_1 → e.adjustToOrientation x = e_1.adjustToOrientation x_1
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ → ∀ (t : Set α), (∀ (g : G), g • t = t) → μ (t ∩ s) = 0 → μ t = 0
-- Mathlib.Analysis.Calculus.Deriv.Add
differentiable_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜], Differentiable 𝕜 Neg.neg
-- Mathlib.RingTheory.SimpleModule.Isotypic
isFullyInvariant_iff_sSup_isotypicComponents : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  {m : Submodule R M}, m.IsFullyInvariant ↔ ∃ s ⊆ isotypicComponents R M, m = sSup s
-- Mathlib.Geometry.Convex.Cone.Simplicial
/-- The conic hull of a finite linearly independent set is simplicial.  -/
PointedCone.IsSimplicial.hull : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {s : Set M},
  s.Finite → LinearIndepOn R id s → (PointedCone.hull R s).IsSimplicial
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
_private.Mathlib.Geometry.Manifold.VectorBundle.Tangent.0.termTM : Lean.ParserDescr
-- Mathlib.Algebra.Group.Units.Defs
/-- The underlying value in the base `Monoid`.  -/
Units.val : {α : Type u} → [inst : Monoid α] → αˣ → α
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.alternatingSum_nil : ∀ {G : Type u_7} [inst : Zero G] [inst_1 : Add G] [inst_2 : Neg G], [].alternatingSum = 0
-- Lean.Meta.Tactic.Grind.Types
/-- Returns a proof that `a = b` if they have the same type. Otherwise, returns a proof of `a ≍ b`.
It assumes `a` and `b` are in the same equivalence class.
 -/
Lean.Meta.Grind.mkEqHEqProof : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Pullback symmetry isomorphism.  -/
CategoryTheory.PreZeroHypercover.pullbackIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S T : C} →
      (f : S ⟶ T) →
        (E : CategoryTheory.PreZeroHypercover T) →
          [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] →
            [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] →
              CategoryTheory.PreZeroHypercover.pullback₁ f E ≅ CategoryTheory.PreZeroHypercover.pullback₂ f E
-- Mathlib.Data.Set.Lattice
Set.iUnion_iUnion_eq_right : ∀ {α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → b = x → Set α}, ⋃ x, ⋃ (h : b = x), s x h = s b ⋯
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.get_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β} {a : α}
  {h : a ∈ m}, Std.DHashMap.Raw.Const.get m a h = Std.DHashMap.Internal.Raw₀.Const.get ⟨m, ⋯⟩ a ⋯
-- Mathlib.Algebra.Order.Module.Equiv
/-- `toLex` as a linear equivalence  -/
toLexLinearEquiv : (α : Type u_1) →
  (β : Type u_2) → [inst : Semiring α] → [inst_1 : AddCommMonoid β] → [inst_2 : Module α β] → β ≃ₗ[α] Lex β
-- Mathlib.Analysis.Normed.Module.FiniteDimension
continuous_clm_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  {X : Type u_1} [inst_6 : TopologicalSpace X] [FiniteDimensional 𝕜 E] {f : X → E →L[𝕜] F},
  Continuous f ↔ ∀ (y : E), Continuous fun x => (f x) y
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_eq_one : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] {x : α}, normalize x = 1 ↔ IsUnit x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_app_assoc : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ) {Z : Type u}
  (h : (f.filtration j).toSSet.obj x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c.ιSigmaHorn.app x) (CategoryTheory.CategoryStruct.comp ((f.t j).app x) h) =
    CategoryTheory.CategoryStruct.comp ((SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn f c).app x) h
-- Mathlib.Data.Matrix.Mul
/-- This instance enables use with `mul_smul_comm`.  -/
Matrix.Semiring.smulCommClass : ∀ {n : Type u_3} {R : Type u_7} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  [inst_2 : Monoid R] [inst_3 : DistribMulAction R α] [SMulCommClass R α α],
  SMulCommClass R (Matrix n n α) (Matrix n n α)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_insert_le_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  (cmp (t.insert k).min! k).isLE = true
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.norm_mul_mul_star_self_of_nonneg : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A] [CStarRing A]
  [inst_4 : NormedSpace ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {a : A} (b : A),
  autoParam (0 ≤ a) CFC.norm_mul_mul_star_self_of_nonneg._auto_1 → ‖b * a * star b‖ = ‖b * CFC.sqrt a‖ ^ 2
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.toListModel_insertManyIfNewUnit!_list : ∀ {α : Type u} {x : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] {l : List α}
  {t : Std.DTreeMap.Internal.Impl α fun x => Unit},
  t.WF →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).toListModel.Perm
      (Std.Internal.List.insertListIfNewUnit t.toListModel l)
-- Init.Data.BitVec.Bitblast
BitVec.sub_add_comm : ∀ {w : ℕ} {z x y : BitVec w}, x - y + z = x + z - y
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- Adding an edge results in an acyclic graph iff the original graph was acyclic and
the edge connects vertices that previously had no path between them.  -/
SimpleGraph.isAcyclic_sup_fromEdgeSet_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V},
  (G ⊔ SimpleGraph.edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformAddGroup.isLeftUniformAddGroup : ∀ (α : Type u_1) [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α], IsLeftUniformAddGroup α
-- Mathlib.CategoryTheory.Action.Basic
Action.inv_hom_hom_assoc : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (f : M ≅ N) {Z : V} (h : N.V ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.inv.hom (CategoryTheory.CategoryStruct.comp f.hom.hom h) = h
-- Init.Data.Array.Nat
Array.le_sum_div_length_of_min?_eq_some_nat : ∀ {x : ℕ} {xs : Array ℕ}, xs.min? = some x → x ≤ xs.sum / xs.size
-- Mathlib.LinearAlgebra.Eigenspace.Charpoly
/-- The roots of the characteristic polynomial are exactly the eigenvalues.

`R` is required to be an integral domain, otherwise there is the counterexample:
R = M = Z/6Z, f(x) = 2x, v = 3, μ = 4, but p = X - 2.
 -/
Module.End.hasEigenvalue_iff_isRoot_charpoly : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.Free R M] [inst_5 : Module.Finite R M] (f : Module.End R M) (μ : R),
  f.HasEigenvalue μ ↔ (LinearMap.charpoly f).IsRoot μ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The (exact) short complex `(G →₀ A) ⟶ A ⟶ A.ρ.coinvariants`.  -/
groupHomology.shortComplexH0 : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instIsOrderedRing : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommSemiring α] [inst_2 : PartialOrder α] [IsOrderedRing α]
  [inst_4 : CanonicallyOrderedAdd α] [inst_5 : NoZeroDivisors α] [inst_6 : Nontrivial α], IsOrderedRing (WithBot α)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.tensorTensorTensorComm_symm : ∀ {R : Type uR} {R' : Type u_1} {S : Type uS} {T : Type u_2} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD}
  [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A]
  [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B]
  [inst_9 : Semiring C] [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C]
  [inst_13 : Semiring D] [inst_14 : Algebra R D] [inst_15 : CommSemiring T] [inst_16 : Algebra R T]
  [inst_17 : Algebra T A] [inst_18 : IsScalarTower R T A] [inst_19 : SMulCommClass S T A] [inst_20 : Algebra S T]
  [inst_21 : IsScalarTower S T A] [inst_22 : CommSemiring R'] [inst_23 : Algebra R R'] [inst_24 : Algebra R' T]
  [inst_25 : Algebra R' A] [inst_26 : Algebra R' B] [inst_27 : IsScalarTower R R' A] [inst_28 : SMulCommClass S R' A]
  [inst_29 : SMulCommClass R' S A] [inst_30 : IsScalarTower R' T A] [inst_31 : IsScalarTower R R' B],
  (Algebra.TensorProduct.tensorTensorTensorComm R R' S T A B C D).symm =
    Algebra.TensorProduct.tensorTensorTensorComm R S R' T A C B D
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_two : ∀ (x : ℂ), x ^ 2 = x ^ 2