mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [inst : ProbabilityTheory.IsFiniteKernel η] (a : α),
  (η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdFstIsoProd_inv_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Z] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
  [inst_3 : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f CategoryTheory.Limits.prod.fst) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
-- Init.Internal.Order.Basic
Lean.Order.ReverseImplicationOrder.instOrder : Lean.Order.PartialOrder Lean.Order.ReverseImplicationOrder
-- Init.Data.String.Basic
String.Pos.Raw.next'_eq : ∀ (s : String) (p : String.Pos.Raw) (h : ¬String.Pos.Raw.atEnd s p = true),
  String.Pos.Raw.next' s p h = String.Pos.Raw.next s p
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.prod : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {E₁ : Type u_3} {E₂ : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} E₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} E₂]
  {F₁ : CategoryTheory.Functor C₁ E₁} {F₂ : CategoryTheory.Functor C₂ E₂},
  W₁.IsInvertedBy F₁ → W₂.IsInvertedBy F₂ → (W₁.prod W₂).IsInvertedBy (F₁.prod F₂)
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_div' : ∀ {x y : ℝ}, 0 ≤ y → (x / y).toNNReal = x.toNNReal / y.toNNReal
-- Mathlib.Topology.Order.OrderClosed
nhds_inf_atBot : ∀ {α : Type u} [inst : Preorder α] [NoBotOrder α] [inst_2 : TopologicalSpace α] [ClosedIicTopology α] (a : α),
  nhds a ⊓ Filter.atBot = ⊥
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
CliffordAlgebra.evenOdd.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (i : ZMod 2), CliffordAlgebra.evenOdd Q i = ⨆ j, (CliffordAlgebra.ι Q).range ^ ↑j
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalRenameInaccessibles : Lean.Elab.Tactic.Tactic
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearEquiv.reduce_mkQ : ∀ {R : Type u_4} {V : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] (W : Submodule R V)
  (u : ↥(MulAction.stabilizer (V ≃ₗ[R] V) W)) (x : V), ((LinearEquiv.reduce W) u) (W.mkQ x) = W.mkQ (↑u x)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftUnitor_inv_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv Y =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).inv
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.lift_unique : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  (hg : ∀ (y : ↥M), IsUnit (g ↑y)) {j : S →+* P}, (∀ (x : R), j ((algebraMap R S) x) = g x) → IsLocalization.lift hg = j
-- Mathlib.Topology.Separation.Lemmas
CompletelyRegularSpace.instTotallySeparatedSpaceOfCountable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T35Space X] [Countable X], TotallySeparatedSpace X
-- Mathlib.Data.Seq.Computation
Computation.results_think : ∀ {α : Type u} {s : Computation α} {a : α} {n : ℕ}, s.Results a n → s.think.Results a (n + 1)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
NNReal.measurableSpace : MeasurableSpace NNReal
-- Lake.Util.Casing
/-- Converts a snake case, kebab case, or lower camel case `String` to upper camel case.  -/
Lake.toUpperCamelCaseString : String → String
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.opEquiv_symm_apply_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (g : X.PtSimplex n x),
  (SSet.PtSimplex.opEquiv.symm g).map = SSet.yonedaEquiv.symm (SSet.opObjEquiv.symm (SSet.yonedaEquiv g.map))
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasFiniteColimits_opposite_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Limits.HasFiniteColimits Cᵒᵖ ↔ CategoryTheory.Limits.HasFiniteLimits C
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.image_source_inter_eq : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α),
  ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)
-- Mathlib.Algebra.Ring.Units
Units.add_eq_mul_one_add_div : ∀ {R : Type x} [inst : Semiring R] {a : Rˣ} {b : R}, ↑a + b = ↑a * (1 + ↑a⁻¹ * b)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
MulOpposite.opLinearIsometryEquiv_apply : ∀ (R : Type u_11) (H : Type u_12) [inst : Semiring R] [inst_1 : SeminormedAddCommGroup H] [inst_2 : Module R H] (a : H),
  (MulOpposite.opLinearIsometryEquiv R H) a = MulOpposite.op a
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.add_apply : ∀ {R : Type u_1} [inst : AddMonoid R] {f g : ArithmeticFunction R} {n : ℕ}, (f + g) n = f n + g n
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.empty_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C) (i : PEmpty.{w + 1}),
  (CategoryTheory.PreZeroHypercover.empty S).f i = i.elim
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.isUnit_iff_bijective : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {f : E →L[𝕜] E}, IsUnit f ↔ Function.Bijective ⇑f
-- Mathlib.RingTheory.Valuation.RankOne
/-- A valuation has rank one if it is nontrivial and its image is contained in `ℝ≥0`.
Note that this class includes the data of an inclusion morphism `Γ₀ → ℝ≥0`.  -/
Valuation.RankOne : {R : Type u_1} →
  {Γ₀ : Type u_2} → [inst : Ring R] → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → Valuation R Γ₀ → Type u_2
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_image' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι]
  {s : Finset κ} {g : κ → ι} (h : κ → M),
  (∀ i ∈ s, f (g i) = ∑ j ∈ s with g j = g i, h j) → ∑ a ∈ Finset.image g s, f a = ∑ i ∈ s, h i
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The profinite completion functor.  -/
ProfiniteGrp.profiniteCompletion : CategoryTheory.Functor GrpCat ProfiniteGrp.{u}
-- Init.Prelude
/-- The data contained in the byte array.

Converting between `Array` and `ByteArray` takes linear time.
 -/
ByteArray.data : ByteArray → Array UInt8
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableWithinAt.rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x →
    DifferentiableWithinAt ℝ g s x → f x ≠ 0 → DifferentiableWithinAt ℝ (fun x => f x ^ g x) s x
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.instNormedCommGroup.eq_1 : ∀ {E : Type u_2} [inst : SeminormedCommGroup E],
  SeparationQuotient.instNormedCommGroup =
    { toNorm := SeparationQuotient.instMulNorm, toCommGroup := SeparationQuotient.instCommGroup,
      toMetricSpace := SeparationQuotient.instMetricSpace, dist_eq := ⋯ }
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.foldM_filterM : ∀ {α β δ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : Std.Internal.Do.Assertion Pred] [inst_8 : Std.Internal.Do.Assertion EPred]
  [inst_9 : Std.Internal.Do.WPMonad o Pred EPred] [inst_10 : Std.IteratorLoop α Id n]
  [inst_11 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o]
  [inst_14 : MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → n (ULift.{w, 0} Bool)} {g : δ → β → o δ} {init : δ}
  {it : Std.Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b => do
          let __do_lift ← liftM (f b)
          if __do_lift.down = true then g d b else pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.Iter.filterM f it) ⦃ Q; eQ ⦄
-- Mathlib.RingTheory.HahnSeries.HEval
HahnSeries.SummableFamily.powerSeriesFamily.congr_simp : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : CommRing V] [inst_5 : Algebra R V]
  (x x_1 : HahnSeries Γ V),
  x = x_1 →
    ∀ (f f_1 : PowerSeries R),
      f = f_1 → HahnSeries.SummableFamily.powerSeriesFamily x f = HahnSeries.SummableFamily.powerSeriesFamily x_1 f_1
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Returns the types of `xs` that are propositions.  -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.getPropTypes : Array Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.NumberTheory.Divisors
Nat.divisors_inj : ∀ {a b : ℕ}, a.divisors = b.divisors ↔ a = b
-- Mathlib.RingTheory.Finiteness.Subalgebra
Subalgebra.fg_bot_toSubmodule : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  (Subalgebra.toSubmodule ⊥).FG
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.toFun_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] (f : OneHom M N), f.toFun = ⇑f
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapRingEquiv_single : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddMonoid M]
  (e : R ≃+* S) (r : R) (m : M),
  (AddMonoidAlgebra.mapRingEquiv M e) (AddMonoidAlgebra.single m r) = AddMonoidAlgebra.single m (e r)
-- Mathlib.Analysis.Normed.Group.Basic
norm_nsmul_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a : E} {n : ℕ}, ‖n • a‖ ≤ ↑n * ‖a‖
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- The left lifting property with respect to all monomorphisms  -/
CategoryTheory.StrongEpi.llp : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P Q : C} {f : P ⟶ Q} [self : CategoryTheory.StrongEpi f]
  ⦃X Y : C⦄ (z : X ⟶ Y) [CategoryTheory.Mono z], CategoryTheory.HasLiftingProperty f z
-- Init.Data.Range.Polymorphic.Iterators
Std.Roi.Internal.iter.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (r : Std.Roi α),
  Std.Roi.Internal.iter r = { internalState := { next := Std.PRange.succ? r.lower } }
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whisker_assoc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Y' : C}
  (f : Y ⟶ Y') (Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y') Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) Z) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y' Z).inv h))
-- Init.Data.Array.Lemmas
Array.extract_loop_eq : ∀ {α : Type u_1} {xs ys : Array α} {size start : ℕ},
  start + size ≤ xs.size → Array.extract.loop xs size start ys = ys ++ xs.extract start (start + size)
-- Mathlib.Algebra.Homology.AlternatingConst
HomologicalComplex.alternatingConstScIsoOdd.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0)
  (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [inst_2 : DecidableRel c.Rel]
  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) {i j k : ℕ} (hij : c.Rel i j) (hjk : c.Rel j k) (h : Odd j),
  HomologicalComplex.alternatingConstScIsoOdd A hOdd hEven hc hij hjk h =
    CategoryTheory.ShortComplex.isoMk
      (CategoryTheory.Iso.refl ((HomologicalComplex.alternatingConst A hOdd hEven hc).sc' i j k).X₁)
      (CategoryTheory.Iso.refl ((HomologicalComplex.alternatingConst A hOdd hEven hc).sc' i j k).X₂)
      (CategoryTheory.Iso.refl ((HomologicalComplex.alternatingConst A hOdd hEven hc).sc' i j k).X₃) ⋯ ⋯
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `deriv_fun_const_smul_field`.

---

A variant of `deriv_fun_const_smul` without differentiability assumption when the scalar
multiplication is by division ring elements.  -/
deriv_fun_const_smul' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {𝕝 : Type u_3} [inst_3 : DivisionSemiring 𝕝] [inst_4 : Module 𝕝 F]
  [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] (c : 𝕝) (f : 𝕜 → F), deriv (fun y => c • f y) x = c • deriv f x
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_strictMono_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f → StrictMono (AddSubmonoid.comap f)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.toInt'.toIntAndExpandWrap : Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.CofibrantObject.homMk_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X : C) [inst_3 : HomotopicalAlgebra.IsCofibrant X],
  HomotopicalAlgebra.CofibrantObject.homMk (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id (HomotopicalAlgebra.CofibrantObject.mk X)
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instCompleteLattice : {α : Type u} → [inst : Group α] → CompleteLattice (GroupTopology α)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.add_mod : ∀ {R : Type u} [inst : Field R] (p₁ p₂ q : Polynomial R), (p₁ + p₂) % q = p₁ % q + p₂ % q
-- Mathlib.Order.Bounds.Image
BddAbove.range_mono : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} (g : α → β),
  (∀ (a : α), f a ≤ g a) → BddAbove (Set.range g) → BddAbove (Set.range f)
-- Mathlib.Topology.Gluing
TopCat.GlueData.fromOpenSubsetsGlue_isOpenMap : ∀ {α : Type u} [inst : TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α),
  IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.GlueData.fromOpenSubsetsGlue U))
-- Mathlib.Combinatorics.SetFamily.Compression.Down
/-- Down-compressing a family is idempotent.  -/
Down.compression_idem : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 : Finset (Finset α)),
  Down.compression a (Down.compression a 𝒜) = Down.compression a 𝒜
-- Mathlib.Topology.FiberPartition
/-- The inclusion map from a fiber of a composition into the intermediate fiber.  -/
TopologicalSpace.Fiber.sigmaInclIncl : {S : Type u_1} →
  {Y : Type u_2} →
    (f : S → Y) →
      [inst : TopologicalSpace S] →
        {X : Type u_3} →
          (g : Y → X) →
            (a : Function.Fiber (g ∘ f)) →
              (b : Function.Fiber (f ∘ ⇑(TopologicalSpace.Fiber.sigmaIncl (g ∘ f) a))) →
                C(↑↑b,
                  ↑↑(Function.Fiber.mk f
                        ↑(Function.Fiber.preimage (f ∘ ⇑(TopologicalSpace.Fiber.sigmaIncl (g ∘ f) a)) b)))
-- Mathlib.Analysis.AbsoluteValue.Equivalence
/-- An absolute value is equivalent to the trivial iff it is trivial itself.  -/
AbsoluteValue.isEquiv_trivial_iff_eq_trivial : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : Semifield S] [inst_2 : LinearOrder S]
  [inst_3 : DecidablePred fun x => x = 0] [inst_4 : NoZeroDivisors R] [inst_5 : IsStrictOrderedRing S]
  {f : AbsoluteValue R S}, f.IsEquiv AbsoluteValue.trivial ↔ f = AbsoluteValue.trivial
-- Std.Data.Iterators.Lemmas.Producers.Empty
Std.Iter.fold_empty : ∀ {β : Type u_1} {γ : Type u_2} {init : γ} {f : γ → β → γ}, Std.Iter.fold f init (Std.Iter.empty β) = init
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.run : Lean.Elab.Term.Do.Code →
  Lean.Syntax →
    Lean.Syntax →
      optParam (Array Lean.Elab.Term.Do.Var) #[] →
        optParam Lean.Elab.Term.Do.ToTerm.Kind Lean.Elab.Term.Do.ToTerm.Kind.regular → Lean.MacroM Lean.Syntax
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Preconnected.exists_adj_of_nontrivial : ∀ {V : Type u} [Nontrivial V] {G : SimpleGraph V}, G.Preconnected → ∀ (v : V), ∃ u, G.Adj v u
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- **Pythagorean theorem**, if-and-only-if angle-at-point form.  -/
EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ p₃ : P),
  dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔
    EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanShape.mk.injEq : ∀ (L : Type w) (R : Type w') (fst snd : L → R) (L_1 : Type w) (R_1 : Type w') (fst_1 snd_1 : L_1 → R_1),
  ({ L := L, R := R, fst := fst, snd := snd } = { L := L_1, R := R_1, fst := fst_1, snd := snd_1 }) =
    (L = L_1 ∧ R = R_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1)
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.sum_eq_zero_iff : ∀ {α : Type u_2} [inst : AddCommMonoid α] {m : Multiset α} [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α]
  [IsOrderedAddMonoid α], m.sum = 0 ↔ ∀ x ∈ m, x = 0
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.isCycle_swap : ∀ {α : Type u_2} {x y : α} [inst : DecidableEq α], x ≠ y → (Equiv.swap x y).IsCycle
-- Mathlib.Data.EReal.Basic
EReal.exists_between_coe_real : ∀ {x z : EReal}, x < z → ∃ y, x < ↑y ∧ ↑y < z
-- Mathlib.Algebra.Order.Module.Defs
le_of_smul_le_smul_of_neg : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulReflectLE α β], a • b₁ ≤ a • b₂ → a < 0 → b₂ ≤ b₁
-- Mathlib.Algebra.Algebra.Tower
AlgHom.mk.congr_simp : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (toRingHom toRingHom_1 : A →+* B)
  (e_toRingHom : toRingHom = toRingHom_1)
  (commutes' : ∀ (r : R), (↑↑toRingHom).toFun ((algebraMap R A) r) = (algebraMap R B) r),
  { toRingHom := toRingHom, commutes' := commutes' } = { toRingHom := toRingHom_1, commutes' := ⋯ }
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.instPreservesZeroMorphismsRepModuleCatFunctor : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (n : ℕ), (groupCohomology.functor k G n).PreservesZeroMorphisms
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.map_id : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι],
  AddCommGroup.DirectLimit.map (fun x => AddMonoidHom.id (G x)) ⋯ = AddMonoidHom.id (AddCommGroup.DirectLimit G f)
-- Init.Tactics
/-- `repeat tac` repeatedly applies `tac` so long as it succeeds.
The tactic `tac` may be a tactic sequence, and if `tac` fails at any point in its execution,
`repeat` will revert any partial changes that `tac` made to the tactic state.

The tactic `tac` should eventually fail, otherwise `repeat tac` will run indefinitely.

See also:
* `try tac` is like `repeat tac` but will apply `tac` at most once.
* `repeat' tac` recursively applies `tac` to each goal.
* `first | tac1 | tac2` implements the backtracking used by `repeat`
 -/
Lean.Parser.Tactic.tacticRepeat_ : Lean.ParserDescr
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConstC.go.induct_unfolding : ∀ (k : ℤ) (c : ℕ) (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k_1 : ℤ), motive (Lean.Grind.CommRing.Poly.num k_1) (Lean.Grind.CommRing.Poly.num (k * k_1 % ↑c))) →
    (∀ (k_1 : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        have k_2 := k * k_1 % ↑c;
        (k_2 == 0) = true →
          motive p (Lean.Grind.CommRing.Poly.mulConstC.go k c p) →
            motive (Lean.Grind.CommRing.Poly.add k_1 m p) (Lean.Grind.CommRing.Poly.mulConstC.go k c p)) →
      (∀ (k_1 : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
          have k_2 := k * k_1 % ↑c;
          (k_2 == 0) = false →
            motive p (Lean.Grind.CommRing.Poly.mulConstC.go k c p) →
              motive (Lean.Grind.CommRing.Poly.add k_1 m p)
                (Lean.Grind.CommRing.Poly.add k_2 m (Lean.Grind.CommRing.Poly.mulConstC.go k c p))) →
        ∀ (a : Lean.Grind.CommRing.Poly), motive a (Lean.Grind.CommRing.Poly.mulConstC.go k c a)
-- Mathlib.CategoryTheory.Comma.LocallySmall
CategoryTheory.Comma.locallySmall : ∀ {A : Type u₁} {B : Type u₂} {T : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [CategoryTheory.LocallySmall.{w, v₁, u₁} A]
  [CategoryTheory.LocallySmall.{w, v₂, u₂} B],
  CategoryTheory.LocallySmall.{w, max v₁ v₂, max (max u₂ u₁) v₃} (CategoryTheory.Comma L R)
-- Mathlib.Order.Cofinal
OrderIso.map_isCofinal : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {s : Set α},
  IsCofinal s → IsCofinal (⇑e '' s)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_eq_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.WF → ∀ {k fallback : α}, k ∈ t → t.getD k fallback = k
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppLeft.eq_1 : ∀ (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 ι],
  TensorProduct.finsuppLeft R S M N ι =
    TensorProduct.AlgebraTensorModule.congr (finsuppLEquivDirectSum S M ι) (LinearEquiv.refl R N) ≪≫ₗ
        TensorProduct.directSumLeft R S (fun x => M) N ≪≫ₗ
      (finsuppLEquivDirectSum S (TensorProduct R M N) ι).symm