mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : (↑U).Opens)
  (W : (↑((TopologicalSpace.Opens.map f.base).obj U)).Opens) (e : W ≤ (TopologicalSpace.Opens.map (f ∣_ U).base).obj V),
  AlgebraicGeometry.Scheme.Hom.appLE (f ∣_ U) V W e =
    AlgebraicGeometry.Scheme.Hom.appLE f ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V)
      ((AlgebraicGeometry.Scheme.Hom.opensFunctor ((TopologicalSpace.Opens.map f.base).obj U).ι).obj W) ⋯
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.toInt : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- Two orthonormal bases with the same orientation determine the same "determinant" top-dimensional
form on `E`, and conversely.  -/
OrthonormalBasis.same_orientation_iff_det_eq_det : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] {e f : OrthonormalBasis ι ℝ E},
  e.toBasis.det = f.toBasis.det ↔ e.toBasis.orientation = f.toBasis.orientation
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valued.coe_valuation_eq_rankOne_hom_comp_valuation : ∀ (L : Type u_1) [inst : Field L] (Γ₀ : Type u_2) [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne], ⇑NormedField.valuation = ⇑(Valuation.RankOne.hom Valued.v) ∘ ⇑Valued.v.restrict
-- Mathlib.Data.Num.Lemmas
Num.cast_mul : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (m n : Num), ↑(m * n) = ↑m * ↑n
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.instAddHom : {R : Type u} → [inst : Semiring R] → {M N : SemimoduleCat R} → Add (M ⟶ N)
-- Mathlib.Data.Seq.Basic
Stream'.const.eq_1 : ∀ {α : Type u} (a : α) (x : ℕ), Stream'.const a x = a
-- Std.Sat.AIG.RefVec
_private.Std.Sat.AIG.RefVec.0.Std.Sat.AIG.RefVec.countKnown.go.match_1.eq_1 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (h_1 : Unit → motive Std.Sat.AIG.Decl.false)
  (h_2 : (x : Std.Sat.AIG.Decl α) → motive x),
  (match Std.Sat.AIG.Decl.false with
    | Std.Sat.AIG.Decl.false => h_1 ()
    | x => h_2 x) =
    h_1 ()
-- Init.Data.Float.Model.Unpacked.Operations.Div
/-- Computes the quotient of two floating point numbers and rounds the result according to
the given specification.
 -/
Float.Model.UnpackedFloat.div : Float.Model.Format → Float.Model.UnpackedFloat → Float.Model.UnpackedFloat → Float.Model.UnpackedFloat
-- Mathlib.Algebra.Order.Group.Synonym
toColex_one : ∀ {α : Type u_1} [inst : One α], toColex 1 = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyLT?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ {k : α}, Std.DTreeMap.Internal.Impl.getKeyLT? k t₁ = Std.DTreeMap.Internal.Impl.getKeyLT? k t₂
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.coe_iSup_of_directed : ∀ {R : Type u} [inst : NonAssocSemiring R] {ι : Sort u_1} [hι : Nonempty ι] {S : ι → Subsemiring R},
  Directed (fun x1 x2 => x1 ≤ x2) S → ↑(⨆ i, S i) = ⋃ i, ↑(S i)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdRingM : Lean.Meta.Grind.Arith.CommRing.MonadSetTermId Lean.Meta.Grind.Arith.CommRing.RingM
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_reindex_inv_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)] (b : β) {Z : C}
  (h : ∐ f ∘ ⇑ε ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f (ε b))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.reindex ε f).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (f ∘ ⇑ε) b) h
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- `toGL` is the map from the special linear group to the general linear group.  -/
Matrix.SpecialLinearGroup.toGL : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → Matrix.SpecialLinearGroup n R →* GL n R
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C} (h₁ h₂ : CategoryTheory.AddGrpObj X), h₁.toAddMonObj = h₂.toAddMonObj → h₁ = h₂
-- Init.Data.Nat.Gcd
Nat.gcd_sub_mul_right_left : ∀ {m n k : ℕ}, k * m ≤ n → (n - k * m).gcd m = n.gcd m
-- Mathlib.Data.Set.Basic
Set.decidableSdiff : {α : Type u} → (s t : Set α) → (a : α) → [Decidable (a ∈ s)] → [Decidable (a ∈ t)] → Decidable (a ∈ s \ t)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.insertMany_nil : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α],
  ↑(m.insertMany []) = m
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.ι_mapBifunctorMap : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] {K₁ L₁ : HomologicalComplex C₁ c₁} {K₂ L₂ : HomologicalComplex C₂ c₂}
  (f₁ : K₁ ⟶ L₁) (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J)
  [inst_8 : TotalComplexShape c₁ c₂ c] [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : L₁.HasMapBifunctor L₂ F c]
  [inst_11 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) = j),
  CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
      ((HomologicalComplex.mapBifunctorMap f₁ f₂ F c).f j) =
    CategoryTheory.CategoryStruct.comp ((F.map (f₁.f i₁)).app (K₂.X i₂))
      (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) (L₁.ιMapBifunctor L₂ F c i₁ i₂ j h))
-- Mathlib.Order.Irreducible
SupPrime.supIrred : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, SupPrime a → SupIrred a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.linePolynomial.eq_1 : ∀ {R : Type r} [inst : CommRing R] (x y ℓ : R),
  WeierstrassCurve.Affine.linePolynomial x y ℓ = Polynomial.C ℓ * (Polynomial.X - Polynomial.C x) + Polynomial.C y
-- Mathlib.Data.Vector3
/-- The vector cons operation  -/
Vector3.cons : {α : Type u_1} → {n : ℕ} → α → Vector3 α n → Vector3 α (n + 1)
-- Mathlib.Topology.Algebra.Monoid
instSeparatelyContinuousAddOrderDual : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M], SeparatelyContinuousAdd Mᵒᵈ
-- Mathlib.Algebra.Ring.Subsemiring.Order
Subsemiring.mem_nonneg : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {x : R},
  x ∈ Subsemiring.nonneg R ↔ 0 ≤ x
-- Mathlib.Logic.Function.Basic
Function.instAsymmOnFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [Std.Asymm r], Std.Asymm (Function.onFun r f)
-- Mathlib.Data.List.NodupEquivFin
/-- A `l : List α` is `Sublist l l'` for `l' : List α` iff
there is `f`, an order-preserving embedding of `ℕ` into `ℕ` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`.
 -/
List.sublist_iff_exists_orderEmbedding_getElem?_eq : ∀ {α : Type u_1} {l l' : List α}, l.Sublist l' ↔ ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sup_comm : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (a b : CauSeq α abs),
  a ⊔ b = b ⊔ a
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_loops : ∀ {α : Type u_1} {M : Matroid α}, M.eRk M.loops = 0
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiable.smul : ∀ {𝕜 : 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] {V : Type u_18} [inst_6 : NormedAddCommGroup V]
  [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V}, MDiff f → MDiff g → MDiff (f • g)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.all_keys : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulHashable α]
  [EquivBEq α] {p : α → Bool}, m.keys.all p = m.all fun a x => p a
-- Lean.Parser.Types
Lean.Parser.ParserState.toErrorMsg : Lean.Parser.InputContext → Lean.Parser.ParserState → String
-- Init.Data.Rat.Lemmas
Rat.maybeNormalize_eq_normalize : ∀ {num : ℤ} {den g : ℕ} (dvd_num : ↑g ∣ num) (dvd_den : g ∣ den) (den_nz : den / g ≠ 0)
  (reduced : (num / ↑g).natAbs.Coprime (den / g)),
  ↑g ∣ num → g ∣ den → Rat.maybeNormalize num den g dvd_num dvd_den den_nz reduced = Rat.normalize num den ⋯
-- Lean.Log
Lean.MonadLog.mk : {m : Type → Type} →
  [toMonadFileMap : Lean.MonadFileMap m] → m Lean.Syntax → m String → m Bool → (Lean.Message → m Unit) → Lean.MonadLog m
-- Mathlib.Algebra.Tropical.Basic
Tropical.tropEquiv_symm_coe_fn : ∀ {R : Type u}, ⇑Tropical.tropEquiv.symm = Tropical.untrop
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.instCharZero : ∀ (k : Type u) [inst : Field k] [CharZero k], CharZero (AlgebraicClosure k)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc),
  (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).Q = cc.pt
-- Mathlib.Data.List.Sigma
List.kreplace_nodupKeys : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)},
  (List.kreplace a b l).NodupKeys ↔ l.NodupKeys
-- Init.Data.Dyadic.Basic
HEq.congr_simp : ∀ {α : Sort u} (a a_1 : α), a = a_1 → ∀ {β : Sort u} (a_2 a_3 : β), a_2 = a_3 → (a ≍ a_2) = (a_1 ≍ a_3)
-- Mathlib.Analysis.Matrix.Normed
/-- Normed algebra instance (using the Frobenius norm) for matrices over `ℝ` or `ℂ`.  Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.frobeniusNormedAlgebra : {R : Type u_1} →
  {m : Type u_3} →
    {α : Type u_5} →
      [inst : Fintype m] →
        [inst_1 : RCLike α] →
          [inst_2 : DecidableEq m] → [inst_3 : NormedField R] → [NormedAlgebra R α] → NormedAlgebra R (Matrix m m α)
-- Mathlib.Topology.Order.AtTopBotIxx
/-- The `atTop` filter for an open interval `Ioo a b` comes from the left-neighbourhoods filter at
the right endpoint in the ambient order.  -/
comap_coe_Ioo_nhdsLT : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] (a b : X),
  autoParam (Order.IsSuccPrelimit b) comap_coe_Ioo_nhdsLT._auto_1 →
    Filter.comap Subtype.val (nhdsWithin b (Set.Iio b)) = Filter.atTop
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.elabNoErrorIfUnused : Lean.Elab.Term.TermElab
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousDiv.mk : ∀ {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : Div G], (Continuous fun p => p.1 / p.2) → ContinuousDiv G
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.congr_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D),
  (CategoryTheory.MonoOver.congr X e).counitIso =
    CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.MonoOver.isoMk (e.counitIso.app Y.obj.left) ⋯) ⋯
-- Mathlib.RingTheory.Extension.Presentation.Basic
_private.Mathlib.RingTheory.Extension.Presentation.Basic.0.Algebra.Presentation.aux.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (_Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ),
  Algebra.Presentation.aux✝ _Q P = MvPolynomial.aeval (Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ P.val))
-- Init.Data.Iterators.Combinators.FilterMap
/-- *Note: This is a very general combinator that requires an advanced understanding of monads,
dependent types and termination proofs. The variants `filterMap` and `filterMapM` are easier to use
and sufficient for most use cases.*

If `it` is an iterator, then `it.filterMapWithPostcondition f` is another iterator that applies a monadic
function `f` to all values emitted by `it`. `f` is expected to return an `Option` inside the monad.
If `f` returns `none`, then nothing is emitted; if it returns `some x`, then `x` is emitted.

`f` is expected to return `PostconditionT n (Option _)`, where `n` is an arbitrary monad.
The `PostconditionT` transformer allows the caller to intrinsically prove properties about
`f`'s return value in the monad `n`, enabling termination proofs depending on the specific behavior
of `f`.

**Marble diagram (without monadic effects):**

```text
it                                ---a --b--c --d-e--⊥
it.filterMapWithPostcondition     ---a'-----c'-------⊥
```

(given that `f a = pure (some a')`, `f c = pure (some c')` and `f b = f d = d e = pure none`)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then
this combinator will preserve productiveness. If `f` is an `ExceptT` monad and will always fail,
then `it.filterMapWithPostcondition` will be finite even if `it` isn't. In the first case, consider
using the `map`/`mapM`/`mapWithPostcondition` combinators instead, which provide more instances out of
the box.

In such situations, the missing instances can be proved manually if the postcondition bundled in
the `PostconditionT n` monad is strong enough. If `f` always returns `some _`, a suitable
postcondition is `fun x => x.isSome`; if `f` always fails, a suitable postcondition might be
`fun _ => False`.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
returned `Option` value.
 -/
Std.Iter.filterMapWithPostcondition : {α β γ : Type w} →
  [Std.Iterator α Id β] →
    {m : Type w → Type w'} →
      [inst : Monad m] → (f : β → Std.Iterators.PostconditionT m (Option γ)) → Std.Iter β → Std.IterM m γ
-- Mathlib.LinearAlgebra.FreeProduct.Basic
_private.Mathlib.LinearAlgebra.FreeProduct.Basic.0.LinearAlgebra.FreeProduct.«term_∘ₐ_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousLinearMap.analyticAt_uncurry_of_multilinear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F) {x : G × ((i : ι) → Em i)},
  AnalyticAt 𝕜 (fun p => (f p.1) p.2) x
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_add_Iic : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a + x) '' Set.Iic b = Set.Iic (a + b)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedClosed₁OfIsTriangulated : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated], P.IsTriangulatedClosed₁
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ1728.eq_1 : ∀ (R : Type u_1) [inst : CommRing R], WeierstrassCurve.ofJ1728 R = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.map_apply_inl : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ M') (g : N →+ N') (x : M),
  (AddMonoid.Coprod.map f g) (AddMonoid.Coprod.inl x) = AddMonoid.Coprod.inl (f x)
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.eq.inj : ∀ {lhs rhs : ℕ} {proof : Lean.Expr} {lhs_1 rhs_1 : ℕ} {proof_1 : Lean.Expr},
  Mathlib.Tactic.Order.AtomicFact.eq lhs rhs proof = Mathlib.Tactic.Order.AtomicFact.eq lhs_1 rhs_1 proof_1 →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc : ∀ {R : CommRingCat} (x : PrimeSpectrum ↑R) {Z : CommRingCat} (h : (AlgebraicGeometry.Spec R).presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal)))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.stalkIso R x).inv h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
      (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ x trivial) h)
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.mk.congr_simp : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (inl inl_1 : N →* E) (e_inl : inl = inl_1) (rightHom rightHom_1 : E →* G) (e_rightHom : rightHom = rightHom_1)
  (inl_injective : Function.Injective ⇑inl) (range_inl_eq_ker_rightHom : inl.range = rightHom.ker)
  (rightHom_surjective : Function.Surjective ⇑rightHom),
  { inl := inl, rightHom := rightHom, inl_injective := inl_injective,
      range_inl_eq_ker_rightHom := range_inl_eq_ker_rightHom, rightHom_surjective := rightHom_surjective } =
    { inl := inl_1, rightHom := rightHom_1, inl_injective := ⋯, range_inl_eq_ker_rightHom := ⋯,
      rightHom_surjective := ⋯ }
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_mul_eq_nnnorm_right : ∀ {E : Type u_5} [inst : SeminormedGroup E] {x : E} (y : E), ‖x‖₊ = 0 → ‖x * y‖₊ = ‖y‖₊
-- Mathlib.RingTheory.Noetherian.Defs
/-- A module is Noetherian iff every nonempty set of submodules has a maximal submodule among them.
 -/
set_has_maximal_iff_noetherian : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M
-- Init.Data.SInt.Lemmas
Int32.toBitVec_toInt16 : ∀ (x : Int32), x.toInt16.toBitVec = BitVec.signExtend 16 x.toBitVec
-- Mathlib.Topology.Algebra.MulAction
MulOpposite.continuousSMul : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : SMul M X]
  [ContinuousSMul M X], ContinuousSMul M Xᵐᵒᵖ
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimTargetInfo.mk.injEq : ∀ (view : Lean.Elab.Tactic.ElimTargetView) (expr : Lean.Expr) (arg? : Option Lean.Meta.GeneralizeArg)
  (view_1 : Lean.Elab.Tactic.ElimTargetView) (expr_1 : Lean.Expr) (arg?_1 : Option Lean.Meta.GeneralizeArg),
  ({ view := view, expr := expr, arg? := arg? } = { view := view_1, expr := expr_1, arg? := arg?_1 }) =
    (view = view_1 ∧ expr = expr_1 ∧ arg? = arg?_1)
-- Init.PropLemmas
cast_cast : ∀ {α β γ : Sort u_1} (ha : α = β) (hb : β = γ) (a : α), cast hb (cast ha a) = cast ⋯ a
-- Mathlib.RingTheory.Extension.Cotangent.Free
/-- If `H¹(L_{S/R}) = 0` and `R[xᵢ] → S` are generators indexed by `σ ⊕ κ` such that the images
of `dxₖ` for `k : κ` span `Ω[S⁄R]` and the span of the `dXₖ` for `k : κ` in
`S ⊗[R] Ω[R[Xᵢ⁄R]]` intersects the kernel of the projection trivially, then the restriction of
`I/I² → ⊕ S dxᵢ` to the direct sum indexed by `i : ι` is an isomorphism.

The assumptions are in particular satisfied if the `dsₖ` form an `S`-basis of `Ω[S⁄R]`,
see `Generators.disjoint_ker_toKaehler_of_linearIndependent` for one half.
Via `PreSubmersivePresentation.isUnit_jacobian_of_cotangentRestrict_bijective`, this can be useful
to show a presentation is submersive.
 -/
Algebra.Generators.cotangentRestrict_bijective_of_isCompl : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_3}
  {σ : Type u_4} {κ : Type u_5} (P : Algebra.Generators R S ι) {u : σ → ι} (hu : Function.Injective u) {v : κ → ι},
  IsCompl (Set.range v) (Set.range u) →
    Submodule.span S (Set.range fun i => (KaehlerDifferential.D R S) (P.val (v i))) = ⊤ →
      Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x => P.cotangentSpaceBasis (v x))) →
        ∀ [Subsingleton (Algebra.H1Cotangent R S)], Function.Bijective ⇑(P.cotangentRestrict hu)
-- Mathlib.Algebra.Algebra.Hom
RingHom.toIntAlgHom_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (x : R), f.toIntAlgHom x = f x
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.coconeOfLE_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J] {j : J}
  (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j),
  (CategoryTheory.SmallObject.coconeOfLE F hi).pt = F.obj ⟨i, hi⟩
-- Aesop.Rule.Name
Aesop.ScopeName : Type
-- Std.Time.Date.Unit.Week
Std.Time.Week.instOrdOrdinal : Ord Std.Time.Week.Ordinal
-- Mathlib.Analysis.LConvolution
MeasureTheory.mlconvolution_assoc₀ : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Group G] [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [MeasureTheory.SFinite μ] {f g k : G → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g μ →
      AEMeasurable k μ →
        MeasureTheory.mlconvolution f (MeasureTheory.mlconvolution g k μ) μ =
          MeasureTheory.mlconvolution (MeasureTheory.mlconvolution f g μ) k μ
-- Mathlib.Tactic.DefEqTransformations
/-- `eta_reduce at loc` eta reduces all sub-expressions at the given location.
This also exists as a `conv`-mode tactic.

For example, `fun x y => f x y` becomes `f` after eta reduction.
 -/
Mathlib.Tactic.etaReduceStx : Lean.ParserDescr
-- Mathlib.Logic.Equiv.Set
Equiv.Set.univ_symm_apply : ∀ (α : Type u_3) (a : α), (Equiv.Set.univ α).symm a = ⟨a, trivial⟩
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.rightAdjointUniq_refl : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G), (adj1.rightAdjointUniq adj1).hom = CategoryTheory.CategoryStruct.id G
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.map_sub : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : PartialOrder S] [IsOrderedRing S] [inst_3 : Ring R]
  (abv : AbsoluteValue R S) [NoZeroDivisors S] (a b : R), abv (a - b) = abv (b - a)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.symmetry_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [inst_2 : F.Full] [F.Faithful],
  CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (hg.snd f') = hf'.fst' g