mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fintype.Card
/-- A reversed version of `Fin.cast_eq_cast` that is easier to rewrite with.  -/
Fin.cast_eq_cast' : ∀ {n m : ℕ} (h : Fin n = Fin m), cast h = Fin.cast ⋯
-- Std.Http.Data.Status
Std.Http.CustomStatus.mk.inj : ∀ {code : UInt16} {phrase : String}
  {validReasonPhrase :
    autoParam (Std.Http.IsValidReasonPhrase phrase) Std.Http.CustomStatus.validReasonPhrase._autoParam}
  {validCode : autoParam (100 ≤ code ∧ code ≤ 999) Std.Http.CustomStatus.validCode._autoParam}
  {validUnknown : autoParam (¬Std.Http.isKnownStatusCode code = true) Std.Http.CustomStatus.validUnknown._autoParam}
  {code_1 : UInt16} {phrase_1 : String}
  {validReasonPhrase_1 :
    autoParam (Std.Http.IsValidReasonPhrase phrase_1) Std.Http.CustomStatus.validReasonPhrase._autoParam}
  {validCode_1 : autoParam (100 ≤ code_1 ∧ code_1 ≤ 999) Std.Http.CustomStatus.validCode._autoParam}
  {validUnknown_1 :
    autoParam (¬Std.Http.isKnownStatusCode code_1 = true) Std.Http.CustomStatus.validUnknown._autoParam},
  { code := code, phrase := phrase, validReasonPhrase := validReasonPhrase, validCode := validCode,
        validUnknown := validUnknown } =
      { code := code_1, phrase := phrase_1, validReasonPhrase := validReasonPhrase_1, validCode := validCode_1,
        validUnknown := validUnknown_1 } →
    code = code_1 ∧ phrase = phrase_1
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.pow : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R} {m : ℕ},
  p.IsMonicOfDegree m → ∀ (n : ℕ), (p ^ n).IsMonicOfDegree (m * n)
-- Mathlib.Data.Num.Prime
_private.Mathlib.Data.Num.Prime.0.PosNum.minFac.match_1.eq_3 : ∀ (motive : PosNum → Sort u_1) (n : PosNum) (h_1 : Unit → motive PosNum.one) (h_2 : (a : PosNum) → motive a.bit0)
  (h_3 : (n : PosNum) → motive n.bit1),
  (match n.bit1 with
    | PosNum.one => h_1 ()
    | a.bit0 => h_2 a
    | n.bit1 => h_3 n) =
    h_3 n
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- `S p i` is Bird's `Sₚ(βᵢ)`: words `α` of length `p` over the alphabet `βᵢ`.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.S : {n : ℕ} → (p : ℕ) → Fin n → Finset (Fin p → Fin n)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : β → β},
  Std.DHashMap.Const.get? (Std.DHashMap.Const.modify m k f) k' =
    if (k == k') = true then Option.map f (Std.DHashMap.Const.get? m k) else Std.DHashMap.Const.get? m k'
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzWith.div : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E}, LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (Kf + Kg) fun x => f x / g x
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_subset : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  {t : Finset ι} {w : ι → R} (z : ι → E) {t' : Finset ι},
  t ⊆ t' → (∀ i ∈ t', i ∉ t → w i = 0) → t.centerMass w z = t'.centerMass w z
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.ext_iff : ∀ {X Y : AddCommMonCat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.log_pow : ∀ {M : Type u_4} [inst : AddMonoid M] (x : WithZero (Multiplicative M)) (n : ℕ), (x ^ n).log = n • x.log
-- Init.Data.List.Count
List.countP_nil : ∀ {α : Type u_1} {p : α → Bool}, List.countP p [] = 0
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} (f : α → β) (g : β → ι) [Filter.TendstoCofinite g]
  [Filter.TendstoCofinite f], Filter.TendstoCofinite (g ∘ f)
-- Mathlib.RingTheory.Finiteness.Finsupp
LinearMap.finsuppLinearMap_bijective_of_finite : ∀ (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (S : Type u_5) [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N]
  [inst_5 : Semiring S] [inst_6 : Module S N] [inst_7 : SMulCommClass R S N] [Finite ι],
  Function.Bijective ⇑(LinearMap.finsuppLinearMap S)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- **Alias** of `Measurable.fun_comp`.

---

Eta-expanded form of `Measurable.comp` -/
Measurable.comp' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x : MeasurableSpace α} {x_1 : MeasurableSpace β}
  {x_2 : MeasurableSpace γ} {g : β → γ} {f : α → β}, Measurable g → Measurable f → Measurable fun x => g (f x)
-- Init.Data.Option.Lemmas
Option.bind.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (x : α → Option β) (a : α), (some a).bind x = x a
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coe_map : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (b : Module.Basis ι R M) (f : M ≃ₗ[R] M'),
  ⇑(b.map f) = ⇑f ∘ ⇑b
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
RightPreLieAlgebra.instLieAdmissibleAlgebra : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] → [inst_1 : RightPreLieRing L] → [RightPreLieAlgebra R L] → LieAdmissibleAlgebra R L
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_eq_tdiv_of_mul_eq_mul : ∀ {a b c d : ℤ}, d ∣ c → b ≠ 0 → d ≠ 0 → a * d = b * c → a.tdiv b = c.tdiv d
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The isomorphism `S₁.opcycles ≅ S₂.opcycles` induced by an isomorphism
of short complexes `S₁ ≅ S₂`.  -/
CategoryTheory.ShortComplex.opcyclesMapIso : {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₂) → [inst_2 : S₁.HasRightHomology] → [inst_3 : S₂.HasRightHomology] → S₁.opcycles ≅ S₂.opcycles
-- Mathlib.Combinatorics.Additive.Convolution
Finset.univ_convolution : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] [inst_2 : Fintype G] (B : Finset G) (a : G),
  Finset.univ.convolution B a = B.card
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHomClass.mk : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] [inst_4 : FunLike F α β] [toLatticeHomClass : LatticeHomClass F α β],
  (∀ (f : F), f ⊤ = ⊤) → (∀ (f : F), f ⊥ = ⊥) → BoundedLatticeHomClass F α β
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.map_rid_comp_map_lid : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (P.map f (CategoryTheory.CategoryStruct.id Y'))
      (P.map (CategoryTheory.CategoryStruct.id X') g) =
    P.map f g
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.degreeLTEquiv_eq_zero_iff_eq_zero : ∀ {R : Type u} [inst : Semiring R] {n : ℕ} {p : Polynomial R} (hp : p ∈ Polynomial.degreeLT R n),
  (Polynomial.degreeLTEquiv R n) ⟨p, hp⟩ = 0 ↔ p = 0
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
/-- The conditional expectation of the indicator of a function over an `m`-measurable set with
respect to the σ-algebra `m` is a.e. equal to the indicator of the conditional expectation.  -/
MeasureTheory.condExp_indicator : ∀ {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} {s : Set α},
  MeasureTheory.Integrable f μ → MeasurableSet s → μ[s.indicator f | m] =ᵐ[μ] s.indicator μ[f | m]
-- Mathlib.Probability.Independence.Integration
/-- If `X` and `Y` are random variables and `B` is a continuous bilinear map
such that `∀ x y, c * ‖x‖ * ‖y‖ ≤ ‖B x y‖`, then `∫ ω, B (X ω) (Y ω) ∂μ = B μ[X] μ[Y].`

The assumption on `B` allows to drop the integrability condition in
`IndepFun.integral_bilin'`, which is useful for the versions where `B` is the scalar
multiplication or the multiplication.  -/
ProbabilityTheory.IndepFun.integral_bilin' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : MeasurableSpace E] [BorelSpace E]
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] [CompleteSpace F] [inst_8 : MeasurableSpace F]
  [BorelSpace F] [inst_10 : NormedAddCommGroup G] [inst_11 : NormedSpace ℝ G] [CompleteSpace G] {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.AEStronglyMeasurable X μ →
      MeasureTheory.AEStronglyMeasurable Y μ →
        ∀ (B : E →L[ℝ] F →L[ℝ] G) (c : NNReal),
          c ≠ 0 →
            (∀ (x : E) (y : F), ↑c * ‖x‖ * ‖y‖ ≤ ‖(B x) y‖) →
              ∫ (ω : Ω), (B (X ω)) (Y ω) ∂μ = (B (∫ (x : Ω), X x ∂μ)) (∫ (x : Ω), Y x ∂μ)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- Applying a non-unital ⋆-algebra homomorphism to every entry of a matrix is itself a
⋆-algebra homomorphism on matrices.  -/
CStarMatrix.mapₙₐ : {n : Type u_2} →
  {R : Type u_3} →
    {A : Type u_5} →
      {B : Type u_6} →
        [inst : Fintype n] →
          [inst_1 : Semiring R] →
            [inst_2 : NonUnitalNonAssocSemiring A] →
              [inst_3 : Module R A] →
                [inst_4 : Star A] →
                  [inst_5 : NonUnitalNonAssocSemiring B] →
                    [inst_6 : Module R B] →
                      [inst_7 : Star B] → (A →⋆ₙₐ[R] B) → CStarMatrix n n A →⋆ₙₐ[R] CStarMatrix n n B
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderAssociator.associator_hom_mem : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  (P : CategoryTheory.MorphismProperty C) [self : P.IsStableUnderAssociator] (c c' c'' : C),
  P (CategoryTheory.MonoidalCategoryStruct.associator c c' c'').hom
-- Init.Data.List.Range
List.range'_eq_map_range : ∀ {s n : ℕ}, List.range' s n = List.map (fun x => s + x) (List.range n)
-- Mathlib.Topology.Hom.ContinuousEval
Filter.Tendsto.eval : ∀ {F : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : FunLike F X Y] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [ContinuousEval F X Y] {α : Type u_5} {l : Filter α}
  {f : α → F} {f₀ : F} {g : α → X} {x₀ : X},
  Filter.Tendsto f l (nhds f₀) → Filter.Tendsto g l (nhds x₀) → Filter.Tendsto (fun a => (f a) (g a)) l (nhds (f₀ x₀))
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.tendsto_atTop : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {u : β → α} {a : α},
  Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' : α} {f : Option β → Option β} {hc : k' ∈ Std.ExtDTreeMap.Const.alter t k f},
  Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.Const.alter t k f) k' hc =
    if heq : cmp k k' = Ordering.eq then (f (Std.ExtDTreeMap.Const.get? t k)).get ⋯
    else Std.ExtDTreeMap.Const.get t k' ⋯
-- Mathlib.Analysis.Normed.Lp.lpHolder
Memℓp.bilin_of_zero_left : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)]
  (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {e : (i : ι) → E i} {f : (i : ι) → F i},
  Memℓp e 0 → Memℓp (fun i => ((B i) (e i)) (f i)) 0
-- Mathlib.Logic.Equiv.Prod
optionProdEquiv_symm_inl : ∀ {α : Type u_9} {β : Type u_10} (b : β), optionProdEquiv.symm (Sum.inl b) = (none, b)
-- Mathlib.Data.Nat.Factorization.Divisors
Nat.Iic_factorization_prod_pow_injective : ∀ (n : ℕ), Function.Injective fun x => (↑x).prod fun x1 x2 => x1 ^ x2
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castLE_Iic : ∀ {m n : ℕ} (i : Fin m) (h : m ≤ n), Fin.castLE h '' Set.Iic i = Set.Iic (Fin.castLE h i)
-- Lean.Meta.Tactic.LibrarySearch
/-- A discharger that tries `grind` on the goal.
The proof is wrapped in `Grind.Marker` so that suggestions display `(by grind)`
instead of the complex grind proof term.
Returns `some []` if grind succeeds, `none` otherwise (leaving the goal as a subgoal).
 -/
Lean.Meta.LibrarySearch.grindDischarger : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndep_bot_right : ∀ {Ω : Type u_1} (m₁ : MeasurableSpace Ω) {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ], ProbabilityTheory.CondIndep m' m₁ ⊥ hm' μ
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.Associative.ε₁_eq_mul : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6}
  {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₃ : ComplexShape I₃} {c₁₂ : ComplexShape I₁₂} {c₂₃ : ComplexShape I₂₃}
  {c : ComplexShape J} {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₁₂ c₃ c}
  {inst_2 : TotalComplexShape c₂ c₃ c₂₃} {inst_3 : TotalComplexShape c₁ c₂₃ c} [self : c₁.Associative c₂ c₃ c₁₂ c₂₃ c]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
  c₁.ε₁ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
-- Mathlib.Algebra.GroupWithZero.Range
/-- For a morphism of monoids with zero `f`, this is the smallest submonoid with zero of the
codomain containing the range of `f`.  -/
MonoidWithZeroHom.ValueMonoid₀ : {A : Type u_1} → {B : Type u_2} → [inst : MonoidWithZero A] → [inst_1 : MonoidWithZero B] → (A →*₀ B) → Type u_2
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.invert_symm : ∀ {R : Type u_3} [inst : CommSemiring R], LaurentPolynomial.invert.symm = LaurentPolynomial.invert
-- Mathlib.Topology.Homotopy.Lifting
FundamentalGroup.mapOfEq.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f f_1 : C(X, Y))
  (e_f : f = f_1) {x : X} {y : Y} (h : f x = y), FundamentalGroup.mapOfEq f h = FundamentalGroup.mapOfEq f_1 ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {l : List (α × β)}
  {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → ∀ {h' : k' ∈ t.insertMany l}, (t.insertMany l)[k'] = v
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_prod : ∀ {R : Type u} {ι : Type y} [inst : CommSemiring R] [inst_1 : DecidableEq ι] {s : Multiset ι} {f : ι → Polynomial R},
  Polynomial.derivative (Multiset.map f s).prod =
    (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * Polynomial.derivative (f i)) s).sum
-- Mathlib.CategoryTheory.Yoneda
/-- The co-Yoneda embedding is fully faithful.  -/
CategoryTheory.Coyoneda.fullyFaithful : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.coyoneda.FullyFaithful
-- Mathlib.GroupTheory.OrderOfElement
/-- The backward direction of `orderOf_eq_prime_iff`.  -/
orderOf_eq_prime : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)], x ^ p = 1 → x ≠ 1 → orderOf x = p
-- Mathlib.RingTheory.Smooth.Basic
Algebra.Extension.H1Cotangent.equivOfFormallySmooth_apply : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {P₁ : Algebra.Extension R A} {P₂ : Algebra.Extension R A} (f : P₁.Hom P₂) [inst_3 : Algebra.FormallySmooth R P₁.Ring]
  [inst_4 : Algebra.FormallySmooth R P₂.Ring] (x : P₁.H1Cotangent),
  (Algebra.Extension.H1Cotangent.equivOfFormallySmooth P₁ P₂) x = (Algebra.Extension.H1Cotangent.map f) x
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Construct the syntax for a rewrite tactic.  -/
Mathlib.Tactic.ClickSuggestions.mkRewrite : Mathlib.Tactic.ClickSuggestions.RwKind →
  Bool → Lean.Term → Option Lean.Ident → optParam Bool false → Lean.CoreM (Lean.TSyntax `tactic)
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] (f : α ≃+*o β), f.toFun = ⇑f
-- Mathlib.AlgebraicGeometry.Modules.Tilde
_private.Mathlib.AlgebraicGeometry.Modules.Tilde.0.AlgebraicGeometry.QuasicoherentTilde.Aux.uniqueness : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} {V : (AlgebraicGeometry.Spec R).Opens},
  AlgebraicGeometry.QuasicoherentTilde.Aux✝ M V →
    ∀ (f : ↑R) (hf : PrimeSpectrum.basicOpen f ≤ V) (t : ↑(M.presheaf.obj (Opposite.op V))),
      (CategoryTheory.ConcreteCategory.hom (M.presheaf.map (CategoryTheory.homOfLE hf).op)) t = 0 → ∃ n, f ^ n • t = 0
-- Mathlib.Tactic.TacticAnalysis
/-- Parse an infotree to find all the sequences of tactics contained within `stx`.

We consider a sequence here to be a maximal interval of tactics joined by `;` or newlines.
This function returns an array of sequences. For example, a proof of the form:
```
by
  tac1
  · tac2; tac3
  · tac4; tac5
```
would result in three sequences:
* `#[tac1, (· tac2; tac3), (· tac4; tac5)]`
* `#[tac2, tac3]`
* `#[tac4, tac5]`

Similarly, a declaration with multiple `by` blocks results in each of the blocks getting its
own sequence.
 -/
Mathlib.TacticAnalysis.findTacticSeqs : Lean.Elab.InfoTree → Lean.Elab.Command.CommandElabM (Array (Array Mathlib.TacticAnalysis.TacticNode))
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_dif : ∀ {M : Type u_2} [inst : CommMonoid M] {p : Prop} [inst_1 : Decidable p] (f : p → M),
  ∏ᶠ (i : p), f i = if h : p then f h else 1
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isUnramified_self : ∀ {K : Type u_2} [inst : Field K] (w : NumberField.InfinitePlace K), NumberField.InfinitePlace.IsUnramified K w
-- Mathlib.Data.Part
Part.coe_some : ∀ {α : Type u_1} (a : α), ↑(some a) = Part.some a
-- Mathlib.RingTheory.IntegralDomain
Finite.isField_of_domain : ∀ (R : Type u_3) [inst : CommRing R] [IsDomain R] [Finite R], IsField R
-- Mathlib.Geometry.Convex.Cone.TensorProduct
PointedCone.minTensorProduct.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H]
  (C₁ : PointedCone R G) (C₂ : PointedCone R H),
  C₁.minTensorProduct C₂ = PointedCone.hull R (Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑C₁ ↑C₂)
-- Mathlib.Topology.Connected.Clopen
/-- If `X` has infinitely many connected components, it admits disjoint union decompositions with
arbitrarily many summands.  -/
ConnectedComponents.exists_fun_isClopen_of_infinite : ∀ (α : Type u) [inst : TopologicalSpace α] [Infinite (ConnectedComponents α)] (n : ℕ),
  0 < n →
    ∃ U,
      (∀ (i : Fin n), IsClopen (U i)) ∧
        (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Function.onFun Disjoint U) ∧ ⋃ i, U i = Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
/-- Every functor `G : Grothendieck F ⥤ H` induces a natural transformation from `G` to the
composition of the forgetful functor on `Grothendieck F` with the fiberwise colimit on `G`.  -/
CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {H : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} H] →
          (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) →
            [inst_2 :
                ∀ {X Y : C} (f : X ⟶ Y),
                  CategoryTheory.Limits.HasColimit
                    ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] →
              G ⟶ (CategoryTheory.Grothendieck.forget F).comp (CategoryTheory.Limits.fiberwiseColimit G)
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImport.mk.inj : ∀ {module : Lean.Lsp.LeanModule} {kind : Lean.Lsp.LeanImportKind} {module_1 : Lean.Lsp.LeanModule}
  {kind_1 : Lean.Lsp.LeanImportKind},
  { module := module, kind := kind } = { module := module_1, kind := kind_1 } → module = module_1 ∧ kind = kind_1
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.mkHom_eqToHom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : F X ⟶ F Y} (h : f = g),
  CategoryTheory.Bicategory.InducedBicategory.mkHom₂ (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Given three collinear points, two on a sphere and one not outside it, the one not outside it
is weakly between the other two points.  -/
EuclideanGeometry.wbtw_of_collinear_of_dist_center_le_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
  Collinear ℝ {p₁, p₂, p₃} → p₁ ∈ s → dist p₂ s.center ≤ s.radius → p₃ ∈ s → p₁ ≠ p₃ → Wbtw ℝ p₁ p₂ p₃
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X} {C : ℝ},
  μ s < ⊤ → (∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C) → ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * μ.real s
-- Mathlib.Data.Set.Function
Function.apply_eq_of_range_eq_singleton : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {b : β}, Set.range f = {b} → ∀ (a : α), f a = b
-- Init.Data.Option.Lemmas
Option.pmap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (x_2 : ∀ (a : α), none = some a → p a),
  Option.pmap f none x_2 = none
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.ext_iff : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {f g : M →ₛₗ[σ] M₃}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteBiproducts : ∀ (C : Type uC) [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteBiproducts C], CategoryTheory.Limits.HasFiniteProducts C
-- Mathlib.Data.Num.Basic
PosNum.bit0 : PosNum → PosNum
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.δ_rightShift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' m' : ℤ) (hn' : n' + a = n)
  (m : ℤ) (hm' : m' + a = m),
  CochainComplex.HomComplex.δ n' m' (γ.rightShift a n' hn') =
    a.negOnePow • (CochainComplex.HomComplex.δ n m γ).rightShift a m' hm'
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.wasCancelledByCancelRequest : Lean.Server.RequestCancellationToken → BaseIO Bool
-- Std.Do.Triple.SpecLemmas
Std.Do.StringSliceInvariant.eq_1 : ∀ (s : String.Slice) (β : Type u) (ps : Std.Do.PostShape),
  Std.Do.StringSliceInvariant s β ps = Std.Do.PostCond (s.Pos × β) ps
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
/-- `Complex.exp` as an `OpenPartialHomeomorph` with `source = {z | -π < im z < π}` and
`target = {z | 0 < re z} ∪ {z | im z ≠ 0}` (a.k.a. `slitPlane`).
This definition is used to prove that `Complex.log`
is complex differentiable at all points but the negative real semi-axis.
 -/
Complex.expOpenPartialHomeomorph : OpenPartialHomeomorph ℂ ℂ