mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
homeomorphUnitSphereProd_symm_apply_coe : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  ↑((homeomorphUnitSphereProd E).symm x) = ↑x.2 • ↑x.1
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.self_comp_coPolarization_eq_corootForm : ∀ {ι : 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] (P : RootPairing ι R M N) [inst_5 : Fintype ι],
  P.toLinearMap ∘ₗ P.CoPolarization = P.CorootForm
-- Mathlib.Data.Rat.Floor
Rat.isInt_intCeil : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] (r : R)
  (m : ℤ), Mathlib.Meta.NormNum.IsInt r m → Mathlib.Meta.NormNum.IsInt ⌈r⌉ m
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimAltInfo.mk.inj : ∀ {name : Lean.Name} {declName? : Option Lean.Name} {numFields : ℕ} {provesMotive : Bool} {name_1 : Lean.Name}
  {declName?_1 : Option Lean.Name} {numFields_1 : ℕ} {provesMotive_1 : Bool},
  { name := name, declName? := declName?, numFields := numFields, provesMotive := provesMotive } =
      { name := name_1, declName? := declName?_1, numFields := numFields_1, provesMotive := provesMotive_1 } →
    name = name_1 ∧ declName? = declName?_1 ∧ numFields = numFields_1 ∧ provesMotive = provesMotive_1
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.map_inf : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : NonUnitalSemiring B]
  [inst_6 : StarRing B] [inst_7 : Module R B] [inst_8 : FunLike F A B] [inst_9 : NonUnitalAlgHomClass F R A B]
  [inst_10 : StarHomClass F A B] [inst_11 : IsScalarTower R A A] [inst_12 : SMulCommClass R A A]
  [inst_13 : StarModule R A] [inst_14 : IsScalarTower R B B] [inst_15 : SMulCommClass R B B] [inst_16 : StarModule R B]
  (f : F),
  Function.Injective ⇑f →
    ∀ (S T : NonUnitalStarSubalgebra R A),
      NonUnitalStarSubalgebra.map f (S ⊓ T) = NonUnitalStarSubalgebra.map f S ⊓ NonUnitalStarSubalgebra.map f T
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_submatrix_sum_swap_sum_swap : ∀ {l : Type u_14} {m : Type u_15} {n : Type u_16} {o : Type u_17} {α : Type u_18} (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α),
  (Matrix.fromBlocks A B C D).submatrix Sum.swap Sum.swap = Matrix.fromBlocks D C B A
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.foldr_apply : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {l : Std.DHashMap.Internal.AssocList α β} {acc : List δ}
  (f : (a : α) → β a → δ),
  Std.DHashMap.Internal.AssocList.foldr (fun k v acc => f k v :: acc) acc l =
    List.map (fun p => f p.fst p.snd) l.toList ++ acc
-- Mathlib.Topology.Order.HullKernel
PrimitiveSpectrum.kernel.eq_1 : ∀ {α : Type u_1} [inst : CompleteLattice α] {T : Set α} (S : Set ↑T),
  PrimitiveSpectrum.kernel S = sInf (Subtype.val '' S)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swap.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Sort u_2) (x x_1 : ℕ) (h_1 : (x x_2 : ℕ) → motive [] x x_2)
  (h_2 : (a : α) → (xs : List α) → motive (a :: xs) 0 0)
  (h_3 : (a : α) → (xs : List α) → (i : ℕ) → motive (a :: xs) 0 i.succ)
  (h_4 : (a : α) → (xs : List α) → (i : ℕ) → motive (a :: xs) i.succ 0)
  (h_5 : (a : α) → (xs : List α) → (i j : ℕ) → motive (a :: xs) i.succ j.succ),
  (match [], x, x_1 with
    | [], x, x_2 => h_1 x x_2
    | a :: xs, 0, 0 => h_2 a xs
    | a :: xs, 0, i.succ => h_3 a xs i
    | a :: xs, i.succ, 0 => h_4 a xs i
    | a :: xs, i.succ, j.succ => h_5 a xs i j) =
    h_1 x x_1
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_eq_cfcₙ_norm : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A),
  autoParam (IsSelfAdjoint a) CFC.abs_eq_cfcₙ_norm._auto_1 → CFC.abs a = cfcₙ (fun x => ‖x‖) a
-- Mathlib.Order.RelSeries
RelSeries.reverse_reverse : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.reverse.reverse = p
-- Init.Data.BEq
BEq.congr_right : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {a b c : α}, (b == c) = true → (a == b) = (a == c)
-- Mathlib.Probability.ProbabilityMassFunction.Monad
/-- The monadic bind operation for `PMF`.  -/
PMF.bind : {α : Type u_1} → {β : Type u_2} → PMF α → (α → PMF β) → PMF β
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.comp_continuousOn_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h : X ≃ₜ Y) (f : Z → X) (s : Set Z), ContinuousOn (⇑h ∘ f) s ↔ ContinuousOn f s
-- Lean.Elab.MutualInductive
/-- An intermediate step for mutual inductive elaboration. See `InductiveElabDescr`  -/
Lean.Elab.Command.InductiveElabStep3 : Type
-- Mathlib.Data.Analysis.Topology
LocallyFinite.Realizer.bas : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      {F : Ctop.Realizer α} → {f : β → Set α} → LocallyFinite.Realizer F f → (a : α) → { s // a ∈ F.F.f s }
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaSubtype_apply : ∀ {α : Type u_9} {β : α → Type u_10} (a : α) (x : { s // s.fst = a }),
  (Equiv.sigmaSubtype a) x =
    match x with
    | ⟨⟨fst, b⟩, h⟩ => h ▸ b
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
CategoryTheory.Limits.PreservesColimitsOfSize.underPost : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, max u₁ v₁, max u₂ v₂} (CategoryTheory.Under.post F)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.modify_eq_empty_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, t.modify k f = ∅ ↔ t = ∅
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- A modification `Γ` between strong transformations (of pseudofunctors) `η` and `θ` consists of a
family of 2-morphisms `Γ.app a : η.app a ⟶ θ.app a`, which satisfies the equation
`(F.map f ◁ app b) ≫ (θ.naturality f).hom = (η.naturality f).hom ≫ (app a ▷ G.map f)`
for each 1-morphism `f : a ⟶ b`.
 -/
CategoryTheory.Pseudofunctor.StrongTrans.Modification : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} → (F ⟶ G) → (F ⟶ G) → Type (max u₁ w₂)
-- Mathlib.Order.WithBot
WithBot.decidableLE.eq_3 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (a b : α),
  WithBot.decidableLE (some a) (some b) = decidable_of_iff' (a ≤ b) ⋯
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.ofEq.injEq : ∀ (x : Int.Internal.Linear.Var) (c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (x_1 : Int.Internal.Linear.Var)
  (c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.ofEq x c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.ofEq x_1 c_1) =
    (x = x_1 ∧ c = c_1)
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
OrderDual.instIsLeftCancelMulZero : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [IsLeftCancelMulZero α], IsLeftCancelMulZero αᵒᵈ
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.SigmaFinite.out' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.SigmaFinite μ],
  Nonempty (μ.FiniteSpanningSetsIn Set.univ)
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.Nondegenerate.mul_iff_left : ∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : CommRing A] [IsDomain A] {M N : Matrix n n A},
  M.Nondegenerate → ((M * N).Nondegenerate ↔ N.Nondegenerate)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsometricContinuousFunctionalCalculus.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (p p_1 : A → Prop),
  p = p_1 →
    ∀ [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R]
      [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A] [inst_7 : MetricSpace A]
      [inst_8 : Algebra R A],
      IsometricContinuousFunctionalCalculus R A p = IsometricContinuousFunctionalCalculus R A p_1
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- The indicator of a disjoint union of two sets is the sum of the indicators of the sets.  -/
MeasureTheory.indicatorConstLp_disjoint_union : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤)
  (hμt : μ t ≠ ⊤),
  Disjoint s t →
    ∀ (c : E),
      MeasureTheory.indicatorConstLp p ⋯ ⋯ c =
        MeasureTheory.indicatorConstLp p hs hμs c + MeasureTheory.indicatorConstLp p ht hμt c
-- Mathlib.Analysis.Normed.Group.Basic
edist_one_right : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), edist a 1 = ‖a‖ₑ
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_iff_tendsto_subseq_of_antitone : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} {α : Type u_5} [inst : SemilatticeSup ι₁] [inst_1 : Preorder ι₂] [Nonempty ι₁]
  [inst_3 : TopologicalSpace α] [inst_4 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [NoMinOrder α]
  {f : ι₂ → α} {φ : ι₁ → ι₂} {l : α},
  Antitone f →
    Filter.Tendsto φ Filter.atTop Filter.atTop →
      (Filter.Tendsto f Filter.atTop (nhds l) ↔ Filter.Tendsto (f ∘ φ) Filter.atTop (nhds l))
-- Init.Data.List.Nat.Find
List.findIdx?_eq_some_le_of_findIdx?_eq_some : ∀ {α : Type u_1} {xs : List α} {p q : α → Bool},
  (∀ x ∈ xs, p x = true → q x = true) → ∀ {i : ℕ}, List.findIdx? p xs = some i → ∃ j ≤ i, List.findIdx? q xs = some j
-- Mathlib.Algebra.GroupWithZero.Associated
Irreducible.dvd_irreducible_iff_associated : ∀ {M : Type u_1} [inst : Monoid M] {p q : M}, Irreducible p → Irreducible q → (p ∣ q ↔ Associated p q)
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instAddCommGroup : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → AddCommGroup (ModularForm Γ k)
-- Mathlib.Topology.Homotopy.Basic
/-- If two maps are homotopic relative to a set, then they are homotopic.  -/
ContinuousMap.HomotopicRel.homotopic : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {S : Set X} {f₀ f₁ : C(X, Y)},
  f₀.HomotopicRel f₁ S → f₀.Homotopic f₁
-- Mathlib.CategoryTheory.Sites.EpiMono
CategoryTheory.Sheaf.instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [inst_4 : J.WEqualsLocallyBijective A]
  (data : CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A)
  [inst_5 : CategoryTheory.HasWeakSheafify J A] (f : CategoryTheory.Arrow (CategoryTheory.Sheaf J A)),
  CategoryTheory.Sheaf.IsLocallyInjective
    ((CategoryTheory.Sheaf.functorialLocallySurjectiveInjectiveFactorization J data).p.app f)
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.le_iff_of_unique : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : LinearOrder α] [inst_2 : Unique α] [inst_3 : PartialOrder N]
  {x y : Lex (α →₀ N)}, x ≤ y ↔ (ofLex x) default ≤ (ofLex y) default
-- Mathlib.RingTheory.Ideal.Defs
Ideal.isTwoSided_iff : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α), I.IsTwoSided ↔ ∀ {a : α} (b : α), a ∈ I → a * b ∈ I
-- Mathlib.Topology.Instances.ENNReal.Lemmas
LipschitzOnWith.closure : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {s : Set α}
  {K : NNReal}, ContinuousOn f (closure s) → LipschitzOnWith K f s → LipschitzOnWith K f (closure s)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Equiv.Perm.sum_comp' : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (σ : Equiv.Perm ι) (s : Finset ι) (f : ι → ι → M),
  {a | σ a ≠ a} ⊆ ↑s → ∑ x ∈ s, f (σ x) x = ∑ x ∈ s, f x ((Equiv.symm σ) x)
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Factors.finiteDimensional_quotient_pow : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : IsDedekindDomain S] [Module.Finite R S] [inst_5 : p.IsMaximal]
  (P : ↥(UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset),
  FiniteDimensional (R ⧸ p) (S ⧸ ↑P ^ p.ramificationIdx' ↑P)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLE_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (a b : ℤ) [t.IsLE X b], t.IsLE ((t.truncLE a).obj X) b
-- Init.Data.Int.Order
Int.sub_one_lt_iff : ∀ {m n : ℤ}, m - 1 < n ↔ m ≤ n
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
AdicCompletion.tensor_map_id_left_injective_of_injective : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) [IsNoetherianRing R] {M : Type u} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {N : Type u} [inst_4 : AddCommGroup N] [inst_5 : Module R N] {f : M →ₗ[R] N} [Module.Finite R M]
  [Module.Finite R N],
  Function.Injective ⇑f → Function.Injective ⇑(TensorProduct.AlgebraTensorModule.map LinearMap.id f)
-- Lean.ReservedNameAction
/-- When trying to resolve a reserved name, an action can be executed to generate the actual definition/theorem.
The action returns `true` if it "handled" the given name.

Remark: usually when one install a reserved name predicate, an associated action is also installed.
 -/
Lean.ReservedNameAction : Type
-- Mathlib.RingTheory.IsPrimary
/-- A proper submodule `S : Submodule R M` is primary iff
`r • x ∈ S` implies `x ∈ S` or `∃ n : ℕ, r ^ n • (⊤ : Submodule R M) ≤ S`.
This generalizes `Ideal.IsPrimary`.  -/
Submodule.IsPrimary : {R : Type u_1} →
  {M : Type u_2} → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Prop
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.order_neg : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddGroup R] [inst_2 : Zero Γ] {f : HahnSeries Γ R},
  (-f).order = f.order
-- Mathlib.Data.Fintype.CardEmbedding
Fintype.card_embedding_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] [emb : Fintype (α ↪ β)],
  Fintype.card (α ↪ β) = (Fintype.card β).descFactorial (Fintype.card α)
-- Std.Time.Date.Unit.Month
Std.Time.Month.instDecidableLeOffset : {x y : Std.Time.Month.Offset} → Decidable (x ≤ y)
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.eraseIdx.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (head : α) (as : List α) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (head : α) → (as : List α) → motive (head :: as) 0)
  (h_3 : (a : α) → (as : List α) → (n : ℕ) → motive (a :: as) n.succ),
  (match head :: as, 0 with
    | [], x => h_1 x
    | head :: as, 0 => h_2 head as
    | a :: as, n.succ => h_3 a as n) =
    h_2 head as
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.sumProdDistrib_apply : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (a : (X ⊕ Y) × Z), Homeomorph.sumProdDistrib a = (Equiv.sumProdDistrib X Y Z) a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).get? k = none
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_total_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f i) (CategoryTheory.Limits.biprod.inl.f i) +
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) (CategoryTheory.Limits.biprod.inr.f i) =
    CategoryTheory.CategoryStruct.id ((K ⊞ L).X i)
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring T] [inst_4 : Algebra R T],
  ↑(Algebra.TensorProduct.linearEquivIncludeRange R S T) =
    TensorProduct.map Algebra.TensorProduct.includeLeft.toLinearMap.rangeRestrict
      Algebra.TensorProduct.includeRight.toLinearMap.rangeRestrict
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKeyD.eq_1 : ∀ {α : Type u} {β : α → Type v} (x : α), Std.DTreeMap.Internal.Impl.leaf.maxKeyD x = x
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The linear span of a generating convex cone equals top.  -/
ConvexCone.IsGenerating.span_eq_top : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {C : ConvexCone R M}, C.IsGenerating → Submodule.span R ↑C = ⊤
-- Mathlib.Analysis.Quaternion
Quaternion.continuous_normSq : Continuous ⇑Quaternion.normSq
-- Mathlib.Order.Monotone.Basic
/-- If `α` is a preorder with no maximal elements, then there exists a strictly antitone function
`ℕ → α` with any prescribed value of `f 0`.  -/
Nat.exists_strictAnti' : ∀ {α : Type u} [inst : Preorder α] [NoMinOrder α] (a : α), ∃ f, StrictAnti f ∧ f 0 = a
-- Init.Prelude
/-- Create array `#[a₁]`  -/
Array.mkArray1 : {α : Type u} → α → Array α
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.generator_lt_one : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [inst_2 : v.IsRankOneDiscrete], Valuation.IsRankOneDiscrete.generator v < 1
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- The left unitor: `𝟙 a ≫ f ≅ f`  -/
CategoryTheory.Bicategory.«termλ_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.pre_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A₁ A₂ A₃ : C}
  [inst_2 : CategoryTheory.Closed A₁] [inst_3 : CategoryTheory.Closed A₂] [inst_4 : CategoryTheory.Closed A₃]
  (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃),
  CategoryTheory.MonoidalClosed.pre (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.pre g) (CategoryTheory.MonoidalClosed.pre f)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.dist_lt_add_of_nonempty_closedBall_inter_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ},
  (Metric.closedBall x ε₁ ∩ Metric.ball y ε₂).Nonempty → dist x y < ε₁ + ε₂
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_boole_mul : ∀ {ι : Type u_1} {K : Type u_3} [inst : Semifield K] [inst_1 : CharZero K] [inst_2 : Fintype ι] [Nonempty ι]
  [inst_4 : DecidableEq ι] (f : ι → K) (i : ι),
  (Finset.univ.expect fun j => (if i = j then ↑(Fintype.card ι) else 0) * f j) = f i
-- Mathlib.Data.Nat.Factorization.Divisors
Nat.divisors_eq_map_attach_Iic_factorization_prod_pow : ∀ {n : ℕ},
  n ≠ 0 →
    n.divisors =
      Finset.map { toFun := fun x => (↑x).prod fun x1 x2 => x1 ^ x2, inj' := ⋯ } (Finset.Iic n.factorization).attach
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- For `1 < s.re`, the Dirichlet L-function is the exponential of the `L`-series of
`n ↦ χ n * Λ n / Real.log n`.
 -/
DirichletCharacter.LSeries_eq_exp_LSeries : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ},
  1 < s.re →
    Complex.exp (LSeries (fun n => χ ↑n * ↑(ArithmeticFunction.vonMangoldt n) / ↑(Real.log ↑n)) s) =
      LSeries (fun n => χ ↑n) s
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.left_le_sup : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f g : E →ₛₗ.[σ] F)
  (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y), f ≤ f.sup g h
-- Init.Data.Range.Polymorphic.Iterators
Std.Roc.Internal.iter.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (r : Std.Roc α),
  Std.Roc.Internal.iter r = { internalState := { next := Std.PRange.succ? r.lower, upperBound := r.upper } }
-- Mathlib.CategoryTheory.Adjunction.Comma
CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor D C)
  [inst_2 : ∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)] (B : D) (A : C)
  (g : G.obj B ⟶ A),
  (CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux G B A) g =
    (CategoryTheory.Limits.terminal.from (CategoryTheory.CostructuredArrow.mk g)).left
-- Mathlib.GroupTheory.CoprodI
/-- The Ping-Pong-Lemma.

Given a group action of `G` on `X` so that the generators of the free groups act in specific
ways on disjoint subsets `X i` and `Y i` we can prove that `lift f` is injective, and thus the image
of `lift f` is isomorphic to the free group.

Often the Ping-Pong-Lemma is stated with regard to group elements that generate the whole group;
we generalize to arbitrary group homomorphisms from the free group to `G` and do not require the
group to be generated by the elements.
 -/
FreeGroup.injective_lift_of_ping_pong : ∀ {ι : Type u_1} [Nontrivial ι] {G : Type u_1} [inst : Group G] (a : ι → G) {α : Type u_4} [inst_1 : MulAction G α]
  (X Y : ι → Set α),
  (∀ (i : ι), (X i).Nonempty) →
    Pairwise (Function.onFun Disjoint X) →
      Pairwise (Function.onFun Disjoint Y) →
        (∀ (i j : ι), Disjoint (X i) (Y j)) →
          (∀ (i : ι), a i • (Y i)ᶜ ⊆ X i) → (∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i) → Function.Injective ⇑(FreeGroup.lift a)
-- Lean.Meta.Tactic.Assert
/-- Convert the given goal `Ctx |- target` into `Ctx |- (hName : type) -> hName = val -> target`.
It assumes `val` has type `type`  -/
Lean.MVarId.assertExt : Lean.MVarId → Lean.Name → Lean.Expr → Lean.Expr → optParam Lean.Name `h → Lean.MetaM Lean.MVarId
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.unpair₁ : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ}, Nat.Primrec' f → Nat.Primrec' fun v => (Nat.unpair (f v)).1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.mul : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Semigroup α] {a b : α},
  MulLECancellable a → MulLECancellable b → MulLECancellable (a * b)
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_eq_biInter_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E),
  B.polar s = ⋂ x ∈ s, ⇑(B x) ⁻¹' Metric.closedBall 0 1
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (f : J → C) (X : C),
  CategoryTheory.rightDistributor f X = CategoryTheory.rightDistributor f X