mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Subfunctor.Basic
/-- If `G` is a subfunctor of `F`, then the sections of `G` on `U` forms a subset of sections of
`F` on `U`.  -/
CategoryTheory.Subfunctor.obj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type w)} → CategoryTheory.Subfunctor F → (U : C) → Set (F.obj U)
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.pos_eq : ∀ {s : String} {p q : s.Pos} {s_1 t t' : String}, p.Splits s_1 t → q.Splits s_1 t' → p = q
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → (m₁ \ m₂).getKey? k = none
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.addCommMonoid : {α : Type u} → [CommMonoid α] → AddCommMonoid (Additive α)
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.add_le_left : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommMonoid M] [Lean.Grind.OrderedAdd M]
  {a b : M}, a ≤ b → ∀ (c : M), a + c ≤ b + c
-- Lean.Meta.MethodSpecs
/-- The spec theorem theorem for an instance can be private even if the instance itself is not.
So un-private the name here when looking for a declaration, and finally check if it matches.
Cf. `Lean.Meta.declFromEqLikeName`. Maybe worth collecting this logic in a central place.
 -/
_private.Lean.Meta.MethodSpecs.0.Lean.isSpecThmNameFor : Lean.Environment → Lean.Name → Option Lean.Name
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.mk.sizeOf_spec : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} [inst : SizeOf α] [inst_1 : SizeOf β]
  (toHom : A →g B) (injective' : Function.Injective ⇑toHom),
  sizeOf { toHom := toHom, injective' := injective' } = 1 + sizeOf toHom
-- Lean.Elab.MutualDef
Lean.Elab.instInhabitedDefViewElabHeader : Inhabited Lean.Elab.DefViewElabHeader
-- Mathlib.Algebra.Group.EvenFunction
Function.Odd.smul_even : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] {γ : Type u_3} {f : α → β} {g : α → γ} [inst_1 : Ring β]
  [inst_2 : AddCommGroup γ] [inst_3 : Module β γ], Function.Odd f → Function.Even g → Function.Odd (f • g)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.Tendsto.uniformity_inv_iff : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {f : ι → α × α}
  {l : Filter ι}, Filter.Tendsto f⁻¹ l (uniformity α) ↔ Filter.Tendsto f l (uniformity α)
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_eq_zero_iff : ∀ {a b : ENNReal}, a / b = 0 ↔ a = 0 ∨ b = ⊤
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSpace.comap_process_pi : ∀ {β : Type u_2} {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] (X_1 : (a : δ) → β → X a),
  MeasurableSpace.comap (fun b a => X_1 a b) inferInstance = ⨆ a, MeasurableSpace.comap (X_1 a) inferInstance
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasProd.update : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f : β → α} {a₁ : α} [L.LeAtTop],
  HasProd f a₁ L → ∀ (b : β) [inst_4 : DecidableEq β] (a : α), HasProd (Function.update f b a) (a / f b * a₁) L
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (toPresheafedSpace : AlgebraicGeometry.PresheafedSpace C) →
      toPresheafedSpace.presheaf.IsSheaf → AlgebraicGeometry.SheafedSpace C
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxKeyD.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) (size : ℕ) (k : α)
  (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (x : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      (fallback : α) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback) =
    h_2 size k v l x
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f : ∀ {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]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.Additive]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x i x_1 : ℤ),
  ((K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom.f i).f x_1 =
    CategoryTheory.CategoryStruct.id ((F.obj (K₁.X (i + x))).obj (K₂.X x_1))
-- Mathlib.LinearAlgebra.DFinsupp
/-- A family of submodules over an additive group are independent if and only iff `DFinsupp.lsum`
applied with `Submodule.subtype` is injective.

Note that this is not generally true for `[Semiring R]`; see
`iSupIndep.dfinsupp_lsum_injective` for details.  -/
iSupIndep_iff_dfinsupp_lsum_injective : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Ring R] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] (p : ι → Submodule R N),
  iSupIndep p ↔ Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (p i).subtype)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanIdentifier : Lean.ToJson Lean.Lsp.LeanIdentifier
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
simplyConnectedSpace_iff : ∀ (X : Type u_3) [inst : TopologicalSpace X],
  SimplyConnectedSpace X ↔ Nonempty (FundamentalGroupoid X ≌ CategoryTheory.Discrete Unit)
-- Init.Prelude
/-- Resolves the given name to an overload list of namespaces.  -/
Lean.Macro.Methods.resolveNamespace : Lean.Macro.Methods → Lean.Name → Lean.MacroM (List Lean.Name)
-- Init.Data.Int.Order
Int.toNat_sub_toNat_neg : ∀ (n : ℤ), ↑n.toNat - ↑(-n).toNat = n
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Stream'.cons.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {P : β → Prop}
  (it : Std.IterM m { out // P out }) (it' : Std.IterM m β) (out : β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)),
  Std.Iterators.Types.Attach.Monadic.modifyStep it ⟨Std.IterStep.yield it' out, h⟩ =
    Std.IterStep.yield { internalState := { inner := it', invariant := ⋯ } } ⟨out, ⋯⟩
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_rw₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f₁ f₁' : α → β}
  {f₂ f₂' : α → γ},
  f₁ =ᵐ[μ] f₁' →
    f₂ =ᵐ[μ] f₂' → ∀ (g : β → γ → ENNReal), ∫⁻ (a : α), g (f₁ a) (f₂ a) ∂μ = ∫⁻ (a : α), g (f₁' a) (f₂' a) ∂μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, k ∈ Std.DTreeMap.Raw.Const.ofList l cmp ↔ (List.map Prod.fst l).contains k = true
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.comonEquivalence_unitIso : ∀ (R : Type u) [inst : CommRing R],
  (CoalgCat.comonEquivalence R).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CoalgCat R)).obj x)) ⋯
-- Std.Do.WP.SimpLemmas
Std.Do.WP.monadLift_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α ρ : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m α)
  (Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)),
  (Std.Do.wp (MonadLift.monadLift x)).apply Q = fun s => (Std.Do.wp x).apply (fun a => Q.1 a s, Q.2)
-- Mathlib.Order.Category.Preord
_private.Mathlib.Order.Category.Preord.0.Preord.Hom.mk.inj : ∀ {X Y : Preord} {hom' hom'_1 : ↑X →o ↑Y}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.quotient_map_eq_zero_iff : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ⟶ D),
  (HomotopyCategory.quotient V c).map f = 0 ↔ Nonempty (Homotopy f 0)
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.trans : ∀ {α : Type u} {β : Type v} {l : Filter α} {f g h : α → β}, f =ᶠ[l] g → g =ᶠ[l] h → f =ᶠ[l] h
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.IsIsolated.not_isUniversal : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [Nontrivial V], G.IsIsolated v → ∀ (w : V), ¬G.IsUniversal w
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullback.π_arrow : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π arrows j) (arrows j) =
    CategoryTheory.Limits.WidePullback.base arrows
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- Comparison test of convergence of `ℝ≥0`-valued series.  -/
NNReal.exists_le_hasSum_of_le : ∀ {β : Type u_2} {f g : β → NNReal} {r : NNReal}, (∀ (b : β), g b ≤ f b) → HasSum f r → ∃ p ≤ r, HasSum g p
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iio_eq_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, LowerSet.Iio a = ⊥ ↔ a = ⊥
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- A helper function for `sumRingEquiv`.  -/
MvPolynomial.mvPolynomialEquivMvPolynomial : (R : Type u) →
  (S₁ : Type v) →
    (S₂ : Type w) →
      (S₃ : Type x) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S₃] →
            (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) →
              (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R) →
                (f.comp g).comp MvPolynomial.C = MvPolynomial.C →
                  (∀ (n : S₂), f (g (MvPolynomial.X n)) = MvPolynomial.X n) →
                    (g.comp f).comp MvPolynomial.C = MvPolynomial.C →
                      (∀ (n : S₁), g (f (MvPolynomial.X n)) = MvPolynomial.X n) →
                        MvPolynomial S₁ R ≃+* MvPolynomial S₂ S₃
-- Mathlib.Order.InitialSeg
PrincipalSeg.ofElement_apply : ∀ {α : Type u_4} (r : α → α → Prop) (a : α) (b : { x // r x a }), (PrincipalSeg.ofElement r a).toRelEmbedding b = ↑b
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
SSet.Augmented.StandardSimplex.shiftFun_zero : ∀ {n : ℕ} {X : Type u_1} [inst : Zero X] (f : Fin n → X), SSet.Augmented.StandardSimplex.shiftFun f 0 = 0
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.map_mul : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) (x y : R), abv (x * y) = abv x * abv y
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Iso.toEquiv_symm_fun : ∀ {X Y : Type u} (i : X ≅ Y), ⇑i.toEquiv.symm = (CategoryTheory.ConcreteCategory.hom i.inv).toFun
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.instInhabited : {R : Type u_1} → [inst : LinearOrder R] → [inst_1 : TopologicalSpace R] → Inhabited (StieltjesFunction R)
-- Aesop.Builder.Basic
Aesop.CoreRuleBuilderOutput : Type
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- `pointWeightsWithCircumcenter` sums to 1.  -/
Affine.Simplex.sum_pointWeightsWithCircumcenter : ∀ {n : ℕ} (i : Fin (n + 1)), ∑ j, Affine.Simplex.pointWeightsWithCircumcenter i j = 1
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_surjective : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c : P) {R : ℝ}, R ≠ 0 → Function.Surjective (EuclideanGeometry.inversion c R)
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.Adjunction.id.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Adjunction.id =
    { unit := CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.id C),
      counit := CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).comp (CategoryTheory.Functor.id C)),
      left_triangle_components := ⋯, right_triangle_components := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftHomologyIso_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp S₁.leftHomologyIso.inv (CategoryTheory.ShortComplex.leftHomologyMap φ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) S₂.leftHomologyIso.inv
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange.equiv_apply : ∀ {ι : Type u_3} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (e : M ≃ N) (hf : e 0 = 0)
  (g : ι →₀ M), (Finsupp.mapRange.equiv e hf) g = Finsupp.mapRange (⇑e) hf g
-- Mathlib.Analysis.Normed.Module.Basic
NormedSpace.ext : ∀ {𝕜 : Type u_6} {E : Type u_7} {inst : NormedField 𝕜} {inst_1 : SeminormedAddCommGroup E} {x y : NormedSpace 𝕜 E},
  SMul.smul = SMul.smul → x = y
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.Lex.wellFounded_of_finite : ∀ {ι : Type u_1} {α : ι → Type u_2} (r : ι → ι → Prop) {s : (i : ι) → α i → α i → Prop} [IsStrictTotalOrder ι r]
  [Finite ι] [inst : (i : ι) → Zero (α i)], (∀ (i : ι), WellFounded (s i)) → WellFounded (DFinsupp.Lex r s)
-- Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
BoxIntegral.Box.upper_sub_lower_splitCenterBox : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Set ι) (i : ι),
  (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_le_ramificationIdx'`. -/
Ideal.ramificationIdx_le_ramificationIdx : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  {T : Type u_2} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T]
  (Q : Ideal T),
  p = Ideal.comap (algebraMap R S) P → p.ramificationIdx' Q ≠ 0 → P.ramificationIdx' Q ≤ p.ramificationIdx' Q
-- Mathlib.Analysis.Normed.Module.MStructure
IsMprojection.proj : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] {P : M},
  IsMprojection X P → IsIdempotentElem P
-- Lean.Elab.DefView
Lean.Elab.Command.mkDefViewOfDef : Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.DefView
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_sdiff_eq_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, μ s = ⊤ → μ t ≠ ⊤ → μ (s \ t) = ⊤
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_addMonoidHom_mk : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α → β) (h₁ : f 1 = 1)
  (h₂ :
    ∀ (x_2 y : α),
      { toFun := f, map_one' := h₁ }.toFun (x_2 * y) =
        { toFun := f, map_one' := h₁ }.toFun x_2 * { toFun := f, map_one' := h₁ }.toFun y)
  (h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0)
  (h₄ :
    ∀ (x_2 y : α),
      (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x_2 + y) =
        (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x_2 +
          (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y),
  ↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ } =
    { toFun := f, map_zero' := h₃, map_add' := h₄ }
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.star_neg : ∀ (z : Complex.UnitDisc), star (-z) = -star z
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.instPartialOrder : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {u : ι → Set X} → {s : Set X} → {p : Set X → Prop} → PartialOrder (ShrinkingLemma.PartialRefinement u s p)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_eq_append : ∀ {m n : ℤ}, m < n → (m<...=n).toList = (m<...=n - 1).toList ++ [n]
-- Mathlib.Algebra.Tropical.Basic
Tropical.decidableLT : {R : Type u} → [inst : LT R] → [DecidableLT R] → DecidableLT (Tropical R)
-- Mathlib.Data.Finset.Max
Finset.exists_next_left : ∀ {α : Type u_2} [inst : LinearOrder α] {x : α} {s : Finset α},
  (∃ y ∈ s, y < x) → ∃ y ∈ s, y < x ∧ ∀ z ∈ s, z < x → z ≤ y
-- Mathlib.Topology.ContinuousMap.Defs
/-- Proposition that `toFun` is continuous  -/
ContinuousMap.continuous_toFun : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (self : C(X, Y)),
  Continuous self.toFun
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite coproducts, then `F.unop : C ⥤ D` preserves finite
products.  -/
CategoryTheory.Limits.preservesFiniteProducts_unop : ∀ {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.PreservesFiniteCoproducts F],
  CategoryTheory.Limits.PreservesFiniteProducts F.unop
-- Init.Data.RArray
Lean.RArray.brecOn.go : {α : Type u} →
  {motive : Lean.RArray α → Sort u_1} →
    (t : Lean.RArray α) → ((t : Lean.RArray α) → Lean.RArray.below t → motive t) → motive t ×' Lean.RArray.below t
-- Mathlib.CategoryTheory.Triangulated.Rotate
/-- Rotating triangles gives an endofunctor on the category of triangles in `C`.
 -/
CategoryTheory.Pretriangulated.rotate : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C) (CategoryTheory.Pretriangulated.Triangle C)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.leftRight : Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
/-- A morphism is separated if the diagonal map is a closed immersion.  -/
AlgebraicGeometry.IsSeparated : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.Topology.Constructions.SumProd
/-- The first projection in a product of topological spaces sends open sets to open sets.  -/
isOpenMap_fst : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsOpenMap Prod.fst
-- Mathlib.MeasureTheory.Measure.AddContent
/-- If an additive content is continuous from below on monotone sequences of sets,
then it is countably additive on pairwise disjoint sequences.  -/
MeasureTheory.addContent_iUnion_eq_tsum_of_addContent_iUnion_eq_iSup : ∀ {α : Type u_1} {C : Set (Set α)},
  MeasureTheory.IsSetRing C →
    ∀ (m : MeasureTheory.AddContent ENNReal C) {s : ℕ → Set α},
      Pairwise (Function.onFun Disjoint s) →
        (∀ (i : ℕ), s i ∈ C) →
          (∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Monotone s → m (⋃ n, s n) = ⨆ n, m (s n)) →
            m (⋃ i, s i) = ∑' (i : ℕ), m (s i)
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.coe_finset : ∀ (α : Type u_1) (n : ℕ) [inst : Fintype α], Set.powersetCard α n = ↑(Finset.powersetCard n Finset.univ)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.instCoeFunHomForallCarrierCarrierCommRingCat : {X Y : AlgebraicGeometry.Scheme} → CoeFun (X ⟶ Y) fun x => ↥X → ↥Y
-- Lean.Meta.HaveTelescope
/-- Routine for simplifying `have` telescopes. Used by `simpLet`.
This is optimized to be able to handle deep `have` telescopes while avoiding quadratic complexity
arising from the locally nameless expression representations.

## Overview

Consider a `have` telescope:
```
have x₁ : T₁ := v₁; ...; have xₙ : Tₙ := vₙ; b
```
We say `xᵢ` is *fixed* if it appears in the type of `b`.
If `xᵢ` is fixed, then it can only be rewritten using definitional equalities.
Otherwise, we can freely rewrite the value using a propositional equality `vᵢ = vᵢ'`.
The body `b` can always be freely rewritten using a propositional equality `b = b'`.
(All the mentioned equalities must be type correct with respect to the obvious local contexts.)

If `xᵢ` neither appears in `b` nor any `Tⱼ` nor any `vⱼ`, then its `have` is *unused*.
Unused `have`s can be eliminated, which we do if `cfg.zetaUnused` is true.
We clear `have`s from the end, to be able to transitively clear chains of unused `have`s.
This is why we honor `zetaUnused` here even though `reduceStep` is also responsible for it;
`reduceStep` can only eliminate unused `have`s at the start of a telescope.
Eliminating all transitively unused `have`s at once like this also avoids quadratic complexity.

If `debug.simp.check.have` is enabled then we typecheck the resulting expression and proof.

## Proof generation

There are two main complications with generating proofs.
1. We work almost exclusively with expressions with loose bound variables,
   to avoid overhead from instantiating and abstracting free variables,
   which can lead to complexity quadratic in the telescope length.
   (See `HaveTelescopeInfo`.)
2. We want to avoid triggering zeta reductions in the kernel.

Regarding this second point, the issue is that we cannot organize the proof using congruence theorems
in the obvious way. For example, given
```
theorem have_congr {α : Sort u} {β : Sort v} {a a' : α} {f f' : α → β}
    (h₁ : a = a') (h₂ : ∀ x, f x = f' x) :
    (have x := a; f x) = (have x := a'; f' x)
```
the kernel sees that the type of `have_congr (fun x => b) (fun x => b') h₁ h₂`
is `(have x := a; (fun x => b) x) = (have x := a'; (fun x => b') x)`,
since when instantiating values it does not beta reduce at the same time.
Hence, when `is_def_eq` is applied to the LHS and `have x := a; b` for example,
it will do `whnf_core` to both sides.

Instead, we use the form `(fun x => b) a = (fun x => b') a'` in the proofs,
which we can reliably match up without triggering beta reductions in the kernel.
The zeta/beta reductions are then limited to the type hint for the entire telescope,
when we convert this back into `have` form.
In the base case, we include an optimization to avoid unnecessary zeta/beta reductions,
by detecting a `simpHaveTelescope` proofs and removing the type hint.
 -/
Lean.Meta.simpHaveTelescope : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] →
      [MonadControlT Lean.MetaM m] →
        [Lean.Meta.MonadSimp m] →
          Lean.Expr →
            optParam Lean.Meta.ZetaUnusedMode Lean.Meta.ZetaUnusedMode.twoPasses → m Lean.Meta.MonadSimp.Result
-- Aesop.Tree.UnsafeQueue
Aesop.PostponedSafeRule.mk.injEq : ∀ (rule : Aesop.SafeRule) (output : Aesop.RuleTacOutput) (rule_1 : Aesop.SafeRule) (output_1 : Aesop.RuleTacOutput),
  ({ rule := rule, output := output } = { rule := rule_1, output := output_1 }) = (rule = rule_1 ∧ output = output_1)