mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ [inst_1 : Inhabited α] {k k' : α} {f : β k → β k},
      (t.modify k f).getKey! k' = if cmp k k' = Ordering.eq then if k ∈ t then k else default else t.getKey! k'
-- Mathlib.Algebra.Group.Action.Option
Option.instMulAction : {M : Type u_1} → {α : Type u_3} → [inst : Monoid M] → [MulAction M α] → MulAction M (Option α)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
/-- Note that the hypothesis `0 ≤ a` is necessary because the continuous functional calculi over
`ℝ≥0` (for the left-hand side) and `ℝ` (for the right-hand side) use different predicates (i.e.,
`(0 ≤ ·)` versus `IsSelfAdjoint`). Consequently, if `a` is selfadjoint but not nonnegative, then
the left-hand side is zero, but the right-hand side is (provably equal to) `CFC.sqrt a⁺`.  -/
CFC.sqrt_eq_real_sqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] (a : A),
  autoParam (0 ≤ a) CFC.sqrt_eq_real_sqrt._auto_1 → CFC.sqrt a = cfcₙ Real.sqrt a
-- Mathlib.Analysis.Convex.Intrinsic
/-- If `f` agrees with a homeomorphism between the affine spans of `s` and `f '' s`, then pulling
`f '' s` back to the affine span of `s` recovers `s` itself.  -/
_private.Mathlib.Analysis.Convex.Intrinsic.0.preimage_image_eq_of_homeomorph_affineSpan : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V]
  [inst_2 : Module 𝕜 V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module 𝕜 W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] {f : P → Q} {s : Set P}
  (e : ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))),
  IsHomeomorph e → (∀ (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x) → f ∘ Subtype.val ⁻¹' f '' s = Subtype.val ⁻¹' s
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesOfIsMulCocycle₂_coe : ∀ {G M : Type} [inst : Group G] [inst_1 : CommGroup M] [inst_2 : MulDistribMulAction G M] {f : G × G → M}
  (hf : groupCohomology.IsMulCocycle₂ f) (a : G × G),
  ↑(groupCohomology.cocyclesOfIsMulCocycle₂ hf) a = (⇑Additive.ofMul ∘ f) a
-- Mathlib.Data.Nat.Size
Nat.size_eq_bits_len : ∀ (n : ℕ), n.bits.length = n.size
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Given `P : Prop` and `a : α`, traverses the expression `P` to find a subexpression of
the form `a = a'` or `a' = a` for some `a'`. It branches at each `And` and walks into
existential quantifiers.

Returns a tuple `(fvars, lctx, P', a')`, where:
* `fvars` is a list of all variables bound by existential quantifiers along the path.
* `lctx` is the local context containing all these free variables.
* `P'` is `P` with all existential quantifiers along the path removed, and corresponding bound
  variables replaced with `fvars`.
* `a'` is the expression found that must be equal to `a`.
  It may contain free variables from `fvars`.  -/
ExistsAndEq.findEq : {u : Lean.Level} →
  {α : Q(Sort u)} →
    Q(«$α») → Q(Prop) → ExistsAndEq.Path → Lean.MetaM (List ExistsAndEq.VarQ × Lean.LocalContext × Q(Prop) × Q(«$α»))
-- Batteries.Data.Vector.Lemmas
Vector.toList_scanr : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {init : β} {f : α → β → β} {as : Vector α n},
  (Vector.scanr f init as).toList = List.scanr f init as.toList
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
powers_eq_top_of_prime_card : ∀ {G : Type u_2} [inst : Group G] {p : ℕ} [hp : Fact (Nat.Prime p)],
  Nat.card G = p → ∀ {g : G}, g ≠ 1 → Submonoid.powers g = ⊤
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.weakEquivalence_of_precomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [hf : HomotopicalAlgebra.WeakEquivalence f]
  [hfg : HomotopicalAlgebra.WeakEquivalence (CategoryTheory.CategoryStruct.comp f g)],
  HomotopicalAlgebra.WeakEquivalence g
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- The seminorms on the space `𝓓^{n}_{K}(E, F)` given by sup of the
`ContDiffMapSupportedIn.seminorm k`for `k ≤ i`.  -/
ContDiffMapSupportedIn.supSeminorm : (𝕜 : Type u_1) →
  (E : Type u_2) →
    (F : Type u_3) →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace ℝ E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace ℝ F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    (n : ℕ∞) → (K : TopologicalSpace.Compacts E) → ℕ → Seminorm 𝕜 (ContDiffMapSupportedIn E F n K)
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumElim_zero_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ], Finsupp.sumElim 0 0 = 0
-- Batteries.Util.ProofWanted
/-- Fresh identifier naming the surfaced binder. Also spliced into the referenced wanted's
application, so the dependency is passed through.  -/
_private.Batteries.Util.ProofWanted.0.WantedDep.ident : WantedDep✝ → Lean.TSyntax `ident
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the coherence isomorphism `⊗𝟙 : f ⟶ g`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.coherenceHomM' : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Mor₁ → Lean.Expr → m Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.Data.PNat.Interval
PNat.Ioo_eq_finset_subtype : ∀ (a b : ℕ+), Finset.Ioo a b = Finset.subtype (fun n => 0 < n) (Finset.Ioo ↑a ↑b)
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.instDeterministicCounit : ∀ {X : SFinKer}, CategoryTheory.Deterministic CategoryTheory.ComonObj.counit
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instRankPosElemERestrictSubtype : ∀ {α : Type u_1} {M : Matroid α} [M.RankPos], (M.restrictSubtype M.E).RankPos
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.chart_mem_atlas : ∀ {H : Type u_5} {inst : TopologicalSpace H} {M : Type u_6} {inst_1 : TopologicalSpace M} [self : ChartedSpace H M]
  (x : M), ChartedSpace.chartAt x ∈ ChartedSpace.atlas
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.Homotopy.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (H : (i : E.I₀) → F.I₁ (f.s₀ i) (g.s₀ i))
  (a : (i : E.I₀) → E.X i ⟶ F.Y (H i))
  (wl : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a i) (F.p₁ (H i)) = f.h₀ i)
  (wr : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a i) (F.p₂ (H i)) = g.h₀ i)
  (H_1 : (i : E.I₀) → F.I₁ (f.s₀ i) (g.s₀ i)) (a_1 : (i : E.I₀) → E.X i ⟶ F.Y (H_1 i))
  (wl_1 : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a_1 i) (F.p₁ (H_1 i)) = f.h₀ i)
  (wr_1 : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a_1 i) (F.p₂ (H_1 i)) = g.h₀ i),
  ({ H := H, a := a, wl := wl, wr := wr } = { H := H_1, a := a_1, wl := wl_1, wr := wr_1 }) = (H = H_1 ∧ a ≍ a_1)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.preimage_toSnowflaking_closedEBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁)
  (d : ENNReal),
  ⇑Metric.Snowflaking.toSnowflaking ⁻¹' Metric.closedEBall x d =
    Metric.closedEBall (Metric.Snowflaking.ofSnowflaking x) (d ^ α⁻¹)
-- Mathlib.Algebra.Regular.Basic
/-- In a semigroup, the product of left-regular elements is left-regular.  -/
IsLeftRegular.mul : ∀ {R : Type u_1} [inst : Semigroup R] {a b : R}, IsLeftRegular a → IsLeftRegular b → IsLeftRegular (a * b)
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
DifferentiableAt.restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → F} {x : E},
  DifferentiableAt 𝕜' f x → DifferentiableAt 𝕜 f x
-- Init.Data.SInt.Lemmas
Int32.toBitVec_ofIntLE : ∀ (x : ℤ) (h₁ : Int32.minValue.toInt ≤ x) (h₂ : x ≤ Int32.maxValue.toInt),
  (Int32.ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 32 x
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.tryAddSyntaxNodeKindInfo : Lean.Syntax → Lean.SyntaxNodeKind → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.δ_L₃_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp S.δ S.L₃.f = 0
-- Init.Data.Array.Extract
Array.takeWhile_filter : ∀ {α : Type u_1} {p q : α → Bool} {as : Array α},
  Array.takeWhile q (Array.filter p as) = Array.filter p (Array.takeWhile (fun a => !p a || q a) as)
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.le_def : ∀ (x y : ℝ), Real.le✝ x y = (x < y ∨ x = y)
-- Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
SummableLocallyUniformlyOn.of_locally_bounded_eventually : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [CompleteSpace F]
  [inst_2 : TopologicalSpace β] [LocallyCompactSpace β] {f : α → β → F} {s : Set β},
  IsOpen s →
    (∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ᶠ (n : α) in Filter.cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n) →
      SummableLocallyUniformlyOn f s
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.coindep_iff_subset_compl_isBase : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Coindep X ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E \ B
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).Q = S.X₂
-- Mathlib.Algebra.Exact.Basic
/-- Two maps `f : M → N` and `g : N → P` are exact if and only if the induced maps
`Set.range f → N → Set.range g` are exact.

Note that if you already have an instance `[Zero (Set.range g)]` (which is unlikely) this lemma
may not apply if the zero of `Set.range g` is not definitionally equal to `⟨0, hg⟩`.  -/
Function.Exact.iff_rangeFactorization : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : Zero P] (hg : 0 ∈ Set.range g),
  Function.Exact f g ↔ Function.Exact Subtype.val (Set.rangeFactorization g)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.prod : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {α : Type u_5}
  {s : Finset α} (f : α → A), (∀ x ∈ s, IsIntegral R (f x)) → IsIntegral R (∏ x ∈ s, f x)
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
HopfAlgCat.leftUnitor_def : ∀ (R : Type u) [inst : CommRing R] (X : HopfAlgCat R),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor X = (Bialgebra.TensorProduct.lid R X.carrier).toHopfAlgIso
-- Mathlib.Logic.Relator
Relator.LeftTotal.refl : ∀ {α : Type u_1} {r₁₁ : α → α → Prop}, (∀ (a : α), r₁₁ a a) → Relator.LeftTotal r₁₁
-- Mathlib.Analysis.Convex.Topology
/-- If we dilate the interior of a convex set about a point in its interior by a scale `t > 1`,
the result includes the closure of the original set.

TODO Generalise this from convex sets to sets that are balanced / star-shaped about `x`.  -/
Convex.closure_subset_image_homothety_interior_of_one_lt : ∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] {s : Set E},
  Convex ℝ s → ∀ {x : E}, x ∈ interior s → ∀ (t : ℝ), 1 < t → closure s ⊆ ⇑(AffineMap.homothety x t) '' interior s
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (fvarId : Lean.FVarId) (attrs : Array Lean.Elab.Attribute) (shortDeclName declName : Lean.Name)
  (parentName? : Option Lean.Name) (lctx : Lean.LocalContext) (localInstances : Lean.LocalInstances)
  (type val : Lean.Expr) (mvarId : Lean.MVarId) (termination : Lean.Elab.TerminationHints) (binders : Lean.Syntax)
  (docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)),
  sizeOf
      { ref := ref, fvarId := fvarId, attrs := attrs, shortDeclName := shortDeclName, declName := declName,
        parentName? := parentName?, lctx := lctx, localInstances := localInstances, type := type, val := val,
        mvarId := mvarId, termination := termination, binders := binders, docString? := docString? } =
    1 + sizeOf ref + sizeOf fvarId + sizeOf attrs + sizeOf shortDeclName + sizeOf declName + sizeOf parentName? +
                    sizeOf lctx +
                  sizeOf localInstances +
                sizeOf type +
              sizeOf val +
            sizeOf mvarId +
          sizeOf termination +
        sizeOf binders +
      sizeOf docString?
-- Init.Tactics
/-- `simp_all` is a stronger version of `simp [*] at *` where the hypotheses and target
are simplified multiple times until no simplification is applicable.
Only non-dependent propositional hypotheses are considered.
 -/
Lean.Parser.Tactic.simpAll : Lean.ParserDescr
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.contained_C' : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2), Profinite.NobelingProof.contained (Profinite.NobelingProof.C' C ho) o
-- Aesop.Index.Basic
Aesop.IndexingMode : Type
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_smul_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_8} [inst_1 : NormedDivisionRing 𝕜] [inst_2 : MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜},
  c ≠ 0 → ∀ (f : α → β), MeasureTheory.Integrable (c • f) μ ↔ MeasureTheory.Integrable f μ
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.noetherianSpace_iff_opens : ∀ (α : Type u_1) [inst : TopologicalSpace α],
  TopologicalSpace.NoetherianSpace α ↔ ∀ (s : TopologicalSpace.Opens α), IsCompact ↑s
-- Mathlib.Analysis.Complex.CoveringMap
/-- `(· ^ n) : 𝕜 \ {0} → 𝕜 \ {0}` is a covering map (if `n ≠ 0` in `𝕜`).  -/
isCoveringMap_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (n : ℤ), ↑n ≠ 0 → IsCoveringMap fun x => ⟨↑x ^ n, ⋯⟩
-- Mathlib.Data.Set.Finite.Basic
/-- Induction principle for finite sets: To prove a property `motive` of a finite set `s`, it's
enough to prove for the empty set and to prove that `motive t → motive ({a} ∪ t)` for all `t`.

See also `Set.Finite.induction_on_subset` for the version requiring to check
`motive t → motive ({a} ∪ t)` only for `t ⊆ s`.  -/
Set.Finite.induction_on : ∀ {α : Type u} {motive : (s : Set α) → s.Finite → Prop} (s : Set α) (hs : s.Finite),
  motive ∅ ⋯ → (∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (insert a s) ⋯) → motive s hs
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.add_measure_left : ∀ {α : Type u_1} {β : Type u_7} [inst : SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {x : MeasurableSpace α}
  (μ ν : MeasureTheory.Measure α),
  MeasureTheory.DominatedFinMeasAdditive ν T C → 0 ≤ C → MeasureTheory.DominatedFinMeasAdditive (μ + ν) T C
-- Mathlib.Logic.Relation
Relation.transGen_swap : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Relation.TransGen (Function.swap r) a b ↔ Relation.TransGen r b a
-- Init.Data.List.MinMax
List.min.congr_simp : ∀ {α : Type u} [inst : Min α] (l l_1 : List α) (e_l : l = l_1) (h : l ≠ []), l.min h = l_1.min ⋯
-- Mathlib.Tactic.Sat.FromLRAT
/-- Asserts that `¬⟦l⟧_v` implies `p`.  -/
Sat.Literal.reify : Sat.Valuation → Sat.Literal → Prop → Prop
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on
`x * S`.  -/
QuotientGroup.instNorm : {M : Type u_1} → [inst : SeminormedCommGroup M] → {S : Subgroup M} → Norm (M ⧸ S)
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.PreservesRxcSize.size_eq : ∀ {α : Type u_1} {β : Type u_2} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : Std.PRange.UpwardEnumerable β}
  {inst_2 : Std.Rxc.HasSize α} {inst_3 : Std.Rxc.HasSize β} {f : Std.PRange.UpwardEnumerable.Map α β}
  [self : f.PreservesRxcSize] {a b : α}, Std.Rxc.HasSize.size a b = Std.Rxc.HasSize.size (f.toFun a) (f.toFun b)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
CategoryTheory.Functor.mem_inducedTopology_iff_of_isCoverDense : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K]
  [G.IsCoverDense K] {X : C} (S : CategoryTheory.Sieve X),
  S ∈ (G.inducedTopology K) X ↔ CategoryTheory.Sieve.functorPushforward G S ∈ K (G.obj X)
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.ext_iff : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {x y : SSet.RelativeMorphism A B φ},
  x = y ↔ x.map = y.map
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
/-- **Divergence theorem** for functions on the plane along rectangles. It is formulated in terms of
two functions `f g : ℝ × ℝ → E` and an integral over `Icc a b = [a.1, b.1] × [a.2, b.2]`, where
`a b : ℝ × ℝ`, `a ≤ b`. When thinking of `f` and `g` as the two coordinates of a single function
`F : ℝ × ℝ → E × E` and when `E = ℝ`, this is the usual statement that the integral of the
divergence of `F` inside the rectangle equals the integral of the normal derivative of `F` along the
boundary.

See also `MeasureTheory.integral2_divergence_prod_of_hasFDerivAt` for a
version that does not assume `a ≤ b` and uses iterated interval integral instead of the integral
over `Icc a b`.

See also `integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le`
for a version that assumes differentiability out of a countable set.  -/
MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_of_le : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f g : ℝ × ℝ → E)
  (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a b : ℝ × ℝ),
  a ≤ b →
    ContinuousOn f (Set.Icc a b) →
      ContinuousOn g (Set.Icc a b) →
        (∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2, HasFDerivAt f (f' x) x) →
          (∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2, HasFDerivAt g (g' x) x) →
            MeasureTheory.IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) MeasureTheory.volume →
              ∫ (x : ℝ × ℝ) in Set.Icc a b, (f' x) (1, 0) + (g' x) (0, 1) =
                (((∫ (x : ℝ) in a.1..b.1, g (x, b.2)) - ∫ (x : ℝ) in a.1..b.1, g (x, a.2)) +
                    ∫ (y : ℝ) in a.2..b.2, f (b.1, y)) -
                  ∫ (y : ℝ) in a.2..b.2, f (a.1, y)
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.shadow.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (𝒜 : Finset (Finset α)), 𝒜.shadow = 𝒜.sup fun s => Finset.image s.erase s
-- Mathlib.Topology.Bornology.Constructions
Bornology.isBounded_prod_self : ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, Bornology.IsBounded (s ×ˢ s) ↔ Bornology.IsBounded s
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitRightOpIsoOpColimit_inv_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).inv
      (CategoryTheory.Limits.limit.π F.rightOp j) =
    (CategoryTheory.Limits.colimit.ι F (Opposite.op j)).op
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchClone.toNatLit? : Lean.Expr → Option Lean.Literal
-- Mathlib.Data.UInt
USize.instNonUnitalCommRing : NonUnitalCommRing USize
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.mvqpfFix : {n : ℕ} → {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → MvQPF (MvQPF.Fix F)
-- Mathlib.Data.Option.NAry
/-- If `a` is a left identity for a binary operation `f`, then `some a` is a left identity for
`Option.map₂ f`.  -/
Option.map₂_left_identity : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {a : α},
  (∀ (b : β), f a b = b) → ∀ (o : Option β), Option.map₂ f (some a) o = o
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.Indep.contract_dep_iff : ∀ {α : Type u_1} {M : Matroid α} {I J : Set α}, M.Indep I → ((M.contract I).Dep J ↔ Disjoint J I ∧ M.Dep (J ∪ I))
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.inclLeft_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (a : C), (CategoryTheory.Join.inclLeft C D).obj a = CategoryTheory.Join.left a
-- Init.Data.Rat.Lemmas
Rat.le_iff_eq_or_lt : ∀ {a b : ℚ}, a ≤ b ↔ a < b ∨ a = b
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomCompTriple.mk : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : outParam (R₁ →+* R₃)}, σ₂₃.comp σ₁₂ = σ₁₃ → RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftAlgHom_apply_ofFractionRing_mk : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} {S : Type u_3} [inst_2 : Field L]
  [inst_3 : CommSemiring S] [inst_4 : Algebra S (Polynomial K)] [inst_5 : Algebra S L] (φ : Polynomial K →ₐ[S] L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (n : Polynomial K)
  (d : ↥(nonZeroDivisors (Polynomial K))),
  (RatFunc.liftAlgHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d
-- Mathlib.Data.Finset.Insert
/-- `insert a s` is the set `{a} ∪ s` containing `a` and the elements of `s`.  -/
Finset.instInsert : {α : Type u_1} → [DecidableEq α] → Insert α (Finset α)
-- Init.Omega.Constraint
Lean.Omega.Constraint.exact_sat : ∀ (r t : ℤ), (Lean.Omega.Constraint.exact r).sat t = decide (r = t)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pullbacks_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C)
  [P.IsStableUnderBaseChange], P.pullbacks ≤ P
-- Aesop.Script.Util
Aesop.Script.matchGoals : Lean.Meta.SavedState →
  Lean.Meta.SavedState →
    Array Lean.MVarId → Array Lean.MVarId → Lean.MetaM (Option (Std.HashMap Lean.MVarId Lean.MVarId))
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.nnratCast : ∀ {R : Type u_1} [inst : DivisionSemiring R] [inst_1 : StarRing R] (q : ℚ≥0), IsSelfAdjoint ↑q
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `MDifferentiableAt.smul` -/
MDifferentiableAt.fun_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] {x : M} {V : Type u_18} [inst_6 : NormedAddCommGroup V]
  [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V}, MDiffAt f x → MDiffAt g x → (MDiffAt fun i => f i • g i) x
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq.eq_def : ∀ (e : Lean.Grind.AC.Expr),
  e.toSeq =
    match e with
    | Lean.Grind.AC.Expr.var x => Lean.Grind.AC.Seq.var x
    | a.op b => a.toSeq' b.toSeq