mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, returning `fallback` if no such key exists.
 -/
Std.TreeMap.getKeyGED : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → α → α
-- Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
/-- The sum of almost everywhere strongly measurable functions is measurable.  -/
MeasureTheory.AEStronglyMeasurable.tsum' : ∀ {X : Type u_4} {E : Type u_5} {ι : Type u_6} [inst : MeasurableSpace X] [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [ContinuousAdd E] {L : SummationFilter ι}
  [L.NeBot] [L.filter.IsCountablyGenerated] {μ : MeasureTheory.Measure X} {f : ι → X → E},
  (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) → MeasureTheory.AEStronglyMeasurable (∑'[L] (i : ι), f i) μ
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.TaggedPrepartition.disjUnion.congr_simp : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ π₁_1 : BoxIntegral.TaggedPrepartition I) (e_π₁ : π₁ = π₁_1)
  (π₂ π₂_1 : BoxIntegral.TaggedPrepartition I) (e_π₂ : π₂ = π₂_1) (h : Disjoint π₁.iUnion π₂.iUnion),
  π₁.disjUnion π₂ h = π₁_1.disjUnion π₂_1 ⋯
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l → (Std.HashMap.unitOfList l).size = l.length
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformlyOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] (f : ι → β → α) (g : β → α) (s : Set β)
  [inst_1 : UniformSpace α],
  HasSumUniformlyOn f g s = HasSum (⇑(UniformOnFun.ofFun {s}) ∘ f) ((UniformOnFun.ofFun {s}) g)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.InitResults.tree : {α : Type} → Lean.Meta.LazyDiscrTree.InitResults α → Lean.Meta.LazyDiscrTree.PreDiscrTree α
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- There are `min n r` parts in a graph on `n` vertices satisfying `G.IsTuranMaximal r`.
`min` handles the `n < r` case, when `G` is complete but still `r + 1`-cliquefree
for having insufficiently many vertices.  -/
SimpleGraph.IsTuranMaximal.card_parts : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ} (h : G.IsTuranMaximal r)
  [inst_2 : DecidableEq V], h.finpartition.parts.card = min (Fintype.card V) r
-- Mathlib.RingTheory.Smooth.Local
/-- The **Jacobian criterion** for smoothness of local algebras.
Suppose `S` is a local `R`-algebra, and `0 → I → P → S → 0` is a presentation such that
`P` is formally-smooth over `R`, `Ω[P⁄R]` is finite free over `P`,
(typically satisfied when `P` is the localization of a polynomial ring of finite type)
and `I` is finitely generated.
Then `S` is formally smooth iff `k ⊗ₛ I/I² → k ⊗ₚ Ω[P/R]` is injective,
where `k` is the residue field of `S`.
 -/
Algebra.FormallySmooth.iff_injective_lTensor_residueField : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsLocalRing S]
  [inst_3 : Algebra R S] (P : Algebra.Extension R S) [Algebra.FormallySmooth R P.Ring] [Module.Free P.Ring Ω[P.Ring⁄R]]
  [Module.Finite P.Ring Ω[P.Ring⁄R]],
  P.ker.FG →
    (Algebra.FormallySmooth R S ↔
      Function.Injective ⇑(LinearMap.lTensor (IsLocalRing.ResidueField S) P.cotangentComplex))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The braiding isomorphism which swaps a binary biproduct.  -/
CategoryTheory.Limits.biprod.braiding : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] → (P Q : C) → P ⊞ Q ≅ Q ⊞ P
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.coe_toAddHom : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {f : M ≃+ N}, ⇑f.toAddHom = ⇑f
-- Mathlib.RingTheory.WittVector.Defs
WittVector.mul_coeff_zero : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x y : WittVector p R),
  (x * y).coeff 0 = x.coeff 0 * y.coeff 0
-- Mathlib.Order.Defs.PartialOrder
le_of_lt_or_eq : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b ∨ a = b → a ≤ b
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coeCLE_refl : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A], ↑(ContinuousAlgEquiv.refl R A) = ContinuousLinearEquiv.refl R A
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.Hom.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Comon C} (hom hom_1 : M.X ⟶ N.X) (e_hom : hom = hom_1)
  [isComonHom_hom : CategoryTheory.IsComonHom hom],
  { hom := hom, isComonHom_hom := isComonHom_hom } = { hom := hom_1, isComonHom_hom := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.whiskerIdCancel_left : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t :
    CategoryTheory.Bicategory.RightLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g))
  {s : CategoryTheory.Bicategory.RightLift f g} (τ : s.whisker (CategoryTheory.CategoryStruct.id c) ⟶ t),
  (t.whiskerIdCancel τ).left =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor s.lift).inv τ.left
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.SynthInstance.mkAnswer : Lean.Meta.SynthInstance.ConsumerNode → Lean.MetaM Lean.Meta.SynthInstance.Answer
-- Mathlib.Topology.Category.CompHausLike.SigmaComparison
/-- The comparison map from the value of a condensed set on a finite coproduct to the product of the
values on the components.
 -/
CompHausLike.sigmaComparison : {P : TopCat → Prop} →
  [inst : CompHausLike.HasExplicitFiniteCoproducts P] →
    (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) →
      {α : Type u} →
        [inst_1 : Finite α] →
          (σ : α → Type u) →
            [inst_2 : (a : α) → TopologicalSpace (σ a)] →
              [inst_3 : ∀ (a : α), CompactSpace (σ a)] →
                [inst_4 : ∀ (a : α), T2Space (σ a)] →
                  [inst_5 : ∀ (a : α), CompHausLike.HasProp P (σ a)] →
                    X.obj (Opposite.op (CompHausLike.of P ((a : α) × σ a))) ⟶
                      (a : α) → X.obj (Opposite.op (CompHausLike.of P (σ a)))
-- Mathlib.Algebra.Module.Shrink
Shrink.instModule : {R : Type u_1} →
  {α : Type u_2} →
    [inst : Small.{v, u_2} α] →
      [inst_1 : Semiring R] → [inst_2 : AddCommMonoid α] → [Module R α] → Module R (Shrink.{v, u_2} α)
-- Mathlib.Order.SuccPred.Limit
/-- Given `j < i` with `i` a successor pre-limit, `IsSuccPrelimit.mid` picks an arbitrary element
strictly between `j` and `i`.  -/
Order.IsSuccPrelimit.mid : {α : Type u_1} → [inst : Preorder α] → {i j : α} → Order.IsSuccPrelimit i → j < i → ↑(Set.Ioo j i)
-- Mathlib.RingTheory.DividedPowers.Basic
/-- The divided power function underlying a divided power structure  -/
DividedPowers.dpow : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → DividedPowers I → ℕ → A → A
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
IsBoundedBilinearMap.differentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {b : E × F → G},
  IsBoundedBilinearMap 𝕜 b → Differentiable 𝕜 b
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.trunc'_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) [inst_1 : DecidableEq σ] {n : σ →₀ ℕ}
  (φ : MvPowerSeries σ R),
  (MvPowerSeries.trunc' R (p • n)) ((MvPowerSeries.expand p hp) φ) =
    (MvPolynomial.expand p) ((MvPowerSeries.trunc' R n) φ)
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.coeff_erase_ne : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] {a a' : α} (f : SkewMonoidAlgebra M α),
  a' ≠ a → ((SkewMonoidAlgebra.erase a) f).coeff a' = f.coeff a'
-- Mathlib.Algebra.Homology.Single
ChainComplex.single₀_map_f_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {A B : V} (f : A ⟶ B), ((ChainComplex.single₀ V).map f).f 0 = f
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.reindex_inv_π : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C)
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).inv
      (CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b) =
    CategoryTheory.Limits.Pi.π f (ε b)
-- Mathlib.RingTheory.AdjoinRoot
/-- Embedding of the original ring `R` into `AdjoinRoot f`.  -/
AdjoinRoot.of : {R : Type u_1} → [inst : CommRing R] → (f : Polynomial R) → R →+* AdjoinRoot f
-- Init.Data.SInt.Bitwise
Int8.xor_zero : ∀ {a : Int8}, a ^^^ 0 = a
-- Lean.Expr
Lean.instHashableFVarId : Hashable Lean.FVarId
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_ne_zero : ∀ {M : Type u_1} [inst : MonoidWithZero M] {a : M}, Associates.mk a ≠ 0 ↔ a ≠ 0
-- Lean.Meta.Tactic.Grind.SimpUtil
/-- Returns the array of simprocs used by `grind`.  -/
Lean.Meta.Grind.getSimprocs : Lean.MetaM (Array Lean.Meta.Simprocs)
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- There exists a vertex of maximal degree. Note the assumption of being nonempty is necessary, as
the lemma implies there exists a vertex.  -/
SimpleGraph.exists_maximal_degree_vertex : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [Nonempty V],
  ∃ v, G.maxDegree = G.degree v
-- Init.Data.Array.Lemmas
Array.foldl_map : ∀ {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {f : β₁ → β₂} {g : α → β₂ → α} {xs : Array β₁} {init : α},
  Array.foldl g init (Array.map f xs) = Array.foldl (fun x y => g x (f y)) init xs
-- Mathlib.Data.Nat.Factorization.Basic
Nat.factorization_ordCompl : ∀ (n p : ℕ), (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_toHomeomorph : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑e.toHomeomorph = ⇑e
-- Mathlib.MeasureTheory.Measure.Restrict
MeasurableEmbedding.map_comap : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ (μ : MeasureTheory.Measure β),
      MeasureTheory.Measure.map f (MeasureTheory.Measure.comap f μ) = μ.restrict (Set.range f)
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.Forall.eq_2 : ∀ {α : Type u_1} (n : ℕ) (P : (Fin (n + 1) → α) → Prop),
  FinVec.Forall P = ∀ (x : α), FinVec.Forall fun v => P (Matrix.vecCons x v)
-- Mathlib.Topology.Compactness.Compact
IsCompact.adherence_nhdset : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X} {f : Filter X},
  IsCompact s → f ≤ Filter.principal s → IsOpen t → (∀ x ∈ s, ClusterPt x f → x ∈ t) → t ∈ f
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the third commutative square of a triangle morphism  -/
CategoryTheory.Pretriangulated.TriangleMorphism.comm₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} (self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂),
  CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map self.hom₁) =
    CategoryTheory.CategoryStruct.comp self.hom₃ T₂.mor₃
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.map : ∀ {F : Type u} {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Field F] [inst_3 : Algebra K L]
  [inst_4 : Algebra F K] [inst_5 : Algebra F L] [IsScalarTower F K L] (f : Polynomial F)
  [Polynomial.IsSplittingField F L f], Polynomial.IsSplittingField K L (Polynomial.map (algebraMap F K) f)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.toEquiv_injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Function.Injective Homeomorph.toEquiv
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.mem_smul_iff_smul_inv_mem : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} {g : G} {x : X} {pt : DiscreteTiling.PlacedTile ps}, x ∈ g • pt ↔ g⁻¹ • x ∈ pt
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_le_min_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, (cmp (t.min ⋯) ((t.erase k).min he)).isLE = true
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.instTensorAddUnit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.AddGrpObj.instTensorAddUnit =
    { toAddMonObj := CategoryTheory.AddMonObj.instTensorAddUnit,
      neg := CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C), left_neg := ⋯,
      right_neg := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.add_pos`.  -/
Left.add_pos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b : α},
  0 < a → 0 < b → 0 < a + b
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
support_iteratedFDeriv_subset : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  (n : ℕ), Function.support (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
-- Mathlib.Algebra.CubicDiscriminant
Cubic.b_of_eq : ∀ {R : Type u_1} {P Q : Cubic R} [inst : Semiring R], P.toPoly = Q.toPoly → P.b = Q.b
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- Reindexing a matrix preserves double stochasticity.  -/
reindex_mem_doublyStochastic_iff : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {m : Type u_3} [inst_5 : Fintype m] [inst_6 : DecidableEq m]
  {M : Matrix n n R} {e₁ e₂ : n ≃ m}, (Matrix.reindex e₁ e₂) M ∈ doublyStochastic R m ↔ M ∈ doublyStochastic R n
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
/-- If `f` is absolutely continuous on `uIcc a b` and `f' x = 0` for a.e. `x ∈ uIcc a b`, then `f`
is constant on `uIcc a b`.  -/
AbsolutelyContinuousOnInterval.const_of_ae_hasDerivAt_zero : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ},
  AbsolutelyContinuousOnInterval f a b →
    (∀ᵐ (x : ℝ), x ∈ Set.uIcc a b → HasDerivAt f 0 x) → ∃ C, ∀ x ∈ Set.uIcc a b, f x = C
-- Mathlib.Data.Set.Image
Set.preimage_image_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} (s : Set α), Function.Injective f → f ⁻¹' f '' s = s
-- Mathlib.Tactic.DepRewrite
/-- `rw!` is like `rewrite!`, but also cleans up introduced refl-casts after every substitution.
It is available as an ordinary tactic and a `conv` tactic.
 -/
Mathlib.Tactic.DepRewrite.depRwSeq : Lean.ParserDescr
-- Init.Data.String.Defs
String.append_assoc : ∀ {s₁ s₂ s₃ : String}, s₁ ++ s₂ ++ s₃ = s₁ ++ (s₂ ++ s₃)
-- Init.Data.Fin.Lemmas
Fin.val_ne_iff : ∀ {n : ℕ} {a b : Fin n}, ↑a ≠ ↑b ↔ a ≠ b
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.hom_refl`. -/
CategoryTheory.Classifier.hom_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞₁ : CategoryTheory.Subobject.Classifier C),
  𝒞₁.hom 𝒞₁ = CategoryTheory.CategoryStruct.id 𝒞₁.Ω
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuous_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {z : β},
  UpperSemicontinuous fun _x => z
-- Mathlib.Order.Max
NoBotOrder.to_noMinOrder : ∀ (α : Type u_3) [inst : LinearOrder α] [NoBotOrder α], NoMinOrder α
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.range_prod_eq : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂]
  {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommGroup M₃] [inst_9 : Module R M₃] {f : M →L[R] M₂}
  {g : M →L[R] M₃}, (↑f).ker ⊔ (↑g).ker = ⊤ → (↑(f.prod g)).range = (↑f).range.prod (↑g).range
-- Std.Data.DTreeMap.Internal.Operations
/-- Internal implementation detail of the hash map  -/
Std.DTreeMap.Internal.Impl.inter : {α : Type u} →
  {β : α → Type v} →
    [Ord α] →
      (m₁ : Std.DTreeMap.Internal.Impl α β) →
        Std.DTreeMap.Internal.Impl α β → m₁.Balanced → Std.DTreeMap.Internal.Impl α β
-- Std.Time.Date.Basic
/-- Convert `Week.Offset` into `Second.Offset`.
 -/
Std.Time.Second.Offset.ofWeeks : Std.Time.Week.Offset → Std.Time.Second.Offset
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.maxD_erase_le_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α},
      (t.erase k).isEmpty = false → ∀ {fallback : α}, (cmp ((t.erase k).maxD fallback) (t.maxD fallback)).isLE = true
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.index.eq_1 : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α)
  (x : Ordinal.{u}),
  p.index x =
    Classical.epsilon fun b =>
      p.c b ∉ ⋃ j, Metric.ball (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∧ ⨆ b, p.r ↑b ≤ p.τ * p.r b
-- Std.Http.Data.Method
/-- Apply a label to a version-controlled resource baseline.
Source: https://www.rfc-editor.org/rfc/rfc3253#section-12.6
 -/
Std.Http.Method.baselineControl : Std.Http.Method
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.decodeNum.eq_def : ∀ (s : String) (p : s.Pos) (res : Lean.Name) (n : ℕ),
  Lean.Name.demangleAux.decodeNum✝ s p res n =
    if h : p = s.endPos then res.num n
    else
      have ch := p.get h;
      have p := p.next h;
      if ch.isDigit = true then Lean.Name.demangleAux.decodeNum✝ s p res (n * 10 + (ch.val - 48).toNat)
      else
        have res := res.num n;
        if h : p = s.endPos then res else Lean.Name.demangleAux.nameStart✝ s (p.next h) res
-- Mathlib.Tactic.Simps.Basic
/-- The `Simps.structureExt` environment extension specifies the preferred projections of the given
structure, used by the `@[simps]` attribute.
- You can generate this with the command `initialize_simps_projections`.
- If not generated, the `@[simps]` attribute will generate this automatically.
- To change the default value, see Note [custom simps projection].
- The first argument is the list of names of the universe variables used in the structure
- The second argument is an array that consists of the projection data for each projection.
 -/
Simps.structureExt : Lean.NameMapExtension (List Lean.Name × Array Simps.ProjectionData)
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.glueData_V : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) (x : ι × ι),
  (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).V x =
    match x with
    | (i, j) => ⋯.pullback (f j)
-- Lean.DocString.Parser
Lean.Doc.Parser.BlockCtxt.mk.injEq : ∀ (minIndent : ℕ) (maxDirective : Option ℕ) (inLists : List Lean.Doc.Parser.InList) (docStartPosition : Lean.Position)
  (baseColumn minIndent_1 : ℕ) (maxDirective_1 : Option ℕ) (inLists_1 : List Lean.Doc.Parser.InList)
  (docStartPosition_1 : Lean.Position) (baseColumn_1 : ℕ),
  ({ minIndent := minIndent, maxDirective := maxDirective, inLists := inLists, docStartPosition := docStartPosition,
        baseColumn := baseColumn } =
      { minIndent := minIndent_1, maxDirective := maxDirective_1, inLists := inLists_1,
        docStartPosition := docStartPosition_1, baseColumn := baseColumn_1 }) =
    (minIndent = minIndent_1 ∧
      maxDirective = maxDirective_1 ∧
        inLists = inLists_1 ∧ docStartPosition = docStartPosition_1 ∧ baseColumn = baseColumn_1)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filterMap!.eq_1 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] (f : (a : α) → β a → Option (γ a)),
  Std.DTreeMap.Internal.Impl.filterMap! f Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.mk.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (toHom toHom_1 : P.Hom Q) (e_toHom : toHom = toHom_1)
  (bijective_weightMap : Function.Bijective ⇑toHom.weightMap)
  (bijective_coweightMap : Function.Bijective ⇑toHom.coweightMap),
  { toHom := toHom, bijective_weightMap := bijective_weightMap, bijective_coweightMap := bijective_coweightMap } =
    { toHom := toHom_1, bijective_weightMap := ⋯, bijective_coweightMap := ⋯ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] {l : List α} {k : α},
  k ∈ t → (t.insertManyIfNewUnit l).getKey? k = t.getKey? k
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.nsmul_mod_period_vadd : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] (n : ℕ) {m : M} {a : α},
  (n % AddAction.period m a) • m +ᵥ a = n • m +ᵥ a
-- Mathlib.RingTheory.WittVector.StructurePolynomial
C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum : ∀ {p : ℕ} {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (n : ℕ),
  (∀ m < n,
      (MvPolynomial.map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) =
        wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) m) →
    MvPolynomial.C ↑(p ^ n) ∣
      (MvPolynomial.bind₁ fun b => (MvPolynomial.rename fun i => (b, i)) (wittPolynomial p ℤ n)) Φ -
        ∑ i ∈ Finset.range n, MvPolynomial.C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` preserves colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : C ⥤ Dᵒᵖ` preserves
limits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.preservesLimit_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimit K.op F.leftOp],
  CategoryTheory.Limits.PreservesLimit K F
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α},
  (t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a b : α} {fallback : β},
  (a == b) = true → Std.ExtDHashMap.Const.getD m a fallback = Std.ExtDHashMap.Const.getD m b fallback