mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- The right uniformity on a topological additive group (as opposed to the left
uniformity).

Warning: in general the right and left uniformities do not coincide and so one does not obtain a
`IsUniformAddGroup` structure. Two important special cases where they _do_ coincide are for
commutative additive groups (see `isUniformAddGroup_of_addCommGroup`) and for compact
additive groups (see `IsUniformAddGroup.of_compactSpace`).  -/
IsTopologicalAddGroup.rightUniformSpace : (G : Type u_1) → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [IsTopologicalAddGroup G] → UniformSpace G
-- Batteries.Data.Array.Match
Array.PrefixTable.step.eq_def : ∀ {α : Type u_1} [inst : BEq α] (t : Array.PrefixTable α) (x : α) (x_1 : Fin (t.size + 1)),
  t.step x x_1 =
    match x_1 with
    | ⟨k, hk⟩ =>
      have cont := fun x_2 =>
        match k, hk with
        | 0, hk => ⟨0, ⋯⟩
        | k.succ, hk =>
          have h2 := ⋯;
          let k' := t.toArray[k].2;
          have hk' := ⋯;
          t.step x ⟨k', ⋯⟩;
      if hsz : k < t.size then if (x == t.toArray[k].1) = true then ⟨k + 1, ⋯⟩ else cont () else cont ()
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.selfEquivOrbitsQuotientProd.eq_1 : ∀ {G : Type u} {X : Type v} [inst : Group G] [inst_1 : MulAction G X] (h : ∀ (b : X), MulAction.stabilizer G b = ⊥),
  MulAction.selfEquivOrbitsQuotientProd h = MulAction.selfEquivOrbitsQuotientProd' ⋯ h
-- Mathlib.Order.Category.DistLat
DistLat.dualEquiv_inverse : DistLat.dualEquiv.inverse = DistLat.dual
-- Std.Internal.UV.Loop
/-- Options for configuring the event loop behavior.
 -/
Std.Internal.UV.Loop.Options : Type
-- Mathlib.Data.Option.NAry
Option.map₂_swap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : Option α) (b : Option β),
  Option.map₂ f a b = Option.map₂ (fun a b => f b a) b a
-- Init.Data.SInt.Lemmas
Int32.toBitVec_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toBitVec = OfNat.ofNat n
-- Std.Do.SPred.SPred
Std.Do.SPred.or_cons : ∀ {σs : List (Type u)} {σ : Type u} {s : σ} {P Q : Std.Do.SPred (σ :: σs)}, spred(P ∨ Q) s = spred(P s ∨ Q s)
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.AEEqFun.Integrable.sub : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f g : α →ₘ[μ] β}, f.Integrable → g.Integrable → (f - g).Integrable
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- If every `x` has a neighbourhood on which `b ↦ ∑' i, f i b`
converges uniformly to `g`, then the sum converges locally uniformly. Note that this is not a
tautology, and the converse is only true if the domain is locally compact.  -/
hasSumLocallyUniformly_of_of_forall_exists_nhds : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  (∀ (x : β), ∃ t ∈ nhds x, HasSumUniformlyOn f g t) → HasSumLocallyUniformly f g
-- Mathlib.GroupTheory.PGroup
ZModModule.isPGroup_multiplicative : ∀ {n : ℕ} {G : Type u_2} [inst : AddCommGroup G] [Module (ZMod n) G], IsPGroup n (Multiplicative G)
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of the reverse direction of `indiscreteTopology_iff_forall_norm_eq_zero`. -/
IndiscreteTopology.of_forall_norm_eq_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], (∀ (x : E), ‖x‖ = 0) → IndiscreteTopology E
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Composition of two equivariant additive monoid homomorphisms.  -/
DistribMulActionHom.comp : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {P : Type u_3} →
          [inst_2 : Monoid P] →
            {φ : M →* N} →
              {ψ : N →* P} →
                {χ : M →* P} →
                  {A : Type u_4} →
                    [inst_3 : AddMonoid A] →
                      [inst_4 : DistribMulAction M A] →
                        {B : Type u_5} →
                          [inst_5 : AddMonoid B] →
                            [inst_6 : DistribMulAction N B] →
                              {C : Type u_7} →
                                [inst_7 : AddMonoid C] →
                                  [inst_8 : DistribMulAction P C] →
                                    [κ : φ.CompTriple ψ χ] → (B →ₑ+[ψ] C) → (A →ₑ+[φ] B) → A →ₑ+[χ] C
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_minKey!_eq_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Inhabited α] (h : t.WF) {hc : Std.DTreeMap.Internal.Impl.contains t.minKey! t = true},
  t.getKey t.minKey! hc = t.minKey ⋯
-- Mathlib.Logic.Equiv.Set
/-- The set product of two sets is equivalent to the type product of their coercions to types.  -/
Equiv.Set.prod : {α : Type u_3} → {β : Type u_4} → (s : Set α) → (t : Set β) → ↑(s ×ˢ t) ≃ ↑s × ↑t
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.adj_of_mem_incidenceSet : ∀ {V : Type u} (G : SimpleGraph V) {a b : V} {e : Sym2 V},
  a ≠ b → e ∈ G.incidenceSet a → e ∈ G.incidenceSet b → G.Adj a b
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.projr_surjective : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K),
  Function.Surjective ⇑(LieAlgebra.SemiDirectSum.projr ψ)
-- Mathlib.Analysis.Normed.Ring.TransferInstance
/-- Transfer a `NormedRing` across an `Equiv`  -/
Equiv.normedRing : {α : Type u_1} → {β : Type u_2} → [NormedRing β] → α ≃ β → NormedRing α
-- Mathlib.CategoryTheory.Filtered.Basic
/-- For every span `j ⟵ i ⟶ j'`, there exists a cocone `j ⟶ k ⟵ j'` such that the square
commutes.  -/
CategoryTheory.IsFiltered.span : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {i j j' : C} (f : i ⟶ j)
  (f' : i ⟶ j'), ∃ k g g', CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
-- Init.Prelude
/-- Similar to `congrFun` but `β` does not depend on `α`.  -/
congrFun' : ∀ {α : Sort u} {β : Sort v} {f g : α → β}, f = g → ∀ (a : α), f a = g a
-- Init.System.IO
IO.Process.Stdio.null.sizeOf_spec : sizeOf IO.Process.Stdio.null = 1
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.whisker_left : ∀ {B : Type u} [inst : Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  (g h : CategoryTheory.FreeBicategory.Hom b c) (η η' : CategoryTheory.FreeBicategory.Hom₂ g h),
  CategoryTheory.FreeBicategory.Rel η η' →
    CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_left f η)
      (CategoryTheory.FreeBicategory.Hom₂.whisker_left f η')
-- Mathlib.Order.Std
/-- Create a `PartialOrder` from a type satisfying `Std.IsPartialOrder`.

If an `LE` instance exists, either an `Std.IsPartialOrder` instance must exist, or there must be an
`Ord` instance together with `Std.LawfulOrderOrd`, `Std.LawfulEqOrd`, and `Std.TransOrd` instances.

If no `LE` instance exists, it can be generated from `Ord`, `Std.LawfulEqOrd`, and `Std.TransOrd`
instances.

If an `LT` instance exists, an `Std.LawfulOrderLT` instance must exist also; otherwise, a suitable
`LT` instance will be generated.  -/
PartialOrder.ofStd : (α : Type u_1) → autoParam (PartialOrder.OfStdArgs α) PartialOrder.ofStd._auto_1 → PartialOrder α
-- Mathlib.Algebra.Order.Kleene
KleeneAlgebra.kstar_mul_le_self : ∀ {α : Type u_5} [self : KleeneAlgebra α] (a b : α), a * b ≤ b → KStar.kstar a * b ≤ b
-- Mathlib.Algebra.Module.LocalizedModule.Away
IsLocalizedModule.Away.of_associated : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {f : M →ₗ[R] N} {r r' : R},
  Associated r r' → ∀ [IsLocalizedModule.Away r f], IsLocalizedModule.Away r' f
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLineRange : Lean.ToJson Lean.Lsp.LineRange
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
ConditionallyCompleteLattice.mk : {α : Type u_5} →
  [toLattice : Lattice α] →
    [toSupSet : SupSet α] →
      [toInfSet : InfSet α] →
        (∀ (s : Set α), s.Nonempty → BddAbove s → IsLUB s (sSup s)) →
          (∀ (s : Set α), s.Nonempty → BddBelow s → IsGLB s (sInf s)) → ConditionallyCompleteLattice α
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_map_dedup_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α → β) (s : Multiset α),
  (Multiset.map f s.dedup).dedup = (Multiset.map f s).dedup
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.le_of_ne_zero : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Zero 𝕜] [inst_1 : LE α] {a b : α} {f : IncidenceAlgebra 𝕜 α}, f a b ≠ 0 → a ≤ b
-- Init.Data.List.Range
List.map_add_range' : ∀ {a : ℕ} (s n step : ℕ), List.map (fun x => a + x) (List.range' s n step) = List.range' (a + s) n step
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Internal.optionPelim'.eq_2 : ∀ {α : Type u_1} {β : Sort u_2} (n_2 : none = none → β) (s_2 : (val : α) → none = some val → β),
  Std.Internal.optionPelim'✝ none n_2 s_2 = n_2 ⋯
-- Mathlib.Algebra.Order.Group.Defs
eq_one_of_inv_eq' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {a : α}, a⁻¹ = a → a = 1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `right` co(ntra)variant.  -/
Right.neg_neg_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a : α}, -a < 0 ↔ 0 < a
-- Init.Data.Vector.Basic
Vector.drop.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (i : ℕ), xs.drop i = Vector.mk (xs.toArray.drop i) ⋯
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.instReprArgSpec.repr.match_1.eq_3 : ∀ (motive : Lean.Doc.ArgSpec✝ → Sort u_1) (a : Lean.Name) (a_1 : Lean.Expr)
  (h_1 : (a : Lean.Name) → (a_2 : Lean.Expr) → motive (Lean.Doc.ArgSpec.positional✝ a a_2))
  (h_2 : (a : Lean.Name) → (a_2 a_3 : Lean.Expr) → motive (Lean.Doc.ArgSpec.named✝ a a_2 a_3))
  (h_3 : (a : Lean.Name) → (a_2 : Lean.Expr) → motive (Lean.Doc.ArgSpec.many✝ a a_2))
  (h_4 : (a : Lean.Name) → (a_2 : Bool) → motive (Lean.Doc.ArgSpec.flag✝ a a_2)),
  (match Lean.Doc.ArgSpec.many✝ a a_1 with
    | Lean.Doc.ArgSpec.positional✝ a a_2 => h_1 a a_2
    | Lean.Doc.ArgSpec.named✝ a a_2 a_3 => h_2 a a_2 a_3
    | Lean.Doc.ArgSpec.many✝ a a_2 => h_3 a a_2
    | Lean.Doc.ArgSpec.flag✝ a a_2 => h_4 a a_2) =
    h_3 a a_1
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.update_def : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n : ℕ) (a : R),
  p.update n a = SkewMonoidAlgebra.update p (Multiplicative.ofAdd n) a
-- Mathlib.Topology.NhdsWithin
Set.EqOn.eventuallyEq_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f g : α → β} {s : Set α} {a : α},
  Set.EqOn f g s → f =ᶠ[nhdsWithin a s] g
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` reflects colimits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.leftOp : Cᵒᵖ ⥤ D`
reflects limits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.reflectsLimit_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.ReflectsColimit K.leftOp F],
  CategoryTheory.Limits.ReflectsLimit K F.leftOp
-- Mathlib.Topology.EMetricSpace.BoundedVariation
LipschitzOnWith.comp_boundedVariationOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {F : Type u_3}
  [inst_2 : PseudoEMetricSpace F] {f : E → F} {C : NNReal} {t : Set E},
  LipschitzOnWith C f t →
    ∀ {g : α → E} {s : Set α}, Set.MapsTo g s t → BoundedVariationOn g s → BoundedVariationOn (f ∘ g) s
-- Mathlib.Order.RelIso.Basic
RelIso.coe_symm_toMap : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α ≃ β), ⇑(RelIso.toMap r f).symm = ⇑f.symm
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.tendsto_toReal_atTop : Filter.Tendsto EReal.toReal (nhdsWithin ⊤ {⊤}ᶜ) Filter.atTop
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.sum_eapproxDiff : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → ENNReal) (n : ℕ) (a : α),
  ∑ k ∈ Finset.range (n + 1), ↑((MeasureTheory.SimpleFunc.eapproxDiff f k) a) = (MeasureTheory.SimpleFunc.eapprox f n) a
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.left_unitor_inv_apply : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {X : (i : I) → C i} {i : I},
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv i =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X i)).inv
-- Mathlib.Tactic.ReduceModChar
Tactic.ReduceModChar.TypeToCharPResult.intLike.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {n : Q(ℕ)} {instRing : Q(Ring «$α»)} {instCharP : Q(CharP «$α» «$n»)} {n_1 : Q(ℕ)}
  {instRing_1 : Q(Ring «$α»)} {instCharP_1 : Q(CharP «$α» «$n_1»)},
  Tactic.ReduceModChar.TypeToCharPResult.intLike n instRing instCharP =
      Tactic.ReduceModChar.TypeToCharPResult.intLike n_1 instRing_1 instCharP_1 →
    n = n_1 ∧ instRing = instRing_1 ∧ instCharP = instCharP_1
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `⨅ i, f i = 0` when the real-valued function `f` is unbounded below,
it suffices to show that `f` takes a nonpositive value to show that `0 ≤ ⨅ i, f i`.  -/
Real.iInf_nonpos' : ∀ {ι : Sort u_1} {f : ι → ℝ}, (∃ i, f i ≤ 0) → ⨅ i, f i ≤ 0
-- Mathlib.Algebra.Homology.Localization
/-- The canonical isomorphism `HomotopyCategory.quotient C c ⋙ Qh ≅ Q`.  -/
HomologicalComplexUpToQuasiIso.quotientCompQhIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {ι : Type u_2} →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Preadditive C] →
          [inst_2 : CategoryTheory.CategoryWithHomology C] →
            [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] →
              [inst_4 : c.QFactorsThroughHomotopy C] →
                (HomotopyCategory.quotient C c).comp HomologicalComplexUpToQuasiIso.Qh ≅
                  HomologicalComplexUpToQuasiIso.Q
-- Mathlib.LinearAlgebra.Quotient.Bilinear
LinearMap.liftQ₂_mk : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} {M : Type u_5} {N : Type u_6} {P : Type u_7}
  [inst : Ring R] [inst_1 : Ring R₂] [inst_2 : Ring S] [inst_3 : Ring S₂] [inst_4 : AddCommGroup M]
  [inst_5 : AddCommGroup N] [inst_6 : AddCommGroup P] [inst_7 : Module R M] [inst_8 : Module S N] [inst_9 : Module R₂ P]
  [inst_10 : Module S₂ P] [inst_11 : SMulCommClass R₂ S₂ P] {ρ : R →+* R₂} {σ : S →+* S₂} {M' : Submodule R M}
  {N' : Submodule S N} {f : M →ₛₗ[ρ] N →ₛₗ[σ] P} (hM' : M' ≤ f.ker) (hN' : N' ≤ f.flip.ker) (m : M) (n : N),
  ((LinearMap.liftQ₂ M' N' f hM' hN') (Submodule.Quotient.mk m)) (Submodule.Quotient.mk n) = (f m) n
-- Mathlib.Topology.UniformSpace.Equicontinuity
EquicontinuousAt.eq_1 : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] (F : ι → X → α) (x₀ : X),
  EquicontinuousAt F x₀ = ∀ U ∈ uniformity α, ∀ᶠ (x : X) in nhds x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
-- Lean.Elab.Tactic.Omega.Frontend
/-- Translates an expression into a `LinearCombo`.
Also returns:
* a proof that this linear combo evaluated at the atoms is equal to the original expression
* a list of new facts which should be recorded:
  * for each new atom `a` of the form `((x : Nat) : Int)`, the fact that `0 ≤ a`
  * for each new atom `a` of the form `x / k`, for `k` a positive numeral, the facts that
    `k * a ≤ x < (k + 1) * a`
  * for each new atom of the form `((a - b : Nat) : Int)`, the fact:
    `b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0`

We also transform the expression as we descend into it:
* pushing coercions: `↑(x + y)`, `↑(x * y)`, `↑(x / k)`, `↑(x % k)`, `↑k`
* unfolding `emod`: `x % k` → `x - x / k`
 -/
Lean.Elab.Tactic.Omega.asLinearComboImpl : Lean.Expr →
  Lean.Elab.Tactic.Omega.OmegaM (Lean.Omega.LinearCombo × Lean.Elab.Tactic.Omega.OmegaM Lean.Expr × List Lean.Expr)
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.eval₂_eq_tsum : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {φ : R →+* S} {a : S}
  [inst_2 : UniformSpace R] [inst_3 : UniformSpace S] [IsUniformAddGroup R] [IsTopologicalSemiring R]
  [IsUniformAddGroup S] [T2Space S] [CompleteSpace S] [IsTopologicalRing S] [IsLinearTopology S S],
  Continuous ⇑φ →
    PowerSeries.HasEval a →
      ∀ (f : PowerSeries R), PowerSeries.eval₂ φ a f = ∑' (d : ℕ), φ ((PowerSeries.coeff d) f) * a ^ d
-- Mathlib.Data.Set.Card
Set.InjOn.ncard_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s → (f '' s).ncard = s.ncard
-- Mathlib.RingTheory.Ideal.Over
Ideal.ne_top_iff_of_liesOver : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [P.LiesOver p], P ≠ ⊤ ↔ p ≠ ⊤
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryLED_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : α × β},
  t₁.Equiv t₂ → Std.DTreeMap.Const.getEntryLED t₁ k fallback = Std.DTreeMap.Const.getEntryLED t₂ k fallback
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  (ι : Type u_2) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S) (X_1 : ↑(F.obj { as := Opposite.op S }).obj),
  ((CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso ι f).inv.app X_1).f =
    CategoryTheory.CategoryStruct.id ((F.map f.op.toLoc).l.toFunctor.obj X_1)
-- Mathlib.Logic.Basic
/-- **Alias** of `forall₂_comm`. -/
forall₂_swap : ∀ {ι₁ : Sort u_3} {ι₂ : Sort u_4} {κ₁ : ι₁ → Sort u_5} {κ₂ : ι₂ → Sort u_6}
  {p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop},
  (∀ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) ↔
    ∀ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.tensorAlgEquiv.eq_1 : ∀ {R : Type u_6} {S : Type u_7} {T : Type u_8} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (p : Polynomial S) (q : Polynomial (TensorProduct R T S))
  (h : Polynomial.map Algebra.TensorProduct.includeRight.toRingHom p = q),
  AdjoinRoot.tensorAlgEquiv p q h =
    AlgEquiv.ofAlgHom
      (Algebra.TensorProduct.lift (Algebra.algHom T T (AdjoinRoot q))
        (AdjoinRoot.mapAlgHom Algebra.TensorProduct.includeRight p q ⋯) ⋯)
      (AdjoinRoot.liftAlgHom q
        (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (Algebra.ofId S (AdjoinRoot p))))
        (1 ⊗ₜ[R] AdjoinRoot.root p) ⋯)
      ⋯ ⋯
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T U : CategoryTheory.Over X} (f : R ⟶ S) (g : T ⟶ U),
  CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    CategoryTheory.ChosenPullbacksAlong.pullbackMap S.hom U.hom R.hom T.hom (CategoryTheory.Over.Hom.left f)
      (CategoryTheory.Over.Hom.left g) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.equivSubgroupOrbitsQuotientGroup.eq_1 : ∀ {G : Type u} {X : Type v} [inst : Group G] [inst_1 : MulAction G X] (x : X) [inst_2 : MulAction.IsPretransitive G X]
  [inst_3 : IsCancelSMul G X] (H : Subgroup G),
  MulAction.equivSubgroupOrbitsQuotientGroup x H =
    { toFun := fun q => Quotient.liftOn' q (fun y => ↑⋯.choose) ⋯,
      invFun := fun q => Quotient.liftOn' q (fun g => ⟦g⁻¹ • x⟧) ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Data.Prod.TProd
List.TProd.ext_iff : ∀ {ι : Type u} {α : ι → Type v} [inst : DecidableEq ι] {l : List ι} {x : l.Nodup} {v w : List.TProd α l},
  v = w ↔ ∀ (i : ι) (hi : i ∈ l), v.elim hi = w.elim hi
-- Init.Data.Vector.Lemmas
Vector.mem_of_contains_eq_true : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [LawfulBEq α] {a : α} {as : Vector α n}, as.contains a = true → a ∈ as
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTrivAt_snd : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (b : B) (p : Bundle.TotalSpace F Z.Fiber),
  (↑(Z.localTrivAt b) p).2 = Z.coordChange (Z.indexAt p.proj) (Z.indexAt b) p.proj p.snd
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
/-- The function `tan` is meromorphic.  -/
Complex.meromorphic_tan : Meromorphic Complex.tan
-- Mathlib.Algebra.Order.Group.Synonym
isAddLeftRegular_ofColex : ∀ {α : Type u_1} [inst : AddMonoid α] {a : Colex α}, IsAddLeftRegular (ofColex a) ↔ IsAddLeftRegular a
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.χ_comp_hom`. -/
CategoryTheory.Classifier.χ_comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C} {X Y : C}
  (m : X ⟶ Y) [inst_1 : CategoryTheory.Mono m], CategoryTheory.CategoryStruct.comp (𝒞₁.χ m) (𝒞₁.hom 𝒞₂) = 𝒞₂.χ m
-- Mathlib.Order.CompleteLattice.Chain
/-- An explicit maximal chain. `maxChain` is taken to be the union of all sets in `ChainClosure`.  -/
maxChain : {α : Type u_1} → (α → α → Prop) → Set α
-- Mathlib.Data.Set.Function
Set.surjOn_id : ∀ {α : Type u_1} (s : Set α), Set.SurjOn id s s
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.deg_mul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜] (c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x), (c1 * c2).deg = c1.deg + c2.deg
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The map `Cochain (K⟦a⟧) L n' → Cochain K L n` when `n + a = n'`.  -/
CochainComplex.HomComplex.Cochain.leftUnshift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n' a : ℤ} →
          CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n' →
            (n : ℤ) → n + a = n' → CochainComplex.HomComplex.Cochain K L n
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.graphFunctor_faithful : CategoryTheory.RelCat.graphFunctor.Faithful
-- Aesop.Index.Forward
Aesop.instInhabitedForwardIndex.default : Aesop.ForwardIndex
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.SavedLocalContext.mk.injEq : ∀ (savedLocalContext : Lean.LocalContext) (savedLocalInstances : Lean.LocalInstances)
  (savedState : Lean.Meta.SavedState) (savedLocalContext_1 : Lean.LocalContext)
  (savedLocalInstances_1 : Lean.LocalInstances) (savedState_1 : Lean.Meta.SavedState),
  ({ savedLocalContext := savedLocalContext, savedLocalInstances := savedLocalInstances, savedState := savedState } =
      { savedLocalContext := savedLocalContext_1, savedLocalInstances := savedLocalInstances_1,
        savedState := savedState_1 }) =
    (savedLocalContext = savedLocalContext_1 ∧ savedLocalInstances = savedLocalInstances_1 ∧ savedState = savedState_1)
-- Mathlib.Data.TypeVec
TypeVec.casesNil_append1 : ∀ {β : TypeVec.{u_2} 0 → Sort u_1} (f : β Fin2.elim0), TypeVec.casesNil f Fin2.elim0 = f
-- Mathlib.RingTheory.IsTensorProduct
TensorProduct.isPushout : ∀ {R : Type u_8} {S : Type u_9} {T : Type u_10} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], Algebra.IsPushout R S T (TensorProduct R S T)