mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.PreDefinition.Structural.FindRecArg
_private.Lean.Elab.PreDefinition.Structural.FindRecArg.0.Lean.Elab.Structural.allCombinations.go.eq_def : ∀ {α : Type u_1} (xss : Array (Array α)) (i : ℕ) (acc : Array α),
  Lean.Elab.Structural.allCombinations.go✝ xss i acc =
    if h : i < xss.size then
      Array.flatMap (fun x => Lean.Elab.Structural.allCombinations.go✝ xss (i + 1) (acc.push x)) xss[i]
    else #[acc]
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_cast_add : ∀ {n : ℕ} (x y : ZMod n), (x + y).cast = (x.cast + y.cast) % ↑n
-- Mathlib.Algebra.Group.Action.Option
Option.instSMul_mathlib.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul M α],
  Option.instSMul_mathlib = { smul := fun a => Option.map fun x => a • x }
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.unop_distinguished : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_succ_dist_weak : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2),
  (Polynomial.aeval a) F ≠ 0 →
    ∀ (n : ℕ),
      ‖newton_seq_gen✝ hnorm (n + 2) - newton_seq_gen✝ hnorm (n + 1)‖ <
        ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.polynomial_ne_zero : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} [Nontrivial R], W.polynomial ≠ 0
-- Mathlib.Algebra.Lie.Ideal
LieSubalgebra.exists_lieIdeal_coe_eq_iff : ∀ (R : Type u) {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (K : LieSubalgebra R L),
  (∃ I, LieIdeal.toLieSubalgebra R L I = K) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K
-- Batteries.Data.PairingHeap
/-- `O(n log n)`. Construct a heap from a list by inserting all the elements.  -/
Batteries.PairingHeap.ofList : {α : Type u} → (le : α → α → Bool) → List α → Batteries.PairingHeap α le
-- Mathlib.Algebra.Prime.Defs
Irreducible.prime : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [DecompositionMonoid M] {a : M}, Irreducible a → Prime a
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.mem_sInf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {S : Set (NonUnitalSubalgebra R A)} {x : A},
  x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.RingTheory.PowerSeries.Restricted
PowerSeries.isRestricted_monomial : ∀ {R : Type u_1} [inst : NormedRing R] (c : ℝ) (n : ℕ) (a : R), PowerSeries.IsRestricted c ((PowerSeries.monomial n) a)
-- Lean.Server.InfoUtils
Lean.Elab.instLEHoverableInfoPrio : LE Lean.Elab.HoverableInfoPrio
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.fst_mul : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Mul α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α]
  (s t : NonemptyInterval α), (s * t).toProd.1 = s.toProd.1 * t.toProd.1
-- Mathlib.Data.List.Cycle
List.next_eq_getElem : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α} (ha : a ∈ l),
  l.next a ha = l[(List.idxOf a l + 1) % l.length]
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fract_fract : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (m : E), ZSpan.fract b (ZSpan.fract b m) = ZSpan.fract b m
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYoneda_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
  (CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X).map f =
    TypeCat.ofHom fun x => { down := CategoryTheory.CategoryStruct.comp f.unop x.down }
-- Mathlib.Data.Matrix.Block
Matrix.toBlocks_fromBlocks₂₁ : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α), (Matrix.fromBlocks A B C D).toBlocks₂₁ = C
-- Mathlib.Tactic.Linter.Whitespace
/-- Scan the two input strings `L` and `M`, assuming `M` is the pretty-printed version of `L`.
This almost means that `L` and `M` only differ in whitespace.

While scanning the two strings, accumulate any discrepancies --- with some heuristics to avoid
flagging some line-breaking changes.
(The pretty-printer does not always produce desirably formatted code.)
 -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.parallelScanAux : Array Mathlib.Linter.FormatError✝ → String.Slice → String.Slice → Array Mathlib.Linter.FormatError✝
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_span_coe_preimage : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  Submodule.span R (Subtype.val ⁻¹' s) = ⊤
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.w_assoc : ∀ {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) {j j' : J} (f : j' ⟶ j) {Z : C} (h : c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (c.ι.app j) h) =
    CategoryTheory.CategoryStruct.comp (c.ι.app j') h
-- Init.Data.Int.Cooper
/-- Given a solution `x` to a divisibility constraint `a ∣ x + c`,
then `x % d` is another solution as long as `a | d`.

See `dvd_mul_emod_add_of_dvd_mul_add` for a more general version allowing a coefficient with `x`.
 -/
Int.dvd_emod_add_of_dvd_add : ∀ {a c d x : ℤ}, a ∣ x + c → a ∣ d → a ∣ x % d + c
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.commMonoid.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : CommMonoid α],
  Finset.commMonoid = Function.Injective.commMonoid SetLike.coe ⋯ ⋯ ⋯ ⋯
-- Std.Time.Time.PlainTime
/-- Creates a `PlainTime` value from a total number of seconds.
 -/
Std.Time.PlainTime.ofSeconds : Std.Time.Second.Offset → Std.Time.PlainTime
-- Mathlib.Topology.Instances.Matrix
/-- When `Ring.inverse` is continuous at the determinant (such as in a `NormedRing`, or a
topological field), so is `Matrix.inv`.  -/
continuousAt_matrix_inv : ∀ {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  [inst_3 : CommRing R] [IsTopologicalRing R] (A : Matrix n n R),
  ContinuousAt Ring.inverse A.det → ContinuousAt Inv.inv A
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ENNReal.measurableSpace : MeasurableSpace ENNReal
-- Mathlib.CategoryTheory.Localization.Trifunctor
/-- The natural transformation `F₁' ⟶ F₂'` of trifunctors induced by a
natural transformation `τ : F₁ ⟶ F₂` when `Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'`
and `Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'` hold.  -/
CategoryTheory.Localization.lift₃NatTrans : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_6} →
        {D₂ : Type u_7} →
          {D₃ : Type u_8} →
            {E : Type u_13} →
              [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
                [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                    [inst_3 : CategoryTheory.Category.{v_4, u_6} D₁] →
                      [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] →
                        [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃] →
                          [inst_6 : CategoryTheory.Category.{v_13, u_13} E] →
                            (L₁ : CategoryTheory.Functor C₁ D₁) →
                              (L₂ : CategoryTheory.Functor C₂ D₂) →
                                (L₃ : CategoryTheory.Functor C₃ D₃) →
                                  (W₁ : CategoryTheory.MorphismProperty C₁) →
                                    (W₂ : CategoryTheory.MorphismProperty C₂) →
                                      (W₃ : CategoryTheory.MorphismProperty C₃) →
                                        [L₁.IsLocalization W₁] →
                                          [L₂.IsLocalization W₂] →
                                            [L₃.IsLocalization W₃] →
                                              [W₁.ContainsIdentities] →
                                                [W₂.ContainsIdentities] →
                                                  [W₃.ContainsIdentities] →
                                                    (F₁ F₂ :
                                                        CategoryTheory.Functor C₁
                                                          (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) →
                                                      (F₁' F₂' :
                                                          CategoryTheory.Functor D₁
                                                            (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) →
                                                        [CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁
                                                              F₁'] →
                                                          [CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂
                                                                F₂'] →
                                                            (F₁ ⟶ F₂) → (F₁' ⟶ F₂')
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.checkDefaultSplitStatus : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Grind.SplitStatus
-- Std.Data.DTreeMap.Internal.Queries
/-- Folds the given function over the mappings in the tree in ascending order.  -/
Std.DTreeMap.Internal.Impl.foldlM : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      {m : Type w → Type u_1} → [Monad m] → (δ → (a : α) → β a → m δ) → δ → Std.DTreeMap.Internal.Impl α β → m δ
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_of_g_is_cokernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C)
  (hS : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) [S.HasHomology], S.Exact
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.cofilteredClosure.below : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] →
      {α : Type w} →
        {f : α → C} →
          {motive : (a : C) → CategoryTheory.IsCofiltered.cofilteredClosure f a → Prop} →
            {a : C} → CategoryTheory.IsCofiltered.cofilteredClosure f a → Prop
-- Init.Core
Decidable.em : ∀ (p : Prop) [Decidable p], p ∨ ¬p
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.subtype_apply : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Subsemiring R} (x : ↥s), s.subtype x = ↑x
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.instInhabited : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → Inhabited (NonUnitalSubsemiring R)
-- Mathlib.Topology.Order.Monotone
/-- A monotone left-continuous function is left-continuous in the order-theoretic sense.  -/
Monotone.leftOrdContinuous : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {f : α → β} [inst_4 : TopologicalSpace β] [OrderTopology β],
  Monotone f → (∀ (x : α), ContinuousWithinAt f (Set.Iic x) x) → LeftOrdContinuous f
-- Mathlib.Topology.Instances.Nat
Nat.dist_cast_real : ∀ (x y : ℕ), dist ↑x ↑y = dist x y
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedCategory.mk : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        (Hom : C → C → V) →
          (id : (X : C) → CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ Hom X X) →
            (comp : (X Y Z : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj (Hom X Y) (Hom Y Z) ⟶ Hom X Z) →
              autoParam
                  (∀ (X Y : C),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Hom X Y)).inv
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (id X) (Hom X Y)) (comp X X Y)) =
                      CategoryTheory.CategoryStruct.id (Hom X Y))
                  CategoryTheory.EnrichedCategory.id_comp._autoParam →
                autoParam
                    (∀ (X Y : C),
                      CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Hom X Y)).inv
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Hom X Y) (id Y)) (comp X Y Y)) =
                        CategoryTheory.CategoryStruct.id (Hom X Y))
                    CategoryTheory.EnrichedCategory.comp_id._autoParam →
                  autoParam
                      (∀ (W X Y Z : C),
                        CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.associator (Hom W X) (Hom X Y) (Hom Y Z)).inv
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.whiskerRight (comp W X Y) (Hom Y Z))
                              (comp W Y Z)) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Hom W X) (comp X Y Z)) (comp W X Z))
                      CategoryTheory.EnrichedCategory.assoc._autoParam →
                    CategoryTheory.EnrichedCategory V C
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreOfNat.injEq : ∀ (a b : Lean.Expr) (natStructId : ℕ) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) (a_1 b_1 : Lean.Expr)
  (natStructId_1 : ℕ) (lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreOfNat a b natStructId lhs rhs =
      Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreOfNat a_1 b_1 natStructId_1 lhs_1 rhs_1) =
    (a = a_1 ∧ b = b_1 ∧ natStructId = natStructId_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.charFn_eq_one : ∀ {X : Type u_1} (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : MulZeroOneClass Y] {U : Set X} [Nontrivial Y]
  (x : X) (hU : IsClopen U), (LocallyConstant.charFn Y hU) x = 1 ↔ x ∈ U
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.OppositeShift.adjunction_counit : ∀ {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] (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G),
  (CategoryTheory.OppositeShift.adjunction A adj).counit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.OppositeShift.natIsoComp A F G).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.OppositeShift.natTrans A adj.unit)
        (CategoryTheory.NatTrans.OppositeShift.natIsoId C A).inv)
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.instInhabitedDecreasingBy : Inhabited Lean.Elab.DecreasingBy
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasLeftInverse.of_comp : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} {G : Type u_6} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f : E →L[R] F} [inst_7 : TopologicalSpace G] [inst_8 : AddCommMonoid G] [inst_9 : Module R G]
  {g : F →L[R] G}, (g ∘SL f).HasLeftInverse → f.HasLeftInverse
-- Mathlib.Topology.Algebra.ConstMulAction
MulAction.IsPretransitive.t1Space_iff : ∀ {α : Type u_2} (G : Type u_4) [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] (x : α) [MulAction.IsPretransitive G α], T1Space α ↔ IsClosed {x}
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.length_eq_one : ∀ {α : Type u_1} {a : FreeAddMonoid α}, a.length = 1 ↔ ∃ m, a = FreeAddMonoid.of m
-- Mathlib.Analysis.Normed.Group.Pointwise
vadd_closedBall_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), x +ᵥ Metric.closedBall 0 δ = Metric.closedBall x δ
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.getElem_toList_eq : ∀ {α : Type u} {r : Std.Rci α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxi.IsAlwaysFinite α] {i : ℕ} {h : i < r.toList.length},
  r.toList[i] = (Std.PRange.succMany? i r.lower).get ⋯
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.PreservesRightKanExtension.mk : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] {G : CategoryTheory.Functor B D} {F : CategoryTheory.Functor A B}
  {L : CategoryTheory.Functor A C},
  (∀ (F' : CategoryTheory.Functor C B) (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α],
      (F'.comp G).IsRightKanExtension
        (CategoryTheory.CategoryStruct.comp (L.associator F' G).inv (CategoryTheory.Functor.whiskerRight α G))) →
    G.PreservesRightKanExtension F L
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, ∅.isEmpty = true
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.continue.inj : ∀ {ref ref_1 : Lean.Syntax}, Lean.Elab.Term.Do.Code.continue ref = Lean.Elab.Term.Do.Code.continue ref_1 → ref = ref_1
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.neg_mem_Ioc_iff : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a c d : α},
  -a ∈ Set.Ioc c d ↔ a ∈ Set.Ico (-d) (-c)
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffWithinAt_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {s : Set M} {x : M}
  {n : WithTop ℕ∞} [inst_11 : One M'], ContMDiffWithinAt I I' n 1 s x
-- Mathlib.Data.Fintype.EquivFin
Finset.card_eq_of_equiv_fin : ∀ {α : Type u_1} {s : Finset α} {n : ℕ} (i : ↥s ≃ Fin n), s.card = n
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.SatelliteConfig.mk : {α : Type u_1} →
  [inst : MetricSpace α] →
    {N : ℕ} →
      {τ : ℝ} →
        (c : Fin N.succ → α) →
          (r : Fin N.succ → ℝ) →
            (∀ (i : Fin N.succ), 0 < r i) →
              (Pairwise fun i j => r i ≤ dist (c i) (c j) ∧ r j ≤ τ * r i ∨ r j ≤ dist (c j) (c i) ∧ r i ≤ τ * r j) →
                (∀ i < Fin.last N, r i ≤ dist (c i) (c (Fin.last N)) ∧ r (Fin.last N) ≤ τ * r i) →
                  (∀ i < Fin.last N, dist (c i) (c (Fin.last N)) ≤ r i + r (Fin.last N)) →
                    Besicovitch.SatelliteConfig α N τ
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.setGrindParams : Lean.TSyntax `tactic → Array Lean.Syntax → Lean.TSyntax `tactic
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOn.prodMap : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [inst_1 : UniformSpace β'] {F' : ι' → α' → β'}
  {f' : α' → β'} {p' : Filter ι'} {s' : Set α'},
  TendstoUniformlyOn F f p s →
    TendstoUniformlyOn F' f' p' s' →
      TendstoUniformlyOn (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (s ×ˢ s')
-- Mathlib.Data.Nat.SuccPred
withBotSucc_one : WithBot.succ 1 = 2
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.eq_freeOn_iff : ∀ {α : Type u_1} {M : Matroid α} {E : Set α}, M = Matroid.freeOn E ↔ M.E = E ∧ M.Indep E
-- Mathlib.NumberTheory.FunctionField
FunctionField.Algebra.IsAlgebraic.adjoin_algebraMap_X : ∀ {F : Type u_3} {K : Type u_4} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (RatFunc F) K] [FunctionField F K]
  [inst_4 : Algebra F K] [IsScalarTower F (RatFunc F) K],
  Algebra.IsAlgebraic (↥F⟮(algebraMap (RatFunc F) K) RatFunc.X⟯) K
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- If `ι` is finite, we use the equivalence of sum and product to obtain an inverse for
`AdicCompletion.sum` from `AdicCompletion.pi`.  -/
AdicCompletion.sumInv : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {ι : Type u_6} →
        (M : ι → Type u_7) →
          [inst_1 : (i : ι) → AddCommGroup (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              [Fintype ι] →
                AdicCompletion I (DirectSum ι fun j => M j) →ₗ[AdicCompletion I R]
                  DirectSum ι fun j => AdicCompletion I (M j)
-- Mathlib.Analysis.Calculus.Deriv.Inv
DifferentiableAt.div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'},
  DifferentiableAt 𝕜 c x → DifferentiableAt 𝕜 d x → d x ≠ 0 → DifferentiableAt 𝕜 (c / d) x
-- Mathlib.Logic.Equiv.Set
Equiv.Set.union_apply_left : ∀ {α : Type u_3} {s t : Set α} [inst : DecidablePred fun x => x ∈ s] (H : Disjoint s t) {a : ↑(s ∪ t)} (ha : ↑a ∈ s),
  (Equiv.Set.union H) a = Sum.inl ⟨↑a, ha⟩
-- Init.Data.UInt.Bitwise
UInt64.and_lt_add_one : ∀ {b c : UInt64}, c ≠ -1 → b &&& c < c + 1
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₂_le : ∀ (x : Ordinal.{u_1}), x.invVeblen₂ ≤ x
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.toOpenPartialHomeomorph_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [inst_5 : CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c)
  (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s),
  ↑(ApproximatesLinearOn.toOpenPartialHomeomorph f s hf hc hs) = f
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instGroup : {α : Type u_1} → [Group α] → Group αᵃᵒᵖ
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
/-- The explicit coproduct cofan constructed in `coproductCofan` is indeed a colimit.  -/
AlgebraicGeometry.LocallyRingedSpace.coproductCofanIsColimit : {ι : Type v} →
  [inst : Small.{u, v} ι] →
    (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) AlgebraicGeometry.LocallyRingedSpace) →
      CategoryTheory.Limits.IsColimit (AlgebraicGeometry.LocallyRingedSpace.coproductCofan F)
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- Reflection is involutive.  -/
Submodule.reflection_trans_reflection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection],
  K.reflection.trans K.reflection = LinearIsometryEquiv.refl 𝕜 E