mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Group.Defs
/-- Eta-expanded form of `ContinuousWithinAt.sub` -/
ContinuousWithinAt.fun_sub : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Sub G]
  [ContinuousSub G] {f g : X → G} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun i => f i - g i) s x
-- Batteries.Util.Cache
/-- Build a `DiscrTreeCache`,
from a function that returns a collection of keys and values for each declaration.
 -/
Batteries.Tactic.DiscrTreeCache.mk : {α : Type} →
  [BEq α] →
    String →
      (Lean.Name → Lean.ConstantInfo → Lean.MetaM (Array (Array Lean.Meta.DiscrTree.Key × α))) →
        optParam (Option (Array α → Array α)) none →
          optParam (Lean.MetaM (Lean.Meta.DiscrTree α)) failure → IO (Batteries.Tactic.DiscrTreeCache α)
-- Std.Data.ExtHashMap.Basic
/-- Internal implementation detail of the hash map  -/
Std.ExtHashMap.inner : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.ExtHashMap α β → Std.ExtDHashMap α fun x => β
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.pos_of_pos : ∀ {x : ℝ}, 0 < x → 0 < x.smoothTransition
-- Mathlib.SetTheory.ZFC.PSet
PSet.Nonempty.eq_1 : ∀ (u : PSet.{u_1}), u.Nonempty = u.toSet.Nonempty
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f],
  ((AlgebraicGeometry.Scheme.Hom.normalizationGlueData f).functor.comp
      AlgebraicGeometry.Scheme.forget).IsLocallyDirected
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.minValueSealed_def : Int8.minValueSealed✝ = Int8.minValue
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_neg : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (x : M →₀ R),
  AddMonoidAlgebra.ofCoeff (-x) = -AddMonoidAlgebra.ofCoeff x
-- Mathlib.Algebra.Group.Ext
CancelMonoid.ext : ∀ {M : Type u_1} ⦃m₁ m₂ : CancelMonoid M⦄, HMul.hMul = HMul.hMul → m₁ = m₂
-- Lean.Structure
Lean.instReprStructureFieldInfo.repr : Lean.StructureFieldInfo → ℕ → Std.Format
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.process : Lean.Meta.Match.Problem → StateRefT' IO.RealWorld Lean.Meta.Match.State Lean.MetaM Unit
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.instIsScalarTower : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {G : Type u_5} {G' : Type u_6} [inst_3 : Group G] [inst_4 : Group G'] [inst_5 : DistribMulAction G M]
  [inst_6 : DistribMulAction G' M] [inst_7 : SMulCommClass G R M] [inst_8 : SMulCommClass G' R M] [inst_9 : SMul G G']
  [IsScalarTower G G' M], IsScalarTower G G' (Module.Basis ι R M)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.insertMany_nil : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.insertMany [] = t
-- Lean.Elab.Term.TermElabM
/-- Pushes a new leaf node to the info tree associating the expression `e` to the syntax `stx`.
As a result, when the user hovers over `stx` they will see the type of `e`, and if `e`
is a constant they will see the constant's doc string.

* `expectedType?`: the expected type of `e` at the point of elaboration, if available
* `lctx?`: the local context in which to interpret `e` (otherwise it will use `← getLCtx`)
* `elaborator`: a declaration name used as an alternative target for go-to-definition
* `isBinder`: if true, this will be treated as defining `e` (which should be a local constant)
  for the purpose of go-to-definition on local variables
* `force`: In patterns, the effect of `addTermInfo` is usually suppressed and replaced
  by a `patternWithRef?` annotation which will be turned into a term info on the
  post-match-elaboration expression. This flag overrides that behavior and adds the term
  info immediately. (See https://github.com/leanprover/lean4/pull/1664.)
 -/
Lean.Elab.Term.addTermInfo : Lean.Syntax →
  Lean.Expr →
    optParam (Option Lean.Expr) none →
      optParam (Option Lean.LocalContext) none →
        optParam Lean.Name Lean.Name.anonymous →
          optParam Bool false → optParam Bool false → optParam Bool false → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.fst_one : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : Zero ι] [inst_1 : GradedMonoid.GOne A], Sigma.fst 1 = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Inhabited α]
  [inst_1 : Std.TransCmp cmp] {k : α}, (t₁ ∩ t₂).getKey! k = if k ∈ t₂ then t₁.getKey! k else default
-- Init.Meta.Defs
Lean.Quote.mk : {α : Type} → {k : optParam Lean.SyntaxNodeKind `term} → (α → Lean.TSyntax k) → Lean.Quote α k
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.injective_of_adjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} [L.PreservesMonomorphisms] (adj : L ⊣ R) (J : D)
  [CategoryTheory.Injective J], CategoryTheory.Injective (R.obj J)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.opFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : (CategoryTheory.ShortComplex C)ᵒᵖ), (CategoryTheory.ShortComplex.opFunctor C).obj S = (Opposite.unop S).op
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.IsInner.mk : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} [inst : P.IsProper],
  (∀ (x : ↑P.II) {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ 0) →
    (∀ (x : ↑P.II) {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ Fin.last (d + 1)) → P.IsInner
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_addNat_Iio_addNat : ∀ {n : ℕ} (m : ℕ) (i : Fin n), (fun x => x.addNat m) ⁻¹' Set.Iio (i.addNat m) = Set.Iio i
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.forget.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  CategoryTheory.Limits.Cocone.forget F =
    { obj := fun t => t.pt, map := fun {Y X} f => f.hom, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- Integrability in the change of variable formula for differentiable functions (one-variable
version): if a function `f` is injective and differentiable on a measurable set `s ⊆ ℝ`, then the
Lebesgue integral of a function `g : ℝ → ℝ≥0∞` on `f '' s` coincides with the Lebesgue integral
of `|(f' x)| * g ∘ f` on `s`.  -/
MeasureTheory.lintegral_image_eq_lintegral_abs_deriv_mul : ∀ {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      Set.InjOn f s → ∀ (g : ℝ → ENNReal), ∫⁻ (x : ℝ) in f '' s, g x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal |f' x| * g (f x)
-- Mathlib.Data.PNat.Defs
PNat.one_le : ∀ (n : ℕ+), 1 ≤ n
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Multiset.ProveZeroOrConsResult.zero.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(Multiset «$α»)} (pf pf_1 : Q(«$s» = 0)),
  (Mathlib.Meta.Multiset.ProveZeroOrConsResult.zero pf = Mathlib.Meta.Multiset.ProveZeroOrConsResult.zero pf_1) =
    (pf = pf_1)
-- Mathlib.Algebra.MvPolynomial.Counit
MvPolynomial.counitNat_C : ∀ (A : Type u_1) [inst : CommSemiring A] (n : ℕ), (MvPolynomial.counitNat A) (MvPolynomial.C n) = ↑n
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is inner regular for finite measure sets with respect to compact sets,
any measurable set of finite mass can be approximated from inside by compact sets.  -/
MeasurableSet.measure_eq_iSup_isCompact_of_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegularCompactLTTop] ⦃A : Set α⦄,
  MeasurableSet A → μ A ≠ ⊤ → μ A = ⨆ K, ⨆ (_ : K ⊆ A), ⨆ (_ : IsCompact K), μ K
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_zero' : ∀ {n : ℕ} {β : Sort u_2} (x : β) (p : Fin n → β), Fin.insertNth 0 x p = Fin.cons x p
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.isPell_iff_mem_unitary : ∀ {d : ℤ} {b : ℤ√d}, Pell.IsPell b ↔ b ∈ unitary (ℤ√d)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.coe_inf_of_nonempty : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β},
  s.Nonempty → ∀ (f : β → α), ↑(s.inf f) = s.inf (WithTop.some ∘ f)
-- Init.Grind.AC
/-- Given `lhs₁ = rhs₁` and `lhs₂ = rhs₂` where `lhs₁ := p * c` and `lhs₂ := c * s`,
`lhs = rhs` where `lhs := rhs₁ * s` and `rhs := p * rhs₂`
 -/
Lean.Grind.AC.superpose : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op}
  (p c s lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.superpose_cert p c s lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs = Lean.Grind.AC.Seq.denote ctx rhs
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prodIsoProd_hom_fst_assoc : ∀ (X Y : TopCat) {Z : TopCat} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom (CategoryTheory.CategoryStruct.comp TopCat.prodFst h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
-- Lean.Parser.Do
Lean.Parser.Term.doIfProp : Lean.Parser.Parser
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.unitOfList_equiv_foldl : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α},
  (Std.HashMap.Raw.unitOfList l).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) ∅ l)
-- Lean.Parser.Basic
Lean.Parser.instInhabitedLeadingIdentBehavior : Inhabited Lean.Parser.LeadingIdentBehavior
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.distinct_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) t.keys
-- Mathlib.CategoryTheory.Galois.EssSurj
Action.FintypeCat.quotientToQuotientOfLE.congr_simp : ∀ {G : Type u_1} [inst : Group G] (H N : Subgroup G) [inst_1 : Fintype (G ⧸ N)] [inst_2 : Fintype (G ⧸ H)] (h : N ≤ H),
  Action.FintypeCat.quotientToQuotientOfLE H N h = Action.FintypeCat.quotientToQuotientOfLE H N h
-- Mathlib.FieldTheory.SeparableClosure
/-- An element is contained in the separable closure of `F` in `E` if and only if
it is a separable element.  -/
mem_separableClosure_iff : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ separableClosure F E ↔ IsSeparable F x
-- Mathlib.Algebra.Polynomial.Bivariate
/-- The notation `R[X][Y]` for `R[X][X]` in the `Polynomial` scope.  -/
Polynomial.Bivariate.«term_[X][Y]» : Lean.TrailingParserDescr
-- Mathlib.Data.Finsupp.Weight
/-- Without zero divisors, nonzero weight is a `NonTorsionWeight`  -/
Finsupp.nonTorsionWeight_of : ∀ {σ : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Semiring R] (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [IsDomain R] [Module.IsTorsionFree R M], (∀ (i : σ), w i ≠ 0) → Finsupp.NonTorsionWeight R w
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.instInhabitedSymbolPriorityEntry : Inhabited Lean.Meta.Grind.SymbolPriorityEntry
-- Lean.Level
Lean.Level.ctorToNat : Lean.Level → ℕ
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.span_image_extend_eq_span_image : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : ι → V} {s t : Set ι} (hs : LinearIndepOn K v s) (hst : s ⊆ t),
  Submodule.span K (v '' hs.extend hst) = Submodule.span K (v '' t)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformation.mk.inj : ∀ {label : Lean.Lsp.ParameterInformationLabel} {documentation? : Option Lean.Lsp.MarkupContent}
  {label_1 : Lean.Lsp.ParameterInformationLabel} {documentation?_1 : Option Lean.Lsp.MarkupContent},
  { label := label, documentation? := documentation? } = { label := label_1, documentation? := documentation?_1 } →
    label = label_1 ∧ documentation? = documentation?_1
-- Mathlib.Data.Countable.Basic
countable_left_of_prod_of_nonempty : ∀ {α : Type u} {β : Type v} [Nonempty β], Countable (α × β) → Countable α
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_lt_mul_iff_right₀ : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [PosMulStrictMono α]
  [PosMulReflectLT α], 0 < a → (a * b < a * c ↔ b < c)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
_private.Mathlib.CategoryTheory.Monoidal.Free.Basic.0.CategoryTheory.FreeMonoidalCategory.«term_⟶ᵐ_» : Lean.TrailingParserDescr
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalFirst : Lean.Elab.Tactic.Tactic
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂)
  (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁),
  (CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ a b comm).hom₂ = b
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.mk'_apply : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  [inst_6 : LieModule R L M] (a : M), (LieSubmodule.Quotient.mk' N) a = LieSubmodule.Quotient.mk a
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_finsetProd_comm : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {s : Finset β}
  (f : α →₀ M) (h : α → M → β → N), (f.prod fun a m => ∏ b ∈ s, h a m b) = ∏ b ∈ s, f.prod fun a m => h a m b
-- Mathlib.RingTheory.AlgebraicIndependent.Adjoin
AlgebraicIndependent.lift_reprField : ∀ {ι : Type u_1} {F : Type u_2} {E : Type u_3} {x : ι → E} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  (hx : AlgebraicIndependent F x) (p : ↥(IntermediateField.adjoin F (Set.range x))),
  (IsFractionRing.lift ⋯) (hx.reprField p) = ↑p
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.mk : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {M : Type u_3} →
            [inst_2 : TopologicalSpace M] →
              [inst_3 : AddCommMonoid M] →
                {M₂ : Type u_4} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R M] →
                        [inst_7 : Module S M₂] →
                          (toLinearMap : M →ₛₗ[σ] M₂) →
                            autoParam (Continuous toLinearMap.toFun) ContinuousLinearMap.cont._autoParam → M →SL[σ] M₂
-- Mathlib.Algebra.Algebra.Tower
Submodule.smul_mem_span_smul_of_mem : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [IsScalarTower R S A] {s : Set S} {t : Set A}
  {k : S}, k ∈ Submodule.span R s → ∀ {x : A}, x ∈ t → k • x ∈ Submodule.span R (s • t)
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first non-`none` result of applying the monadic function `f` to each output
of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.

`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
examined in order of iteration.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.findSomeM?` always terminates after finitely many steps.

Example:
```lean example
#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none
```
```output
Almost! 6
Almost! 5
```
```output
some 10
```
 -/
Std.IterM.findSomeM? : {α β γ : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → Std.IterM m β → (β → m (Option γ)) → m (Option γ)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.corepresentableByUliftFunctorEquiv_apply_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C}
  (R : (F.comp CategoryTheory.uliftFunctor.{w, v}).CorepresentableBy X) {Y : C},
  (CategoryTheory.Functor.corepresentableByUliftFunctorEquiv R).homEquiv = R.homEquiv.trans Equiv.ulift
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
UpperHalfPlane.gl_smul_eq_iff_num_eq : ∀ {g : GL (Fin 2) ℝ} {z w : UpperHalfPlane},
  g • z = w ↔ UpperHalfPlane.num g ↑z = (UpperHalfPlane.σ g) ↑w * UpperHalfPlane.denom g ↑z
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.isEquivalence_iff : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂]
  (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'}
  [inst_7 : CategoryTheory.Category.{v₄', u₄'} D₁'] [inst_8 : CategoryTheory.Category.{v₅', u₅'} D₂']
  (L₁' : CategoryTheory.Functor C₁ D₁') (L₂' : CategoryTheory.Functor C₂ D₂') [L₁'.IsLocalization W₁]
  [L₂'.IsLocalization W₂] (G' : CategoryTheory.Functor D₁' D₂') [CategoryTheory.CatCommSq Φ.functor L₁' L₂' G'],
  G.IsEquivalence ↔ G'.IsEquivalence
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
extChartAt_inl_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_16} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {x y : M}, ↑(extChartAt I (Sum.inl x)) (Sum.inl y) = ↑(extChartAt I x) y
-- Mathlib.Algebra.Ring.Prod
/-- A ring `R` is isomorphic to `R × S` when `S` is the zero ring  -/
RingEquiv.prodZeroRing : (R : Type u_1) →
  (S : Type u_3) → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → [Subsingleton S] → R ≃+* R × S
-- Mathlib.Geometry.Manifold.Instances.Real
IccLeftChart_apply : ∀ {x y : ℝ} [hxy : Fact (x < y)] (z : ↑(Set.Icc x y)), ↑(IccLeftChart x y) z = ⟨WithLp.toLp 2 fun x_1 => ↑z - x, ⋯⟩
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.acyclic_truncLE_iff_isSupportedOutside : ∀ {ι : 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.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C], (K.truncLE e).Acyclic ↔ K.IsSupportedOutside e
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.head_succ' : ∀ {F : PFunctor.{uA, uB}} (n m : ℕ) (x : (n : ℕ) → PFunctor.Approx.CofixA F n),
  PFunctor.Approx.AllAgree x → PFunctor.Approx.head' (x n.succ) = PFunctor.Approx.head' (x m.succ)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Create an equal copy of a subgraph (see `copy_eq`) with possibly different definitional equalities.
See Note [range copy pattern].
 -/
SimpleGraph.Subgraph.copy : {V : Type u} →
  {G : SimpleGraph V} →
    (G' : G.Subgraph) → (V'' : Set V) → V'' = G'.verts → (adj' : V → V → Prop) → adj' = G'.Adj → G.Subgraph
-- Mathlib.Geometry.Manifold.Immersion
/-- The local property of being an immersion at a point: `f : M → N` is an immersion at `x` if
there exist charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively, such that in these
charts, `f` looks like the inclusion `u ↦ (u, 0)`.

This definition has a fixed parameter `F`, which is a choice of complement of `E` in the model
normed space `E'` of `N`: being an immersion at `x` includes a choice of linear isomorphism
between `E × F` and `E'`.  -/
Manifold.ImmersionAtProp : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        (F : Type u_5) →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup E''] →
                [inst_4 : NormedSpace 𝕜 E''] →
                  [inst_5 : NormedAddCommGroup F] →
                    [NormedSpace 𝕜 F] →
                      {H : Type u_7} →
                        [inst_7 : TopologicalSpace H] →
                          {G : Type u_9} →
                            [inst_8 : TopologicalSpace G] →
                              ModelWithCorners 𝕜 E H →
                                ModelWithCorners 𝕜 E'' G →
                                  (M : Type u_11) →
                                    [inst : TopologicalSpace M] →
                                      (N : Type u_13) →
                                        [inst_9 : TopologicalSpace N] →
                                          (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.cyclesOpIso_hom_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (CategoryTheory.ShortComplex.opMap φ))
      S₁.cyclesOpIso.hom =
    CategoryTheory.CategoryStruct.comp S₂.cyclesOpIso.hom (CategoryTheory.ShortComplex.opcyclesMap φ).op
-- Mathlib.Geometry.Diffeology.Basic
/-- The plots belonging to a diffeology, as a subset of
`(n : ℕ) × (EuclideanSpace ℝ (Fin n) → X)`.  -/
DiffeologicalSpace.toPlots : {X : Type u_1} → DiffeologicalSpace X → Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.mk.injEq : ∀ {α : Type u_7} (MeasurableSet' : Set α → Prop) (measurableSet_empty : MeasurableSet' ∅)
  (measurableSet_compl : ∀ (s : Set α), MeasurableSet' s → MeasurableSet' sᶜ)
  (measurableSet_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet' (f i)) → MeasurableSet' (⋃ i, f i))
  (MeasurableSet'_1 : Set α → Prop) (measurableSet_empty_1 : MeasurableSet'_1 ∅)
  (measurableSet_compl_1 : ∀ (s : Set α), MeasurableSet'_1 s → MeasurableSet'_1 sᶜ)
  (measurableSet_iUnion_1 : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet'_1 (f i)) → MeasurableSet'_1 (⋃ i, f i)),
  ({ MeasurableSet' := MeasurableSet', measurableSet_empty := measurableSet_empty,
        measurableSet_compl := measurableSet_compl, measurableSet_iUnion := measurableSet_iUnion } =
      { MeasurableSet' := MeasurableSet'_1, measurableSet_empty := measurableSet_empty_1,
        measurableSet_compl := measurableSet_compl_1, measurableSet_iUnion := measurableSet_iUnion_1 }) =
    (MeasurableSet' = MeasurableSet'_1)