mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum' : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α]
  [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ {f : α → E} {t : Set α},
      MeasureTheory.IntegrableOn f t μ → ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ
-- Mathlib.Logic.Relation
Relation.TransGen.lift : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {p : β → β → Prop} (f : α → β),
  r ≤ Function.onFun p f → Relation.TransGen r ≤ Function.onFun (Relation.TransGen p) f
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.map_singleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Presieve.map F (CategoryTheory.Presieve.singleton f) = CategoryTheory.Presieve.singleton (F.map f)
-- Init.Data.Int.Order
Int.lt_neg_iff : ∀ {x y : ℤ}, x < -y ↔ y < -x
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
AbsConvexOpenSets.coe_balanced : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : SeminormedRing 𝕜]
  [inst_3 : SMul 𝕜 E] [inst_4 : PartialOrder 𝕜] (s : AbsConvexOpenSets 𝕜 E), Balanced 𝕜 ↑s
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- `MeasurableSet s` means that `s` is measurable (in the ambient measure space on `α`)  -/
MeasurableSet : {α : Type u_1} → [MeasurableSpace α] → Set α → Prop
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
/-- A helper lemma for `MultilinearMap.domCoprod_alternization`.  -/
MultilinearMap.domCoprod_alternization_coe : ∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
  {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
  [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : MultilinearMap R' (fun x => Mᵢ) N₁)
  (b : MultilinearMap R' (fun x => Mᵢ) N₂),
  (↑(MultilinearMap.alternatization a)).domCoprod ↑(MultilinearMap.alternatization b) =
    ∑ σa,
      ∑ σb,
        Equiv.Perm.sign σa •
          Equiv.Perm.sign σb • (MultilinearMap.domDomCongr σa a).domCoprod (MultilinearMap.domDomCongr σb b)
-- Mathlib.Analysis.Calculus.FDeriv.Pow
/-- Eta-expanded form of `Differentiable.pow` -/
Differentiable.fun_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸},
  Differentiable 𝕜 f → ∀ (n : ℕ), Differentiable 𝕜 fun i => f i ^ n
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.mapRightHomologyIso_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hr : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S.HasRightHomology]
  [inst_6 : F.PreservesRightHomologyOf S],
  S.mapRightHomologyIso F = (hr.map F).rightHomologyIso ≪≫ F.mapIso hr.rightHomologyIso.symm
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
_private.Std.Tactic.BVDecide.LRAT.Internal.Clause.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_1.eq_2 : ∀ (motive : Option Bool → Sort u_1) (x : Option Bool) (h_1 : (val' : Bool) → motive (some val'))
  (h_2 : (x : Option Bool) → motive x),
  (∀ (val' : Bool), x = some val' → False) →
    (match x with
      | some val' => h_1 val'
      | x => h_2 x) =
      h_2 x
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.submoduleMap_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M₂] [inst_5 : TopologicalSpace M₂]
  {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃SL[σ₁₂] M₂) (p : Submodule R M) (x : ↥p), ↑((e.submoduleMap p) x) = e ↑x
-- Mathlib.CategoryTheory.Monad.Limits
/-- The forgetful functor from the Eilenberg-Moore category creates limits.  -/
CategoryTheory.Monad.forgetCreatesLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} → CategoryTheory.CreatesLimitsOfSize.{u_1, u_2, v₁, v₁, max u₁ v₁, u₁} T.forget
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- An equivalence `F` induces an equivalence `CostructuredArrow F X ≌ Over X`.  -/
CategoryTheory.CostructuredArrow.isEquivalence_toOver : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (X : T) [F.IsEquivalence],
  (CategoryTheory.CostructuredArrow.toOver F X).IsEquivalence
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
/-- The inverse of an element of the quaternion group.
 -/
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.QuaternionGroup.inv : {n : ℕ} → QuaternionGroup n → QuaternionGroup n
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Poly.add_denote : ∀ (ctx : Nat.Internal.Linear.Context) (p₁ p₂ : Nat.Internal.SOM.Poly),
  Nat.Internal.SOM.Poly.denote ctx (p₁.add p₂) =
    Nat.Internal.SOM.Poly.denote ctx p₁ + Nat.Internal.SOM.Poly.denote ctx p₂
-- Qq.MetaM
Qq.instantiateMVarsQ : {u : Lean.Level} → {α : Q(Sort u)} → Q(«$α») → Lean.MetaM Q(«$α»)
-- Aesop.Forward.Substitution
_private.Aesop.Forward.Substitution.0.Aesop.Substitution.cmpExprs : Lean.Expr → Lean.Expr → Ordering
-- Lean.Syntax
Lean.Syntax.isAntiquots : Lean.Syntax → Bool
-- Mathlib.Order.Filter.Pointwise
Filter.inv_le_self : ∀ {α : Type u_2} [inst : InvolutiveInv α] {f : Filter α}, f⁻¹ ≤ f ↔ f⁻¹ = f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_modify_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} {f : β → β}, m.WF → (m.modify k f).getKey? k = if k ∈ m then some k else none
-- Init.Data.Nat.Bitwise.Lemmas
Nat.xor_lt_two_pow : ∀ {x y n : ℕ}, x < 2 ^ n → y < 2 ^ n → x ^^^ y < 2 ^ n
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- the induced functor on the constructed localized categories is fully faithful  -/
CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.nonempty_fullyFaithful : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C₁}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  [self : Φ.IsLocalizedFullyFaithful], Nonempty (Φ.localizedFunctor W₁.Q W₂.Q).FullyFaithful
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_le_ofENat : ∀ {m n : ℕ∞}, ↑m ≤ ↑n ↔ m ≤ n
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.one_mem_inv_mul_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Group α] {s t : Finset α}, 1 ∈ t⁻¹ * s ↔ ¬Disjoint s t
-- Mathlib.Tactic.Simps.Basic
/-- The type of rules that specify how metadata for projections in changes.
See `initialize_simps_projections`.  -/
Simps.ProjectionRule : Type
-- Mathlib.Computability.Ackermann
ack_inj_left : ∀ {m₁ m₂ n : ℕ}, ack m₁ n = ack m₂ n ↔ m₁ = m₂
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `Group.isSolvable_of_ker_le_range`. -/
solvable_of_ker_le_range : ∀ {G : Type u_1} [inst : Group G] {G' : Type u_3} {G'' : Type u_4} [inst_1 : Group G'] [inst_2 : Group G'']
  (f : G' →* G) (g : G →* G''),
  g.ker ≤ f.range → ∀ [hG' : Group.IsSolvable G'] [hG'' : Group.IsSolvable G''], Group.IsSolvable G
-- Mathlib.Algebra.Order.Ring.Defs
/-- A nontrivial ordered ring is of characteristic zero.
This is not made a global instance for performance reasons.  -/
IsOrderedRing.toCharZero : ∀ {R : Type u} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Nontrivial R], CharZero R
-- Mathlib.Topology.LocallyFinsupp
/-- Simplifier lemma: Support does not change when replacing a function with locally finite support by
its negative.
 -/
Function.locallyFinsuppWithin.support_neg : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddGroup Y]
  (D : Function.locallyFinsuppWithin U Y), (-D).support = D.support
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinAt.restrictScalars : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕜' : Type u_9}
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' E]
  [inst_8 : IsScalarTower 𝕜 𝕜' E] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜' E F} {x : E} {s : Set E},
  HasFPowerSeriesWithinAt f p s x → HasFPowerSeriesWithinAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) s x
-- Mathlib.Topology.Algebra.Valued.WithVal
Valuation.exists_div_eq_of_surjective : ∀ {K : Type u_7} [inst : DivisionRing K] {Γ₀ : Type u_8} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  {v : Valuation K Γ₀}, Function.Surjective ⇑v → ∀ (γ : Γ₀ˣ), ∃ r s, 0 < v r ∧ 0 < v s ∧ v r / v s = ↑γ
-- Init.Data.SInt.Bitwise
Int32.and_neg_one : ∀ {a : Int32}, a &&& -1 = a
-- Mathlib.Computability.NFA
NFA.evalFrom_iUnion₂ : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) {ι : Sort u_1} {κ : ι → Sort u_2} (f : (i : ι) → κ i → Set σ) (x : List α),
  M.evalFrom (⋃ i, ⋃ j, f i j) x = ⋃ i, ⋃ j, M.evalFrom (f i j) x
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
/-- Given a set of vertex pairs, remove all of the corresponding edges from the
graph's edge set, if present.

See also: `SimpleGraph.Subgraph.deleteEdges`.  -/
SimpleGraph.deleteEdges : {V : Type u_1} → SimpleGraph V → Set (Sym2 V) → SimpleGraph V
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- Let `F` be a functor from sheaf of `R`-module to sheaf of `S`-module, if `F` preserves
colimits and `F.obj (unit R) ≅ unit S`, given a `P : Presentation M`, then we will get a
`Presentation (F.obj M)`.  -/
SheafOfModules.Presentation.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {C' : Type u₂} →
              [inst_3 : CategoryTheory.Category.{v₂, u₂} C'] →
                {J' : CategoryTheory.GrothendieckTopology C'} →
                  {S : CategoryTheory.Sheaf J' RingCat} →
                    [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] →
                      [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat] →
                        {M : SheafOfModules R} →
                          M.Presentation →
                            (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) →
                              [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂,
                                      max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
                                    F] →
                                (SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) → (F.obj M).Presentation
-- Init.Data.Nat.Lemmas
Nat.max_self : ∀ (a : ℕ), max a a = a
-- Lean.Elab.Tactic.Simp
/-- Configuration for `simp`, for supporting tactic configuration option syntax.
 -/
Lean.Meta.Simp.ConfigWithOptions : Type
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instSetLike.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenAddSubgroup.instSetLike = { coe := fun U => ↑↑U, coe_injective := ⋯ }
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- emetric space instance on the product of finitely many emetric spaces, using the `L^p`
edistance, and having as uniformity the product uniformity.  -/
PiLp.instEMetricSpace : (p : ENNReal) →
  {ι : Type u_2} →
    (α : ι → Type u_3) → [hp : Fact (1 ≤ p)] → [Fintype ι] → [(i : ι) → EMetricSpace (α i)] → EMetricSpace (PiLp p α)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.split_dvd : ∀ {o o' : ONote} {m : ℕ} [o.NF], o.split = (o', m) → Ordinal.omega0 ∣ o'.repr
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.step_eq_step : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α] {it : Std.Iter α},
  it.step = ⟨Std.Rxo.Iterator.step it, ⋯⟩
-- Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
isProperMap_dist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [ProperSpace α] (x : α), IsProperMap (dist x)
-- Init.MetaTypes
/-- When `true` (default : `true`), then `simp` catches runtime exceptions and
converts them into `simp` exceptions.
 -/
Lean.Meta.Simp.Config.catchRuntime : Lean.Meta.Simp.Config → Bool
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Vector.0.Std.Iterators.Types.ArrayIterator.instIterator.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) (it : Std.IterM m α)
  (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_2 it
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.BimonObj.one_counit : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (M : C) [self : CategoryTheory.BimonObj M],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.ComonObj.counit =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S}
  {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (P : CategoryTheory.Functor Cᵒᵖ A)
  {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c)
  {d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)} (g : F.Hom G)
  (t : CategoryTheory.Limits.Multifork (G.multicospanIndex P)) (hd : CategoryTheory.Limits.IsLimit d) {Z : A}
  (h : c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((f.comp g).mapMultiforkOfIsLimit P hc t) h =
    CategoryTheory.CategoryStruct.comp (g.mapMultiforkOfIsLimit P hd t)
      (CategoryTheory.CategoryStruct.comp (f.mapMultiforkOfIsLimit P hc d) h)
-- Mathlib.Data.Set.Prod
Equiv.piCongrLeft_symm_preimage_pi : ∀ {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} (f : ι' ≃ ι) (s : Set ι') (t : (i : ι) → Set (α i)),
  (⇑(Equiv.piCongrLeft α f).symm ⁻¹' s.pi fun i' => t (f i')) = (⇑f '' s).pi t
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.subsingleton_fiber_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  [CategoryTheory.LocallySmall.{w, v, u} C] {U T : C} (f : U ⟶ T) [CategoryTheory.Mono f]
  (hT : CategoryTheory.Limits.IsTerminal T), Subsingleton (Φ.fiber.obj U)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
csInf_singleton : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] (a : α), sInf {a} = a
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- (Impl) A preliminary definition to avoid timeouts.  -/
CategoryTheory.Over.ConstructProducts.conesEquivCounitIso : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (B : C) →
        (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) →
          (CategoryTheory.Over.ConstructProducts.conesEquivInverse B F).comp
              (CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F) ≅
            CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
/-- The rank of `M` at the stalk of `p` is the rank of `Mₚ` as a `Rₚ`-module.  -/
Module.rankAtStalk : {R : Type uR} → (M : Type uM) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → PrimeSpectrum R → ℕ
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.cancelBaseChange_symm_comp_lTensor : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_8) [inst_1 : CommRing A] [inst_2 : Algebra R A] (C : Type u_11)
  [inst_3 : CommRing C] [inst_4 : Algebra R C] [inst_5 : Algebra A C] [inst_6 : IsScalarTower R A C] (S : Type u_12)
  [inst_7 : CommRing S] [inst_8 : Algebra R S],
  (↑(Algebra.IsPushout.cancelBaseChangeAlg R S A (TensorProduct R S A) C).symm).comp
      (Algebra.TensorProduct.lTensor S (IsScalarTower.toAlgHom R A C)) =
    Algebra.TensorProduct.includeLeft
-- Mathlib.Order.SymmDiff
symmDiff_symmDiff_left : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b c : α),
  symmDiff (symmDiff a b) c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of the forward direction of `nonpos_iff_eq_zero`. -/
eq_zero_of_nonpos : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α], a ≤ 0 → a = 0
-- Mathlib.Topology.MetricSpace.Cover
Metric.IsCover.anti : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {s t N : Set X},
  s ⊆ t → Metric.IsCover ε t N → Metric.IsCover ε s N
-- Mathlib.Data.List.Cycle
List.nextOr_infix_of_mem_dropLast : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α}, a ∈ l.dropLast → ∀ (d : α), [a, l.nextOr a d] <:+: l
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin_symm : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂),
  (Matrix.toLin v₁ v₂).symm = LinearMap.toMatrix v₁ v₂
-- Mathlib.Algebra.Group.Pi.Basic
Sum.elim_zero_single : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Zero γ] (i : β)
  (c : γ), Sum.elim 0 (Pi.single i c) = Pi.single (Sum.inr i) c
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.denom_cocycle : ∀ (g h : GL (Fin 2) ℝ) {z : ℂ},
  z.im ≠ 0 →
    UpperHalfPlane.denom (g * h) z =
      UpperHalfPlane.denom g (UpperHalfPlane.num h z / UpperHalfPlane.denom h z) * UpperHalfPlane.denom h z
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_eq_default : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)}, l.isEmpty = true → Std.Internal.List.maxKey! l = default
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.toTopologicalSpace_le : ∀ {α : Type u} [inst : AddGroup α] {x y : AddGroupTopology α}, x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore subtrahend of a difference.  -/
AddOreLocalization.AddOreSet.oreSubtra : {R : Type u_1} → {inst : AddMonoid R} → {S : AddSubmonoid R} → [self : AddOreLocalization.AddOreSet S] → R → ↥S → ↥S
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.mkIte : Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.hasLeftHomology_iff_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.HasLeftHomology ↔ S.op.HasRightHomology
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.workerCrashed : Lean.JsonRpc.ErrorCode
-- Mathlib.CategoryTheory.Types.Basic
/-- **Alias** of `CategoryTheory.Iso.hom_inv_id_apply`. -/
CategoryTheory.hom_inv_id_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {F : C → C → Type uF}
  {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_1 : CategoryTheory.ConcreteCategory C F] (x : carrier X),
  (CategoryTheory.ConcreteCategory.hom self.inv) ((CategoryTheory.ConcreteCategory.hom self.hom) x) = x
-- Mathlib.Algebra.Module.Equiv.Basic
/-- **Alias** of `LinearEquiv.toLinearMap_ofLinearMap`. -/
LinearEquiv.ofLinear_toLinearMap : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂)
  (g : M₂ →ₛₗ[σ₂₁] M) (h₁ : f ∘ₛₗ g = LinearMap.id) (h₂ : g ∘ₛₗ f = LinearMap.id),
  ↑(LinearEquiv.ofLinearMap f g h₁ h₂) = f
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Descr.toOLeanEntry : {α β σ : Type} → Lean.ScopedEnvExtension.Descr α β σ → β → α
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.LinearCnstr.toArith : Array Lean.Expr → Lean.Meta.Simp.Arith.Nat.LinearCnstr → Lean.MetaM Lean.Expr
-- Mathlib.Data.List.Basic
List.length_eq_succ_iff : ∀ {α : Type u} {n : ℕ} {l : List α}, l.length = n + 1 ↔ ∃ h t, h :: t = l ∧ t.length = n
-- Lean.Meta.Tactic.Subst
/-- Given a goal `(a = b) → goal[b]`, creates a new goal `goal[a]`, clearing `b`.

This is essentially `intro h; subst h`, but in the case that `b` is a free variable and has no
forward dependencies implements this without introducing the equality, which can make a difference
in terms of performance.

If `substLHS = true`, assume `(a = b) → goal[a]` and create goal `goal[b]`, clearing `a`.

Also handles heterogeneous equalities in cases where `eq_of_heq` would apply.
 -/
Lean.Meta.introSubstEq : Lean.MVarId → optParam Bool false → Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId)
-- Mathlib.Order.CompleteLattice.Basic
sSup_eq_bot' : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.types_ι_jointly_surjective : ∀ (D : CategoryTheory.GlueData (Type v)) (x : D.glued), ∃ i y, (CategoryTheory.ConcreteCategory.hom (D.ι i)) y = x
-- Std.Do.Internal.Ensures.Lemmas
/-- `MayReturn` implies `MonadAttach.CanReturn` for `WeaklyLawfulMonadAttach` instances.  -/
Std.Do.Internal.MayReturn.canReturn : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m]
  [WeaklyLawfulMonadAttach m] {x : m α} {a : α}, Std.Do.Internal.MayReturn x a → MonadAttach.CanReturn x a
-- Mathlib.Topology.MetricSpace.BundledFun
/-- A pseudometric can be nonarchimedean (or ultrametric), with a stronger triangle
inequality such that `d x z ≤ max (d x y) (d y z)`.  -/
PseudoMetric.IsUltra : {X : Type u_1} →
  {R : Type u_2} → [inst : Zero R] → [inst_1 : Add R] → [inst_2 : LE R] → [Max R] → PseudoMetric X R → Prop
-- Init.Data.BitVec.Decidable
BitVec.instDecidableExistsBitVecZero : (P : BitVec 0 → Prop) → [Decidable (P 0#0)] → Decidable (∃ v, P v)