mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.ReflectsColimitOfIsSplitPair.out : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₁, u₂} D}
  {G : CategoryTheory.Functor D C} [self : CategoryTheory.Monad.ReflectsColimitOfIsSplitPair G] {A B : D} (f g : A ⟶ B)
  [G.IsSplitPair f g], CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair f g) G
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` reflects finite colimits, then `F.rightOp : C ⥤ Dᵒᵖ` reflects finite
limits.  -/
CategoryTheory.Limits.reflectsFiniteLimits_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsFiniteColimits F],
  CategoryTheory.Limits.ReflectsFiniteLimits F.rightOp
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.jp.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl : Lean.Compiler.LCNF.FunDecl pu),
  sizeOf (Lean.Compiler.LCNF.CodeDecl.jp decl) = 1 + sizeOf decl
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.cons : {V : Type u} → [inst : Quiver V] → {a b c : V} → Quiver.Path a b → (b ⟶ c) → Quiver.Path a c
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
IsSymmSndFDerivWithinAt.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F) (s : Set E) (x : E),
  IsSymmSndFDerivWithinAt 𝕜 f s x =
    ∀ (v w : E), ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) w) v
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
/-- The vertex cover number of `G` is the minimal number of vertices in a vertex cover of `G`.  -/
SimpleGraph.vertexCoverNum : {V : Type u_1} → SimpleGraph V → ℕ∞
-- Mathlib.Data.NNRat.BigOperators
NNRat.toNNRat_sum_of_nonneg : ∀ {α : Type u_1} {s : Finset α} {f : α → ℚ}, (∀ a ∈ s, 0 ≤ f a) → (∑ a ∈ s, f a).toNNRat = ∑ a ∈ s, (f a).toNNRat
-- Mathlib.Order.OrderIsoNat
WellFoundedGT.iSup_eq_monotonicSequenceLimit : ∀ {α : Type u_1} [inst : CompleteLattice α] [WellFoundedGT α] (a : ℕ →o α), iSup ⇑a = monotonicSequenceLimit a
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainTermGoal.mk : String → Lean.Lsp.Range → Lean.Lsp.PlainTermGoal
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.ge_antitone : ∀ {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), Antitone t.ge
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.fst_op_opIso_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst.op (CategoryTheory.Limits.biprod.opIso P Q).hom =
    CategoryTheory.Limits.biprod.inl
-- Mathlib.Data.Option.Basic
/-- Given an element of `a : Option α`, a default element `b : β` and a function `α → β`, apply this
function to `a` if it comes from `α`, and return `b` otherwise.  -/
Option.casesOn' : {α : Type u_1} → {β : Type u_2} → Option α → β → (α → β) → β
-- Mathlib.RingTheory.Ideal.Nonunits
mem_nonunits_iff : ∀ {α : Type u_2} {a : α} [inst : Monoid α], a ∈ nonunits α ↔ ¬IsUnit a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlex_k_eq_revlex : ∀ (m₁ m₂ : Lean.Grind.CommRing.Mon), m₁.revlex_k m₂ = m₁.revlex m₂
-- Std.Data.TreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the key-value pair with the smallest key.
 -/
Std.TreeMap.minEntry : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → (t : Std.TreeMap α β cmp) → t.isEmpty = false → α × β
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
zmodMulEquivOfGenerator_apply_ofAdd_one : ∀ {G : Type u_2} [inst : Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n),
  (zmodMulEquivOfGenerator hg hn) (Multiplicative.ofAdd 1) = g
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instInhabited : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Inhabited (Std.ExtHashMap α β)
-- Init.Data.List.Nat.Sum
List.le_sum_div_length_of_min?_eq_some_nat : ∀ {x : ℕ} {xs : List ℕ}, xs.min? = some x → x ≤ xs.sum / xs.length
-- Mathlib.Algebra.Group.Defs
IsLeftCancelAdd.mk : ∀ {G : Type u} [inst : Add G], (∀ (a : G), IsAddLeftRegular a) → IsLeftCancelAdd G
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The isomorphism expressing the commutation between taking
the cylinder of a homological complex and applying an additive functor.  -/
HomologicalComplex.cylinder.mapHomologicalComplexObjIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (F : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              {D : Type u_3} →
                [inst_3 : CategoryTheory.Category.{v_2, u_3} D] →
                  [inst_4 : CategoryTheory.Preadditive D] →
                    (H : CategoryTheory.Functor C D) →
                      [inst_5 : H.Additive] →
                        [inst_6 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X i) (F.X i)] →
                          [inst_7 :
                              HomologicalComplex.HasHomotopyCofiber
                                (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F)
                                  (-CategoryTheory.CategoryStruct.id F))] →
                            [inst_8 :
                                ∀ (i : ι),
                                  CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i)
                                    (((H.mapHomologicalComplex c).obj F).X i)] →
                              [inst_9 :
                                  HomologicalComplex.HasHomotopyCofiber
                                    (CategoryTheory.Limits.biprod.lift
                                      (CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F))
                                      (-CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F)))] →
                                [HomologicalComplex.HasHomotopyCofiber
                                      ((H.mapHomologicalComplex c).map
                                        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F)
                                          (-CategoryTheory.CategoryStruct.id F)))] →
                                  (∀ (j : ι), ∃ i, c.Rel i j) →
                                    ((H.mapHomologicalComplex c).obj F.cylinder ≅
                                      ((H.mapHomologicalComplex c).obj F).cylinder)
-- Mathlib.FieldTheory.Normal.Basic
AlgHom.restrict_liftNormal : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} [inst_1 : Field K₁] [inst_2 : Algebra F K₁] (E : Type u_6)
  [inst_3 : Field E] [inst_4 : Algebra F E] [inst_5 : Algebra K₁ E] [inst_6 : IsScalarTower F K₁ E] (ϕ : K₁ →ₐ[F] K₁)
  [inst_7 : Normal F K₁] [inst_8 : Normal F E], (ϕ.liftNormal E).restrictNormal K₁ = ϕ
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
/-- The recursive definition of the sequence of Catalan numbers:
`catalan (n + 1) = ∑ i : Fin n.succ, catalan i * catalan (n - i)`  -/
catalan : ℕ → ℕ
-- Lean.Data.LOption
Lean.LOption : Type u → Type u
-- Init.Control.Lawful.Instances
OptionT.bind_throw : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} {e : PUnit.{u_3 + 1}} [inst : Monad m] [LawfulMonad m]
  (f : α → OptionT m β), throw e >>= f = throw e
-- Batteries.Tactic.NoMatch
/-- The syntax `match ⋯ with.` has been deprecated in favor of `nomatch ⋯`.

Both now support multiple discriminants.
 -/
Batteries.Tactic.«tacticMatch_,,With.» : Lean.ParserDescr
-- Mathlib.Logic.Equiv.Multiset
/-- Explicit decoding function for `Multiset α`  -/
decodeMultiset : {α : Type u_1} → [Encodable α] → ℕ → Option (Multiset α)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isCircuit_def : ∀ {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u), p.IsCircuit ↔ p.IsTrail ∧ p ≠ SimpleGraph.Walk.nil
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instNonAssocRing : {R : Type u_1} → [NonAssocRing R] → NonAssocRing Rᵃᵒᵖ
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.doublingGamma_add_one : ∀ (s : ℝ), s ≠ 0 → (s + 1).doublingGamma = s * s.doublingGamma
-- Mathlib.Data.Matrix.Basic
/-- `Matrix.transpose` as an `AddEquiv`  -/
Matrix.transposeAddEquiv : (m : Type u_2) → (n : Type u_3) → (α : Type u_11) → [inst : Add α] → Matrix m n α ≃+ Matrix n m α
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
/-- The function `expNegInvGlue` is positive on `(0, +∞)`.  -/
expNegInvGlue.pos_of_pos : ∀ {x : ℝ}, 0 < x → 0 < expNegInvGlue x
-- Init.Try
/-- Marker for try?-solved subproofs in `exact? +try?` suggestions.
When `exact?` uses try? as a discharger, it wraps the proof in this marker
so that the unexpander can replace it with `(by try?)` in the suggestion.
 -/
Lean.Try.Marker : {α : Sort u} → α → α
-- Mathlib.Geometry.Manifold.Complex
IsMaxFilter.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder β] (f : α → β) (l : Filter α) (a : α),
  IsMaxFilter f l a = ∀ᶠ (x : α) in l, f x ≤ f a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  l.contains k = false → (Std.TreeMap.Raw.unitOfList l cmp).getKey? k = none
-- Mathlib.RingTheory.Extension.Generators
/-- The designated section w.r.t. a family of generators.  -/
Algebra.Generators.σ : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Generators R S ι) → S → P.Ring
-- Mathlib.RingTheory.Norm.Defs
Algebra.norm_eq_one_of_not_module_finite : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S],
  ¬Module.Finite R S → ∀ (x : S), (Algebra.norm R) x = 1
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instHashableFanin.hash : Std.Sat.AIG.Fanin → UInt64
-- Std.Data.Internal.List.Associative
Std.Internal.List.forM_eq_forM_keys : ∀ {α : Type u} {β : α → Type v} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m'] {l : List ((a : α) × β a)}
  {f : α → m' PUnit.{w + 1}}, (l.forM fun a => f a.fst) = (Std.Internal.List.keys l).forM f
-- Mathlib.Data.Num.Lemmas
Num.linearOrder : LinearOrder Num
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.cancel_unit_right_assoc' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {W X X' Y Y' Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h (e.unit.app Z))) =
      CategoryTheory.CategoryStruct.comp f'
        (CategoryTheory.CategoryStruct.comp g' (CategoryTheory.CategoryStruct.comp h' (e.unit.app Z))) ↔
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) =
      CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h')
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Iic_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α) {c : α},
  c < 0 → (fun x => c * x) ⁻¹' Set.Iic a = Set.Ici (a / c)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakSpace.instAddCommGroup : {𝕜 : Type u_2} →
  {E : Type u_4} →
    [inst : CommRing 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : IsTopologicalAddGroup 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommGroup E] →
              [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → AddCommGroup (WeakSpace 𝕜 E)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.addCommMonoid.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.IsCommAddMonObj M],
  CategoryTheory.Hom.addCommMonoid = { toAddMonoid := CategoryTheory.Hom.addMonoid, add_comm := ⋯ }
-- Mathlib.RingTheory.NormalClosure
Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S],
  IsScalarTower S (Ring.NormalClosure R S)
    ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AntitoneOn.mul_const' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [MulRightMono α], AntitoneOn f s → ∀ (a : α), AntitoneOn (fun x => f x * a) s
-- Mathlib.Data.BitVec
BitVec.equivFin_symm_apply_toFin : ∀ {m : ℕ} (a : Fin (2 ^ m)), (BitVec.equivFin.symm a).toFin = a
-- Std.Time.Time.HourMarker
Std.Time.HourMarker.am.sizeOf_spec : sizeOf Std.Time.HourMarker.am = 1
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.finsum_smul_mem_convex : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {H : Type uH} [inst_4 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M] {s : Set M}
  (f : SmoothPartitionOfUnity ι I M s) {g : ι → M → F} {t : Set F} {x : M},
  x ∈ s → (∀ (i : ι), (f i) x ≠ 0 → g i x ∈ t) → Convex ℝ t → ∑ᶠ (i : ι), (f i) x • g i x ∈ t
-- Mathlib.Order.Heyting.Hom
/-- Copy of a `HeytingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
HeytingHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : HeytingAlgebra α] →
      [inst_1 : HeytingAlgebra β] → (f : HeytingHom α β) → (f' : α → β) → f' = ⇑f → HeytingHom α β
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F) (x : E),
  ‖A x‖ ^ 2 = RCLike.re (inner 𝕜 ((ContinuousLinearMap.adjoint A ∘SL A) x) x)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_eval₂ : ∀ {S : Type u} [inst : Semiring S] {T : Type v} [inst_1 : Semiring T] (f : S →+* T) (n : ℕ) (t : T),
  Polynomial.eval t (ascPochhammer T n) = Polynomial.eval₂ f t (ascPochhammer S n)
-- Mathlib.Util.Superscript
/-- Formatter for the superscript parser.  -/
Mathlib.Tactic.superscript.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.Subcomplex.Pairing.anodyneExtensions : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular], SSet.anodyneExtensions A.ι
-- Mathlib.Analysis.Normed.Order.Hom.Basic
AddGroupSeminormClass.toSeminormedAddGroup_norm_eq : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : AddGroup α] [inst_2 : AddGroupSeminormClass F α ℝ]
  (f : F) (x : α), ‖x‖ = f x
-- Mathlib.Data.Nat.ModEq
/-- The natural number less than `lcm n m` congruent to `a` mod `n` and `b` mod `m`  -/
Nat.chineseRemainder' : {m n a b : ℕ} → a ≡ b [MOD n.gcd m] → { k // k ≡ a [MOD n] ∧ k ≡ b [MOD m] }
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.star_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid β]
  [inst_3 : StarAddMonoid β] [inst_4 : ContinuousStar β] (f : ZeroAtInftyContinuousMap α β) (x : α),
  (star f) x = star (f x)
-- Mathlib.Order.WithBot
WithTop.strictMono_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : WithTop α → β},
  StrictMono f ↔ (StrictMono fun a => f ↑a) ∧ ∀ (x : α), f ↑x < f ⊤
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_left_cancel_iff_of_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b c : α} [inst_1 : PartialOrder α] [PosMulReflectLE α],
  0 < a → (a * b = a * c ↔ b = c)
-- Mathlib.Algebra.Torsor.Defs
Equiv.pointReflection_vsub_left : ∀ {G : Type u_3} {P : Type u_4} [inst : AddGroup G] [inst_1 : AddTorsor G P] (x y : P),
  (Equiv.pointReflection x) y -ᵥ x = x -ᵥ y
-- Std.Sync.CancellationToken
/-- Explicitly cancelled
 -/
Std.CancellationReason.cancel : Std.CancellationReason
-- Mathlib.Tactic.TermCongr
/-- Combine two congruence proofs using transitivity.
Does not check that `res1.rhs` is defeq to `res2.lhs`.
If both `res1` and `res2` are trivial then the result is trivial.  -/
Mathlib.Tactic.TermCongr.CongrResult.trans : Mathlib.Tactic.TermCongr.CongrResult → Mathlib.Tactic.TermCongr.CongrResult → Mathlib.Tactic.TermCongr.CongrResult
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
HomologicalComplex.homotopyEquivalences_extendMap_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {K L : HomologicalComplex C c} (f : K ⟶ L) (e : c.Embedding c') [e.IsRelIff],
  HomologicalComplex.homotopyEquivalences C c' (HomologicalComplex.extendMap f e) ↔
    HomologicalComplex.homotopyEquivalences C c f
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.efixedPoint_mem' : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s)
  (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s)
  (hx : edist x (f x) ≠ ⊤), ContractingWith.efixedPoint' f hsc hsf hf x hxs hx ∈ s
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.Quotient.subsingleton_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M},
  Subsingleton (M ⧸ p) ↔ p = ⊤
-- Mathlib.Topology.Order.Basic
/-- **Alias** of `tendsto_of_tendsto_of_tendsto_of_le_of_le'`.

---

**Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities
hold eventually for the filter.  -/
Filter.Tendsto.squeeze' : ∀ {α : Type u} {β : Type v} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {f g h : β → α}
  {b : Filter β} {a : α},
  Filter.Tendsto g b (nhds a) →
    Filter.Tendsto h b (nhds a) →
      (∀ᶠ (b : β) in b, g b ≤ f b) → (∀ᶠ (b : β) in b, f b ≤ h b) → Filter.Tendsto f b (nhds a)
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). "Attach" the information that every element of `t` satisfies property
P to these elements inside the set, producing a set in the subtype.

```
attach' (fun x ↦ x < 4) {1, 2} H = ({1, 2} : Ordnode {x // x<4})
```  -/
Ordnode.attach' : {α : Type u_1} → {P : α → Prop} → (t : Ordnode α) → Ordnode.All P t → Ordnode { a // P a }
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.Pushforward.id_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X)
  (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (TopCat.Presheaf.Pushforward.id ℱ).inv.app U = CategoryTheory.CategoryStruct.id (ℱ.obj U)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearMap.mdifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E →L[𝕜] E') {x : E}, MDiffAt ⇑f x
-- Mathlib.Order.RelSeries
/-- A relation `r` is said to be finite dimensional iff there is a relation series of `r` with the
maximum length.  -/
SetRel.FiniteDimensional : {α : Type u_1} → SetRel α α → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKey!_alter_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.isEmpty = false →
    ((Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.minKey! = k ↔
      (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true)
-- Mathlib.Analysis.Normed.Group.Basic
edist_eq_enorm_sub : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E), edist a b = ‖a - b‖ₑ
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.inverse_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  (X : CategoryTheory.ShrinkHoms.{u} C), (CategoryTheory.ShrinkHoms.inverse C).obj X = X.fromShrinkHoms
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_comp_inv_atBot_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] {l : Filter α}
  {f : G → α}, Filter.Tendsto (fun x => f x⁻¹) Filter.atBot l ↔ Filter.Tendsto f Filter.atTop l
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Equivalence.mapCommGrp_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] (e : C ≌ D)
  [inst_6 : e.functor.Braided] [inst_7 : e.inverse.Braided],
  e.mapCommGrp.unitIso =
    CategoryTheory.Functor.mapCommGrpIdIso.symm ≪≫
      CategoryTheory.Functor.mapCommGrpNatIso e.unitIso ≪≫ CategoryTheory.Functor.mapCommGrpCompIso
-- Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
Nat.moebius_eq : ∀ (n : ℕ), UniqueFactorizationMonoid.moebius n = ArithmeticFunction.moebius n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.min?_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : Min α]
  [inst_1 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.WF → t.keys.min? = t.minKey?
-- Mathlib.LinearAlgebra.Dual.Defs
Module.Dual.eval_comp_comp_evalEquiv_eq : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.IsReflexive R M] {M' : Type u_6} [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] {f : M →ₗ[R] M'},
  Module.Dual.eval R M' ∘ₗ f ∘ₗ ↑(Module.evalEquiv R M).symm = f.dualMap.dualMap