mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux1.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option (Computation α))) → Sort u_2)
  (x : Option (Stream'.Seq1 (Option (Computation α)))) (h_1 : Unit → motive none)
  (h_2 : (S' : Stream'.Seq (Option (Computation α))) → motive (some (none, S')))
  (h_3 : (c : Computation α) → (S' : Stream'.Seq (Option (Computation α))) → motive (some (some c, S')))
  (S' : Stream'.Seq (Option (Computation α))),
  x = some (none, S') →
    (match x with
      | none => h_1 ()
      | some (none, S') => h_2 S'
      | some (some c, S') => h_3 c S') ≍
      h_2 S'
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.toEmoji : Aesop.SafeRulesResult → String
-- Mathlib.Data.Nat.Squarefree
Nat.minSqFacProp_div : ∀ (n : ℕ) {k : ℕ}, Nat.Prime k → k ∣ n → ¬k * k ∣ n → ∀ {o : Option ℕ}, (n / k).MinSqFacProp o → n.MinSqFacProp o
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.generateFrom_surjective : ∀ {X : Type u_1}, Function.Surjective DiffeologicalSpace.generateFrom
-- Lean.Meta.Tactic.Cases
_private.Lean.Meta.Tactic.Cases.0.Lean.Meta.mkEqAndProof : Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_le_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → ∀ {fallback : α}, (cmp (t.minKeyD fallback) k).isLE = true
-- Mathlib.Order.JordanHolder
/-- Two `CompositionSeries X`, `s₁` and `s₂` are equivalent if there is a bijection
`e : Fin s₁.length ≃ Fin s₂.length` such that for any `i`,
`Iso (s₁ i) (s₁ i.succ) (s₂ (e i), s₂ (e i.succ))`  -/
CompositionSeries.Equivalent : {X : Type u} → [inst : Lattice X] → [inst_1 : JordanHolderLattice X] → CompositionSeries X → CompositionSeries X → Prop
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans F G) {a : B} {a' : C}
  (f : G.obj a ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.id a)).hom f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.id a)) f).hom
        (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapId a) f))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (η.app a)) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom f)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv f)
          (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.id (G.obj a)) f).hom))
-- Mathlib.Control.Random
/-- Sample an element of this type from the provided generator.  -/
Random.random : {m : Type u → Type u_1} → {α : Type u} → [self : Random m α] → {g : Type} → [RandomGen g] → RandGT g m α
-- Mathlib.RingTheory.Extension.Presentation.Basic
_private.Mathlib.RingTheory.Extension.Presentation.Basic.0.Algebra.Presentation.aux_X : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ) (i : ι' ⊕ ι),
  (Algebra.Presentation.aux✝ Q P) (MvPolynomial.X i) = Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ P.val) i
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup.eq_1 : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup = inferInstance
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_contLinear_eq_linear : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P] [inst_11 : TopologicalSpace W] [inst_12 : IsTopologicalAddTorsor Q]
  (f : P →ᴬ[R] Q), ↑f.contLinear = (↑f).linear
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.to_subbox_aux : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I J : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  [CompleteSpace F],
  BoxIntegral.Integrable I l f vol →
    ∀ (hJ : J ≤ I),
      ∃ y,
        BoxIntegral.HasIntegral J l f vol y ∧
          Filter.Tendsto (BoxIntegral.integralSum f vol)
            (BoxIntegral.IntegrationParams.toFilteriUnion I (BoxIntegral.Prepartition.single I J hJ)) (nhds y)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.variation_transpose_eq_smul : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) [Nontrivial E] {C : NNReal},
  (∀ (x : E) (y : F), ‖(B x) y‖₊ = C * ‖x‖₊ * ‖y‖₊) → (μ.transpose B).variation = C • μ.variation
-- Lean.Elab.Tactic.RCases
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.instToMessageData : Lean.ToMessageData Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.Topology.ContinuousOn
Topology.IsInducing.continuousWithinAt_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {g : β → γ},
  Topology.IsInducing g → ∀ {s : Set α} {x : α}, ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x
-- Mathlib.Topology.Compactness.Paracompact
/-- The product of a compact space and a paracompact space is a paracompact space. The formalization
is based on https://dantopology.wordpress.com/2009/10/24/compact-x-paracompact-is-paracompact/
with some minor modifications.

This version assumes that `X` in `X × Y` is compact and `Y` is paracompact, see next lemma for the
other case.  -/
instParacompactSpaceProdOfCompactSpace : ∀ {X : Type v} {Y : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X]
  [ParacompactSpace Y], ParacompactSpace (X × Y)
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.max : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f g : α → ℝ} {Kf Kg : NNReal},
  LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (max Kf Kg) fun x => max (f x) (g x)
-- Init.Data.Order.PackageFactories
Std.PreorderPackage.mk : {α : Type u} →
  [toLE : LE α] →
    [toLT : LT α] →
      [toBEq : BEq α] →
        [toLawfulOrderLT : Std.LawfulOrderLT α] →
          [toLawfulOrderBEq : Std.LawfulOrderBEq α] →
            [toIsPreorder : Std.IsPreorder α] → DecidableLE α → DecidableLT α → Std.PreorderPackage α
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_of_getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {a a' : α}, m.WF → m.getKey? a = some a' → a' ∈ m
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If the action of a countable group `G` admits an invariant measure `μ` with a fundamental domain
`s`, then every null-measurable set `t` of measure strictly greater than `μ s` contains two
points `x y` such that `g • x = y` for some `g ≠ 1`.  -/
MeasureTheory.IsFundamentalDomain.exists_ne_one_smul_eq : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ →
    MeasureTheory.NullMeasurableSet t μ → μ s < μ t → ∃ x ∈ t, ∃ y ∈ t, ∃ g, g ≠ 1 ∧ g • x = y
-- Mathlib.Logic.IsEmpty.Defs
instIsEmptyFalse : IsEmpty False
-- Mathlib.Topology.Instances.NNReal.Lemmas
ContinuousOn.ofReal_map_toNNReal : ∀ {f : NNReal → NNReal} {s : Set ℝ} {t : Set NNReal},
  ContinuousOn f t → Set.MapsTo Real.toNNReal s t → ContinuousOn (fun x => ↑(f x.toNNReal)) s
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewFact.eq.injEq : ∀ (lhs rhs proof : Lean.Expr) (isHEq : Bool) (lhs_1 rhs_1 proof_1 : Lean.Expr) (isHEq_1 : Bool),
  (Lean.Meta.Grind.NewFact.eq lhs rhs proof isHEq = Lean.Meta.Grind.NewFact.eq lhs_1 rhs_1 proof_1 isHEq_1) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1 ∧ isHEq = isHEq_1)
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.inv_inv_add_inv : ∀ {p q r : ℝ}, p.HolderTriple q r → (p⁻¹ + q⁻¹)⁻¹ = r
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint submodules, then there is the natural isomorphism
`M ⊗[R] N ≃ₗ[R] M * N` induced by multiplication in `S`.  -/
Submodule.LinearDisjoint.mulMap : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] → {M N : Submodule R S} → M.LinearDisjoint N → TensorProduct R ↥M ↥N ≃ₗ[R] ↥(M * N)
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
_private.Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties.0.AlgebraicGeometry.HasRingHomProperty.respects_isOpenImmersion_aux : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q],
  (RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q) →
    ∀ {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U),
      P f → P (CategoryTheory.CategoryStruct.comp f U.ι)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic absolute value function on `K` defined as `b` raised to negative `v`-adic
valuation, for some `b` in `ℝ≥0`  -/
IsDedekindDomain.HeightOneSpectrum.adicAbvDef : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      {K : Type u_2} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [IsFractionRing R K] → IsDedekindDomain.HeightOneSpectrum R → {b : NNReal} → 1 < b → K → NNReal
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- Ultrametric inequality with `Finset.sum`.  -/
IsNonarchimedean.apply_sum_le_sup : ∀ {R : Type u_1} [inst : LinearOrder R] {α : Type u_2} {β : Type u_3} [inst_1 : AddCommMonoid α] {f : α → R},
  IsNonarchimedean f →
    ∀ {s : Finset β} (hnonempty : s.Nonempty) {l : β → α}, f (∑ i ∈ s, l i) ≤ s.sup' hnonempty fun i => f (l i)
-- Mathlib.Data.FinEnum
FinEnum.Finset.mem_enum : ∀ {α : Type u} [inst : DecidableEq α] (s : Finset α) (xs : List α), s ∈ FinEnum.Finset.enum xs ↔ ∀ x ∈ s, x ∈ xs
-- Mathlib.Algebra.Group.Defs
AddZero.ext : ∀ {M : Type u_2} {x y : AddZero M}, Zero.zero = Zero.zero → Add.add = Add.add → x = y
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsAddCyclic.card_nsmulAddMonoidHom_range : ∀ (G : Type u_2) [inst : AddCommGroup G] [hG : IsAddCyclic G] [Finite G] (d : ℕ),
  Nat.card ↥(nsmulAddMonoidHom d).range = Nat.card G / (Nat.card G).gcd d
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_maxKey?_eq_not_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey?.isSome = !t.isEmpty
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β] (f : InfTopHom α β),
  f.comp (InfTopHom.id α) = f
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.over_iso_iff : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] (P : CategoryTheory.MorphismProperty T) [P.RespectsIso]
  {X : T} {f g : CategoryTheory.Over X} (e : f ≅ g), P f.hom ↔ P g.hom
-- Lean.EnvExtension
Lean.MapDeclarationExtension.mk : {α : Type} →
  Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α) → Lean.MapDeclarationExtension α
-- Init.Data.Char.Ordinal
Char.ofOrdinal_ordinal : ∀ {c : Char}, Char.ofOrdinal c.ordinal = c
-- Std.Net.Addr
Std.Net.instDecidableEqIPAddr : DecidableEq Std.Net.IPAddr
-- Init.Grind.AC
Lean.Grind.AC.eq_erase0_cert : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.Analysis.Quaternion
Quaternion.continuous_imJ : Continuous fun q => q.imJ
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
/-- The generating cofibrations: this is the family of morphisms in `SSet`
which consists of boundary inclusions `∂Δ[n].ι : ∂Δ[n] ⟶ Δ[n]`.  -/
SSet.modelCategoryQuillen.I : CategoryTheory.MorphismProperty SSet
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.diagnostics.threshold.proofSize : Lean.Option ℕ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  k ∉ m₂ → (m₁ ∩ m₂).get? k = none
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.keys_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} (h : t.WF),
  (Std.DTreeMap.Raw.filter f t).keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (Std.DTreeMap.Raw.Const.get t x ⋯))
        t.keys.attach).unattach
-- Mathlib.Computability.Partrec
Computable.comp : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : β → σ} {g : α → β}, Computable f → Computable g → Computable fun a => f (g a)
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.mem_vaddAntidiagonal : ∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] {s : Set G} {t : Set P} (a : P) (h : (s.vaddAntidiagonal t a).Finite)
  {x : G × P}, x ∈ Finset.VAddAntidiagonal a h ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 +ᵥ x.2 = a
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.lanLift.congr_simp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f f_1 : b ⟶ a) (e_f : f = f_1) (g g_1 : c ⟶ a)
  (e_g : g = g_1) [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g],
  CategoryTheory.Bicategory.lanLift f g = CategoryTheory.Bicategory.lanLift f_1 g_1
-- Mathlib.Data.List.Zip
List.zipWith3_same_right : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → β → γ) (la : List α) (lb : List β),
  List.zipWith3 f la lb lb = List.zipWith (fun a b => f a b b) la lb
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- `HasPullbacksAlong f` states that pullbacks of all morphisms into `Y`
along `f : X ⟶ Y` exist.  -/
CategoryTheory.Limits.HasPullbacksAlong : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → Prop
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getEntry? : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → Option ((a : α) × β a)
-- Mathlib.CategoryTheory.Whiskering
/-- Auxiliary definition for `whiskeringLeft₃`.  -/
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_4} →
        {D₂ : Type u_5} →
          {D₃ : Type u_6} →
            [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_4} D₁] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] →
                        (E : Type u_7) →
                          [inst_6 : CategoryTheory.Category.{v_7, u_7} E] →
                            CategoryTheory.Functor C₁ D₁ →
                              CategoryTheory.Functor C₂ D₂ →
                                CategoryTheory.Functor C₃ D₃ →
                                  CategoryTheory.Functor
                                    (CategoryTheory.Functor D₁
                                      (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)))
                                    (CategoryTheory.Functor C₁
                                      (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)))
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_sub : ∀ {A : Type u_3} {E : Type u_4} (x y : WithCStarModule A E) [inst : AddCommGroup E],
  (WithCStarModule.equiv A E) (x - y) = (WithCStarModule.equiv A E) x - (WithCStarModule.equiv A E) y
-- Mathlib.Tactic.Widget.LibraryRewrite
_private.Mathlib.Tactic.Widget.LibraryRewrite.0.Mathlib.Tactic.LibraryRewrite.instInhabitedExtState : Inhabited Mathlib.Tactic.LibraryRewrite.ExtState✝
-- Mathlib.Combinatorics.Matroid.Basic
/-- The `Indep`endent sets are those contained in `Base`s.  -/
Matroid.indep_iff' : ∀ {α : Type u_1} (self : Matroid α) ⦃I : Set α⦄, self.Indep I ↔ ∃ B, self.IsBase B ∧ I ⊆ B
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_eq_get_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} {h : k ∈ t},
  t.get k h = (t.get? k).get ⋯
-- Mathlib.Tactic.Widget.CommDiag
/-- Square with `homs = [f,g,h,i]` and `objs = [A,B,C,D]`
```
A f B
i   g
D h C
```
 -/
Mathlib.Tactic.Widget.subSquare : String
-- Init.Sym.Lemmas
Lean.Sym.Nat.le_eq_true : ∀ (a b : ℕ), decide (a ≤ b) = true → (a ≤ b) = True
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectL_map : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (c : C)
  {X Y : B} (a : X ⟶ Y),
  (CategoryTheory.Bicategory.Prod.sectL B c).map a = CategoryTheory.Prod.mkHom a (CategoryTheory.CategoryStruct.id c)
-- Mathlib.Topology.Connected.PathConnected
Joined.add : ∀ {M : Type u_4} [inst : Add M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {a b c d : M},
  Joined a b → Joined c d → Joined (a + c) (b + d)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_inter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        (m₁.inter! m₂).getKey? k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then m₁.getKey? k else none
-- Mathlib.Topology.Category.CompHaus.Basic
CompHaus.instT2SpaceCarrierToTopTrue : ∀ {X : CompHaus}, T2Space ↑X.toTop
-- Init.Data.SInt.Bitwise
ISize.xor_eq_zero_iff : ∀ {a b : ISize}, a ^^^ b = 0 ↔ a = b
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.yoneda_ℐ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Limits.IndObjectPresentation.yoneda X).ℐ = CategoryTheory.discreteCategory PUnit.{v + 1}
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- Auxiliary function for `trans_assoc_reparam`.  -/
Path.Homotopy.transAssocReparamAux : ↑unitInterval → ℝ
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating that there is a \(longest\) match ending at the given position.
 -/
String.Slice.Pattern.Model.RevMatchesAt : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → {s : String.Slice} → s.Pos → Prop
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toArray_roo : ∀ {m n fallback : ℤ} {i : ℕ},
  (m<...n).toArray.getD i fallback = if i < (n - (m + 1)).toNat then m + 1 + ↑i else fallback
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- An additive submonoid contains `0`.  -/
Subsemiring.zero_mem' : ∀ {R : Type u} [inst : NonAssocSemiring R] (self : Subsemiring R), 0 ∈ self.carrier
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instDefinable₂Insert : ZFSet.Definable₂ insert
-- Mathlib.Data.Set.Lattice
Antitone.iInter_nat_add : ∀ {α : Type u_1} {f : ℕ → Set α}, Antitone f → ∀ (k : ℕ), ⋂ n, f (n + k) = ⋂ n, f n
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Result.mk.sizeOf_spec : ∀ (expr : Lean.Expr) (proof? : Option Lean.Expr) (cache : Bool),
  sizeOf { expr := expr, proof? := proof?, cache := cache } = 1 + sizeOf expr + sizeOf proof? + sizeOf cache
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.sylvesterMap_apply_coe : ∀ {m n : ℕ} {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n)
  (pq : ↥(Polynomial.degreeLT R m) × ↥(Polynomial.degreeLT R n)), ↑((f.sylvesterMap g hf hg) pq) = f * ↑pq.2 + g * ↑pq.1
-- Mathlib.GroupTheory.Coset.Basic
mem_rightAddCoset : ∀ {α : Type u_1} [inst : Add α] {s : Set α} {x : α} (a : α), x ∈ s → x + a ∈ AddOpposite.op a +ᵥ s
-- Init.Data.String.Decode
Char.utf8Size_eq_two_iff : ∀ {c : Char}, c.utf8Size = 2 ↔ 127 < c.val ∧ c.val ≤ 2047
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.mk.injEq : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} (toFun : ι → C(X, ℝ))
  (locallyFinite' : LocallyFinite fun i => Function.support ⇑(toFun i)) (nonneg' : 0 ≤ toFun)
  (sum_eq_one' : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun i) x = 1) (sum_le_one' : ∀ (x : X), ∑ᶠ (i : ι), (toFun i) x ≤ 1)
  (toFun_1 : ι → C(X, ℝ)) (locallyFinite'_1 : LocallyFinite fun i => Function.support ⇑(toFun_1 i))
  (nonneg'_1 : 0 ≤ toFun_1) (sum_eq_one'_1 : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun_1 i) x = 1)
  (sum_le_one'_1 : ∀ (x : X), ∑ᶠ (i : ι), (toFun_1 i) x ≤ 1),
  ({ toFun := toFun, locallyFinite' := locallyFinite', nonneg' := nonneg', sum_eq_one' := sum_eq_one',
        sum_le_one' := sum_le_one' } =
      { toFun := toFun_1, locallyFinite' := locallyFinite'_1, nonneg' := nonneg'_1, sum_eq_one' := sum_eq_one'_1,
        sum_le_one' := sum_le_one'_1 }) =
    (toFun = toFun_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k} {h₁ : a ∈ m.insertIfNew k v},
  (m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ k ∉ m then k else m.getKey a ⋯
-- Mathlib.Order.WithBot
Equiv.withTopCongr_refl : ∀ {α : Type u_1}, (Equiv.refl α).withTopCongr = Equiv.refl (WithTop α)
-- Init.Data.Dyadic.Basic
Dyadic.ofOdd_eq_ofIntWithPrec : ∀ {n k : ℤ} {hn : n % 2 = 1}, Dyadic.ofOdd n k hn = Dyadic.ofIntWithPrec n k
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.polar_prod : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (x y : M₁ × M₂),
  QuadraticMap.polar (⇑(Q₁.prod Q₂)) x y = QuadraticMap.polar (⇑Q₁) x.1 y.1 + QuadraticMap.polar (⇑Q₂) x.2 y.2
-- Init.Data.String.Slice
String.Slice.instInhabitedSplitInclusiveIterator : {a : String.Slice → Type} →
  {a_1 : Type} →
    {a_2 : a_1} →
      {a_3 : String.Slice} →
        {a_4 : String.Slice.Pattern.ToForwardSearcher a_2 a} → Inhabited (String.Slice.SplitInclusiveIterator a_2 a_3)
-- Mathlib.Analysis.SpecificLimits.Normed
/-- The series `∑' n, x ^ n / n!` is summable of any `x : ℝ`. See also `expSeries_div_summable`
for a version that also works in `ℂ`, and `NormedSpace.expSeries_summable'` for a version
that works in any normed algebra over `ℝ` or `ℂ`.  -/
Real.summable_pow_div_factorial : ∀ (x : ℝ), Summable fun n => x ^ n / ↑n.factorial