mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.Fernique
/-- Auxiliary lemma for `lintegral_exp_mul_sq_norm_le_mul`, in which we find an upper bound on an
integral by dealing separately with the contribution of each set in a sequence of annuli.
This is the bound of the integral over one of those annuli.  -/
ProbabilityTheory.Fernique.lintegral_closedBall_sdiff_exp_logRatio_mul_sq_le : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    2⁻¹ < μ {x | ‖x‖ ≤ a} →
      μ {x | ‖x‖ ≤ a} < 1 →
        ∀ (n : ℕ),
          ∫⁻ (x : E) in
              Metric.closedBall 0 (ProbabilityTheory.Fernique.normThreshold a (n + 1)) \
                Metric.closedBall 0 (ProbabilityTheory.Fernique.normThreshold a n),
              ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio (μ {x | ‖x‖ ≤ a}) * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
            μ {x | ‖x‖ ≤ a} *
              ENNReal.ofReal (Real.exp (-2⁻¹ * Real.log (μ {x | ‖x‖ ≤ a} / (1 - μ {x | ‖x‖ ≤ a})).toReal * 2 ^ n))
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.coe_sup : ∀ {X : Type u_1} {R : Type u_2} [inst : AddZeroClass R] [inst_1 : SemilatticeSup R] [inst_2 : AddLeftMono R]
  [inst_3 : AddRightMono R] (d d' : PseudoMetric X R), ⇑(d ⊔ d') = ⇑d ⊔ ⇑d'
-- Init.Data.UInt.Bitwise
USize.toFin_xor : ∀ (a b : USize), (a ^^^ b).toFin = a.toFin ^^^ b.toFin
-- Mathlib.LinearAlgebra.TensorProduct.Pi
/-- Tensor product commutes with finite products on the right.  -/
TensorProduct.piRight : (R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (N : Type u_3) →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                [inst_5 : Module S N] →
                  [inst_6 : IsScalarTower R S N] →
                    {ι : Type u_4} →
                      (M : ι → Type u_5) →
                        [inst_7 : (i : ι) → AddCommMonoid (M i)] →
                          [inst_8 : (i : ι) → Module R (M i)] →
                            [Fintype ι] →
                              [DecidableEq ι] →
                                TensorProduct R N ((i : ι) → M i) ≃ₗ[S] (i : ι) → TensorProduct R N (M i)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.conj_apply_apply : ∀ {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [inst : CommSemiring R₁']
  [inst_1 : CommSemiring R₂'] [inst_2 : AddCommMonoid M₁'] [inst_3 : AddCommMonoid M₂'] [inst_4 : Module R₁' M₁']
  [inst_5 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [inst_6 : RingHomInvPair σ₁'₂' σ₂'₁']
  [inst_7 : RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₁' M₁') (x : M₂'),
  (e.conj f) x = e (f (e.symm x))
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
Mathlib.Tactic.ClickSuggestions.ApplyAtKey.mk.injEq : ∀ (numGoals nameLength replacementSize : ℕ) (name : String) (newGoals : Array Lean.Meta.AbstractMVarsResult)
  (numGoals_1 nameLength_1 replacementSize_1 : ℕ) (name_1 : String) (newGoals_1 : Array Lean.Meta.AbstractMVarsResult),
  ({ numGoals := numGoals, nameLength := nameLength, replacementSize := replacementSize, name := name,
        newGoals := newGoals } =
      { numGoals := numGoals_1, nameLength := nameLength_1, replacementSize := replacementSize_1, name := name_1,
        newGoals := newGoals_1 }) =
    (numGoals = numGoals_1 ∧
      nameLength = nameLength_1 ∧ replacementSize = replacementSize_1 ∧ name = name_1 ∧ newGoals = newGoals_1)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_perm : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') [inst_5 : DecidableEq ι]
  [inst_6 : Fintype ι] (v : ι → M) (σ : Equiv.Perm ι), g (v ∘ ⇑σ) = Equiv.Perm.sign σ • g v
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.SeparatingRight.eq_1 : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M), B.SeparatingRight = ∀ (y : M₂), (∀ (x : M₁), (B x) y = 0) → y = 0
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany_succ_eq_succ_succMany : ∀ {n : ℕ} {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {a : α},
  Std.PRange.succMany n (Std.PRange.succ a) = Std.PRange.succ (Std.PRange.succMany n a)
-- Mathlib.Analysis.RCLike.Basic
RCLike.im_eq_zero_iff_isSelfAdjoint : ∀ {K : Type u_1} [inst : RCLike K] {x : K}, RCLike.im x = 0 ↔ IsSelfAdjoint x
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Auxiliary definition to avoid looping in `dsimp`
with `Bundle.Trivialization.sourceHomeomorphBaseSetProd_symm_apply`.  -/
Bundle.Trivialization.sourceHomeomorphBaseSetProd_symm_apply.aux : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] → (e : Bundle.Trivialization F proj) → ↑e.baseSet × F ≃ₜ ↑e.source
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_injective_right : ∀ {α : Type u_1} [inst : DistribLattice α] (a : α), Function.Injective fun b => Set.uIcc b a
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.isOpen_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extend_pt : ∀ {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.Cone F) {X : C} (f : X ⟶ c.pt), (c.extend f).pt = X
-- Mathlib.Data.Nat.Count
Nat.count_lt_count_succ_iff : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, Nat.count p n < Nat.count p (n + 1) ↔ p n
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
MeasureTheory.condExp_stronglyMeasurable_bilin_of_bound : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G)
  [CompleteSpace E],
  m ≤ mΩ →
    ∀ [MeasureTheory.IsFiniteMeasure μ] {f : Ω → F} {g : Ω → E},
      MeasureTheory.StronglyMeasurable f →
        MeasureTheory.Integrable g μ →
          ∀ (c : ℝ), (∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c) → μ[fun ω => (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω => (B (f ω)) (μ[g | m] ω)
-- Mathlib.Tactic.Polynomial.Core
/-- Environment extensions for `polynomial` declarations  -/
Mathlib.Tactic.Polynomial.polynomialExt : Lean.PersistentEnvExtension Lean.Name (Lean.Name × Mathlib.Tactic.Polynomial.PolynomialExt)
  (List Lean.Name × List (Lean.Name × Mathlib.Tactic.Polynomial.PolynomialExt))
-- Mathlib.RingTheory.OreLocalization.Basic
/-- A characterization of the addition on the Ore localization, allowing for arbitrary Ore
numerator and Ore denominator.  -/
OreLocalization.oreDiv_add_char : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] {r r' : X} (s s' : ↥S) (rb : R) (sb : ↥S),
  ↑sb * ↑s = rb * ↑s' → r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ (sb * s)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_X : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  ¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.X✝ S
-- Mathlib.RingTheory.Spectrum.Prime.Topology
StableUnderGeneralization.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X),
  StableUnderGeneralization s = ∀ ⦃x y : X⦄, y ⤳ x → x ∈ s → y ∈ s
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.forIn_filterMapM : ∀ {α β β₂ γ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [inst_4 : Std.Internal.Do.Assertion Pred]
  [inst_5 : Std.Internal.Do.Assertion EPred] [inst_6 : Std.Internal.Do.WPMonad o Pred EPred] [inst_7 : MonadAttach n]
  [WeaklyLawfulMonadAttach n] [inst_9 : MonadLiftT n o] [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id]
  [inst_12 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β} {f : β → n (Option β₂)}
  {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out)
        match __do_lift with
          | some c => g c acc
          | none => pure (ForInStep.yield acc) ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.Iter.filterMapM f it) init g ⦃ Q; eQ ⦄
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.instHasHomotopyCofiberOfHasBinaryBiproducts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [CategoryTheory.Limits.HasBinaryBiproducts C],
  HomologicalComplex.HasHomotopyCofiber φ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).maxKey?.isSome = true
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Given a map `f : R →+* S` and an element `r : R`, we may construct a map `Rᵣ →+* Sᵣ`.  -/
IsLocalization.Away.map : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {P : Type u_3} →
            [inst_3 : CommSemiring P] →
              (Q : Type u_4) →
                [inst_4 : CommSemiring Q] →
                  [inst_5 : Algebra P Q] →
                    (f : R →+* P) → (r : R) → [IsLocalization.Away r S] → [IsLocalization.Away (f r) Q] → S →+* Q
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_rpow_iff_of_neg : ∀ {x y z : ℝ}, 0 < x → 0 < y → z < 0 → (x ^ z < y ^ z ↔ y < x)
-- Mathlib.Data.Rat.Defs
Rat.zero_of_num_zero : ∀ {q : ℚ}, q.num = 0 → q = 0
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.smul_mem : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M)
  {x : M} (r : R), x ∈ p → r • x ∈ p
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelBorel : ∀ {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [inst : MeasurableSpace.CountablyGenerated γ] {mΩ : MeasurableSpace Ω} [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] (κ : ProbabilityTheory.Kernel α (γ × Ω)) [inst_3 : ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsMarkovKernel κ.condKernelBorel
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.Unsafe.unassignedMVarsEqualUpToIdsCore : Lean.MVarId → Lean.MVarId → Aesop.EqualUpToIdsM Bool
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1'_apply_coeToLp : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} (𝕜 : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : NormedRing 𝕜] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] [inst_7 : IsBoundedSMul 𝕜 E]
  [inst_8 : IsBoundedSMul 𝕜 F] [inst_9 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ}
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (f : ↥(α →₁ₛ[μ] E)),
  (MeasureTheory.L1.setToL1' 𝕜 hT h_smul) ((MeasureTheory.Lp.simpleFunc.coeToLp α E ℝ) f) =
    (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_lie_mul_eq : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f g h : M →ₗ[R] M),
  (LinearMap.trace R M) (⁅f, g⁆ * h) = (LinearMap.trace R M) (f * ⁅g, h⁆)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.ofReal_toReal : ∀ (x : ℝ), (Tactic.ComputeAsymptotics.MultiseriesExpansion.ofReal x).toReal = x
-- Aesop.Tree.Data
Aesop.instBEqNodeState : BEq Aesop.NodeState
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMonoidWithZero : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [MonoidWithZero R] → MonoidWithZero (l.Germ R)
-- Lean.Parser.Do
Lean.Parser.Term.dependentParam.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Products distribute over sums (on the right) as measurable spaces.  -/
MeasurableEquiv.sumProdDistrib : (α : Type u_6) →
  (β : Type u_7) →
    (γ : Type u_8) →
      [inst : MeasurableSpace α] →
        [inst_1 : MeasurableSpace β] → [inst_2 : MeasurableSpace γ] → (α ⊕ β) × γ ≃ᵐ α × γ ⊕ β × γ
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.of.inj : ∀ {carrier : Type u} {str : MeasurableSpace carrier} {carrier_1 : Type u} {str_1 : MeasurableSpace carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.GroupTheory.Submonoid.Inverses
IsUnit.submonoid.coe_inv : ∀ {M : Type u_1} [inst : Monoid M] (x : ↥(IsUnit.submonoid M)), ↑x⁻¹ = ↑(IsUnit.unit ⋯)⁻¹
-- Batteries.Data.Fin.Coding
/-- Decode `Fin m → Fin n` from `Fin (n ^ m)`.  -/
Fin.decodeFun : {n m : ℕ} → Fin (n ^ m) → Fin m → Fin n
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.InductionCandidate : Type
-- Mathlib.RingTheory.MvPowerSeries.Equiv
PowerSeries.toMvPowerSeries_inj : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] (i : σ) {p q : PowerSeries R},
  (PowerSeries.toMvPowerSeries i) p = (PowerSeries.toMvPowerSeries i) q ↔ p = q
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.splitter : (motive : Turing.PartrecToTM2.Λ' → Sort u_1) →
  (x : Turing.PartrecToTM2.Λ') →
    ((p : Turing.PartrecToTM2.Γ' → Bool) →
        (k₁ k₂ : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q)) →
      ((k : Turing.PartrecToTM2.K') →
          (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
            (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k f q)) →
        ((q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q)) →
          ((p : Turing.PartrecToTM2.Γ' → Bool) →
              (k : Turing.PartrecToTM2.K') →
                (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q)) →
            ((q : Turing.PartrecToTM2.Λ') → motive q.copy) →
              ((q : Turing.PartrecToTM2.Λ') → motive q.succ) →
                ((q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂)) →
                  ((fs : Turing.ToPartrec.Code) →
                      (k : Turing.PartrecToTM2.Cont') →
                        motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k))) →
                    ((k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k.cons₂)) →
                      ((f : Turing.ToPartrec.Code) →
                          (k : Turing.PartrecToTM2.Cont') →
                            motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k))) →
                        ((f : Turing.ToPartrec.Code) →
                            (k : Turing.PartrecToTM2.Cont') →
                              motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k))) →
                          (Unit → motive (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt)) → motive x
-- Mathlib.Algebra.Exact.Basic
Function.MulExact.monoidHom_comp_eq_zero : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Group M] [inst_1 : Group N] [inst_2 : Group P] {f : M →* N}
  {g : N →* P}, Function.MulExact ⇑f ⇑g → g.comp f = 1
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_one : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv], CauSeq.const abv 1 = 1
-- Init.Prelude
instDecidableEqUInt64 : DecidableEq UInt64
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.inl_freeSumIso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] (I J_1 : Type u) {Z : SheafOfModules R}
  (h : SheafOfModules.free (I ⊕ J_1) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (SheafOfModules.freeSumIso I J_1).hom h) =
    CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap Sum.inl) h
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.dropUntil : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} {p : G.Walk v w},
  p.IsPath → ∀ (h : u ∈ p.support), (p.dropUntil u h).IsPath
-- Mathlib.GroupTheory.Exponent
AddGroup.exponent_dvd_nat_card : ∀ {G : Type u} [inst : AddGroup G], AddMonoid.exponent G ∣ Nat.card G
-- Mathlib.Algebra.Azumaya.Matrix
AlgHom.mulLeftRightMatrix.comp_inv : ∀ (R : Type u_1) (n : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  (AlgHom.mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ AlgHom.mulLeftRightMatrix_inv R n = LinearMap.id
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `containsThenInsertIfNew` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.containsThenInsertIfNew : ∀ {α : Type u} [inst : Ord α] {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k},
  t.WF → (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v t h).2.impl.WF
-- Mathlib.FieldTheory.IsAlgClosed.Basic
isAlgClosure_iff : ∀ (k : Type u) [inst : Field k] (K : Type v) [inst_1 : Field K] [inst_2 : Algebra k K],
  IsAlgClosure k K ↔ IsAlgClosed K ∧ Algebra.IsAlgebraic k K
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.MemLp.sup : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [inst_1 : Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] {f g : α → E},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp g p μ → MeasureTheory.MemLp (f ⊔ g) p μ
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.TZSpec.filePath.inj : ∀ {p p_1 : String}, Std.Time.Database.TZdb.TZSpec.filePath p = Std.Time.Database.TZdb.TZSpec.filePath p_1 → p = p_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula.0.WeierstrassCurve.Jacobian.toAffine_negAddY_of_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      ∀ {n d : F},
        d ≠ 0 →
          W.toAffine.negAddY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (n / (P 2 * Q 2 * d)) =
            (n *
                    (n ^ 2 + W.a₁ * n * P 2 * Q 2 * d - W.a₂ * P 2 ^ 2 * Q 2 ^ 2 * d ^ 2 - P 0 * Q 2 ^ 2 * d ^ 2 -
                        Q 0 * P 2 ^ 2 * d ^ 2 -
                      P 0 * Q 2 ^ 2 * d ^ 2) +
                  P 1 * Q 2 ^ 3 * d ^ 3) /
                (P 2 * Q 2) ^ 3 /
              d ^ 3
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- The product of two `C^n` manifolds is naturally a `C^n` manifold.  -/
IsManifold.prod : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_5} [inst : NontriviallyNormedField 𝕜] {E : Type u_6} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_7} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_8}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_9} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} (M : Type u_10) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [IsManifold I n M] (M' : Type u_11) [inst_10 : TopologicalSpace M'] [inst_11 : ChartedSpace H' M']
  [IsManifold I' n M'], IsManifold (I.prod I') n (M × M')
-- Lean.Elab.InfoTree.Types
Lean.Elab.DelabTermInfo.mk.sizeOf_spec : ∀ (toTermInfo : Lean.Elab.TermInfo) (location? : Option Lean.DeclarationLocation)
  (mkDocString? : Option (Lean.PPContext → IO String)) (explicit : Bool),
  sizeOf { toTermInfo := toTermInfo, location? := location?, mkDocString? := mkDocString?, explicit := explicit } =
    1 + sizeOf toTermInfo + sizeOf location? + sizeOf mkDocString? + sizeOf explicit
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.arrowCongr'_apply : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₁' : Type u_5} {A₂' : Type u_6} [inst : Monoid R]
  [inst_1 : NonUnitalNonAssocSemiring A₁] [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁]
  [inst_4 : NonUnitalNonAssocSemiring A₂] [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂]
  [inst_7 : NonUnitalNonAssocSemiring A₁'] [inst_8 : DistribMulAction R A₁'] [inst_9 : Star A₁']
  [inst_10 : NonUnitalNonAssocSemiring A₂'] [inst_11 : DistribMulAction R A₂'] [inst_12 : Star A₂'] (e₁ : A₁ ≃⋆ₐ[R] A₁')
  (e₂ : A₂ ≃⋆ₐ[R] A₂') (f : A₁ →⋆ₙₐ[R] A₂),
  (e₁.arrowCongr' e₂) f = (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.copy.hcongr_9 : ∀ (V V' : Type u),
  V = V' →
    ∀ (G : SimpleGraph V) (G' : SimpleGraph V'),
      G ≍ G' →
        ∀ (u : V) (u' : V'),
          u ≍ u' →
            ∀ (v : V) (v' : V'),
              v ≍ v' →
                ∀ (u'_1 : V) (u'' : V'),
                  u'_1 ≍ u'' →
                    ∀ (v'_1 : V) (v'' : V'),
                      v'_1 ≍ v'' →
                        ∀ (p : G.Walk u v) (p' : G'.Walk u' v'),
                          p ≍ p' →
                            ∀ (hu : u = u'_1) (hu' : u' = u''),
                              hu ≍ hu' → ∀ (hv : v = v'_1) (hv' : v' = v''), hv ≍ hv' → p.copy hu hv ≍ p'.copy hu' hv'
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_eq_X_mul_S_add_C : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  2 * Polynomial.Chebyshev.S R (n + 1) = Polynomial.X * Polynomial.Chebyshev.S R n + Polynomial.Chebyshev.C R (n + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piPiIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C)
  [inst_1 : ∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)]
  [inst_2 : CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i],
  (CategoryTheory.Limits.piPiIso f g).inv =
    CategoryTheory.Limits.Pi.lift fun i =>
      CategoryTheory.Limits.Pi.lift fun x => CategoryTheory.Limits.Pi.π (fun p => g p.fst p.snd) ⟨i, x⟩
-- Mathlib.RingTheory.Localization.BaseChange
LocalizedModule.equivTensorProduct.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (M : Type u_3) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LocalizedModule.equivTensorProduct S M = ⋯.equiv.symm
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.lowerCentralSeries.eq_1 : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (k : ℕ),
  LieModule.lowerCentralSeries R L M k = LieSubmodule.lcs k ⊤