mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
/-- The counit isomorphism of the equivalence
`Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c`.  -/
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse.comp
              CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor ≅
            CategoryTheory.Functor.id (HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c)
-- Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
/-- The `G`-action on `X` is proper iff, for each pair of compacts `U, V` in `X`,
the set of `g` such that `U` intersects `g +ᵥ V` is compact.

See `ProperVAdd.isCompact_setOfPred_inter_nonempty`
for a one-way implication with fewer conditions.

**Note**: We assume `CompactlyCoherentSpace (X × X)`
as this is the minimal assumption needed to make the proof work;
but this follows from various more familiar conditions,
such as `FirstCountableTopology X`.
Importing `Mathlib.Topology.Sequences` makes this implication available.
 -/
AddAction.properVAdd_iff_isCompact_setOfPred_inter_nonempty : ∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  [inst_3 : AddAction G X] [CompactlyGeneratedSpace (X × X)] [T2Space X] [ContinuousVAdd G X],
  ProperVAdd G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | ((g +ᵥ U) ∩ V).Nonempty}
-- Init.Data.String.Slice
/-- Rewinds `pos` as long as `pat` matches.
 -/
String.Slice.Pos.revSkipWhile : {ρ : Type} → {s : String.Slice} → s.Pos → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → s.Pos
-- Mathlib.Algebra.Ring.Parity
Nat.odd_mul : ∀ {m n : ℕ}, Odd (m * n) ↔ Odd m ∧ Odd n
-- Mathlib.Algebra.Ring.Defs
Ring.toSemiring : {R : Type u} → [self : Ring R] → Semiring R
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_mk : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (x : G) (hx : x ∈ H), ↑⟨x, hx⟩ = x
-- Init.Data.List.Attach
List.pmap_append : ∀ {ι : Type u_1} {α : Type u_2} {p : ι → Prop} {f : (a : ι) → p a → α} {l₁ l₂ : List ι} (h : ∀ a ∈ l₁ ++ l₂, p a),
  List.pmap f (l₁ ++ l₂) h = List.pmap f l₁ ⋯ ++ List.pmap f l₂ ⋯
-- Mathlib.AlgebraicGeometry.Sites.BigZariski
AlgebraicGeometry.Scheme.subcanonical_zariskiTopology : AlgebraicGeometry.Scheme.zariskiTopology.Subcanonical
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.instIsSchemeTheoreticallyDominantCompScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsSchemeTheoreticallyDominant f]
  [AlgebraicGeometry.IsSchemeTheoreticallyDominant g],
  AlgebraicGeometry.IsSchemeTheoreticallyDominant (CategoryTheory.CategoryStruct.comp f g)
-- Lean.Parser.Do
Lean.Parser.Term.doMatchExprAlts : Lean.Parser.Parser
-- Mathlib.Topology.Compactness.LocallyCompact
/-- For spaces that are not Hausdorff.  -/
Pi.locallyCompactSpace : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LocallyCompactSpace (X i)]
  [∀ (i : ι), CompactSpace (X i)], LocallyCompactSpace ((i : ι) → X i)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
ComplexShape.Embedding.truncGE'Functor_obj : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsTruncGE]
  (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c'),
  (e.truncGE'Functor C).obj K = K.truncGE' e
-- Mathlib.CategoryTheory.Adjunction.Restrict
CategoryTheory.Adjunction.restrictFullyFaithful.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'}
  {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful)
  (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
  (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC),
  adj.restrictFullyFaithful hiC hiD comm1 comm2 =
    CategoryTheory.Adjunction.mkOfHomEquiv
      {
        homEquiv := fun X Y =>
          Trans.trans
            (Trans.trans
              (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X).homCongr (CategoryTheory.Iso.refl (iD.obj Y))))
                (adj.homEquiv (iC.obj X) (iD.obj Y)))
              ((CategoryTheory.Iso.refl (iC.obj X)).homCongr (comm2.app Y)))
            hiC.homEquiv.symm,
        homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }
-- Mathlib.GroupTheory.Perm.Fin
Equiv.Perm.decomposeFin_symm_of_refl : ∀ {n : ℕ} (p : Fin (n + 1)), Equiv.Perm.decomposeFin.symm (p, Equiv.refl (Fin n)) = Equiv.swap 0 p
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry!_eq_get!_maxEntry? : ∀ {α : Type u} {β : Type v} [Ord α] {l : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Inhabited (α × β)],
  Std.DTreeMap.Internal.Impl.Const.maxEntry! l = (Std.DTreeMap.Internal.Impl.Const.maxEntry? l).get!
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_quot_le : ∀ {α : Type u} {r : α → α → Prop}, Cardinal.mk (Quot r) ≤ Cardinal.mk α
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement'.disjoint : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsComplement' K → Disjoint H K
-- Init.Data.UInt.Bitwise
Bool.toBitVec_toUInt16 : ∀ {b : Bool}, b.toUInt16.toBitVec = BitVec.setWidth 16 (BitVec.ofBool b)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofDiseqSplit.inj : ∀ {c₁ : Lean.Meta.Grind.Arith.Linear.DiseqCnstr} {decVar : Lean.FVarId} {h : Lean.Meta.Grind.Arith.Linear.UnsatProof}
  {decVars : Array Lean.FVarId} {c₁_1 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr} {decVar_1 : Lean.FVarId}
  {h_1 : Lean.Meta.Grind.Arith.Linear.UnsatProof} {decVars_1 : Array Lean.FVarId},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofDiseqSplit c₁ decVar h decVars =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofDiseqSplit c₁_1 decVar_1 h_1 decVars_1 →
    c₁ = c₁_1 ∧ decVar = decVar_1 ∧ h = h_1 ∧ decVars = decVars_1
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.injective_sum_to : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2), Function.Injective (Profinite.NobelingProof.GoodProducts.sum_to C ho)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_iter : ∀ {n : Type (max u_1 u_2) → Type u_3} {ps : Std.Do.PostShape} [inst : Monad n] [inst_1 : Std.Do.WPMonad n ps]
  {α β : Type u_2} {γ : Type (max u_1 u_2)} [inst_2 : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {init : γ} {f : β → γ → n (ForInStep γ)}
  {it : Std.Iter β} (inv : Std.Do.Invariant it.toList γ ps),
  (∀ (pref : List β) (cur : β) (suff : List β) (h : it.toList = pref ++ cur :: suff) (b : γ),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := it.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := it.toList, property := ⋯ }, init)⦄
      forIn it init f ⦃(fun b => inv.1 ({ «prefix» := it.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_sub_le : ∀ {R : Type u} [inst : Ring R] (p q : Polynomial R), (p - q).natDegree ≤ max p.natDegree q.natDegree
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_one : ∀ {n : ℕ} [inst : NeZero n], Fin.castPred 1 ⋯ = 1
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_union_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {b c d : α}, min c d < b → Set.Iio b ∪ Set.Ioo c d = Set.Iio (max b d)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasOfPostcompPropertyUnopOfHasOfPrecompPropertyOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W₁ W₂ : CategoryTheory.MorphismProperty Cᵒᵖ)
  [W₁.HasOfPrecompProperty W₂], W₁.unop.HasOfPostcompProperty W₂.unop
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.toPermHom_apply_toCentralizer : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)),
  (Equiv.Perm.OnCycleFactors.toPermHom g) (a.toCentralizer τ) = ↑τ
-- Init.Data.AC
Lean.Data.AC.Context.op : {α : Sort u} → Lean.Data.AC.Context α → α → α → α
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The cosine of an angle in a right-angled triangle as a ratio of sides.  -/
Orientation.cos_oangle_add_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle x (x + y)).cos = ‖x‖ / ‖x + y‖
-- Lean.Widget.UserWidget
_private.Lean.Widget.UserWidget.0.Lean.Widget.evalModuleUnsafe : Lean.Expr → Lean.MetaM Lean.Widget.Module
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Composing on the right by a function preserves uniform convergence  -/
TendstoUniformly.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β}
  {p : Filter ι}, TendstoUniformly F f p → ∀ (g : γ → α), TendstoUniformly (fun n => F n ∘ g) (f ∘ g) p
-- Mathlib.Algebra.CharP.Defs
/-- The characteristic equals the exponential characteristic iff the former is prime.  -/
char_eq_expChar_iff : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p q : ℕ) [hp : CharP R p] [hq : ExpChar R q], p = q ↔ Nat.Prime p
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
/-- Helper definition to prove `balanced_core_eq_iInter`  -/
balancedCoreAux : (𝕜 : Type u_1) → {E : Type u_2} → [SeminormedRing 𝕜] → [SMul 𝕜 E] → Set E → Set E
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.mk.inj : ∀ {α : Type u_5} {β : Type u_6} {inst : NonUnitalNonAssocSemiring α} {inst_1 : NonUnitalNonAssocSemiring β}
  {toMulHom : α →ₙ* β} {map_zero' : toMulHom.toFun 0 = 0}
  {map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y} {toMulHom_1 : α →ₙ* β}
  {map_zero'_1 : toMulHom_1.toFun 0 = 0}
  {map_add'_1 : ∀ (x y : α), toMulHom_1.toFun (x + y) = toMulHom_1.toFun x + toMulHom_1.toFun y},
  { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' } =
      { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 } →
    toMulHom = toMulHom_1
-- Mathlib.Order.Lattice
pairwise_iff_lt : ∀ {α : Type u} [inst : LinearOrder α] {p : α → α → Prop} [Std.Symm p], Pairwise p ↔ ∀ ⦃a b : α⦄, a < b → p a b
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_symm_of : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] {i : ι} (x : ↥(ℳ i)),
  (DirectSum.decompose ℳ).symm ((DirectSum.of (fun i => ↥(ℳ i)) i) x) = ↑x
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddMonoid α],
  Lex.instAddMonoid =
    { toAddSemigroup := Lex.instAddSemigroup, toZero := Lex.instZero, zero_add := ⋯, add_zero := ⋯,
      toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.instReprWeekday.repr.match_1.eq_6 : ∀ (motive : Std.Time.Weekday → Sort u_1) (h_1 : Unit → motive Std.Time.Weekday.monday)
  (h_2 : Unit → motive Std.Time.Weekday.tuesday) (h_3 : Unit → motive Std.Time.Weekday.wednesday)
  (h_4 : Unit → motive Std.Time.Weekday.thursday) (h_5 : Unit → motive Std.Time.Weekday.friday)
  (h_6 : Unit → motive Std.Time.Weekday.saturday) (h_7 : Unit → motive Std.Time.Weekday.sunday),
  (match Std.Time.Weekday.saturday with
    | Std.Time.Weekday.monday => h_1 ()
    | Std.Time.Weekday.tuesday => h_2 ()
    | Std.Time.Weekday.wednesday => h_3 ()
    | Std.Time.Weekday.thursday => h_4 ()
    | Std.Time.Weekday.friday => h_5 ()
    | Std.Time.Weekday.saturday => h_6 ()
    | Std.Time.Weekday.sunday => h_7 ()) =
    h_6 ()
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedCtorView : Inhabited Lean.Elab.Command.CtorView
-- Mathlib.Algebra.Module.ZLattice.Basic
basisOfTopLeSpanOfCardEqFinrank.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : OrzechProperty R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {ι : Type u_3} [inst_4 : Fintype ι] (b b_1 : ι → M) (e_b : b = b_1)
  (le_span : ⊤ ≤ Submodule.span R (Set.range b)) (card_eq : Fintype.card ι = Module.finrank R M),
  basisOfTopLeSpanOfCardEqFinrank b le_span card_eq = basisOfTopLeSpanOfCardEqFinrank b_1 ⋯ card_eq
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.combineMinIdxOn_lt' : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) {xs ys : List α} (zs : List α)
  {i j : ℕ} (hi : i < xs.length) (hj : j < ys.length), zs = xs ++ ys → List.combineMinIdxOn✝ f i j hi hj < zs.length
-- Mathlib.Computability.Primrec.Basic
Primrec.id : ∀ {α : Type u_1} [inst : Primcodable α], Primrec id
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Localization.mk_zero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} (x : ↥S), Localization.mk 0 x = 0
-- Mathlib.NumberTheory.Padics.Complex
/-- The valuation of `x : PadicAlgCl p` agrees with its `ℝ≥0`-valued norm.  -/
PadicAlgCl.valuation_def : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p), Valued.v x = ‖x‖₊
-- Mathlib.Topology.Path
Path.trans.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X} (γ : Path x y) (γ' : Path y z),
  γ.trans γ' =
    { toFun := (fun t => if t ≤ 1 / 2 then γ.extend (2 * t) else γ'.extend (2 * t - 1)) ∘ Subtype.val,
      continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
isAddHaarMeasure_basis_addHaar : ∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (b : Module.Basis ι ℝ E), b.addHaar.IsAddHaarMeasure
-- Aesop.RuleSet.Name
Aesop.builtinRuleSetNames : Array Aesop.RuleSetName
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorem.getValue : Lean.Meta.SimpTheorem → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.paste_horiz_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃},
  CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂ →
    CategoryTheory.CategoryStruct.comp h₁₁ v₁₂ = CategoryTheory.CategoryStruct.comp v₁₁ h₂₁ →
      (CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃
          (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂) ↔
        CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁)
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The equivalence between `AddCircle p` and the quotient of `[a, a + p]` by the relation
identifying the endpoints.  -/
AddCircle.equivIccQuot : {𝕜 : Type u_1} →
  [inst : AddCommGroup 𝕜] →
    [inst_1 : LinearOrder 𝕜] →
      [inst_2 : IsOrderedAddMonoid 𝕜] →
        (p a : 𝕜) → [hp : Fact (0 < p)] → [Archimedean 𝕜] → AddCircle p ≃ Quot (AddCircle.EndpointIdent p a)
-- Mathlib.Analysis.Complex.Norm
/-- The limit of a Cauchy sequence of complex numbers.  -/
Complex.limAux : (CauSeq ℂ fun x => ‖x‖) → ℂ
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_comm : ∀ {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] (f : M → N) (x y : M),
  QuadraticMap.polar f x y = QuadraticMap.polar f y x
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.rel₂_of_left : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Std.Iterators.Productive α₁ m] [inst_3 : Std.Iterators.Finite α₂ m] {right : Std.IterM m β₂}
  {b b' : Option { out // ∃ it, it.IsPlausibleOutput out }} {it' it : Std.IterM m β₁},
  b' = b →
    it'.finitelyManySkips.Rel it.finitelyManySkips →
      Std.Iterators.Types.Zip.Rel₂ m { internalState := { left := it', memoizedLeft := b', right := right } }
        { internalState := { left := it, memoizedLeft := b, right := right } }
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsCompl_symm : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (hpq : IsCompl p q) {φ : ↥p →ₗ[R] F}
  {ψ : ↥q →ₗ[R] F}, LinearMap.ofIsCompl ⋯ ψ φ = LinearMap.ofIsCompl hpq φ ψ
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.completedLFunction_eq : ∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ) (s : ℂ),
  ZMod.completedLFunction Φ s = ZMod.completedLFunction₀ Φ s - ↑N ^ (-s) * Φ 0 / s - (↑N ^ (-s) * ∑ j, Φ j) / (1 - s)
-- Aesop.Tree.Data
Aesop.RappData.mk.sizeOf_spec : ∀ {Goal MVarCluster : Type} [inst : SizeOf Goal] [inst_1 : SizeOf MVarCluster] (id : Aesop.RappId)
  (parent : IO.Ref Goal) (children : Array (IO.Ref MVarCluster)) (state : Aesop.NodeState) (isIrrelevant : Bool)
  (appliedRule : Aesop.RegularRule) (scriptSteps? : Option (Array Aesop.Script.LazyStep))
  (originalSubgoals : Array Lean.MVarId) (successProbability : Aesop.Percent) (metaState : Lean.Meta.SavedState)
  (introducedMVars assignedMVars : Aesop.UnorderedArraySet Lean.MVarId),
  sizeOf
      { id := id, parent := parent, children := children, state := state, isIrrelevant := isIrrelevant,
        appliedRule := appliedRule, scriptSteps? := scriptSteps?, originalSubgoals := originalSubgoals,
        successProbability := successProbability, metaState := metaState, introducedMVars := introducedMVars,
        assignedMVars := assignedMVars } =
    1 + sizeOf id + sizeOf parent + sizeOf children + sizeOf state + sizeOf isIrrelevant + sizeOf appliedRule +
                sizeOf scriptSteps? +
              sizeOf originalSubgoals +
            sizeOf successProbability +
          sizeOf metaState +
        sizeOf introducedMVars +
      sizeOf assignedMVars
-- Init.Data.Int.DivMod.Pow
_private.Init.Data.Int.DivMod.Pow.0.Int.tdiv_pow : ∀ {a b : ℤ} {n : ℕ}, b ∣ a → a.tdiv b ^ n = (a ^ n).tdiv (b ^ n)
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
_private.Mathlib.Analysis.Convex.SpecificFunctions.Deriv.0.Nat.iterate.match_1.eq_1 : ∀ {α : Sort u_2} (motive : ℕ → α → Sort u_1) (a : α) (h_1 : (a : α) → motive 0 a)
  (h_2 : (k : ℕ) → (a : α) → motive k.succ a),
  (match 0, a with
    | 0, a => h_1 a
    | k.succ, a => h_2 k a) =
    h_1 a
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.compLpₗ_apply : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] (L : E →SL[σ] F)
  (f : ↥(MeasureTheory.Lp E p μ)), (ContinuousLinearMap.compLpₗ p μ L) f = L.compLp f
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Complex.betaIntegral.eq_1 : ∀ (u v : ℂ), u.betaIntegral v = ∫ (x : ℝ) in 0..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.forIn_filterMapWithPostcondition : ∀ {α : Type u₁} {n : Type u₁ → Type u_1} {o : Type u₁ → Type u_2} {β₂ γ : Type u₁} {m : Type u₁ → Type u_3}
  {β : Type u₁} {ps : Std.Do.PostShape} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n]
  [inst_4 : Monad o] [LawfulMonad o] [inst_6 : Std.Do.WPMonad o ps] [inst_7 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_9 : MonadLiftT n o] [LawfulMonadLiftT n o] [inst_11 : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_13 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β}
  {f : β → Std.Iterators.PostconditionT n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        match __do_lift with
          | some c => g c acc
          | none => pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.IterM.filterMapWithPostcondition f it) init g ⦃Q⦄
-- Mathlib.Probability.Kernel.Composition.RadonNikodym
/-- The Radon-Nikodym derivative `∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)` equals the product of `∂μ/∂ν` and
`∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η)`.  -/
ProbabilityTheory.rnDeriv_compProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ]
  [ProbabilityTheory.IsFiniteKernel η],
  (μ.compProd κ).AbsolutelyContinuous (μ.compProd η) →
    ∀ (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν],
      (μ.compProd κ).rnDeriv (ν.compProd η) =ᵐ[ν.compProd η] fun p =>
        μ.rnDeriv ν p.1 * (μ.compProd κ).rnDeriv (μ.compProd η) p
-- Mathlib.Topology.NoetherianSpace
/-- Type class for Noetherian spaces. It is defined to be spaces whose open sets satisfies ACC.  -/
TopologicalSpace.NoetherianSpace : (α : Type u_1) → [TopologicalSpace α] → Prop
-- Mathlib.Data.Set.Prod
Set.prod_preimage_right : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {s : Set α} {t : Set β} {g : δ → β},
  s ×ˢ (g ⁻¹' t) = (fun p => (p.1, g p.2)) ⁻¹' s ×ˢ t
-- Mathlib.Analysis.Convex.Slope
/-- If `f` is concave on a set `s` in a linearly ordered field, and `f y < f x` for two points
`x < y` in `s`, then `f` is strictly antitone on `s ∩ [y, ∞)`.  -/
ConcaveOn.strictAntiOn : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  ConcaveOn 𝕜 s f → ∀ {x y : 𝕜}, x ∈ s → x < y → f y < f x → StrictAntiOn f (s ∩ Set.Ici y)
-- Mathlib.Order.Bounds.OrderIso
OrderIso.upperBounds_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set α},
  upperBounds (⇑f '' s) = ⇑f '' upperBounds s
-- Mathlib.SetTheory.ZFC.Ordinal
/-- The union of a transitive set is transitive.  -/
ZFSet.IsTransitive.sUnion : ∀ {x : ZFSet.{u}}, x.IsTransitive → x.sUnion.IsTransitive
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLT_iff_pairwise`. -/
List.SortedLT.pairwise : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLT → List.Pairwise (fun x1 x2 => x1 < x2) l