mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.isPushout_aux : ∀ {X Y : SSet} {i : X ⟶ Y} {d n : ℕ},
  ∀
    y ∉
      Set.range
        ⇑(CategoryTheory.ConcreteCategory.hom ((SSet.relativeCellComplexOfMono.l i d).app (Opposite.op { len := n }))),
    ∃ c f,
      ∃ (_ : CategoryTheory.Epi f),
        (CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app (Opposite.op { len := n })))
            (SSet.stdSimplex.objEquiv.symm f) =
          y
-- Mathlib.Topology.Closure
interior_union_inter_interior_compl_right_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, interior (s ∪ t) ∩ interior tᶜ ⊆ interior s
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α}, ∅.contains a = false
-- Lean.Parser.Extension
Lean.Parser.ParserAliasInfo.mk.sizeOf_spec : ∀ (declName : Lean.Name) (stackSz? : Option ℕ) (autoGroupArgs : Bool),
  sizeOf { declName := declName, stackSz? := stackSz?, autoGroupArgs := autoGroupArgs } =
    1 + sizeOf declName + sizeOf stackSz? + sizeOf autoGroupArgs
-- Mathlib.Topology.ContinuousOn
continuousOn_id' : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α), ContinuousOn (fun x => x) s
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.ι_colimitIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E) [inst_4 : CategoryTheory.Limits.HasColimit G] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (F.obj X))
      (CategoryTheory.Functor.Final.colimitIso F G).inv =
    CategoryTheory.Limits.colimit.ι (F.comp G) X
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mk_neg : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {m : M} {s : ↥S}, LocalizedModule.mk (-m) s = -LocalizedModule.mk m s
-- Mathlib.Algebra.Lie.Submodule
/-- The natural functor that forgets the action of `L` as an order embedding.  -/
LieSubmodule.toSubmodule_orderEmbedding : (R : Type u) →
  (L : Type v) →
    (M : Type w) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → LieSubmodule R L M ↪o Submodule R M
-- Mathlib.Topology.MetricSpace.Pseudo.Real
Real.dist_left_le_of_mem_uIcc : ∀ {x y z : ℝ}, y ∈ Set.uIcc x z → dist x y ≤ dist x z
-- Mathlib.Analysis.Convex.StdSimplex
/-- The (sup metric) diameter of a standard simplex indexed by a nontrivial index is 1.  -/
diam_stdSimplex : ∀ {ι : Type u_1} [inst : Fintype ι] [Nontrivial ι], Metric.diam (stdSimplex ℝ ι) = 1
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis'.isBasis_inter_ground : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis' I X → M.IsBasis I (X ∩ M.E)
-- Mathlib.Topology.Constructions
continuous_toAdd : ∀ {X : Type u} [inst : TopologicalSpace X], Continuous ⇑Multiplicative.toAdd
-- Mathlib.Data.List.AList
AList.insertRec_empty : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {C : AList β → Sort u_1} (H0 : C ∅)
  (IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (AList.insert a b l)), AList.insertRec H0 IH ∅ = H0
-- Init.Prelude
Lean.Macro.instInhabitedState : Inhabited Lean.Macro.State
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.single_eq_zero : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i : ι} {xi : β i},
  (fun₀ | i => xi) = 0 ↔ xi = 0
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The composite of `(coprod.inr ▷ X) : Z ⊗ X ⟶ (Y ⨿ Z) ⊗ X` and
`(∂R X Y Z).inv :  (Y ⨿ Z) ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X)` is equal to the right coprojection
`coprod.inr : Z ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X)`.  -/
CategoryTheory.whiskerRight_coprod_inr_rightDistrib_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalRightDistrib C]
  {X Y Z Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inr X)
      (CategoryTheory.CategoryStruct.comp (∂R X Y Z).inv h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj W
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).inv
        Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator W X
              (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
        h)
-- Mathlib.GroupTheory.Finiteness
AddGroup.fg_of_surjective : ∀ {G : Type u_3} [inst : AddGroup G] {G' : Type u_5} [inst_1 : AddGroup G'] [hG : AddGroup.FG G] {f : G →+ G'},
  Function.Surjective ⇑f → AddGroup.FG G'
-- Mathlib.Analysis.SumIntegralComparisons
integral_le_sum_Ico_of_le : ∀ {a b : ℕ} {f g : ℝ → ℝ},
  a ≤ b →
    (∀ i ∈ Set.Ico a b, ∀ x ∈ Set.Ico ↑i ↑(i + 1), g x ≤ f ↑i) →
      MeasureTheory.IntegrableOn g (Set.Ico ↑a ↑b) MeasureTheory.volume →
        ∫ (x : ℝ) in ↑a..↑b, g x ≤ ∑ i ∈ Finset.Ico a b, f ↑i
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Icc_right_eq_Icc_add_one : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {a b : α},
  a ≤ b + 1 → insert (b + 1) (Set.Icc a b) = Set.Icc a (b + 1)
-- Mathlib.Order.Minimal
OrderEmbedding.minimal_mem_image_iff : ∀ {α : Type u_2} {β : Type u_3} {a : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α ↪o β},
  a ∈ s → (Minimal (fun x => x ∈ ⇑f '' s) (f a) ↔ Minimal (fun x => x ∈ s) a)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g f) h
-- Mathlib.CategoryTheory.Comma.Over.OverClass
/-- Bundle `X` with an `OverClass X S` instance into `Over S`.  -/
CategoryTheory.OverClass.asOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (X S : C) → [CategoryTheory.OverClass X S] → CategoryTheory.Over S
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.liftH.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0),
  h.liftH k hk = CategoryTheory.CategoryStruct.comp (h.liftK k hk) h.π
-- Std.Async.System
Std.Async.System.instReprEnvironment : Repr Std.Async.System.Environment
-- Init.Data.String.Decode
String.utf8EncodeChar_eq_cons_cons : ∀ {c : Char},
  c.utf8Size = 2 → String.utf8EncodeChar c = [(c.val >>> 6).toUInt8 &&& 31 ||| 192, c.val.toUInt8 &&& 63 ||| 128]
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.offset_eq_rawEndPos : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ : String}, p.Splits t₁ t₂ → p.offset = t₁.rawEndPos
-- Mathlib.Algebra.Lie.Abelian
LieSubalgebra.isLieAbelian_lieSpan_iff : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {s : Set L},
  IsLieAbelian ↥(LieSubalgebra.lieSpan R L s) ↔ ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
-- Mathlib.LinearAlgebra.Dimension.Finrank
Module.finrank_lt_of_rank_lt : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
  Module.rank R M < ↑n → Module.finrank R M < n
-- Mathlib.NumberTheory.LucasLehmer
/-- **Alias** of `LucasLehmer.norm_num_ext.sModNatAux`.

---

Generalization of `sModNat` with arbitrary base case,
useful for proving `sModNatTR` and `sModNat` agree.
 -/
LucasLehmer.norm_num_ext.sModNat_aux : ℕ → ℕ → ℕ → ℕ
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.Context.zetaDelta : Lean.Meta.Sym.UnifyM.Context✝ → Bool
-- Mathlib.Algebra.Order.Nonneg.Lattice
Nonneg.semilatticeInf : {α : Type u_1} → [inst : SemilatticeInf α] → {a : α} → SemilatticeInf { x // a ≤ x }
-- Std.Http.Data.Version
Std.Http.Version.ofNat : ℕ → Std.Http.Version
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.sub_iff_left : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a₁ a₂ b₁ b₂ : G},
  a₁ ≡ b₁ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p])
-- Mathlib.Analysis.Meromorphic.Order
/-- **Alias** of `MeromorphicOn.codiscreteWithin_setOfPred_meromorphicOrderAt_eq_zero_or_top`.

---

Variant of `codiscrete_setOfPred_meromorphicOrderAt_eq_zero_or_top`: The set where a meromorphic
function has zero or infinite order is codiscrete within its domain of meromorphicity.
 -/
MeromorphicOn.codiscreteWithin_setOf_meromorphicOrderAt_eq_zero_or_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U →
    (∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤) →
      {u | u ∈ U ∧ (meromorphicOrderAt f u = 0 ∨ meromorphicOrderAt f u = ⊤)} ∈ Filter.codiscreteWithin U
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_union : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s t : Set M),
  Submodule.span R (s ∪ t) = Submodule.span R s ⊔ Submodule.span R t
-- Std.Do.WP.Basic
Std.Do.Except.instWP : {ε : Type u_1} → Std.Do.WP (Except ε) (Std.Do.PostShape.except ε Std.Do.PostShape.pure)
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.coe_mk : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R] (S : Subsemiring R)
  (h : ∀ {a : R}, a ∈ S.carrier → star a ∈ S.carrier), ↑{ toSubsemiring := S, star_mem' := h } = ↑S
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.surjective : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), Function.Surjective ⇑e
-- Mathlib.Data.Multiset.Defs
/-- If `p` is a decidable predicate,
so is the existence of an element in a multiset satisfying `p`.  -/
Multiset.decidableExistsMultiset : {α : Type u_1} → {m : Multiset α} → {p : α → Prop} → [DecidablePred p] → Decidable (∃ x ∈ m, p x)
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- The tactic syntax  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.TacticData.stx : Mathlib.Linter.Flexible.TacticData✝ → Lean.Syntax
-- Init.Grind.Interactive
/-- Performs a case-split on a logical connective, `match`-expression, `if-then-else`-expression,
or inductive predicate. The argument is an anchor referencing one of the case-split candidates
in the `grind` state. You can use `cases?` to select a specific candidate using a code action.
If multiple candidates match the anchor (e.g., they differ only in inaccessible variables),
an ordinal reference such as `#a56e/2` selects the second matching candidate.
 -/
Lean.Parser.Tactic.Grind.cases : Lean.ParserDescr
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_eq_of_natDegree_add_lt_left : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p + q).natDegree < p.natDegree → p.natDegree = q.natDegree
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.instIsComonHomInv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.ComonObj M] [inst_3 : CategoryTheory.ComonObj N] (f : M ⟶ N) [CategoryTheory.IsComonHom f]
  [inst_5 : CategoryTheory.IsIso f], CategoryTheory.IsComonHom (CategoryTheory.inv f)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
/-- The `DefaultClause` structure is primarily a list of literals. The additional field `nodupkey` is
included to ensure that `not_tautology` is provable (which is needed to prove `sat_of_insertRup`
and `sat_of_insertRat` in `LRAT.Formula.Internal.RupAddSound` and `LRAT.Formula.Internal.RatAddSound`).
The additional field `nodup` is included to ensure that `delete` can be implemented by simply calling
`erase` on the `clause` field. Without `nodup`, it would be necessary to iterate through the entire
`clause` field and erase all instances of the literal to be deleted, since there would potentially
be more than one.

In principle, one could combine `nodupkey` and `nodup` to instead have one additional field that
stipulates that `∀ l1 : PosFin numVarsSucc, ∀ l2 : PosFin numVarsSucc, l1.1 ≠ l2.1`. This would work
just as well, and the only reason that `DefaultClause` is structured in this manner is that the
`nodup` field was only included in a later stage of the verification process when it became clear
that it was needed.
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause : ℕ → Type
-- Lean.Elab.Tactic.Simp
/-- User options. Registering a global option `tactic.simp.user.myOption` enables the tactic
configurations `(user.myOption := ...)` and `+user.myOption`.  -/
Lean.Meta.Simp.ConfigWithOptions.userConfig : Lean.Meta.Simp.ConfigWithOptions → Lean.Options
-- Lean.Meta.Basic
Lean.Meta.getConfig : Lean.MetaM Lean.Meta.Config
-- Mathlib.Algebra.Category.Grp.Limits
/-- A choice of limit cone for a functor into `GrpCat`.
(Generally, you'll just want to use `limit F`.)  -/
AddGrpCat.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddGrpCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections] → CategoryTheory.Limits.Cone F
-- Mathlib.Analysis.Complex.AbelLimit
_private.Mathlib.Analysis.Complex.AbelLimit.0.Complex.stolzCone_subset_stolzSet_aux' : ∀ (s : ℝ),
  ∃ M ε, 0 < M ∧ 0 < ε ∧ ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.instInhabited : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h₁ : S₁.LeftHomologyData) →
            (h₂ : S₂.LeftHomologyData) → Inhabited (CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Function.Injective.hasProd_comap_iff_of_hasSupport : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} {f : β → α} {a : α} [L.HasSupport] {g : γ → β} (hg : Function.Injective g),
  (∀ x ∈ L.support, x ∉ Set.range g → f x = 1) →
    (HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L)
-- Mathlib.Data.Finset.Basic
Finset.filter_singleton : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (a : α), Finset.filter p {a} = if p a then {a} else ∅
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.IsPos.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b b_1 : P.Base),
  b = b_1 → ∀ [inst_5 : CharZero R] (i i_1 : ι), i = i_1 → b.IsPos i = b_1.IsPos i_1
-- Batteries.Data.List.Lemmas
List.findIdxs_singleton : ∀ {α : Type u_1} {x : α} {p : α → Bool} {s : ℕ}, List.findIdxs p [x] s = if p x = true then [s] else []
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.Context.mk.sizeOf_spec : ∀ (mainGoalDischarger : Lean.MVarId → Lean.MetaM Bool) (sideGoalDischarger : Lean.MVarId → Lean.MetaM Unit),
  sizeOf { mainGoalDischarger := mainGoalDischarger, sideGoalDischarger := sideGoalDischarger } = 1
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.symm_apply_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) (v : V), φ.symm (φ v) = v
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.denote.match_1.splitter : (motive : Int.Internal.Linear.Poly → Sort u_1) →
  (p : Int.Internal.Linear.Poly) →
    ((k : ℤ) → motive (Int.Internal.Linear.Poly.num k)) →
      ((k : ℤ) →
          (v : Int.Internal.Linear.Var) →
            (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.add k v p)) →
        motive p
-- Init.Data.Nat.Lemmas
Nat.left_eq_add : ∀ {a b : ℕ}, a = a + b ↔ b = 0
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
CategoryTheory.isNoetherianObject_iff_not_strictMono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.IsNoetherianObject X ↔ ∀ (f : ℕ → CategoryTheory.Subobject X), ¬StrictMono f
-- Batteries.Tactic.PrintDependents
/-- The command `#print dependents X Y` prints a list of all the declarations in the file that
transitively depend on `X` or `Y`. After each declaration, it shows the list of all declarations
referred to directly in the body which also depend on `X` or `Y`.

For example, `#print axioms bar'` below shows that `bar'` depends on `Classical.choice`, but not
why. `#print dependents Classical.choice` says that `bar'` depends on `Classical.choice` because
it uses `foo` and `foo` uses `Classical.em`. `bar` is not listed because it is proved without using
`Classical.choice`.
```
import Batteries.Tactic.PrintDependents

theorem foo : x = y ∨ x ≠ y := Classical.em _
theorem bar : 1 = 1 ∨ 1 ≠ 1 := by simp
theorem bar' : 1 = 1 ∨ 1 ≠ 1 := foo

#print axioms bar'
-- 'bar'' depends on axioms: [Classical.choice, Quot.sound, propext]

#print dependents Classical.choice
-- foo: Classical.em
-- bar': foo
```

 -/
Batteries.Tactic.«command#printDependents___» : Lean.ParserDescr
-- Mathlib.Order.Basic
eq_of_forall_ge_iff : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, (∀ (c : α), a ≤ c ↔ b ≤ c) → a = b
-- Mathlib.Data.Setoid.Partition
/-- Defining a partial order on partitions as the partial order on their induced
equivalence relations.  -/
Setoid.Partition.partialOrder : {α : Type u_1} → PartialOrder (Setoid.Partitions α)
-- Mathlib.Algebra.Algebra.StrictPositivity
IsStrictlyPositive.iff_of_unital : ∀ {A : Type u_1} [inst : LE A] [inst_1 : Monoid A] [inst_2 : Zero A] {a : A}, IsStrictlyPositive a ↔ 0 ≤ a ∧ IsUnit a
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The norm is submultiplicative.  -/
NonUnitalNormedRing.norm_mul_le : ∀ {α : Type u_5} [self : NonUnitalNormedRing α] (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasRightCalculusOfFractions] {X Y : C} (φ : W.LeftFraction X Y),
  CategoryTheory.CategoryStruct.comp φ.rightFraction.s φ.f = CategoryTheory.CategoryStruct.comp φ.rightFraction.f φ.s
-- Mathlib.Topology.Subpath
/-- Concatenating one path `F 0` is homotopic to that path.  -/
Path.Homotopic.concat_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] (p : Fin 2 → X) (F : (k : Fin 1) → Path (p k.castSucc) (p k.succ)),
  (Path.concat p F).Homotopic (F 0)
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ico_consecutive : ∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ → M) {m n k : ℕ},
  m ≤ n → n ≤ k → ∑ i ∈ Finset.Ico m n, f i + ∑ i ∈ Finset.Ico n k, f i = ∑ i ∈ Finset.Ico m k, f i
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- Deleting a non-bridge edge from a connected graph preserves connectedness.  -/
SimpleGraph.Connected.connected_delete_edge_of_not_isBridge : ∀ {V : Type u} {G : SimpleGraph V}, G.Connected → ∀ {x y : V}, ¬G.IsBridge s(x, y) → (G.deleteEdges {s(x, y)}).Connected
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ZeroExtend
Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (aig : Std.Sat.AIG α) →
        (w : ℕ) →
          aig.RefVec w → (newWidth curr : ℕ) → curr ≤ newWidth → aig.RefVec curr → Std.Sat.AIG.RefVecEntry α newWidth
-- Std.Time.Format.Modifier
/-- `ZoneId` represents different time zone ID formats based on the number of pattern letters.
 -/
Std.Time.ZoneId : Type
-- Mathlib.RingTheory.Multiplicity
emultiplicity_ne_zero : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, emultiplicity a b ≠ 0 ↔ a ∣ b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_modify : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] (h : (↑m).WF) {k k' : α} {f : β k → β k} (hc : (m.modify k f).contains k' = true),
  (m.modify k f).get k' hc = if heq : (k == k') = true then cast ⋯ (f (m.get k ⋯)) else m.get k' ⋯
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The condition of being a pointwise left Kan extension at an object `Y` is
unchanged by replacing `Y` by an isomorphic object `Y'`.  -/
CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtOfIso' : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                (E : L.LeftExtension F) →
                  {Y : D} → E.IsPointwiseLeftKanExtensionAt Y → {Y' : D} → (Y ≅ Y') → E.IsPointwiseLeftKanExtensionAt Y'
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.AuxGluingStruct.mk.injEq : ∀ {A : Type} [inst : MetricSpace A] (Space : Type) (metric : MetricSpace Space) (embed : A → Space)
  (isom : Isometry embed) (Space_1 : Type) (metric_1 : MetricSpace Space_1) (embed_1 : A → Space_1)
  (isom_1 : Isometry embed_1),
  ({ Space := Space, metric := metric, embed := embed, isom := isom } =
      { Space := Space_1, metric := metric_1, embed := embed_1, isom := isom_1 }) =
    (Space = Space_1 ∧ metric ≍ metric_1 ∧ embed ≍ embed_1)
-- Mathlib.Algebra.Group.Basic
mul_mul_mul_comm : ∀ {G : Type u_3} [inst : CommSemigroup G] (a b c d : G), a * b * (c * d) = a * c * (b * d)